Remove subgoals implied by prior errors, filter all errors in a type-…

…checking body

crates/argus-cli/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "argus-cli"
-version = "0.1.9"
+version = "0.1.10"
 edition = "2021"
 authors = ["Gavin Gray <[email protected]>"]
 repository = "https://github.com/cognitive-engineering-lab/argus"
@@ -10,8 +10,8 @@ license = "MIT"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-argus-lib = { version = "0.1.9", path = "../argus" }
-argus-ext = { version = "0.1.9", path = "../argus-ext" }
+argus-lib = { version = "0.1.10", path = "../argus" }
+argus-ext = { version = "0.1.10", path = "../argus-ext" }
 rustc_plugin = "=0.10.0-nightly-2024-05-20"
 
 rustc_utils.workspace = true

crates/argus-ext/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "argus-ext"
-version = "0.1.9"
+version = "0.1.10"
 edition = "2021"
 authors = ["Gavin Gray <[email protected]>"]
 repository = "https://github.com/cognitive-engineering-lab/argus"

crates/argus-ext/src/ty.rs

@@ -8,6 +8,7 @@ use rustc_middle::ty::{self, Predicate, TyCtxt, TypeVisitable, TypeckResults};
 use rustc_span::{FileName, Span};
 use rustc_trait_selection::solve::inspect::InspectCandidate;
 use rustc_utils::source_map::range::CharRange;
+use smallvec::SmallVec;
 
 use crate::EvaluationResult;
 
@@ -101,6 +102,56 @@ pub trait VarCounterExt<'tcx>: TypeVisitable<TyCtxt<'tcx>> {
   fn count_vars(self, tcx: TyCtxt<'tcx>) -> usize;
 }
 
+fn make_failing_bound_implicationp<'a, 'tcx, T>(
+  items: &'a [(usize, &T)],
+  get_predicate: impl Fn(&T) -> Predicate<'tcx> + 'a,
+  get_tcx: impl Fn(&T) -> TyCtxt<'tcx> + 'a,
+) -> impl Fn((usize, &T)) -> bool + 'a {
+  move |(i, other): (usize, &T)| {
+    items.iter().any(|&(j, bound)| {
+      let poly_tp = get_predicate(bound).expect_trait_predicate();
+      if i != j // Don't consider reflexive implication
+        && let ty::TraitPredicate {
+          trait_ref,
+          polarity: ty::PredicatePolarity::Positive,
+        } = poly_tp.skip_binder()
+      {
+        get_tcx(other).does_trait_ref_occur_in(
+          poly_tp.rebind(trait_ref),
+          get_predicate(other),
+        )
+      } else {
+        false
+      }
+    })
+  }
+}
+
+/// If possible, use `retain_error_sources` which sorts and filters in place.
+pub fn identify_error_sources<'tcx, T>(
+  all_items: &[T],
+  get_result: impl Fn(&T) -> EvaluationResult,
+  get_predicate: impl Fn(&T) -> Predicate<'tcx>,
+  get_tcx: impl Fn(&T) -> TyCtxt<'tcx>,
+) -> impl Iterator<Item = usize> + '_ {
+  let (trait_preds, _): (Vec<(usize, &T)>, _) =
+    all_items.iter().enumerate().partition(|(_, t)| {
+      !get_result(t).is_yes() && get_predicate(t).is_trait_predicate()
+    });
+
+  let is_implied_by_failing_bound =
+    make_failing_bound_implicationp(&trait_preds, get_predicate, get_tcx);
+
+  let mut to_keep = SmallVec::<[_; 8]>::default();
+  for t in all_items.iter().enumerate() {
+    if !is_implied_by_failing_bound(t) {
+      to_keep.push(t.0);
+    }
+  }
+
+  to_keep.into_iter()
+}
+
 /// Select only the items that are not implied by another failing bound.
 ///
 /// ## Example:
@@ -116,7 +167,6 @@ pub fn retain_error_sources<'tcx, T>(
   get_result: impl Fn(&T) -> EvaluationResult,
   get_predicate: impl Fn(&T) -> Predicate<'tcx>,
   get_tcx: impl Fn(&T) -> TyCtxt<'tcx>,
-  eq: impl Fn(&T, &T) -> bool,
 ) {
   if all_items.is_empty() {
     return;
@@ -127,34 +177,25 @@ pub fn retain_error_sources<'tcx, T>(
   });
 
   let (trait_preds, _) = all_items.split_at(idx);
+  let trait_preds_enumerated =
+    trait_preds.iter().enumerate().collect::<SmallVec<[_; 8]>>();
 
-  let is_implied_by_failing_bound = |other: &T| {
-    trait_preds.iter().any(|bound| {
-      let poly_tp = get_predicate(bound).expect_trait_predicate();
-      if let ty::TraitPredicate {
-        trait_ref,
-        polarity: ty::PredicatePolarity::Positive,
-      } = poly_tp.skip_binder()
-      // Don't consider reflexive implication
-        && !eq(bound, other)
-      {
-        get_tcx(other).does_trait_ref_occur_in(
-          poly_tp.rebind(trait_ref),
-          get_predicate(other),
-        )
-      } else {
-        false
-      }
-    })
-  };
+  let is_implied_by_failing_bound = make_failing_bound_implicationp(
+    &trait_preds_enumerated,
+    get_predicate,
+    get_tcx,
+  );
 
   let to_remove = &mut vec![];
