		Search-engine friendly clone of the ACL2 documentation.

Lifters

Axe Lifters

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 lift-java-code (or try the more experimental lift-java-code2, for compositional lifting).

For lifting x86 binaries, two lifters are available. For code that is unrollable, use x::def-unrolled (still experimental). When loops cannot be unrolled and so must be lifted into recursive functions, try x::lift-subroutine (very experimental).

For lifting rank-1 constraint systems, use r1cs::lift-r1cs or one of its variants.

Subtopics

Unroll-java-code: Lift a Java method to create a DAG, unrolling loops as needed.
Unroll-java-code2: Given a Java method, define a function that represents the (unrolled) effect of the given method on the JVM state (under the given assumptions). This uses symbolic execution including unrolling all loops.