-
Notifications
You must be signed in to change notification settings - Fork 89
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
Contract fails due to promoted constants being havocked #3228
Comments
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();
}
|
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();
}
|
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();
}
|
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)] |
This one fails with the struct version as well: #[kani::ensures(Foo { x: 3 } != Foo { x: 5 })] |
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 |
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 |
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 |
@remi-delmas-3000 how does CBMC handles static strings? Is there anyv way we can mark an allocation constant? |
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 |
Some explanations on what is going on: anonymous constants like 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 |
When verifying contracts, CBMC initializes all static variables to non-deterministic values, except for those with constant types or with types / values annotated with `ID_C_no_nondet_initialization`. Kani compiler never set these flags, which caused spurious failures when verification depended on promoted constants or constant static variables. This fix changes that. First, I did a bit of refactoring since we may need to set this `Symbol` property at a later time for static variables. I also got rid of the initialization function, since the allocation initialization can be done directly from an expression. Then, I added the new property to the `Symbol` type. In CBMC, this is a property of the type or expression. However, I decided to add it to `Symbol` to avoid having to add this attribute to all variants of `Type` and `Expr`. Resolves #3228
I tried this code:
using the following command line invocation:
with Kani version: 7bf23a2
I expected to see this happen: Verification succeeds
Instead, this happened:
The text was updated successfully, but these errors were encountered: