Repository Layout

This section describes the crates located in the Prusti repository, their function, and key modules. Some important files are linked and described individually, although this list is far from complete.

Binaries

These crates relate to the runnable executables produced during compilation.

• prusti/
  • src/bin/prusti-driver.rs - invokes the Rust compiler with Prusti callbacks set up.
  • src/bin/prusti-rustc.rs - spawns prusti-driver with the correct environment.
• prusti-launch/ - utilities for Prusti binaries.
• prusti-server/ - Prusti compilation server.

Specification parsing

These crates relate to parsing Prusti-specific specifications in Rust code (e.g. requires, ensures, etc). These specifications are defined using procedural macros, which must be contained in their own crates, hence the additional prusti-contracts/* crates.

• prusti-contracts/prusti-contracts/ - stubs for Rust pseudo-functions used in specifications; currently old and before_expiry. It also reexports the procedural macros requires, ensures, etc. Depending on the prusti feature, it exports either impl or internal.
• prusti-contracts/prusti-contracts-proc-macros/ – a procedural macro crate that either forwards calls to prusti-specs (if the prusti feature is enabled) or tries to be invisible when compiling with the regular compiler (if the prusti feature is disabled). The prusti feature is set automatically when compiling with Prusti.
• prusti-contracts/prusti-specs/ - does the specification rewriting.
• prusti-contracts/prusti-contracts-test – a minimal test that checks that prusti-contracts can be used with a regular compiler.

Common library code

These crates contain the majority of Prusti's code.

• prusti-common/ - common modules used across Prusti (code independent from Rust internals).
  • src/vir/ - VIR.
    • ast/ - Viper IR enum definitions and methods to generate Viper code (as text).
    • optimizations/ - optimizations of Viper IR.
    • borrows.rs - reborrowing DAG definition.
    • conversions.rs - implicit casts from Rust types to Viper IR.
    • program.rs - struct holding a full Viper program.
    • to_viper.rs - conversion of vir module structs to Viper AST.
    • utils.rs - functional operations on VIR.
  • (+ other utility code)
• prusti-interface/ - wrapper around the Rust compiler internals that aims to provide a more stable interface (however, it fails to completely encapsulate the Rust compiler from its clients).
  • src/environment/ - most of the wrapper code lives here.
  • src/specs/ – collect type-checked specifications.
• prusti-viper/ - MIR to VIR encoding.

JVM bindings

• viper-sys – low-level (unsafe) JVM bindings.
• viper – higher-level JVM bindings.

Deprecated or removed

• prusti-filter/ - walks through Rust crates to check which are supported by Prusti (used for evaluation in Prusti publication).
• prusti-macros/ - macros to simplify parsing code.