`proof_for_contract` rejects code accepted by `proof`

[BusyBeaver-42]

I tried this code:

#[kani::requires(true)]
fn foo() {
    for _ in 0..2 {
        for _ in 0..2 {}
    }
}

#[kani::proof_for_contract(foo)]
#[kani::unwind(3)]
fn check_foo_contract() {
    foo()
}

using the following command line invocation:

cargo kani -Z function-contracts

with Kani version: cargo-kani 0.57.0

I expected to see this happen:

VERIFICATION:- SUCCESSFUL

Instead, this happened:

SUMMARY:
 ** 1 of 55 failed
Failed Checks: Check that self->start is assignable
 File: "/home/runner/.rustup/toolchains/nightly-2024-12-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/range.rs", line 767, in <std::ops::Range<i32> as std::iter::range::RangeIteratorImpl>::spec_next

VERIFICATION:- FAILED

Note: Verification using kani::proof works as expected.

#[kani::proof]
#[kani::unwind(3)]
fn check_foo() {
    foo()
}

[zhassan-aws]

Hi @BusyBeaver-42. Thanks for filing this issue, and thanks for the minimal example! Apparently, the logic for checking if the variables are assignable is incorrectly applied to a local variable. We will take a look.

[remi-delmas-3000]

I diagnosed two problems:

1. goto-instrument does not pick up dynamic storageLive events
2. goto-symex seems to be doing something wrong too (using the same object to represent distinct objects)

• @tautschnig could you please take a look and confirm there's actually a problem ?

StorageLive problem

The instrumented goto program for the function looks like this:

• var_5::iter and var_11::iter represent the two iterators introduced by the outer and inner loops.

  DECL var_5::iter : Range<i32>
  CALL __CPROVER_contracts_write_set_add_decl(__write_set_to_check, address_of(var_5::iter))

  DECL var_11::iter : Range<i32>
  CALL __CPROVER_contracts_write_set_add_decl(__write_set_to_check, address_of(var_11::iter))

They are added to the write set right after they are declared, which makes them writable.

However we see that the inner iterator variable var_11::iter is declared dead after the completion of the inner loop:

7: ASSIGN var_10 := { 0, 2 }
CALL var_9 := into_iter(var_10, __write_set_to_check)
ASSIGN __CPROVER_dead_object := (__CPROVER_dead_object = cast(address_of(var_11::iter), empty*) ? NULL : __CPROVER_dead_object)
ASSIGN var_11::iter := var_9
8: ASSIGN var_13 := address_of(var_11::iter)
CALL var_12 := next(var_13, __write_set_to_check)
ASSIGN var_14 := cast(var_12.case, signedbv[64])
LOCATION
IF var_14 = 0 THEN GOTO 9
IF var_14 = 1 THEN GOTO 10
GOTO 11
9: GOTO 13
10: GOTO 12
11: ASSERT false // unreachable code
ASSUME false
12: GOTO 8
13: ASSIGN __CPROVER_dead_object := (side_effect statement="nondet" ? cast(address_of(var_11::iter), empty*) : __CPROVER_dead_object)

The statement at label 13 encodes a storageDead event and is picked up by goto-instrument, the object is removed from the write set using:

CALL __CPROVER_contracts_write_set_record_dead(__write_set_to_check, cast(address_of(var_11::iter), empty*))

This can explain the failure, since the write set will only contain var_11::iter for the first occurrence of the inner loop, but not for the next ones.

storageLive events seem to be encoded by the following statements:

ASSIGN __CPROVER_dead_object := (__CPROVER_dead_object = cast(address_of(var_11::iter), empty*) ? NULL : __CPROVER_dead_object)

Right now goto-instrument does not handle this at all. The fix would be to match storageLive events and dynamically re-add the object to the write set.

Symex problem

I also looked at --program-only output of CBMC and saw a potential error. @tautschnig could you confirm the following analysis ?

Symex uses the same object iter!0@1#1 to represent both iterators var_5::iter and var_11::iter:

