Contract fails due to promoted constants being havocked

[zhassan-aws]

I tried this code:

extern crate kani;

#[derive(PartialEq, Eq)]
pub enum Foo {
    A,
    B,
}

#[kani::ensures(result == Foo::A)]
pub fn a() -> Foo {
    Foo::A
}

#[kani::proof_for_contract(a)]
fn check() {
    let _ = a();
}

using the following command line invocation:

kani enum_ensures_bug.rs -Zfunction-contracts

with Kani version: 7bf23a2

I expected to see this happen: Verification succeeds

Instead, this happened:

SUMMARY:
 ** 1 of 1336 failed
Failed Checks: result == Foo::A
 File: "enum_ensures_bug.rs", line 9, in a_check_7b31b

VERIFICATION:- FAILED
Verification Time: 1.9666983s

[zhassan-aws]

This occurs with structs as well, e.g.

extern crate kani;

#[derive(PartialEq, Eq)]
pub struct Foo {
    x: i32,
}

#[kani::ensures(result == Foo { x: 5 })]
pub fn a() -> Foo {
    Foo { x: 5 }
}

#[kani::proof_for_contract(a)]
fn check() {
        let _ = a();
}

SUMMARY:
 ** 1 of 1334 failed
Failed Checks: result == Foo { x: 5 }
 File: "ensures_struct.rs", line 8, in a_check_7d30f5

VERIFICATION:- FAILED
Verification Time: 1.9546859s

[zhassan-aws]

The same occurs with tuple structs:

extern crate kani;

#[derive(PartialEq, Eq)]
pub struct Foo(i32);

#[kani::ensures(result == Foo(5))]
pub fn a() -> Foo {
    Foo(5)
}

#[kani::proof_for_contract(a)]
fn check() {
        let _ = a();
}

SUMMARY:
 ** 1 of 1334 failed
Failed Checks: result == Foo(5)
 File: "ensures_struct.rs", line 6, in a_check_b53d87

VERIFICATION:- FAILED
Verification Time: 1.9567466s

[zhassan-aws]

This version works:

extern crate kani;

#[derive(PartialEq, Eq)]
pub struct Foo {
    x: i32,
}

impl Foo {
    pub fn new(x: i32) -> Foo {
        Foo { x }
    }
}

#[kani::ensures(result == Foo::new(5))]
pub fn a() -> Foo {
    Foo::new(5)
}

#[kani::proof_for_contract(a)]
fn check() {
        let _ = a();
}

SUMMARY:
 ** 0 of 1337 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 1.9658625s

[celinval]

This ensures seems to fail, which makes me think that this could be something weird is going on with promoted constants:

#[kani::ensures(Foo::A != Foo::B)] 

[zhassan-aws]

This one fails with the struct version as well:

#[kani::ensures(Foo { x: 3 } != Foo { x: 5 })]

[pi314mm]

I expanded the macros for the following test:

#[derive(PartialEq, Eq)]
enum Foo {
    A,
    B,
}

#[kani::ensures(|_| Foo::A != Foo::B)]
fn a() {
}

#[kani::proof_for_contract(a)]
fn check() {
  a();
}

Then simplified the expansion into this:

#[derive(PartialEq, Eq)]
enum Foo {
    A,
    B,
}

#[kanitool::checked_with = "check"]
#[kanitool::replaced_with = "b"]
#[kanitool::inner_check = "b"]
fn a() {}

#[allow(dead_code, unused_variables, unused_mut)]
fn check() {
    static mut REENTRY: bool = false;
    if unsafe { REENTRY } {}
    else {
        let _ = b();
        kani::assert(Foo::A != Foo::B, "Foo::A != Foo::B")
    }
}

fn b() {}

#[allow(dead_code)]
#[kanitool::proof_for_contract = "a"]
fn harness() { kani::internal::init_contracts(); { a(); } }

and this still causes the same error.

It seems like the error doesn't happen within the macro expansion, but within the kanitool::checked_with = "check" attribute. Surprisingly (since this function doesn't have any arguments), if we add #[kanitool::proof] to the check function, the test passes. It seems we are doing something for the kanitool::proof attribute that we aren't properly doing for the kanitool::checked_with.

[celinval]

Something is very weird... I created the following code:

extern crate kani;
use kani::Arbitrary;

#[derive(PartialEq, Eq, kani::Arbitrary)]
pub struct Foo(u8);

#[kani::requires(foo == Foo(1))]
pub fn foo_a(foo: Foo) -> Foo {
    kani::assume(foo == Foo(1));
    assert!(foo.0 == 1);
    foo
}

#[kani::proof_for_contract(foo_a)]
fn check_contract() {
    foo_a(kani::any());
}

#[kani::proof]
fn check_call() {
    foo_a(kani::any());
}

For some very weird reason, the check_contract fails but the check_call succeeds.

[celinval]

I think I know what's going on here! The problem is that CBMC is setting all static variables to nondet when we are enabling contracts. 🤦

I remember we had to add --nondet-static-exclude for the recursion tracker. It looks like we have to do that for every constant allocation. 😢

[celinval]

@remi-delmas-3000 how does CBMC handles static strings? Is there anyv way we can mark an allocation constant?

[celinval]

Talked to @remi-delmas-3000 offline, and he pointed me to this code where CBMC decides which static it is going to havoc.

It looks like tagging a symbol (and possibly the value too) with ID_C_no_nondet_initialization should do the trick.

[remi-delmas-3000]

Some explanations on what is going on: anonymous constants like Foo(1) that appear inline in expressions and are not bound using a let get lifted to const statics by the rustc compiler.

So this

#[kani::requires(foo == Foo(1))]
pub fn foo_a(foo: Foo) -> Foo {
    kani::assume(foo == Foo(1));
    assert!(foo.0 == 1);
    foo
}

becomes something like this:

static STATIC_FOO1 = Foo(1);

#[kani::requires(foo == Foo(1))]
pub fn foo_a(foo: Foo) -> Foo {
    kani::assume(foo == *&STATIC_FOO1);
    assert!(foo.0 == 1);
    foo
}

Static symbols like STATIC_FOO1 are havoced by CBMC when contracts are applied, unless you explicitly say they should not using the --nondet-static-exclude flag, if you set the ID_C_no_nondet_initialization boolean tag on the Irep representing the type or the value of the static symbol.

[celinval]

https://github.com/rust-lang/const-eval/blob/master/promotion.md