diff options
| -rw-r--r-- | src/tools/miri/README.md | 23 | ||||
| -rw-r--r-- | src/tools/miri/src/diagnostics.rs | 26 | ||||
| -rw-r--r-- | src/tools/miri/src/shims/native_lib.rs | 13 | ||||
| -rw-r--r-- | src/tools/miri/tests/native-lib/pass/ptr_read_access.stderr | 18 | ||||
| -rw-r--r-- | src/tools/miri/tests/native-lib/pass/ptr_write_access.stderr | 18 |
5 files changed, 88 insertions, 10 deletions
diff --git a/src/tools/miri/README.md b/src/tools/miri/README.md index 4e30dea18ff..8f577295d17 100644 --- a/src/tools/miri/README.md +++ b/src/tools/miri/README.md @@ -375,16 +375,19 @@ to Miri failing to detect cases of undefined behavior in a program. * `-Zmiri-disable-weak-memory-emulation` disables the emulation of some C++11 weak memory effects. * `-Zmiri-native-lib=<path to a shared object file>` is an experimental flag for providing support - for calling native functions from inside the interpreter via FFI. Functions not provided by that - file are still executed via the usual Miri shims. - **WARNING**: If an invalid/incorrect `.so` file is specified, this can cause Undefined Behavior in Miri itself! - And of course, Miri cannot do any checks on the actions taken by the native code. - Note that Miri has its own handling of file descriptors, so if you want to replace *some* functions - working on file descriptors, you will have to replace *all* of them, or the two kinds of - file descriptors will be mixed up. - This is **work in progress**; currently, only integer arguments and return values are - supported (and no, pointer/integer casts to work around this limitation will not work; - they will fail horribly). It also only works on Unix hosts for now. + for calling native functions from inside the interpreter via FFI. The flag is supported only on + Unix systems. Functions not provided by that file are still executed via the usual Miri shims. + **WARNING**: If an invalid/incorrect `.so` file is specified, this can cause Undefined Behavior in + Miri itself! And of course, Miri cannot do any checks on the actions taken by the native code. + Note that Miri has its own handling of file descriptors, so if you want to replace *some* + functions working on file descriptors, you will have to replace *all* of them, or the two kinds of + file descriptors will be mixed up. This is **work in progress**; currently, only integer and + pointers arguments and return values are supported and memory allocated by the native code cannot + be accessed from Rust (only the other way around). Native code must not spawn threads that keep + running in the background after the call has returned to Rust and that access Rust-allocated + memory. Finally, the flag is **unsound** in the sense that Miri stops tracking details such as + initialization and provenance on memory shared with native code, so it is easily possible to write + code that has UB which is missed by Miri. * `-Zmiri-measureme=<name>` enables `measureme` profiling for the interpreted program. This can be used to find which parts of your program are executing slowly under Miri. The profile is written out to a file inside a directory called `<name>`, and can be processed diff --git a/src/tools/miri/src/diagnostics.rs b/src/tools/miri/src/diagnostics.rs index 41b7be37c37..6b5646d5473 100644 --- a/src/tools/miri/src/diagnostics.rs +++ b/src/tools/miri/src/diagnostics.rs @@ -126,6 +126,7 @@ pub enum NonHaltingDiagnostic { Int2Ptr { details: bool, }, + NativeCallSharedMem, WeakMemoryOutdatedLoad { ptr: Pointer, }, @@ -602,6 +603,8 @@ impl<'tcx> MiriMachine<'tcx> { RejectedIsolatedOp(_) => ("operation rejected by isolation".to_string(), DiagLevel::Warning), Int2Ptr { .. } => ("integer-to-pointer cast".to_string(), DiagLevel::Warning), + NativeCallSharedMem => + ("sharing memory with a native function".to_string(), DiagLevel::Warning), ExternTypeReborrow => ("reborrow of reference to `extern type`".to_string(), DiagLevel::Warning), CreatedPointerTag(..) @@ -637,6 +640,7 @@ impl<'tcx> MiriMachine<'tcx> { ProgressReport { .. } => format!("progress report: current operation being executed is here"), Int2Ptr { .. } => format!("integer-to-pointer cast"), + NativeCallSharedMem => format!("sharing memory with a native function called via FFI"), WeakMemoryOutdatedLoad { ptr } => format!("weak memory emulation: outdated value returned from load at {ptr}"), ExternTypeReborrow => @@ -679,7 +683,29 @@ impl<'tcx> MiriMachine<'tcx> { } v } + NativeCallSharedMem => { + vec![ + note!( + "when memory is shared with a native function call, Miri stops tracking initialization and provenance for that memory" + ), + note!( + "in particular, Miri assumes that the native call initializes all memory it has access to" + ), + note!( + "Miri also assumes that any part of this memory may be a pointer that is permitted to point to arbitrary exposed memory" + ), + note!( + "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" + ), + ] + } ExternTypeReborrow => { + assert!(self.borrow_tracker.as_ref().is_some_and(|b| { + matches!( + b.borrow().borrow_tracker_method(), + BorrowTrackerMethod::StackedBorrows + ) + })); vec