-  for (i, here) in all_items.iter().enumerate() {
-    if is_implied_by_failing_bound(here) {
-      to_remove.push(i);
+  for t in all_items.iter().enumerate() {
+    if is_implied_by_failing_bound(t) {
+      to_remove.push(t.0);
     }
   }
 
+  drop(is_implied_by_failing_bound);
+  drop(trait_preds_enumerated);
+
   for i in to_remove.iter().rev() {
     all_items.remove(*i);
   }
@@ -165,7 +206,6 @@ pub fn retain_method_calls<'tcx, T>(
   _get_result: impl Fn(&T) -> EvaluationResult,
   get_predicate: impl Fn(&T) -> Predicate<'tcx>,
   get_tcx: impl Fn(&T) -> TyCtxt<'tcx>,
-  _eq: impl Fn(&T, &T) -> bool,
 ) {
   if all_items.is_empty() {
     return;

crates/argus-ser/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "argus-ser"
-version = "0.1.9"
+version = "0.1.10"
 edition = "2021"
 authors = ["Gavin Gray <[email protected]>"]
 repository = "https://github.com/cognitive-engineering-lab/argus"
@@ -28,7 +28,7 @@ smallvec = "1.11.2"
 itertools = "0.12.0"
 ts-rs = { version = "7.1.1", features = ["indexmap-impl"], optional = true }
 index_vec = { version = "0.1.3", features = ["serde"] }
-argus-ext = { version = "0.1.9", path = "../argus-ext" }
+argus-ext = { version = "0.1.10", path = "../argus-ext" }
 
 [dev-dependencies]
 argus-ser = { path = ".", features = ["testing"] }

crates/argus/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "argus-lib"
-version = "0.1.9"
+version = "0.1.10"
 edition = "2021"
 authors = ["Gavin Gray <[email protected]>"]
 repository = "https://github.com/cognitive-engineering-lab/argus"
@@ -21,8 +21,8 @@ fluid-let.workspace = true
 serde.workspace = true
 serde_json.workspace = true
 
-argus-ext = { version = "0.1.9", path = "../argus-ext" }
-argus-ser = { version = "0.1.9", path = "../argus-ser" }
+argus-ext = { version = "0.1.10", path = "../argus-ext" }
+argus-ser = { version = "0.1.10", path = "../argus-ser" }
 index_vec = { version = "0.1.3", features = ["serde"] }
 smallvec = "1.11.2"
 itertools = "0.12.0"
@@ -35,7 +35,7 @@ ts-rs = { version = "7.1.1", features = ["indexmap-impl"], optional = true }
 
 [dev-dependencies]
 argus-lib = { path = ".", features = ["testing"] }
-argus-ser = { version = "0.1.9", path = "../argus-ser", features = ["testing"] }
+argus-ser = { version = "0.1.10", path = "../argus-ser", features = ["testing"] }
 rustc_utils = { version = "=0.10.0-nightly-2024-05-20", features = ["serde", "ts-rs"] }
 test-log = "0.2.11"
 env_logger = "0.9.3"

crates/argus/src/aadebug/mod.rs

@@ -1,5 +1,5 @@
 mod dnf;
-mod tree;
+pub(crate) mod tree;
 mod ty;
 
 use std::time::Instant;

crates/argus/src/aadebug/tree.rs

@@ -297,7 +297,6 @@ impl<'a, 'tcx> Candidate<'a, 'tcx> {
       |g| g.result,
       |g| g.goal.predicate,
       |g| g.infcx.tcx,
-      |a, b| a.idx == b.idx,
     );
 
     all_goals.into_iter()

crates/argus/src/analysis/entry.rs

@@ -204,11 +204,22 @@ pub(in crate::analysis) fn build_obligations_in_body<'tcx>(
   body_id: BodyId,
   typeck_results: &'tcx TypeckResults<'tcx>,
 ) -> (Forgettable<FullData<'tcx>>, ObligationsInBody) {
-  let obligations = tls::take_obligations();
+  let mut obligations = tls::take_obligations();
   let obligation_data = tls::unsafe_take_data();
-
   let obligation_data = FullData::new(obligation_data);
 
+  // XXX: it's possible that Argus reports false negatives. Meaning that
+  // in a body that type checks, failing obligations are reported.
+  // This happens as a result of how predicates are extracted from rustc (ask gavin)
+  // so as a first heuristic, if the body isn't tainted by errors, we'll just remove
+  // all non-successful obligations.
+  if typeck_results.tainted_by_errors.is_none() {
+    log::info!("BODY HAS NO ERRORS");
+    obligations.retain(|prov| prov.it.result.is_yes());
+  } else {
+    log::info!("BODY TAINTED! {:?}", typeck_results.hir_owner);
+  }
+
   let ctx = ErrorAssemblyCtx {
     tcx,
     body_id,

crates/argus/src/analysis/transform.rs

@@ -232,22 +232,20 @@ impl<'a, 'tcx: 'a> ObligationsBuilder<'a, 'tcx> {
       // Filter down the set of obligations as much as possible.
       //
       // 1. Remove obligations that shouldn't have been checked. (I.e., a failed
-      // precondition dissalows it from succeeding.) Hopefully, in the future these
+      // precondition dissallows it from succeeding.) Hopefully, in the future these
       // aren't even solved for.
       retain_error_sources(
         &mut obligations,
         |&i| gfdata(i).result,
         |&i| gfdata(i).obligation.predicate,
         |_| self.tcx,
-        |&a, &b| a == b,
       );
 
       retain_method_calls(
         &mut obligations,
         |&i| gfdata(i).result,
         |&i| gfdata(i).obligation.predicate,
         |_| self.tcx,
-        |&a, &b| a == b,
       );
 
       let obligations = obligations