Skip to content

Commit

Permalink
Analyze const/static bodies, and those from macros.
Browse files Browse the repository at this point in the history
Intern proof tree information.
  • Loading branch information
gavinleroy committed Feb 26, 2024
1 parent cda0077 commit 7f25d7a
Show file tree
Hide file tree
Showing 15 changed files with 265 additions and 146 deletions.
2 changes: 1 addition & 1 deletion crates/argus/src/analysis/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ pub fn obligations<'tcx>(
body_id: BodyId,
) -> Result<ObligationsInBody> {
rustc_middle::ty::print::with_no_trimmed_paths! {{
log::debug!("Typeck'ing body {body_id:?}");
log::info!("Typeck'ing body {body_id:?}");

let typeck_results = tcx.inspect_typeck(body_id, entry::process_obligation);

Expand Down
39 changes: 26 additions & 13 deletions crates/argus/src/analysis/transform.rs
Original file line number Diff line number Diff line change
Expand Up @@ -182,6 +182,11 @@ impl<'a, 'tcx: 'a> ObligationsBuilder<'a, 'tcx> {
);
};

log::info!(
"Building table for method call: {}",
self.tcx.hir().node_to_string(call_expr.hir_id)
);

if let Some((idx, error_recvr, error_call)) = self
.relate_method_call(
call_expr,
Expand All @@ -192,12 +197,14 @@ impl<'a, 'tcx: 'a> ObligationsBuilder<'a, 'tcx> {
&obligations,
)
{
log::info!("built table!");
ambiguous_call = error_recvr || error_call;
MethodCall {
data: idx,
error_recvr,
}
} else {
log::info!("Failed to build table...");
Misc
}
}
Expand Down Expand Up @@ -330,22 +337,24 @@ impl<'a, 'tcx: 'a> ObligationsBuilder<'a, 'tcx> {
let (necessary_queries, trait_candidates): (Vec<_>, Vec<_>) = obligations
.iter()
.filter_map(|&idx| {
let Some(fdata) = self.obligations[idx]
let fdata = self.obligations[idx]
.full_data
.map(|fdidx| self.full_data.get(fdidx))
else {
return None;
};
.map(|fdidx| self.full_data.get(fdidx))?;

let is_necessary = fdata.obligation.predicate.is_trait_predicate() &&
fdata
.infcx
.obligation_necessity(&fdata.obligation)
.is_necessary(fdata.result)
if fdata.obligation.predicate.is_trait_predicate() {
log::info!(
"Predicate is a trait predicate {:?}",
fdata.obligation.predicate
);
}

let is_necessary =
// Bounds for extension method calls are always trait predicates.
fdata.obligation.predicate.is_trait_predicate() &&
// TODO: Obligations for method calls are registered
// usder 'misc,' this of course can change. Find a better
// way to gather the attempted traits!
&& matches!(
matches!(
fdata.obligation.cause.code(),
ObligationCauseCode::MiscObligation
);
Expand Down Expand Up @@ -376,12 +385,16 @@ impl<'a, 'tcx: 'a> ObligationsBuilder<'a, 'tcx> {
}
}

let (full_query_idx, query) =
let Some((full_query_idx, query)) =
necessary_queries.first().and_then(|&idx| {
self.obligations[idx]
.full_data
.map(|fdidx| (fdidx, self.full_data.get(fdidx)))
})?;
})
else {
log::error!("necessary queries empty! {:?}", necessary_queries);
return None;
};

let infcx = &query.infcx;
let o = &query.obligation;
Expand Down
14 changes: 12 additions & 2 deletions crates/argus/src/ext.rs
Original file line number Diff line number Diff line change
Expand Up @@ -370,9 +370,19 @@ impl<'tcx> InferCtxtExt<'tcx> for InferCtxt<'tcx> {
.any(|(_lang_item, def_id)| p.is_trait_pred_rhs(def_id))
};

if !p.is_trait_predicate() {
let is_writeable = || {
use rustc_type_ir::ClauseKind::*;
matches!(
p.kind().skip_binder(),
ty::PredicateKind::Clause(
Trait(..) | RegionOutlives(..) | TypeOutlives(..) | Projection(..)
)
)
};

if !is_writeable() {
ForProfessionals
} else if is_rhs_lang_item() {
} else if p.is_trait_predicate() && is_rhs_lang_item() {
OnError
} else {
Yes
Expand Down
70 changes: 70 additions & 0 deletions crates/argus/src/find_bodies.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
//! This is a copy of the `BodyFinder` from `rustc_utils` but it
//! does *not* skip const/static items. Funny enough, these items
//! often have imporant trait contraints evaluated (think derive macros).
use rustc_hir::{intravisit::Visitor, BodyId};
use rustc_middle::{hir::nested_filter::OnlyBodies, ty::TyCtxt};
use rustc_span::Span;
use rustc_utils::{block_timer, SpanExt};

struct BodyFinder<'tcx> {
tcx: TyCtxt<'tcx>,
bodies: Vec<(Span, BodyId)>,
}

impl<'tcx> Visitor<'tcx> for BodyFinder<'tcx> {
type NestedFilter = OnlyBodies;

fn nested_visit_map(&mut self) -> Self::Map {
self.tcx.hir()
}

fn visit_nested_body(&mut self, id: BodyId) {
let hir = self.nested_visit_map();

// // const/static items are considered to have bodies, so we want to exclude
// // them from our search for functions
// if !hir
// .body_owner_kind(hir.body_owner_def_id(id))
// .is_fn_or_closure()
// {
// return;
// }

let body = hir.body(id);
self.visit_body(body);

let hir = self.tcx.hir();
let span = hir.span_with_body(hir.body_owner(id));
log::trace!(
"Searching body for {:?} with span {span:?} (local {:?})",
self
.tcx
.def_path_debug_str(hir.body_owner_def_id(id).to_def_id()),
span.as_local(body.value.span)
);

self.bodies.push((span, id));
}
}

/// Finds all bodies in the current crate
pub fn find_bodies(tcx: TyCtxt) -> Vec<(Span, BodyId)> {
block_timer!("find_bodies");
let mut finder = BodyFinder {
tcx,
bodies: Vec::new(),
};
tcx.hir().visit_all_item_likes_in_crate(&mut finder);
finder.bodies
}

/// Finds all the bodies that enclose the given span, from innermost to outermost
pub fn find_enclosing_bodies(
tcx: TyCtxt,
sp: Span,
) -> impl Iterator<Item = BodyId> {
let mut bodies = find_bodies(tcx);
bodies.retain(|(other, _)| other.contains(sp));
bodies.sort_by_key(|(span, _)| span.size());
bodies.into_iter().map(|(_, id)| id)
}
2 changes: 2 additions & 0 deletions crates/argus/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,8 @@ extern crate rustc_type_ir;
pub mod analysis;
pub mod emitter;
mod ext;
// TODO: remove when upstreamed to rustc-plugin
pub mod find_bodies;
mod proof_tree;
mod rustc;
mod serialize;
Expand Down
13 changes: 7 additions & 6 deletions crates/argus/src/proof_tree/interners.rs
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ impl Interners {
let result_idx = self.intern_result(goal.result());
let goal = goal.goal();
let goal_idx = self.intern_goal(infcx, &goal, result_idx);
Node::Goal(goal_idx, result_idx)
Node::Goal(goal_idx)
}

