-
Notifications
You must be signed in to change notification settings - Fork 353
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Rollup merge of #133211 - Strophox:miri-correct-state-update-ffi, r=R…
…alfJung Extend Miri to correctly pass mutable pointers through FFI Based off of rust-lang/rust#129684, this PR further extends Miri to execute native calls that make use of pointers to *mutable* memory. We adapt Miri's bookkeeping of internal state upon any FFI call that gives external code permission to mutate memory. Native code may now possibly write and therefore initialize and change the pointer provenance of bytes it has access to: Such memory is assumed to be *initialized* afterwards and bytes are given *arbitrary (wildcard) provenance*. This enables programs that correctly use mutating FFI calls to run Miri without errors, at the cost of possibly missing Undefined Behaviour caused by incorrect usage of mutating FFI. > <details> > > <summary> Simple example </summary> > > ```rust > extern "C" { > fn init_int(ptr: *mut i32); > } > > fn main() { > let mut x = std::mem::MaybeUninit::<i32>::uninit(); > let x = unsafe { > init_int(x.as_mut_ptr()); > x.assume_init() > }; > > println!("C initialized my memory to: {x}"); > } > ``` > ```c > void init_int(int *ptr) { > *ptr = 42; > } > ``` > should now show `C initialized my memory to: 42`. > > </details> r? ``@RalfJung``
- Loading branch information
Showing
11 changed files
with
366 additions
and
47 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.