search

dwrensha / seer

symbolic execution engine for Rust
Other
345 stars 7 forks source link

Support for `numeric_intrinsic`s #7

Closed ranma42 closed 6 years ago

ranma42 commented 6 years ago

The code I am working on uses the cttz intrinsic on PrimVal::Abstract, resulting in a panic on line 624 in intrinsic.rs.

What would be the best approach to implement it? I believe an open-coded implementation (based on comparisons) would work/be required for these intrinsics, as Z3 does not seem to provide them natively.

I would likt to work on these intrinsics, but I just started looking at the code and I might use some directions :)

dwrensha commented 6 years ago

Yeah, it looks like cttz, unlike bswap, is going to require that we add some constraints to the ConstraintContext. Encoding cttz should be possible with the existing variants of Constraint, but perhaps it makes sense to add a new constraint variant -- then all of the complicated logic could go in the contraint_to_ast() method, where you might have a better chance of more naturally handling bit manipulations.

ranma42 commented 6 years ago

I tried to follow your suggestion here: https://github.com/dwrensha/seer/pull/8 More patches coming when I get the design right :)