Skip to content

Commit

Permalink
Introducing obligation implication.
Browse files Browse the repository at this point in the history
Filter ambiguous obligations if a latter (stronger) obligation implies
the result of the former. Use unique candidates for method call tables.
It seems call tables are still shown in the output even if they were successful.
  • Loading branch information
gavinleroy committed Feb 28, 2024
1 parent 014fd73 commit 81f3aff
Show file tree
Hide file tree
Showing 7 changed files with 190 additions and 50 deletions.
18 changes: 13 additions & 5 deletions crates/argus/src/analysis/entry.rs
Original file line number Diff line number Diff line change
Expand Up @@ -61,18 +61,26 @@ pub fn process_obligation<'tcx>(
return;
};

// Use this to get rid of any resolved inference variables,
// these could have been resolved while trying to solve the obligation
// and we want to present it as such to the user.
let obl = &infcx.resolve_vars_if_possible(obl.clone());

// HACK: Remove ambiguous obligations if a "stronger" result was found and
// the predicate implies the previous. This is necessary because we
// can't (currently) distinguish between a subsequent solving attempt
// of a previous obligation.
if result.is_yes() || result.is_no() {
tls::drain_implied_ambiguities(infcx, &obl);
}

if !INCLUDE_SUCCESSES.copied().unwrap_or(false) && result.is_yes() {
log::debug!("Skipping successful obligation {obl:?}");
return;
}

log::debug!("Processing obligation {obl:?}");

// Use this to get rid of any resolved inference variables,
// these could have been resolved while trying to solve the obligation
// and we want to present it as such to the user.
let obl = &infcx.resolve_vars_if_possible(obl.clone());

// TODO: we need to figure out when to save the full data.
// Saving it for every obligation consumes lots of memory
// and this is (one of) the reasons the tool is relatively slow,
Expand Down
120 changes: 82 additions & 38 deletions crates/argus/src/analysis/tls.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,9 @@ pub use unsafe_tls::{
};

use crate::{
ext::InferCtxtExt,
ext::{EvaluationResultExt, InferCtxtExt},
proof_tree::SerializedTree,
rustc::InferCtxtExt as RustcInferCtxtExt,
types::{intermediate::Provenance, Obligation, ObligationHash},
};

Expand All @@ -31,6 +32,70 @@ thread_local! {
static REPORTED_ERRORS: RefCell<FxIndexMap<Span, Vec<ObligationHash>>> = Default::default();
}

pub fn store_obligation(obl: Provenance<Obligation>) {
OBLIGATIONS.with(|obls| {
if obls
.borrow()
.iter()
.find(|o| *o.hash == *obl.hash)
.is_none()
{
obls.borrow_mut().push(obl)
}
})
}

pub fn drain_implied_ambiguities<'tcx>(
infcx: &InferCtxt<'tcx>,
obligation: &PredicateObligation<'tcx>,
) {
OBLIGATIONS.with(|obls| {
obls.borrow_mut().retain(|o| {
// Drain all elements that are:
// 1. Ambiguous, and--
// 2. Implied by the passed obligation
let should_remove = o.result.is_maybe()
&& o
.full_data
.map(|idx| {
unsafe_tls::borrow_in(idx, |fdata| {
fdata.infcx.universe() == infcx.universe()
&& infcx.error_implies(
obligation.predicate.clone(),
fdata.obligation.predicate.clone(),
)
})
})
.unwrap_or(false);
!should_remove
})
})
}

pub fn take_obligations() -> Vec<Provenance<Obligation>> {
OBLIGATIONS.with(|obls| obls.take())
}

pub fn replace_reported_errors(errs: FxIndexMap<Span, Vec<ObligationHash>>) {
REPORTED_ERRORS.with(|rerrs| rerrs.replace(errs));
}

pub fn take_reported_errors() -> FxIndexMap<Span, Vec<ObligationHash>> {
REPORTED_ERRORS.with(|rerrs| rerrs.take())
}

pub fn store_tree(new_tree: SerializedTree) {
TREE.with(|tree| {
if tree.borrow().is_none() {
tree.replace(Some(new_tree));
}
})
}

pub fn take_tree() -> Option<SerializedTree> {
TREE.with(|tree| tree.take())
}

// This is for complex obligations and their inference contexts.
// We don't want to store the entire inference context and obligation for
// every query, so we do it sparingly.
Expand Down Expand Up @@ -88,6 +153,22 @@ mod unsafe_tls {
})
}

// NOTE: ignore the 'tcx lifetime on the resulting reference. This data
// lives as long as the thread does, but the function can only be used
// from within this module so it shouldn't be an issue.
pub(super) fn borrow_in<'tcx, R>(
idx: UODIdx,
f: impl FnOnce(&'tcx FullObligationData<'tcx>) -> R,
) -> R {
OBLIGATION_DATA.with(|data| {
let data = data.borrow();
let ud = data.get(idx);
let d: &'tcx FullObligationData<'tcx> =
unsafe { std::mem::transmute(ud) };
f(d)
})
}

pub fn take<'tcx>() -> IndexVec<UODIdx, FullObligationData<'tcx>> {
OBLIGATION_DATA.with(|data| {
data
Expand All @@ -102,40 +183,3 @@ mod unsafe_tls {
})
}
}

pub fn store_obligation(obl: Provenance<Obligation>) {
OBLIGATIONS.with(|obls| {
if obls
.borrow()
.iter()
.find(|o| *o.hash == *obl.hash)
.is_none()
{
obls.borrow_mut().push(obl)
}
})
}

pub fn take_obligations() -> Vec<Provenance<Obligation>> {
OBLIGATIONS.with(|obls| obls.take())
}

pub fn replace_reported_errors(errs: FxIndexMap<Span, Vec<ObligationHash>>) {
REPORTED_ERRORS.with(|rerrs| rerrs.replace(errs));
}

pub fn take_reported_errors() -> FxIndexMap<Span, Vec<ObligationHash>> {
REPORTED_ERRORS.with(|rerrs| rerrs.take())
}

pub fn store_tree(new_tree: SerializedTree) {
TREE.with(|tree| {
if tree.borrow().is_none() {
tree.replace(Some(new_tree));
}
})
}

pub fn take_tree() -> Option<SerializedTree> {
TREE.with(|tree| tree.take())
}
4 changes: 4 additions & 0 deletions crates/argus/src/analysis/transform.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
use index_vec::IndexVec;
use indexmap::IndexSet;
use itertools::Itertools;
use rustc_data_structures::fx::{FxHashMap as HashMap, FxIndexMap};
use rustc_hir::{self as hir, intravisit::Map, BodyId, HirId};
use rustc_infer::{
Expand Down Expand Up @@ -398,6 +399,9 @@ impl<'a, 'tcx: 'a> ObligationsBuilder<'a, 'tcx> {
})
.unzip();

let trait_candidates =
trait_candidates.into_iter().unique().collect::<Vec<_>>();

let mut param_env = None;
for &idx in &necessary_queries {
let query = self.obligations[idx]
Expand Down
7 changes: 6 additions & 1 deletion crates/argus/src/ext.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ use rustc_middle::ty::{
TypeckResults,
};
use rustc_query_system::ich::StableHashingContext;
use rustc_trait_selection::traits::solve::Certainty;
use rustc_utils::source_map::range::CharRange;
use serde::Serialize;

Expand Down Expand Up @@ -116,6 +117,7 @@ pub trait TypeckResultsExt<'tcx> {

pub trait EvaluationResultExt {
fn is_yes(&self) -> bool;
fn is_maybe(&self) -> bool;
fn is_no(&self) -> bool;
}

Expand Down Expand Up @@ -197,10 +199,13 @@ impl CharRangeExt for CharRange {

impl EvaluationResultExt for EvaluationResult {
fn is_yes(&self) -> bool {
use rustc_trait_selection::traits::solve::Certainty;
matches!(self, EvaluationResult::Ok(Certainty::Yes))
}

fn is_maybe(&self) -> bool {
matches!(self, EvaluationResult::Ok(Certainty::Maybe(..)))
}

fn is_no(&self) -> bool {
matches!(self, EvaluationResult::Err(..))
}
Expand Down
65 changes: 60 additions & 5 deletions crates/argus/src/rustc/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,21 +7,18 @@
//! The goal is that each copied block of code is modified minimally,
//! making replacement easier in the future.

use rustc_infer::{
infer::InferCtxt,
traits::{
query::NoSolution, FulfillmentError,
FulfillmentErrorCode, MismatchedProjectionTypes,
PredicateObligation, SelectionError,
query::NoSolution, FulfillmentError, FulfillmentErrorCode,
MismatchedProjectionTypes, PredicateObligation, SelectionError,
},
};
use rustc_middle::{
ty,
ty::error::{ExpectedFound, TypeError},
};


use crate::types::intermediate::EvaluationResult;

pub mod fn_ctx;
Expand All @@ -38,6 +35,12 @@ pub trait InferCtxtExt<'tcx> {
obligation: &PredicateObligation<'tcx>,
result: EvaluationResult,
) -> Option<FulfillmentError<'tcx>>;

fn error_implies(
&self,
cond: ty::Predicate<'tcx>,
error: ty::Predicate<'tcx>,
) -> bool;
}

impl<'tcx> InferCtxtExt<'tcx> for InferCtxt<'tcx> {
Expand Down Expand Up @@ -111,4 +114,56 @@ impl<'tcx> InferCtxtExt<'tcx> for InferCtxt<'tcx> {
},
)
}

