Skip to content

Commit ec6d6b9

Browse files
workingjubileeworkingjubilee
authored
Rollup merge of #142260 - RalfJung:miri-sync, r=RalfJung
Miri subtree update r? `@ghost`
2 parents a5a7977 + eb420d1 commit ec6d6b9

File tree

21 files changed

+285
-202
lines changed

21 files changed

+285
-202
lines changed

‎Cargo.lock

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2326,7 +2326,6 @@ dependencies = [
23262326
"tempfile",
23272327
"tikv-jemalloc-sys",
23282328
"ui_test",
2329-
"windows-sys 0.59.0",
23302329
]
23312330

23322331
[[package]]

‎src/tools/miri/Cargo.lock

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -555,7 +555,6 @@ dependencies = [
555555
"tempfile",
556556
"tikv-jemalloc-sys",
557557
"ui_test",
558-
"windows-sys",
559558
]
560559

561560
[[package]]

‎src/tools/miri/Cargo.toml

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -40,13 +40,6 @@ libc = "0.2"
4040
libffi = "4.0.0"
4141
libloading = "0.8"
4242

43-
[target.'cfg(target_family = "windows")'.dependencies]
44-
windows-sys = { version = "0.59", features = [
45-
"Win32_Foundation",
46-
"Win32_System_IO",
47-
"Win32_Storage_FileSystem",
48-
] }
49-
5043
[dev-dependencies]
5144
ui_test = "0.29.1"
5245
colored = "2"

‎src/tools/miri/README.md

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -398,9 +398,11 @@ to Miri failing to detect cases of undefined behavior in a program.
398398
**unsound** since the fallback body might not be checking for all UB.
399399
* `-Zmiri-native-lib=<path to a shared object file>` is an experimental flag for providing support
400400
for calling native functions from inside the interpreter via FFI. The flag is supported only on
401-
Unix systems. Functions not provided by that file are still executed via the usual Miri shims.
401+
Unix systems. Functions not provided by that file are still executed via the usual Miri shims. If
402+
a path to a directory is specified, all files in that directory are included nonrecursively. This
403+
flag can be passed multiple times to specify multiple files and/or directories.
402404
**WARNING**: If an invalid/incorrect `.so` file is specified, this can cause Undefined Behavior in
403-
Miri itself! And of course, Miri cannot do any checks on the actions taken by the native code.
405+
Miri itself! And of course, Miri often cannot do any checks on the actions taken by the native code.
404406
Note that Miri has its own handling of file descriptors, so if you want to replace *some*
405407
functions working on file descriptors, you will have to replace *all* of them, or the two kinds of
406408
file descriptors will be mixed up. This is **work in progress**; currently, only integer and
@@ -458,6 +460,10 @@ to Miri failing to detect cases of undefined behavior in a program.
458460
This is much less likely with Stacked Borrows.
459461
Using Tree Borrows currently implies `-Zmiri-strict-provenance` because integer-to-pointer
460462
casts are not supported in this mode, but that may change in the future.
463+
* `-Zmiri-tree-borrows-no-precise-interior-mut` makes Tree Borrows
464+
track interior mutable data on the level of references instead of on the
465+
byte-level as is done by default. Therefore, with this flag, Tree
466+
Borrows will be more permissive.
461467
* `-Zmiri-force-page-size=<num>` overrides the default page size for an architecture, in multiples of 1k.
462468
`4` is default for most targets. This value should always be a power of 2 and nonzero.
463469

‎src/tools/miri/rust-version

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
337c11e5932275e7d450c1f2e26f289f0ddfa717
1+
c31cccb7b5cc098b1a8c1794ed38d7fdbec0ccb0

‎src/tools/miri/src/alloc_addresses/mod.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,7 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
132132
assert!(!matches!(info.kind, AllocKind::Dead));
133133

