Skip to content

Commit

Permalink
pthread_mutex: store mutex ID outside adressable memory, so it can be…
Browse files Browse the repository at this point in the history
… trusted
  • Loading branch information
RalfJung committed Oct 14, 2024
1 parent bd8f2af commit 89323bf
Show file tree
Hide file tree
Showing 7 changed files with 181 additions and 127 deletions.
16 changes: 5 additions & 11 deletions src/tools/miri/src/concurrency/sync.rs
Original file line number Diff line number Diff line change
Expand Up @@ -167,8 +167,10 @@ pub struct SynchronizationObjects {
mutexes: IndexVec<MutexId, Mutex>,
rwlocks: IndexVec<RwLockId, RwLock>,
condvars: IndexVec<CondvarId, Condvar>,
futexes: FxHashMap<u64, Futex>,
pub(super) init_onces: IndexVec<InitOnceId, InitOnce>,

/// Futex info for the futex at the given address.
futexes: FxHashMap<u64, Futex>,
}

// Private extension trait for local helper methods
Expand Down Expand Up @@ -277,17 +279,9 @@ pub(super) trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
/// Eagerly create and initialize a new mutex.
fn mutex_create(
&mut self,
lock: &MPlaceTy<'tcx>,
offset: u64,
data: Option<Box<dyn Any>>,
) -> InterpResult<'tcx, MutexId> {
fn mutex_create(&mut self) -> MutexId {
let this = self.eval_context_mut();
this.create_id(lock, offset, |ecx| &mut ecx.machine.sync.mutexes, Mutex {
data,
..Default::default()
})
this.machine.sync.mutexes.push(Default::default())
}

/// Lazily create a new mutex.
Expand Down
7 changes: 3 additions & 4 deletions src/tools/miri/src/helpers.rs
Original file line number Diff line number Diff line change
Expand Up @@ -223,14 +223,13 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
}

/// Evaluates the scalar at the specified path.
fn eval_path(&self, path: &[&str]) -> OpTy<'tcx> {
fn eval_path(&self, path: &[&str]) -> MPlaceTy<'tcx> {
let this = self.eval_context_ref();
let instance = resolve_path(*this.tcx, path, Namespace::ValueNS);
// We don't give a span -- this isn't actually used directly by the program anyway.
let const_val = this.eval_global(instance).unwrap_or_else(|err| {
this.eval_global(instance).unwrap_or_else(|err| {
panic!("failed to evaluate required Rust item: {path:?}\n{err:?}")
});
const_val.into()
})
}
fn eval_path_scalar(&self, path: &[&str]) -> Scalar {
let this = self.eval_context_ref();
Expand Down
16 changes: 14 additions & 2 deletions src/tools/miri/src/machine.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
//! Global machine state as well as implementation of the interpreter engine
//! `Machine` trait.

use std::any::Any;
use std::borrow::Cow;
use std::cell::RefCell;
use std::collections::hash_map::Entry;
Expand Down Expand Up @@ -336,6 +337,11 @@ pub struct AllocExtra<'tcx> {
/// if this allocation is leakable. The backtrace is not
/// pruned yet; that should be done before printing it.
pub backtrace: Option<Vec<FrameInfo<'tcx>>>,
/// Synchronization primitives like to attach extra data to particular addresses. We store that
/// inside the relevant allocation, to ensure that everything is removed when the allocation is
/// freed.
/// This maps offsets to synchronization-primitive-specific data.
pub sync: FxHashMap<Size, Box<dyn Any>>,
}

// We need a `Clone` impl because the machine passes `Allocation` through `Cow`...
Expand All @@ -348,7 +354,7 @@ impl<'tcx> Clone for AllocExtra<'tcx> {

impl VisitProvenance for AllocExtra<'_> {
fn visit_provenance(&self, visit: &mut VisitWith<'_>) {
let AllocExtra { borrow_tracker, data_race, weak_memory, backtrace: _ } = self;
let AllocExtra { borrow_tracker, data_race, weak_memory, backtrace: _, sync: _ } = self;

borrow_tracker.visit_provenance(visit);
data_race.visit_provenance(visit);
Expand Down Expand Up @@ -1187,7 +1193,13 @@ impl<'tcx> Machine<'tcx> for MiriMachine<'tcx> {
.insert(id, (ecx.machine.current_span(), None));
}

interp_ok(AllocExtra { borrow_tracker, data_race, weak_memory, backtrace })
interp_ok(AllocExtra {
borrow_tracker,
data_race,
weak_memory,
backtrace,
sync: FxHashMap::default(),
})
}

fn adjust_alloc_root_pointer(
Expand Down
Loading

0 comments on commit 89323bf

Please sign in to comment.