CrossHair
CrossHair copied to clipboard
Implement true floating point semantics
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