134134
// This allocation does not have a base address yet, pick or reuse one.
135-
if this.machine.native_lib.is_some() {
135+
if !this.machine.native_lib.is_empty() {
136136
// In native lib mode, we use the "real" address of the bytes for this allocation.
137137
// This ensures the interpreted program and native code have the same view of memory.
138138
let params = this.machine.get_default_alloc_params();
@@ -413,7 +413,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
413413
) -> InterpResult<'tcx, MiriAllocBytes> {
414414
let this = self.eval_context_ref();
415415
assert!(this.tcx.try_get_global_alloc(id).is_some());
416-
if this.machine.native_lib.is_some() {
416+
if !this.machine.native_lib.is_empty() {
417417
// In native lib mode, MiriAllocBytes for global allocations are handled via `prepared_alloc_bytes`.
418418
// This additional call ensures that some `MiriAllocBytes` are always prepared, just in case
419419
// this function gets called before the first time `addr_from_alloc_id` gets called.

‎src/tools/miri/src/bin/miri.rs

Lines changed: 30 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ use std::sync::{Arc, Once};
3535

3636
use miri::{
3737
BacktraceStyle, BorrowTrackerMethod, GenmcConfig, GenmcCtx, MiriConfig, MiriEntryFnType,
38-
ProvenanceMode, RetagFields, ValidationMode,
38+
ProvenanceMode, RetagFields, TreeBorrowsParams, ValidationMode,
3939
};
4040
use rustc_abi::ExternAbi;
4141
use rustc_data_structures::sync;
@@ -554,8 +554,21 @@ fn main() {
554554
} else if arg == "-Zmiri-disable-stacked-borrows" {
555555
miri_config.borrow_tracker = None;
556556
} else if arg == "-Zmiri-tree-borrows" {
557-
miri_config.borrow_tracker = Some(BorrowTrackerMethod::TreeBorrows);
557+
miri_config.borrow_tracker =
558+
Some(BorrowTrackerMethod::TreeBorrows(TreeBorrowsParams {
559+
precise_interior_mut: true,
560+
}));
558561
miri_config.provenance_mode = ProvenanceMode::Strict;
562+
} else if arg == "-Zmiri-tree-borrows-no-precise-interior-mut" {
563+
match &mut miri_config.borrow_tracker {
564+
Some(BorrowTrackerMethod::TreeBorrows(params)) => {
565+
params.precise_interior_mut = false;
566+
}
567+
_ =>
568+
show_error!(
569+
"`-Zmiri-tree-borrows` is required before `-Zmiri-tree-borrows-no-precise-interior-mut`"
570+
),
571+
};
559572
} else if arg == "-Zmiri-disable-data-race-detector" {
560573
miri_config.data_race_detector = false;
561574
miri_config.weak_memory_emulation = false;
@@ -692,11 +705,18 @@ fn main() {
692705
};
693706
} else if let Some(param) = arg.strip_prefix("-Zmiri-native-lib=") {
694707
let filename = param.to_string();
695-
if std::path::Path::new(&filename).exists() {
696-
if let Some(other_filename) = miri_config.native_lib {
697-
show_error!("-Zmiri-native-lib is already set to {}", other_filename.display());
708+
let file_path = std::path::Path::new(&filename);
709+
if file_path.exists() {
710+
// For directories, nonrecursively add all normal files inside
711+
if let Ok(dir) = file_path.read_dir() {
712+
for lib in dir.filter_map(|res| res.ok()) {
713+
if lib.file_type().unwrap().is_file() {
714+
miri_config.native_lib.push(lib.path().to_owned());
715+
}
716+
}
717+
} else {
718+
miri_config.native_lib.push(filename.into());
698719
}
699-
miri_config.native_lib = Some(filename.into());
700720
} else {
701721
show_error!("-Zmiri-native-lib `{}` does not exist", filename);
702722
}
@@ -725,18 +745,19 @@ fn main() {
725745
}
726746
}
727747
// Tree Borrows implies strict provenance, and is not compatible with native calls.
728-
if matches!(miri_config.borrow_tracker, Some(BorrowTrackerMethod::TreeBorrows)) {
748+
if matches!(miri_config.borrow_tracker, Some(BorrowTrackerMethod::TreeBorrows { .. })) {
729749
if miri_config.provenance_mode != ProvenanceMode::Strict {
730750
show_error!(
731751
"Tree Borrows does not support integer-to-pointer casts, and hence requires strict provenance"
732752
);
733753
}
734-
if miri_config.native_lib.is_some() {
754+
if !miri_config.native_lib.is_empty() {
735755
show_error!("Tree Borrows is not compatible with calling native functions");
736756
}
737757
}
758+
738759
// Native calls and strict provenance are not compatible.
739-
if miri_config.native_lib.is_some() && miri_config.provenance_mode == ProvenanceMode::Strict {
760+
if !miri_config.native_lib.is_empty() && miri_config.provenance_mode == ProvenanceMode::Strict {
740761
show_error!("strict provenance is not compatible with calling native functions");
741762
}
742763
// You can set either one seed or many.

‎src/tools/miri/src/borrow_tracker/mod.rs

Lines changed: 21 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -226,7 +226,13 @@ pub enum BorrowTrackerMethod {
226226
/// Stacked Borrows, as implemented in borrow_tracker/stacked_borrows
227227
StackedBorrows,
228228
/// Tree borrows, as implemented in borrow_tracker/tree_borrows
229-
TreeBorrows,
229+
TreeBorrows(TreeBorrowsParams),
230+
}
231+
232+
/// Parameters that Tree Borrows can take.
233+
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
234+
pub struct TreeBorrowsParams {
235+
pub precise_interior_mut: bool,
230236
}
231237

232238
impl BorrowTrackerMethod {
@@ -237,6 +243,13 @@ impl BorrowTrackerMethod {
237243
config.retag_fields,
238244
))
239245
}
246+
247+
pub fn get_tree_borrows_params(self) -> TreeBorrowsParams {
248+
match self {
249+
BorrowTrackerMethod::TreeBorrows(params) => params,
250+
_ => panic!("can only be called when `BorrowTrackerMethod` is `TreeBorrows`"),
251+
}
252+
}
240253
}
241254

242255
impl GlobalStateInner {
@@ -252,7 +265,7 @@ impl GlobalStateInner {
252265
AllocState::StackedBorrows(Box::new(RefCell::new(Stacks::new_allocation(
253266
id, alloc_size, self, kind, machine,
254267
)))),
255-
BorrowTrackerMethod::TreeBorrows =>
268+
BorrowTrackerMethod::TreeBorrows { .. } =>
256269
AllocState::TreeBorrows(Box::new(RefCell::new(Tree::new_allocation(
257270
id, alloc_size, self, kind, machine,
258271
)))),
@@ -271,7 +284,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
271284
let method = this.machine.borrow_tracker.as_ref().unwrap().borrow().borrow_tracker_method;
272285
match method {
273286
BorrowTrackerMethod::StackedBorrows => this.sb_retag_ptr_value(kind, val),
274-
BorrowTrackerMethod::TreeBorrows => this.tb_retag_ptr_value(kind, val),
287+
BorrowTrackerMethod::TreeBorrows { .. } => this.tb_retag_ptr_value(kind, val),
275288
}
276289
}
277290

@@ -284,7 +297,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
284297
let method = this.machine.borrow_tracker.as_ref().unwrap().borrow().borrow_tracker_method;
285298
match method {
286299
BorrowTrackerMethod::StackedBorrows => this.sb_retag_place_contents(kind, place),
287-
BorrowTrackerMethod::TreeBorrows => this.tb_retag_place_contents(kind, place),
300+
BorrowTrackerMethod::TreeBorrows { .. } => this.tb_retag_place_contents(kind, place),
288301
}
289302
}
290303

@@ -293,7 +306,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
293306
let method = this.machine.borrow_tracker.as_ref().unwrap().borrow().borrow_tracker_method;
294307
match method {
295308
BorrowTrackerMethod::StackedBorrows => this.sb_protect_place(place),
296-
BorrowTrackerMethod::TreeBorrows => this.tb_protect_place(place),
309+
BorrowTrackerMethod::TreeBorrows { .. } => this.tb_protect_place(place),
297310
}
298311
}
299312

@@ -302,7 +315,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
302315
let method = this.machine.borrow_tracker.as_ref().unwrap().borrow().borrow_tracker_method;
303316
match method {
304317
BorrowTrackerMethod::StackedBorrows => this.sb_expose_tag(alloc_id, tag),
305-
BorrowTrackerMethod::TreeBorrows => this.tb_expose_tag(alloc_id, tag),
318+
BorrowTrackerMethod::TreeBorrows { .. } => this.tb_expose_tag(alloc_id, tag),
306319
}
307320
}
308321

@@ -319,7 +332,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
319332
this.tcx.tcx.dcx().warn("Stacked Borrows does not support named pointers; `miri_pointer_name` is a no-op");
320333
interp_ok(())
321334
}
322-
BorrowTrackerMethod::TreeBorrows =>
335+
BorrowTrackerMethod::TreeBorrows { .. } =>
323336
this.tb_give_pointer_debug_name(ptr, nth_parent, name),
324337
}
325338
}
@@ -333,7 +346,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
333346
let method = borrow_tracker.borrow().borrow_tracker_method;
334347
match method {
335348
BorrowTrackerMethod::StackedBorrows => this.print_stacks(alloc_id),
336-
BorrowTrackerMethod::TreeBorrows => this.print_tree(alloc_id, show_unnamed),
349+
BorrowTrackerMethod::TreeBorrows { .. } => this.print_tree(alloc_id, show_unnamed),
337350
}
338351
}
339352

