Introduction

This is the developer guide for Prusti, intended to make Prusti more approachable for new contributors. For installation instructions and a tutorial on using Prusti, see the user guide.

Direct links to code are provided in boxes like this. Note that we sometimes link to specific lines in the linked files, which requires that the links refer to a specific commit in Prusti's history. When reading through the code using this guide, make sure to check if the code has since changed.

Configuration

Providing Flags

Flags can be set in one of four ways, in increasing order of priority:

Provided individually as environment variables with the prefix DEFAULT_PRUSTI_ (for example, DEFAULT_PRUSTI_CACHE_PATH for the CACHE_PATH flag).

Note: One should only use this to change the default value of flags, such that this can be overridden by a config file

Provided lowercase in a Prusti.toml file (allowed formats, e.g. check_overflows = true for the CHECK_OVERFLOWS flag). Prusti searches for a Prusti.toml depending on how it is run:
- As cargo prusti (on an entire crate): in the CARGO_MANIFEST_DIR, i.e. next to the crate's Cargo.toml
- As prusti-rustc (on a single Rust file): in the current working directory
Provided individually as environment variables with the prefix PRUSTI_ (for example, PRUSTI_ASSERT_TIMEOUT for the ASSERT_TIMEOUT flag).
Provided individually as command-line arguments to Prusti with the prefix -P (for example, -Pprint_desugared_specs for the PRINT_DESUGARED_SPECS flag).

Multi-crate Cargo Prusti Projects

Setting flags becomes slightly more complicated when Prusti is run on multiple crates as cargo prusti; e.g. which Prusti.toml file will be used. Though overriding priority as above remains the same, the three possible approaches to providing flags all behave differently, in particular depending on flag Category.

Environment Variables

The environment persists throughout compilation, therefore all flags set through the DEFAULT_PRUSTI_ or PRUSTI_ will apply to all crates, and flags of both Category A and B. For example setting PRUSTI_CHECK_OVERFLOWS=false will disable overflow checks in all dependencies, even if they try to override this with a Prusti.toml file.

Prusti Config File

A Prusti.toml is optionally loaded from the current working directory prior to compilation. This file is used to configure flags in Category B only and these flags apply to the entire compilation.

Then, as each individual crate is checked (from the roots of the dependency tree) a Prusti.toml is optionally loaded from the directory where the crate's corresponding Cargo.toml is located. This file is used to configure flags in Category A only — it would not make sense to set e.g. NO_VERIFY_DEPS in a dependency since all of its dependencies have already been verified.

Therefore, when publishing a lib crate to git/crates.io one can configure Category A flags by including a Prusti.toml file next to their Cargo.toml.

Note: Currently cargo does not track Prusti.toml files as a dependency, therefore if it's the only file that changed in a crate you may need to run cargo clean -p <crate> to force reverification

The Prusti.toml used to load Category B flags at the start and the one used to load Category A flags at the end for the root crate will often be one and the same because cargo prusti is typically run from the root crate's directory. This can be changed by providing the --manifest-path flag.

Commandline Arguments

Prusti -P flags can be provided after a -- (e.g. cargo prusti -- -Pcargo_command=build). Currently flags from Category B only are supported; providing a flag in Category A this way will be ignored.

Flags to cargo are provided in the regular way (e.g. cargo prusti --features foo).

List of Configuration Flags

Name	Rust type	Default value	Multi-Crate Category
`ALLOW_UNREACHABLE_UNSUPPORTED_CODE`	`bool`	`false`	A
`ASSERT_TIMEOUT`	`u64`	`10_000`	A
`BE_RUSTC`	`bool`	`false`	B
`BOOGIE_PATH`	`Option<String>`	`env::var("BOOGIE_EXE")`	A
`CACHE_PATH`	`String`	`""`	A*
`CARGO_COMMAND`	`String`	`"check"`	B
`CARGO_PATH`	`String`	`"cargo"`	B
`CHECK_FOLDUNFOLD_STATE`	`bool`	`false`	A
`CHECK_OVERFLOWS`	`bool`	`true`	A
`CHECK_PANICS`	`bool`	`true`	A
`CHECK_TIMEOUT`	`Option<u32>`	`None`	A
`COUNTEREXAMPLE`	`bool`	`false`	A
`DELETE_BASIC_BLOCKS`	`Vec<String>`	`vec![]`	A
`DISABLE_NAME_MANGLING`	`bool`	`false`	A
`DUMP_BORROWCK_INFO`	`bool`	`false`	A
`DUMP_DEBUG_INFO`	`bool`	`false`	A
`DUMP_DEBUG_INFO_DURING_FOLD`	`bool`	`false`	A
`DUMP_PATH_CTXT_IN_DEBUG_INFO`	`bool`	`false`	A
`DUMP_REBORROWING_DAG_IN_DEBUG_INFO`	`bool`	`false`	A
`DUMP_VIPER_PROGRAM`	`bool`	`false`	A
`ENABLE_CACHE`	`bool`	`true`	A
`ENABLE_PURIFICATION_OPTIMIZATION`	`bool`	`false`	A
`ENABLE_TYPE_INVARIANTS`	`bool`	`false`	A
`ENABLE_VERIFY_ONLY_BASIC_BLOCK_PATH`	`bool`	`false`	A
`ENCODE_BITVECTORS`	`bool`	`false`	A
`ENCODE_UNSIGNED_NUM_CONSTRAINT`	`bool`	`false`	A
`EXTRA_JVM_ARGS`	`Vec<String>`	`vec![]`	A
`EXTRA_VERIFIER_ARGS`	`Vec<String>`	`vec![]`	A
`FOLDUNFOLD_STATE_FILTER`	`String`	`""`	A
`FULL_COMPILATION`	`bool`	`false`	A*
`HIDE_UUIDS`	`bool`	`false`	A
`IGNORE_REGIONS`	`bool`	`false`	A
`INTERNAL_ERRORS_AS_WARNINGS`	`bool`	`false`	A
`INTERN_NAMES`	`bool`	`true`	A
`JAVA_HOME`	`Option<String>`	`None`	A
`JSON_COMMUNICATION`	`bool`	`false`	A
`LOG`	`String`	`""`	A
`LOG_DIR`	`String`	`"log"`	A*
`LOG_STYLE`	`String`	`"auto"`	A
`LOG_SMT_WRAPPER_INTERACTION`	`bool`	`false`	A
`LOG_TRACING`	`bool`	`true`	A
`MAX_LOG_FILE_NAME_LENGTH`	`usize`	`60`	A
`MIN_PRUSTI_VERSION`	`Option<String>`	`None`	A
`NO_VERIFY`	`bool`	`false`	A
`NO_VERIFY_DEPS`	`bool`	`false`	B
`IGNORE_DEPS_CONTRACTS`	`bool`	`false`	B
`OPT_IN_VERIFICATION`	`bool`	`false`	A
`OPTIMIZATIONS`	`Vec<String>`	"all"	A
`PRESERVE_SMT_TRACE_FILES`	`bool`	`false`	A
`PRINT_COLLECTED_VERIFICATION_ITEMS`	`bool`	`false`	A
`PRINT_COUNTEREXAMPLE_IF_MODEL_IS_PRESENT`	`bool`	`false`	A
`PRINT_DESUGARED_SPECS`	`bool`	`false`	A
`PRINT_HASH`	`bool`	`false`	A
`PRINT_TYPECKD_SPECS`	`bool`	`false`	A
`QUIET`	`bool`	`false`	A*
`SERVER_ADDRESS`	`Option<String>`	`None`	A
`SERVER_MAX_CONCURRENCY`	`Option<usize>`	`None`	A
`SERVER_MAX_STORED_VERIFIERS`	`Option<usize>`	`None`	A
`SIMPLIFY_ENCODING`	`bool`	`true`	A
`SKIP_UNSUPPORTED_FEATURES`	`bool`	`false`	A
`SMT_QI_BOUND_GLOBAL`	`Option<u64>`	`None`	A
`SMT_QI_BOUND_GLOBAL_KIND`	`Option<u64>`	`None`	A
`SMT_QI_BOUND_TRACE`	`Option<u64>`	`None`	A
`SMT_QI_BOUND_TRACE_KIND`	`Option<u64>`	`None`	A
`SMT_QI_IGNORE_BUILTIN`	`bool`	`true`	A
`SMT_QI_EAGER_THRESHOLD`	`u64`	`1000`	A
`SMT_SOLVER_PATH`	`Option<String>`	`env::var("Z3_EXE")`	A
`SMT_SOLVER_WRAPPER_PATH`	`Option<String>`	`None`	A
`SMT_UNIQUE_TRIGGERS_BOUND`	`Option<u64>`	`None`	A
`SMT_UNIQUE_TRIGGERS_BOUND_TOTAL`	`Option<u64>`	`None`	A
`UNSAFE_CORE_PROOF`	`bool`	`false`	A
`USE_MORE_COMPLETE_EXHALE`	`bool`	`true`	A
`USE_SMT_WRAPPER`	`bool`	`false`	A
`VERIFICATION_DEADLINE`	`Option<u64>`	`None`	A
`VERIFY_ONLY_BASIC_BLOCK_PATH`	`Vec<String>`	`vec![]`	A
`VERIFY_ONLY_PREAMBLE`	`bool`	`false`	A
`VIPER_BACKEND`	`String`	`"Silicon"`	A
`VIPER_HOME`	`Option<String>`	`None`	A
`WRITE_SMT_STATISTICS`	`bool`	`false`	A

