Skip to content
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

Spurious failures caused by handling of storage markers #3099

Closed
zhassan-aws opened this issue Mar 21, 2024 · 1 comment · Fixed by #2995
Closed

Spurious failures caused by handling of storage markers #3099

zhassan-aws opened this issue Mar 21, 2024 · 1 comment · Fixed by #2995
Labels
[C] Bug This is a bug. Something isn't working. [F] Spurious Failure Issues that cause Kani verification to fail despite the code being correct.

Comments

@zhassan-aws
Copy link
Contributor

zhassan-aws commented Mar 21, 2024

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 zhassan-aws added [C] Bug This is a bug. Something isn't working. [F] Spurious Failure Issues that cause Kani verification to fail despite the code being correct. labels Mar 21, 2024
@zhassan-aws
Copy link
Contributor Author

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

zhassan-aws added a commit to zhassan-aws/kani that referenced this issue Mar 21, 2024
zhassan-aws added a commit to zhassan-aws/kani that referenced this issue Mar 21, 2024
zhassan-aws added a commit to zhassan-aws/kani that referenced this issue Mar 22, 2024
adpaco-aws pushed a commit that referenced this issue Mar 22, 2024
Add a reproducer for #3099.
tautschnig added a commit that referenced this issue Apr 5, 2024
Updated version in all `Cargo.toml` files (via
`find . -name Cargo.toml -exec sed -i 's/version = "0.48.0"/version =
"0.49.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files
updated.

GitHub generated release notes:

## What's Changed
* Upgrade Rust toolchain to 2024-03-14 by @zhassan-aws in
#3081
* Disable removal of storage markers by @zhassan-aws in
#3083
* Automatic cargo update to 2024-03-18 by @github-actions in
#3086
* Bump tests/perf/s2n-quic from `1a7faa8` to `9e39ca0` by @dependabot in
#3087
* Upgrade toolchain to nightly-2024-03-15 by @celinval in
#3084
* Add optional scatterplot to benchcomp output by @tautschnig in
#3077
* Benchcomp scatterplots: quote axis labels by @tautschnig in
#3097
* Expand ${var} in benchcomp variant `env` by @karkhaz in
#3090
* Add test for #3099 by @zhassan-aws in
#3100
* Automatic cargo update to 2024-03-25 by @github-actions in
#3103
* Bump tests/perf/s2n-quic from `1a7faa8` to `0a60ec1` by @dependabot in
#3104
* Implement validity checks by @celinval in
#3085
* Add `benchcomp filter` command by @karkhaz in
#3105
* Add CI test for --use-local-toolchain by @jaisnan in
#3074
* Upgrade Rust toolchain to `nightly-2024-03-21` by @adpaco-aws in
#3102
* Use `intrinsic_name` to get the intrinsic name by @adpaco-aws in
#3114
* Bump tests/perf/s2n-quic from `0a60ec1` to `2d5e891` by @dependabot in
#3118
* Allow modifies clause for verification only by @feliperodri in
#3098
* Automatic cargo update to 2024-04-01 by @github-actions in
#3117
* Automatic cargo update to 2024-04-04 by @github-actions in
#3122
* Remove bookrunner by @tautschnig in
#3123
* Upgrade Rust toolchain to nightly-2024-03-29 by @feliperodri in
#3116
* Remove unnecessary build step for some workflows by @zhassan-aws in
#3124
* Ensure storage markers are kept in std code by @zhassan-aws in
#3080


**Full Changelog**:
kani-0.48.0...kani-0.49.0
tautschnig added a commit to tautschnig/kani that referenced this issue Apr 26, 2024
This changes our handling of storage markers to be marking is-alive
only rather than treating StorageLive as creating a new object. That is,
object instances are now tied to their Mir-provided declarations (which,
at present, only appear once per function). To still account for when
Rust scopes deem an object to be alive, we use StorageLive and
StorageDead to update `__CPROVER_dead_object`. This (global) variable is
used by CBMC's pointer checks to track when a pointer may not be safe to
dereference for it could be pointing to an object that no longer is in
scope.

Resolves: model-checking#3099
zpzigi754 pushed a commit to zpzigi754/kani that referenced this issue May 8, 2024
Updated version in all `Cargo.toml` files (via
`find . -name Cargo.toml -exec sed -i 's/version = "0.48.0"/version =
"0.49.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files
updated.

GitHub generated release notes:

## What's Changed
* Upgrade Rust toolchain to 2024-03-14 by @zhassan-aws in
model-checking#3081
* Disable removal of storage markers by @zhassan-aws in
model-checking#3083
* Automatic cargo update to 2024-03-18 by @github-actions in
model-checking#3086
* Bump tests/perf/s2n-quic from `1a7faa8` to `9e39ca0` by @dependabot in
model-checking#3087
* Upgrade toolchain to nightly-2024-03-15 by @celinval in
model-checking#3084
* Add optional scatterplot to benchcomp output by @tautschnig in
model-checking#3077
* Benchcomp scatterplots: quote axis labels by @tautschnig in
model-checking#3097
* Expand ${var} in benchcomp variant `env` by @karkhaz in
model-checking#3090
* Add test for model-checking#3099 by @zhassan-aws in
model-checking#3100
* Automatic cargo update to 2024-03-25 by @github-actions in
model-checking#3103
* Bump tests/perf/s2n-quic from `1a7faa8` to `0a60ec1` by @dependabot in
model-checking#3104
* Implement validity checks by @celinval in
model-checking#3085
* Add `benchcomp filter` command by @karkhaz in
model-checking#3105
* Add CI test for --use-local-toolchain by @jaisnan in
model-checking#3074
* Upgrade Rust toolchain to `nightly-2024-03-21` by @adpaco-aws in
model-checking#3102
* Use `intrinsic_name` to get the intrinsic name by @adpaco-aws in
model-checking#3114
* Bump tests/perf/s2n-quic from `0a60ec1` to `2d5e891` by @dependabot in
model-checking#3118
* Allow modifies clause for verification only by @feliperodri in
model-checking#3098
* Automatic cargo update to 2024-04-01 by @github-actions in
model-checking#3117
* Automatic cargo update to 2024-04-04 by @github-actions in
model-checking#3122
* Remove bookrunner by @tautschnig in
model-checking#3123
* Upgrade Rust toolchain to nightly-2024-03-29 by @feliperodri in
model-checking#3116
* Remove unnecessary build step for some workflows by @zhassan-aws in
model-checking#3124
* Ensure storage markers are kept in std code by @zhassan-aws in
model-checking#3080


**Full Changelog**:
model-checking/kani@kani-0.48.0...kani-0.49.0
tautschnig added a commit to tautschnig/kani that referenced this issue Jun 20, 2024
This changes our handling of storage markers to be marking is-alive
only rather than treating StorageLive as creating a new object. That is,
object instances are now tied to their Mir-provided declarations (which,
at present, only appear once per function). To still account for when
Rust scopes deem an object to be alive, we use StorageLive and
StorageDead to update `__CPROVER_dead_object`. This (global) variable is
used by CBMC's pointer checks to track when a pointer may not be safe to
dereference for it could be pointing to an object that no longer is in
scope.

Resolves: model-checking#3099
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working. [F] Spurious Failure Issues that cause Kani verification to fail despite the code being correct.
Projects
None yet
1 participant