A program synthesis framework for verified lifting applications
Get Started at metalift.pages.dev
See tests folder for test cases.
Check out any of the python files in that folder to see how to define
your target language and build your own lifting based compiler.
Do not use main.py.
We currently support Rosette (and cvc5 but cvc5 has been flaky) as the synthesis backend, and Z3 as the verifier.
We currently support LLVM 11
Run the following to build the LLVM pass for processing branch instructions (works for LLVM 11):
cd llvm-pass
mkdir build
cd build
cmake ..
make
cd ..
Then run it with:
opt -load build/addEmptyBlocks/libAddEmptyBlocksPass.so -addEmptyBlock -S <.ll name>
This pass is called in tests/compile-add-blocks.
To run synthesis, build CVC5 from source, run configure with debug and then build.
Then run metalift from main.py.
Example synthesis usage: main.py tests/while4.ll tests/while4-grammar.sl tests/out.smt test tests/while4.loops <path to cvc5>
Example verification usage (using pre-generated answer): main.py tests/while4.ll tests/while4-ans.smt tests/out.smt test tests/while4.loops
This prints the verification file to out.smt that can be run using an external solver (e.g., z3)
To get a development environment up and running, one option is to use Nix, which can automatically pull and build the necessary dependencies. First, you'll need to install Nix. Note that this will require temporary root access as Nix sets up a daemon to handle builds, and will set up a separate volume for storing build artifacts if on macOS.
Once you've got Nix installed, you'll need to enable flakes.
Then, all you have to do is navigate to the Metalift directory and run the following command:
$ nix developThis will build all of Metalift's dependencies and drop you into a temporary shell with all the dependencies available.
Note: you still will need to install Racket and Rosette separately. There is a solution for doing this through Nix, but it requires nix-ld to be installed and is generally not recommended unless you run NixOS.
We use Poetry for dependency management. To set up the environment, simply install Poetry, run poetry install, and then poetry shell to enter an environment with the dependencies installed.