The Axe toolkit provides several tools for lifting code into logic. Currently, Axe can lift JVM bytecode, x86 binaries, and rank-1 constraint systems.
For lifting JVM bytecode, four lifters are available. For code that is unrollable, use unroll-java-code (or try the more experimental unroll-java-code2, for compositional lifting). When loops cannot be unrolled and so must be lifted into recursive functions, use
For lifting x86 binaries, two lifters are available. For code that is unrollable, use
For lifting rank-1 constraint systems, use r1cs::lift-r1cs or one of its variants.