CrossHair icon indicating copy to clipboard operation
CrossHair copied to clipboard

Implement true floating point semantics

Open pschanely opened this issue 2 years ago • 0 comments

One big gotcha with CrossHair and floats: For performance reasons CrossHair approximates floating point behavior using true (arbitrary precision) real numbers.

Z3 is technically capable of doing floating-point-accurate symbolic execution. However, those capabilities are very slow; it might take O(minutes) to reason about a single floating point operation. In an ideal world, we might try both approaches.

Originally posted by @pschanely in https://github.com/pschanely/CrossHair/issues/188#issuecomment-1322620429

pschanely avatar Nov 16 '23 16:11 pschanely