slightly adjust and synchronize Machine passing for SB and DataRace
This commit is contained in:
Ralf Jung
parent
f479404b12
commit
a7f72218c8
@ -838,18 +838,18 @@ impl VClockAlloc {
|
||||
&self,
|
||||
alloc_id: AllocId,
|
||||
range: AllocRange,
|
||||
global: &GlobalState,
|
||||
thread_mgr: &ThreadManager<'_, '_>,
|
||||
machine: &MiriMachine<'_, '_>,
|
||||
) -> InterpResult<'tcx> {
|
||||
let global = machine.data_race.as_ref().unwrap();
|
||||
if global.race_detecting() {
|
||||
let (index, clocks) = global.current_thread_state(thread_mgr);
|
||||
let (index, clocks) = global.current_thread_state(&machine.threads);
|
||||
let mut alloc_ranges = self.alloc_ranges.borrow_mut();
|
||||
for (offset, range) in alloc_ranges.iter_mut(range.start, range.size) {
|
||||
if let Err(DataRace) = range.read_race_detect(&clocks, index) {
|
||||
// Report data-race.
|
||||
return Self::report_data_race(
|
||||
global,
|
||||
thread_mgr,
|
||||
&machine.threads,
|
||||
range,
|
||||
"Read",
|
||||
false,
|
||||
@ -869,17 +869,17 @@ impl VClockAlloc {
|
||||
alloc_id: AllocId,
|
||||
range: AllocRange,
|
||||
write_type: WriteType,
|
||||
global: &mut GlobalState,
|
||||
thread_mgr: &ThreadManager<'_, '_>,
|
||||
machine: &mut MiriMachine<'_, '_>,
|
||||
) -> InterpResult<'tcx> {
|
||||
let global = machine.data_race.as_mut().unwrap();
|
||||
if global.race_detecting() {
|
||||
let (index, clocks) = global.current_thread_state(thread_mgr);
|
||||
let (index, clocks) = global.current_thread_state(&machine.threads);
|
||||
for (offset, range) in self.alloc_ranges.get_mut().iter_mut(range.start, range.size) {
|
||||
if let Err(DataRace) = range.write_race_detect(&clocks, index, write_type) {
|
||||
// Report data-race
|
||||
return Self::report_data_race(
|
||||
global,
|
||||
thread_mgr,
|
||||
&machine.threads,
|
||||
range,
|
||||
write_type.get_descriptor(),
|
||||
false,
|
||||
@ -901,10 +901,9 @@ impl VClockAlloc {
|
||||
&mut self,
|
||||
alloc_id: AllocId,
|
||||
range: AllocRange,
|
||||
global: &mut GlobalState,
|
||||
thread_mgr: &ThreadManager<'_, '_>,
|
||||
machine: &mut MiriMachine<'_, '_>,
|
||||
) -> InterpResult<'tcx> {
|
||||
self.unique_access(alloc_id, range, WriteType::Write, global, thread_mgr)
|
||||
self.unique_access(alloc_id, range, WriteType::Write, machine)
|
||||
}
|
||||
|
||||
/// Detect data-races for an unsynchronized deallocate operation, will not perform
|
||||
@ -915,10 +914,9 @@ impl VClockAlloc {
|
||||
&mut self,
|
||||
alloc_id: AllocId,
|
||||
range: AllocRange,
|
||||
global: &mut GlobalState,
|
||||
thread_mgr: &ThreadManager<'_, '_>,
|
||||
machine: &mut MiriMachine<'_, '_>,
|
||||
) -> InterpResult<'tcx> {
|
||||
self.unique_access(alloc_id, range, WriteType::Deallocate, global, thread_mgr)
|
||||
self.unique_access(alloc_id, range, WriteType::Deallocate, machine)
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@ -1003,21 +1003,12 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for MiriMachine<'mir, 'tcx> {
|
||||
range: AllocRange,
|
||||
) -> InterpResult<'tcx> {
|
||||
if let Some(data_race) = &alloc_extra.data_race {
|
||||
data_race.read(
|
||||
alloc_id,
|
||||
range,
|
||||
machine.data_race.as_ref().unwrap(),
|
||||
&machine.threads,
|
||||
)?;
|
||||
data_race.read(alloc_id, range, machine)?;
|
||||
}
|
||||
if let Some(stacked_borrows) = &alloc_extra.stacked_borrows {
|
||||
stacked_borrows.borrow_mut().before_memory_read(
|
||||
alloc_id,
|
||||
prov_extra,
|
||||
range,
|
||||
machine.stacked_borrows.as_ref().unwrap(),
|
||||
machine,
|
||||
)?;
|
||||
stacked_borrows
|
||||
.borrow_mut()
|
||||
.before_memory_read(alloc_id, prov_extra, range, machine)?;
|
||||
}
|
||||
if let Some(weak_memory) = &alloc_extra.weak_memory {
|
||||
weak_memory.memory_accessed(range, machine.data_race.as_ref().unwrap());
|
||||
@ -1034,21 +1025,10 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for MiriMachine<'mir, 'tcx> {
|
||||
range: AllocRange,
|
||||
) -> InterpResult<'tcx> {
|
||||
if let Some(data_race) = &mut alloc_extra.data_race {
|
||||
data_race.write(
|
||||
alloc_id,
|
||||
range,
|
||||
machine.data_race.as_mut().unwrap(),
|
||||
&machine.threads,
|
||||
)?;
|
||||
data_race.write(alloc_id, range, machine)?;
|
||||
}
|
||||
if let Some(stacked_borrows) = &mut alloc_extra.stacked_borrows {
|
||||
stacked_borrows.get_mut().before_memory_write(
|
||||
alloc_id,
|
||||
prov_extra,
|
||||
range,
|
||||
machine.stacked_borrows.as_ref().unwrap(),
|
||||
machine,
|
||||
)?;
|
||||
stacked_borrows.get_mut().before_memory_write(alloc_id, prov_extra, range, machine)?;
|
||||
}
|
||||
if let Some(weak_memory) = &alloc_extra.weak_memory {
|
||||
weak_memory.memory_accessed(range, machine.data_race.as_ref().unwrap());
|
||||
@ -1068,19 +1048,13 @@ impl<'mir, 'tcx> Machine<'mir, 'tcx> for MiriMachine<'mir, 'tcx> {
|
||||
machine.emit_diagnostic(NonHaltingDiagnostic::FreedAlloc(alloc_id));
|
||||
}
|
||||
if let Some(data_race) = &mut alloc_extra.data_race {
|
||||
data_race.deallocate(
|
||||
alloc_id,
|
||||
range,
|
||||
machine.data_race.as_mut().unwrap(),
|
||||
&machine.threads,
|
||||
)?;
|
||||
data_race.deallocate(alloc_id, range, machine)?;
|
||||
}
|
||||
if let Some(stacked_borrows) = &mut alloc_extra.stacked_borrows {
|
||||
stacked_borrows.get_mut().before_memory_deallocation(
|
||||
alloc_id,
|
||||
prove_extra,
|
||||
range,
|
||||
machine.stacked_borrows.as_ref().unwrap(),
|
||||
machine,
|
||||
)
|
||||
} else {
|
||||
|
||||
@ -644,7 +644,6 @@ impl Stacks {
|
||||
alloc_id: AllocId,
|
||||
tag: ProvenanceExtra,
|
||||
range: AllocRange,
|
||||
state: &GlobalState,
|
||||
machine: &'ecx MiriMachine<'mir, 'tcx>,
|
||||
) -> InterpResult<'tcx>
|
||||
where
|
||||
@ -657,7 +656,7 @@ impl Stacks {
|
||||
range.size.bytes()
|
||||
);
|
||||
let dcx = DiagnosticCxBuilder::read(machine, tag, range);
|
||||
let state = state.borrow();
|
||||
let state = machine.stacked_borrows.as_ref().unwrap().borrow();
|
||||
self.for_each(range, dcx, |stack, dcx, exposed_tags| {
|
||||
stack.access(AccessKind::Read, tag, &state, dcx, exposed_tags)
|
||||
})
|
||||
@ -669,8 +668,7 @@ impl Stacks {
|
||||
alloc_id: AllocId,
|
||||
tag: ProvenanceExtra,
|
||||
range: AllocRange,
|
||||
state: &GlobalState,
|
||||
machine: &'ecx MiriMachine<'mir, 'tcx>,
|
||||
machine: &'ecx mut MiriMachine<'mir, 'tcx>,
|
||||
) -> InterpResult<'tcx> {
|
||||
trace!(
|
||||
"write access with tag {:?}: {:?}, size {}",
|
||||
@ -679,7 +677,7 @@ impl Stacks {
|
||||
range.size.bytes()
|
||||
);
|
||||
let dcx = DiagnosticCxBuilder::write(machine, tag, range);
|
||||
let state = state.borrow();
|
||||
let state = machine.stacked_borrows.as_ref().unwrap().borrow();
|
||||
self.for_each(range, dcx, |stack, dcx, exposed_tags| {
|
||||
stack.access(AccessKind::Write, tag, &state, dcx, exposed_tags)
|
||||
})
|
||||
@ -691,12 +689,11 @@ impl Stacks {
|
||||
alloc_id: AllocId,
|
||||
tag: ProvenanceExtra,
|
||||
range: AllocRange,
|
||||
state: &GlobalState,
|
||||
machine: &'ecx MiriMachine<'mir, 'tcx>,
|
||||
machine: &'ecx mut MiriMachine<'mir, 'tcx>,
|
||||
) -> InterpResult<'tcx> {
|
||||
trace!("deallocation with tag {:?}: {:?}, size {}", tag, alloc_id, range.size.bytes());
|
||||
let dcx = DiagnosticCxBuilder::dealloc(machine, tag);
|
||||
let state = state.borrow();
|
||||
let state = machine.stacked_borrows.as_ref().unwrap().borrow();
|
||||
self.for_each(range, dcx, |stack, dcx, exposed_tags| {
|
||||
stack.dealloc(tag, &state, dcx, exposed_tags)
|
||||
})?;
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user