Skip to content

Commit cd954db

Browse files
committed
TB: public interface to permissions
1 parent 3628637 commit cd954db

File tree

1 file changed

+93
-0
lines changed
  • src/tools/miri/src/borrow_tracker/tree_borrows

1 file changed

+93
-0
lines changed

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

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
use std::cmp::{Ordering, PartialOrd};
22
use std::fmt;
33

4+
use crate::borrow_tracker::tree_borrows::tree::AccessRelatedness;
5+
use crate::borrow_tracker::AccessKind;
6+
47
/// The activation states of a pointer
58
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
69
enum PermissionPriv {
@@ -92,6 +95,21 @@ mod transition {
9295
_ => Disabled,
9396
})
9497
}
98+
99+
/// Dispatch handler depending on the kind of access and its position.
100+
pub(super) fn perform_access(
101+
kind: AccessKind,
102+
rel_pos: AccessRelatedness,
103+
child: PermissionPriv,
104+
protected: bool,
105+
) -> Option<PermissionPriv> {
106+
match (kind, rel_pos.is_foreign()) {
107+
(AccessKind::Write, true) => foreign_write(child, protected),
108+
(AccessKind::Read, true) => foreign_read(child, protected),
109+
(AccessKind::Write, false) => child_write(child, protected),
110+
(AccessKind::Read, false) => child_read(child, protected),
111+
}
112+
}
95113
}
96114

97115
impl PermissionPriv {
@@ -117,6 +135,81 @@ impl PermissionPriv {
117135
}
118136
}
119137

138+
/// Public interface to the state machine that controls read-write permissions.
139+
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
140+
pub struct Permission(PermissionPriv);
141+
142+
impl fmt::Display for Permission {
143+
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
144+
write!(
145+
f,
146+
"{}",
147+
match self.0 {
148+
PermissionPriv::Reserved { .. } => "Reserved",
149+
PermissionPriv::Active => "Active",
150+
PermissionPriv::Frozen => "Frozen",
151+
PermissionPriv::Disabled => "Disabled",
152+
}
153+
)
154+
}
155+
}
156+
157+
impl Permission {
158+
/// Default initial permission of the root of a new tree.
159+
pub fn new_root() -> Self {
160+
Self(Active)
161+
}
162+
163+
/// Default initial permission of a reborrowed mutable reference.
164+
pub fn new_unique_2phase(ty_is_freeze: bool) -> Self {
165+
Self(Reserved { ty_is_freeze })
166+
}
167+
168+
/// Default initial permission of a reborrowed shared reference
169+
pub fn new_frozen() -> Self {
170+
Self(Frozen)
171+
}
172+
173+
/// Pretty-printing. Needs to be here and not in diagnostics.rs
174+
/// because `Self` is private.
175+
pub fn short_name(self) -> &'static str {
176+
// Make sure there are all of the same length as each other
177+
// and also as `diagnostics::DisplayFmtPermission.uninit` otherwise
178+
// alignment will be incorrect.
179+
match self.0 {
180+
Reserved { ty_is_freeze: true } => "Res",
181+
Reserved { ty_is_freeze: false } => "Re*",
182+
Active => "Act",
183+
Frozen => "Frz",
184+
Disabled => "Dis",
185+
}
186+
}
187+
188+
/// Check that there are no complaints from a possible protector.
189+
///
190+
/// Note: this is not in charge of checking that there *is* a protector,
191+
/// it should be used as
192+
/// ```
193+
/// let no_protector_error = if is_protected(tag) {
194+
/// old_perm.protector_allows_transition(new_perm)
195+
/// };
196+
/// ```
197+
pub fn protector_allows_transition(self, new: Self) -> bool {
198+
self.0.protector_allows_transition(new.0)
199+
}
200+
201+
/// Apply the transition to the inner PermissionPriv.
202+
pub fn perform_access(
203+
kind: AccessKind,
204+
rel_pos: AccessRelatedness,
205+
old_perm: Self,
206+
protected: bool,
207+
) -> Option<Self> {
208+
let old_state = old_perm.0;
209+
transition::perform_access(kind, rel_pos, old_state, protected).map(Self)
210+
}
211+
}
212+
120213
#[cfg(test)]
121214
mod propagation_optimization_checks {
122215
pub use super::*;

0 commit comments

Comments
 (0)