proof_for_contract much slower than proof (or even runs out of memory)

[BusyBeaver-42]

Note: To reproduce the example, the loops must be manually unrolled otherwise an other issue occurs (see #3796).

I tried this code:

use std::ptr;

const SIZE: usize = 5;

unsafe fn copy(s: *mut u8, i: usize, j: usize)
{
    unsafe {
        let i = s.add(i);
        let j = s.add(j);
        ptr::copy(i, j, 1);
    }
}

#[kani::requires(s.len() >= SIZE)]
#[kani::modifies(&s[..SIZE])]
fn foo(s: &mut [u8])
{
    if s.len() < SIZE {
        panic!();
    }

    let s = s.as_mut_ptr();
    unsafe {
        // manually unroll these loops to reproduce the example
        for i in 0..SIZE {
            for j in 0..SIZE {
                copy(s, i, j);
            }
        }
    }
}

#[kani::proof]
fn check_foo() {
    let mut arr: [u8; SIZE + 2] = kani::any();
    let s = kani::slice::any_slice_of_array_mut(&mut arr);

    kani::assume(s.len() >= SIZE);

    foo(s);
}

#[kani::proof_for_contract(foo)]
fn check_foo_contract() {
    let mut arr: [u8; SIZE + 2] = kani::any();
    let s = kani::slice::any_slice_of_array_mut(&mut arr);

    foo(s);
}

using the following command line invocation:

cargo kani -Z function-contracts

with Kani version:

• cargo-kani 0.57.0
• CBMC version 6.4.1 (cbmc-6.4.1) 64-bit x86_64 linux

I expected to see this happen: Both of the verifications to take roughly the same time.

Instead, this happened:

• SIZE = 5
  • proof Verification Time: 1.4301268s
  • proof_for_contract Verification Time: 48.407013s
• SIZE = 10
  • proof Verification Time: 4.190568s
  • proof_for_contract Verification Time: CBMC failed VERIFICATION:- FAILED CBMC appears to have run out of memory.

[zhassan-aws]

Thanks for filing this issue @BusyBeaver-42. The performance difference is not unexpected. The proof_for_contract harness performs more checks than than the proof one. In particular, it checks that no variables are assigned other than the ones specified in the modifies clause. This is to ensure soundness when replacing the function with its contract.

Nevertheless, we'll investigate to check if performance can be improved.

[remi-delmas-3000]

Hi, I can confirm @zhassan-aws answer. Contracts instrumentation adds a number of ghost array variables to the model in order to track detailed read/write permissions, each allocation or assignment triggers a lookup in these ghost arrays. Our generation of array theory lemmas in CBMC is known to have a quadratic blowup in bad cases. The size of these ghost arrays is determined by the value passed to CBMC for --object-bits (16 by default, arrays end up being 2^16 in size).
Combined with 10x10 unwinding yielding a 100 arrays update and possibly 10k array lemmas that's what you are observing.

Possible workarounds would be:

• use loop contracts to get rid of the 10x10 unwinding which causes the array lemma generation blowup
• reduce --object-bits to a lower value (e.g. 10 instead of 16) to reduce the ghost array size and instrumentation overhead (I doubt it would really fix the blowup since the program would still have same number of array accesses anyway, and that's what matters most).

[BusyBeaver-42]

Hi, thanks for your replies! Since the locations where the function writes are statically known, I naively assumed that verifying the #[modifies(...)] part of the contract wouldn’t be significantly more expensive than verifying that there are no unauthorized writes in the #[proof] harness.

I understand that I can use loop contracts in this case, but I was aiming to provide a simple example. The actual functions I am trying to verify are sort9_optimal and sort13_optimal. However, sort13_optimal fails even when verifying safety only (i.e., without correctness verification), and this happens even with 32 GB of memory.

Regarding loop contracts, I tried using them, but they didn’t seem to have any effect (whether or not I used #[unwind(_)]). I checked the documentation and the two RFCs but couldn’t figure out what I was doing wrong. I understand that creating comprehensive documentation for loop contracts—similar to what exists for function contracts—takes time, but I think including at least a small example in the documentation would be very helpful.

PS: On the topic of documentation, there’s a small issue in the documentation for mem::can_dereference and similar functions. It refers to items in kani's mem module using crate::mem, but these items aren’t actually present in the documentation for the mem module of kani. Instead, they’re found in the documentation for the mem module of kani_core, where functions like can_dereference are defined.

[zhassan-aws]

Regarding loop contracts, I tried using them, but they didn’t seem to have any effect (whether or not I used #[unwind(_)]). I checked the documentation and the two RFCs but couldn’t figure out what I was doing wrong. I understand that creating comprehensive documentation for loop contracts—similar to what exists for function contracts—takes time, but I think including at least a small example in the documentation would be very helpful

CC @qinheping

PS: On the topic of documentation, there’s a small issue in the documentation for mem::can_dereference and similar functions. It refers to items in kani's mem module using crate::mem, but these items aren’t actually present in the documentation for the mem module of kani. Instead, they’re found in the documentation for the mem module of kani_core, where functions like can_dereference are defined.

Good catch. Can you file an issue?

[qinheping]

Thank you for your feedback!

Regarding loop contracts, I tried using them, but they didn’t seem to have any effect (whether or not I used #[unwind(_)]). I checked the documentation and the two RFCs but couldn’t figure out what I was doing wrong.

I guess you did nothing wrong with loop contracts. The reason it didn't work is that the loop contracts now only support while-loops with boolean expressions as conditions. You could try to use loop contracts by rewriting your loops as follow.

        let mut i = 0;
        #[kani::loop_invariant(0 <= i && i <= SIZE)]
        while i < SIZE {
            let mut j = 0;
            #[kani::loop_invariant(0 <= j && j <= SIZE)]
            while j < SIZE {
                copy(s, i, j);
                j += 1;
            }
            i += 1;
        }

I understand that creating comprehensive documentation for loop contracts—similar to what exists for function contracts—takes time, but I think including at least a small example in the documentation would be very helpful

Good point. There are some examples in https://github.com/model-checking/kani/tree/main/tests/expected/loop-contract. I will add more to the documentation.

[BusyBeaver-42]

Thanks for your replies!

Good catch. Can you file an issue?

@zhassan-aws I've opened issue #3815.

Good point. There are some examples in https://github.com/model-checking/kani/tree/main/tests/expected/loop-contract. I will add more to the documentation.

I actually did not think of looking at the tests ^^', that's a great advice. :-)