add warning explaining the limitations of the native code mode

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

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![
                     note!(
                         "`extern type` are not compatible with the Stacked Borrows aliasing model implemented by Miri; Miri may miss bugs in this code"

src/shims/native_lib.rs

@@ -1,4 +1,5 @@
 //! Implements calling functions from a native library.
+use std::cell::RefCell;
 use std::ops::Deref;
 
 use libffi::high::call as ffi;
@@ -172,6 +173,18 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
                     // Wildcard pointer, whatever it points to must be already exposed.
                     continue;
                 };
+                // The first time this happens at a particular location, print a warning.
+                thread_local! {
+                    static HAVE_WARNED: RefCell<bool> = const { RefCell::new(false) };
+                }
+                HAVE_WARNED.with_borrow_mut(|have_warned| {
+                    if !*have_warned {
+                        // Newly inserted, so first time we see this span.
+                        this.emit_diagnostic(NonHaltingDiagnostic::NativeCallSharedMem);
+                        *have_warned = true;
+                    }
+                });
+
                 this.prepare_for_native_call(alloc_id, prov)?;
             }
         }

tests/native-lib/pass/ptr_read_access.stderr

@@ -0,0 +1,18 @@
+warning: sharing memory with a native function
+  --> tests/native-lib/pass/ptr_read_access.rs:LL:CC
+   |
+LL |     unsafe { print_pointer(&x) };
+   |              ^^^^^^^^^^^^^^^^^ sharing memory with a native function called via FFI
+   |
+   = 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 `test_access_pointer` at tests/native-lib/pass/ptr_read_access.rs:LL:CC
+note: inside `main`
+  --> tests/native-lib/pass/ptr_read_access.rs:LL:CC
+   |
+LL |     test_access_pointer();
+   |     ^^^^^^^^^^^^^^^^^^^^^
+

tests/native-lib/pass/ptr_write_access.stderr

@@ -0,0 +1,18 @@
+warning: sharing memory with a native function
+  --> tests/native-lib/pass/ptr_write_access.rs:LL:CC
+   |
+LL |     unsafe { increment_int(&mut x) };
+   |              ^^^^^^^^^^^^^^^^^^^^^ sharing memory with a native function called via FFI
+   |
+   = 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 `test_increment_int` at tests/native-lib/pass/ptr_write_access.rs:LL:CC
+note: inside `main`
+  --> tests/native-lib/pass/ptr_write_access.rs:LL:CC
+   |
+LL |     test_increment_int();
+   |     ^^^^^^^^^^^^^^^^^^^^
+