fn error_implies(
&self,
cond: ty::Predicate<'tcx>,
error: ty::Predicate<'tcx>,
) -> bool {
use rustc_middle::ty::ToPolyTraitRef;
use rustc_trait_selection::traits::elaborate;

if cond == error {
return true;
}

// FIXME: It should be possible to deal with `ForAll` in a cleaner way.
let bound_error = error.kind();
let (cond, error) =
match (cond.kind().skip_binder(), bound_error.skip_binder()) {
(
ty::PredicateKind::Clause(ty::ClauseKind::Trait(..)),
ty::PredicateKind::Clause(ty::ClauseKind::Trait(error)),
) => (cond, bound_error.rebind(error)),
_ => {
// FIXME: make this work in other cases too.
return false;
}
};

for pred in elaborate(self.tcx, std::iter::once(cond)) {
let bound_predicate = pred.kind();
if let ty::PredicateKind::Clause(ty::ClauseKind::Trait(implication)) =
bound_predicate.skip_binder()
{
let error = error.to_poly_trait_ref();
let implication = bound_predicate.rebind(implication.trait_ref);
// FIXME: I'm just not taking associated types at all here.
// Eventually I'll need to implement param-env-aware
// `Γ₁ ⊦ φ₁ => Γ₂ ⊦ φ₂` logic.
let param_env = ty::ParamEnv::empty();
if self.can_sub(param_env, error, implication) {
log::debug!(
"error_implies: {:?} -> {:?} -> {:?}",
cond,
error,
implication
);
return true;
}
}
}

false
}
}
23 changes: 23 additions & 0 deletions ide/packages/panoptes/src/BodyInfo.ts
Original file line number Diff line number Diff line change
Expand Up @@ -4,13 +4,16 @@ import {
ExprIdx,
MethodLookup,
MethodLookupIdx,
MethodStep,
Obligation,
ObligationHash,
ObligationIdx,
ObligationsInBody,
} from "@argus/common/bindings";
import _ from "lodash";

import { isObject } from "./utilities/func";

class BodyInfo {
constructor(
private readonly oib: ObligationsInBody,
Expand Down Expand Up @@ -54,6 +57,26 @@ class BodyInfo {
return this.oib.exprs[idx];
}

isErrorMethodCall(expr: Expr): boolean {
if (!(isObject(expr.kind) && "MethodCall" in expr.kind)) {
return false;
}

if (expr.kind.MethodCall.errorRecvr) {
return true;
}

const lookup = this.getMethodLookup(expr.kind.MethodCall.data);

// This is an error method call if there doesn't exist an entry with a result "yes".
return !_.some(lookup.table, step =>
_.some(
step.traitPredicates,
idx => this.getObligation(idx).result === "yes"
)
);
}

visibleObligations(idx: ExprIdx): ObligationIdx[] {
const filtered = _.filter(this.oib.exprs[idx].obligations, i =>
this.notHidden(i)
Expand Down
3 changes: 2 additions & 1 deletion ide/packages/panoptes/src/File.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -218,7 +218,7 @@ const InExpr = ({ idx }: { idx: ExprIdx }) => {
);

if (
!(isObject(expr.kind) && "MethodCall" in expr.kind) &&
!bodyInfo.isErrorMethodCall(expr) &&
bodyInfo.visibleObligations(idx).length === 0
) {
return null;
Expand All @@ -234,6 +234,7 @@ const InExpr = ({ idx }: { idx: ExprIdx }) => {
);

// TODO: we should limit the length of the expression snippet.
// or at the very least syntax highlight it in some way...
const header = <pre>{expr.snippet}</pre>;

const openChildren = idx === highlightedObligation.value?.exprIdx;
Expand Down

0 comments on commit 81f3aff

Please sign in to comment.