Skip to content

Commit 1a51dd9

Browse files
borsbors
committed
Auto merge of #3754 - Vanille-N:master, r=RalfJung
Make unused states of Reserved unrepresentable In the [previous TB update](rust-lang/miri#3742) we discovered that the existence of `Reserved + !ty_is_freeze + protected` is undesirable. This has the side effect of making `Reserved { conflicted: true, ty_is_freeze: false }` unreachable. As such it is desirable that this state would also be unrepresentable. This PR eliminates the unused configuration by changing ```rs enum PermissionPriv { Reserved { ty_is_freeze: bool, conflicted: bool }, ... } ``` into ```rs enum PermissionPriv { ReservedFrz { conflicted: bool }, ReservedIM, ... } ``` but this is not the only solution and `Reserved(Activable | Conflicted | InteriorMut)` could be discussed. In addition to making the unreachable state not representable anymore, this change has the nice side effect of enabling `foreign_read` to no longer depend explicitly on the `protected` flag. Currently waiting for - `@JoJoDeveloping` to confirm that this is the same representation of `Reserved` as what is being implemented in simuliris, - `@RalfJung` to approve that this does not introduce too much overhead in the trusted codebase.
2 parents 86783be + 2c166f4 commit 1a51dd9

13 files changed

+200
-134
lines changed

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

Lines changed: 12 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,6 @@
11
use rustc_middle::{
22
mir::{Mutability, RetagKind},
3-
ty::{
4-
self,
5-
layout::{HasParamEnv, HasTyCtxt},
6-
Ty,
7-
},
3+
ty::{self, layout::HasParamEnv, Ty},
84
};
95
use rustc_span::def_id::DefId;
106
use rustc_target::abi::{Abi, Size};
@@ -146,10 +142,9 @@ impl<'tcx> NewPermission {
146142
// interior mutability and protectors interact poorly.
147143
// To eliminate the case of Protected Reserved IM we override interior mutability
148144
// in the case of a protected reference: protected references are always considered
149-
// "freeze".
145+
// "freeze" in their reservation phase.
150146
let initial_state = match mutability {
151-
Mutability::Mut if ty_is_unpin =>
152-
Permission::new_reserved(ty_is_freeze || is_protected),
147+
Mutability::Mut if ty_is_unpin => Permission::new_reserved(ty_is_freeze, is_protected),
153148
Mutability::Not if ty_is_freeze => Permission::new_frozen(),
154149
// Raw pointers never enter this function so they are not handled.
155150
// However raw pointers are not the only pointers that take the parent
@@ -176,10 +171,12 @@ impl<'tcx> NewPermission {
176171
// Regular `Unpin` box, give it `noalias` but only a weak protector
177172
// because it is valid to deallocate it within the function.
178173
let ty_is_freeze = ty.is_freeze(*cx.tcx, cx.param_env());
174+
let protected = kind == RetagKind::FnEntry;
175+
let initial_state = Permission::new_reserved(ty_is_freeze, protected);
179176
Self {
180177
zero_size,
181-
initial_state: Permission::new_reserved(ty_is_freeze),
182-
protector: (kind == RetagKind::FnEntry).then_some(ProtectorKind::WeakProtector),
178+
initial_state,
179+
protector: protected.then_some(ProtectorKind::WeakProtector),
183180
}
184181
})
185182
}
@@ -521,11 +518,13 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
521518
fn tb_protect_place(&mut self, place: &MPlaceTy<'tcx>) -> InterpResult<'tcx, MPlaceTy<'tcx>> {
522519
let this = self.eval_context_mut();
523520

521+
// Note: if we were to inline `new_reserved` below we would find out that
522+
// `ty_is_freeze` is eventually unused because it appears in a `ty_is_freeze || true`.
523+
// We are nevertheless including it here for clarity.
524+
let ty_is_freeze = place.layout.ty.is_freeze(*this.tcx, this.param_env());
524525
// Retag it. With protection! That is the entire point.
525526
let new_perm = NewPermission {
526-
initial_state: Permission::new_reserved(
527-
place.layout.ty.is_freeze(this.tcx(), this.param_env()),
528-
),
527+
initial_state: Permission::new_reserved(ty_is_freeze, /* protected */ true),
529528
zero_size: false,
530529
protector: Some(ProtectorKind::StrongProtector),
531530
};

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

Lines changed: 113 additions & 69 deletions
Large diffs are not rendered by default.

‎src/tools/miri/src/borrow_tracker/tree_borrows/tree/tests.rs

Lines changed: 29 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,15 @@ impl Exhaustive for LocationState {
1414
}
1515
}
1616