‎src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs

Lines changed: 65 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -312,8 +312,6 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
312312
}
313313

314314
let span = this.machine.current_span();
315-
let alloc_extra = this.get_alloc_extra(alloc_id)?;
316-
let mut tree_borrows = alloc_extra.borrow_tracker_tb().borrow_mut();
317315

318316
// Store initial permissions and their corresponding range.
319317
let mut perms_map: RangeMap<LocationState> = RangeMap::new(
@@ -342,36 +340,83 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
342340
assert!(new_perm.freeze_access);
343341

344342
let protected = new_perm.protector.is_some();
345-
this.visit_freeze_sensitive(place, ptr_size, |range, frozen| {
346-
has_unsafe_cell = has_unsafe_cell || !frozen;
347-
348-
// We are only ever `Frozen` inside the frozen bits.
349-
let (perm, access) = if frozen {
343+
let precise_interior_mut = this
344+
.machine
345+
.borrow_tracker
346+
.as_mut()
347+
.unwrap()
348+
.get_mut()
349+
.borrow_tracker_method
350+
.get_tree_borrows_params()
351+
.precise_interior_mut;
352+
353+
let default_perm = if !precise_interior_mut {
354+
// NOTE: Using `ty_is_freeze` doesn't give the same result as going through the range
355+
// and computing `has_unsafe_cell`. This is because of zero-sized `UnsafeCell`, for which
356+
// `has_unsafe_cell` is false, but `!ty_is_freeze` is true.
357+
let ty_is_freeze = place.layout.ty.is_freeze(*this.tcx, this.typing_env());
358+
let (perm, access) = if ty_is_freeze {
350359
(new_perm.freeze_perm, new_perm.freeze_access)
351360
} else {
352361
(new_perm.nonfreeze_perm, new_perm.nonfreeze_access)
353362
};
363+
let sifa = perm.strongest_idempotent_foreign_access(protected);
364+
let new_loc = if access {
365+
LocationState::new_accessed(perm, sifa)
366+
} else {
367+
LocationState::new_non_accessed(perm, sifa)
368+
};
369+
370+
for (_loc_range, loc) in perms_map.iter_mut_all() {
371+
*loc = new_loc;
372+
}
373+
374+
perm
375+
} else {
376+
this.visit_freeze_sensitive(place, ptr_size, |range, frozen| {
377+
has_unsafe_cell = has_unsafe_cell || !frozen;
354378

355-
// Store initial permissions.
356-
for (_loc_range, loc) in perms_map.iter_mut(range.start, range.size) {
379+
// We are only ever `Frozen` inside the frozen bits.
380+
let (perm, access) = if frozen {
381+
(new_perm.freeze_perm, new_perm.freeze_access)
382+
} else {
383+
(new_perm.nonfreeze_perm, new_perm.nonfreeze_access)
384+
};
357385
let sifa = perm.strongest_idempotent_foreign_access(protected);
358386
// NOTE: Currently, `access` is false if and only if `perm` is Cell, so this `if`
359387
// doesn't not change whether any code is UB or not. We could just always use
360388
// `new_accessed` and everything would stay the same. But that seems conceptually
361389
// odd, so we keep the initial "accessed" bit of the `LocationState` in sync with whether
362390
// a read access is performed below.
363-
if access {
364-
*loc = LocationState::new_accessed(perm, sifa);
391+
let new_loc = if access {
392+
LocationState::new_accessed(perm, sifa)
365393
} else {
366-
*loc = LocationState::new_non_accessed(perm, sifa);
394+
LocationState::new_non_accessed(perm, sifa)
395+
};
396+
397+
// Store initial permissions.
398+
for (_loc_range, loc) in perms_map.iter_mut(range.start, range.size) {
399+
*loc = new_loc;
367400
}
368-
}
369401

370-
// Some reborrows incur a read access to the parent.
371-
if access {
402+
interp_ok(())
403+
})?;
404+
405+
// Allow lazily writing to surrounding data if we found an `UnsafeCell`.
406+
if has_unsafe_cell { new_perm.nonfreeze_perm } else { new_perm.freeze_perm }
407+
};
408+
409+
let alloc_extra = this.get_alloc_extra(alloc_id)?;
410+
let mut tree_borrows = alloc_extra.borrow_tracker_tb().borrow_mut();
411+
412+
for (perm_range, perm) in perms_map.iter_mut_all() {
413+
if perm.is_accessed() {
414+
// Some reborrows incur a read access to the parent.
372415
// Adjust range to be relative to allocation start (rather than to `place`).
373-
let mut range_in_alloc = range;
374-
range_in_alloc.start += base_offset;
416+
let range_in_alloc = AllocRange {
417+
start: Size::from_bytes(perm_range.start) + base_offset,
418+
size: Size::from_bytes(perm_range.end - perm_range.start),
419+
};
375420

376421
tree_borrows.perform_access(
377422
orig_tag,
@@ -382,7 +427,7 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
382427
)?;
383428

384429
// Also inform the data race model (but only if any bytes are actually affected).
385-
if range.size.bytes() > 0 {
430+
if range_in_alloc.size.bytes() > 0 {
386431
if let Some(data_race) = alloc_extra.data_race.as_vclocks_ref() {
387432
data_race.read(
388433
alloc_id,
@@ -394,17 +439,15 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
394439
}
395440
}
396441
}
397-
interp_ok(())
398-
})?;
442+
}
399443

400444
// Record the parent-child pair in the tree.
401445
tree_borrows.new_child(
402446
base_offset,
403447
orig_tag,
404448
new_tag,
405449
perms_map,
406-
// Allow lazily writing to surrounding data if we found an `UnsafeCell`.
407-
if has_unsafe_cell { new_perm.nonfreeze_perm } else { new_perm.freeze_perm },
450+
default_perm,
408451
protected,
409452
span,
410453
)?;

‎src/tools/miri/src/diagnostics.rs

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -682,7 +682,10 @@ impl<'tcx> MiriMachine<'tcx> {
682682
),
683683
];
684684
if self.borrow_tracker.as_ref().is_some_and(|b| {
685-
matches!(b.borrow().borrow_tracker_method(), BorrowTrackerMethod::TreeBorrows)
685+
matches!(
686+
b.borrow().borrow_tracker_method(),
687+
BorrowTrackerMethod::TreeBorrows { .. }
688+
)
686689
}) {
687690
v.push(
688691
note!("Tree Borrows does not support integer-to-pointer casts, so the program is likely to go wrong when this pointer gets used")

0 commit comments

Comments
 (0)