Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions src/test/cbmc/DynTrait/dyn_fn_param.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,7 @@
// Check that we can pass a dyn function pointer to a stand alone
// function definition

#![feature(raw)]
#![allow(deprecated)]
#![feature(ptr_metadata)]

include!("../Helpers/vtable_utils_ignore.rs");

Expand Down
3 changes: 1 addition & 2 deletions src/test/cbmc/DynTrait/dyn_fn_param_closure.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,7 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT

// Check that we can pass a dyn function pointer to a simple closure
#![feature(raw)]
#![allow(deprecated)]
#![feature(ptr_metadata)]

include!("../Helpers/vtable_utils_ignore.rs");

Expand Down
3 changes: 1 addition & 2 deletions src/test/cbmc/DynTrait/dyn_fn_param_closure_capture.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,7 @@

// Check that we can pass a dyn function pointer to a closure that captures
// some data
#![feature(raw)]
#![allow(deprecated)]
#![feature(ptr_metadata)]

include!("../Helpers/vtable_utils_ignore.rs");

Expand Down
3 changes: 1 addition & 2 deletions src/test/cbmc/DynTrait/dyn_fn_param_closure_capture_fail.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,7 @@

// Check that we can pass a dyn function pointer to a closure that captures
// some data
#![feature(raw)]
#![allow(deprecated)]
#![feature(ptr_metadata)]

include!("../Helpers/vtable_utils_ignore.rs");
include!("../../rmc-prelude.rs");
Expand Down
3 changes: 1 addition & 2 deletions src/test/cbmc/DynTrait/dyn_fn_param_closure_fail.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,7 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT

// Check that we can pass a dyn function pointer to a simple closure
#![feature(raw)]
#![allow(deprecated)]
#![feature(ptr_metadata)]

include!("../Helpers/vtable_utils_ignore.rs");
include!("../../rmc-prelude.rs");
Expand Down
4 changes: 1 addition & 3 deletions src/test/cbmc/DynTrait/dyn_fn_param_fail_fixme.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,7 @@
// function definition. Inverted negative test.

// FIXME https://github.com/model-checking/rmc/issues/240

#![feature(raw)]
#![allow(deprecated)]
#![feature(ptr_metadata)]

include!("../Helpers/vtable_utils_ignore.rs");
include!("../../rmc-prelude.rs");
Expand Down
11 changes: 6 additions & 5 deletions src/test/cbmc/DynTrait/nested_boxes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,11 @@
// outter 2 dynamic trait objects have fat pointers as their backing data.

#![feature(core_intrinsics)]
#![feature(raw)]
#![allow(deprecated)]
#![feature(ptr_metadata)]

use std::any::Any;
use std::intrinsics::size_of;
use std::ptr::DynMetadata;

include!("../Helpers/vtable_utils_ignore.rs");

