Skip to content

Commit efc2af4

Browse files
committed
fix protectors so that all reads actually commute
1 parent 6ac86bb commit efc2af4

16 files changed

+59
-87
lines changed

src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -227,10 +227,10 @@ pub(super) enum TransitionError {
227227
ChildAccessForbidden(Permission),
228228
/// A protector was triggered due to an invalid transition that loses
229229
/// too much permissions.
230-
/// For example, if a protected tag goes from `Active` to `Frozen` due
231-
/// to a foreign write this will produce a `ProtectedTransition(PermTransition(Active, Frozen))`.
230+
/// For example, if a protected tag goes from `Active` to `Disabled` due
231+
/// to a foreign write this will produce a `ProtectedDisabled(Active)`.
232232
/// This kind of error can only occur on foreign accesses.
233-
ProtectedTransition(PermTransition),
233+
ProtectedDisabled(Permission),
234234
/// Cannot deallocate because some tag in the allocation is strongly protected.
235235
/// This kind of error can only occur on deallocations.
236236
ProtectedDealloc,
@@ -302,20 +302,17 @@ impl TbError<'_> {
302302
));
303303
(title, details, conflicting_tag_name)
304304
}
305-
ProtectedTransition(transition) => {
305+
ProtectedDisabled(before_disabled) => {
306306
let conflicting_tag_name = "protected";
307307
let access = cause.print_as_access(/* is_foreign */ true);
308308
let details = vec![
309309
format!(
310310
"the accessed tag {accessed} is foreign to the {conflicting_tag_name} tag {conflicting} (i.e., it is not a child)"
311311
),
312312
format!(
313-
"this {access} would cause the {conflicting_tag_name} tag {conflicting} to transition {transition}"
314-
),
315-
format!(
316-
"this transition would be {loss}, which is not allowed for protected tags",
317-
loss = transition.summary(),
313+
"this {access} would cause the {conflicting_tag_name} tag {conflicting} currently {before_disabled} to become Disabled"
318314
),
315+
format!("protected tags must not become Disabled"),
319316
];
320317
(title, details, conflicting_tag_name)
321318
}

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

Lines changed: 25 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,12 @@ mod transition {
7272
// accesses, since the data is not being mutated. Hence the `{ .. }`
7373
res @ Reserved { .. } if !protected => res,
7474
Reserved { .. } => Frozen, // protected reserved
75-
Active => Frozen,
75+
Active =>
76+
if protected {
77+
Disabled
78+
} else {
79+
Frozen
80+
},
7681
non_writeable @ (Frozen | Disabled) => non_writeable,
7782
})
7883
}
@@ -189,34 +194,9 @@ impl PermTransition {
189194
Permission { inner: self.from }
190195
}
191196

192-
/// Determines whether a transition that occured is compatible with the presence
193-
/// of a Protector. This is not included in the `transition` functions because
194-
/// it would distract from the few places where the transition is modified
195-
/// because of a protector, but not forbidden.
196-
///
197-
/// Note: this is not in charge of checking that there *is* a protector,
198-
/// it should be used as
199-
/// ```
200-
/// let no_protector_error = if is_protected(tag) {
201-
/// transition.is_allowed_by_protector()
202-
/// };
203-
/// ```
204-
pub fn is_allowed_by_protector(&self) -> bool {
205-
assert!(self.is_possible());
206-
match (self.from, self.to) {
207-
_ if self.from == self.to => true,
208-
// It is always a protector violation to not be readable anymore
209-
(_, Disabled) => false,
210-
// In the case of a `Reserved` under a protector, both transitions
211-
// `Reserved => Active` and `Reserved => Frozen` can legitimately occur.
212-
// The first is standard (Child Write), the second is for Foreign Writes
213-
// on protected Reserved where we must ensure that the pointer is not
214-
// written to in the future.
215-
(Reserved { .. }, Active) | (Reserved { .. }, Frozen) => true,
216-
// This pointer should have stayed writeable for the whole function
217-
(Active, Frozen) => false,
218-
_ => unreachable!("Transition {} should never be possible", self),
219-
}
197+
/// Determines if this transition would disable the permission.
198+
pub fn produces_disabled(self) -> bool {
199+
self.to == Disabled
220200
}
221201
}
222202

