Merge pull request #4098 from RalfJung/native-call-warning
add warning explaining the limitations of the native code mode
This commit is contained in:
commit
0aec399b83
5 changed files with 88 additions and 10 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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)?;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
18
src/tools/miri/tests/native-lib/pass/ptr_read_access.stderr
Normal file
18
src/tools/miri/tests/native-lib/pass/ptr_read_access.stderr
Normal file
|
|
@ -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();
|
||||
| ^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
18
src/tools/miri/tests/native-lib/pass/ptr_write_access.stderr
Normal file
18
src/tools/miri/tests/native-lib/pass/ptr_write_access.stderr
Normal file
|
|
@ -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();
|
||||
| ^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
Loading…
Add table
Add a link
Reference in a new issue