Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Runtime checks #1452

Draft
wants to merge 49 commits into
base: master
Choose a base branch
from
Draft

Runtime checks #1452

wants to merge 49 commits into from

Conversation

cedihegi
Copy link
Contributor

@cedihegi cedihegi commented Sep 6, 2023

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

Some examples can be found in prusti-tests/tests/runtime_checks/.

Mir optimizations:

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).

To use: set variable PRUSTI_REMOVE_DEAD_CODE.
Examples: prusti-tests/tests/mir_optimizations

cedihegi and others added 30 commits April 12, 2023 11:24
Where to insert them is still an issue
- when there was a pledge and a postcondition, the runtime check for the
  postcondition would be skipped
- also created template to find difference between mir_promoted and
  elaborated
We now manually clone old values instead of running a store function.
expiration locations of pledges are now figured out automatically and
inserted, without using user annotations.
Dead code elimination now works using only the encoder, and no longer
modifying the MIR before verification.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant