Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Cap maximum depth of incomplete type display #221

Merged
merged 4 commits into from
Jun 28, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 38 additions & 9 deletions src/dag.rs
Original file line number Diff line number Diff line change
Expand Up @@ -278,13 +278,15 @@ pub trait DagLike: Sized {
/// yielded, you may be better off using this iterator instead.
fn verbose_pre_order_iter<S: SharingTracker<Self> + Default>(
self,
max_depth: Option<usize>,
) -> VerbosePreOrderIter<Self, S>
where
Self: Clone,
{
VerbosePreOrderIter {
stack: vec![PreOrderIterItem::initial(self, None)],
stack: vec![PreOrderIterItem::initial(self, 0, None)],
index: 0,
max_depth,
tracker: Default::default(),
}
}
Expand Down Expand Up @@ -775,6 +777,16 @@ pub struct VerbosePreOrderIter<D, S> {
/// children are put onto the stack followed by their left, so that the
/// appropriate one will be yielded on the next iteration.
stack: Vec<PreOrderIterItem<D>>,
/// Maximum depth (distance from root) that the iterator will go to. Any
/// children at a greater depth will not be yielded. However, the parent
/// of such children will still be yielded multiple times, one for each
/// (unyielded) child, with `n_children_yielded` incremented as though
/// the children had been yielded.
///
/// To determine whether pruning has happened, you should manually check
/// the [`PreOrderIterItem::depth`] field against the maximum depth that
/// you set when constructing the iterator.
max_depth: Option<usize>,
/// The index of the next item to be yielded.
///
/// Note that unlike the [`PostOrderIter`], this value is not monotonic
Expand Down Expand Up @@ -809,19 +821,31 @@ impl<D: DagLike + Clone, S: SharingTracker<D>> Iterator for VerbosePreOrderIter<
(0, 0) => {}
(0, n) => {
self.stack.push(top.clone().increment(n == 1));
let child = top.node.left_child().unwrap();
self.stack
.push(PreOrderIterItem::initial(child, Some(top.node.clone())));
if top.depth < self.max_depth.unwrap_or(top.depth + 1) {
let child = top.node.left_child().unwrap();
self.stack.push(PreOrderIterItem::initial(
child,
top.depth + 1,
Some(top.node.clone()),
));
}
}
(1, 0) => unreachable!(),
(1, 1) => {}
(1, _) => {
self.stack.push(top.clone().increment(true));
let child = top.node.right_child().unwrap();
self.stack
.push(PreOrderIterItem::initial(child, Some(top.node.clone())));
if top.depth < self.max_depth.unwrap_or(top.depth + 1) {
let child = top.node.right_child().unwrap();
self.stack.push(PreOrderIterItem::initial(
child,
top.depth + 1,
Some(top.node.clone()),
));
}
}
(x, y) => {
debug_assert_eq!((x, y), (2, 2));
}
(_, _) => {}
}
// Then yield the element.
return Some(top);
Expand All @@ -840,6 +864,9 @@ pub struct PreOrderIterItem<D> {
pub parent: Option<D>,
/// The index when the element was first yielded.
pub index: usize,
/// The distance of this element from the initial node. 0 for the initial
/// node itself.
pub depth: usize,
/// How many of this item's children have been yielded.
///
/// This can also be interpreted as a count of how many times this
Expand All @@ -853,12 +880,13 @@ impl<D: DagLike + Clone> PreOrderIterItem<D> {
/// Creates a `PreOrderIterItem` which yields a given element for the first time.
///
/// Marks the index as 0. The index must be manually set before yielding.
fn initial(d: D, parent: Option<D>) -> Self {
fn initial(d: D, depth: usize, parent: Option<D>) -> Self {
PreOrderIterItem {
is_complete: matches!(d.as_dag_node(), Dag::Nullary),
node: d,
parent,
index: 0,
depth,
n_children_yielded: 0,
}
}
Expand All @@ -868,6 +896,7 @@ impl<D: DagLike + Clone> PreOrderIterItem<D> {
PreOrderIterItem {
node: self.node,
index: self.index,
depth: self.depth,
parent: self.parent,
n_children_yielded: self.n_children_yielded + 1,
is_complete,
Expand Down
37 changes: 37 additions & 0 deletions src/node/commit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -538,4 +538,41 @@ mod tests {
// I created this unit test by hand
assert_program_not_deserializable::<Core>(&[0xa9, 0x48, 0x00], &Error::NotInCanonicalOrder);
}

#[test]
fn regression_177() {
// `case (drop iden) iden` from upstream occurs-check test. Has an infinitely sized
// input type. Will fail trying to unify the input type with the unit type before
// doing the occurs check, putting an infinitely-sized type into the error variant.
//
// The human-readable encoding will keep going and then also hit the occurs check.
//
// Check that both error types can be generated and printed in finite space/time.
let bad_prog = "
id := iden
main := case (drop id) id
";
match Forest::<Core>::parse(bad_prog) {
Ok(_) => panic!("program should have failed"),
Err(set) => {
let mut errs_happened = (false, false);
for err in set.iter() {
match err {
crate::human_encoding::Error::TypeCheck(e @ types::Error::Bind { .. }) => {
errs_happened.0 = true;
e.to_string();
}
crate::human_encoding::Error::TypeCheck(
e @ types::Error::OccursCheck { .. },
) => {
errs_happened.1 = true;
e.to_string();
}
x => panic!("unexpected error {x:?}"),
}
}
assert_eq!(errs_happened, (true, true));
}
};
}
}
6 changes: 3 additions & 3 deletions src/node/construct.rs
Original file line number Diff line number Diff line change
Expand Up @@ -300,7 +300,7 @@ mod tests {

assert!(matches!(
node.finalize_types_non_program(),
Err(crate::Error::Type(types::Error::OccursCheck)),
Err(crate::Error::Type(types::Error::OccursCheck { .. })),
));
}

Expand All @@ -320,7 +320,7 @@ mod tests {

assert!(matches!(
comp2.finalize_types_non_program(),
Err(crate::Error::Type(types::Error::OccursCheck)),
Err(crate::Error::Type(types::Error::OccursCheck { .. })),
));
}

Expand All @@ -347,7 +347,7 @@ mod tests {

assert!(matches!(
comp8.finalize_types_non_program(),
Err(crate::Error::Type(types::Error::OccursCheck)),
Err(crate::Error::Type(types::Error::OccursCheck { .. })),
));
}

Expand Down
2 changes: 1 addition & 1 deletion src/node/display.rs
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ where
&'a Node<M>: DagLike,
{
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
for data in self.0.verbose_pre_order_iter::<NoSharing>() {
for data in self.0.verbose_pre_order_iter::<NoSharing>(None) {
match data.n_children_yielded {
1 => match data.node.inner() {
Inner::Comp(..) => f.write_str("; ")?,
Expand Down
2 changes: 1 addition & 1 deletion src/types/final_data.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ impl fmt::Debug for Final {
impl fmt::Display for Final {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
let mut skipping: Option<Tmr> = None;
for data in self.verbose_pre_order_iter::<NoSharing>() {
for data in self.verbose_pre_order_iter::<NoSharing>(None) {
if let Some(skip) = skipping {
if data.is_complete && data.node.tmr == skip {
skipping = None;
Expand Down
72 changes: 59 additions & 13 deletions src/types/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,7 @@ pub enum Error {
hint: &'static str,
},
/// A type is recursive (i.e., occurs within itself), violating the "occurs check"
OccursCheck,
OccursCheck { infinite_bound: Arc<Bound> },
}

impl fmt::Display for Error {
Expand Down Expand Up @@ -131,7 +131,9 @@ impl fmt::Display for Error {
type1, type2, hint,
)
}
Error::OccursCheck => f.write_str("detected infinitely-sized type"),
Error::OccursCheck { infinite_bound } => {
write!(f, "infinitely-sized type {}", infinite_bound,)
}
}
}
}
Expand Down Expand Up @@ -294,10 +296,18 @@ impl Bound {
}
}

const MAX_DISPLAY_DEPTH: usize = 64;

impl fmt::Debug for Bound {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
let arc = Arc::new(self.shallow_clone());
for data in arc.verbose_pre_order_iter::<NoSharing>() {
for data in arc.verbose_pre_order_iter::<NoSharing>(Some(MAX_DISPLAY_DEPTH)) {
if data.depth == MAX_DISPLAY_DEPTH {
if data.n_children_yielded == 0 {
f.write_str("...")?;
}
continue;
}
match (&*data.node, data.n_children_yielded) {
(Bound::Free(ref s), _) => f.write_str(s)?,
(Bound::Complete(ref comp), _) => fmt::Debug::fmt(comp, f)?,
Expand All @@ -314,13 +324,19 @@ impl fmt::Debug for Bound {
impl fmt::Display for Bound {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
let arc = Arc::new(self.shallow_clone());
for data in arc.verbose_pre_order_iter::<NoSharing>() {
for data in arc.verbose_pre_order_iter::<NoSharing>(Some(MAX_DISPLAY_DEPTH)) {
if data.depth == MAX_DISPLAY_DEPTH {
if data.n_children_yielded == 0 {
f.write_str("...")?;
}
continue;
}
match (&*data.node, data.n_children_yielded) {
(Bound::Free(ref s), _) => f.write_str(s)?,
(Bound::Complete(ref comp), _) => fmt::Display::fmt(comp, f)?,
(Bound::Sum(..), 0) | (Bound::Product(..), 0) => {
if data.index > 0 {
f.write_str("(")?
f.write_str("(")?;
}
}
(Bound::Sum(..), 2) | (Bound::Product(..), 2) => {
Expand Down Expand Up @@ -449,21 +465,51 @@ impl Type {

/// Attempts to finalize the type. Returns its TMR on success.
pub fn finalize(&self) -> Result<Arc<Final>, Error> {
/// Helper type for the occurs-check.
enum OccursCheckStack {
Iterate(Arc<Bound>),
Complete(*const Bound),
}

// Done with sharing tracker. Actual algorithm follows.
let root = self.bound.root();
let bound = root.get();
if let Bound::Complete(ref data) = *bound {
return Ok(Arc::clone(data));
}

// First, do occurs-check to ensure that we have no infinitely sized types.
let mut occurs_check = HashSet::new();
for data in bound.verbose_pre_order_iter::<NoSharing>() {
if data.is_complete {
occurs_check.remove(&(data.node.as_ref() as *const _));
} else if data.n_children_yielded == 0
&& !occurs_check.insert(data.node.as_ref() as *const _)
{
return Err(Error::OccursCheck);
let mut stack = vec![OccursCheckStack::Iterate(Arc::clone(&bound))];
let mut in_progress = HashSet::new();
let mut completed = HashSet::new();
while let Some(top) = stack.pop() {
let bound = match top {
OccursCheckStack::Complete(ptr) => {
in_progress.remove(&ptr);
completed.insert(ptr);
continue;
}
OccursCheckStack::Iterate(b) => b,
};

let ptr = bound.as_ref() as *const _;
if completed.contains(&ptr) {
// Once we have iterated through a type, we don't need to check it again.
// Without this shortcut the occurs-check would take exponential time.
continue;
}
if !in_progress.insert(ptr) {
return Err(Error::OccursCheck {
infinite_bound: bound,
});
}

stack.push(OccursCheckStack::Complete(ptr));
if let Some(child) = bound.right_child() {
stack.push(OccursCheckStack::Iterate(child));
}
if let Some(child) = bound.left_child() {
stack.push(OccursCheckStack::Iterate(child));
}
}

Expand Down
2 changes: 1 addition & 1 deletion src/value.rs
Original file line number Diff line number Diff line change
Expand Up @@ -339,7 +339,7 @@ impl fmt::Debug for Value {

impl fmt::Display for Value {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
for data in self.verbose_pre_order_iter::<NoSharing>() {
for data in self.verbose_pre_order_iter::<NoSharing>(None) {
match data.node {
Value::Unit => {
if data.n_children_yielded == 0
Expand Down
Loading