forked from model-checking/kani
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Inject pointer validity check when casting raw pointers to references (…
…model-checking#3221) Resolves model-checking#2975 This PR makes Kani able to check if a raw pointer is valid before casting it to a reference. To check for the pointer validity when casting it to a reference, inject asserting `__CPROVER_r_ok(ptr, sz)` into places where a raw pointer is dereferenced and a reference is immediately taken. Since this check seems to cause some of the CIs to run out of memory, it is only enabled under `-Z ptr-to-ref-cast-checks` flag. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent
0bb1325
commit ffcb5ad
Showing
10 changed files
with
305 additions
and
4 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,75 @@ | ||
Checking harness check_zst_deref... | ||
|
||
Status: FAILURE\ | ||
Description: "dereference failure: pointer invalid"\ | ||
in function zst_deref | ||
|
||
VERIFICATION:- FAILED | ||
|
||
Checking harness check_equal_size_deref... | ||
|
||
Status: SUCCESS\ | ||
Description: "dereference failure: pointer invalid"\ | ||
in function equal_size_deref | ||
|
||
Status: SUCCESS\ | ||
Description: "dereference failure: pointer invalid"\ | ||
in function equal_size_deref | ||
|
||
VERIFICATION:- SUCCESSFUL | ||
|
||
Checking harness check_smaller_deref... | ||
|
||
Status: SUCCESS\ | ||
Description: "dereference failure: pointer invalid"\ | ||
in function smaller_deref | ||
|
||
Status: SUCCESS\ | ||
Description: "dereference failure: pointer invalid"\ | ||
in function smaller_deref | ||
|
||
VERIFICATION:- SUCCESSFUL | ||
|
||
Checking harness check_larger_deref_struct... | ||
|
||
Status: FAILURE\ | ||
Description: "dereference failure: pointer invalid"\ | ||
in function larger_deref_struct | ||
|
||
VERIFICATION:- FAILED | ||
|
||
Checking harness check_larger_deref_into_ptr... | ||
|
||
Status: FAILURE\ | ||
Description: "dereference failure: pointer invalid"\ | ||
in function larger_deref_into_ptr | ||
|
||
VERIFICATION:- FAILED | ||
|
||
Checking harness check_larger_deref... | ||
|
||
Status: FAILURE\ | ||
Description: "dereference failure: pointer invalid"\ | ||
in function larger_deref | ||
|
||
VERIFICATION:- FAILED | ||
|
||
Checking harness check_store... | ||
|
||
Status: FAILURE\ | ||
Description: "dereference failure: pointer invalid"\ | ||
in function Store::<'_, 3>::from | ||
|
||
Status: SUCCESS\ | ||
Description: "assertion failed: broken.data.len() == 3"\ | ||
in function check_store | ||
|
||
VERIFICATION:- FAILED | ||
|
||
Summary: | ||
Verification failed for - check_zst_deref | ||
Verification failed for - check_larger_deref_struct | ||
Verification failed for - check_larger_deref_into_ptr | ||
Verification failed for - check_larger_deref | ||
Verification failed for - check_store | ||
Complete - 2 successfully verified harnesses, 5 failures, 7 total. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,140 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
// kani-flags: -Z ptr-to-ref-cast-checks | ||
|
||
//! This test case checks that raw pointer validity is checked before converting it to a reference, e.g., &(*ptr). | ||
// 1. Original example. | ||
|
||
struct Store<'a, const LEN: usize> { | ||
data: [&'a i128; LEN], | ||
} | ||
|
||
impl<'a, const LEN: usize> Store<'a, LEN> { | ||
pub fn from(var: &i64) -> Self { | ||
let ref1: *const i64 = var; | ||
let ref2: *const i128 = ref1 as *const i128; | ||
unsafe { | ||
Store { data: [&*ref2; LEN] } // ---- THIS LINE SHOULD FAIL | ||
} | ||
} | ||
} | ||
|
||
#[kani::proof] | ||
pub fn check_store() { | ||
let val = 1; | ||
let broken = Store::<3>::from(&val); | ||
assert_eq!(broken.data.len(), 3) | ||
} | ||
|
||
// 2. Make sure the error is raised when casting to a simple type of a larger size. | ||
|
||
pub fn larger_deref(var: &i64) { | ||
let ref1: *const i64 = var; | ||
let ref2: *const i128 = ref1 as *const i128; | ||
let ref3: &i128 = unsafe { &*ref2 }; // ---- THIS LINE SHOULD FAIL | ||
} | ||
|
||
#[kani::proof] | ||
pub fn check_larger_deref() { | ||
let var: i64 = kani::any(); | ||
larger_deref(&var); | ||
} | ||
|
||
// 3. Make sure the error is raised when casting to a simple type of a larger size and storing the result in a pointer. | ||
|
||
pub fn larger_deref_into_ptr(var: &i64) { | ||
let ref1: *const i64 = var; | ||
let ref2: *const i128 = ref1 as *const i128; | ||
let ref3: *const i128 = unsafe { &*ref2 }; // ---- THIS LINE SHOULD FAIL | ||
} | ||
|
||
#[kani::proof] | ||
pub fn check_larger_deref_into_ptr() { | ||
let var: i64 = kani::any(); | ||
larger_deref_into_ptr(&var); | ||
} | ||
|
||
// 4. Make sure the error is raised when casting to a struct of a larger size. | ||
|
||
#[derive(kani::Arbitrary)] | ||
struct Foo { | ||
a: u8, | ||
} | ||
|
||
#[derive(kani::Arbitrary)] | ||
struct Bar { | ||
a: u8, | ||
b: u64, | ||
c: u64, | ||
} | ||
|
||
pub fn larger_deref_struct(var: &Foo) { | ||
let ref1: *const Foo = var; | ||
let ref2: *const Bar = ref1 as *const Bar; | ||
let ref3: &Bar = unsafe { &*ref2 }; // ---- THIS LINE SHOULD FAIL | ||
} | ||
|
||
#[kani::proof] | ||
pub fn check_larger_deref_struct() { | ||
let var: Foo = kani::any(); | ||
larger_deref_struct(&var); | ||
} | ||
|
||
// 5. Make sure the error is not raised if the target size is smaller. | ||
|
||
pub fn smaller_deref(var: &i64, var_struct: &Bar) { | ||
let ref1: *const i64 = var; | ||
let ref2: *const i32 = ref1 as *const i32; | ||
let ref3: &i32 = unsafe { &*ref2 }; | ||
|
||
let ref1_struct: *const Bar = var_struct; | ||
let ref2_struct: *const Foo = ref1_struct as *const Foo; | ||
let ref3_struct: &Foo = unsafe { &*ref2_struct }; | ||
} | ||
|
||
#[kani::proof] | ||
pub fn check_smaller_deref() { | ||
let var: i64 = kani::any(); | ||
let var_struct: Bar = kani::any(); | ||
smaller_deref(&var, &var_struct); | ||
} | ||
|
||
// 6. Make sure the error is not raised if the target size is the same. | ||
|
||
pub fn equal_size_deref(var: &i64, var_struct: &Foo) { | ||
let ref1: *const i64 = var; | ||
let ref2: &i64 = unsafe { &*ref1 }; | ||
|
||
let ref1_struct: *const Foo = var_struct; | ||
let ref2_struct: &Foo = unsafe { &*ref1_struct }; | ||
} | ||
|
||
#[kani::proof] | ||
pub fn check_equal_size_deref() { | ||
let var: i64 = kani::any(); | ||
let var_struct: Foo = kani::any(); | ||
equal_size_deref(&var, &var_struct); | ||
} | ||
|
||
// 7. Make sure the check works with ZSTs. | ||
|
||
#[derive(kani::Arbitrary)] | ||
struct Zero; | ||
|
||
pub fn zst_deref(var_struct: &Foo, var_zst: &Zero) { | ||
let ref1_struct: *const Foo = var_struct; | ||
let ref2_struct: *const Zero = ref1_struct as *const Zero; | ||
let ref3_struct: &Zero = unsafe { &*ref2_struct }; | ||
|
||
let ref1_zst: *const Zero = var_zst; | ||
let ref2_zst: *const Foo = ref1_zst as *const Foo; | ||
let ref3_zst: &Foo = unsafe { &*ref2_zst }; // ---- THIS LINE SHOULD FAIL | ||
} | ||
|
||
#[kani::proof] | ||
pub fn check_zst_deref() { | ||
let var_struct: Foo = kani::any(); | ||
let var_zst: Zero = kani::any(); | ||
zst_deref(&var_struct, &var_zst); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,3 +1,4 @@ | ||
Summary: | ||
Verification failed for - ptr::verify::check_replace_unit | ||
Complete - 5 successfully verified harnesses, 1 failures, 6 total. | ||
Verification failed for - ptr::verify::check_as_ref_dangling | ||
Complete - 4 successfully verified harnesses, 2 failures, 6 total. |