`ALLOW_UNREACHABLE_UNSUPPORTED_CODE`

When enabled, unsupported code is encoded as assert false. This way error messages are reported only for unsupported code that is actually reachable.

`ASSERT_TIMEOUT`

Maximum time (in milliseconds) for the verifier to spend on a single assertion. Set to 0 to disable timeout. Maps to the verifier command-line argument --assertTimeout.

`BE_RUSTC`

When enabled, Prusti will behave like rustc.

Note: applied to all dependency crates when running with cargo prusti.

`BOOGIE_PATH`

A path to Boogie.

Note: prusti-rustc sets this option.

`CACHE_PATH`

Path to a cache file, where verification cache will be loaded from and saved to. The default empty string disables saving any cache to disk. A path to a file which does not yet exist will result in using an empty cache, but then creating and saving to that location on exit.

Note: cargo prusti sets this flag with DEFAULT_PRUSTI_CACHE_PATH=$CARGO_TARGET_DIR/cache.bin.

`CARGO_COMMAND`

The cargo command to run when checking a crate with cargo prusti. Change to build to export binaries, library files and specs.

Note: Applicable only under cargo prusti.

`CARGO_PATH`

The path to cargo when running cargo prusti. Useful if cargo is not available in the path.

Note: Applicable only under cargo prusti.

`CHECK_FOLDUNFOLD_STATE`

When enabled, additional, slow, checks for the fold/unfold algorithm will be generated.

`CHECK_OVERFLOWS`

When enabled, binary operations and numeric casts will be checked for overflows. See integer type encoding.

`CHECK_PANICS`

When enabled, Prusti will check for an absence of panic!s.

`CHECK_TIMEOUT`

Maximum time (in milliseconds) for the verifier to spend on checks. Set to None uses the verifier's default value. Maps to the verifier command-line argument --checkTimeout. For more information see here.

`COUNTEREXAMPLE`

When enabled, Prusti will try to find and print a counterexample for any failed assertion or specification.

`DELETE_BASIC_BLOCKS`

The given basic blocks will be replaced with assume false.

`DISABLE_NAME_MANGLING`

When enabled, Viper name mangling will be disabled.

Note: This is very likely to result in invalid programs being generated because of name collisions.

`DUMP_BORROWCK_INFO`

When enabled, borrow checking info will be output.

`DUMP_DEBUG_INFO`

When enabled, debug files will be created.

`DUMP_DEBUG_INFO_DURING_FOLD`

When enabled, the state of the fold-unfold algorithm after each step will be dumped to a file.

`DUMP_PATH_CTXT_IN_DEBUG_INFO`

When enabled, branch context state will be output in debug files.

`DUMP_REBORROWING_DAG_IN_DEBUG_INFO`

When enabled, reborrowing DAGs will be output in debug files.

`DUMP_VIPER_PROGRAM`

When enabled, the encoded Viper programs will be output. You can find them either in log/viper_program or target/verify/log/viper_program.

`ENABLE_CACHE`

When enabled, verification requests (to verify individual fns) are cached to improve future verification. By default the cache is only saved in memory (of the prusti-server if enabled). For long-running verification projects use CACHE_PATH to save to disk.

`ENABLE_PURIFICATION_OPTIMIZATION`

When enabled, impure methods are optimized using the purification optimization, which tries to convert heap operations to pure (snapshot-based) operations.

Note: This option is highly experimental.

`ENABLE_TYPE_INVARIANTS`

When enabled, type invariants can be declared on types using the #[invariant(...)] attribute.

`ENABLE_VERIFY_ONLY_BASIC_BLOCK_PATH`

When enabled, only the path given in VERIFY_ONLY_BASIC_BLOCK_PATH will be verified.

Note: This flag is only for debugging Prusti.

`ENCODE_BITVECTORS`

When enabled, bitwise integer operations are encoded using bitvectors.

Note: This option is highly experimental.

`ENCODE_UNSIGNED_NUM_CONSTRAINT`

When enabled, non-negativity of unsigned integers will be encoded and checked.

`EXTRA_JVM_ARGS`

Additional arguments to pass to the JVM when launching a verifier backend.

`EXTRA_VERIFIER_ARGS`

Additional arguments to pass to the verifier backend.

