search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.06k stars 85 forks source link

Spurious failures caused by handling of storage markers #3099

Open zhassan-aws opened 4 months ago

zhassan-aws commented 4 months ago

The handling of MIR's storage markers (StorageLive and StorageDead) introduced in #3063 causes spurious failures.

For example, on tests/kani/Spurious/storage_fixme.rs, the following failures are reported:

** 33 of 305 failed (272 undetermined)
Failed Checks: rust_dealloc must be called on an object whose allocated size matches its layout
 File: "/home/ubuntu/git/kani/library/kani/kani_lib.c", line 86, in __rust_dealloc
Failed Checks: misaligned pointer dereference: address must be a multiple of its type's alignment
 File: "src/main.rs", line 149, in NodeRef::<marker::Dying, marker::Leaf>::len
Failed Checks: explicit panic
 File: "src/main.rs", line 300, in NodeRef::<marker::Dying, marker::Leaf>::force
Failed Checks: called `Option::unwrap()` on a `None` value
 File: "/home/ubuntu/.rustup/toolchains/nightly-2024-03-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs", line 1985, in std::option::unwrap_failed
Failed Checks: attempt to add with overflow
 File: "src/main.rs", line 336, in Handle::<NodeRef<marker::Dying, marker::Leaf>, marker::KV>::right_edge
Failed Checks: assertion failed: idx <= node.len()
 File: "src/main.rs", line 344, in Handle::<NodeRef<marker::Dying, marker::Leaf>, marker::Edge>::new_edge
Failed Checks: free argument must be NULL or valid pointer
 File: "/home/ubuntu/git/kani/library/kani/kani_lib.c", line 88, in __rust_dealloc
Failed Checks: free argument must be dynamic object
 File: "/home/ubuntu/git/kani/library/kani/kani_lib.c", line 88, in __rust_dealloc
Failed Checks: free argument has offset zero
 File: "/home/ubuntu/git/kani/library/kani/kani_lib.c", line 88, in __rust_dealloc
Failed Checks: double free
 File: "/home/ubuntu/git/kani/library/kani/kani_lib.c", line 88, in __rust_dealloc
Failed Checks: dereference failure: pointer NULL
 File: "src/main.rs", line 177, in NodeRef::<marker::Dying, marker::Leaf>::ascend
Failed Checks: dereference failure: pointer invalid
 File: "src/main.rs", line 177, in NodeRef::<marker::Dying, marker::Leaf>::ascend
Failed Checks: dereference failure: deallocated dynamic object
 File: "src/main.rs", line 177, in NodeRef::<marker::Dying, marker::Leaf>::ascend
Failed Checks: dereference failure: dead object
 File: "src/main.rs", line 177, in NodeRef::<marker::Dying, marker::Leaf>::ascend
Failed Checks: dereference failure: pointer outside object bounds
 File: "src/main.rs", line 177, in NodeRef::<marker::Dying, marker::Leaf>::ascend
Failed Checks: dereference failure: invalid integer address
 File: "src/main.rs", line 177, in NodeRef::<marker::Dying, marker::Leaf>::ascend
Failed Checks: dereference failure: deallocated dynamic object
 File: "/home/ubuntu/.rustup/toolchains/nightly-2024-03-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/alloc/layout.rs", line 142, in std::alloc::Layout::align
Failed Checks: dereference failure: deallocated dynamic object
 File: "/home/ubuntu/.rustup/toolchains/nightly-2024-03-15-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/alloc/layout.rs", line 129, in std::alloc::Layout::size
Failed Checks: dereference failure: pointer NULL
 File: "src/main.rs", line 149, in NodeRef::<marker::Dying, marker::Leaf>::len
Failed Checks: dereference failure: pointer invalid
 File: "src/main.rs", line 149, in NodeRef::<marker::Dying, marker::Leaf>::len
Failed Checks: dereference failure: deallocated dynamic object
 File: "src/main.rs", line 149, in NodeRef::<marker::Dying, marker::Leaf>::len
Failed Checks: dereference failure: dead object
 File: "src/main.rs", line 149, in NodeRef::<marker::Dying, marker::Leaf>::len
Failed Checks: dereference failure: pointer outside object bounds
 File: "src/main.rs", line 149, in NodeRef::<marker::Dying, marker::Leaf>::len
Failed Checks: dereference failure: invalid integer address
 File: "src/main.rs", line 149, in NodeRef::<marker::Dying, marker::Leaf>::len
Failed Checks: dereference failure: deallocated dynamic object
 File: "src/main.rs", line 159, in NodeRef::<marker::Dying, marker::Leaf>::as_leaf_ptr
Failed Checks: dereference failure: deallocated dynamic object
 File: "src/main.rs", line 180, in NodeRef::<marker::Dying, marker::Leaf>::ascend::{closure#0}
Failed Checks: dereference failure: pointer NULL
 File: "src/main.rs", line 181, in NodeRef::<marker::Dying, marker::Leaf>::ascend::{closure#0}
Failed Checks: dereference failure: pointer invalid
 File: "src/main.rs", line 181, in NodeRef::<marker::Dying, marker::Leaf>::ascend::{closure#0}
Failed Checks: dereference failure: deallocated dynamic object
 File: "src/main.rs", line 181, in NodeRef::<marker::Dying, marker::Leaf>::ascend::{closure#0}
Failed Checks: dereference failure: dead object
 File: "src/main.rs", line 181, in NodeRef::<marker::Dying, marker::Leaf>::ascend::{closure#0}
Failed Checks: dereference failure: pointer outside object bounds
 File: "src/main.rs", line 181, in NodeRef::<marker::Dying, marker::Leaf>::ascend::{closure#0}
Failed Checks: dereference failure: invalid integer address
 File: "src/main.rs", line 181, in NodeRef::<marker::Dying, marker::Leaf>::ascend::{closure#0}
Failed Checks: unwinding assertion loop 0
 File: "src/main.rs", line 527, in Handle::<NodeRef<marker::Dying, marker::Leaf>, marker::Edge>::deallocating_end
zhassan-aws commented 4 months ago

If I replace the handling of StorageLive and StorageDead here by Stmt::skip(location), the failures disappear.