17+
impl LocationState {
18+
/// Ensure that the current internal state can exist at the same time as a protector.
19+
/// In practice this only eliminates `ReservedIM` that is never used in the presence
20+
/// of a protector (we instead emit `ReservedFrz` on retag).
21+
pub fn compatible_with_protector(&self) -> bool {
22+
self.permission.compatible_with_protector()
23+
}
24+
}
25+
1726
#[test]
1827
#[rustfmt::skip]
1928
// Exhaustive check that for any starting configuration loc,
@@ -30,6 +39,9 @@ fn all_read_accesses_commute() {
3039
// so the two read accesses occur under the same protector.
3140
for protected in bool::exhaustive() {
3241
for loc in LocationState::exhaustive() {
42+
if protected {
43+
precondition!(loc.compatible_with_protector());
44+
}
3345
// Apply 1 then 2. Failure here means that there is UB in the source
3446
// and we skip the check in the target.
3547
let mut loc12 = loc;
@@ -61,8 +73,8 @@ fn protected_enforces_noalias() {
6173
// We want to check pairs of accesses where one is foreign and one is not.
6274
precondition!(rel1.is_foreign() != rel2.is_foreign());
6375
for [kind1, kind2] in <[AccessKind; 2]>::exhaustive() {
64-
for mut state in LocationState::exhaustive() {
65-
let protected = true;
76+
let protected = true;
77+
for mut state in LocationState::exhaustive().filter(|s| s.compatible_with_protector()) {
6678
precondition!(state.perform_access(kind1, rel1, protected).is_ok());
6779
precondition!(state.perform_access(kind2, rel2, protected).is_ok());
6880
// If these were both allowed, it must have been two reads.
@@ -387,6 +399,9 @@ mod spurious_read {
387399

388400
fn retag_y(self, new_y: LocStateProt) -> Result<Self, ()> {
389401
assert!(new_y.is_initial());
402+
if new_y.prot && !new_y.state.compatible_with_protector() {
403+
return Err(());
404+
}
390405
// `xy_rel` changes to "mutually foreign" now: `y` can no longer be a parent of `x`.
391406
Self { y: new_y, xy_rel: RelPosXY::MutuallyForeign, ..self }
392407
.read_if_initialized(PtrSelector::Y)
@@ -511,7 +526,7 @@ mod spurious_read {
511526
}
512527

513528
#[test]
514-
// `Reserved(aliased=false)` and `Reserved(aliased=true)` are properly indistinguishable
529+
// `Reserved { conflicted: false }` and `Reserved { conflicted: true }` are properly indistinguishable
515530
// under the conditions where we want to insert a spurious read.
516531
fn reserved_aliased_protected_indistinguishable() {
517532
let source = LocStateProtPair {
@@ -521,14 +536,16 @@ mod spurious_read {
521536
prot: true,
522537
},
523538
y: LocStateProt {
524-
state: LocationState::new_uninit(Permission::new_reserved(false)),
539+
state: LocationState::new_uninit(Permission::new_reserved(
540+
/* freeze */ true, /* protected */ true,
541+
)),
525542
prot: true,
526543
},
527544
};
528545
let acc = TestAccess { ptr: PtrSelector::X, kind: AccessKind::Read };
529546
let target = source.clone().perform_test_access(&acc).unwrap();
530-
assert!(source.y.state.permission.is_reserved_with_conflicted(false));
531-
assert!(target.y.state.permission.is_reserved_with_conflicted(true));
547+
assert!(source.y.state.permission.is_reserved_frz_with_conflicted(false));
548+
assert!(target.y.state.permission.is_reserved_frz_with_conflicted(true));
532549
assert!(!source.distinguishable::<(), ()>(&target))
533550
}
534551

@@ -563,7 +580,13 @@ mod spurious_read {
563580
precondition!(x_retag_perm.initialized);
564581
// And `x` just got retagged, so it must be initial.
565582
precondition!(x_retag_perm.permission.is_initial());
583+
// As stated earlier, `x` is always protected in the patterns we consider here.
584+
precondition!(x_retag_perm.compatible_with_protector());
566585
for y_protected in bool::exhaustive() {
586+
// Finally `y` that is optionally protected must have a compatible permission.
587+
if y_protected {
588+
precondition!(y_current_perm.compatible_with_protector());
589+
}
567590
v.push(Pattern { xy_rel, x_retag_perm, y_current_perm, y_protected });
568591
}
569592
}

‎src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,11 @@
22
Warning: this tree is indicative only. Some tags may have been hidden.
33
0.. 1
44
| Act | └─┬──<TAG=root of the allocation>
5-
| RsM | └─┬──<TAG=base>
6-
| RsM | ├─┬──<TAG=x>
7-
| RsM | │ └─┬──<TAG=caller:x>
8-
| Rs | │ └────<TAG=callee:x> Strongly protected
9-
| RsM | └────<TAG=y, callee:y, caller:y>
5+
| ReIM| └─┬──<TAG=base>
6+
| ReIM| ├─┬──<TAG=x>
7+
| ReIM| │ └─┬──<TAG=caller:x>
8+
| Res | │ └────<TAG=callee:x> Strongly protected
9+
| ReIM| └────<TAG=y, callee:y, caller:y>
1010
──────────────────────────────────────────────────
1111
error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) at ALLOC[0x0] is forbidden
1212
--> $DIR/cell-protected-write.rs:LL:CC

‎src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,11 @@
22
Warning: this tree is indicative only. Some tags may have been hidden.
33
0.. 1
44
| Act | └─┬──<TAG=root of the allocation>
5-
| Rs | └─┬──<TAG=n>
6-
| Rs | ├─┬──<TAG=x>
7-
| Rs | │ └─┬──<TAG=caller:x>
8-
| Rs | │ └────<TAG=callee:x> Strongly protected
9-
| Rs | └────<TAG=y, callee:y, caller:y>
5+
| Res | └─┬──<TAG=n>
6+
| Res | ├─┬──<TAG=x>
7+
| Res | │ └─┬──<TAG=caller:x>
8+
| Res | │ └────<TAG=callee:x> Strongly protected
9+
| Res | └────<TAG=y, callee:y, caller:y>
1010
──────────────────────────────────────────────────
1111
error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) at ALLOC[0x0] is forbidden
1212
--> $DIR/int-protected-write.rs:LL:CC

‎src/tools/miri/tests/pass/tree_borrows/cell-alternate-writes.stderr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
Warning: this tree is indicative only. Some tags may have been hidden.
33
0.. 1
44
| Act | └─┬──<TAG=root of the allocation>
5-
| RsM | └────<TAG=data, x, y>
5+
| ReIM| └────<TAG=data, x, y>
66
──────────────────────────────────────────────────
77
──────────────────────────────────────────────────
88
Warning: this tree is indicative only. Some tags may have been hidden.

‎src/tools/miri/tests/pass/tree_borrows/end-of-protector.stderr

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -2,27 +2,27 @@
22
Warning: this tree is indicative only. Some tags may have been hidden.
33
0.. 1
44
| Act | └─┬──<TAG=root of the allocation>
5-
| Rs | └─┬──<TAG=data>
6-
| Rs | └────<TAG=x>
5+
| Res | └─┬──<TAG=data>
6+
| Res | └────<TAG=x>
77
──────────────────────────────────────────────────
88
──────────────────────────────────────────────────
99
Warning: this tree is indicative only. Some tags may have been hidden.
1010
0.. 1
1111
| Act | └─┬──<TAG=root of the allocation>
12-
| Rs | └─┬──<TAG=data>
13-
| Rs | └─┬──<TAG=x>
14-
| Rs | └─┬──<TAG=caller:x>
15-
| Rs | └────<TAG=callee:x> Strongly protected
12+
| Res | └─┬──<TAG=data>
13+
| Res | └─┬──<TAG=x>
14+
| Res | └─┬──<TAG=caller:x>
15+
| Res | └────<TAG=callee:x> Strongly protected
1616
──────────────────────────────────────────────────
1717
──────────────────────────────────────────────────
1818
Warning: this tree is indicative only. Some tags may have been hidden.
1919
0.. 1
2020
| Act | └─┬──<TAG=root of the allocation>
21-
| Rs | └─┬──<TAG=data>
22-
| Rs | ├─┬──<TAG=x>
23-
| Rs | │ └─┬──<TAG=caller:x>
24-
| Rs | │ └────<TAG=callee:x>
25-
| Rs | └────<TAG=y>
21+
| Res | └─┬──<TAG=data>
22+
| Res | ├─┬──<TAG=x>
23+
| Res | │ └─┬──<TAG=caller:x>
24+
| Res | │ └────<TAG=callee:x>
25+
| Res | └────<TAG=y>
2626
──────────────────────────────────────────────────
2727
──────────────────────────────────────────────────
2828
Warning: this tree is indicative only. Some tags may have been hidden.

‎src/tools/miri/tests/pass/tree_borrows/formatting.stderr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
Warning: this tree is indicative only. Some tags may have been hidden.
33
0.. 1.. 2.. 10.. 11.. 100.. 101..1000..1001..1024
44
| Act | Act | Act | Act | Act | Act | Act | Act | Act | └─┬──<TAG=root of the allocation>
5-
| Rs | Act | Rs | Act | Rs | Act | Rs | Act | Rs | └─┬──<TAG=data, data>
5+
| Res | Act | Res | Act | Res | Act | Res | Act | Res | └─┬──<TAG=data, data>
66
|-----| Act |-----|?Dis |-----|?Dis |-----|?Dis |-----| ├────<TAG=data[1]>
77
|-----|-----|-----| Act |-----|?Dis |-----|?Dis |-----| ├────<TAG=data[10]>
88
|-----|-----|-----|-----|-----| Frz |-----|?Dis |-----| ├────<TAG=data[100]>

‎src/tools/miri/tests/pass/tree_borrows/reborrow-is-read.stderr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,5 +11,5 @@ Warning: this tree is indicative only. Some tags may have been hidden.
1111
| Act | └─┬──<TAG=root of the allocation>
1212
| Act | └─┬──<TAG=parent>
1313
| Frz | ├────<TAG=x>
14-
| Rs | └────<TAG=y>
14+
| Res | └────<TAG=y>
1515
──────────────────────────────────────────────────

‎src/tools/miri/tests/pass/tree_borrows/reserved.stderr

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -3,49 +3,49 @@
33
Warning: this tree is indicative only. Some tags may have been hidden.
44
0.. 1
55
| Act | └─┬──<TAG=root of the allocation>
6-
| RsM | └─┬──<TAG=base>
7-
| RsM | ├─┬──<TAG=x>
8-
| RsM | │ └─┬──<TAG=caller:x>
9-
| RsC | │ └────<TAG=callee:x>
10-
| RsM | └────<TAG=y, caller:y, callee:y>
6+
| ReIM| └─┬──<TAG=base>
7+
| ReIM| ├─┬──<TAG=x>
8+
| ReIM| │ └─┬──<TAG=caller:x>
9+
| ResC| │ └────<TAG=callee:x>
10+
| ReIM| └────<TAG=y, caller:y, callee:y>
1111
──────────────────────────────────────────────────
1212
[interior mut] Foreign Read: Re* -> Re*
1313
──────────────────────────────────────────────────
1414
Warning: this tree is indicative only. Some tags may have been hidden.
1515
0.. 8
1616
| Act | └─┬──<TAG=root of the allocation>
17-
| RsM | └─┬──<TAG=base>
18-
| RsM | ├────<TAG=x>
19-
| RsM | └────<TAG=y>
17+
| ReIM| └─┬──<TAG=base>
18+
| ReIM| ├────<TAG=x>
19+
| ReIM| └────<TAG=y>
2020
──────────────────────────────────────────────────
2121
[interior mut] Foreign Write: Re* -> Re*
2222
──────────────────────────────────────────────────
2323
Warning: this tree is indicative only. Some tags may have been hidden.
2424
0.. 8
2525
| Act | └─┬──<TAG=root of the allocation>
2626
| Act | └─┬──<TAG=base>
27-
| RsM | ├────<TAG=x>
27+
| ReIM| ├────<TAG=x>
2828
| Act | └────<TAG=y>
2929
──────────────────────────────────────────────────
3030
[protected] Foreign Read: Res -> Frz
3131
──────────────────────────────────────────────────
3232
Warning: this tree is indicative only. Some tags may have been hidden.
3333
0.. 1
3434
| Act | └─┬──<TAG=root of the allocation>
35-
| Rs | └─┬──<TAG=base>
36-
| Rs | ├─┬──<TAG=x>
37-
| Rs | │ └─┬──<TAG=caller:x>
38-
| RsC | │ └────<TAG=callee:x>
39-
| Rs | └────<TAG=y, caller:y, callee:y>
35+
| Res | └─┬──<TAG=base>
36+
| Res | ├─┬──<TAG=x>
37+
| Res | │ └─┬──<TAG=caller:x>
38+
| ResC| │ └────<TAG=callee:x>
39+
| Res | └────<TAG=y, caller:y, callee:y>
4040
──────────────────────────────────────────────────
4141
[] Foreign Read: Res -> Res
4242
──────────────────────────────────────────────────
4343
Warning: this tree is indicative only. Some tags may have been hidden.
4444
0.. 1
4545
| Act | └─┬──<TAG=root of the allocation>
46-
| Rs | └─┬──<TAG=base>
47-
| Rs | ├────<TAG=x>
48-
| Rs | └────<TAG=y>
46+
| Res | └─┬──<TAG=base>
47+
| Res | ├────<TAG=x>
48+
| Res | └────<TAG=y>
4949
──────────────────────────────────────────────────
5050
[] Foreign Write: Res -> Dis
5151
──────────────────────────────────────────────────

‎src/tools/miri/tests/pass/tree_borrows/unique.default.stderr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@
22
Warning: this tree is indicative only. Some tags may have been hidden.
33
0.. 1
44
| Act | └─┬──<TAG=root of the allocation>
5-
| Rs | └─┬──<TAG=base>
6-
| Rs | └────<TAG=raw, uniq, uniq>
5+
| Res | └─┬──<TAG=base>
6+
| Res | └────<TAG=raw, uniq, uniq>
77
──────────────────────────────────────────────────
88
──────────────────────────────────────────────────
99
Warning: this tree is indicative only. Some tags may have been hidden.

‎src/tools/miri/tests/pass/tree_borrows/unique.uniq.stderr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@
22
Warning: this tree is indicative only. Some tags may have been hidden.
33
0.. 1
44
| Act | └─┬──<TAG=root of the allocation>
5-
| Rs | └─┬──<TAG=base>
6-
| Rs | └─┬──<TAG=raw>
5+
| Res | └─┬──<TAG=base>
6+
| Res | └─┬──<TAG=raw>
77
|-----| └────<TAG=uniq, uniq>
88
──────────────────────────────────────────────────
99
──────────────────────────────────────────────────

‎src/tools/miri/tests/pass/tree_borrows/vec_unique.default.stderr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
Warning: this tree is indicative only. Some tags may have been hidden.
33
0.. 2
44
| Act | └─┬──<TAG=root of the allocation>
5-
| Rs | └────<TAG=base.as_ptr(), base.as_ptr(), raw_parts.0, reconstructed.as_ptr(), reconstructed.as_ptr()>
5+
| Res | └────<TAG=base.as_ptr(), base.as_ptr(), raw_parts.0, reconstructed.as_ptr(), reconstructed.as_ptr()>
66
──────────────────────────────────────────────────

0 commit comments

Comments
 (0)