`FOLDUNFOLD_STATE_FILTER`

Filter for fold/unfold nodes when debug info is dumped.

`FULL_COMPILATION`

When enabled, compilation will continue and a binary will be generated after Prusti terminates.

Note: cargo prusti sets this flag with DEFAULT_PRUSTI_FULL_COMPILATION=true.

`HIDE_UUIDS`

When enabled, UUIDs of expressions and specifications printed with PRINT_TYPECKD_SPECS are hidden.

`IGNORE_REGIONS`

When enabled, debug files dumped by rustc will not contain lifetime regions.

`INTERNAL_ERRORS_AS_WARNINGS`

When enabled, internal errors are presented as warnings.

Note: This should only be used for debugging, as enabling this setting could hide actual verification errors.

`INTERN_NAMES`

When enabled, Viper identifiers are interned to shorten them when possible.

`JAVA_HOME`

The path the directory containing Java.

Note: prusti-rustc sets this option.

`JSON_COMMUNICATION`

When enabled, communication with the server will be encoded as JSON instead of the default bincode.

`LOG`

Log level and filters. See env_logger documentation.

For example, PRUSTI_LOG=prusti_viper=trace enables trace logging for the prusti-viper crate, or PRUSTI_LOG=debug enables lighter logging everywhere. When using trace it is recommended to disable jni messages with e.g. PRUSTI_LOG=trace,jni=warn. A useful explanation of this can be found in the rustc docs (we set PRUSTI_LOG rather than RUSTC_LOG). When running prusti-rustc and prusti-server, it is possible to report log messages to stderr, however in release builds all trace and most debug logs are not available.

`LOG_DIR`

Path to directory in which log files and dumped output will be stored.

Note: cargo prusti sets this flag with DEFAULT_PRUSTI_LOG_DIR=$CARGO_TARGET_DIR/log.

`LOG_STYLE`

Log style. See env_logger documentation. Has no effect when LOG_TRACING=true.

`LOG_SMT_WRAPPER_INTERACTION`

When enabled, logs all SMT wrapper interaction to a file.

Note: Requires USE_SMT_WRAPPER to be true.

`LOG_TRACING`

When enabled, logs are outputted using the tracing_chrome crate rather than as std output with the env_logger. You can find the file at $LOG_DIR/trace.json which can be opened in ui.perfetto.dev. The file is only generated if LOG is set.

`MAX_LOG_FILE_NAME_LENGTH`

Maximum allowed length of a log file name. If this is exceeded, the file name is truncated.

`MIN_PRUSTI_VERSION`

Minimum required version of Prusti that is allowed to run. If Prusti detects that its own version is lower than this, it will throw an error and refuse to verify files. Generally set in a Prusti.toml file of a crate to enforce a minimum Prusti version.

`NO_VERIFY`

When enabled, verification is skipped altogether, though specs are still exported.

`NO_VERIFY_DEPS`

When enabled, verification is skipped for dependencies. Equivalent to enabling NO_VERIFY for all dependencies. Remote dependencies from e.g. git/crates.io are already automatically NO_VERIFY.

Note: applied to all dependency crates when running with cargo prusti.

`IGNORE_DEPS_CONTRACTS`

When enabled, Prusti will not collect contracts from the project's dependencies. This is useful for debugging and working around unsupported language features in the dependencies.

`OPT_IN_VERIFICATION`

When enabled, Prusti will only try to verify the functions annotated with #[verified]. All other functions are assumed to be #[trusted], by default. Functions annotated with both #[trusted] and #[verified] will not be verified.

`ONLY_MEMORY_SAFETY`

When enabled, only the core proof is verified.

Note: This should be used only when UNSAFE_CORE_PROOF is enabled.

`OPTIMIZATIONS`

Comma-separated list of optimizations to enable, or "all" to enable all. Possible values in the list are:

"inline_constant_functions"
"delete_unused_predicates"
"optimize_folding"
"remove_empty_if"
"purify_vars"
"fix_quantifiers"
"fix_unfoldings"
"remove_unused_vars"
"remove_trivial_assertions"
"clean_cfg"

`PRESERVE_SMT_TRACE_FILES`

When enabled, does not delete Z3 trace files.

Note: Requires USE_SMT_WRAPPER to be true.

`PRINT_COLLECTED_VERIFICATION_ITEMS`

When enabled, prints the items collected for verification.

`PRINT_COUNTEREXAMPLE_IF_MODEL_IS_PRESENT`

When enabled, a counterexample contains values for the original type and its model.

`PRINT_DESUGARED_SPECS`

When enabled, prints the AST with desugared specifications.

`PRINT_HASH`

When enabled, prints the hash of a verification request (the hash is used for caching). This is a debugging option which does not perform verification — it is similar to NO_VERIFY, except that this flag stops the verification process at a later stage.

`PRINT_TYPECKD_SPECS`

When enabled, prints the type-checked specifications.

`QUIET`

When enabled, user messages are not printed. Otherwise, messages output into stderr.

Note: cargo prusti sets this flag with DEFAULT_PRUSTI_QUIET=true.

`SERVER_ADDRESS`

When set to an address and port (e.g. "127.0.0.1:2468"), Prusti will connect to the given server and use it for its verification backend.

When set to "MOCK", the server is run off-thread, effectively mocking connecting to a server without having to start it up separately.

`SERVER_MAX_CONCURRENCY`

Maximum amount of verification requests the server will work on concurrently. If not set, defaults to the number of (logical) cores on the system.

`SERVER_MAX_STORED_VERIFIERS`

Maximum amount of instantiated Viper verifiers the server will keep around for reuse. If not set, defaults to SERVER_MAX_CONCURRENT_VERIFICATION_OPERATIONS. It also doesn't make much sense to set this option to less than that, since then the server will likely have to keep creating new verifiers, reducing the performance gained from reuse.

Note: This does not limit how many verification requests the server handles concurrently, only the size of what is essentially its verifier cache.

`SIMPLIFY_ENCODING`

When enabled, the encoded program is simplified before it is passed to the Viper backend.

`SKIP_UNSUPPORTED_FEATURES`

When enabled, features not supported by Prusti will be reported as warnings rather than errors.

`SMT_QI_BOUND_GLOBAL`

If not None, checks that the number of global quantifier instantiations reported by the SMT wrapper is smaller than the specified bound.

Note: Requires USE_SMT_WRAPPER to be true.

`SMT_QI_BOUND_GLOBAL_KIND`

If not None, checks that the number of global quantifier instantiations for each quantifier reported by the SMT wrapper is smaller than the specified bound.

Note: Requires USE_SMT_WRAPPER to be true.

`SMT_QI_BOUND_TRACE`

If not None, checks that the number of quantifier instantiations in each trace reported by the SMT wrapper is smaller than the specified bound.

Note: Requires USE_SMT_WRAPPER to be true.

