Skip to content

Commit 85fd3f8

Browse files
authored
Merge pull request #297 from RalfJung/mir-validate
Validation update
2 parents 65a3131 + 8e8c9c8 commit 85fd3f8

20 files changed

+412
-117
lines changed

.travis.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ script:
1616
- |
1717
# Test plain miri
1818
cargo build --release --features "cargo_miri" &&
19-
cargo test --release &&
19+
cargo test --release --all &&
2020
cargo install --features "cargo_miri"
2121
- |
2222
# Test cargo miri

src/librustc_mir/Cargo.toml

-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@ version = "0.1.0"
88
workspace = "../.."
99

1010
[lib]
11-
test = false
1211
path = "lib.rs"
1312

1413
[dependencies]

src/librustc_mir/interpret/memory.rs

+46-57
Original file line numberDiff line numberDiff line change
@@ -29,19 +29,14 @@ pub enum AccessKind {
2929
/// Information about a lock that is currently held.
3030
#[derive(Clone, Debug)]
3131
struct LockInfo {
32-
suspended: Vec<SuspendedWriteLock>,
32+
/// Stores for which lifetimes (of the original write lock) we got
33+
/// which suspensions.
34+
suspended: HashMap<DynamicLifetime, Vec<CodeExtent>>,
35+
/// The current state of the lock that's actually effective.
3336
active: Lock,
3437
}
3538

36-
#[derive(Clone, Debug)]
37-
struct SuspendedWriteLock {
38-
/// Original lifetime of the lock that is now suspended
39-
lft: DynamicLifetime,
40-
/// Regions that all have to end to reenable this suspension
41-
suspensions: Vec<CodeExtent>,
42-
}
43-
44-
#[derive(Clone, Debug)]
39+
#[derive(Clone, Debug, PartialEq)]
4540
pub enum Lock {
4641
NoLock,
4742
WriteLock(DynamicLifetime),
@@ -57,7 +52,7 @@ impl Default for LockInfo {
5752

5853
impl LockInfo {
5954
fn new(lock: Lock) -> LockInfo {
60-
LockInfo { suspended: Vec::new(), active: lock }
55+
LockInfo { suspended: HashMap::new(), active: lock }
6156
}
6257

6358
fn access_permitted(&self, frame: Option<usize>, access: AccessKind) -> bool {
@@ -513,17 +508,17 @@ impl<'a, 'tcx, M: Machine<'tcx>> Memory<'a, 'tcx, M> {
513508
}
514509

515510
/// Release or suspend a write lock of the given lifetime prematurely.
516-
/// When releasing, if there is no write lock or someone else's write lock, that's an error.
511+
/// When releasing, if there is a read lock or someone else's write lock, that's an error.
512+
/// We *do* accept relasing a NoLock, as this can happen when a local is first acquired and later force_allocate'd.
517513
/// When suspending, the same cases are fine; we just register an additional suspension.
518-
pub(crate) fn release_write_lock(&mut self, ptr: MemoryPointer, len: u64,
514+
pub(crate) fn suspend_write_lock(&mut self, ptr: MemoryPointer, len: u64,
519515
lock_region: Option<CodeExtent>, suspend: Option<CodeExtent>) -> EvalResult<'tcx> {
520516
assert!(len > 0);
521517
let cur_frame = self.cur_frame;
522518
let lock_lft = DynamicLifetime { frame: cur_frame, region: lock_region };
523519
let alloc = self.get_mut_unchecked(ptr.alloc_id)?;
524520

525521
'locks: for lock in alloc.locks.iter_mut(ptr.offset, len) {
526-
trace!("Releasing {:?}", lock);
527522
let is_our_lock = match lock.active {
528523
WriteLock(lft) => {
529524
lft == lock_lft
@@ -533,30 +528,25 @@ impl<'a, 'tcx, M: Machine<'tcx>> Memory<'a, 'tcx, M> {
533528
}
534529
};
535530
if is_our_lock {
531+
trace!("Releasing {:?} at {:?}", lock.active, lock_lft);
536532
// Disable the lock
537533
lock.active = NoLock;
534+
} else {
535+
trace!("Not touching {:?} at {:?} as its not our lock", lock.active, lock_lft);
538536
}
539537
match suspend {
540538
Some(suspend_region) => {
541-
if is_our_lock {
542-
// We just released this lock, so add a new suspension
543-
lock.suspended.push(SuspendedWriteLock { lft: lock_lft, suspensions: vec![suspend_region] });
544-
} else {
545-
// Find our lock in the suspended ones
546-
for suspended_lock in lock.suspended.iter_mut().rev() {
547-
if suspended_lock.lft == lock_lft {
548-
// Found it!
549-
suspended_lock.suspensions.push(suspend_region);
550-
continue 'locks;
551-
}
552-
}
553-
// We did not find it. Someone else had the lock and we have not suspended it, that's just wrong.
554-
return err!(InvalidMemoryLockRelease { ptr, len, frame: cur_frame, lock: lock.active.clone() });
555-
}
539+
trace!("Adding suspension to {:?} at {:?}", lock.active, lock_lft);
540+
// We just released this lock, so add a new suspension.
541+
// FIXME: Really, if there ever already is a suspension when is_our_lock, or if there is no suspension when !is_our_lock, something is amiss.
542+
// But this model is not good enough yet to prevent that.
543+
lock.suspended.entry(lock_lft)
544+
.or_insert_with(|| Vec::new())
545+
.push(suspend_region);
556546
}
557547
None => {
558-
// If we do not suspend, make sure we actually released something
559-
if !is_our_lock {
548+
// Make sure we did not try to release someone else's lock.
549+
if !is_our_lock && lock.active != NoLock {
560550
return err!(InvalidMemoryLockRelease { ptr, len, frame: cur_frame, lock: lock.active.clone() });
561551
}
562552
}
@@ -577,34 +567,33 @@ impl<'a, 'tcx, M: Machine<'tcx>> Memory<'a, 'tcx, M> {
577567
let alloc = self.get_mut_unchecked(ptr.alloc_id)?;
578568

579569
for lock in alloc.locks.iter_mut(ptr.offset, len) {
580-
// If we have a suspension here, it will be the topmost one
581-
let (got_the_lock, pop_suspension) = match lock.suspended.last_mut() {
582-
None => (true, false),
583-
Some(suspended_lock) => {
584-
if suspended_lock.lft == lock_lft {
585-
// That's us! Remove suspension (it should be in there). The same suspension can
586-
// occur multiple times (when there are multiple shared borrows of this that have the same
587-
// lifetime); only remove one of them.
588-
let idx = match suspended_lock.suspensions.iter().enumerate().find(|&(_, re)| re == &suspended_region) {
589-
None => // TODO: Can the user trigger this?
590-
bug!("We have this lock suspended, but not for the given region."),
591-
Some((idx, _)) => idx
592-
};
593-
suspended_lock.suspensions.remove(idx);
594-
let got_lock = suspended_lock.suspensions.is_empty();
595-
(got_lock, got_lock)
596-
} else {
597-
// Someone else's suspension up top, we should be able to grab the lock
598-
(true, false)
570+
// Check if we have a suspension here
571+
let (got_the_lock, remove_suspension) = match lock.suspended.get_mut(&lock_lft) {
572+
None => {
573+
trace!("No suspension around, we can just acquire");
574+
(true, false)
575+
}
576+
Some(suspensions) => {
577+
trace!("Found suspension of {:?}, removing it", lock_lft);
578+
// That's us! Remove suspension (it should be in there). The same suspension can
579+
// occur multiple times (when there are multiple shared borrows of this that have the same
580+
// lifetime); only remove one of them.
581+
let idx = match suspensions.iter().enumerate().find(|&(_, re)| re == &suspended_region) {
582+
None => // TODO: Can the user trigger this?
583+
bug!("We have this lock suspended, but not for the given region."),
584+
Some((idx, _)) => idx
585+
};
586+
suspensions.remove(idx);
587+
let got_lock = suspensions.is_empty();
588+
if got_lock {
589+
trace!("All suspensions are gone, we can have the lock again");
599590
}
591+
(got_lock, got_lock)
600592
}
601593
};
602-
if pop_suspension { // with NLL; we could do that up in the match above...
603-
lock.suspended.pop();
604-
} else {
605-
// Sanity check: Our lock should not be in the suspension list
606-
let found = lock.suspended.iter().find(|suspended_lock| suspended_lock.lft == lock_lft);
607-
assert!(found.is_none());
594+
if remove_suspension { // with NLL, we could do that up in the match above...
595+
assert!(got_the_lock);
596+
lock.suspended.remove(&lock_lft);
608597
}
609598
if got_the_lock {
610599
match lock.active {
@@ -653,7 +642,7 @@ impl<'a, 'tcx, M: Machine<'tcx>> Memory<'a, 'tcx, M> {
653642
lock.active = NoLock;
654643
}
655644
// Also clean up suspended write locks
656-
lock.suspended.retain(|suspended_lock| !has_ended(&suspended_lock.lft));
645+
lock.suspended.retain(|lft, _suspensions| !has_ended(lft));
657646
}
658647
// Clean up the map
659648
alloc.locks.retain(|lock| {

src/librustc_mir/interpret/range_map.rs

+58-8
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,9 @@
1-
//! Implements a map from disjoint non-empty integer ranges to data associated with those ranges
1+
//! Implements a map from integer indices to data.
2+
//! Rather than storing data for every index, internally, this maps entire ranges to the data.
3+
//! To this end, the APIs all work on ranges, not on individual integers. Ranges are split as
4+
//! necessary (e.g. when [0,5) is first associated with X, and then [1,2) is mutated).
5+
//! Users must not depend on whether a range is coalesced or not, even though this is observable
6+
//! via the iteration APIs.
27
use std::collections::{BTreeMap};
38
use std::ops;
49

@@ -21,6 +26,7 @@ struct Range {
2126

2227
impl Range {
2328
fn range(offset: u64, len: u64) -> ops::Range<Range> {
29+
assert!(len > 0);
2430
// We select all elements that are within
2531
// the range given by the offset into the allocation and the length.
2632
// This is sound if all ranges that intersect with the argument range, are in the
@@ -36,6 +42,7 @@ impl Range {
3642
left..right
3743
}
3844

45+
/// Tests if all of [offset, offset+len) are contained in this range.
3946
fn overlaps(&self, offset: u64, len: u64) -> bool {
4047
assert!(len > 0);
4148
offset < self.end && offset+len >= self.start
@@ -48,6 +55,7 @@ impl<T> RangeMap<T> {
4855
}
4956

5057
fn iter_with_range<'a>(&'a self, offset: u64, len: u64) -> impl Iterator<Item=(&'a Range, &'a T)> + 'a {
58+
assert!(len > 0);
5159
self.map.range(Range::range(offset, len))
5260
.filter_map(move |(range, data)| {
5361
if range.overlaps(offset, len) {
@@ -63,7 +71,7 @@ impl<T> RangeMap<T> {
6371
}
6472

6573
fn split_entry_at(&mut self, offset: u64) where T: Clone {
66-
let range = match self.iter_with_range(offset, 0).next() {
74+
let range = match self.iter_with_range(offset, 1).next() {
6775
Some((&range, _)) => range,
6876
None => return,
6977
};
@@ -88,6 +96,7 @@ impl<T> RangeMap<T> {
8896
pub fn iter_mut_with_gaps<'a>(&'a mut self, offset: u64, len: u64) -> impl Iterator<Item=&'a mut T> + 'a
8997
where T: Clone
9098
{
99+
assert!(len > 0);
91100
// Preparation: Split first and last entry as needed.
92101
self.split_entry_at(offset);
93102
self.split_entry_at(offset+len);
@@ -112,14 +121,15 @@ impl<T> RangeMap<T> {
112121
{
113122
// Do a first iteration to collect the gaps
114123
let mut gaps = Vec::new();
115-
let mut last_end = None;
124+
let mut last_end = offset;
116125
for (range, _) in self.iter_with_range(offset, len) {
117-
if let Some(last_end) = last_end {
118-
if last_end < range.start {
119-
gaps.push(Range { start: last_end, end: range.start });
120-
}
126+
if last_end < range.start {
127+
gaps.push(Range { start: last_end, end: range.start });
121128
}
122-
last_end = Some(range.end);
129+
last_end = range.end;
130+
}
131+
if last_end < offset+len {
132+
gaps.push(Range { start: last_end, end: offset+len });
123133
}
124134

125135
// Add default for all gaps
@@ -147,3 +157,43 @@ impl<T> RangeMap<T> {
147157
}
148158
}
149159
}
160+
161+
#[cfg(test)]
162+
mod tests {
163+
use super::*;
164+
165+
/// Query the map at every offset in the range and collect the results.
166+
fn to_vec<T: Copy>(map: &RangeMap<T>, offset: u64, len: u64) -> Vec<T> {
167+
(offset..offset+len).into_iter().map(|i| *map.iter(i, 1).next().unwrap()).collect()
168+
}
169+
170+
#[test]
171+
fn basic_insert() {
172+
let mut map = RangeMap::<i32>::new();
173+
// Insert
174+
for x in map.iter_mut(10, 1) {
175+
*x = 42;
176+
}
177+
// Check
178+
assert_eq!(to_vec(&map, 10, 1), vec![42]);
179+
}
180+
181+
#[test]
182+
fn gaps() {
183+
let mut map = RangeMap::<i32>::new();
184+
for x in map.iter_mut(11, 1) {
185+
*x = 42;
186+
}
187+
for x in map.iter_mut(15, 1) {
188+
*x = 42;
189+
}
190+
191+
// Now request a range that needs three gaps filled
192+
for x in map.iter_mut(10, 10) {
193+
if *x != 42 { *x = 23; }
194+
}
195+
196+
assert_eq!(to_vec(&map, 10, 10), vec![23, 42, 23, 23, 23, 42, 23, 23, 23, 23]);
197+
assert_eq!(to_vec(&map, 13, 5), vec![23, 23, 42, 23, 23]);
198+
}
199+
}

0 commit comments

Comments
 (0)