-
Notifications
You must be signed in to change notification settings - Fork 84
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Instrument validity checks for pointer to reference casts for slices …
…and str's
- Loading branch information
1 parent
76ad701
commit e88fec1
Showing
8 changed files
with
106 additions
and
39 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
Status: FAILURE\ | ||
Description: "dereference failure: pointer invalid"\ | ||
|
||
Verification failed for - check_with_byte_add | ||
Verification failed for - check_with_metadata | ||
Complete - 1 successfully verified harnesses, 2 failures, 3 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,36 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
#![feature(set_ptr_value)] | ||
|
||
//! This test checks that Kani detects UB resulting from converting a raw | ||
//! pointer to a reference when the metadata is not valid. | ||
|
||
// Generate invalid fat pointer by combining the metadata. | ||
#[kani::proof] | ||
fn check_with_metadata_fail() { | ||
let short = [0u32; 2]; | ||
let long = [0u32; 10]; | ||
let ptr = &short as *const [u32]; | ||
// This should trigger UB since the slice is not valid for the new length. | ||
let fake_long = unsafe { &*ptr.with_metadata_of(&long) }; | ||
assert_eq!(fake_long.len(), long.len()); | ||
} | ||
|
||
#[kani::proof] | ||
fn check_with_byte_add_fail() { | ||
let data = [5u8; 5]; | ||
let ptr = &data as *const [u8]; | ||
// This should trigger UB since the metadata does not get adjusted. | ||
let val = unsafe { &*ptr.byte_add(1) }; | ||
assert_eq!(val.len(), data.len()); | ||
} | ||
|
||
#[kani::proof] | ||
fn check_with_byte_add_sub_pass() { | ||
let data = [5u8; 5]; | ||
let ptr = &data as *const [u8]; | ||
let offset = kani::any_where(|i| *i < 100); | ||
// This should pass since the resulting metadata is valid | ||
let val = unsafe { &*ptr.byte_add(offset).byte_sub(offset) }; | ||
assert_eq!(val.len(), data.len()); | ||
} |
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,5 @@ | ||
Status: FAILURE\ | ||
Description: "dereference failure: pointer invalid"\ | ||
|
||
VERIFICATION:- FAILED | ||
Verification failed for - check_with_metadata |
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,16 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
#![feature(set_ptr_value)] | ||
|
||
//! This test checks that Kani detects UB resulting from converting a raw | ||
//! pointer to a reference when the metadata is not valid. | ||
|
||
#[kani::proof] | ||
fn check_with_metadata_fail() { | ||
let short = "sh"; | ||
let long = "longer"; | ||
let ptr = short as *const str; | ||
// This should trigger UB since the slice is not valid for the new length. | ||
let fake_long = unsafe { &*ptr.with_metadata_of(long) }; | ||
assert_eq!(fake_long.len(), long.len()); | ||
} |
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