`SMT_QI_BOUND_TRACE_KIND`

If not None, checks that the number of quantifier instantiations in each trace for each quantifier reported by the SMT wrapper is smaller than the specified bound.

Note: Requires USE_SMT_WRAPPER to be true.

`SMT_QI_IGNORE_BUILTIN`

When enabled, ignores the built-in quantifiers in SMT quantifier instantiation bounds checking.

`SMT_QI_EAGER_THRESHOLD`

A threshold controlling how many times Z3 should instantiate a single quantifier. This option controls a tradeoff between performance and completeness:

Setting it to a too small value, may lead to spurious verification errors and unstable verification.

Setting it to a too large value, may significantly impact performance.

`SMT_SOLVER_PATH`

Path to Z3.

Note: prusti-rustc sets this option.

`SMT_SOLVER_WRAPPER_PATH`

A path to prusti-smt-solver.

Note: prusti-rustc sets this option.

`SMT_UNIQUE_TRIGGERS_BOUND`

If not None, checks that the number of unique triggers used for each quantifier reported by the SMT wrapper is smaller than the specified bound.

Note: Requires USE_SMT_WRAPPER to be true.

`SMT_UNIQUE_TRIGGERS_BOUND_TOTAL`

If not None, checks that the total number of unique triggers reported by the SMT wrapper is smaller than the specified bound.

Note: Requires USE_SMT_WRAPPER to be true.

`UNSAFE_CORE_PROOF`

When enabled, the new core proof is used, suitable for unsafe code

Note: This option is currently very incomplete.

`USE_MORE_COMPLETE_EXHALE`

When enabled, a more complete exhale version is used in the verifier. See consolidate. Equivalent to the verifier command-line argument --enableMoreCompleteExhale.

`USE_SMT_WRAPPER`

Whether to use the SMT solver wrapper. Enabling this is required to be able to use quantifier instantiation bounds checking.

This flag is intended to be used in tests only.

`VERIFICATION_DEADLINE`

Deadline (in seconds) within which Prusti should encode and verify the program.

Prusti panics if it fails to meet this deadline. This flag is intended to be used for tests that aim to catch performance regressions.

`VERIFY_ONLY_BASIC_BLOCK_PATH`

Verify only the single execution path goes through the given basic blocks. All basic blocks not on this execution path are replaced with assume false. Must be enabled using the ENABLE_VERIFY_ONLY_BASIC_BLOCK_PATH flag.

Note: This option is only for debugging Prusti.

`VERIFY_ONLY_PREAMBLE`

When enabled, only the preamble will be verified: domains, functions, and predicates.

Note: With this flag enabled, no methods are verified!

`VIPER_BACKEND`

Verification backend to use. Possible values:

Carbon - verification-condition-generation-based backend Carbon.
Silicon - symbolic-execution-based backend Silicon.

`VIPER_HOME`

The path the directory containing the Viper JARs.

Note: prusti-rustc sets this option.

`WRITE_SMT_STATISTICS`

When enabled, dumps the statistics collected by the SMT wrapper into files next to the Z3 trace files.

Note: Requires USE_SMT_WRAPPER to be true.

Verification Pipeline

At a high level, Prusti is a plugin to the Rust compiler that converts Rust code enriched with Prusti specifications into Viper code, verifies the code with an external verifier, and then reports the results back to the user.

This chapter summarizes the steps that take place when the user runs Prusti on a given Rust file. The steps are described in greater detail in the subsequent sections. Although we present the steps in separate “stages”, this distinction only exists for the purposes of this guide, and is not clearly mirrored in the codebase.

Binary stage
- The user invokes the binary prusti-rustc <file.rs>.
- The binary sets up important environment variables, then invokes prusti_driver.
Rust compilation stage
- prusti_driver registers callbacks and calls the Rust compiler.
- The compiler expands all procedural macros, which includes the specifications.
- The compiler does the type-checking.
- The Prusti callback is called.
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.
Viper verification stage
- (With Prusti server only) Send VIR to the server.
- VIR is encoded into Viper.
- The Viper verifier is called and the results are obtained.
- (With Prusti server only) Send verification results back to the client.
Reporting stage
- The Prusti client reports compilation and verification errors.

Prusti supports tracing which can be useful to get an idea of the most important functions in stages 3 to 5. To enable this, set the log flag, for example:

./x.py run --bin prusti-rustc -- --edition=2021 prusti-tests/**/nfm22/bst_generics.rs -Plog=debug

Prusti then generates a log/trace.json file which can be opened in ui.perfetto.dev to visualize the trace.

Binary stage

The user invokes the binary prusti-rustc <file.rs>.
The binary sets up important environment variables, then invokes prusti_driver.

This is a short stage responsible for setting up the correct environment variables for the Rust compiler and the Prusti-supporting libraries. To invoke prusti-driver correctly, the following arguments are set up:

--sysroot, pointing to the Rust sysroot where its libraries are stored.
-L, adding Prusti's target/*/deps directory into the library search path.
--extern prusti_contracts=... and --extern prusti_contracts_internal=..., specifying the path for the dynamic libraries containing the procedural macros for Prusti specifications.

prusti/src/bin/prusti-rustc.rs

Rust compilation stage

prusti_driver registers callbacks and calls the Rust compiler.
The compiler expands all procedural macros, which includes the specifications.
The compiler does the type-checking.
The Prusti callback is called.

In this stage, the actual Rust compiler is invoked to make sure the given code is valid Rust code, both syntactically and semantically. Prusti integrates with the Rust compiler using rustc_driver. This allows running the Rust compiler with callbacks triggered when important stages of processing are completed. In Prusti, we are interested in two stages:

prusti/src/callbacks.rs - PrustiCompilerCalls::after_expansion - for debugging and unit testing purposes, it is useful to see the Rust AST after the Prusti specifications are processed.
prusti/src/callbacks.rs - PrustiCompilerCalls::after_analysis - once the type checking is done and the code is determined to be type safe. Code that is syntactically invalid or has type errors is not relevant for Prusti applications.

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.

Viper verification stage

(With Prusti server only) Send VIR to the server.
VIR is encoded into Viper.
The Viper verifier is called and the results are obtained.
(With Prusti server only) Send verification results back to the client.

Prusti server

Prusti server is an optional component of Prusti that can significantly reduce verification times by running a background process. The background process keeps an instance of JVM open, which is what Viper backends use to perform verification of Viper code. With the server enabled, a client only needs to send VIR to the server and receive the results once they are ready.

prusti-viper/src/verifier.rs - Verifier::verify - verification with the server.

prusti-viper/src/verifier.rs - Verifier::verify - verification without the server.

Encoding VIR to Viper

As noted in the previous section, VIR is an intermediate representation separate from Viper AST. In this step the encoding from one to the other is performed.

prusti-server/src/verifier_runner.rs - VerifierRunner::verify - call to to_viper.