Expand All @@ -27,15 +28,15 @@ fn main() {
// Outermost trait object
// The size is 16, because the data is another fat pointer
let dyn_3 = &*dyn_trait3 as &dyn Send;
let vtable3: *mut usize = vtable!(dyn_3);
let vtable3: DynMetadata<dyn Any> = vtable!(dyn_3);
assert!(size_from_vtable(vtable3) == 16);
assert!(align_from_vtable(vtable3) == 8);

// Inspect the data pointer from dyn_trait3
let data_ptr3 = data!(dyn_3) as *mut usize;

// The second half of this fat pointer is another vtable, for dyn_trait2
let vtable2 = *(data_ptr3.offset(1) as *mut *mut usize);
let vtable2 = *(data_ptr3.offset(1) as *mut DynMetadata<dyn Any>);

// The size is 16, because the data is another fat pointer
assert!(size_from_vtable(vtable2) == 16);
Expand All @@ -45,7 +46,7 @@ fn main() {
let data_ptr2 = *(data_ptr3 as *mut *mut usize);

// The second half of this fat pointer is another vtable, for dyn_trait1
let vtable1 = *(data_ptr2.offset(1) as *mut *mut usize);
let vtable1 = *(data_ptr2.offset(1) as *mut DynMetadata<dyn Any>);

// The size is 8, because the data is the Foo itself
assert!(size_from_vtable(vtable1) == size_of::<Foo>());
Expand Down
3 changes: 1 addition & 2 deletions src/test/cbmc/DynTrait/nested_boxes_fail.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,7 @@
// In this failing tests, assertions are inverted to use !=.

#![feature(core_intrinsics)]
#![feature(raw)]
#![allow(deprecated)]
#![feature(ptr_metadata)]

use std::intrinsics::size_of;

Expand Down
7 changes: 3 additions & 4 deletions src/test/cbmc/DynTrait/vtable_size_align_drop.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,11 @@

// This test checks the `size` and `align` fields of vtables, for a
// dynamic trait where two implementing structs have different sizes.
// The strategy is to cast the dyn trait object to a raw::TraitObject
// then do some unsafe pointer math.
// The strategy is to use the new pointer metadata API:
// https://github.com/rust-lang/rust/issues/81513

#![feature(core_intrinsics)]
#![feature(raw)]
#![allow(deprecated)]
#![feature(ptr_metadata)]

use std::intrinsics::size_of;
use std::ptr::drop_in_place;
Expand Down
7 changes: 3 additions & 4 deletions src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,14 +3,13 @@

// This test checks the `size` and `align` fields of vtables, for a
// dynamic trait where two implementing structs have different sizes.
// The strategy is to cast the dyn trait object to a raw::TraitObject
// then do some unsafe pointer math.
// The strategy is to use the new pointer metadata API:
// https://github.com/rust-lang/rust/issues/81513

// In this _fail version, all asserts should fail.

#![feature(core_intrinsics)]
#![feature(raw)]
#![allow(deprecated)]
#![feature(ptr_metadata)]

use std::intrinsics::size_of;
use std::ptr::drop_in_place;
Expand Down
7 changes: 4 additions & 3 deletions src/test/cbmc/FatPointers/boxmuttrait.rs
Original file line number Diff line number Diff line change
@@ -1,10 +1,11 @@
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT
#![feature(core_intrinsics)]
#![feature(raw)]
#![allow(deprecated)]
#![feature(ptr_metadata)]

use std::io::{sink, Write};
use std::ptr::DynMetadata;
use std::any::Any;

include!("../Helpers/vtable_utils_ignore.rs");

Expand All @@ -31,7 +32,7 @@ fn main() {
let dest_data_ptr = data!(dest_ptr) as *mut usize;

// // The second half of this fat pointer is another vtable, for log
let second_vtable_ptr = dest_data_ptr.offset(1) as *mut *mut usize;
let second_vtable_ptr = dest_data_ptr.offset(1) as *mut DynMetadata<dyn Any>;
let second_vtable = *second_vtable_ptr;

// The sink itself has no size, weirdly enough
Expand Down
28 changes: 16 additions & 12 deletions src/test/cbmc/Helpers/vtable_utils_ignore.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,35 +5,39 @@
// an import! to share this code across test directories.

// Macro rules because we can't cast between incompatible dyn trait fat pointer types
macro_rules! vtable {
macro_rules! data {
($f:ident) => {{
unsafe {
let trait_object: std::raw::TraitObject = std::mem::transmute($f);
trait_object.vtable as *mut usize
let ptr: *mut dyn std::any::Any = std::mem::transmute($f);
let data: *mut () = ptr.cast();
data
}
}};
}

macro_rules! data {
macro_rules! vtable {
($f:ident) => {{
unsafe {
let trait_object: std::raw::TraitObject = std::mem::transmute($f);
trait_object.data as *mut ()
let ptr: *mut dyn std::any::Any = std::mem::transmute($f);
std::ptr::metadata(ptr)
}
}};
}

fn drop_from_vtable(vtable_ptr: *mut usize) -> *mut () {
fn drop_from_vtable(vtable_ptr: std::ptr::DynMetadata<dyn std::any::Any>) -> *mut () {
// 1st pointer-sized position
unsafe { *vtable_ptr as *mut () }
unsafe {
let ptr: *mut usize = std::mem::transmute(vtable_ptr);
*ptr as *mut ()
}
}

fn size_from_vtable(vtable_ptr: *mut usize) -> usize {
fn size_from_vtable(vtable_ptr: std::ptr::DynMetadata<dyn std::any::Any>) -> usize {
// 2nd usize-sized position
unsafe { *(vtable_ptr.offset(1)) }
vtable_ptr.size_of()
}

fn align_from_vtable(vtable_ptr: *mut usize) -> usize {
fn align_from_vtable(vtable_ptr: std::ptr::DynMetadata<dyn std::any::Any>) -> usize {
// 3rd usize-sized position
unsafe { *(vtable_ptr.offset(2)) }
vtable_ptr.align_of()
}