// 584 file src/main.rs line 5 column 18 function proof::foo
(132) SHARED_WRITE(iter!0@1#1)

// 592 file src/main.rs line 6 column 22 function proof::foo
(133) SHARED_WRITE(iter!0@1#1)

So what could also be happening is that is that the symex engine confounds the two iterators into a single iterator. When the first occurrence of the inner loop terminates the object iter!0@1 is declared dead,
and the analysis fails when the outer loop takes its second iteration (i.e. if fails even before attempting to step into the inner loop for the second time as explained above).

Here's the details:

• dynamic_object$13 is the abstract map that tracks pointers to locally allocated/writable objects keyed under their object IDs.
• It is stored in the field write_set.allocated.elems of the write set.

(470) SHARED_WRITE(dynamic_object$13#1)
// 481 file <builtin-library-__CPROVER_contracts_library> line 260 function __CPROVER_contracts_obj_set_create_indexed_by_object_id
(471) dynamic_object$13#1 == ARRAY_OF(NULL)
// 481 file <builtin-library-__CPROVER_contracts_library> line 260 function __CPROVER_contracts_obj_set_create_indexed_by_object_id
(472) malloc_value!0@9#2 == (const void *)dynamic_object$13
// 482 file <builtin-library-__CPROVER_contracts_library> line 254 function __CPROVER_contracts_obj_set_create_indexed_by_object_id
(486) __contract_write_set!0@1#2..allocated..elems == dynamic_object$13

Object iter!0@1#! is inserted two times in the write set

(539) SHARED_WRITE(dynamic_object$13#2)
// 526 file <builtin-library-__CPROVER_contracts_library> line 634 function __CPROVER_contracts_write_set_add_decl
(540) dynamic_object$13#2 == ARRAY_OF(NULL) WITH [(long int)__CPROVER_POINTER_OBJECT(&iter!0@1):=(const void *)&iter!0@1]
// 526 file <builtin-library-__CPROVER_contracts_library> line 634 function __CPROVER_contracts_write_set_add_decl
(549) SHARED_WRITE(dynamic_object$13#3)
// 526 file <builtin-library-__CPROVER_contracts_library> line 634 function __CPROVER_contracts_write_set_add_decl
(550) dynamic_object$13#3 == dynamic_object$13#2 WITH [(long int)__CPROVER_POINTER_OBJECT(&iter!0@1):=(const void *)&iter!0@1]

We see assigns clause checks like this (this one should pass because we know the object is in dynamic_object$13#3).

// 397 file <builtin-library-__CPROVER_contracts_library> line 784 function __CPROVER_contracts_write_set_check_assignment
(674) \guard#1 == !(dynamic_object$13#3[(long int)__CPROVER_POINTER_OBJECT(&iter!0@1)] == NULL)
// 398 file <builtin-library-__CPROVER_contracts_library> line 785 function __CPROVER_contracts_write_set_check_assignment
(675) __CPROVER_contracts_write_set_check_assignment!0#1 == TRUE
      guard: \guard#1
// 401 file <builtin-library-__CPROVER_contracts_library> line 789 function __CPROVER_contracts_write_set_check_assignment
(676) __CPROVER_contracts_write_set_check_assignment!0#2 == FALSE
      guard: !\guard#1
// 402 file <builtin-library-__CPROVER_contracts_library> line 789 function __CPROVER_contracts_write_set_check_assignment
// 427 file <builtin-library-__CPROVER_contracts_library> line 818 function __CPROVER_contracts_write_set_check_assignment
(677) __CPROVER_contracts_write_set_check_assignment!0#3 == \guard#1
// 427 file <builtin-library-__CPROVER_contracts_library> line 818 function __CPROVER_contracts_write_set_check_assignment
// 1119 file /Users/delmasrd/.rustup/toolchains/nightly-2024-12-18-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/range.rs line 767 column 13 function <std::ops::Range<i32> as std::iter::range::RangeIteratorImpl>::spec_next
(678) __check_lhs_assignment!0@1#2 == __CPROVER_contracts_write_set_check_assignment!0#3
// 1120 file /Users/delmasrd/.rustup/toolchains/nightly-2024-12-18-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/range.rs line 767 column 13 function <std::ops::Range<i32> as std::iter::range::RangeIteratorImpl>::spec_next
(679) ASSERT(__check_lhs_assignment!0@1#2)

However later in the formula we see that &iter!0@1 is removed from the write set:

// 390 file <builtin-library-__CPROVER_contracts_library> line 660 function __CPROVER_contracts_write_set_record_dead
(1061) dynamic_object$13#4 == dynamic_object$13#3 WITH [(long int)__CPROVER_POINTER_OBJECT(&iter!0@1):=NULL]

And we immediately check that if the object is writable which is where the analysis fails

// 397 file <builtin-library-__CPROVER_contracts_library> line 784 function __CPROVER_contracts_write_set_check_assignment
(1170) \guard#4 == !(dynamic_object$13#4[(long int)__CPROVER_POINTER_OBJECT(&iter!0@1)] == NULL)
// 398 file <builtin-library-__CPROVER_contracts_library> line 785 function __CPROVER_contracts_write_set_check_assignment
(1171) __CPROVER_contracts_write_set_check_assignment!0#10 == TRUE
       guard: \guard#4
// 399 file <builtin-library-__CPROVER_contracts_library> line 785 function __CPROVER_contracts_write_set_check_assignment
// 400 file <builtin-library-__CPROVER_contracts_library> line 788 function __CPROVER_contracts_write_set_check_assignment
// 401 file <builtin-library-__CPROVER_contracts_library> line 789 function __CPROVER_contracts_write_set_check_assignment
(1172) __CPROVER_contracts_write_set_check_assignment!0#11 == FALSE
       guard: !\guard#4
// 402 file <builtin-library-__CPROVER_contracts_library> line 789 function __CPROVER_contracts_write_set_check_assignment
// 427 file <builtin-library-__CPROVER_contracts_library> line 818 function __CPROVER_contracts_write_set_check_assignment
(1173) __CPROVER_contracts_write_set_check_assignment!0#12 == \guard#4
// 427 file <builtin-library-__CPROVER_contracts_library> line 818 function __CPROVER_contracts_write_set_check_assignment
// 1119 file /Users/delmasrd/.rustup/toolchains/nightly-2024-12-18-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/range.rs line 767 column 13 function <std::ops::Range<i32> as std::iter::range::RangeIteratorImpl>::spec_next
(1174) __check_lhs_assignment!0@4#2 == __CPROVER_contracts_write_set_check_assignment!0#12
// 1120 file /Users/delmasrd/.rustup/toolchains/nightly-2024-12-18-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/range.rs line 767 column 13 function <std::ops::Range<i32> as std::iter::range::RangeIteratorImpl>::spec_next
(1175) ASSERT(__check_lhs_assignment!0@4#2)

From the immediate preceding context this is triggered at line 5 of the program, i.e. in the outer loop, not the inner loop.

// 861 file src/main.rs line 5 column 18 function proof::foo::{closure#2}::{closure#0}
(1064) __write_set_to_check!0@5#1 == &__contract_write_set!0@1

So this would mean that symex indeed confuses both iterators.

[remi-delmas-3000]

Looking at the translation rules from MIR to GOTO here ,

• Each MIR place declaration gives a GOTO DECL place;
• StorageLive gives __CPROVER_dead_object = __CPROVER_dead_object == &place ? NULL : __CPROVER_dead_object;
• StorageDead gives __CPROVER_dead_object = nondet() ? &place : __CPROVER_dead_object;

With this encoding a place is considered live by default, but is it really the case according to MIR semantics ?

At GOTO level shouldn't we immediately declare the place dead after declaration ?
So that its lifetime is actually delimited by pairs of [storageLive,storageDead] instead of [DECL, storageDead] followed by [storageLive, storageDead] ?

[remi-delmas-3000]

Update: this CBMC PR fixes the problem diffblue/cbmc#8554, by ignoring both storageLive and storageDead events at the contract instrumentation level. This eliminates the spurious CEX caused by only tracking storageDead and not storageLive at the contracts level.
The default --pointer-check will still detect invalid pointer accesses for objects where dynamic lifetime is modelled via __CPROVER_dead_object.

[tautschnig]

Re-opening as this should only be closed for good once Kani actually uses the fixed CBMC version.