prusti-common/src/vir/to_viper.rs - implementation of ToViper trait.

Reporting stage

The Prusti client reports compilation and verification errors.

In this final stage, any errors and warnings that occurred during verification are reported to the user.

prusti-viper/src/verifier.rs - Verifier::verify - collection of errors from verification call.

prusti-viper/src/encoder/errors/prusti_error.rs - PrustiError::emit - emission of Prusti errors as messages and source file spans into the compiler environment.

Macros

Prusti makes use of procedural macros as the interface for user-provided specifications.

Specification syntax

Prusti specification syntax is a superset of Rust boolean expressions. The parsing of Prusti-specific syntax is achieved with a custom preparser. Parsing of Rust syntax is delegated to the syn crate.

prusti-specs/src/specifications/preparser.rs

The preparser accepts the following EBNF grammar:

assertion ::= prusti_expr ;
pledge ::= pledge_lhs, ",", prusti_expr ;
pledge_lhs ::= [ ? actual rust expression ?, "=>" ], prusti_expr ;
 
prusti_expr ::= conjunction, [ "==>", prusti_expr ] ;
conjunction ::= entailment, { "&&", entailment } ;
entailment ::= primary | ? actual rust expression ?, [ "|=", [ "|", ? args as parsed by syn2 ?, "|" ], "[", [ ( requires | ensures ), { ",", ( requires | ensures ) } ], "]" ] ;
primary ::= "(", prusti_expr, ")"
          | "forall", "(", "|", ? one or more args as parsed by syn2 ?, "|", prusti_expr, [ ",", "triggers", "=", ? array as parsed by syn2 ? ] ")"
          ;
requires ::= "requires", "(", prusti_expr, ")" ;
ensures ::= "ensures", "(", prusti_expr, ")" ;

Specification serialization

Because procedural macros are executed in a separate, sandboxed process, it is not straight-forward to pass data from procedural macros to the rest of the Prusti pipeline. Any collected data (e.g. parsed assertions) is therefore serialized and inserted into the processed HIR as attributes on dummy functions, where it can be picked up by a HIR visitor.

prusti-specs/src/rewriter.rs - rewriter, generates functions with serialized specifications.
prusti-interface/src/specs/mod.rs - SpecCollector - specification collector, implements intravisit::Visitor for walking the HIR.

Viper Encoding

This chapter details how particular features of the Rust language are encoded into Viper.

Types

This section describes how Rust types are encoded into Viper. There are two methods used in Prusti:

Heap-based type encoding

This encoding uses Viper predicates and Refs.

Primitive types

A small number of Rust types have direct analogues in the Viper type system. However, because it is possible to reference local variables and arguments in Rust, all variables are encoded as Refs, and specific fields are used to refer to the "primitive value" contained in those Refs.

`Bool`

Bool is encoded to Viper Bool.

field val_bool: Bool
predicate bool(self: Ref) {
  acc(self.val_bool, write)
}

`i`, `u`, `char`

All Rust integers (i8, i16, i32, i64, i128, isize, u8, u16, u32, u64, u128, usize) and char are encoded to Viper Int.

field val_int: Int
predicate i32(self: Ref) {
  acc(self.val_int, write)
}

When the CHECK_OVERFLOWS flag is enabled, integer bounds are encoded with the type.

// with CHECK_OVERFLOWS
predicate i32(self: Ref) {
  acc(self.val_int, write) && -2147483648 <= self.val_int && self.val_int <= 2147483647
}

When the ENCODE_UNSIGNED_NUM_CONSTRAINT flag is enabled (even when CHECK_OVERFLOWS is not), non-negativity of unsigned integers is always encoded.

// with ENCODE_UNSIGNED_NUM_CONSTRAINT
predicate u32(self: Ref) {
  acc(self.val_int, write) && 0 <= self.val_int
}

Composite types

There are no classes in Viper (every Ref instance has all fields), so non-primitive Rust types are encoded as predicates composed of multiple components.

Tuples

Each component of a tuple is a field of type Ref, named tuple_0, tuple_1, etc. The type of each component is encoded recursively.

field tuple_0: Ref
field tuple_1: Ref
// ...

// for some types X and Y
predicate Tuple_X_Y(self: Ref) {
  acc(self.tuple_0, write) && X(self.tuple_0) &&
  acc(self.tuple_1, write) && Y(self.tuple_1)
}

Structures

Structures are encoded similarly to tuples, except that fields names correspond to the names defined in the Rust type.

type X = ();
type Y = ();

// for a Rust type, assuming types X and Y are defined
struct SomeStruct {
  a: X,
  b: Y,
}

field SomeStruct_a: Ref
field SomeStruct_b: Ref
predicate SomeStruct(self:Ref) {
  acc(self.SomeStruct_a, write) && X(self.SomeStruct_a) &&
  acc(self.SomeStruct_b, write) && Y(self.SomeStruct_b)
}

Enumerations

Enumerations (ADTs) have values corresponding to one of their variants. Each variant can hold different types of data, so the Viper encoding contains implications of the form "if the variant of the value is X, the value contains the following fields". The variant index is encoded as the discriminant field.

type X = ();

// for a Rust type, assuming type X is defined
enum SomeEnum {
  Foo,
  Bar(X),
}

field discriminant: Int
field elt0: Ref
// ...

predicate SomeEnum(self: Ref) {
  acc(self.discriminant, write) &&
  0 <= self.discriminant && self.discriminant <= 1 &&
  // variant `Foo`
  (self.discriminant == 0 ==> true) &&
  // variant `Bar(X)`
  (self.discriminant == 1 ==> acc(self.elt0, write) && X(self.elt0))
}

References

Rust references, mutable or otherwise, are encoded using the val_ref field.

field val_ref: Ref

// for some Rust type X, &mut X is the following
predicate RefMutX(self: Ref) {
  acc(self.val_ref, write) && X(self.val_ref)
}

Snapshot-based type encoding

Prusti's default encoding of types heavily relies on the heap component of the Viper program state to model parts of Rust's ownership system through permissions.

However, some Viper features do not work well with Prusti's heap-based encoding. For example, quantification over structs is problematic because they are encoded using predicates instead of heap-independent types. Similarly, since Viper functions must not have resource assertions in their postconditions, the heap-based encoding prevents modeling pure Rust functions that return (copyable) structures.

Prusti uses an alternative encoding of most types - called the snapshot-based encoding - to circumvent these issues. Snapshots use Viper domains to model each Rust type as a new (heap-independent) type in Viper instead of relying on Viper predicates.

The snapshot-based encoding of a Rust type, say T, consists of four components:

A domain type Snap$T representing the Rust type T. Instances of Snap$T can be thought of as deep values representing a Rust value of type T.
A constructor function cons$T (for each variant of T) that takes all values that make up a Rust value of type T and returns the corresponding deep value of type Snap$T.
Axioms that ensure that each Rust value of type T corresponds to exactly one deep value of type Snap$T and the other way around, i.e., there is a bijection between instances of the Rust type and its snapshot encoding.
A heap-dependent snapshot function that converts the heap-based encoding of a Rust value of type T into a heap-independent representation of type Snap$T.

