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

Emit dead goto-instructions on MIR StatementDead #3063

Merged
merged 7 commits into from
Mar 13, 2024

Conversation

karkhaz
Copy link
Contributor

@karkhaz karkhaz commented Mar 7, 2024

This commit adds a new Dead goto-instruction that gets codegened
whenever Kani sees a MIR StatementDead statement. This new
goto instruction corresponds to the CBMC code_deadt statement
that marks the point where a local variable goes out of scope.

This new instruction is needed to detect invalid accesses of dead local
variables.

The commit also codegens a CBMC Decl instruction upon seeing a MIR
StatementLive. This ensures that variables that go out of scope at the
end of a loop are not falsely marked as having a dead dereference when
they are accessed on the next loop iteration.

Resolves #3061

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Mar 7, 2024
@karkhaz karkhaz force-pushed the kk-emit-dead-statement branch 3 times, most recently from 62ebeaa to d4a82ab Compare March 12, 2024 17:26
This instruction corresponds to the cprover language's code_deadt and
marks the point where a variable goes out of scope. This new statement
type is needed in a future commit where MIR StorageDead statements get
codegenned into these new Dead statements.
Kani now codegens goto-program Dead instructions when it sees MIR
StatementDead statements.

This commit fixes model-checking#3061.
This turns off a MIR pass that drops StatementLive and StatementDead
nodes. These nodes are needed for us to detect when local variables go
out of scope.
This is because new Dead instructions are being generated.
@karkhaz karkhaz marked this pull request as ready for review March 12, 2024 18:56
@karkhaz karkhaz requested a review from a team as a code owner March 12, 2024 18:56
@karkhaz karkhaz enabled auto-merge (squash) March 12, 2024 19:35
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks good. Can you also please add a cargo test to ensure dependencies also contains these statements?

For that, you will have to create 2 crates. You add the defective code in one crate, and the harness in the other crate. Thanks!

kani-driver/src/call_single_file.rs Show resolved Hide resolved
@karkhaz karkhaz merged commit 0cc4b24 into model-checking:main Mar 13, 2024
20 checks passed
@karkhaz karkhaz deleted the kk-emit-dead-statement branch March 13, 2024 21:25
zhassan-aws added a commit that referenced this pull request Mar 13, 2024
These are the original release notes for the reference:

## What's Changed
* Automatic cargo update to 2024-02-26 by @github-actions in
#3043
* Upgrade rust toolchain to 2024-02-17 by @celinval in
#3040
* Upgrade `windows-targets` crate to version 0.52.4 by @adpaco-aws in
#3049
* Fix `codegen_atomic_binop` for `atomic_ptr` by @qinheping in
#3047
* Upgrade Rust toolchain to `nightly-2024-02-25` by @adpaco-aws in
#3048
* Update s2n-quic submodule by @zhassan-aws in
#3050
* Update s2n-quic submodule weekly through dependabot by @zhassan-aws in
#3053
* Retrieve info for recursion tracker reliably by @feliperodri in
#3045
* Automatic cargo update to 2024-03-04 by @github-actions in
#3055
* Upgrade Rust toolchain to `nightly-2024-03-01` by @adpaco-aws in
#3052
* Add `--use-local-toolchain` to Kani setup by @jaisnan in
#3056
* Replace internal reverse_postorder by a stable one by @celinval in
#3064
* Add option to override `--crate-name` from `kani` by @adpaco-aws in
#3054
* cargo update and fix macos CI by @zhassan-aws in
#3067
* Bump tests/perf/s2n-quic from `d103836` to `1a7faa8` by @dependabot in
#3066
* Upgrade toolchain to 2024-03-11 by @zhassan-aws in
#3071
* Emit `dead` goto-instructions on MIR StatementDead by @karkhaz in
#3063


**Full Changelog**:
kani-0.47.0...kani-0.48.0
@zhassan-aws
Copy link
Contributor

It looks good. Can you also please add a cargo test to ensure dependencies also contains these statements?

For that, you will have to create 2 crates. You add the defective code in one crate, and the harness in the other crate. Thanks!

I confirmed that these scenario is correctly captured by the fix. I'll open a PR that integrates that test.

zhassan-aws added a commit that referenced this pull request Mar 14, 2024
This is a follow-up on #3063 that adds a test with multiple crates to
make sure this scenario is correctly handled and that Kani reports the
bug.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
tautschnig pushed a commit that referenced this pull request Apr 5, 2024
This is a follow-up to #3063 that turns off that MIR pass while
compiling `std` as well to ensure any bugs of the same nature in `std`
are captured by Kani.

Resolves #3079
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Kani should fail due to invalid access of a dead local variable via raw pointer
3 participants