Skip to content

Commit 0cc4b24

Browse files
karkhazkarkhaz
authoredMar 13, 2024··
Emit dead goto-instructions on MIR StatementDead (#3063)
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]( https://diffblue.github.io/cbmc/classcode__deadt.html) 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.
·
kani-0.60.0kani-0.48.0
1 parent e7a4d83 commit 0cc4b24

File tree

20 files changed

+65
-20
lines changed

20 files changed

+65
-20
lines changed
 

‎cprover_bindings/src/goto_program/stmt.rs

+7
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,8 @@ pub enum StmtBody {
5757
Break,
5858
/// `continue;`
5959
Continue,
60+
/// End-of-life of a local variable
61+
Dead(Expr),
6062
/// `lhs.typ lhs = value;` or `lhs.typ lhs;`
6163
Decl {
6264
lhs: Expr, // SymbolExpr
@@ -232,6 +234,11 @@ impl Stmt {
232234
BuiltinFn::CProverCover.call(vec![cond], loc).as_stmt(loc)
233235
}
234236

237+
/// Local variable goes out of scope
238+
pub fn dead(symbol: Expr, loc: Location) -> Self {
239+
stmt!(Dead(symbol), loc)
240+
}
241+
235242
/// `lhs.typ lhs = value;` or `lhs.typ lhs;`
236243
pub fn decl(lhs: Expr, value: Option<Expr>, loc: Location) -> Self {
237244
assert!(lhs.is_symbol());

‎cprover_bindings/src/irep/to_irep.rs

+1
Original file line numberDiff line numberDiff line change
@@ -433,6 +433,7 @@ impl ToIrep for StmtBody {
433433
}
434434
StmtBody::Break => code_irep(IrepId::Break, vec![]),
435435
StmtBody::Continue => code_irep(IrepId::Continue, vec![]),
436+
StmtBody::Dead(symbol) => code_irep(IrepId::Dead, vec![symbol.to_irep(mm)]),
436437
StmtBody::Decl { lhs, value } => {
437438
if value.is_some() {
438439
code_irep(

‎kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -381,7 +381,7 @@ impl<'tcx> GotocCtx<'tcx> {
381381
}
382382

383383
/// Codegen for a local
384-
fn codegen_local(&mut self, l: Local) -> Expr {
384+
pub fn codegen_local(&mut self, l: Local) -> Expr {
385385
let local_ty = self.local_ty_stable(l);
386386
// Check if the local is a function definition (see comment above)
387387
if let Some(fn_def) = self.codegen_local_fndef(local_ty) {

‎kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

+4-2
Original file line numberDiff line numberDiff line change
@@ -75,8 +75,10 @@ impl<'tcx> GotocCtx<'tcx> {
7575
.goto_expr;
7676
self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location)
7777
}
78-
StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me
79-
StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me
78+
StatementKind::StorageLive(var_id) => {
79+
Stmt::decl(self.codegen_local(*var_id), None, location)
80+
}
81+
StatementKind::StorageDead(var_id) => Stmt::dead(self.codegen_local(*var_id), location),
8082
StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(
8183
CopyNonOverlapping { src, dst, count },
8284
)) => {

‎kani-driver/src/call_single_file.rs

+2
Original file line numberDiff line numberDiff line change
@@ -122,6 +122,8 @@ impl KaniSession {
122122
"symbol-mangling-version=v0",
123123
"-Z",
124124
"panic_abort_tests=yes",
125+
"-Z",
126+
"sanitizer=address",
125127
]
126128
.map(OsString::from),
127129
);

‎tests/coverage/reachable/assert-false/expected

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
coverage/reachable/assert-false/main.rs, 6, FULL
22
coverage/reachable/assert-false/main.rs, 7, FULL
3-
coverage/reachable/assert-false/main.rs, 11, FULL
4-
coverage/reachable/assert-false/main.rs, 12, FULL
5-
coverage/reachable/assert-false/main.rs, 15, FULL
3+
coverage/reachable/assert-false/main.rs, 11, PARTIAL
4+
coverage/reachable/assert-false/main.rs, 12, PARTIAL
5+
coverage/reachable/assert-false/main.rs, 15, PARTIAL
66
coverage/reachable/assert-false/main.rs, 16, FULL
77
coverage/reachable/assert-false/main.rs, 17, PARTIAL
88
coverage/reachable/assert-false/main.rs, 19, FULL

‎tests/coverage/reachable/assert/reachable_pass/expected

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
coverage/reachable/assert/reachable_pass/test.rs, 6, FULL
2-
coverage/reachable/assert/reachable_pass/test.rs, 7, FULL
2+
coverage/reachable/assert/reachable_pass/test.rs, 7, PARTIAL
33
coverage/reachable/assert/reachable_pass/test.rs, 8, FULL
44
coverage/reachable/assert/reachable_pass/test.rs, 10, FULL

‎tests/coverage/reachable/bounds/reachable_fail/expected

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
coverage/reachable/bounds/reachable_fail/test.rs, 5, PARTIAL
22
coverage/reachable/bounds/reachable_fail/test.rs, 6, NONE
3-
coverage/reachable/bounds/reachable_fail/test.rs, 10, FULL
3+
coverage/reachable/bounds/reachable_fail/test.rs, 10, PARTIAL
44
coverage/reachable/bounds/reachable_fail/test.rs, 11, NONE

‎tests/coverage/reachable/div-zero/reachable_fail/expected

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
coverage/reachable/div-zero/reachable_fail/test.rs, 5, PARTIAL
22
coverage/reachable/div-zero/reachable_fail/test.rs, 6, NONE
3-
coverage/reachable/div-zero/reachable_fail/test.rs, 10, FULL
3+
coverage/reachable/div-zero/reachable_fail/test.rs, 10, PARTIAL
44
coverage/reachable/div-zero/reachable_fail/test.rs, 11, NONE

‎tests/coverage/reachable/overflow/reachable_fail/expected

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
coverage/reachable/overflow/reachable_fail/test.rs, 8, PARTIAL
22
coverage/reachable/overflow/reachable_fail/test.rs, 9, FULL
33
coverage/reachable/overflow/reachable_fail/test.rs, 13, FULL
4-
coverage/reachable/overflow/reachable_fail/test.rs, 14, FULL
4+
coverage/reachable/overflow/reachable_fail/test.rs, 14, PARTIAL
55
coverage/reachable/overflow/reachable_fail/test.rs, 15, NONE

‎tests/coverage/reachable/rem-zero/reachable_fail/expected

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
coverage/reachable/rem-zero/reachable_fail/test.rs, 5, PARTIAL
22
coverage/reachable/rem-zero/reachable_fail/test.rs, 6, NONE
3-
coverage/reachable/rem-zero/reachable_fail/test.rs, 10, FULL
3+
coverage/reachable/rem-zero/reachable_fail/test.rs, 10, PARTIAL
44
coverage/reachable/rem-zero/reachable_fail/test.rs, 11, NONE

‎tests/coverage/unreachable/assert/expected

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
coverage/unreachable/assert/test.rs, 6, FULL
2-
coverage/unreachable/assert/test.rs, 7, FULL
3-
coverage/unreachable/assert/test.rs, 9, FULL
2+
coverage/unreachable/assert/test.rs, 7, PARTIAL
3+
coverage/unreachable/assert/test.rs, 9, PARTIAL
44
coverage/unreachable/assert/test.rs, 10, NONE
55
coverage/unreachable/assert/test.rs, 12, NONE
66
coverage/unreachable/assert/test.rs, 16, FULL

‎tests/coverage/unreachable/assert_eq/expected

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
coverage/unreachable/assert_eq/test.rs, 6, FULL
22
coverage/unreachable/assert_eq/test.rs, 7, FULL
3-
coverage/unreachable/assert_eq/test.rs, 8, FULL
3+
coverage/unreachable/assert_eq/test.rs, 8, PARTIAL
44
coverage/unreachable/assert_eq/test.rs, 9, NONE
55
coverage/unreachable/assert_eq/test.rs, 11, FULL

‎tests/coverage/unreachable/assert_ne/expected

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
coverage/unreachable/assert_ne/test.rs, 6, FULL
22
coverage/unreachable/assert_ne/test.rs, 7, FULL
33
coverage/unreachable/assert_ne/test.rs, 8, FULL
4-
coverage/unreachable/assert_ne/test.rs, 10, FULL
4+
coverage/unreachable/assert_ne/test.rs, 10, PARTIAL
55
coverage/unreachable/assert_ne/test.rs, 11, NONE
66
coverage/unreachable/assert_ne/test.rs, 14, FULL

‎tests/coverage/unreachable/check_id/expected

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
coverage/unreachable/check_id/main.rs, 5, FULL
2-
coverage/unreachable/check_id/main.rs, 6, FULL
2+
coverage/unreachable/check_id/main.rs, 6, PARTIAL
33
coverage/unreachable/check_id/main.rs, 8, NONE
44
coverage/unreachable/check_id/main.rs, 10, FULL
55
coverage/unreachable/check_id/main.rs, 14, FULL
@@ -12,5 +12,5 @@ coverage/unreachable/check_id/main.rs, 20, FULL
1212
coverage/unreachable/check_id/main.rs, 21, FULL
1313
coverage/unreachable/check_id/main.rs, 22, FULL
1414
coverage/unreachable/check_id/main.rs, 23, FULL
15-
coverage/unreachable/check_id/main.rs, 24, FULL
15+
coverage/unreachable/check_id/main.rs, 24, PARTIAL
1616
coverage/unreachable/check_id/main.rs, 25, NONE

‎tests/coverage/unreachable/if-statement/expected

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
coverage/unreachable/if-statement/main.rs, 5, FULL
1+
coverage/unreachable/if-statement/main.rs, 5, PARTIAL
22
coverage/unreachable/if-statement/main.rs, 7, PARTIAL
33
coverage/unreachable/if-statement/main.rs, 8, NONE
44
coverage/unreachable/if-statement/main.rs, 9, NONE

‎tests/coverage/unreachable/tutorial_unreachable/expected

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
coverage/unreachable/tutorial_unreachable/main.rs, 6, FULL
22
coverage/unreachable/tutorial_unreachable/main.rs, 7, FULL
3-
coverage/unreachable/tutorial_unreachable/main.rs, 8, FULL
3+
coverage/unreachable/tutorial_unreachable/main.rs, 8, PARTIAL
44
coverage/unreachable/tutorial_unreachable/main.rs, 9, NONE
55
coverage/unreachable/tutorial_unreachable/main.rs, 11, FULL

‎tests/coverage/unreachable/while-loop-break/expected

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
coverage/unreachable/while-loop-break/main.rs, 8, FULL
2-
coverage/unreachable/while-loop-break/main.rs, 9, FULL
2+
coverage/unreachable/while-loop-break/main.rs, 9, PARTIAL
33
coverage/unreachable/while-loop-break/main.rs, 10, FULL
44
coverage/unreachable/while-loop-break/main.rs, 11, FULL
55
coverage/unreachable/while-loop-break/main.rs, 13, FULL

‎tests/expected/dead-invalid-access-via-raw/expected

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
SUCCESS\
2+
address must be a multiple of its type's alignment
3+
FAILURE\
4+
unsafe { *raw_ptr } == 10
5+
SUCCESS\
6+
pointer NULL
7+
SUCCESS\
8+
pointer invalid
9+
SUCCESS\
10+
deallocated dynamic object
11+
FAILURE\
12+
dead object
13+
SUCCESS\
14+
pointer outside object bounds
15+
SUCCESS\
16+
invalid integer address

‎tests/expected/dead-invalid-access-via-raw/main.rs

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
//
4+
// This test checks an issue reported in github.com/model-checking/kani#3063.
5+
// The access of the raw pointer should fail because the value being dereferenced has gone out of
6+
// scope at the time of access.
7+
8+
#[kani::proof]
9+
pub fn check_invalid_ptr() {
10+
let raw_ptr = {
11+
let var = 10;
12+
&var as *const _
13+
};
14+
15+
// This should fail since it is de-referencing a dead object.
16+
assert_eq!(unsafe { *raw_ptr }, 10);
17+
}

0 commit comments

Comments
 (0)
Please sign in to comment.