Example

Consider the Rust struct declared below.

struct SomeStruct {
  a: i32,
  b: i32,
}

Prusti generates the following Viper domain covering components (1) - (3) for the above function. In particular, the single axiom ensures that two instances of Snap$SomeStruct are equal if and only if all of their underlying components are equal; the "only if" direction is implicit because the constructor is a function and thus produces the same value whenever the same arguments are supplied.

domain Snap$SomeStruct { // (1)
 
  // (2) 
  function cons$SomeStruct(a: Int, b: Int): Snap$SomeStruct

  // (3)
  axiom Snap$SomeStruct$injectivity {
    forall
      a1: Int, b1: Int, a2: Int, b2: Int :: { cons$SomeStruct(a1, b1), cons$SomeStruct(a2, b2) }
      cons$SomeStruct(a1, b1) == cons$SomeStruct(a2, b2) ==> a1 == a2 && b1 == b2
  }

}

To guarantee that there is a bijection between instances of SomeStruct and Snap$SomeStruct one needs, in principle, another axiom formalizing that every instance of Snap$SomeStruct corresponds to an application of the constructor function; a corresponding axiom is found below. However, we never encountered a case in which the axiom is actually needed. Prusti thus does not generate it at the moment.

axiom Snap$SomeStruct$surjectivity {
  forall
    s: Snap$SomeStruct ::
    (forall a: Int, b: Int :: {cons$SomeStruct(a, b)} s != cons$SomeStruct(a, b)) ==> false
}

Finally, component (4), i.e., the heap-dependent function for converting instances of SomeStruct in the heap-based encoding into the snapshot-based representation, is defined as follows:

// (4)
function snap$SomeStruct(self: Ref): Snap$SomeStruct
  requires acc(SomeStruct(self, read$()))
{
  unfolding acc(SomeStruct(self, read$())) in
    cons$SomeStruct(snap$i32(self.SomeStruct_a), snap$i32(self.SomeStruct_b))
}

The above function recursively unfolds all predicates involved in the encoding of SomeStruct. It then calls the constructor of Snap$SomeStruct. Furthermore, for each argument, it calls the snap$ function of the argument's type to obtain a heap-independent deep value instead of a reference.

Primitive types

Prusti also generates snap$ functions for primitive types such that we do not have to check whether a type is primitive or not; these functions return the primitive type itself instead of a domain type. For instance, the function snap$i32 used in the above example is defined as follows:

function snap$i32(self: Ref): Int
  requires acc(i32(self), read$())
{
  unfolding acc(i32(self), read$()) in self.val_int
}

Since the snapshot types of primitive types correspond directly to Viper types, they can also be inlined:

// SomeStruct as above

function snap$SomeStruct(self: Ref): Snap$SomeStruct
  requires acc(SomeStruct(self, read$()))
{
  unfolding acc(SomeStruct(self, read$())) in
    unfolding acc(i32(self.SomeStruct_a), read$()) in
    unfolding acc(i32(self.SomeStruct_b), read$()) in
      cons$SomeStruct(self.SomeStruct_a.val_int, self.SomeStruct_b.val_int)
}

Nested structures

Nested Rust structures are encoded as in the previous example - the main difference is that every reference to another structure needs to be replaced with the corresponding snapshot type in every constructor.

For instance, assume we extend the previous example with another structure that re-uses SomeStruct:

struct SomeStruct {
  a: i32,
  b: i32,
}

struct BiggerStruct {
  foo: i32,
  bar: SomeStruct,
}

In this case, Prusti generates another domain type for BiggerStruct whose constructor takes a snapshot type for every instance of SomeStruct; analogously, its snapshot function invokes snap$SomeStruct to convert references to SomeStruct into deep values of type Snap$SomeStruct:

domain Snap$BiggerStruct {
  function cons$BiggerStruct(foo: Int, bar: Snap$SomeStruct): Snap$BiggerStruct

  // axioms ...
}

function snap$BiggerStruct(self: Ref): Snap$BiggerStruct
  requires acc(BiggerStruct(self, read$()))
{
  unfolding acc(BiggerStruct(self, read$())) in
    cons$BiggerStruct(snap$i32(self.BiggerStruct_foo), snap$SomeStruct(self.BiggerStruct_bar))
}

Enumerations

This feature is not fully implemented in Prusti yet.

While the snapshot-based encoding of enumerations is mostly analogous to the encoding of structs, it needs to account for multiple enum variants, which are distinguished by an integer-valued discriminant. Consequently, the snapshot domain generated for an enumeration is slightly more involved:

It contains one constructor for each variant of the enumeration.
It contains one injectivity axiom for each variant.
It additionally needs to ensure that different constructors yield different snapshot values. To this end, we introduce a new domain function mapping every snapshot value to its enumeration discriminant - an integer representing the variant. Moreover, for each variant, we add an axiom expressing that constructors yield snapshot values with the correct discriminant.
Its heap-dependent snap$ function needs to branch over the enumeration's discriminant field to select the correct constructor when converting a reference to a snapshot value.

For example, consider the enumeration below, which defines a custom Option type.

struct SomeStruct {
  a: i32,
  b: i32,
}

enum MyOption {
  _Some(SomeStruct),
  _None,
}

The corresponding snapshot encoding is defined as follows:

domain Snap$MyOption {
  // one constructor for each variant
  function cons$MyOption$0(): Snap$MyOption
  function cons$MyOption$1(x: Snap$SomeStruct): Snap$MyOption

  // injectivity axioms for all constructors with parameters
  axiom Snap$MyOption$injectivity$1 {
    forall
      i: Snap$SomeStruct, j: Snap$SomeStruct :: { cons$MyOption$1(i), cons$MyOption$1(j) }
      cons$MyOption$1(i) == cons$MyOption$1(j) ==> i == j
  }

  // map snapshot values to variant discriminant
  function discriminant$MyOption(x: Snap$MyOption): Int

  // axiom defining possible discriminant values 
  axiom Snap$MyOption$discriminants {
    forall
      x: Snap$MyOption :: 
      discriminant$MyOption(x) == 0 || discriminant$MyOption(x) == 1
  }

  // one axiom characterizing the discriminant for each constructor
  axiom Snap$MyOption$0 {
    discriminant$MyOption(cons$MyOption$0()) == 0
  }
  
  axiom Snap$MyOption$1 {
    forall
      i: Snap$SomeStruct :: { cons$MyOption$1(i) } 
      discriminant$MyOption(cons$MyOption$1(i)) == 1
  }
}

