Important
Gillian-Rust is a prototype to demonstrate the feasibility of Hybrid Verification for Rust. It is unstable and will provide unclear error messages. For easy installation and experimentation, we recommend taking a look at our PLDI25 artifact. We also provide ARTIFACT.pdf in this repo, though the instructions may be slightly out of sync with this repo.
To build this project, you need to build:
- the Rust-to-GIL compiler (written in Rust, using directly the Rust compiler API); and
- the Gillian-Rust backend, based on the Gillian framework written in OCaml.
To build the compiler, you first need to install Rust. Then, you should be able to simply build and test the compiler. This will automatically install the exact version of the Rust compiler that is required:
cargo build
cargo test
cargo test --test ui -- --checkTo build the Gillian-Rust backend, you first need to install OCaml.
Then, go to the Gillian-Rust folder, create a local switch and install the dependencies. This will automatically install the appropriate version of the OCaml compiler.
opam switch create . --deps-onlyTo run Gillian-Rust, you need to install globally a version of z3. Gillian-Rust was thoroughly tested with z3 4.12.4, but other versions should work too.
You can check if you have z3 installed by running
z3 --version
# Z3 version 4.13.4 - 64 bitIf not, you can install it as follows:
# MacOS
brew install z3
# linux, x86_64
cd ~ && curl -L -o z3.zip "https://github.com/Z3Prover/z3/releases/download/z3-4.12.4/z3-4.12.4-x64-glibc-2.35.zip" && unzip z3.zip -d /opt/z3 && rm z3.zip && sudo ln -s /opt/z3/z3-4.12.4-x64-glibc-2.35/bin/z3 /usr/local/bin/z3
# linux, arm64
cd ~ && curl -L -o z3.zip "https://github.com/Z3Prover/z3/releases/download/z3-4.12.4/z3-4.12.4-arm64-glibc-2.34.zip" && unzip z3.zip -d /opt/z3 && rm z3.zip && sudo ln -s /opt/z3/z3-4.12.4-arm64-glibc-2.34/bin/z3 /usr/local/bin/z3Still in the Gillian-Rust folder, run:
dune build @allThen, in the root folder, run the following command to run all our tests and case studies:
./test_ci_gil.sh