Prusti processing stage

• The MIR of functions that should be checked is obtained.
• MIR is encoded into VIR - Prusti's intermediate representation.
• VIR is enriched with fold/unfold statements and other ghost code.
• VIR is simplified and optimized.

• prusti/src/verifier.rs - verify - function combining the steps in this stage.

MIR and VIR

Prusti starts with Rust's MIR (mid-level intermediate representation). The MIR is a CFG-based representation that encodes Rust in a highly simplified (and therefore easier to programmatically process) manner.

The output of this stage is VIR (Viper intermediate representation). The VIR is similar to Viper AST, but it is CFG-based and contains some extra instructions to aid the generation of fold/unfold statements. The conversion of VIR to Viper AST is straight-forward by design.

• prusti-common/src/vir/ast - definitions of most VIR data structures, e.g. expressions.
• prusti-common/src/vir/cfg - definitions of the CFG-specific parts of VIR, i.e. methods composed of a graph of basic blocks.

Finding functions to check

In this step, functions to be checked are found by visiting the HIR with a visitor that looks for Prusti-defined attributes.

• prusti-interface/src/environment/mod.rs - Environment::get_annotated_procedures

Encoding MIR to VIR

In this step, Rust MIR is encoded to VIR. Pure functions are treated separately, since they may be used in specifications. The details of this encoding are complex, but a high-level overview can be found in the Prusti publication, Appendix A.

• prusti-viper/src/verifier.rs - Verifier::verify - initialisation of the encoding queue.
• prusti-viper/src/encoder/encoder.rs - Encoder::process_encoding_queue - processing loop for the encoding queue.
• prusti-viper/src/encoder/procedure_encoder.rs - module for encoding impure functions.

VIR processing

At the end of procedure encoding, fold/unfold statements are added. The VIR may also be optimized, e.g. by removing empty branches in if chains.

• prusti-viper/src/encoder/foldunfold/mod.rs - fold/unfold logic.
• prusti-viper/src/verifier.rs - Verifier::verify - optional optimization.