From 60c837ebf6e31be5ab5b098270d4a657820b9990 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Wed, 6 Mar 2024 23:58:40 +0000 Subject: [PATCH 1/7] Add a new Dead goto-instruction 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. --- cprover_bindings/src/goto_program/stmt.rs | 7 +++++++ cprover_bindings/src/irep/to_irep.rs | 1 + 2 files changed, 8 insertions(+) diff --git a/cprover_bindings/src/goto_program/stmt.rs b/cprover_bindings/src/goto_program/stmt.rs index 58755a0bffae..951e58f9a954 100644 --- a/cprover_bindings/src/goto_program/stmt.rs +++ b/cprover_bindings/src/goto_program/stmt.rs @@ -57,6 +57,8 @@ pub enum StmtBody { Break, /// `continue;` Continue, + /// End-of-life of a local variable + Dead(Expr), /// `lhs.typ lhs = value;` or `lhs.typ lhs;` Decl { lhs: Expr, // SymbolExpr @@ -232,6 +234,11 @@ impl Stmt { BuiltinFn::CProverCover.call(vec![cond], loc).as_stmt(loc) } + /// Local variable goes out of scope + pub fn dead(symbol: Expr, loc: Location) -> Self { + stmt!(Dead(symbol), loc) + } + /// `lhs.typ lhs = value;` or `lhs.typ lhs;` pub fn decl(lhs: Expr, value: Option, loc: Location) -> Self { assert!(lhs.is_symbol()); diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 16b8b69c8fe7..5c17ecf87b5d 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -433,6 +433,7 @@ impl ToIrep for StmtBody { } StmtBody::Break => code_irep(IrepId::Break, vec![]), StmtBody::Continue => code_irep(IrepId::Continue, vec![]), + StmtBody::Dead(symbol) => code_irep(IrepId::Dead, vec![symbol.to_irep(mm)]), StmtBody::Decl { lhs, value } => { if value.is_some() { code_irep( From f3c4d7d934b4a695d726dcb7e641a5be025634f3 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Thu, 7 Mar 2024 00:01:20 +0000 Subject: [PATCH 2/7] Fail when accessing dead local var via raw pointer Kani now codegens goto-program Dead instructions when it sees MIR StatementDead statements. This commit fixes #3061. --- kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs | 2 +- kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 9296b713c862..6b764fb63365 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -381,7 +381,7 @@ impl<'tcx> GotocCtx<'tcx> { } /// Codegen for a local - fn codegen_local(&mut self, l: Local) -> Expr { + pub fn codegen_local(&mut self, l: Local) -> Expr { let local_ty = self.local_ty_stable(l); // Check if the local is a function definition (see comment above) if let Some(fn_def) = self.codegen_local_fndef(local_ty) { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 05b153f9583f..1c830fda438d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -76,7 +76,7 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location) } StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me - StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me + StatementKind::StorageDead(var_id) => Stmt::dead(self.codegen_local(*var_id), location), StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping( CopyNonOverlapping { src, dst, count }, )) => { From 46341e1d3ee623863f8e4264b06b2e59438c622e Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Thu, 7 Mar 2024 00:43:28 +0000 Subject: [PATCH 3/7] Enable address sanitizer 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. --- kani-driver/src/call_single_file.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 9b6e0598daa5..fc41bac69d9c 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -122,6 +122,8 @@ impl KaniSession { "symbol-mangling-version=v0", "-Z", "panic_abort_tests=yes", + "-Z", + "sanitizer=address", ] .map(OsString::from), ); From e928d3050c2eb6b359494f44ee9a9c3e34cd17d9 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Mon, 11 Mar 2024 23:01:36 +0000 Subject: [PATCH 4/7] Expect PARTIAL coverage results from some tests This is because new Dead instructions are being generated. --- tests/coverage/reachable/assert-false/expected | 6 +++--- tests/coverage/reachable/assert/reachable_pass/expected | 2 +- tests/coverage/reachable/bounds/reachable_fail/expected | 2 +- tests/coverage/reachable/div-zero/reachable_fail/expected | 2 +- tests/coverage/reachable/overflow/reachable_fail/expected | 2 +- tests/coverage/reachable/rem-zero/reachable_fail/expected | 2 +- tests/coverage/unreachable/assert/expected | 4 ++-- tests/coverage/unreachable/assert_eq/expected | 2 +- tests/coverage/unreachable/assert_ne/expected | 2 +- tests/coverage/unreachable/check_id/expected | 4 ++-- tests/coverage/unreachable/if-statement/expected | 2 +- tests/coverage/unreachable/tutorial_unreachable/expected | 2 +- tests/coverage/unreachable/while-loop-break/expected | 2 +- 13 files changed, 17 insertions(+), 17 deletions(-) diff --git a/tests/coverage/reachable/assert-false/expected b/tests/coverage/reachable/assert-false/expected index 7a9fef1ca77c..97ffbe1d96e4 100644 --- a/tests/coverage/reachable/assert-false/expected +++ b/tests/coverage/reachable/assert-false/expected @@ -1,8 +1,8 @@ coverage/reachable/assert-false/main.rs, 6, FULL coverage/reachable/assert-false/main.rs, 7, FULL -coverage/reachable/assert-false/main.rs, 11, FULL -coverage/reachable/assert-false/main.rs, 12, FULL -coverage/reachable/assert-false/main.rs, 15, FULL +coverage/reachable/assert-false/main.rs, 11, PARTIAL +coverage/reachable/assert-false/main.rs, 12, PARTIAL +coverage/reachable/assert-false/main.rs, 15, PARTIAL coverage/reachable/assert-false/main.rs, 16, FULL coverage/reachable/assert-false/main.rs, 17, PARTIAL coverage/reachable/assert-false/main.rs, 19, FULL diff --git a/tests/coverage/reachable/assert/reachable_pass/expected b/tests/coverage/reachable/assert/reachable_pass/expected index 67ae085a3e83..9d21185b3a83 100644 --- a/tests/coverage/reachable/assert/reachable_pass/expected +++ b/tests/coverage/reachable/assert/reachable_pass/expected @@ -1,4 +1,4 @@ coverage/reachable/assert/reachable_pass/test.rs, 6, FULL -coverage/reachable/assert/reachable_pass/test.rs, 7, FULL +coverage/reachable/assert/reachable_pass/test.rs, 7, PARTIAL coverage/reachable/assert/reachable_pass/test.rs, 8, FULL coverage/reachable/assert/reachable_pass/test.rs, 10, FULL diff --git a/tests/coverage/reachable/bounds/reachable_fail/expected b/tests/coverage/reachable/bounds/reachable_fail/expected index af2f30e51fe2..fedfec8b2a1e 100644 --- a/tests/coverage/reachable/bounds/reachable_fail/expected +++ b/tests/coverage/reachable/bounds/reachable_fail/expected @@ -1,4 +1,4 @@ coverage/reachable/bounds/reachable_fail/test.rs, 5, PARTIAL coverage/reachable/bounds/reachable_fail/test.rs, 6, NONE -coverage/reachable/bounds/reachable_fail/test.rs, 10, FULL +coverage/reachable/bounds/reachable_fail/test.rs, 10, PARTIAL coverage/reachable/bounds/reachable_fail/test.rs, 11, NONE diff --git a/tests/coverage/reachable/div-zero/reachable_fail/expected b/tests/coverage/reachable/div-zero/reachable_fail/expected index 1ec1abefffd8..c1ac77404680 100644 --- a/tests/coverage/reachable/div-zero/reachable_fail/expected +++ b/tests/coverage/reachable/div-zero/reachable_fail/expected @@ -1,4 +1,4 @@ coverage/reachable/div-zero/reachable_fail/test.rs, 5, PARTIAL coverage/reachable/div-zero/reachable_fail/test.rs, 6, NONE -coverage/reachable/div-zero/reachable_fail/test.rs, 10, FULL +coverage/reachable/div-zero/reachable_fail/test.rs, 10, PARTIAL coverage/reachable/div-zero/reachable_fail/test.rs, 11, NONE diff --git a/tests/coverage/reachable/overflow/reachable_fail/expected b/tests/coverage/reachable/overflow/reachable_fail/expected index f20826fb1a8e..d45edcc37a63 100644 --- a/tests/coverage/reachable/overflow/reachable_fail/expected +++ b/tests/coverage/reachable/overflow/reachable_fail/expected @@ -1,5 +1,5 @@ coverage/reachable/overflow/reachable_fail/test.rs, 8, PARTIAL coverage/reachable/overflow/reachable_fail/test.rs, 9, FULL coverage/reachable/overflow/reachable_fail/test.rs, 13, FULL -coverage/reachable/overflow/reachable_fail/test.rs, 14, FULL +coverage/reachable/overflow/reachable_fail/test.rs, 14, PARTIAL coverage/reachable/overflow/reachable_fail/test.rs, 15, NONE diff --git a/tests/coverage/reachable/rem-zero/reachable_fail/expected b/tests/coverage/reachable/rem-zero/reachable_fail/expected index f7fa6ed7efeb..7852461e4f57 100644 --- a/tests/coverage/reachable/rem-zero/reachable_fail/expected +++ b/tests/coverage/reachable/rem-zero/reachable_fail/expected @@ -1,4 +1,4 @@ coverage/reachable/rem-zero/reachable_fail/test.rs, 5, PARTIAL coverage/reachable/rem-zero/reachable_fail/test.rs, 6, NONE -coverage/reachable/rem-zero/reachable_fail/test.rs, 10, FULL +coverage/reachable/rem-zero/reachable_fail/test.rs, 10, PARTIAL coverage/reachable/rem-zero/reachable_fail/test.rs, 11, NONE diff --git a/tests/coverage/unreachable/assert/expected b/tests/coverage/unreachable/assert/expected index f5b5f8044769..9bc6d8faa4f9 100644 --- a/tests/coverage/unreachable/assert/expected +++ b/tests/coverage/unreachable/assert/expected @@ -1,6 +1,6 @@ coverage/unreachable/assert/test.rs, 6, FULL -coverage/unreachable/assert/test.rs, 7, FULL -coverage/unreachable/assert/test.rs, 9, FULL +coverage/unreachable/assert/test.rs, 7, PARTIAL +coverage/unreachable/assert/test.rs, 9, PARTIAL coverage/unreachable/assert/test.rs, 10, NONE coverage/unreachable/assert/test.rs, 12, NONE coverage/unreachable/assert/test.rs, 16, FULL diff --git a/tests/coverage/unreachable/assert_eq/expected b/tests/coverage/unreachable/assert_eq/expected index f4e7608b2c13..9b13c3c96ded 100644 --- a/tests/coverage/unreachable/assert_eq/expected +++ b/tests/coverage/unreachable/assert_eq/expected @@ -1,5 +1,5 @@ coverage/unreachable/assert_eq/test.rs, 6, FULL coverage/unreachable/assert_eq/test.rs, 7, FULL -coverage/unreachable/assert_eq/test.rs, 8, FULL +coverage/unreachable/assert_eq/test.rs, 8, PARTIAL coverage/unreachable/assert_eq/test.rs, 9, NONE coverage/unreachable/assert_eq/test.rs, 11, FULL diff --git a/tests/coverage/unreachable/assert_ne/expected b/tests/coverage/unreachable/assert_ne/expected index 3b57defb4c36..f027f432e280 100644 --- a/tests/coverage/unreachable/assert_ne/expected +++ b/tests/coverage/unreachable/assert_ne/expected @@ -1,6 +1,6 @@ coverage/unreachable/assert_ne/test.rs, 6, FULL coverage/unreachable/assert_ne/test.rs, 7, FULL coverage/unreachable/assert_ne/test.rs, 8, FULL -coverage/unreachable/assert_ne/test.rs, 10, FULL +coverage/unreachable/assert_ne/test.rs, 10, PARTIAL coverage/unreachable/assert_ne/test.rs, 11, NONE coverage/unreachable/assert_ne/test.rs, 14, FULL diff --git a/tests/coverage/unreachable/check_id/expected b/tests/coverage/unreachable/check_id/expected index 214cbfa827bd..a2d296f0f9a3 100644 --- a/tests/coverage/unreachable/check_id/expected +++ b/tests/coverage/unreachable/check_id/expected @@ -1,5 +1,5 @@ coverage/unreachable/check_id/main.rs, 5, FULL -coverage/unreachable/check_id/main.rs, 6, FULL +coverage/unreachable/check_id/main.rs, 6, PARTIAL coverage/unreachable/check_id/main.rs, 8, NONE coverage/unreachable/check_id/main.rs, 10, FULL coverage/unreachable/check_id/main.rs, 14, FULL @@ -12,5 +12,5 @@ coverage/unreachable/check_id/main.rs, 20, FULL coverage/unreachable/check_id/main.rs, 21, FULL coverage/unreachable/check_id/main.rs, 22, FULL coverage/unreachable/check_id/main.rs, 23, FULL -coverage/unreachable/check_id/main.rs, 24, FULL +coverage/unreachable/check_id/main.rs, 24, PARTIAL coverage/unreachable/check_id/main.rs, 25, NONE diff --git a/tests/coverage/unreachable/if-statement/expected b/tests/coverage/unreachable/if-statement/expected index 4460f23a80de..8b481863a163 100644 --- a/tests/coverage/unreachable/if-statement/expected +++ b/tests/coverage/unreachable/if-statement/expected @@ -1,4 +1,4 @@ -coverage/unreachable/if-statement/main.rs, 5, FULL +coverage/unreachable/if-statement/main.rs, 5, PARTIAL coverage/unreachable/if-statement/main.rs, 7, PARTIAL coverage/unreachable/if-statement/main.rs, 8, NONE coverage/unreachable/if-statement/main.rs, 9, NONE diff --git a/tests/coverage/unreachable/tutorial_unreachable/expected b/tests/coverage/unreachable/tutorial_unreachable/expected index cf45a502d295..624aa520edc9 100644 --- a/tests/coverage/unreachable/tutorial_unreachable/expected +++ b/tests/coverage/unreachable/tutorial_unreachable/expected @@ -1,5 +1,5 @@ coverage/unreachable/tutorial_unreachable/main.rs, 6, FULL coverage/unreachable/tutorial_unreachable/main.rs, 7, FULL -coverage/unreachable/tutorial_unreachable/main.rs, 8, FULL +coverage/unreachable/tutorial_unreachable/main.rs, 8, PARTIAL coverage/unreachable/tutorial_unreachable/main.rs, 9, NONE coverage/unreachable/tutorial_unreachable/main.rs, 11, FULL diff --git a/tests/coverage/unreachable/while-loop-break/expected b/tests/coverage/unreachable/while-loop-break/expected index a0e43c183846..dc66d3e823d3 100644 --- a/tests/coverage/unreachable/while-loop-break/expected +++ b/tests/coverage/unreachable/while-loop-break/expected @@ -1,5 +1,5 @@ coverage/unreachable/while-loop-break/main.rs, 8, FULL -coverage/unreachable/while-loop-break/main.rs, 9, FULL +coverage/unreachable/while-loop-break/main.rs, 9, PARTIAL coverage/unreachable/while-loop-break/main.rs, 10, FULL coverage/unreachable/while-loop-break/main.rs, 11, FULL coverage/unreachable/while-loop-break/main.rs, 13, FULL From b318ed5b35240271f809ef042ef3bfea82da3d4a Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Mon, 11 Mar 2024 20:32:11 +0000 Subject: [PATCH 5/7] Codegen Stmt:decl when seeing StorageLive --- kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 1c830fda438d..6379a023423f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -75,7 +75,9 @@ impl<'tcx> GotocCtx<'tcx> { .goto_expr; self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location) } - StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me + StatementKind::StorageLive(var_id) => { + Stmt::decl(self.codegen_local(*var_id), None, location) + } StatementKind::StorageDead(var_id) => Stmt::dead(self.codegen_local(*var_id), location), StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping( CopyNonOverlapping { src, dst, count }, From d77ac68cae7ae7a566a1edd93eaf1b728a3f13af Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Tue, 12 Mar 2024 17:34:51 +0000 Subject: [PATCH 6/7] Add test case from issue #3061 --- .../dead-invalid-access-via-raw/expected | 16 ++++++++++++++++ .../expected/dead-invalid-access-via-raw/main.rs | 12 ++++++++++++ 2 files changed, 28 insertions(+) create mode 100644 tests/expected/dead-invalid-access-via-raw/expected create mode 100644 tests/expected/dead-invalid-access-via-raw/main.rs diff --git a/tests/expected/dead-invalid-access-via-raw/expected b/tests/expected/dead-invalid-access-via-raw/expected new file mode 100644 index 000000000000..1d464eb5f031 --- /dev/null +++ b/tests/expected/dead-invalid-access-via-raw/expected @@ -0,0 +1,16 @@ +SUCCESS\ +address must be a multiple of its type's alignment +FAILURE\ +unsafe { *raw_ptr } == 10 +SUCCESS\ +pointer NULL +SUCCESS\ +pointer invalid +SUCCESS\ +deallocated dynamic object +FAILURE\ +dead object +SUCCESS\ +pointer outside object bounds +SUCCESS\ +invalid integer address diff --git a/tests/expected/dead-invalid-access-via-raw/main.rs b/tests/expected/dead-invalid-access-via-raw/main.rs new file mode 100644 index 000000000000..299c25849a7b --- /dev/null +++ b/tests/expected/dead-invalid-access-via-raw/main.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +pub fn check_invalid_ptr() { + let raw_ptr = { + let var = 10; + &var as *const _ + }; + // This should fail since it is de-referencing a dead object. + assert_eq!(unsafe { *raw_ptr }, 10); +} From 5ba148a25da537ae2f4826f8057bdee837bc1326 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Wed, 13 Mar 2024 14:40:30 +0000 Subject: [PATCH 7/7] Add comment explaining test case --- tests/expected/dead-invalid-access-via-raw/main.rs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/tests/expected/dead-invalid-access-via-raw/main.rs b/tests/expected/dead-invalid-access-via-raw/main.rs index 299c25849a7b..ed3ea655839e 100644 --- a/tests/expected/dead-invalid-access-via-raw/main.rs +++ b/tests/expected/dead-invalid-access-via-raw/main.rs @@ -1,5 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// +// This test checks an issue reported in github.com/model-checking/kani#3063. +// The access of the raw pointer should fail because the value being dereferenced has gone out of +// scope at the time of access. #[kani::proof] pub fn check_invalid_ptr() { @@ -7,6 +11,7 @@ pub fn check_invalid_ptr() { let var = 10; &var as *const _ }; + // This should fail since it is de-referencing a dead object. assert_eq!(unsafe { *raw_ptr }, 10); }