Skip to content

Commit

Permalink
Auto merge of #3067 - Vanille-N:spurious-incremental, r=RalfJung
Browse files Browse the repository at this point in the history
Continuation of #3054: enable spurious reads in TB

The last additions to the test suite of TB left some unresolved `#[should_panic]` that these new modifications solve.

## Problem

Recall that the issues were arising from the interleavings that follow.

### A. `Reserved -> Frozen` has visible effects after function exit

The transition `Reserved -> Frozen` irreversibly blocks write accesses to the tag, so in the interleaving below `y` initially `Reserved` becomes `Frozen` only in the target where a spurious read through `x` is inserted. This makes the later write through `y` UB only in the target and not in the source.
```
1: retag x (&, protect)
2: retag y (&mut, protect)
1: spurious read x
1: ret x
2: ret y
2: write y
```

### B. Protectors only announce their presence on retag

There is a read-on-reborrow for protected locations, but if the retag of `x` occurs before that of `y` and there is no explicit access through `x`, then `y` is unaware of the existence of `x`. This is problematic because a spurious read inserted through `x` between the retag of `y` and the return of the function protecting `x` is a noalias violation in the target without UB in the source.
```
1: retag x (&, protect)
2: retag y (&mut, protect)
1: spurious read x
1: ret x
2: write y
2: ret y
```

## Step 1: Finer behavior for `Reserved`

Since one problem is that `Reserved -> Frozen` has consequences beyond function exit, we decide to remove this transition entirely. To replace it we introduce a new subtype of `Reserved` with the extra boolean `aliased` set.
`Reserved { aliased: true }` forbids child accesses, but only temporarily: it has no effect on activation once the tag is no longer protected.
This makes the semantics of Tree Borrows slightly weaker in favor of being more similar to noalias.

This solves interleaving **A.**, but **B.** is still a problem and the exhaustive tests do not pass yet.

## Step 2: Read on function exit

Protected tags issue a "reminder" that they are protected until this instant inclusive, in the form of an implicit read (symmetrically to the implicit read on retag). This ensures that if the periods on which two tags `x` and `y` are protected overlap then no matter the interleaving of retags and returns, there is either a protector currently active or a read that has been emitted, both of which temporarily block activation.

This makes the exhaustive test designed previously pass, but it has an effect on the ability to return an activated pointer that I had not foreseen before implementing it.

## Step 2': Do not propagate to children

A naive implementation of **Step 2** makes the following code UB:
```rs
fn reborrow(x: &mut u8) -> &mut u8 {
    let y = &mut *x;
    *y = *y;
    y // callee returns `y: Active`...
}

let x = &mut 0u8;
let y = reborrow(x); // ... and caller receives `y: Frozen`
*y = 1; // UB
```
This is unacceptable, and a simple fix is to make this implicit read visible only to foreign tags.

We still lack hindsight on the ramifications of this decision, and the fact that the problematic pattern was only discovered because it occured in one completely unrelated test (with a cryptic error message) is worrying. We should be vigilant as to how this interacts with the rest of the model.

## TODO

As of commit #281c30, the data race model has not been fully updated.
We have removed the reborrow of mutable references counting as a write access, but we still need the implicit read of function exit to count as a read.
  • Loading branch information
bors committed Oct 6, 2023
2 parents 370a961 + f95bcbb commit 4e4426b
Show file tree
Hide file tree
Showing 37 changed files with 1,097 additions and 481 deletions.
20 changes: 18 additions & 2 deletions src/borrow_tracker/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -66,10 +66,13 @@ pub struct FrameState {
/// `stacked_borrows::GlobalState` upon function return, and if we attempt to pop a protected
/// tag, to identify which call is responsible for protecting the tag.
/// See `Stack::item_popped` for more explanation.
/// Tree Borrows also needs to know which allocation these tags
/// belong to so that it can perform a read through them immediately before
/// the frame gets popped.
///
/// This will contain one tag per reference passed to the function, so
/// a size of 2 is enough for the vast majority of functions.
pub protected_tags: SmallVec<[BorTag; 2]>,
pub protected_tags: SmallVec<[(AllocId, BorTag); 2]>,
}

