diff --git a/Cargo.toml b/Cargo.toml index 99111092d3..924dfed2bc 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -39,7 +39,7 @@ features = ['unprefixed_malloc_on_supported_platforms'] [target.'cfg(unix)'.dependencies] libc = "0.2" # native-lib dependencies -libffi = { version = "4.0.0", optional = true } +libffi = { version = "4.1.1", optional = true } libloading = { version = "0.8", optional = true } serde = { version = "1.0.219", features = ["derive"], optional = true } diff --git a/src/shims/native_lib/ffi.rs b/src/shims/native_lib/ffi.rs new file mode 100644 index 0000000000..0badf22bb7 --- /dev/null +++ b/src/shims/native_lib/ffi.rs @@ -0,0 +1,46 @@ +//! Support code for dealing with libffi. + +use libffi::low::CodePtr; +use libffi::middle::{Arg as ArgPtr, Cif, Type as FfiType}; + +/// Perform the actual FFI call. +/// +/// # Safety +/// +/// The safety invariants of the foreign function being called must be upheld (if any). +pub unsafe fn call(fun: CodePtr, args: &mut [OwnedArg]) -> R { + let arg_ptrs: Vec<_> = args.iter().map(|arg| arg.ptr()).collect(); + let cif = Cif::new(args.iter_mut().map(|arg| arg.ty.take().unwrap()), R::reify().into_middle()); + // SAFETY: Caller upholds that the function is safe to call, and since we + // were passed a slice reference we know the `OwnedArg`s won't have been + // dropped by this point. + unsafe { cif.call(fun, &arg_ptrs) } +} + +/// An argument for an FFI call. +#[derive(Debug, Clone)] +pub struct OwnedArg { + /// The type descriptor for this argument. + ty: Option, + /// Corresponding bytes for the value. + bytes: Box<[u8]>, +} + +impl OwnedArg { + /// Instantiates an argument from a type descriptor and bytes. + pub fn new(ty: FfiType, bytes: Box<[u8]>) -> Self { + Self { ty: Some(ty), bytes } + } + + /// Creates a libffi argument pointer pointing to this argument's bytes. + /// NB: Since `libffi::middle::Arg` ignores the lifetime of the reference + /// it's derived from, it is up to the caller to ensure the `OwnedArg` is + /// not dropped before unsafely calling `libffi::middle::Cif::call()`! + fn ptr(&self) -> ArgPtr { + // FIXME: Using `&self.bytes[0]` to reference the whole array is + // definitely unsound under SB, but we're waiting on + // https://github.com/libffi-rs/libffi-rs/commit/112a37b3b6ffb35bd75241fbcc580de40ba74a73 + // to land in a release so that we don't need to do this. + ArgPtr::new(&self.bytes[0]) + } +} diff --git a/src/shims/native_lib/mod.rs b/src/shims/native_lib/mod.rs index 74b9b704fe..da8f785e37 100644 --- a/src/shims/native_lib/mod.rs +++ b/src/shims/native_lib/mod.rs @@ -2,14 +2,15 @@ use std::ops::Deref; -use libffi::high::call as ffi; use libffi::low::CodePtr; -use rustc_abi::{BackendRepr, HasDataLayout, Size}; -use rustc_middle::mir::interpret::Pointer; -use rustc_middle::ty::{self as ty, IntTy, UintTy}; +use libffi::middle::Type as FfiType; +use rustc_abi::{HasDataLayout, Size}; +use rustc_middle::ty::{self as ty, IntTy, Ty, UintTy}; use rustc_span::Symbol; use serde::{Deserialize, Serialize}; +mod ffi; + #[cfg_attr( not(all( target_os = "linux", @@ -20,6 +21,7 @@ use serde::{Deserialize, Serialize}; )] pub mod trace; +use self::ffi::OwnedArg; use crate::*; /// The final results of an FFI trace, containing every relevant event detected @@ -70,12 +72,12 @@ impl AccessRange { impl<'tcx> EvalContextExtPriv<'tcx> for crate::MiriInterpCx<'tcx> {} trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> { /// Call native host function and return the output as an immediate. - fn call_native_with_args<'a>( + fn call_native_with_args( &mut self, link_name: Symbol, dest: &MPlaceTy<'tcx>, - ptr: CodePtr, - libffi_args: Vec>, + fun: CodePtr, + libffi_args: &mut [OwnedArg], ) -> InterpResult<'tcx, (crate::ImmTy<'tcx>, Option)> { let this = self.eval_context_mut(); #[cfg(target_os = "linux")] @@ -93,55 +95,55 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> { // Unsafe because of the call to native code. // Because this is calling a C function it is not necessarily sound, // but there is no way around this and we've checked as much as we can. - let x = unsafe { ffi::call::(ptr, libffi_args.as_slice()) }; + let x = unsafe { ffi::call::(fun, libffi_args) }; Scalar::from_i8(x) } ty::Int(IntTy::I16) => { - let x = unsafe { ffi::call::(ptr, libffi_args.as_slice()) }; + let x = unsafe { ffi::call::(fun, libffi_args) }; Scalar::from_i16(x) } ty::Int(IntTy::I32) => { - let x = unsafe { ffi::call::(ptr, libffi_args.as_slice()) }; + let x = unsafe { ffi::call::(fun, libffi_args) }; Scalar::from_i32(x) } ty::Int(IntTy::I64) => { - let x = unsafe { ffi::call::(ptr, libffi_args.as_slice()) }; + let x = unsafe { ffi::call::(fun, libffi_args) }; Scalar::from_i64(x) } ty::Int(IntTy::Isize) => { - let x = unsafe { ffi::call::(ptr, libffi_args.as_slice()) }; + let x = unsafe { ffi::call::(fun, libffi_args) }; Scalar::from_target_isize(x.try_into().unwrap(), this) } // uints ty::Uint(UintTy::U8) => { - let x = unsafe { ffi::call::(ptr, libffi_args.as_slice()) }; + let x = unsafe { ffi::call::(fun, libffi_args) }; Scalar::from_u8(x) } ty::Uint(UintTy::U16) => { - let x = unsafe { ffi::call::(ptr, libffi_args.as_slice()) }; + let x = unsafe { ffi::call::(fun, libffi_args) }; Scalar::from_u16(x) } ty::Uint(UintTy::U32) => { - let x = unsafe { ffi::call::(ptr, libffi_args.as_slice()) }; + let x = unsafe { ffi::call::(fun, libffi_args) }; Scalar::from_u32(x) } ty::Uint(UintTy::U64) => { - let x = unsafe { ffi::call::(ptr, libffi_args.as_slice()) }; + let x = unsafe { ffi::call::(fun, libffi_args) }; Scalar::from_u64(x) } ty::Uint(UintTy::Usize) => { - let x = unsafe { ffi::call::(ptr, libffi_args.as_slice()) }; + let x = unsafe { ffi::call::(fun, libffi_args) }; Scalar::from_target_usize(x.try_into().unwrap(), this) } // Functions with no declared return type (i.e., the default return) // have the output_type `Tuple([])`. ty::Tuple(t_list) if (*t_list).deref().is_empty() => { - unsafe { ffi::call::<()>(ptr, libffi_args.as_slice()) }; + unsafe { ffi::call::<()>(fun, libffi_args) }; return interp_ok(ImmTy::uninit(dest.layout)); } ty::RawPtr(..) => { - let x = unsafe { ffi::call::<*const ()>(ptr, libffi_args.as_slice()) }; - let ptr = Pointer::new(Provenance::Wildcard, Size::from_bytes(x.addr())); + let x = unsafe { ffi::call::<*const ()>(fun, libffi_args) }; + let ptr = StrictPointer::new(Provenance::Wildcard, Size::from_bytes(x.addr())); Scalar::from_pointer(ptr, this) } _ => @@ -267,6 +269,150 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> { interp_ok(()) } + + /// Extract the value from the result of reading an operand from the machine + /// and convert it to a `OwnedArg`. + fn op_to_ffi_arg(&self, v: &OpTy<'tcx>, tracing: bool) -> InterpResult<'tcx, OwnedArg> { + let this = self.eval_context_ref(); + + // This should go first so that we emit unsupported before doing a bunch + // of extra work for types that aren't supported yet. + let ty = this.ty_to_ffitype(v.layout.ty)?; + + // Helper to print a warning when a pointer is shared with the native code. + let expose = |prov: Provenance| -> InterpResult<'tcx> { + // The first time this happens, print a warning. + if !this.machine.native_call_mem_warned.replace(true) { + // Newly set, so first time we get here. + this.emit_diagnostic(NonHaltingDiagnostic::NativeCallSharedMem { tracing }); + } + + this.expose_provenance(prov)?; + interp_ok(()) + }; + + // Compute the byte-level representation of the argument. If there's a pointer in there, we + // expose it inside the AM. Later in `visit_reachable_allocs`, the "meta"-level provenance + // for accessing the pointee gets exposed; this is crucial to justify the C code effectively + // casting the integer in `byte` to a pointer and using that. + let bytes = match v.as_mplace_or_imm() { + either::Either::Left(mplace) => { + // Get the alloc id corresponding to this mplace, alongside + // a pointer that's offset to point to this particular + // mplace (not one at the base addr of the allocation). + let sz = mplace.layout.size.bytes_usize(); + if sz == 0 { + throw_unsup_format!("attempting to pass a ZST over FFI"); + } + let (id, ofs, _) = this.ptr_get_alloc_id(mplace.ptr(), sz.try_into().unwrap())?; + let ofs = ofs.bytes_usize(); + let range = ofs..ofs.strict_add(sz); + // Expose all provenances in the allocation within the byte range of the struct, if + // any. These pointers are being directly passed to native code by-value. + let alloc = this.get_alloc_raw(id)?; + for prov in alloc.provenance().get_range(this, range.clone().into()) { + expose(prov)?; + } + // Read the bytes that make up this argument. We cannot use the normal getter as + // those would fail if any part of the argument is uninitialized. Native code + // is kind of outside the interpreter, after all... + Box::from(alloc.inspect_with_uninit_and_ptr_outside_interpreter(range)) + } + either::Either::Right(imm) => { + let mut bytes: Box<[u8]> = vec![0; imm.layout.size.bytes_usize()].into(); + + // A little helper to write scalars to our byte array. + let mut write_scalar = |this: &MiriInterpCx<'tcx>, sc: Scalar, pos: usize| { + // If a scalar is a pointer, then expose its provenance. + if let interpret::Scalar::Ptr(p, _) = sc { + expose(p.provenance)?; + } + write_target_uint( + this.data_layout().endian, + &mut bytes[pos..][..sc.size().bytes_usize()], + sc.to_scalar_int()?.to_bits_unchecked(), + ) + .unwrap(); + interp_ok(()) + }; + + // Write the scalar into the `bytes` buffer. + match *imm { + Immediate::Scalar(sc) => write_scalar(this, sc, 0)?, + Immediate::ScalarPair(sc_first, sc_second) => { + // The first scalar has an offset of zero; compute the offset of the 2nd. + let ofs_second = { + let rustc_abi::BackendRepr::ScalarPair(a, b) = imm.layout.backend_repr + else { + span_bug!( + this.cur_span(), + "op_to_ffi_arg: invalid scalar pair layout: {:#?}", + imm.layout + ) + }; + a.size(this).align_to(b.align(this).abi).bytes_usize() + }; + + write_scalar(this, sc_first, 0)?; + write_scalar(this, sc_second, ofs_second)?; + } + Immediate::Uninit => { + // Nothing to write. + } + } + + bytes + } + }; + interp_ok(OwnedArg::new(ty, bytes)) + } + + /// Parses an ADT to construct the matching libffi type. + fn adt_to_ffitype( + &self, + orig_ty: Ty<'_>, + adt_def: ty::AdtDef<'tcx>, + args: &'tcx ty::List>, + ) -> InterpResult<'tcx, FfiType> { + // TODO: Certain non-C reprs should be okay also. + if !adt_def.repr().c() { + throw_unsup_format!("passing a non-#[repr(C)] struct over FFI: {orig_ty}") + } + // TODO: unions, etc. + if !adt_def.is_struct() { + throw_unsup_format!( + "unsupported argument type for native call: {orig_ty} is an enum or union" + ); + } + + let this = self.eval_context_ref(); + let mut fields = vec![]; + for field in &adt_def.non_enum_variant().fields { + fields.push(this.ty_to_ffitype(field.ty(*this.tcx, args))?); + } + + interp_ok(FfiType::structure(fields)) + } + + /// Gets the matching libffi type for a given Ty. + fn ty_to_ffitype(&self, ty: Ty<'tcx>) -> InterpResult<'tcx, FfiType> { + interp_ok(match ty.kind() { + ty::Int(IntTy::I8) => FfiType::i8(), + ty::Int(IntTy::I16) => FfiType::i16(), + ty::Int(IntTy::I32) => FfiType::i32(), + ty::Int(IntTy::I64) => FfiType::i64(), + ty::Int(IntTy::Isize) => FfiType::isize(), + // the uints + ty::Uint(UintTy::U8) => FfiType::u8(), + ty::Uint(UintTy::U16) => FfiType::u16(), + ty::Uint(UintTy::U32) => FfiType::u32(), + ty::Uint(UintTy::U64) => FfiType::u64(), + ty::Uint(UintTy::Usize) => FfiType::usize(), + ty::RawPtr(..) => FfiType::pointer(), + ty::Adt(adt_def, args) => self.adt_to_ffitype(ty, *adt_def, args)?, + _ => throw_unsup_format!("unsupported argument type for native call: {}", ty), + }) + } } impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {} @@ -295,36 +441,11 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { // Do we have ptrace? let tracing = trace::Supervisor::is_enabled(); - // Get the function arguments, and convert them to `libffi`-compatible form. - let mut libffi_args = Vec::::with_capacity(args.len()); + // Get the function arguments, copy them, and prepare the type descriptions. + let mut libffi_args = Vec::::with_capacity(args.len()); for arg in args.iter() { - if !matches!(arg.layout.backend_repr, BackendRepr::Scalar(_)) { - throw_unsup_format!("only scalar argument types are supported for native calls") - } - let imm = this.read_immediate(arg)?; - libffi_args.push(imm_to_carg(&imm, this)?); - // If we are passing a pointer, expose its provenance. Below, all exposed memory - // (previously exposed and new exposed) will then be properly prepared. - if matches!(arg.layout.ty.kind(), ty::RawPtr(..)) { - let ptr = imm.to_scalar().to_pointer(this)?; - let Some(prov) = ptr.provenance else { - // Pointer without provenance may not access any memory anyway, skip. - continue; - }; - // The first time this happens, print a warning. - if !this.machine.native_call_mem_warned.replace(true) { - // Newly set, so first time we get here. - this.emit_diagnostic(NonHaltingDiagnostic::NativeCallSharedMem { tracing }); - } - - this.expose_provenance(prov)?; - } + libffi_args.push(this.op_to_ffi_arg(arg, tracing)?); } - // Convert arguments to `libffi::high::Arg` type. - let libffi_args = libffi_args - .iter() - .map(|arg| arg.arg_downcast()) - .collect::>>(); // Prepare all exposed memory (both previously exposed, and just newly exposed since a // pointer was passed as argument). Uninitialised memory is left as-is, but any data @@ -343,8 +464,9 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { std::hint::black_box(alloc.get_bytes_unchecked_raw().expose_provenance()); if !tracing { - // Expose all provenances in this allocation, since the native code can do $whatever. - // Can be skipped when tracing; in that case we'll expose just the actually-read parts later. + // Expose all provenances in this allocation, since the native code can do + // $whatever. Can be skipped when tracing; in that case we'll expose just the + // actually-read parts later. for prov in alloc.provenance().provenances() { this.expose_provenance(prov)?; } @@ -354,7 +476,8 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { if info.mutbl.is_mut() { let (alloc, cx) = this.get_alloc_raw_mut(alloc_id)?; // These writes could initialize everything and wreck havoc with the pointers. - // We can skip that when tracing; in that case we'll later do that only for the memory that got actually written. + // We can skip that when tracing; in that case we'll later do that only for the + // memory that got actually written. if !tracing { alloc.process_native_write(&cx.tcx, None); } @@ -367,7 +490,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { // Call the function and store output, depending on return type in the function signature. let (ret, maybe_memevents) = - this.call_native_with_args(link_name, dest, code_ptr, libffi_args)?; + this.call_native_with_args(link_name, dest, code_ptr, &mut libffi_args)?; if tracing { this.tracing_apply_accesses(maybe_memevents.unwrap())?; @@ -377,83 +500,3 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { interp_ok(true) } } - -#[derive(Debug, Clone)] -/// Enum of supported arguments to external C functions. -// We introduce this enum instead of just calling `ffi::arg` and storing a list -// of `libffi::high::Arg` directly, because the `libffi::high::Arg` just wraps a reference -// to the value it represents: https://docs.rs/libffi/latest/libffi/high/call/struct.Arg.html -// and we need to store a copy of the value, and pass a reference to this copy to C instead. -enum CArg { - /// 8-bit signed integer. - Int8(i8), - /// 16-bit signed integer. - Int16(i16), - /// 32-bit signed integer. - Int32(i32), - /// 64-bit signed integer. - Int64(i64), - /// isize. - ISize(isize), - /// 8-bit unsigned integer. - UInt8(u8), - /// 16-bit unsigned integer. - UInt16(u16), - /// 32-bit unsigned integer. - UInt32(u32), - /// 64-bit unsigned integer. - UInt64(u64), - /// usize. - USize(usize), - /// Raw pointer, stored as C's `void*`. - RawPtr(*mut std::ffi::c_void), -} - -impl<'a> CArg { - /// Convert a `CArg` to a `libffi` argument type. - fn arg_downcast(&'a self) -> libffi::high::Arg<'a> { - match self { - CArg::Int8(i) => ffi::arg(i), - CArg::Int16(i) => ffi::arg(i), - CArg::Int32(i) => ffi::arg(i), - CArg::Int64(i) => ffi::arg(i), - CArg::ISize(i) => ffi::arg(i), - CArg::UInt8(i) => ffi::arg(i), - CArg::UInt16(i) => ffi::arg(i), - CArg::UInt32(i) => ffi::arg(i), - CArg::UInt64(i) => ffi::arg(i), - CArg::USize(i) => ffi::arg(i), - CArg::RawPtr(i) => ffi::arg(i), - } - } -} - -/// Extract the scalar value from the result of reading a scalar from the machine, -/// and convert it to a `CArg`. -fn imm_to_carg<'tcx>(v: &ImmTy<'tcx>, cx: &impl HasDataLayout) -> InterpResult<'tcx, CArg> { - interp_ok(match v.layout.ty.kind() { - // If the primitive provided can be converted to a type matching the type pattern - // then create a `CArg` of this primitive value with the corresponding `CArg` constructor. - // the ints - ty::Int(IntTy::I8) => CArg::Int8(v.to_scalar().to_i8()?), - ty::Int(IntTy::I16) => CArg::Int16(v.to_scalar().to_i16()?), - ty::Int(IntTy::I32) => CArg::Int32(v.to_scalar().to_i32()?), - ty::Int(IntTy::I64) => CArg::Int64(v.to_scalar().to_i64()?), - ty::Int(IntTy::Isize) => - CArg::ISize(v.to_scalar().to_target_isize(cx)?.try_into().unwrap()), - // the uints - ty::Uint(UintTy::U8) => CArg::UInt8(v.to_scalar().to_u8()?), - ty::Uint(UintTy::U16) => CArg::UInt16(v.to_scalar().to_u16()?), - ty::Uint(UintTy::U32) => CArg::UInt32(v.to_scalar().to_u32()?), - ty::Uint(UintTy::U64) => CArg::UInt64(v.to_scalar().to_u64()?), - ty::Uint(UintTy::Usize) => - CArg::USize(v.to_scalar().to_target_usize(cx)?.try_into().unwrap()), - ty::RawPtr(..) => { - let s = v.to_scalar().to_pointer(cx)?.addr(); - // This relies on the `expose_provenance` in the `visit_reachable_allocs` callback - // above. - CArg::RawPtr(std::ptr::with_exposed_provenance_mut(s.bytes_usize())) - } - _ => throw_unsup_format!("unsupported argument type for native call: {}", v.layout.ty), - }) -} diff --git a/tests/native-lib/aggregate_arguments.c b/tests/native-lib/aggregate_arguments.c new file mode 100644 index 0000000000..8ad687f2ae --- /dev/null +++ b/tests/native-lib/aggregate_arguments.c @@ -0,0 +1,52 @@ +#include + +// See comments in build_native_lib() +#define EXPORT __attribute__((visibility("default"))) + +/* Test: fail/pass_struct_expose_only_range */ + +typedef struct HasPointer { + uint8_t *ptr; +} HasPointer; + +EXPORT uint8_t access_struct_ptr(const HasPointer s) { + return *s.ptr; +} + +/* Test: test_pass_struct */ + +typedef struct PassMe { + int32_t value; + int64_t other_value; +} PassMe; + +EXPORT int64_t pass_struct(const PassMe pass_me) { + return pass_me.value + pass_me.other_value; +} + +/* Test: test_pass_struct_complex */ + +typedef struct Part1 { + uint16_t high; + uint16_t low; +} Part1; + +typedef struct Part2 { + uint32_t bits; +} Part2; + +typedef struct ComplexStruct { + Part1 part_1; + Part2 part_2; + uint32_t part_3; +} ComplexStruct; + +EXPORT int32_t pass_struct_complex(const ComplexStruct complex, uint16_t high, uint16_t low, uint32_t bits) { + if (complex.part_1.high == high && complex.part_1.low == low + && complex.part_2.bits == bits + && complex.part_3 == bits) + return 0; + else { + return 1; + } +} diff --git a/tests/native-lib/fail/pass_struct_expose_only_range.rs b/tests/native-lib/fail/pass_struct_expose_only_range.rs new file mode 100644 index 0000000000..a2b43031a2 --- /dev/null +++ b/tests/native-lib/fail/pass_struct_expose_only_range.rs @@ -0,0 +1,23 @@ +//@compile-flags: -Zmiri-permissive-provenance + +#[repr(C)] +#[derive(Copy, Clone)] +struct HasPointer { + ptr: *const u8, +} + +extern "C" { + fn access_struct_ptr(s: HasPointer) -> u8; +} + +fn main() { + let structs = vec![HasPointer { ptr: &0 }, HasPointer { ptr: &1 }]; + unsafe { + let r = access_struct_ptr(structs[1]); + assert_eq!(r, 1); + // There are two pointers stored in the allocation backing `structs`; ensure + // we only exposed the one that was actually passed to C. + let _val = *std::ptr::with_exposed_provenance::(structs[1].ptr.addr()); // fine, ptr got sent to C + let _val = *std::ptr::with_exposed_provenance::(structs[0].ptr.addr()); //~ ERROR: memory access failed + }; +} diff --git a/tests/native-lib/fail/pass_struct_expose_only_range.stderr b/tests/native-lib/fail/pass_struct_expose_only_range.stderr new file mode 100644 index 0000000000..a8f85001c2 --- /dev/null +++ b/tests/native-lib/fail/pass_struct_expose_only_range.stderr @@ -0,0 +1,28 @@ +warning: sharing memory with a native function called via FFI + --> tests/native-lib/fail/pass_struct_expose_only_range.rs:LL:CC + | +LL | let r = access_struct_ptr(structs[1]); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ sharing memory with a native function + | + = help: when memory is shared with a native function call, Miri stops tracking initialization and provenance for that memory + = help: in particular, Miri assumes that the native call initializes all memory it has access to + = help: Miri also assumes that any part of this memory may be a pointer that is permitted to point to arbitrary exposed memory + = help: what this means is that Miri will easily miss Undefined Behavior related to incorrect usage of this shared memory, so you should not take a clean Miri run as a signal that your FFI code is UB-free + = note: BACKTRACE: + = note: inside `main` at tests/native-lib/fail/pass_struct_expose_only_range.rs:LL:CC + +error: Undefined Behavior: memory access failed: attempting to access 1 byte, but got $HEX[noalloc] which is a dangling pointer (it has no provenance) + --> tests/native-lib/fail/pass_struct_expose_only_range.rs:LL:CC + | +LL | let _val = *std::ptr::with_exposed_provenance::(structs[0].ptr.addr()); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Undefined Behavior occurred here + | + = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior + = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information + = note: BACKTRACE: + = note: inside `main` at tests/native-lib/fail/pass_struct_expose_only_range.rs:LL:CC + +note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace + +error: aborting due to 1 previous error; 1 warning emitted + diff --git a/tests/native-lib/fail/struct_not_extern_c.rs b/tests/native-lib/fail/struct_not_extern_c.rs new file mode 100644 index 0000000000..cf8315e0fd --- /dev/null +++ b/tests/native-lib/fail/struct_not_extern_c.rs @@ -0,0 +1,19 @@ +// Only works on Unix targets +//@ignore-target: windows wasm +//@only-on-host + +#![allow(improper_ctypes)] + +pub struct PassMe { + pub value: i32, + pub other_value: i64, +} + +extern "C" { + fn pass_struct(s: PassMe) -> i64; +} + +fn main() { + let pass_me = PassMe { value: 42, other_value: 1337 }; + unsafe { pass_struct(pass_me) }; //~ ERROR: unsupported operation: passing a non-#[repr(C)] struct over FFI +} diff --git a/tests/native-lib/fail/struct_not_extern_c.stderr b/tests/native-lib/fail/struct_not_extern_c.stderr new file mode 100644 index 0000000000..90e59a31da --- /dev/null +++ b/tests/native-lib/fail/struct_not_extern_c.stderr @@ -0,0 +1,14 @@ +error: unsupported operation: passing a non-#[repr(C)] struct over FFI: PassMe + --> tests/native-lib/fail/struct_not_extern_c.rs:LL:CC + | +LL | unsafe { pass_struct(pass_me) }; + | ^^^^^^^^^^^^^^^^^^^^ unsupported operation occurred here + | + = help: this is likely not a bug in the program; it indicates that the program performed an operation that Miri does not support + = note: BACKTRACE: + = note: inside `main` at tests/native-lib/fail/struct_not_extern_c.rs:LL:CC + +note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace + +error: aborting due to 1 previous error + diff --git a/tests/native-lib/fail/uninit_struct.rs b/tests/native-lib/fail/uninit_struct.rs new file mode 100644 index 0000000000..cf61c7f391 --- /dev/null +++ b/tests/native-lib/fail/uninit_struct.rs @@ -0,0 +1,27 @@ +#[repr(C)] +#[derive(Copy, Clone)] +struct ComplexStruct { + part_1: Part1, + part_2: Part2, + part_3: u32, +} +#[repr(C)] +#[derive(Copy, Clone)] +struct Part1 { + high: u16, + low: u16, +} +#[repr(C)] +#[derive(Copy, Clone)] +struct Part2 { + bits: u32, +} + +extern "C" { + fn pass_struct_complex(s: ComplexStruct, high: u16, low: u16, bits: u32) -> i32; +} + +fn main() { + let arg = std::mem::MaybeUninit::::uninit(); + unsafe { pass_struct_complex(*arg.as_ptr(), 0, 0, 0) }; //~ ERROR: Undefined Behavior: constructing invalid value +} diff --git a/tests/native-lib/fail/uninit_struct.stderr b/tests/native-lib/fail/uninit_struct.stderr new file mode 100644 index 0000000000..0fe6ad9c77 --- /dev/null +++ b/tests/native-lib/fail/uninit_struct.stderr @@ -0,0 +1,15 @@ +error: Undefined Behavior: constructing invalid value at .part_1.high: encountered uninitialized memory, but expected an integer + --> tests/native-lib/fail/uninit_struct.rs:LL:CC + | +LL | unsafe { pass_struct_complex(*arg.as_ptr(), 0, 0, 0) }; + | ^^^^^^^^^^^^^ Undefined Behavior occurred here + | + = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior + = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information + = note: BACKTRACE: + = note: inside `main` at tests/native-lib/fail/uninit_struct.rs:LL:CC + +note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace + +error: aborting due to 1 previous error + diff --git a/tests/native-lib/pass/aggregate_arguments.rs b/tests/native-lib/pass/aggregate_arguments.rs new file mode 100644 index 0000000000..55acb24061 --- /dev/null +++ b/tests/native-lib/pass/aggregate_arguments.rs @@ -0,0 +1,52 @@ +fn main() { + test_pass_struct(); + test_pass_struct_complex(); +} + +/// Test passing a basic struct as an argument. +fn test_pass_struct() { + // Exactly two fields, so that we hit the ScalarPair case. + #[repr(C)] + struct PassMe { + value: i32, + other_value: i64, + } + + extern "C" { + fn pass_struct(s: PassMe) -> i64; + } + + let pass_me = PassMe { value: 42, other_value: 1337 }; + assert_eq!(unsafe { pass_struct(pass_me) }, 42 + 1337); +} + +/// Test passing a more complex struct as an argument. +fn test_pass_struct_complex() { + #[repr(C)] + struct ComplexStruct { + part_1: Part1, + part_2: Part2, + part_3: u32, + } + #[repr(C)] + struct Part1 { + high: u16, + low: u16, + } + #[repr(C)] + struct Part2 { + bits: u32, + } + + extern "C" { + fn pass_struct_complex(s: ComplexStruct, high: u16, low: u16, bits: u32) -> i32; + } + + let high = 0xabcd; + let low = 0xef01; + let bits = 0xabcdef01; + + let complex = + ComplexStruct { part_1: Part1 { high, low }, part_2: Part2 { bits }, part_3: bits }; + assert_eq!(unsafe { pass_struct_complex(complex, high, low, bits) }, 0); +} diff --git a/tests/native-lib/pass/ptr_read_access.rs b/tests/native-lib/pass/ptr_read_access.rs index 4f3c37f00c..bab73f7cf1 100644 --- a/tests/native-lib/pass/ptr_read_access.rs +++ b/tests/native-lib/pass/ptr_read_access.rs @@ -1,6 +1,7 @@ //@revisions: trace notrace //@[trace] only-target: x86_64-unknown-linux-gnu i686-unknown-linux-gnu //@[trace] compile-flags: -Zmiri-native-lib-enable-tracing +//@compile-flags: -Zmiri-permissive-provenance fn main() { test_access_pointer(); diff --git a/tests/ui.rs b/tests/ui.rs index f021d5194c..b7286d9a36 100644 --- a/tests/ui.rs +++ b/tests/ui.rs @@ -60,6 +60,7 @@ fn build_native_lib(target: &str) -> PathBuf { native_lib_path.to_str().unwrap(), // FIXME: Automate gathering of all relevant C source files in the directory. "tests/native-lib/scalar_arguments.c", + "tests/native-lib/aggregate_arguments.c", "tests/native-lib/ptr_read_access.c", "tests/native-lib/ptr_write_access.c", // Ensure we notice serious problems in the C code.