Skip to content
A static verifier for Rust, based on the Viper verification infrastructure.
Rust Shell Python Other
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
.cargo
bin
design
docker
evaluation
jni-gen
prusti-contracts
prusti-filter
prusti-interface
prusti-viper
prusti
viper-sys
viper
.dockerignore
.gitattributes
.gitignore
.gitlab-ci.yml
Cargo.lock
Cargo.toml
LICENSE
Makefile
README.md
Vagrantfile
playground.service
rust-toolchain

README.md

Prusti-dev

Prusti is a prototype verifier for Rust, built upon the the Viper verification infrastructure.

By default Prusti verifies absence of panics by proving that statements such as unreachable!() and panic!() are unreachable. Overflow checking can be enabled with a configuration flag, otherwise all integers are treated as unbounded. In Prusti, the functional behaviour of a function can be specified by using preconditions, postconditions, and loop invariants. The tool checks them, reporting error messages when the code does not adhere to the provided specification.

To see examples of programs annotated with specifications, look into the prusti/tests/verify/pass/rosetta and prusti/tests/verify/pass-overflow/rosetta folders.

Build for local development

The following instructions has been tested on Ubuntu 16.04:

  • Install the viper package.

    wget -q -O - https://pmserver.inf.ethz.ch/viper/debs/xenial/key.asc | sudo apt-key add -
    echo 'deb http://pmserver.inf.ethz.ch/viper/debs/xenial /' | sudo tee /etc/apt/sources.list.d/viper.list
    sudo apt-get update
    sudo apt-get install -y viper
  • Install Java 8 or a later version.

    sudo apt-get install -y default-jdk
  • Install Rustup

    curl https://sh.rustup.rs -sSf | sh
    source $HOME/.cargo/env
  • Install the dependencies required by some Rust libraries

    sudo apt-get install -y build-essential pkg-config gcc libssl-dev
  • Download this Prusti repository and move to the prusti-dev folder

    git clone "<url-of-prusti-repository>"
    cd prusti-dev
  • Install the Rust compiler (the exact compiler version is stored in the rust-toolchain file)

    rustup toolchain install $(cat rust-toolchain)
  • You can now compile Prusti

    make build
  • Make sure that the tests are passing

    make test
  • To run Prusti and verify a program (without overflow checks) there are three options:

    # Recommended, cross-platform
    ./target/debug/prusti-rustc path/to/the/program_to_be_verified.rs

    or

    ./bin/prusti path/to/the/program_to_be_verified.rs

    or

    make run RUN_FILE=path/to/the/program_to_be_verified.rs
  • To enable overflow checks, run the previous commands with the environment variable PRUSTI_CHECK_BINARY_OPERATIONS set to true.

  • (Optional) To install additional tools required by some scripts in the evaluation folder:

    sudo apt-get install -y jq

Demo with rust-playground

If you have Vagrant installed, just run make demo and open http://localhost:23438/?version=nightly&mode=debug&edition=2018. Otherwise, you can follow the following instructions.

  1. Choose a folder in which to run the demo

    export PRUSTI_DEMO_DIR="/tmp/prusti-demo"
    mkdir -p "$PRUSTI_DEMO_DIR"
  2. Build Prusti

    cd "$PRUSTI_DEMO_DIR"
    git clone "<url-of-prusti-repository>"
    make build-docker-images
  3. Build rust-playground

    cd "$PRUSTI_DEMO_DIR"
    git clone git@github.com:integer32llc/rust-playground.git
    cd rust-playground
    git checkout f103d06cfb4c96ca6055ae9f4b16ca5cca03c852
    cd ui
    cargo build --release
    cd frontend
    yarn
    yarn run build:production
  4. Start the demo

    cd "$PRUSTI_DEMO_DIR/rust-playground/ui"
    TMPDIR=/tmp \
    RUST_LOG=debug \
    PLAYGROUND_UI_ADDRESS=0.0.0.0 \
    PLAYGROUND_UI_PORT=8080 \
    PLAYGROUND_UI_ROOT=$PWD/frontend/build \
    PLAYGROUND_GITHUB_TOKEN="" \
    ./target/release/ui
  5. Use the demo:

    • Visit http://localhost:8080/
    • Select "Nightly channel".
    • Write the following program:
      extern crate prusti_contracts;
      
      fn main() {
          unreachable!();
      }
    • Click on "Build" and watch at the compiler and verifier messages.
You can’t perform that action at this time.