impl VisitTags for FrameState {
Expand Down Expand Up @@ -208,7 +211,7 @@ impl GlobalStateInner {
}

pub fn end_call(&mut self, frame: &machine::FrameExtra<'_>) {
for tag in &frame
for (_, tag) in &frame
.borrow_tracker
.as_ref()
.expect("we should have borrow tracking data")
Expand Down Expand Up @@ -453,6 +456,19 @@ impl AllocState {
AllocState::TreeBorrows(tb) => tb.borrow_mut().remove_unreachable_tags(tags),
}
}

/// Tree Borrows needs to be told when a tag stops being protected.
pub fn release_protector<'tcx>(
&self,
machine: &MiriMachine<'_, 'tcx>,
global: &GlobalState,
tag: BorTag,
) -> InterpResult<'tcx> {
match self {
AllocState::StackedBorrows(_sb) => Ok(()),
AllocState::TreeBorrows(tb) => tb.borrow_mut().release_protector(machine, global, tag),
}
}
}

impl VisitTags for AllocState {
Expand Down
3 changes: 2 additions & 1 deletion src/borrow_tracker/stacked_borrows/diagnostics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -436,6 +436,7 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
ProtectorKind::WeakProtector => "weakly protected",
ProtectorKind::StrongProtector => "strongly protected",
};
let item_tag = item.tag();
let call_id = self
.machine
.threads
Expand All @@ -444,7 +445,7 @@ impl<'history, 'ecx, 'mir, 'tcx> DiagnosticCx<'history, 'ecx, 'mir, 'tcx> {
.map(|frame| {
frame.extra.borrow_tracker.as_ref().expect("we should have borrow tracking data")
})
.find(|frame| frame.protected_tags.contains(&item.tag()))
.find(|frame| frame.protected_tags.iter().any(|(_, tag)| tag == &item_tag))
.map(|frame| frame.call_id)
.unwrap(); // FIXME: Surely we should find something, but a panic seems wrong here?
match self.operation {
Expand Down
8 changes: 7 additions & 1 deletion src/borrow_tracker/stacked_borrows/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -719,7 +719,13 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'

if let Some(protect) = new_perm.protector() {
// See comment in `Stack::item_invalidated` for why we store the tag twice.
this.frame_mut().extra.borrow_tracker.as_mut().unwrap().protected_tags.push(new_tag);
this.frame_mut()
.extra
.borrow_tracker
.as_mut()
.unwrap()
.protected_tags
.push((alloc_id, new_tag));
this.machine
.borrow_tracker
.as_mut()
Expand Down
21 changes: 18 additions & 3 deletions src/borrow_tracker/tree_borrows/diagnostics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ pub enum AccessCause {
Explicit(AccessKind),
Reborrow,
Dealloc,
FnExit,
}

impl fmt::Display for AccessCause {
Expand All @@ -27,6 +28,7 @@ impl fmt::Display for AccessCause {
Self::Explicit(kind) => write!(f, "{kind}"),
Self::Reborrow => write!(f, "reborrow"),
Self::Dealloc => write!(f, "deallocation"),
Self::FnExit => write!(f, "protector release"),
}
}
}
Expand All @@ -38,6 +40,7 @@ impl AccessCause {
Self::Explicit(kind) => format!("{rel} {kind}"),
Self::Reborrow => format!("reborrow (acting as a {rel} read access)"),
Self::Dealloc => format!("deallocation (acting as a {rel} write access)"),
Self::FnExit => format!("protector release (acting as a {rel} read access)"),
}
}
}
Expand All @@ -52,7 +55,9 @@ pub struct Event {
/// Relative position of the tag to the one used for the access.
pub is_foreign: bool,
/// User-visible range of the access.
pub access_range: AllocRange,
/// `None` means that this is an implicit access to the entire allocation
/// (used for the implicit read on protector release).
pub access_range: Option<AllocRange>,
/// The transition recorded by this event only occured on a subrange of
/// `access_range`: a single access on `access_range` triggers several events,
/// each with their own mutually disjoint `transition_range`. No-op transitions
Expand Down Expand Up @@ -123,7 +128,17 @@ impl HistoryData {
// NOTE: `transition_range` is explicitly absent from the error message, it has no significance
// to the user. The meaningful one is `access_range`.
let access = access_cause.print_as_access(is_foreign);
self.events.push((Some(span.data()), format!("{this} later transitioned to {endpoint} due to a {access} at offsets {access_range:?}", endpoint = transition.endpoint())));
let access_range_text = match access_range {
Some(r) => format!("at offsets {r:?}"),
None => format!("on every location previously accessed by this tag"),
};
self.events.push((
Some(span.data()),
format!(
"{this} later transitioned to {endpoint} due to a {access} {access_range_text}",
endpoint = transition.endpoint()
),
));
self.events
.push((None, format!("this transition corresponds to {}", transition.summary())));
}
Expand Down Expand Up @@ -745,7 +760,7 @@ const DEFAULT_FORMATTER: DisplayFmt = DisplayFmt {
bot: '─',
warning_text: "Warning: this tree is indicative only. Some tags may have been hidden.",
},
perm: DisplayFmtPermission { open: "|", sep: "|", close: "|", uninit: "---", range_sep: ".." },
perm: DisplayFmtPermission { open: "|", sep: "|", close: "|", uninit: "----", range_sep: ".." },
padding: DisplayFmtPadding {
join_middle: "├",
join_last: "└",
Expand Down
57 changes: 37 additions & 20 deletions src/borrow_tracker/tree_borrows/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,9 @@ use log::trace;

use rustc_target::abi::{Abi, Align, Size};

use crate::borrow_tracker::{AccessKind, GlobalStateInner, ProtectorKind, RetagFields};
use crate::borrow_tracker::{
AccessKind, GlobalState, GlobalStateInner, ProtectorKind, RetagFields,
};
use rustc_middle::{
mir::{Mutability, RetagKind},
ty::{
Expand Down Expand Up @@ -70,7 +72,7 @@ impl<'tcx> Tree {
self.perform_access(
access_kind,
tag,
range,
Some(range),
global,
span,
diagnostics::AccessCause::Explicit(access_kind),
Expand Down Expand Up @@ -99,6 +101,29 @@ impl<'tcx> Tree {
pub fn expose_tag(&mut self, _tag: BorTag) {
// TODO
}

/// A tag just lost its protector.
///
/// This emits a special kind of access that is only applied
/// to initialized locations, as a protection against other
/// tags not having been made aware of the existence of this
/// protector.
pub fn release_protector(
&mut self,
machine: &MiriMachine<'_, 'tcx>,
global: &GlobalState,
tag: BorTag,
) -> InterpResult<'tcx> {
let span = machine.current_span();
self.perform_access(
AccessKind::Read,
tag,
None, // no specified range because it occurs on the entire allocation
global,
span,
diagnostics::AccessCause::FnExit,
)
}
}

/// Policy for a new borrow.
Expand Down Expand Up @@ -248,7 +273,13 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
// We register the protection in two different places.
// This makes creating a protector slower, but checking whether a tag
// is protected faster.
this.frame_mut().extra.borrow_tracker.as_mut().unwrap().protected_tags.push(new_tag);
this.frame_mut()
.extra
.borrow_tracker
.as_mut()
.unwrap()
.protected_tags
.push((alloc_id, new_tag));
this.machine
.borrow_tracker
.as_mut()
Expand All @@ -275,7 +306,7 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
tree_borrows.perform_access(
AccessKind::Read,
orig_tag,
range,
Some(range),
this.machine.borrow_tracker.as_ref().unwrap(),
this.machine.current_span(),
diagnostics::AccessCause::Reborrow,
Expand All @@ -287,21 +318,7 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
// Also inform the data race model (but only if any bytes are actually affected).
if range.size.bytes() > 0 {
if let Some(data_race) = alloc_extra.data_race.as_ref() {
// We sometimes need to make it a write, since not all retags commute with reads!
// FIXME: Is that truly the semantics we want? Some optimizations are likely to be
// very unhappy without this. We'd tsill ge some UB just by picking a suitable
// interleaving, but wether UB happens can depend on whether a write occurs in the
// future...
let is_write = new_perm.initial_state.is_active()
|| (new_perm.initial_state.is_reserved(None) && new_perm.protector.is_some());
if is_write {
// Need to get mutable access to alloc_extra.
// (Cannot always do this as we can do read-only reborrowing on read-only allocations.)
let (alloc_extra, machine) = this.get_alloc_extra_mut(alloc_id)?;
alloc_extra.data_race.as_mut().unwrap().write(alloc_id, range, machine)?;
} else {
data_race.read(alloc_id, range, &this.machine)?;
}
data_race.read(alloc_id, range, &this.machine)?;
}
}

Expand Down Expand Up @@ -532,7 +549,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
// if converting this alloc_id from a global to a local one
// uncovers a non-supported `extern static`.
let alloc_extra = this.get_alloc_extra(alloc_id)?;
trace!("Stacked Borrows tag {tag:?} exposed in {alloc_id:?}");
trace!("Tree Borrows tag {tag:?} exposed in {alloc_id:?}");
alloc_extra.borrow_tracker_tb().borrow_mut().expose_tag(tag);
}
AllocKind::Function | AllocKind::VTable | AllocKind::Dead => {
Expand Down

0 comments on commit 4e4426b

Please sign in to comment.