// heap-dependent function for computing snapshot values
function snap$MyOption(x: Ref): Snap$MyOption
  requires acc(MyOption(x), read$())
{
  // call the cons function matching the discriminant
  unfolding acc(MyOption(x), read$()) in 
    x.discriminant == 1
      ? unfolding acc(MyOption$_Some(x.enum_val), read$()) in
          cons$MyOption$1(snap$SomeStruct(x.enum_val))
      : cons$MyOption$0()
}

Applications of snapshots

Prusti makes use of the heap-independent encoding of types via snapshots to implement several features, which are collected below.

Structural equality

Prusti uses the snapshot-based encoding for checking whether two instances of a data structure are equal. That is, both x == y and std::cmp::eq(x,y) are encoded as a comparison of the snapshot values of x and y:

snap$Type(x) == snap$Type(y)

Inequalities x != y are encoded analogously.

Notice that Prusti only uses snapshots for a subset of supported types. More precisely, a type T has to meet the following conditions:

T automatically derives the trait Eq.
T is composed of other supported types, i.e., primitive types and other types that derive Eq.

If a type does not meet these criteria, it either invokes a user-supplied custom implementation or a bodyless stub function.

Comparing return values of pure functions

Whenever one invokes a pure function with equal arguments, the function should yield the same return value, i.e., a function f with one argument should satisfy the following specification:

x == y  ==> f(x) == f(y)

For non-recursive types, the snapshot function snap$type(ref) recursively unfolds the predicate encoding the type of ref. Hence, the above property holds whenever equality of the type of x and y corresponds to structural equality, i.e., whenever the Eq trait is automatically derived.

For example, the following piece of Rust code verifies while internally using snapshots to discharge equality checks:

// The next line is only used to enable mdBook doctests for this file to work
extern crate prusti_contracts;

use prusti_contracts::*;

// as before, but derives Eq
#[derive(PartialEq, Eq)]
struct SomeStruct {
  a: i32,
  b: i32,
}

#[pure]
#[requires(x == y)]
#[ensures(result == y.a)]
fn foo(x: SomeStruct) -> i32 {
  x.a
}

#[requires(x == y)]
#[ensures(result == 2 * foo(x))]
fn test(x: SomeStruct, y: SomeStruct) -> i32 {
    foo(x) + foo(y)
}

However, the snapshot function cannot completely unfold potentially unbounded recursive types. To enable the same behavior as specified above, Prusti thus introduces a shortcut that enables lazy evaluation of snapshot functions: For each pure function f that takes a recursive type (that also derives Eq) as an argument, it generates a domain function mirror$f - called the mirror function - that takes snapshots instead of references as arguments. In the postcondition of f, Prusti then links the return values of f to the return value of mirror$f: Both functions are required to yield the same return value whenever mirror$f is invoked on the snapshot of f's argument. The code snippet below outlines this encoding.

domain Mirrors {
  function mirror$f(x: Snap$SomeRecStruct) : Int
}

function f(x:Ref) : Int
  requires SomeRecStruct(x)
  ensures [result == mirror$f(snap$SomeRecStruct(x)), true]
{
  // ... 
}

Pure functions returning copy types

Prusti uses snapshots to encode pure Rust functions that return structures or enumerations. This is necessary because Viper does not allow resource assertions within the postcondition of functions. At the moment, only types implementing the Copy trait are supported.

As an example, assume both the struct BiggerStruct and the struct SomeStruct from previous examples derive the traits Copy and Eq. Moreover, consider the following pure function get mapping every instance of BiggerStruct to its wrapped instance of SomeStruct:

#[pure]
fn get(x: BiggerStruct) -> SomeStruct {
  x.bar
}

Prusti encodes the function get as a Viper function that first computes the result of get and then invokes the snapshot function snap$SomeStruct to return a snapshot value instead of a reference:

// snapshot domains are encoded as in previous examples
function get(x: Ref): Snap$SomeStruct
  requires BiggerStruct(x)
{
  unfolding BiggerStruct(x) in snap$SomeStruct(x.bar)
}

At the call site, the returned snapshot value is transformed into the default heap-based encoding by first havocking the involved reference and then assuming that the reference's snapshot coincides with the returned snapshot value:

// encoding of x = get(y)
var x: Ref 
x := builtin$havoc_ref()
inhale acc(SomeStruct(x), write) && snap$SomeStruct(x) == get(y)

Warning: Pure functions returning non-primitive types are partially supported by Prusti. In particular, chaining pure functions, e.g., f(g(h(x, y))), and constructing new instances of Copy types within pure functions is currently not fully supported.

Quantification over structures

TODO: Has this been added in the context of closures?

Pure function encoding

