Skip to content

Commit

Permalink
more lazyness, less heavy on the memory
Browse files Browse the repository at this point in the history
  • Loading branch information
@Vanille-N
Vanille-N committed Sep 7, 2023
1 parent 5b219ee commit f9b83a0
Show file tree
Hide file tree
Showing 3 changed files with 91 additions and 134 deletions.
95 changes: 32 additions & 63 deletions src/borrow_tracker/tree_borrows/exhaustive.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
#![cfg(test)]

pub trait Exhaustive: Sized {
fn exhaustive() -> Vec<Self>;
fn exhaustive() -> Box<dyn Iterator<Item = Self>>;
}

macro_rules! precondition {
Expand All @@ -18,111 +18,80 @@ macro_rules! precondition {
pub(crate) use precondition;

impl Exhaustive for bool {
fn exhaustive() -> Vec<Self> {
vec![true, false]
fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
Box::new(vec![true, false].into_iter())
}
}

// Some container impls for `Exhaustive`

impl<T> Exhaustive for Option<T>
where
T: Exhaustive,
T: Exhaustive + 'static,
{
fn exhaustive() -> Vec<Self> {
let mut v = vec![None];
for t in T::exhaustive() {
v.push(Some(t));
}
v
fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
Box::new(std::iter::once(None).chain(T::exhaustive().map(Some)))
}
}

impl<T1, T2> Exhaustive for (T1, T2)
where
T1: Exhaustive + Clone,
T2: Exhaustive,
T1: Exhaustive + Clone + 'static,
T2: Exhaustive + 'static,
{
fn exhaustive() -> Vec<Self> {
let mut v = Vec::new();
for t1 in T1::exhaustive() {
for t2 in T2::exhaustive() {
v.push((t1.clone(), t2));
}
}
v
fn exhaustive() -> Box<dyn Iterator<Item=Self>> {
Box::new(T1::exhaustive().flat_map(|t1| T2::exhaustive().map(move |t2| (t1.clone(), t2))))
}
}

impl<T> Exhaustive for [T; 1]
where
T: Exhaustive,
T: Exhaustive + 'static,
{
fn exhaustive() -> Vec<Self> {
let mut v = Vec::new();
for t1 in T::exhaustive() {
v.push([t1]);
}
v
fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
Box::new(T::exhaustive().map(|t| [t]))
}
}

impl<T> Exhaustive for [T; 2]
where
T: Exhaustive + Clone,
T: Exhaustive + Clone + 'static,
{
fn exhaustive() -> Vec<Self> {
let mut v = Vec::new();
for t1 in T::exhaustive() {
for t2 in T::exhaustive() {
v.push([t1.clone(), t2]);
}
}
v
fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
Box::new(T::exhaustive().flat_map(|t1| T::exhaustive().map(move |t2| [t1.clone(), t2])))
}
}

impl<T> Exhaustive for [T; 3]
where
T: Exhaustive + Clone,
T: Exhaustive + Clone + 'static,
{
fn exhaustive() -> Vec<Self> {
let mut v = Vec::new();
for [t1, t2] in <[T; 2]>::exhaustive() {
for t3 in T::exhaustive() {
v.push([t1.clone(), t2.clone(), t3]);
}
}
v
fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
Box::new(
<[T; 2]>::exhaustive()
.flat_map(|[t1, t2]| T::exhaustive().map(move |t3| [t1.clone(), t2.clone(), t3])),
)
}
}

impl<T> Exhaustive for [T; 4]
where
T: Exhaustive + Clone,
T: Exhaustive + Clone + 'static,
{
fn exhaustive() -> Vec<Self> {
let mut v = Vec::new();
for [t1, t2] in <[T; 2]>::exhaustive() {
for [t3, t4] in <[T; 2]>::exhaustive() {
v.push([t1.clone(), t2.clone(), t3, t4]);
}
}
v
fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
Box::new(<[T; 2]>::exhaustive().flat_map(|[t1, t2]| {
<[T; 2]>::exhaustive().map(move |[t3, t4]| [t1.clone(), t2.clone(), t3, t4])
}))
}
}

impl<T> Exhaustive for [T; 5]
where
T: Exhaustive + Clone,
T: Exhaustive + Clone + 'static,
{
fn exhaustive() -> Vec<Self> {
let mut v = Vec::new();
for [t1, t2] in <[T; 2]>::exhaustive() {
for [t3, t4, t5] in <[T; 3]>::exhaustive() {
v.push([t1.clone(), t2.clone(), t3, t4, t5]);
}
}
v
fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
Box::new(<[T; 2]>::exhaustive().flat_map(|[t1, t2]| {
<[T; 3]>::exhaustive().map(move |[t3, t4, t5]| [t1.clone(), t2.clone(), t3, t4, t5])
}))
}
}
24 changes: 12 additions & 12 deletions src/borrow_tracker/tree_borrows/perms.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -410,32 +410,32 @@ mod propagation_optimization_checks {
use crate::borrow_tracker::tree_borrows::exhaustive::{precondition, Exhaustive};

impl Exhaustive for PermissionPriv {
fn exhaustive() -> Vec<Self> {
let mut v = vec![Active, Frozen, Disabled];
for ty_is_freeze in bool::exhaustive() {
v.push(Reserved { ty_is_freeze });
}
v
fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
Box::new(
vec![Active, Frozen, Disabled]
.into_iter()
.chain(bool::exhaustive().map(|ty_is_freeze| Reserved { ty_is_freeze })),
)
}
}

impl Exhaustive for Permission {
fn exhaustive() -> Vec<Self> {
PermissionPriv::exhaustive().into_iter().map(|inner| Self { inner }).collect()
fn exhaustive() -> Box<dyn Iterator<Item=Self>> {
Box::new(PermissionPriv::exhaustive().map(|inner| Self { inner }))
}
}

impl Exhaustive for AccessKind {
fn exhaustive() -> Vec<Self> {
fn exhaustive() -> Box<dyn Iterator<Item=Self>> {
use AccessKind::*;
vec![Read, Write]
Box::new(vec![Read, Write].into_iter())
}
}

impl Exhaustive for AccessRelatedness {
fn exhaustive() -> Vec<Self> {
fn exhaustive() -> Box<dyn Iterator<Item=Self>> {
use AccessRelatedness::*;
vec![This, StrictChildAccess, AncestorAccess, DistantAccess]
Box::new(vec![This, StrictChildAccess, AncestorAccess, DistantAccess].into_iter())
}
}

Expand Down
106 changes: 47 additions & 59 deletions src/borrow_tracker/tree_borrows/tree.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -685,13 +685,9 @@ mod commutation_tests {
use std::fmt;

impl Exhaustive for LocationState {
fn exhaustive() -> Vec<Self> {
fn exhaustive() -> Box<dyn Iterator<Item=Self>> {
// We keep `latest_foreign_access` at `None` as that's just a cache.
let mut v = Vec::new();
for (permission, initialized) in <(Permission, bool)>::exhaustive() {
v.push(Self { permission, initialized, latest_foreign_access: None });
}
v
Box::new(<(Permission, bool)>::exhaustive().map(|(permission, initialized)| Self { permission, initialized, latest_foreign_access: None }))
}
}

Expand Down Expand Up @@ -769,9 +765,9 @@ mod commutation_tests {
}

impl Exhaustive for AccessRel2 {
fn exhaustive() -> Vec<Self> {
fn exhaustive() -> Box<dyn Iterator<Item=Self>> {
use AccessRel2 as Rel;
vec![Rel::ChildX, Rel::ChildY, Rel::Other]
Box::new(vec![Rel::ChildX, Rel::ChildY, Rel::Other].into_iter())
}
}

Expand All @@ -782,11 +778,9 @@ mod commutation_tests {
}

impl Exhaustive for Access2 {
fn exhaustive() -> Vec<Self> {
<(AccessRel2, AccessKind)>::exhaustive()
.into_iter()
.map(|(rel2, kind)| Access2 { rel2, kind })
.collect()
fn exhaustive() -> Box<dyn Iterator<Item=Self>> {
Box::new(<(AccessRel2, AccessKind)>::exhaustive()
.map(|(rel2, kind)| Access2 { rel2, kind }))
}
}

Expand Down Expand Up @@ -815,14 +809,8 @@ mod commutation_tests {
}

impl Exhaustive for LocStateProt {
fn exhaustive() -> Vec<Self> {
let mut v = Vec::new();
for state in LocationState::exhaustive() {
for prot in bool::exhaustive() {
v.push(Self { state, prot });
}
}
v
fn exhaustive() -> Box<dyn Iterator<Item=Self>> {
Box::new(<(LocationState, bool)>::exhaustive().map(|(state, prot)| Self { state, prot }))
}
}

Expand Down Expand Up @@ -885,12 +873,8 @@ mod commutation_tests {
}

impl Exhaustive for LocStateProt2 {
fn exhaustive() -> Vec<Self> {
let mut v = Vec::new();
for [x, y] in <[LocStateProt; 2]>::exhaustive() {
v.push(Self { x, y });
}
v
fn exhaustive() -> Box<dyn Iterator<Item=Self>> {
Box::new(<[LocStateProt; 2]>::exhaustive().map(|[x, y]| Self { x, y }))
}
}

Expand All @@ -907,15 +891,13 @@ mod commutation_tests {
}

impl Opaque2 {
fn exhaustive_witness() -> Vec<Self> {
<[Option<Access2>; 5]>::exhaustive()
.into_iter()
.map(|x| Opaque2 { events: x.into_iter().collect() })
.collect()
fn exhaustive_witness() -> Box<dyn Iterator<Item=Self>> {
Box::new(<[Option<Access2>; 5]>::exhaustive()
.map(|x| Opaque2 { events: x.into_iter().collect() }))
}
}
impl Exhaustive for Opaque2 {
fn exhaustive() -> Vec<Self> {
fn exhaustive() -> Box<dyn Iterator<Item=Self>> {
// There are a lot of combinations (infinitely many in fact),
// so we're only generating a small subset and then testing through other means
// that we have a representative sample.
Expand All @@ -924,35 +906,41 @@ mod commutation_tests {
// - since accesses are idempotent it's never useful to have the same twice in a row
// - sequences of length 3 or less might as well have their noops at the end
// This reduces by a lot the space to explore.
let mut v = Vec::new();
for acc0 in <Option<Access2>>::exhaustive() {
for acc1 in <Option<Access2>>::exhaustive() {
precondition!(acc0.is_none() || acc1.is_some());
precondition!(if let (Some(acc0), Some(acc1)) = (acc0, acc1) {
Box::new(<[Option<Access2>; 2]>::exhaustive()
.filter(|[acc0, acc1]| acc0.is_none() || acc1.is_some())
.filter(|[acc0, acc1]| {
if let (Some(acc0), Some(acc1)) = (acc0, acc1) {
acc0.rel2 != acc1.rel2
} else {
true
});
for acc2 in <Option<Access2>>::exhaustive() {
precondition!(acc1.is_none() || acc2.is_some());
precondition!(if let (Some(acc1), Some(acc2)) = (acc1, acc2) {
acc1.rel2 != acc2.rel2
} else {
true
});
for acc3 in <Option<Access2>>::exhaustive() {
precondition!(acc2.is_none() || acc3.is_some());
precondition!(if let (Some(acc2), Some(acc3)) = (acc2, acc3) {
acc2.rel2 != acc3.rel2
}
})
.flat_map(|[acc0, acc1]| {
<Option<Access2>>::exhaustive()
.filter(move |acc2| acc1.is_none() || acc2.is_some())
.filter(move |acc2| {
if let (Some(acc1), Some(acc2)) = (acc1, acc2) {
acc1.rel2 != acc2.rel2
} else {
true
});
v.push(Opaque2 { events: vec![acc0, acc1, acc2, acc3] })
}
}
}
}
v
}
})
.flat_map(move |acc2| {
<Option<Access2>>::exhaustive()
.filter(move |acc3| acc2.is_none() || acc3.is_some())
.filter(move |acc3| {
if let (Some(acc2), Some(acc3)) = (acc2, acc3) {
acc2.rel2 != acc3.rel2
} else {
true
}
})
.map(move |acc3| {
Opaque2 { events: vec![acc0, acc1, acc2, acc3] }
})
})
})
)
}
}

Expand Down Expand Up @@ -1108,7 +1096,7 @@ mod commutation_tests {
}

impl Exhaustive for Pattern {
fn exhaustive() -> Vec<Self> {
fn exhaustive() -> Box<dyn Iterator<Item=Self>> {
let mut v = Vec::new();
for (x_initial_state, y_initial_state) in
<(LocationState, LocationState)>::exhaustive()
Expand All @@ -1134,7 +1122,7 @@ mod commutation_tests {
}
}
}
v
Box::new(v.into_iter())
}
}

Expand Down

0 comments on commit f9b83a0

Please sign in to comment.