Skip to content

Commit 285ac5b

Browse files
artemagvanianartemagvanian
committed
Put the extra check behind an unstable feature flag
1 parent 4561d35 commit 285ac5b

File tree

6 files changed

+32
-17
lines changed

6 files changed

+32
-17
lines changed

‎kani-compiler/src/args.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,4 +85,7 @@ pub enum ExtraChecks {
8585
/// Check that produced values are valid except for uninitialized values.
8686
/// See https://github.com/model-checking/kani/issues/920.
8787
Validity,
88+
/// Check that pointer is valid before casting it to reference.
89+
/// See https://github.com/model-checking/kani/issues/2975.
90+
PtrToRefCast,
8891
}

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

Lines changed: 12 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

4+
use crate::args::ExtraChecks;
45
use crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace;
56
use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable;
67
use crate::codegen_cprover_gotoc::codegen::PropertyClass;
@@ -723,13 +724,17 @@ impl<'tcx> GotocCtx<'tcx> {
723724
Rvalue::Repeat(op, sz) => self.codegen_rvalue_repeat(op, sz, loc),
724725
Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => {
725726
let place_ref = self.codegen_place_ref_stable(&p);
726-
let place_ref_type = place_ref.typ().clone();
727-
match self.codegen_raw_ptr_deref_validity_check(&p, &loc) {
728-
Some(ptr_validity_check_expr) => Expr::statement_expression(
729-
vec![ptr_validity_check_expr, place_ref.as_stmt(loc)],
730-
place_ref_type,
731-
),
732-
None => place_ref,
727+
if self.queries.args().ub_check.contains(&ExtraChecks::PtrToRefCast) {
728+
let place_ref_type = place_ref.typ().clone();
729+
match self.codegen_raw_ptr_deref_validity_check(&p, &loc) {
730+
Some(ptr_validity_check_expr) => Expr::statement_expression(
731+
vec![ptr_validity_check_expr, place_ref.as_stmt(loc)],
732+
place_ref_type,
733+
),
734+
None => place_ref,
735+
}
736+
} else {
737+
place_ref
733738
}
734739
}
735740
Rvalue::Len(p) => self.codegen_rvalue_len(p),

‎kani-driver/src/call_single_file.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -105,6 +105,10 @@ impl KaniSession {
105105
flags.push("--ub-check=validity".into())
106106
}
107107

108+
if self.args.common_args.unstable_features.contains(UnstableFeature::PtrToRefCastChecks) {
109+
flags.push("--ub-check=ptr_to_ref_cast".into())
110+
}
111+
108112
if self.args.ignore_locals_lifetime {
109113
flags.push("--ignore-storage-markers".into())
110114
}

‎kani_metadata/src/unstable.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -89,6 +89,8 @@ pub enum UnstableFeature {
8989
ValidValueChecks,
9090
/// Ghost state and shadow memory APIs
9191
GhostState,
92+
/// Pointer validity checks when casting pointer to reference.
93+
PtrToRefCastChecks,
9294
}
9395

9496
impl UnstableFeature {

‎tests/expected/ptr_to_ref_cast/expected

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -2,67 +2,67 @@ Checking harness check_zst_deref...
22

33
Status: FAILURE
44
Description: "dereferencing a pointer to invalid memory location"
5-
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:131:35 in function zst_deref
5+
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:132:35 in function zst_deref
66

77
VERIFICATION:- FAILED
88

99
Checking harness check_equal_size_deref...
1010

1111
Status: SUCCESS
1212
Description: "dereferencing a pointer to invalid memory location"
13-
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:106:31 in function equal_size_deref
13+
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:107:31 in function equal_size_deref
1414

1515
Status: SUCCESS
1616
Description: "dereferencing a pointer to invalid memory location"
17-
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:109:38 in function equal_size_deref
17+
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:110:38 in function equal_size_deref
1818

1919
VERIFICATION:- SUCCESSFUL
2020

2121
Checking harness check_smaller_deref...
2222

2323
Status: SUCCESS
2424
Description: "dereferencing a pointer to invalid memory location"
25-
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:88:31 in function smaller_deref
25+
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:89:31 in function smaller_deref
2626

2727
Status: SUCCESS
2828
Description: "dereferencing a pointer to invalid memory location"
29-
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:92:38 in function smaller_deref
29+
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:93:38 in function smaller_deref
3030

3131
VERIFICATION:- SUCCESSFUL
3232

3333
Checking harness check_larger_deref_struct...
3434

3535
Status: FAILURE
3636
Description: "dereferencing a pointer to invalid memory location"
37-
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:74:31 in function larger_deref_struct
37+
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:75:31 in function larger_deref_struct
3838

3939
VERIFICATION:- FAILED
4040

4141
Checking harness check_larger_deref_into_ptr...
4242

4343
Status: FAILURE
4444
Description: "dereferencing a pointer to invalid memory location"
45-
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:48:38 in function larger_deref_into_ptr
45+
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:49:38 in function larger_deref_into_ptr
4646

4747
VERIFICATION:- FAILED
4848

4949
Checking harness check_larger_deref...
5050

5151
Status: FAILURE
5252
Description: "dereferencing a pointer to invalid memory location"
53-
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:34:32 in function larger_deref
53+
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:35:32 in function larger_deref
5454

5555
VERIFICATION:- FAILED
5656

5757
Checking harness check_store...
5858

5959
Status: FAILURE
6060
Description: "dereferencing a pointer to invalid memory location"
61-
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:17:28 in function Store::<'_, 3>::from
61+
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:18:28 in function Store::<'_, 3>::from
6262

6363
Status: SUCCESS
6464
Description: "assertion failed: broken.data.len() == 3"
65-
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:26:5 in function check_store
65+
Location: tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs:27:5 in function check_store
6666

6767
VERIFICATION:- FAILED
6868

‎tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
// kani-flags: -Z ptr-to-ref-cast-checks
34

45
//! This test case checks that raw pointer validity is checked before converting it to a reference, e.g., &(*ptr).
56

0 commit comments

Comments
 (0)