Skip to content

Commit 0623b87

Browse files
markrtuttletedinski
authored andcommitted
Add unsized pointer cast regression tests (rust-lang#89)
Add fat-pointer regression tests
1 parent 9027dde commit 0623b87

14 files changed

+316
-0
lines changed

Diff for: rust-tests/cbmc-reg/FatPointers/boxslice1.rs

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
// Casts boxed array to boxed slice (example taken from rust documentation)
5+
use std::str;
6+
7+
fn main() {
8+
// This vector of bytes is used to initialize a Box<[u8; 4]>
9+
let sparkle_heart_vec = vec![240, 159, 146, 150];
10+
11+
// This transformer produces a Box<[u8>]
12+
let _sparkle_heart_str = str::from_utf8(&sparkle_heart_vec);
13+
14+
// see boxslice2_fail.rs for an attempt to test sparkle_heart_str
15+
}

Diff for: rust-tests/cbmc-reg/FatPointers/boxslice2_fail.rs

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
// Casts boxed array to boxed slice (example taken from rust documentation)
5+
use std::str;
6+
7+
fn main() {
8+
// This vector of bytes is used to initialize a Box<[u8; 4]>
9+
let sparkle_heart_vec = vec![240, 159, 146, 150];
10+
11+
// This transformer produces a Box<[u8>]
12+
let sparkle_heart_str = str::from_utf8(&sparkle_heart_vec);
13+
14+
// This match statement generates failures even though
15+
// the binary runs without failures.
16+
match sparkle_heart_str {
17+
Ok(string) => match string.bytes().nth(0) {
18+
Some(b) => assert!(b == 240),
19+
_ => assert!(true),
20+
},
21+
_ => assert!(true),
22+
}
23+
}

Diff for: rust-tests/cbmc-reg/FatPointers/boxtrait.rs

+34
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
// This is handled by the box to box case of unsized pointers
5+
6+
pub trait Trait {
7+
fn increment(&mut self);
8+
fn get(&self) -> u32;
9+
}
10+
11+
struct Concrete {
12+
pub index: u32,
13+
}
14+
15+
impl Concrete {
16+
fn new() -> Self {
17+
Concrete { index: 0 }
18+
}
19+
}
20+
21+
impl Trait for Concrete {
22+
fn increment(&mut self) {
23+
self.index = self.index + 1;
24+
}
25+
fn get(&self) -> u32 {
26+
self.index
27+
}
28+
}
29+
30+
fn main() {
31+
let mut x: Box<dyn Trait> = Box::new(Concrete::new());
32+
x.increment();
33+
assert!(x.get() == 1);
34+
}

Diff for: rust-tests/cbmc-reg/FatPointers/slice1.rs

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
fn main() {
5+
let array = [1, 2, 3, 4, 5, 6];
6+
let slice: &[u32] = &array;
7+
assert!(slice[0] == 1);
8+
assert!(slice[5] == 6);
9+
}

Diff for: rust-tests/cbmc-reg/FatPointers/slice2.rs

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
fn main() {
5+
let array = [1, 2, 3, 4, 5, 6];
6+
let slice = &array[2..5];
7+
assert!(slice[0] == 3);
8+
assert!(slice[2] == 5);
9+
}

Diff for: rust-tests/cbmc-reg/FatPointers/slice3.rs

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
fn main() {
5+
let array = [1, 2, 3, 4, 5, 6];
6+
let slice1 = &array[2..5];
7+
let slice2 = &slice1[1..2];
8+
assert!(slice2[0] == 4);
9+
}

Diff for: rust-tests/cbmc-reg/FatPointers/structslice.rs

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
struct Concrete {
5+
array: [u32; 4],
6+
}
7+
8+
struct Abstract<'a> {
9+
uints: &'a [u32],
10+
}
11+
12+
fn main() {
13+
let x = Concrete { array: [1, 2, 3, 4] };
14+
assert!(x.array[0] == 1);
15+
let y = Abstract { uints: &[10, 11, 12, 13] };
16+
assert!(y.uints[0] == 10);
17+
assert!(y.uints[3] == 13);
18+
}

Diff for: rust-tests/cbmc-reg/FatPointers/trait1.rs

+31
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
// Cast a concrete ref to a trait ref.
5+
6+
pub trait Subscriber {
7+
fn process(&self) -> u32;
8+
}
9+
10+
struct DummySubscriber {
11+
val: u32,
12+
}
13+
14+
impl DummySubscriber {
15+
fn new() -> Self {
16+
DummySubscriber { val: 0 }
17+
}
18+
}
19+
20+
impl Subscriber for DummySubscriber {
21+
fn process(&self) -> u32 {
22+
let DummySubscriber { val: v } = self;
23+
*v + 1
24+
}
25+
}
26+
27+
fn main() {
28+
let _d = DummySubscriber::new();
29+
let _s = &_d as &dyn Subscriber;
30+
assert!(_s.process() == 1);
31+
}

Diff for: rust-tests/cbmc-reg/FatPointers/trait2.rs

