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.
Instrument validity checks for pointer to reference casts for slices …
…and str's
- Loading branch information
1 parent
76ad701
commit 46e0856
Showing
9 changed files
with
165 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() { | ||
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() { | ||
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() { | ||
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() { | ||
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
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,59 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
// kani-flags: --default-unwind 5 | ||
|
||
//! This test case checks the usage of slices of slices (&[&[T]]). | ||
use std::mem::size_of_val; | ||
|
||
/// Structure with a raw string (i.e.: [char]). | ||
struct MyStr { | ||
header: u16, | ||
data: str, | ||
} | ||
|
||
impl MyStr { | ||
/// This creates a MyStr from a byte slice. | ||
fn new(original: &mut String) -> &mut Self { | ||
let buf = original.get_mut(..).unwrap(); | ||
assert!(size_of_val(buf) > 2, "This requires at least 2 bytes"); | ||
let unsized_len = buf.len() - 2; | ||
let ptr = std::ptr::slice_from_raw_parts_mut(buf.as_mut_ptr(), unsized_len); | ||
unsafe { &mut *(ptr as *mut Self) } | ||
} | ||
} | ||
|
||
#[kani::proof] | ||
fn sanity_check_my_str() { | ||
let mut buf = String::from("123456"); | ||
let my_str = MyStr::new(&mut buf); | ||
my_str.header = 0; | ||
|
||
assert_eq!(size_of_val(my_str), 6); | ||
assert_eq!(my_str.data.len(), 4); | ||
assert_eq!(my_str.data.chars().nth(0), Some('3')); | ||
assert_eq!(my_str.data.chars().nth(3), Some('6')); | ||
} | ||
|
||
#[kani::proof] | ||
fn check_slice_my_str() { | ||
let mut buf_0 = String::from("000"); | ||
let mut buf_1 = String::from("001"); | ||
let my_slice = &[MyStr::new(&mut buf_0), MyStr::new(&mut buf_1)]; | ||
assert_eq!(my_slice.len(), 2); | ||
|
||
assert_eq!(my_slice[0].data.len(), 1); | ||
assert_eq!(my_slice[1].data.len(), 1); | ||
|
||
assert_eq!(my_slice[0].data.chars().nth(0), Some('0')); | ||
assert_eq!(my_slice[1].data.chars().nth(0), Some('1')); | ||
} | ||
|
||
#[kani::proof] | ||
fn check_size_of_val() { | ||
let mut buf_0 = String::from("000"); | ||
let mut buf_1 = String::from("001"); | ||
let my_slice = &[MyStr::new(&mut buf_0), MyStr::new(&mut buf_1)]; | ||
assert_eq!(size_of_val(my_slice), 32); // Slice of 2 fat pointers. | ||
assert_eq!(size_of_val(my_slice[0]), 4); // Size of a fat pointer. | ||
assert_eq!(size_of_val(&my_slice[0].data), 1); // Size of str. | ||
} |