Skip to main content

Installation

Let's get started by installing Metalift and its dependencies!

Get the Metalift source code​

First, you'll need to clone the Metalift repository (we are working on making Metalift available as a Python package in the near future):

git clone https://github.com/metalift/metalift.git
cd metalift

Install the dependencies​

  • Racket as the underlying language for the synthesis engine
  • Rosette, the synthesis engine that Metalift uses
    • For maximum performance on Apple Silicon machines, you may want to replace the built-in Intel binary for Z3 with a native build
  • CVC5, the theorem prover that Metalift uses to check candidate solutions
  • Clang/LLVM 11, to compile input programs to LLVM IR for analysis
  • CMake, to build the custom LLVM pass

Install Python Dependencies​

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.

Installation using Nix​

If you use Nix, you can automatically get all these dependencies using the flake.nix definition in the base directory of the Metalift repository. Once you've got Nix installed, you'll need to enable flakes.

$ nix develop
$ # all dependencies are available!

Build the custom LLVM pass​

Metalift makes use of a custom LLVM pass to organize the basic blocks in a way that is easier to analyze. To build the pass, we'll use CMake:

cd llvm-pass
mkdir build
cd build
cmake ..
make 
cd ../..

Now, we are ready to start building verified lifting systems with Metalift!