For some queries (especially in symbolic execution of binary programs), it is significantly faster to provide bit rotation expressions directly to Z3 (where they can be inferred) instead of using a bitwise-or of a right shift and left shift. SMT-LIB2 does not have non-indexed bit rotates in the bitvector theory, but Z3 provides the custom operations ext_rotate_left and ext_rotate_right. I only use Z3, but I also tried to find out how other solvers do this, and from my quick survey:
- Z3, Boolector:
ext_rotate_{left,right}
- Bitwuzla:
bvrol/bvror
- CVC4, CVC5, Yices2, STP: no support
It would be very useful to be able to output these operations in SMT queries, but given the inconsistent support in other solvers, I'm not sure what the best way to accomplish this could be. Some ideas:
- Reimplement
bvrol and bvror in Rosette as symbolic operations, and lower a solver-specific form or left+right shift depending on the solver in use
- Provide a generic interface for programs to be able to use custom SMT-LIB2 operations
I already have a basic patch where I add ext_rotate_left and ext_rotate_right directly (in a way that only supports Z3 for now and probably breaks every other solver except for maybe Boolector, but this works for what I needed). But I can contribute a more complete implementation, so I would appreciate some guidance on the above.
For some queries (especially in symbolic execution of binary programs), it is significantly faster to provide bit rotation expressions directly to Z3 (where they can be inferred) instead of using a bitwise-or of a right shift and left shift. SMT-LIB2 does not have non-indexed bit rotates in the bitvector theory, but Z3 provides the custom operations
ext_rotate_leftandext_rotate_right. I only use Z3, but I also tried to find out how other solvers do this, and from my quick survey:ext_rotate_{left,right}bvrol/bvrorIt would be very useful to be able to output these operations in SMT queries, but given the inconsistent support in other solvers, I'm not sure what the best way to accomplish this could be. Some ideas:
bvrolandbvrorin Rosette as symbolic operations, and lower a solver-specific form or left+right shift depending on the solver in useI already have a basic patch where I add
ext_rotate_leftandext_rotate_rightdirectly (in a way that only supports Z3 for now and probably breaks every other solver except for maybe Boolector, but this works for what I needed). But I can contribute a more complete implementation, so I would appreciate some guidance on the above.