forked from rust-lang/rust
-
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.
Audit for
copy
intrinsic (rust-lang#1199)
* Add/restore tests for copy intrinsics * Audit for `copy` intrinsic * More expected tests (readable/writable)
- Loading branch information
1 parent
2aef548
commit deaa485
Showing
13 changed files
with
190 additions
and
48 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
FAILURE\ | ||
copy: attempt to compute number in bytes which would overflow |
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,18 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
||
// Checks that `copy` triggers an overflow failure if the `count` argument can | ||
// overflow a `usize` | ||
#[kani::proof] | ||
fn test_copy_unaligned() { | ||
let arr: [i32; 3] = [0, 1, 0]; | ||
let src: *const i32 = arr.as_ptr(); | ||
// Passing `max_count` is guaranteed to overflow | ||
// the count in bytes for `i32` pointers | ||
let max_count = usize::MAX / 4 + 1; | ||
|
||
unsafe { | ||
let dst = src.add(1) as *mut i32; | ||
core::intrinsics::copy(src, dst, max_count); | ||
} | ||
} |
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,2 @@ | ||
FAILURE\ | ||
`dst` is properly aligned |
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 | ||
|
||
// Checks that `copy` fails when `dst` is not aligned. | ||
#[kani::proof] | ||
fn test_copy_unaligned() { | ||
let arr: [i32; 3] = [0, 1, 0]; | ||
let src: *const i32 = arr.as_ptr(); | ||
|
||
unsafe { | ||
// Get an unaligned pointer with a single-byte offset | ||
let dst_i8: *const i8 = src.add(1) as *mut i8; | ||
let dst_unaligned = unsafe { dst_i8.add(1) as *mut i32 }; | ||
core::intrinsics::copy(src, dst_unaligned, 1); | ||
} | ||
} |
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,2 @@ | ||
FAILURE\ | ||
`src` is properly aligned |
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,17 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
||
// Checks that `copy` fails when `src` is not aligned. | ||
#[kani::proof] | ||
fn test_copy_unaligned() { | ||
let arr: [i32; 3] = [0, 1, 0]; | ||
let src: *const i32 = arr.as_ptr(); | ||
|
||
unsafe { | ||
// Get an unaligned pointer with a single-byte offset | ||
let src_i8: *const i8 = src as *const i8; | ||
let src_unaligned = unsafe { src_i8.add(1) as *const i32 }; | ||
let dst = src.add(1) as *mut i32; | ||
core::intrinsics::copy(src_unaligned, dst, 1); | ||
} | ||
} |
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,2 @@ | ||
FAILURE\ | ||
memmove source region readable |
16 changes: 16 additions & 0 deletions
16
tests/expected/intrinsics/copy/copy-unreadable-src/main.rs
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 | ||
|
||
// Checks that `copy` fails when `src` is not valid for reads. | ||
#[kani::proof] | ||
fn test_copy_invalid() { | ||
let arr: [i32; 3] = [0, 1, 0]; | ||
let src: *const i32 = arr.as_ptr(); | ||
|
||
unsafe { | ||
// Get an invalid pointer with a negative offset | ||
let src_invalid = unsafe { src.sub(1) as *const i32 }; | ||
let dst = src.add(1) as *mut i32; | ||
core::intrinsics::copy(src_invalid, dst, 1); | ||
} | ||
} |
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,2 @@ | ||
FAILURE\ | ||
memmove destination region writeable |
15 changes: 15 additions & 0 deletions
15
tests/expected/intrinsics/copy/copy-unwritable-dst/main.rs
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,15 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
||
// Checks that `copy` fails when `dst` is not valid for writes. | ||
#[kani::proof] | ||
fn test_copy_invalid() { | ||
let arr: [i32; 3] = [0, 1, 0]; | ||
let src: *const i32 = arr.as_ptr(); | ||
|
||
unsafe { | ||
// Get an invalid pointer with an out-of-bounds offset | ||
let dst_invalid = src.add(3) as *mut i32; | ||
core::intrinsics::copy(src, dst_invalid, 1); | ||
} | ||
} |
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,33 @@ | ||
// Copyright Kani Contributors | ||
// SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
||
// Check that `copy` works as expected: Copies a number `n` of elements from | ||
// pointer `src` to pointer `dst`, even if their regions overlap. | ||
|
||
#[kani::proof] | ||
fn test_copy_simple() { | ||
let mut expected_val = 42; | ||
let src: *mut i32 = &mut expected_val as *mut i32; | ||
let mut old_val = 99; | ||
let dst: *mut i32 = &mut old_val; | ||
unsafe { | ||
core::intrinsics::copy(src, dst, 1); | ||
assert!(*dst == expected_val); | ||
} | ||
} | ||
|
||
#[kani::proof] | ||
fn test_copy_with_overlap() { | ||
let arr: [i32; 3] = [0, 1, 0]; | ||
let src: *const i32 = arr.as_ptr(); | ||
|
||
unsafe { | ||
let dst = src.add(1) as *mut i32; | ||
core::intrinsics::copy(src, dst, 2); | ||
// The first value does not change | ||
assert!(arr[0] == 0); | ||
// The next values are copied from `arr[0..=1]` | ||
assert!(arr[1] == 0); | ||
assert!(arr[2] == 1); | ||
} | ||
} |
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