+31
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
// Cast a concrete ref to a trait raw pointer.
5+
6+
pub trait Subscriber {
7+
fn process(&self) -> u32;
8+
}
9+
10+
struct DummySubscriber {
11+
val: u32,
12+
}
13+
14+
impl DummySubscriber {
15+
fn new() -> Self {
16+
DummySubscriber { val: 0 }
17+
}
18+
}
19+
20+
impl Subscriber for DummySubscriber {
21+
fn process(&self) -> u32 {
22+
let DummySubscriber { val: v } = self;
23+
*v + 1
24+
}
25+
}
26+
27+
fn main() {
28+
let _d = DummySubscriber::new();
29+
let _s = &_d as *const dyn Subscriber;
30+
assert!(unsafe { _s.as_ref().unwrap().process() } == 1);
31+
}

Diff for: rust-tests/cbmc-reg/FatPointers/trait3.rs

+45
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
// Cast a concrete ref to
5+
// concrete raw pointer
6+
// trait ref
7+
// trait raw pointer
8+
// Cast a trait ref to a trait raw pointer
9+
10+
pub trait Subscriber {
11+
fn process(&self) -> u32;
12+
}
13+
14+
struct DummySubscriber {
15+
val: u32,
16+
}
17+
18+
impl DummySubscriber {
19+
fn new() -> Self {
20+
DummySubscriber { val: 0 }
21+
}
22+
}
23+
24+
impl Subscriber for DummySubscriber {
25+
fn process(&self) -> u32 {
26+
let DummySubscriber { val: v } = self;
27+
*v + 1
28+
}
29+
}
30+
31+
fn main() {
32+
let d = DummySubscriber::new();
33+
34+
let d1 = &d as *const DummySubscriber;
35+
assert!(unsafe { d1.as_ref().unwrap().process() } == 1);
36+
37+
let s = &d as &dyn Subscriber;
38+
assert!(s.process() == 1);
39+
40+
let s1 = &d as *const dyn Subscriber;
41+
assert!(unsafe { s1.as_ref().unwrap().process() } == 1);
42+
43+
let x = s as *const dyn Subscriber;
44+
assert!(unsafe { x.as_ref().unwrap().process() } == 1);
45+
}

Diff for: rust-tests/cbmc-reg/Transparent/transparent1.rs

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
fn main() {
5+
let mut x: u32 = 4;
6+
let pointer0: std::ptr::NonNull<u32> = std::ptr::NonNull::new(&mut x).unwrap();
7+
let y = unsafe { *pointer0.as_ptr() };
8+
assert!(y == 4);
9+
}

Diff for: rust-tests/cbmc-reg/Transparent/transparent2.rs

+36
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
#[derive(Clone, Copy)]
5+
struct Target {
6+
x: u32,
7+
y: u32,
8+
}
9+
10+
struct Container<T> {
11+
ptr: std::ptr::NonNull<T>,
12+
}
13+
14+
impl<T> Container<T>
15+
where
16+
T: Copy,
17+
{
18+
fn new(val: &mut T) -> Self {
19+
return Container { ptr: std::ptr::NonNull::new(val).unwrap() };
20+
}
21+
fn get(&self) -> T {
22+
return unsafe { *self.ptr.as_ptr() };
23+
}
24+
}
25+
26+
fn main() {
27+
let mut x: u32 = 4;
28+
let container = Container::new(&mut x);
29+
let _y = container.get();
30+
assert_eq!(_y, 4);
31+
32+
let mut target: Target = Target { x: 3, y: 4 };
33+
let cont = Container::new(&mut target);
34+
assert!((unsafe { *cont.ptr.as_ptr() }).x == 3);
35+
assert!((unsafe { *cont.ptr.as_ptr() }).y == 4);
36+
}

Diff for: rust-tests/cbmc-reg/Transparent/transparent3.rs

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
//#repr(transparent)]
5+
pub struct Pointer<T> {
6+
pointer: *const T,
7+
}
8+
9+
pub struct Container<T> {
10+
container: Pointer<T>,
11+
}
12+
13+
fn main() {
14+
let x: u32 = 4;
15+
let my_pointer = Pointer { pointer: &x };
16+
let my_container = Container { container: my_pointer };
17+
18+
let y: u32 = unsafe { *my_container.container.pointer };
19+
assert!(y == 4);
20+
}

Diff for: rust-tests/cbmc-reg/Transparent/transparent4.rs

+27
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
4+
#[repr(transparent)]
5+
pub struct Pointer<T> {
6+
pointer: *const T,
7+
}
8+
9+
#[repr(transparent)]
10+
pub struct Wrapper<T>(T);
11+
12+
pub struct Container<T> {
13+
container: Pointer<T>,
14+
}
15+
16+
fn main() {
17+
let x: u32 = 4;
18+
let my_container = Container { container: Pointer { pointer: &x } };
19+
20+
let y: u32 = unsafe { *my_container.container.pointer };
21+
assert!(y == 4);
22+
23+
let w: Wrapper<u32> = Wrapper(4);
24+
25+
let Wrapper(c) = w;
26+
assert!(c == 4);
27+
}

0 commit comments

Comments
 (0)