pub fn mk_candidate_node<'tcx>(
Expand Down Expand Up @@ -164,6 +164,7 @@ impl Interners {
necessity,
num_vars,
is_lhs_ty_var,
result: result_idx,

#[cfg(debug_assertions)]
debug_comparison: format!("{:?}", goal.predicate.kind().skip_binder()),
Expand Down Expand Up @@ -193,21 +194,21 @@ impl Interners {
return i;
}

let tcx = infcx.tcx;

// First, try to get an impl header from the def_id ty
if let Some(header) = tcx.get_impl_header(def_id) {
if let Some(header) = infcx.tcx.get_impl_header(def_id) {
return self.candidates.insert(
CanKey::Impl(def_id),
CandidateData::new_impl_header(infcx, &header),
);
}

// Second, try to get the span of the impl or just default to a fallback.
let string = tcx
let string = infcx
.tcx
.span_of_impl(def_id)
.map(|sp| {
tcx
infcx
.tcx
.sess
.source_map()
.span_to_snippet(sp)
Expand Down
50 changes: 23 additions & 27 deletions crates/argus/src/proof_tree/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -32,21 +32,34 @@ crate::define_idx! {
ResultIdx
}

// FIXME: Nodes shouldn't be PartialEq, or Eq. They are currently
// so we can "detect cycles" by doing a raw comparison of the nodes.
// Of course, this isn't robust and should be removed ASAP.
//
// Same goes for Candidates and Goals.
#[derive(Serialize, Debug, Clone, PartialEq, Eq)]
#[derive(Serialize, Copy, Clone, Debug, PartialEq, Eq)]
#[cfg_attr(feature = "testing", derive(TS))]
#[cfg_attr(feature = "testing", ts(export))]
pub enum Node {
Result(ResultIdx),
Goal(GoalIdx),
Candidate(CandidateIdx),
Goal(GoalIdx, ResultIdx),
Result(ResultIdx),
}

#[derive(Serialize, Debug, Clone)]
#[serde(rename_all = "camelCase")]
#[cfg_attr(feature = "testing", derive(TS))]
#[cfg_attr(feature = "testing", ts(export))]
pub struct GoalData {
#[cfg_attr(feature = "testing", ts(type = "GoalPredicate"))]
value: serde_json::Value,

necessity: ObligationNecessity,
num_vars: usize,
is_lhs_ty_var: bool,
result: ResultIdx,

#[cfg(debug_assertions)]
#[cfg_attr(feature = "testing", ts(type = "string | undefined"))]
debug_comparison: String,
}

#[derive(Serialize, Clone, Debug, PartialEq, Eq)]
#[derive(Serialize, Clone, Debug)]
#[cfg_attr(feature = "testing", derive(TS))]
#[cfg_attr(feature = "testing", ts(export))]
pub enum CandidateData {
Expand All @@ -58,7 +71,7 @@ pub enum CandidateData {
Any(String),
}

#[derive(Serialize, Clone, Debug, PartialEq, Eq)]
#[derive(Serialize, Clone, Debug)]
#[cfg_attr(feature = "testing", derive(TS))]
#[cfg_attr(feature = "testing", ts(export))]
pub struct ResultData(
Expand All @@ -67,23 +80,6 @@ pub struct ResultData(
EvaluationResult,
);

#[derive(Serialize, Debug, Clone)]
#[serde(rename_all = "camelCase")]
#[cfg_attr(feature = "testing", derive(TS))]
#[cfg_attr(feature = "testing", ts(export))]
pub struct GoalData {
#[cfg_attr(feature = "testing", ts(type = "GoalPredicate"))]
value: serde_json::Value,

necessity: ObligationNecessity,
num_vars: usize,
is_lhs_ty_var: bool,

#[cfg(debug_assertions)]
#[cfg_attr(feature = "testing", ts(type = "string | undefined"))]
debug_comparison: String,
}

#[derive(Serialize, Debug, Clone)]
#[serde(rename_all = "camelCase")]
#[cfg_attr(feature = "testing", derive(TS))]
Expand Down
16 changes: 5 additions & 11 deletions crates/argus/src/proof_tree/serialize.rs
Original file line number Diff line number Diff line change
Expand Up @@ -79,18 +79,12 @@ impl SerializedTreeVisitor {
return;
}

let Node::Goal(from_idx, result) = &self.nodes[from] else {
return;
};

let to_root = self.topology.path_to_root(from);
if to_root.iter_exclusive().any(|idx| {
let Node::Goal(here_idx, hresult) = &self.nodes[*idx] else {
return false;
};

here_idx == from_idx && hresult == result
}) {
let from_node = self.nodes[from];
if to_root
.iter_exclusive()
.any(|middle| self.nodes[*middle] == from_node)
{
self.cycle = Some(to_root.into());
}
}
Expand Down
Loading

0 comments on commit 7f25d7a

Please sign in to comment.