search

pschanely / CrossHair

An analysis tool for Python that blurs the line between testing and type systems.
Other
1.03k stars 49 forks source link

Implement true floating point semantics #230

Closed pschanely closed 2 months ago

pschanely commented 1 year ago

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 commented 2 months ago

@Zac-HD and anyone else following along: I've been busy working on this recently. I can safely say that this mode will be quite slow, and suspect that the conversions between floats and unbounded integers (which are uniquely bountiful in Python) could turn even simple cases to impossible. Still, I think some use cases could benefit from it, and then we'll be prepared for advances on the solving side.

Hoping to have something by this weekend!

pschanely commented 2 months ago

I have an initial version shipped in 0.0.72; this version will, with a low probability, attempt executions down a parallel path tree that implements true-float semantics instead of the real-based ones. The main thing I'm still missing is something to validate real-based executions. In other words, this version attempts to find bugs that the previously implementation missed, but does not help with false positive reports. I'll address those in #309.

@Zac-HD Although this should fix a test or two, there's a good chance that I'll regress on a few, due to the shiny new surface area for bugs.