The PR of my Master's thesis: Contract Checking at Runtime in a Rust Verifier.
adds the ability to check Prusti contracts at runtime
based on verification results, perform certain MIR optimizations.
Runtime checks:
supported "kinds" of contracts: pre / postconditions, pledges, type conditional specifications, external specifications, prusti_assume!, prusti_assert!, body_invariant!
supported contents of contracts: Any rust expressions that can contain old-expressions and quantifiers. Other prusti features like snapshot equality, predicates, or calls of prusti-specific functions like snap() and others will break the results of these checks.
How to use them (for now):
Either annotate contracts you want to be checked with #[insert_runtime_check] attribute, or set environment variable PRUSTI_RUNTIME_CHECK_ALL_CONTRACTS (which causes ast-rewriter to generate executable check methods for each contract).
Set PRUSTI_INSERT_RUNTIME_CHECKS (which will lead to insertion of calls to previously mentioned check methods into the MIR).
Produce an executable / Run the function: with prusti_rustc set PRUSTI_FULL_COMPILATION, or with cargo-prusti set PRUSTI_CARGO_COMMAND=run
2 kinds of optimizations based on verification results:
Elimination of unreachable blocks
elimination of unnecessary assertions and their corresponding checked operations (e.g. overflow checks for an addition that can be eliminated, will lead to removal of the corresponding assertion, and change the checked addition to a unchecked addition).
The PR of my Master's thesis: Contract Checking at Runtime in a Rust Verifier.
Runtime checks:
prusti_assume!,prusti_assert!,body_invariant!snap()and others will break the results of these checks.How to use them (for now):
#[insert_runtime_check]attribute, or set environment variablePRUSTI_RUNTIME_CHECK_ALL_CONTRACTS(which causes ast-rewriter to generate executable check methods for each contract).PRUSTI_INSERT_RUNTIME_CHECKS(which will lead to insertion of calls to previously mentioned check methods into the MIR).prusti_rustcsetPRUSTI_FULL_COMPILATION, or with cargo-prusti setPRUSTI_CARGO_COMMAND=runSome examples can be found in prusti-tests/tests/runtime_checks/.
Mir optimizations:
2 kinds of optimizations based on verification results:
To use: set variable
PRUSTI_REMOVE_DEAD_CODE. Examples: prusti-tests/tests/mir_optimizations