To encode specifications and side-effect-free functions (marked with #[pure]), Prusti generates Viper functions. A Viper function consists of a single expression, so Rust function bodies must be folded accordingly. This is only possible for loop-less functions.

For example, the Rust function:

// The next line is only used to enable mdBook doctests for this file to work
extern crate prusti_contracts;

use prusti_contracts::*;

#[pure]
fn hello(a: i32) -> i32 {
  let mut b = 10;
  if a < 3 {
    b = a + 2
  } else if a > 10 {
    b = a - 2
  }
  b
}

Is encoded as:

function hello(a: Int): Int
  requires true
{
  !(a < 3) ? (!(a > 10) ? 10 : a - 2) : a + 2
}

prusti-viper/src/encoder/mir_interpreter.rs - run_backward_interpretation - backward state interpreter, used to determine if MIR has any loops.

prusti-viper/src/encoder/pure_function_encoder.rs

Name mangling

To ensure there are no duplicate names in the generated Viper code, name mangling is employed. Name mangling can be disabled with the DISABLE_NAME_MANGLING flag, although this may result in errors due to name collisions.

For example, to encode the type std::ops::Range, rather than generating the predicate:

predicate Range(self) {
  ...
}

Prusti generates:

predicate m_core$$ops$opensqu$0$closesqu$$$range$opensqu$0$closesqu$$$Range$opensqu$0$closesqu$$_beg_$i32$_end_(self) {
  ...
}

This is the encoded form of m_core::ops[0]::range[0]::Range[0]$_beg_$i32$_end_.

Mangling rules

The following replacements are performed during name mangling:

Original characters	Replacement
`::`	`$$`
`<`	$openang$
`>`	$closeang$
`(`	$openrou$
`)`	$closerou$
`[`	$opensqu$
`]`	$closesqu$
`{`	$opencur$
`}`	$closecur$
`,`	$comma$
`;`	$semic$
	$space$

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.

Development

Setup

This section details the setup required before Prusti can be built from source.

Prerequisites

rustup
Python 3 (for x.py)

`x.py`

x.py is a Python script that provides a convenient wrapper for a Prusti development setup. It can be initialized by running:

$ ./x.py setup

The script will perform the following steps:

(Ubuntu only) Installs the native dependencies (except for java).
- On other OS (including non-Ubuntu Linux distributions) this step has to be performed manually.
Downloads and extracts the latest Viper tools.
Sets up the Rust toolchain.

Step 1 can be skipped by adding the --no-deps argument to the command line. --dry-run can be used to prevent any shell commands from actually running, only printing them to the terminal.

The setup step should be repeated if the Rust toolchain version changes, or if the native dependencies or Viper tools need to be updated.

Native dependencies

Linux

On a Linux-based OS, the required libraries are:

build-essential
pkg-config
curl
gcc
libssl-dev
openjdk-11-jdk (or newer)

macOS

On macOS, Java JDK 11 or newer is required.

Viper tools

Viper tools are required by Prusti. Extracting the appropriate version into a directory called viper_tools in the project root allows x.py to automatically locate the Viper libraries and the Z3 solver.

`rustup` setup

Rust versions and components are managed with rustup. The toolchain version in use is listed in the rust-toolchain file. Additional components used are:

rust-src
rustc-dev
llvm-tools-preview
rustfmt (optional)

Using locally built version in Prusti Assistant

Note: These instructions were tested only on Ubuntu.

To use the locally compiled version in Prusti Assistant, make sure to build Prusti in release mode:

./x.py build --release

Prepare a Prusti package in a new folder:

./x.py package release <prusti-package-path>

Open VS Code and change its settings as follows:

Set prusti-assistant.buildChannel to Local.
Set prusti-assistant.localPrustiPath to the <prusti-package-path> that you chose.

Now, you should be able to verify Rust programs with a locally built version of Prusti.

Building

Once the development setup is complete, Prusti can be compiled. Using the Python wrapper script:

$ ./x.py build

The script will set the following environment variables if they are not already set, before running cargo build:

Variable	Default value	Description
`JAVA_HOME`	Detected based on OS.	Java JDK location.
`RUST_TEST_THREADS`	`1`	Limits the number of threads used for running tests.
`LD_LIBRARY_PATH` (and `DYLD_LIBRARY_PATH` on macOS)	Detected inside `JAVA_HOME`	Path containing `libjvm.so` (`libjvm.dylib` on macOS).
`VIPER_HOME`	`viper_tools/backends`	Path containing `silicon.jar`, `carbon.jar`, and various supporting Java libraries.
`Z3_EXE`	`(VIPER_HOME)/../z3/bin/z3`	Path to the `z3` solver executable.

Any additional arguments are added to the cargo build command line. For example:

$ ./x.py build --all --verbose

Verbose mode

To see which environment variables ./x.py is setting, the ++verbose flag can be passed on the command line before the cargo command:

./x.py ++verbose build

Tests

Tests for the Prusti project can be executed using the Python wrapper script:

./x.py test

The script sets up environment variables just like in the build phase, then runs cargo test.

Any additional arguments are added to the cargo test command line. For example:

$ ./x.py test --all --verbose

Filtering tests

The options available when running cargo test still apply. For example, to only run tests which contain mod in their name:

$ ./x.py test mod

Additional flags

Some tests require setting additional flags, for example, to ensure that the number of quantifier instantiations is below a certain bound. This can be achieved by adding at the top of the test file // compile-flags: followed by the list of arguments to Prusti. For example, the following comment would bound the number of unique triggers used to instantiate a quantifier to 20:

#![allow(unused)]
fn main() {
// compile-flags: -Psmt_unique_triggers_bound=20
}

Debugging tests

See the debugging section.

IDE integration

Warnings as Errors

Prusti uses rather strict code style settings, producing errors for unnecessary code like unused imports. Although this is useful (especially since incremental builds can hide warnings that still apply), it is often obstructive while actively working on the codebase. These linter errors can be treated as warnings instead of errors by providing a compiler flag:

With a command-line argument to Rust: --cap-lints warn
With an environment variable: RUSTFLAGS='--cap-lints warn'

VS Code

Assuming VS Code is in PATH, it can be launched directly with the correct environment variables set up using x.py:

$ ./x.py ide

Any additional arguments are passed to VS Code.

IntelliJ Rust

When using the Rust Plugin for IntelliJ, a lot of spurious errors may be found in the code. This is because Prusti uses a custom toolchain (set in the rust-toolchain file), which makes the plugin fail to load the prelude definitions. The issue is tracked in the intellij-rust repository here.

A temporary workaround is to set the path to the toolchain in use in IntelliJ settings.

Inside the Prusti directory, run rustup which cargo in the terminal.
Go to Preferences > Languages & Frameworks > Rust.
Change the standard library location to the standard library directory inside the Rust toolchain.

As an example, if rustup which cargo returned /Users/example/.rustup/toolchains/nightly-2020-08-17-x86_64-apple-darwin/bin/cargo, the standard library directory is /Users/example/.rustup/toolchains/nightly-2020-08-17-x86_64-apple-darwin/lib/rustlib/src/rust/library.

Debugging

The x.py script can be used to run Prusti on an individual file:

$ ./x.py run --bin prusti-rustc path/to/the/file.rs

See the list of flags for way to configure Prusti. Of particular use when debugging are:

Debugging tests

A proposed way of fixing Prusti limitations is to add a regression test by creating a new file in prusti-tests/tests and then use the following command to get Prusti output:

./x.py build --all && \
RUST_BACKTRACE=1 PRUSTI_DUMP_VIPER_PROGRAM=true PRUSTI_DUMP_DEBUG_INFO=true \
./x.py ++verbose verify-test <path-to-the-test-file>

This command does the following:

Ensures that Prusti is compiled.
Runs the specified test taking into account the configuration flags specified in the test file.
Dumps the information that is most commonly needed for debugging Prusti into the log directory.

Tip: to see the expanded Prusti specification macros, add the following comment at the beginning of the test file:

#![allow(unused)]
fn main() {
// compile-flags: -Zunpretty=expanded
}

Running Prusti in a debugger

The verify-test command also generates a VS Code launch config, which allows you to run Prusti in a debugger.

In the Cargo.toml, section [profile.dev], set debug = 2. This enables debug symbols.
Install the CodeLLDB VS Code extension.

Now you can set breakpoints and launch the debugger.

Debugging performance problems

In case you are debugging a performance problem and suspect that it is caused by quantifiers, append --analyze-quantifiers to the command after the <path-to-the-test-file>. This will run Z3 in tracing mode and produce CSV files with various statistics in log/smt directory. In case you want to see all terms that were used to trigger a specific quantifier, you can produce the list of them with the following command:

PRUSTI_SMT_TRACE_QUANTIFIER_TRIGGERS=<quantifier-id> \
./x.py ++verbose run --release --bin smt-log-analyzer log/smt/<function>/trace1.log

You can find the list of quantifier ids and names in log/smt/<function>/trace1.log.unique-triggers.csv. Running the smt-log-analyzer will generate log/smt/<function>/trace1.log.quantifier-<quantifier-id>-triggers.csv file containing all triggers used to instantiate the quantifier.

Prusti dev guide