Resources, Obligations, Time Reasoning

[vfukala]

NOTE: Caching has been disabled in this PR (see prusti-server/src/process_verification.rs) because it led to errors in the Github CI. Consider re-enabling it before merging.

Adding time reasoning (see #1275), resources, and obligations to Prusti. Obligations can be defined by the user with arbitrary arguments. For each obligation, Prusti checks that no instances of it are leaked. This means that all obligation instances held at the end of a function must be asserted (exhaled) in the postcondition.

For example, the following program verifies.

use prusti_contracts::*;

obligation! {
    fn alloced(amount: usize, loc: usize);
}

#[trusted]
#[ensures(alloced(1, loc))]
fn alloc(loc: usize) {
    // do allocation here
}

#[trusted]
#[requires(alloced(1, loc))]
fn dealloc(loc: usize) {
    // do deallocation here
}

#[ensures(alloced(1, base + offset))]
fn alloc_offset(base: usize, offset: usize) {
    alloc(base + offset);
}

#[ensures(alloced(1, 67))]
fn main() {
    alloc_offset(32, 1);
    alloc_offset(64, 3);
    dealloc(33);
}

It wouldn't verify if the postcondition of main were left out, for example.

TO DO (in future):

• Check for misplaced impure expressions (resources in negations, disjunctions, etc.) while encoding MIR into VIR and not separately after the optimizations have been done. (Contrary to how it was before, it should now be possible to do these checks on the directly generated VIR without relying on optimizations to remove some internally introduced constructs.)

out of scope:

• In some cases, quantified obligations don't verify even though they should due to an incompleteness in Silicon (like here, also see Silicon incompleteness).