diff --git a/crates/argus/src/analysis/entry.rs b/crates/argus/src/analysis/entry.rs index 12e6508..94e9ebf 100644 --- a/crates/argus/src/analysis/entry.rs +++ b/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; } diff --git a/crates/argus/src/analysis/transform.rs b/crates/argus/src/analysis/transform.rs index 3bf3621..d135193 100644 --- a/crates/argus/src/analysis/transform.rs +++ b/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>, bins: Vec, ) -> 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 - }) -} diff --git a/crates/argus/src/proof_tree/ext.rs b/crates/argus/src/proof_tree/ext.rs index 2b4242c..1769212 100644 --- a/crates/argus/src/proof_tree/ext.rs +++ b/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(_), + .. + }) } } diff --git a/crates/argus/src/proof_tree/interners.rs b/crates/argus/src/proof_tree/interners.rs index f70e877..36b5ae5 100644 --- a/crates/argus/src/proof_tree/interners.rs +++ b/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)) } diff --git a/crates/argus/src/proof_tree/mod.rs b/crates/argus/src/proof_tree/mod.rs index 808f839..b8293a1 100644 --- a/crates/argus/src/proof_tree/mod.rs +++ b/crates/argus/src/proof_tree/mod.rs @@ -100,7 +100,6 @@ pub struct SerializedTree { pub results: IndexVec, pub topology: TreeTopology, - pub error_leaves: Vec, pub unnecessary_roots: HashSet, #[serde(skip_serializing_if = "Option::is_none")] pub cycle: Option, diff --git a/crates/argus/src/proof_tree/serialize.rs b/crates/argus/src/proof_tree/serialize.rs index 5bf4492..e6a7187 100644 --- a/crates/argus/src/proof_tree/serialize.rs +++ b/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, pub nodes: IndexVec, pub topology: TreeTopology, - pub error_leaves: Vec, pub unnecessary_roots: HashSet, pub cycle: Option, 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 { + #[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 { 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(()) } diff --git a/ide/packages/panoptes/src/TreeView/BottomUp.tsx b/ide/packages/panoptes/src/TreeView/BottomUp.tsx index e74fe23..09b6418 100644 --- a/ide/packages/panoptes/src/TreeView/BottomUp.tsx +++ b/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}`); } }); diff --git a/ide/packages/panoptes/src/TreeView/TreeApp.tsx b/ide/packages/panoptes/src/TreeView/TreeApp.tsx index 3905c27..b405425 100644 --- a/ide/packages/panoptes/src/TreeView/TreeApp.tsx +++ b/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]); } diff --git a/ide/packages/panoptes/src/TreeView/TreeInfo.ts b/ide/packages/panoptes/src/TreeView/TreeInfo.ts index f2dc51a..fb2b703 100644 --- a/ide/packages/panoptes/src/TreeView/TreeInfo.ts +++ b/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]; diff --git a/ide/packages/panoptes/src/print/print.tsx b/ide/packages/panoptes/src/print/print.tsx index 3bdc9c9..8b71a56 100644 --- a/ide/packages/panoptes/src/print/print.tsx +++ b/ide/packages/panoptes/src/print/print.tsx @@ -120,7 +120,8 @@ export const PrintBodyName = ({ defPath }: { defPath: any }) => { return ( } + // Content={() => } + Content={() => } /> ); };