This repository was archived by the owner on May 28, 2025. It is now read-only.
Commit e3b8092
authored
Unrolled build for rust-lang#133211
Rollup merge of rust-lang#133211 - Strophox:miri-correct-state-update-ffi, r=RalfJung
Extend Miri to correctly pass mutable pointers through FFI
Based off of rust-lang#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``File tree
19 files changed
+476
-59
lines changed- compiler
- rustc_const_eval/src
- const_eval
- interpret
- rustc_middle/src/mir/interpret
- allocation
- src/tools/miri
- src
- alloc_addresses
- borrow_tracker
- stacked_borrows
- tree_borrows
- shims
- tests
- native-lib
- pass
19 files changed
+476
-59
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
168 | 168 | | |
169 | 169 | | |
170 | 170 | | |
171 | | - | |
172 | | - | |
173 | | - | |
| 171 | + | |
| 172 | + | |
| 173 | + | |
174 | 174 | | |
175 | 175 | | |
176 | 176 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
21 | 21 | | |
22 | 22 | | |
23 | 23 | | |
24 | | - | |
25 | | - | |
26 | | - | |
| 24 | + | |
| 25 | + | |
27 | 26 | | |
28 | 27 | | |
29 | 28 | | |
| |||
586 | 585 | | |
587 | 586 | | |
588 | 587 | | |
589 | | - | |
| 588 | + | |
| 589 | + | |
| 590 | + | |
| 591 | + | |
590 | 592 | | |
591 | 593 | | |
592 | 594 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
238 | 238 | | |
239 | 239 | | |
240 | 240 | | |
241 | | - | |
| 241 | + | |
242 | 242 | | |
243 | 243 | | |
244 | 244 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
327 | 327 | | |
328 | 328 | | |
329 | 329 | | |
330 | | - | |
| 330 | + | |
331 | 331 | | |
332 | | - | |
333 | | - | |
334 | | - | |
| 332 | + | |
| 333 | + | |
| 334 | + | |
335 | 335 | | |
336 | 336 | | |
337 | 337 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
944 | 944 | | |
945 | 945 | | |
946 | 946 | | |
| 947 | + | |
| 948 | + | |
| 949 | + | |
| 950 | + | |
| 951 | + | |
| 952 | + | |
| 953 | + | |
| 954 | + | |
| 955 | + | |
| 956 | + | |
| 957 | + | |
| 958 | + | |
| 959 | + | |
| 960 | + | |
| 961 | + | |
| 962 | + | |
| 963 | + | |
| 964 | + | |
| 965 | + | |
| 966 | + | |
| 967 | + | |
| 968 | + | |
| 969 | + | |
| 970 | + | |
| 971 | + | |
| 972 | + | |
| 973 | + | |
| 974 | + | |
| 975 | + | |
| 976 | + | |
| 977 | + | |
| 978 | + | |
| 979 | + | |
| 980 | + | |
| 981 | + | |
| 982 | + | |
| 983 | + | |
| 984 | + | |
| 985 | + | |
| 986 | + | |
| 987 | + | |
| 988 | + | |
| 989 | + | |
| 990 | + | |
| 991 | + | |
| 992 | + | |
947 | 993 | | |
948 | 994 | | |
949 | 995 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
643 | 643 | | |
644 | 644 | | |
645 | 645 | | |
| 646 | + | |
| 647 | + | |
| 648 | + | |
| 649 | + | |
| 650 | + | |
| 651 | + | |
| 652 | + | |
| 653 | + | |
| 654 | + | |
| 655 | + | |
| 656 | + | |
| 657 | + | |
| 658 | + | |
| 659 | + | |
| 660 | + | |
| 661 | + | |
| 662 | + | |
| 663 | + | |
| 664 | + | |
| 665 | + | |
| 666 | + | |
| 667 | + | |
646 | 668 | | |
647 | 669 | | |
648 | 670 | | |
| |||
Lines changed: 19 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
195 | 195 | | |
196 | 196 | | |
197 | 197 | | |
| 198 | + | |
| 199 | + | |
| 200 | + | |
| 201 | + | |
| 202 | + | |
| 203 | + | |
| 204 | + | |
| 205 | + | |
| 206 | + | |
| 207 | + | |
| 208 | + | |
| 209 | + | |
| 210 | + | |
| 211 | + | |
| 212 | + | |
| 213 | + | |
| 214 | + | |
| 215 | + | |
| 216 | + | |
198 | 217 | | |
199 | 218 | | |
200 | 219 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
66 | 66 | | |
67 | 67 | | |
68 | 68 | | |
| 69 | + | |
| 70 | + | |
| 71 | + | |
69 | 72 | | |
70 | 73 | | |
71 | 74 | | |
| |||
168 | 171 | | |
169 | 172 | | |
170 | 173 | | |
| 174 | + | |
| 175 | + | |
| 176 | + | |
171 | 177 | | |
172 | 178 | | |
173 | 179 | | |
| |||
197 | 203 | | |
198 | 204 | | |
199 | 205 | | |
| 206 | + | |
| 207 | + | |
| 208 | + | |
200 | 209 | | |
201 | 210 | | |
202 | 211 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
286 | 286 | | |
287 | 287 | | |
288 | 288 | | |
289 | | - | |
290 | | - | |
291 | | - | |
| 289 | + | |
| 290 | + | |
| 291 | + | |
292 | 292 | | |
293 | 293 | | |
294 | 294 | | |
| |||
299 | 299 | | |
300 | 300 | | |
301 | 301 | | |
302 | | - | |
303 | 302 | | |
| 303 | + | |
| 304 | + | |
| 305 | + | |
304 | 306 | | |
305 | 307 | | |
306 | 308 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
302 | 302 | | |
303 | 303 | | |
304 | 304 | | |
305 | | - | |
306 | | - | |
| 305 | + | |
| 306 | + | |
307 | 307 | | |
308 | 308 | | |
309 | 309 | | |
| |||
0 commit comments