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
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions cprover_bindings/src/goto_program/stmt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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<Expr>, loc: Location) -> Self {
assert!(lhs.is_symbol());
Expand Down
1 change: 1 addition & 0 deletions cprover_bindings/src/irep/to_irep.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -75,8 +75,10 @@ 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::StorageDead(_) => 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 },
)) => {
Expand Down
2 changes: 2 additions & 0 deletions kani-driver/src/call_single_file.rs
Original file line number Diff line number Diff line change
Expand Up @@ -122,6 +122,8 @@ impl KaniSession {
"symbol-mangling-version=v0",
"-Z",
"panic_abort_tests=yes",
"-Z",
"sanitizer=address",
zhassan-aws marked this conversation as resolved.
Show resolved Hide resolved
]
.map(OsString::from),
);
Expand Down
6 changes: 3 additions & 3 deletions tests/coverage/reachable/assert-false/expected
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion tests/coverage/reachable/assert/reachable_pass/expected
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion tests/coverage/reachable/bounds/reachable_fail/expected
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
@@ -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
4 changes: 2 additions & 2 deletions tests/coverage/unreachable/assert/expected
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion tests/coverage/unreachable/assert_eq/expected
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion tests/coverage/unreachable/assert_ne/expected
Original file line number Diff line number Diff line change
@@ -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
4 changes: 2 additions & 2 deletions tests/coverage/unreachable/check_id/expected
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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
2 changes: 1 addition & 1 deletion tests/coverage/unreachable/if-statement/expected
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion tests/coverage/unreachable/tutorial_unreachable/expected
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion tests/coverage/unreachable/while-loop-break/expected
Original file line number Diff line number Diff line change
@@ -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
Expand Down
16 changes: 16 additions & 0 deletions tests/expected/dead-invalid-access-via-raw/expected
Original file line number Diff line number Diff line change
@@ -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
17 changes: 17 additions & 0 deletions tests/expected/dead-invalid-access-via-raw/main.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
// 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.

karkhaz marked this conversation as resolved.
Show resolved Hide resolved
#[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);
}
Loading