@@ -298,14 +278,15 @@ pub mod diagnostics {
298278
///
299279
/// This function assumes that its arguments apply to the same location
300280
/// and that they were obtained during a normal execution. It will panic otherwise.
301-
/// - `err` cannot be a `ProtectedTransition(_)` of a noop transition, as those
302-
/// never trigger protectors;
303281
/// - all transitions involved in `self` and `err` should be increasing
304282
/// (Reserved < Active < Frozen < Disabled);
305283
/// - between `self` and `err` the permission should also be increasing,
306284
/// so all permissions inside `err` should be greater than `self.1`;
307285
/// - `Active` and `Reserved` cannot cause an error due to insufficient permissions,
308286
/// so `err` cannot be a `ChildAccessForbidden(_)` of either of them;
287+
/// - `err` should not be `ProtectedDisabled(Disabled)`, because the protected
288+
/// tag should not have been `Disabled` in the first place (if this occurs it means
289+
/// we have unprotected tags that become protected)
309290
pub(in super::super) fn is_relevant(&self, err: TransitionError) -> bool {
310291
// NOTE: `super::super` is the visibility of `TransitionError`
311292
assert!(self.is_possible());
@@ -342,45 +323,39 @@ pub mod diagnostics {
342323
unreachable!("permissions between self and err must be increasing"),
343324
}
344325
}
345-
TransitionError::ProtectedTransition(forbidden) => {
346-
assert!(!forbidden.is_noop());
326+
TransitionError::ProtectedDisabled(before_disabled) => {
347327
// Show how we got to the starting point of the forbidden transition,
348328
// but ignore what came before.
349329
// This eliminates transitions like `Reserved -> Active`
350330
// when the error is a `Frozen -> Disabled`.
351-
match (self.to, forbidden.from, forbidden.to) {
331+
match (self.to, before_disabled.inner) {
352332
// We absolutely want to know where it was activated.
353-
(Active, Active, Frozen | Disabled) => true,
333+
(Active, Active) => true,
354334
// And knowing where it became Frozen is also important.
355-
(Frozen, Frozen, Disabled) => true,
335+
(Frozen, Frozen) => true,
356336
// If the error is a transition `Frozen -> Disabled`, then we don't really
357337
// care whether before that was `Reserved -> Active -> Frozen` or
358338
// `Reserved -> Frozen` or even `Frozen` directly.
359339
// The error will only show either
360340
// - created as Frozen, then Frozen -> Disabled is forbidden
361341
// - created as Reserved, later became Frozen, then Frozen -> Disabled is forbidden
362342
// In both cases the `Reserved -> Active` part is inexistant or irrelevant.
363-
(Active, Frozen, Disabled) => false,
343+
(Active, Frozen) => false,
364344

365-
// `Reserved -> Frozen` does not trigger protectors.
366-
(_, Reserved { .. }, Frozen) =>
367-
unreachable!("this transition cannot cause an error"),
345+
(_, Disabled) =>
346+
unreachable!(
347+
"permission that results in Disabled should not itself be Disabled in the first place"
348+
),
368349
// No transition has `Reserved` as its `.to` unless it's a noop.
369-
(Reserved { .. }, _, _) => unreachable!("self is a noop transition"),
370-
(_, Disabled, Disabled) | (_, Frozen, Frozen) | (_, Active, Active) =>
371-
unreachable!("err contains a noop transition"),
350+
(Reserved { .. }, _) => unreachable!("self is a noop transition"),
372351

373352
// Permissions only evolve in the order `Reserved -> Active -> Frozen -> Disabled`,
374353
// so permissions found must be increasing in the order
375354
// `self.from < self.to <= forbidden.from < forbidden.to`.
376-
(Disabled, Reserved { .. } | Active | Frozen, _)
377-
| (Frozen, Reserved { .. } | Active, _)
378-
| (Active, Reserved { .. }, _) =>
355+
(Disabled, Reserved { .. } | Active | Frozen)
356+
| (Frozen, Reserved { .. } | Active)
357+
| (Active, Reserved { .. }) =>
379358
unreachable!("permissions between self and err must be increasing"),
380-
(_, Disabled, Reserved { .. } | Active | Frozen)
381-
| (_, Frozen, Reserved { .. } | Active)
382-
| (_, Active, Reserved { .. }) =>
383-
unreachable!("permissions within err must be increasing"),
384359
}
385360
}
386361
// We don't care because protectors evolve independently from

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -456,9 +456,9 @@ impl<'tcx> Tree {
456456
if protected
457457
// Can't trigger Protector on uninitialized locations
458458
&& old_state.initialized
459-
&& !transition.is_allowed_by_protector()
459+
&& transition.produces_disabled()
460460
{
461-
return Err(TransitionError::ProtectedTransition(transition));
461+
return Err(TransitionError::ProtectedDisabled(old_perm));
462462
}
463463
// Record the event as part of the history
464464
if !transition.is_noop() {

src/tools/miri/tests/fail/both_borrows/aliasing_mut4.tree.stderr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@ LL | ptr::write(dest, src);
66
|
77
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
88
= help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
9-
= help: this foreign write access would cause the protected tag <TAG> to transition from Frozen to Disabled
10-
= help: this transition would be a loss of read permissions, which is not allowed for protected tags
9+
= help: this foreign write access would cause the protected tag <TAG> currently Frozen to become Disabled
10+
= help: protected tags must not become Disabled
1111
help: the accessed tag <TAG> was created here
1212
--> $DIR/aliasing_mut4.rs:LL:CC
1313
|

src/tools/miri/tests/fail/both_borrows/box_noalias_violation.tree.stderr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@ LL | *y
66
|
77
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
88
= help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
9-
= help: this foreign read access would cause the protected tag <TAG> to transition from Active to Frozen
10-
= help: this transition would be a loss of write permissions, which is not allowed for protected tags
9+
= help: this foreign read access would cause the protected tag <TAG> currently Active to become Disabled
10+
= help: protected tags must not become Disabled
1111
help: the accessed tag <TAG> was created here
1212
--> $DIR/box_noalias_violation.rs:LL:CC
1313
|

src/tools/miri/tests/fail/both_borrows/illegal_write6.tree.stderr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@ LL | unsafe { *y = 2 };
66
|
77
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
88
= help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
9-
= help: this foreign write access would cause the protected tag <TAG> to transition from Active to Disabled
10-
= help: this transition would be a loss of read and write permissions, which is not allowed for protected tags
9+
= help: this foreign write access would cause the protected tag <TAG> currently Active to become Disabled
10+
= help: protected tags must not become Disabled
1111
help: the accessed tag <TAG> was created here
1212
--> $DIR/illegal_write6.rs:LL:CC
1313
|

src/tools/miri/tests/fail/both_borrows/invalidate_against_protector2.tree.stderr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@ LL | unsafe { *x = 0 };
66
|
77
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
88
= help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
9-
= help: this foreign write access would cause the protected tag <TAG> to transition from Frozen to Disabled
10-
= help: this transition would be a loss of read permissions, which is not allowed for protected tags
9+
= help: this foreign write access would cause the protected tag <TAG> currently Frozen to become Disabled
10+
= help: protected tags must not become Disabled
1111
help: the accessed tag <TAG> was created here
1212
--> $DIR/invalidate_against_protector2.rs:LL:CC
1313
|

src/tools/miri/tests/fail/both_borrows/invalidate_against_protector3.tree.stderr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@ LL | unsafe { *x = 0 };
66
|
77
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
88
= help: the accessed tag <TAG> (root of the allocation) is foreign to the protected tag <TAG> (i.e., it is not a child)
9-
= help: this foreign write access would cause the protected tag <TAG> to transition from Frozen to Disabled
10-
= help: this transition would be a loss of read permissions, which is not allowed for protected tags
9+
= help: this foreign write access would cause the protected tag <TAG> currently Frozen to become Disabled
10+
= help: protected tags must not become Disabled
1111
help: the accessed tag <TAG> was created here
1212
--> $DIR/invalidate_against_protector3.rs:LL:CC
1313
|

src/tools/miri/tests/fail/both_borrows/newtype_pair_retagging.tree.stderr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@ LL | unsafe { __rust_dealloc(ptr, layout.size(), layout.align()) }
66
|
77
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
88
= help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
9-
= help: this deallocation (acting as a foreign write access) would cause the protected tag <TAG> to transition from Frozen to Disabled
10-
= help: this transition would be a loss of read permissions, which is not allowed for protected tags
9+
= help: this deallocation (acting as a foreign write access) would cause the protected tag <TAG> currently Frozen to become Disabled
10+
= help: protected tags must not become Disabled
1111
help: the accessed tag <TAG> was created here
1212
--> $DIR/newtype_pair_retagging.rs:LL:CC
1313
|

src/tools/miri/tests/fail/both_borrows/newtype_retagging.tree.stderr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@ LL | unsafe { __rust_dealloc(ptr, layout.size(), layout.align()) }
66
|
77
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
88
= help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
9-
= help: this deallocation (acting as a foreign write access) would cause the protected tag <TAG> to transition from Frozen to Disabled
10-
= help: this transition would be a loss of read permissions, which is not allowed for protected tags
9+
= help: this deallocation (acting as a foreign write access) would cause the protected tag <TAG> currently Frozen to become Disabled
10+
= help: protected tags must not become Disabled
1111
help: the accessed tag <TAG> was created here
1212
--> $DIR/newtype_retagging.rs:LL:CC
1313
|

src/tools/miri/tests/fail/function_calls/arg_inplace_mutate.tree.stderr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@ LL | unsafe { ptr.write(S(0)) };
66
|
77
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
88
= help: the accessed tag <TAG> (root of the allocation) is foreign to the protected tag <TAG> (i.e., it is not a child)
9-
= help: this foreign write access would cause the protected tag <TAG> to transition from Active to Disabled
10-
= help: this transition would be a loss of read and write permissions, which is not allowed for protected tags
9+
= help: this foreign write access would cause the protected tag <TAG> currently Active to become Disabled
10+
= help: protected tags must not become Disabled
1111
help: the accessed tag <TAG> was created here
1212
--> $DIR/arg_inplace_mutate.rs:LL:CC
1313
|

src/tools/miri/tests/fail/function_calls/arg_inplace_observe_during.tree.stderr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@ LL | unsafe { ptr.read() };
66
|
77
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
88
= help: the accessed tag <TAG> (root of the allocation) is foreign to the protected tag <TAG> (i.e., it is not a child)
9-
= help: this foreign read access would cause the protected tag <TAG> to transition from Active to Frozen
10-
= help: this transition would be a loss of write permissions, which is not allowed for protected tags
9+
= help: this foreign read access would cause the protected tag <TAG> currently Active to become Disabled
10+
= help: protected tags must not become Disabled
1111
help: the accessed tag <TAG> was created here
1212
--> $DIR/arg_inplace_observe_during.rs:LL:CC
1313
|

src/tools/miri/tests/fail/function_calls/return_pointer_aliasing.tree.stderr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@ LL | unsafe { ptr.read() };
66
|
77
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
88
= help: the accessed tag <TAG> (root of the allocation) is foreign to the protected tag <TAG> (i.e., it is not a child)
9-
= help: this foreign read access would cause the protected tag <TAG> to transition from Active to Frozen
10-
= help: this transition would be a loss of write permissions, which is not allowed for protected tags
9+
= help: this foreign read access would cause the protected tag <TAG> currently Active to become Disabled
10+
= help: protected tags must not become Disabled
1111
help: the accessed tag <TAG> was created here
1212
--> $DIR/return_pointer_aliasing.rs:LL:CC
1313
|

src/tools/miri/tests/fail/tree_borrows/outside-range.stderr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@ LL | *y.add(3) = 42;
66
|
77
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
88
= help: the accessed tag <TAG> is foreign to the protected tag <TAG> (i.e., it is not a child)
9-
= help: this foreign write access would cause the protected tag <TAG> to transition from Reserved to Disabled
10-
= help: this transition would be a loss of read and write permissions, which is not allowed for protected tags
9+
= help: this foreign write access would cause the protected tag <TAG> currently Reserved to become Disabled
10+
= help: protected tags must not become Disabled
1111
help: the accessed tag <TAG> was created here
1212
--> $DIR/outside-range.rs:LL:CC
1313
|

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,8 @@ LL | *y = 1;
1616
|
1717
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
1818
= help: the accessed tag <TAG> (y, callee:y, caller:y) is foreign to the protected tag <TAG> (callee:x) (i.e., it is not a child)
19-
= help: this foreign write access would cause the protected tag <TAG> (callee:x) to transition from Reserved to Disabled
20-
= help: this transition would be a loss of read and write permissions, which is not allowed for protected tags
19+
= help: this foreign write access would cause the protected tag <TAG> (callee:x) currently Reserved to become Disabled
20+
= help: protected tags must not become Disabled
2121
help: the accessed tag <TAG> was created here
2222
--> $DIR/cell-protected-write.rs:LL:CC
2323
|

0 commit comments

Comments
 (0)