Tree / Obligation runtime checks.

Print abbreviated def paths for body names.

crates/argus/src/analysis/entry.rs

@@ -61,7 +61,7 @@ pub fn process_obligation<'tcx>(
     return;
   };
 
-  if INCLUDE_SUCCESSES.copied().unwrap_or(false) && result.is_yes() {
+  if !INCLUDE_SUCCESSES.copied().unwrap_or(false) && result.is_yes() {
     log::debug!("Skipping successful obligation {obl:?}");
     return;
   }

crates/argus/src/analysis/transform.rs

@@ -24,7 +24,7 @@ use crate::{
 
 macro_rules! property_is_ok {
   ($prop:expr, $t:tt) => {{
-    #[cfg(feature = "testing")]
+    #[cfg(any(feature = "testing", debug_assertions))]
     {
       let it = $prop;
       if !it.is_ok() {
@@ -66,6 +66,17 @@ pub fn compute_provenance<'tcx>(
   }
 }
 
+fn expect_trait_ref<'tcx>(
+  p: &ty::Predicate<'tcx>,
+) -> ty::Binder<'tcx, ty::TraitPredicate<'tcx>> {
+  p.kind().map_bound(|f| {
+    let ty::PredicateKind::Clause(ty::ClauseKind::Trait(tr)) = f else {
+      unreachable!();
+    };
+    tr
+  })
+}
+
 pub fn transform<'a, 'tcx: 'a>(
   tcx: TyCtxt<'tcx>,
   body_id: BodyId,
@@ -76,7 +87,7 @@ pub fn transform<'a, 'tcx: 'a>(
   reported_trait_errors: &FxIndexMap<Span, Vec<ObligationHash>>,
   bins: Vec<Bin>,
 ) -> ObligationsInBody {
-  #[cfg(feature = "testing")]
+  #[cfg(debug_assertions)]
   {
     assert!(synthetic_data.is_empty(), "synthetic data not empty");
     assert!(
@@ -543,7 +554,7 @@ impl<'a, 'tcx: 'a> ObligationsBuilder<'a, 'tcx> {
     ))
   }
 
-  #[cfg(feature = "testing")]
+  #[cfg(any(feature = "testing", debug_assertions))]
   fn is_valid(&self) -> anyhow::Result<()> {
     for obl in self.raw_obligations.iter() {
       if obl.is_synthetic {
@@ -564,14 +575,3 @@ impl<'a, 'tcx: 'a> ObligationsBuilder<'a, 'tcx> {
     Ok(())
   }
 }
-
-fn expect_trait_ref<'tcx>(
-  p: &ty::Predicate<'tcx>,
-) -> ty::Binder<'tcx, ty::TraitPredicate<'tcx>> {
-  p.kind().map_bound(|f| {
-    let ty::PredicateKind::Clause(ty::ClauseKind::Trait(tr)) = f else {
-      unreachable!();
-    };
-    tr
-  })
-}

crates/argus/src/proof_tree/ext.rs

@@ -66,15 +66,9 @@ impl CandidateExt for InspectCandidate<'_, '_> {
   }
 
   fn is_informative_probe(&self) -> bool {
-    matches!(
-      self.kind(),
-      ProbeKind::TraitCandidate {
-        source: CandidateSource::Impl(_),
-        ..
-      } | ProbeKind::TraitCandidate {
-        source: CandidateSource::BuiltinImpl(_),
-        ..
-      }
-    )
+    matches!(self.kind(), ProbeKind::TraitCandidate {
+      source: CandidateSource::Impl(_) | CandidateSource::ParamEnv(_),
+      ..
+    })
   }
 }

crates/argus/src/proof_tree/interners.rs

@@ -87,6 +87,14 @@ impl Interners {
     )
   }
 
+  pub fn goal(&self, g: GoalIdx) -> &GoalData {
+    &self.goals.values[g]
+  }
+
+  pub fn candidate(&self, c: CandidateIdx) -> &CandidateData {
+    &self.candidates.values[c]
+  }
+
   pub fn mk_result_node(&mut self, result: EvaluationResult) -> Node {
     Node::Result(self.intern_result(result))
   }

crates/argus/src/proof_tree/mod.rs

@@ -100,7 +100,6 @@ pub struct SerializedTree {
   pub results: IndexVec<ResultIdx, ResultData>,
 
   pub topology: TreeTopology,
-  pub error_leaves: Vec<ProofNodeIdx>,
   pub unnecessary_roots: HashSet<ProofNodeIdx>,
   #[serde(skip_serializing_if = "Option::is_none")]
   pub cycle: Option<ProofCycle>,

crates/argus/src/proof_tree/serialize.rs

@@ -1,7 +1,7 @@
 use std::{collections::HashSet, ops::ControlFlow};
 
 use anyhow::{bail, Result};
-use ext::{CandidateExt, EvaluationResultExt};
+use ext::CandidateExt;
 use index_vec::IndexVec;
 use rustc_hir::def_id::DefId;
 use rustc_infer::infer::InferCtxt;
@@ -19,7 +19,6 @@ pub struct SerializedTreeVisitor {
   pub previous: Option<ProofNodeIdx>,
   pub nodes: IndexVec<ProofNodeIdx, Node>,
   pub topology: TreeTopology,
-  pub error_leaves: Vec<ProofNodeIdx>,
   pub unnecessary_roots: HashSet<ProofNodeIdx>,
   pub cycle: Option<ProofCycle>,
   interners: Interners,
@@ -33,19 +32,49 @@ impl SerializedTreeVisitor {
       previous: None,
       nodes: IndexVec::default(),
       topology: TreeTopology::new(),
-      error_leaves: Vec::default(),
       unnecessary_roots: HashSet::default(),
       cycle: None,
       interners: Interners::default(),
     }
   }
 
+  #[cfg(debug_assertions)]
+  fn is_valid(&self) -> Result<()> {
+    for (pidx, node) in self.nodes.iter_enumerated() {
+      match node {
+        Node::Goal(g) => {
+          anyhow::ensure!(
+            !self.topology.is_leaf(pidx),
+            "non-leaf node (goal) has no children {:?}",
+            self.interners.goal(*g)
+          );
+        }
+        Node::Candidate(c) => {
+          anyhow::ensure!(
+            !self.topology.is_leaf(pidx),
+            "non-leaf node (candidate) has no children {:?}",
+            self.interners.candidate(*c)
+          );
+        }
+        Node::Result(..) => {
+          anyhow::ensure!(
+            self.topology.is_leaf(pidx),
+            "result node is not a leaf"
+          );
+        }
+      }
+    }
+    Ok(())
+  }
+
   pub fn into_tree(self) -> Result<SerializedTree> {
+    #[cfg(debug_assertions)]
+    self.is_valid()?;
+
     let SerializedTreeVisitor {
       root: Some(root),
       nodes,
       topology,
-      error_leaves,
       unnecessary_roots,
       cycle,
       interners,
@@ -64,7 +93,6 @@ impl SerializedTreeVisitor {
       results,
       nodes,
       topology,
-      error_leaves,
       unnecessary_roots,
       cycle,
     })
@@ -98,7 +126,6 @@ impl<'tcx> ProofTreeVisitor<'tcx> for SerializedTreeVisitor {
     goal: &InspectGoal<'_, 'tcx>,
   ) -> ControlFlow<Self::BreakTy> {
     let here_node = self.interners.mk_goal_node(goal);
-
     let here_idx = self.nodes.push(here_node.clone());
 
     if self.root.is_none() {
@@ -114,35 +141,32 @@ impl<'tcx> ProofTreeVisitor<'tcx> for SerializedTreeVisitor {
     // how the solver actually works, and is ignorant of inference vars.
     self.check_for_cycle_from(here_idx);
 
-    let prev = self.previous.clone();
-    self.previous = Some(here_idx);
+    let here_parent = self.previous.clone();
+
+    let add_result_if_empty = |this: &mut Self, n: ProofNodeIdx| {
+      if this.topology.is_leaf(n) {
+        let result = goal.result();
+        let leaf = this.interners.mk_result_node(result);
+        let leaf_idx = this.nodes.push(leaf);
+        this.topology.add(n, leaf_idx);
+      }
+    };
 
     for c in goal.candidates() {
+      if !c.is_informative_probe() {
+        continue;
+      }
+
       let here_candidate = self.interners.mk_candidate_node(&c);
       let candidate_idx = self.nodes.push(here_candidate);
-
-      let prev_idx = if c.is_informative_probe() {
-        self.topology.add(here_idx, candidate_idx);
-        self.previous = Some(candidate_idx);
-        candidate_idx
-      } else {
-        here_idx
-      };
-
+      self.topology.add(here_idx, candidate_idx);
+      self.previous = Some(candidate_idx);
       c.visit_nested(self)?;
-
-      if self.topology.is_leaf(prev_idx) {
-        let result = goal.result();
-        let leaf = self.interners.mk_result_node(result);
-        let leaf_idx = self.nodes.push(leaf);
-        self.topology.add(prev_idx, leaf_idx);
-        if !result.is_yes() {
-          self.error_leaves.push(leaf_idx);
-        }
-      }
+      add_result_if_empty(self, candidate_idx);
     }
 
-    self.previous = prev;
+    add_result_if_empty(self, here_idx);
+    self.previous = here_parent;
 
     ControlFlow::Continue(())
   }

ide/packages/panoptes/src/TreeView/BottomUp.tsx

@@ -102,7 +102,8 @@ function invertViewWithRoots(
     // Each element of the group is equivalent, so just take the first
     const builder = new TopologyBuilder(group[0], tree);
 
-    // Get the paths to the root from all leaves
+    // Get the paths to the root from all leaves, filter paths that
+    // contain successful nodes.
     const pathsToRoot = _.map(group, parent => tree.pathToRoot(parent).path);
 
     console.debug(
@@ -128,16 +129,16 @@ const BottomUp = () => {
   const mkGetChildren = (view: TreeView) => (idx: ProofNodeIdx) =>
     view.topology.children[idx] ?? [];
 
-  const leaves = _.map(tree.errorNodesRecommendedOrder(), leaf => {
-    let curr: ProofNodeIdx | undefined = leaf;
+  const liftToGoal = (idx: ProofNodeIdx) => {
+    let curr: ProofNodeIdx | undefined = idx;
     while (curr !== undefined && !("Goal" in tree.node(curr))) {
       curr = tree.parent(curr);
     }
     return curr;
-  });
+  };
 
+  const leaves = _.map(tree.errorLeavesRecommendedOrder(), liftToGoal);
   const invertedViews = invertViewWithRoots(_.compact(leaves), tree);
-
   // The "Argus recommended" errors are shown expanded, and the
   // "others" are collapsed. Argus recommended errors are the ones
   // that failed or are ambiguous with a concrete type on the LHS.
@@ -149,7 +150,7 @@ const BottomUp = () => {
       return result === "no" || result === "maybe-overflow" || !goal.isLhsTyVar;
     } else {
       // Leaves should only be goals...
-      return false;
+      throw new Error(`Leaves should only be goals ${node}`);
     }
   });
 

ide/packages/panoptes/src/TreeView/TreeApp.tsx

@@ -37,7 +37,7 @@ const TreeApp = ({
 
   const tabs: [string, React.FC][] = [["Top Down", TopDown]];
 
-  if (treeInfo.errorNodes().length > 0) {
+  if (treeInfo.errorLeaves().length > 0) {
     tabs.unshift(["Bottom Up", BottomUp]);
   }
 

ide/packages/panoptes/src/TreeView/TreeInfo.ts

@@ -195,17 +195,33 @@ export class TreeInfo {
     };
   }
 
-  public errorNodes(): ProofNodeIdx[] {
-    const allLeaves = this.tree.errorLeaves;
-    const viewLeaves = _.filter(
-      allLeaves,
-      leaf => this.view.topology.parent[leaf] !== undefined
-    );
-    return viewLeaves;
+  public errorLeaves(): ProofNodeIdx[] {
+    if (this.nodeResult(this.root) === "yes") {
+      return [];
+    }
+
+    let errorLeaves = [];
+    let stack = [this.root];
+    while (stack.length > 0) {
+      const current = stack.pop()!;
+      const children = this.children(current);
+      if (children.length === 0 && this.nodeResult(current) !== "yes") {
+        const node = this.node(current);
+        if ("Result" in node) {
+          errorLeaves.push(current);
+        } else {
+          console.error("Node has no children but isn't a leaf", node);
+        }
+      } else {
+        const errorKids = _.filter(children, n => this.nodeResult(n) !== "yes");
+        stack.push(...errorKids);
+      }
+    }
+    return errorLeaves;
   }
 
-  public errorNodesRecommendedOrder(): ProofNodeIdx[] {
-    const viewLeaves = this.errorNodes();
+  public errorLeavesRecommendedOrder(): ProofNodeIdx[] {
+    const viewLeaves = this.errorLeaves();
 
     const sortErrorsFirst = (leaf: ProofNodeIdx) => {
       const node = this.tree.nodes[leaf];

ide/packages/panoptes/src/print/print.tsx

@@ -120,7 +120,8 @@ export const PrintBodyName = ({ defPath }: { defPath: any }) => {
   return (
     <PrintWithFallback
       object={defPath}
-      Content={() => <UnsafePrintDefPathFull o={defPath} />}
+      // Content={() => <UnsafePrintDefPathFull o={defPath} />}
+      Content={() => <UnsafePrintDefPath o={defPath} />}
     />
   );
 };