From c943b4db70c2ea2e07cf6aa3a7a480ec0150e12d Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Mon, 4 Nov 2024 17:29:04 +0100 Subject: [PATCH 1/6] Rework the termination check --- creusot/src/translation/traits.rs | 23 ++ creusot/src/validate_terminates.rs | 570 ++++++++++++++++------------- 2 files changed, 346 insertions(+), 247 deletions(-) diff --git a/creusot/src/translation/traits.rs b/creusot/src/translation/traits.rs index 48414236bf..3c443cfa54 100644 --- a/creusot/src/translation/traits.rs +++ b/creusot/src/translation/traits.rs @@ -305,6 +305,29 @@ impl<'tcx> TraitResolved<'tcx> { } } + /// Given a trait and some type parameters, try to find a concrete `impl` block for + /// this trait. + pub(crate) fn impl_id_of_trait( + tcx: TyCtxt<'tcx>, + param_env: ParamEnv<'tcx>, + trait_def_id: DefId, + substs: GenericArgsRef<'tcx>, + ) -> Option { + let trait_ref = TraitRef::from_method(tcx, trait_def_id, substs); + let trait_ref = tcx.normalize_erasing_regions(param_env, trait_ref); + + let Ok(source) = tcx.codegen_select_candidate((param_env, trait_ref)) else { + return None; + }; + trace!("resolve_assoc_item_opt {source:?}",); + match source { + ImplSource::UserDefined(impl_data) => Some(impl_data.impl_def_id), + ImplSource::Param(_) => None, + // TODO: should we return something here, like we do in the above method? + ImplSource::Builtin(_, _) => None, + } + } + pub fn to_opt( self, did: DefId, diff --git a/creusot/src/validate_terminates.rs b/creusot/src/validate_terminates.rs index 98ba482013..a65d5ab496 100644 --- a/creusot/src/validate_terminates.rs +++ b/creusot/src/validate_terminates.rs @@ -20,9 +20,17 @@ //! T::foo(); //! } //! ``` +//! +//! The main idea is that `#[terminates]` functions must be ordonnable: if there exists +//! an order, such that no function can refer to a function defined before, then there +//! can be no cycles. use crate::{ - backend::is_trusted_function, contracts_items, ctx::TranslationCtx, specification::contract_of, + backend::is_trusted_function, + contracts_items, + ctx::TranslationCtx, + pearlite::{TermKind, TermVisitor}, + specification::contract_of, traits::TraitResolved, }; use indexmap::{IndexMap, IndexSet}; @@ -30,7 +38,9 @@ use petgraph::{graph, visit::EdgeRef as _}; use rustc_hir::def_id::{DefId, LocalDefId}; use rustc_middle::{ thir, - ty::{EarlyBinder, FnDef, GenericArgKind, GenericArgs, ParamEnv, TyCtxt, TyKind}, + ty::{ + EarlyBinder, FnDef, GenericArgKind, GenericArgs, GenericArgsRef, ParamEnv, TyCtxt, TyKind, + }, }; use rustc_span::Span; @@ -48,16 +58,21 @@ pub(crate) fn validate_terminates(ctx: &mut TranslationCtx) { // Detect simple recursion, and loops for fun_index in call_graph.node_indices() { - let fun_inst = call_graph.node_weight(fun_index).unwrap(); - let def_id = fun_inst.def_id; + let def_id = call_graph.node_weight(fun_index).unwrap().def_id(); + let function_data = &additional_data[&fun_index]; if let Some(self_edge) = call_graph.edges_connecting(fun_index, fun_index).next() { - let (self_edge, span) = (self_edge.id(), *self_edge.weight()); - if additional_data[&fun_index].is_pearlite { + let (self_edge, call) = (self_edge.id(), *self_edge.weight()); + let span = match call { + CallKind::Direct(span) => span, + _ => continue, + }; + if function_data.is_pearlite { + // Allow simple recursion in logic functions call_graph.remove_edge(self_edge); continue; } call_graph.remove_edge(self_edge); - if !additional_data[&fun_index].has_variant && def_id.is_local() { + if !function_data.has_variant && def_id.is_local() { let fun_span = ctx.tcx.def_span(def_id); let mut error = ctx.error(fun_span, "Recursive function without a `#[variant]` clause"); @@ -65,7 +80,7 @@ pub(crate) fn validate_terminates(ctx: &mut TranslationCtx) { error.emit(); } }; - if let Some(loop_span) = additional_data[&fun_index].has_loops { + if let Some(loop_span) = function_data.has_loops { let fun_span = ctx.tcx.def_span(def_id); let mut error = if contracts_items::is_ghost_closure(ctx.tcx, def_id) { ctx.error(fun_span, "`ghost!` block must not contain loops.") @@ -80,14 +95,16 @@ pub(crate) fn validate_terminates(ctx: &mut TranslationCtx) { // detect mutual recursion let cycles = petgraph::algo::kosaraju_scc(&call_graph); for mut cycle in cycles { - if cycle.iter().all(|n| !call_graph.node_weight(*n).unwrap().def_id.is_local()) { - // The cycle needs to involve at least one function in the current crate. - continue; - } - let Some(root) = cycle.pop() else { + // find a root as a local function + let Some(root_idx) = cycle.iter().position(|n| { + let id = call_graph.node_weight(*n).unwrap().def_id(); + id.is_local() && ctx.def_kind(id).is_fn_like() + }) else { continue; }; - if cycle.is_empty() { + let root = cycle.remove(root_idx); + + if cycle.is_empty() && call_graph.edges_connecting(root, root).count() == 0 { // Need more than 2 components. continue; } @@ -112,10 +129,7 @@ pub(crate) fn validate_terminates(ctx: &mut TranslationCtx) { } }); - cycle.reverse(); - - let root_def_id = call_graph.node_weight(root).unwrap().def_id; - let mut next_instance = root; + let root_def_id = call_graph.node_weight(root).unwrap().def_id(); let mut error = ctx.error( ctx.def_span(root_def_id), &format!( @@ -123,39 +137,37 @@ pub(crate) fn validate_terminates(ctx: &mut TranslationCtx) { ctx.tcx.def_path_str(root_def_id) ), ); - let mut instance; - while let Some(id) = cycle.pop() { - instance = next_instance; - next_instance = id; - if let Some(e) = call_graph.edges_connecting(instance, next_instance).next() { - let span = *e.weight(); - let d1 = call_graph.node_weight(instance).unwrap().def_id; - let d2 = call_graph.node_weight(next_instance).unwrap().def_id; - error.span_note( - span, - format!( - "then `{}` calls `{}`...", - ctx.tcx.def_path_str(d1), - ctx.tcx.def_path_str(d2) - ), - ); + let mut next_node = root; + let mut current_node; + for (idx, &node) in cycle.iter().chain(std::iter::once(&root)).enumerate() { + current_node = next_node; + next_node = node; + let last = idx == cycle.len(); + if let Some(e) = call_graph.edges_connecting(current_node, next_node).next() { + let call = *e.weight(); + let adverb = if last && cycle.len() >= 1 { "finally" } else { "then" }; + let punct = if last { "." } else { "..." }; + let f1 = + ctx.tcx.def_path_str(call_graph.node_weight(current_node).unwrap().def_id()); + let f2 = ctx.tcx.def_path_str(call_graph.node_weight(next_node).unwrap().def_id()); + + match call { + CallKind::Direct(span) => { + error.span_note(span, format!("{adverb} `{f1}` calls `{f2}`{punct}")); + } + CallKind::Ghost => { /* skip the ghost call in the message */ } + CallKind::GenericBound(indirect_id, span) => { + let f3 = ctx.tcx.def_path_str(indirect_id); + error.span_note( + span, + format!( + "{adverb} `{f1}` might call `{f2}` via the call to `{f3}`{punct}" + ), + ); + } + } } } - instance = next_instance; - next_instance = root; - if let Some(e) = call_graph.edges_connecting(instance, next_instance).next() { - let span = *e.weight(); - let d1 = call_graph.node_weight(instance).unwrap().def_id; - let d2 = call_graph.node_weight(next_instance).unwrap().def_id; - error.span_note( - span, - format!( - "finally `{}` calls `{}`.", - ctx.tcx.def_path_str(d1), - ctx.tcx.def_path_str(d2) - ), - ); - } error.emit(); } @@ -163,26 +175,72 @@ pub(crate) fn validate_terminates(ctx: &mut TranslationCtx) { ctx.tcx.dcx().abort_if_errors(); } -struct CallGraph<'tcx> { - graph: graph::DiGraph, Span>, +struct CallGraph { + graph: graph::DiGraph, additional_data: IndexMap, } #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] -struct FunctionInstance<'tcx> { - def_id: DefId, - generic_args: &'tcx GenericArgs<'tcx>, +enum GraphNode { + /// A normal function. + Function(DefId), + /// This node is used in the following case: + /// ``` + /// # macro_rules! ignore { ($($t:tt)*) => {}; } + /// # ignore! { + /// trait Tr { // possibly in another crate + /// #[logic] #[open] fn f() { /* ... */ } + /// } + /// impl Tr {} // in the current crate + /// # } + /// ``` + /// In this case, we create an additional node in the graph, corresponding to the + /// implementation of the default function. + /// + /// # Why though? + /// + /// First, this is sound, because it acts as if the function was actually written in + /// the impl block (with the same definition as the default one). + /// + /// Then we feel this is justified to do this transformation, precisely because the + /// default function is transparent at the point of the impl, so the user can 'see' + /// its definition. + ImplDefaultTransparent { default_function: DefId, impl_block: LocalDefId }, +} +impl GraphNode { + fn def_id(&self) -> DefId { + match self { + GraphNode::Function(def_id) => *def_id, + GraphNode::ImplDefaultTransparent { default_function, .. } => *default_function, + } + } } #[derive(Default)] -struct BuildFunctionsGraph<'tcx> { - graph: graph::DiGraph, Span>, +struct BuildFunctionsGraph { + graph: graph::DiGraph, additional_data: IndexMap, - instance_to_index: IndexMap, graph::NodeIndex>, - to_visit: Vec<(ToVisit<'tcx>, graph::NodeIndex)>, + graph_node_to_index: IndexMap, } -#[derive(Default)] +#[derive(Clone, Copy, Debug)] +enum CallKind { + /// Call of a function. + Direct(Span), + /// Call of the closure inside a `ghost!` block. + Ghost, + /// 'Indirect' call, this is an egde going inside an `impl` block. This happens when + /// calling a generic function while specializing a type. For example: + /// ```rust + /// fn f() { /* ... */ } + /// fn g() { f::(); } // arc from g to `i32::clone` + /// ``` + /// + /// The `DefId` is the one for the generic function, here `f`. + GenericBound(DefId, Span), +} + +#[derive(Debug)] struct FunctionData { /// `true` if the function is a pearlite function (e.g. `#[logic]`). is_pearlite: bool, @@ -197,200 +255,219 @@ struct FunctionData { has_loops: Option, } -impl<'tcx> BuildFunctionsGraph<'tcx> { - /// Insert a new instance function in the graph, or fetch the pre-existing instance. - /// - /// If it wasn't already in the graph, push it onto the `to_visit` stack. - fn insert_instance( - &mut self, - tcx: TyCtxt<'tcx>, - caller_def_id: DefId, - instance: FunctionInstance<'tcx>, - ) -> graph::NodeIndex { - match self.instance_to_index.entry(instance) { +impl BuildFunctionsGraph { + /// Insert a new node in the graph, or fetch an existing node id. + fn insert_function(&mut self, tcx: TyCtxt, graph_node: GraphNode) -> graph::NodeIndex { + let def_id = graph_node.def_id(); + match self.graph_node_to_index.entry(graph_node) { indexmap::map::Entry::Occupied(n) => *n.get(), indexmap::map::Entry::Vacant(entry) => { - let next_visit = if let Some(local) = instance.def_id.as_local() { - ToVisit::Local { function_def_id: local, generic_args: instance.generic_args } - } else { - ToVisit::Extern { - caller_def_id, - function_def_id: instance.def_id, - generic_args: instance.generic_args, - } - }; - let node = self.graph.add_node(instance); + let node = self.graph.add_node(graph_node); self.additional_data.insert( node, FunctionData { - is_pearlite: contracts_items::is_pearlite(tcx, instance.def_id), - has_variant: contracts_items::has_variant_clause(tcx, instance.def_id), + is_pearlite: contracts_items::is_pearlite(tcx, def_id), + has_variant: contracts_items::has_variant_clause(tcx, def_id), has_loops: None, }, ); - self.to_visit.push((next_visit, node)); entry.insert(node); node } } } -} -#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] -enum ToVisit<'tcx> { - /// The function is defined in the crate - Local { function_def_id: LocalDefId, generic_args: &'tcx GenericArgs<'tcx> }, - /// The function is defined in another crate. - /// - /// We keep the generic parameters it was instantiated with, so that trait - /// parameters can be specialized to specific instances. - Extern { caller_def_id: DefId, function_def_id: DefId, generic_args: &'tcx GenericArgs<'tcx> }, -} -impl<'tcx> ToVisit<'tcx> { - fn def_id(&self) -> DefId { - match self { - ToVisit::Local { function_def_id, .. } => function_def_id.to_def_id(), - ToVisit::Extern { function_def_id, .. } => *function_def_id, + /// Process the call from `node` to `called_id`. + fn function_call<'tcx>( + &mut self, + tcx: TyCtxt<'tcx>, + node: graph::NodeIndex, + param_env: ParamEnv<'tcx>, + called_id: DefId, + generic_args: GenericArgsRef<'tcx>, + call_span: Span, + ) { + let (called_id, generic_args) = if TraitResolved::is_trait_item(tcx, called_id) { + match TraitResolved::resolve_item(tcx, param_env, called_id, generic_args) { + TraitResolved::Instance(def_id, subst) => (def_id, subst), + _ => (called_id, generic_args), + } + } else { + (called_id, generic_args) + }; + if contracts_items::is_ghost_from_fn(tcx, called_id) { + // This is a `ghost!` call, so it needs special handling. + let &[_, ty] = generic_args.as_slice() else { + unreachable!(); + }; + let GenericArgKind::Type(ty) = ty.unpack() else { unreachable!() }; + let TyKind::Closure(ghost_def_id, _) = ty.kind() else { unreachable!() }; + + let ghost_node = self.insert_function(tcx, GraphNode::Function(*ghost_def_id)); + self.graph.update_edge(node, ghost_node, CallKind::Ghost); + return; + } + + let (called_node, skip_self_bounds) = if TraitResolved::is_trait_item(tcx, called_id) + && let Some(called_node) = TraitResolved::impl_id_of_trait( + tcx, + param_env, + tcx.trait_of_item(called_id).unwrap(), + generic_args, + ) + .and_then(|id| { + self.graph_node_to_index.get(&GraphNode::ImplDefaultTransparent { + default_function: called_id, + impl_block: id.as_local()?, + }) + }) { + (*called_node, true) + } else { + (self.insert_function(tcx, GraphNode::Function(called_id)), false) + }; + self.graph.update_edge(node, called_node, CallKind::Direct(call_span)); + + // Iterate over the trait bounds of the called function, and assume we call all functions of the corresponding trait if they are specialized. + for bound in tcx.param_env(called_id).caller_bounds() { + let Some(clause) = bound.as_trait_clause() else { continue }; + let clause = tcx.instantiate_bound_regions_with_erased(clause); + let trait_ref = clause.trait_ref; + let subst = trait_ref.args; + let subst = EarlyBinder::bind(subst).instantiate(tcx, generic_args); + + match clause.self_ty().kind() { + rustc_type_ir::TyKind::Param(ty) => { + if ty.index == 0 && skip_self_bounds { + // trait Tr { + // #[logic] fn f() {} + // } + // impl Tr for i32 {} + // + // #[logic] fn g() { + // ::f::() + // } + // + // ==> T: Tr should appear in the bounds, but not Self: Tr. + // TODO: Is this only true for Self? + continue; + } + } + _ => {} + } + + for &item in tcx.associated_item_def_ids(trait_ref.def_id) { + let (item_id, _) = match TraitResolved::resolve_item(tcx, param_env, item, subst) { + TraitResolved::Instance(def_id, subst) => (def_id, subst), + _ => continue, + }; + let item_node = self.insert_function(tcx, GraphNode::Function(item_id)); + self.graph.update_edge( + node, + item_node, + CallKind::GenericBound(called_id, call_span), + ); + } } } } -impl<'tcx> CallGraph<'tcx> { +impl CallGraph { /// Build the call graph of all functions appearing in the current crate, /// exclusively for the purpose of termination checking. /// /// In particular, this means it only contains `#[terminates]` functions. - fn build(ctx: &mut TranslationCtx<'tcx>) -> Self { + fn build(ctx: &mut TranslationCtx) -> Self { + let tcx = ctx.tcx; let mut build_call_graph = BuildFunctionsGraph::default(); - for d in ctx.hir().body_owners() { - if !(contracts_items::is_pearlite(ctx.tcx, d.to_def_id()) - || contract_of(ctx, d.to_def_id()).terminates) - { - // Only consider functions marked with `terminates`: we already ensured that a `terminates` functions only calls other `terminates` functions. - } else { - let generic_args = GenericArgs::identity_for_item(ctx.tcx, d); - let def_id = d.to_def_id(); - build_call_graph.insert_instance( - ctx.tcx, - def_id, - FunctionInstance { def_id, generic_args }, + // Create the `GraphNode::ImplDefaultTransparent` nodes + for (trait_id, impls) in tcx.all_local_trait_impls(()) { + for &impl_id in impls { + let items_in_impl = tcx.impl_item_implementor_ids(impl_id.to_def_id()); + for &item_id in tcx.associated_item_def_ids(trait_id) { + if items_in_impl.contains_key(&item_id) { + continue; + } + let is_transparent = ctx.is_transparent_from( + item_id, + tcx.parent_module_from_def_id(impl_id).to_def_id(), + ); + if !is_transparent || !contracts_items::is_pearlite(tcx, item_id) { + continue; + } + build_call_graph.insert_function( + tcx, + GraphNode::ImplDefaultTransparent { + default_function: item_id, + impl_block: impl_id, + }, + ); + } + } + } + + for (graph_node, node) in build_call_graph.graph_node_to_index.clone() { + let GraphNode::ImplDefaultTransparent { default_function: item_id, impl_block: _ } = + graph_node + else { + continue; + }; + + let param_env = tcx.param_env(item_id); + let term = ctx.term(item_id).unwrap(); + let mut visitor = TermCalls { results: IndexSet::new() }; + visitor.visit_term(term); + + for (called_id, generic_args, call_span) in visitor.results { + // FIXME: weird, why does taking the param_env/generic_args of item_id (aka the function in the *trait*, not the one specialized in the *impl*) works? + // This may not be sound. + build_call_graph.function_call( + tcx, + node, + param_env, + called_id, + generic_args, + call_span, ); } } - while let Some((visit, caller_node)) = build_call_graph.to_visit.pop() { - let caller_def_id = visit.def_id(); - if is_trusted_function(ctx.tcx, caller_def_id) - || contracts_items::is_no_translate(ctx.tcx, caller_def_id) + for local_id in ctx.hir().body_owners() { + if !(contracts_items::is_pearlite(ctx.tcx, local_id.to_def_id()) + || contract_of(ctx, local_id.to_def_id()).terminates) { - // FIXME: does this work with trait functions marked `#[terminates]`/`#[pure]` ? - build_call_graph.additional_data[&caller_node] = - FunctionData { is_pearlite: false, has_variant: false, has_loops: None }; - } else { - match visit { - // Function defined in the current crate: visit its body - ToVisit::Local { function_def_id: local_id, generic_args } => { - let caller_def_id = local_id.to_def_id(); - let param_env = ctx.tcx.param_env(caller_def_id); - let tcx = ctx.tcx; - let (thir, expr) = ctx.thir_body(local_id).unwrap(); - let thir = thir.borrow(); - let mut visitor = FunctionCalls { - thir: &thir, - tcx, - generic_args, - param_env, - calls: IndexSet::new(), - has_loops: None, - }; - ::visit_expr( - &mut visitor, - &thir[expr], - ); - let (visited_calls, has_loops) = (visitor.calls, visitor.has_loops); - - for (function_def_id, span, subst) in visited_calls { - if !ctx.tcx.is_mir_available(function_def_id) { - continue; - } - - let next_node = build_call_graph.insert_instance( - ctx.tcx, - caller_def_id, - FunctionInstance { def_id: function_def_id, generic_args: subst }, - ); - - build_call_graph.graph.add_edge(caller_node, next_node, span); - } - build_call_graph.additional_data[&caller_node].has_loops = has_loops; - } - // Function defined in another crate: assume all the functions corresponding to its trait bounds can be called. - ToVisit::Extern { caller_def_id, function_def_id, generic_args } => { - if contracts_items::is_ghost_from_fn(ctx.tcx, function_def_id) { - // This is a `ghost!` call, so it needs special handling. - let &[_, ty] = generic_args.as_slice() else { - unreachable!(); - }; - let GenericArgKind::Type(ty) = ty.unpack() else { unreachable!() }; - let TyKind::Closure(ghost_def_id, ghost_args_ty) = ty.kind() else { - unreachable!() - }; - build_call_graph.insert_instance( - ctx.tcx, - caller_def_id, - FunctionInstance { - def_id: *ghost_def_id, - generic_args: ghost_args_ty, - }, - ); - } else { - for bound in ctx.tcx.param_env(function_def_id).caller_bounds() { - let Some(clause) = bound.as_trait_clause() else { continue }; - let tcx = ctx.tcx; - let param_env = tcx.param_env(caller_def_id); - let subst = tcx - .instantiate_bound_regions_with_erased(clause) - .trait_ref - .args; - let subst = EarlyBinder::bind(subst).instantiate(tcx, generic_args); - - for &item_id in tcx - .associated_item_def_ids(clause.skip_binder().trait_ref.def_id) - { - if !tcx.def_kind(item_id).is_fn_like() { - continue; - } - - let TraitResolved::Instance(called_id, called_generic_args) = - TraitResolved::resolve_item(tcx, param_env, item_id, subst) - else { - // We could not find a concrete function to call, - // so we don't consider this to be an actual call: we cannot resolve it to any concrete function yet. - continue; - }; - - let span = ctx.tcx.def_span(function_def_id); - let next_node = build_call_graph.insert_instance( - ctx.tcx, - function_def_id, - FunctionInstance { - def_id: called_id, - generic_args: called_generic_args, - }, - ); - - build_call_graph.graph.add_edge(caller_node, next_node, span); - - build_call_graph.additional_data[&next_node].has_variant = - contracts_items::has_variant_clause(ctx.tcx, item_id); - } - } - } - // build_call_graph.additional_data[&caller_node] = - // FunctionData { is_pearlite: false, has_variant: true, has_loops: None }; - } - } + // Only consider functions marked with `terminates`: we already ensured that a `terminates` functions only calls other `terminates` functions. + continue; + } + let def_id = local_id.to_def_id(); + let node = build_call_graph.insert_function(ctx.tcx, GraphNode::Function(def_id)); + + if is_trusted_function(ctx.tcx, def_id) + || contracts_items::is_no_translate(ctx.tcx, def_id) + { + // Cut all arcs from this function. + continue; + } + + let param_env = ctx.tcx.param_env(def_id); + let (thir, expr) = ctx.thir_body(local_id).unwrap(); + let thir = thir.borrow(); + // Collect functions called by this function + let mut visitor = + FunctionCalls { thir: &thir, tcx, calls: IndexSet::new(), has_loops: None }; + ::visit_expr(&mut visitor, &thir[expr]); + + build_call_graph.additional_data[&node].has_loops = visitor.has_loops; + + for (called_id, generic_args, call_span) in visitor.calls { + build_call_graph.function_call( + tcx, + node, + param_env, + called_id, + generic_args, + call_span, + ); } } @@ -402,15 +479,12 @@ impl<'tcx> CallGraph<'tcx> { struct FunctionCalls<'thir, 'tcx> { thir: &'thir thir::Thir<'tcx>, tcx: TyCtxt<'tcx>, - /// Generic arguments that the function was intantiated with. - generic_args: &'tcx GenericArgs<'tcx>, - param_env: ParamEnv<'tcx>, /// Contains: - /// - The id of the _called_ function - /// - The span of the call (for error messages) - /// - The generic arguments instantiating the call - calls: IndexSet<(DefId, Span, &'tcx GenericArgs<'tcx>)>, - /// `true` if the function contains a loop construct. + /// - The id of the _called_ function. + /// - The generic args for this call. + /// - The span of the call (for error messages). + calls: IndexSet<(DefId, &'tcx GenericArgs<'tcx>, Span)>, + /// `Some` if the function contains a loop construct. has_loops: Option, } @@ -422,18 +496,8 @@ impl<'thir, 'tcx> thir::visit::Visitor<'thir, 'tcx> for FunctionCalls<'thir, 'tc fn visit_expr(&mut self, expr: &'thir thir::Expr<'tcx>) { match expr.kind { thir::ExprKind::Call { fun, fn_span, .. } => { - if let &FnDef(def_id, subst) = self.thir[fun].ty.kind() { - let subst = EarlyBinder::bind(self.tcx.erase_regions(subst)) - .instantiate(self.tcx, self.generic_args); - let (def_id, subst) = if TraitResolved::is_trait_item(self.tcx, def_id) { - match TraitResolved::resolve_item(self.tcx, self.param_env, def_id, subst) { - TraitResolved::Instance(id, subst) => (id, subst), - _ => (def_id, subst), - } - } else { - (def_id, subst) - }; - self.calls.insert((def_id, fn_span, subst)); + if let &FnDef(def_id, generic_args) = self.thir[fun].ty.kind() { + self.calls.insert((def_id, generic_args, fn_span)); } } thir::ExprKind::Closure(box thir::ClosureExpr { closure_id, .. }) => { @@ -446,13 +510,12 @@ impl<'thir, 'tcx> thir::visit::Visitor<'thir, 'tcx> for FunctionCalls<'thir, 'tc let mut closure_visitor = FunctionCalls { thir: &thir, tcx: self.tcx, - generic_args: GenericArgs::identity_for_item(self.tcx, closure_id.to_def_id()), - param_env: self.param_env, calls: std::mem::take(&mut self.calls), has_loops: None, }; thir::visit::walk_expr(&mut closure_visitor, &thir[expr]); - self.calls = closure_visitor.calls; + self.calls.extend(closure_visitor.calls); + self.has_loops = self.has_loops.or(closure_visitor.has_loops); } thir::ExprKind::Loop { .. } => self.has_loops = Some(expr.span), _ => {} @@ -460,3 +523,16 @@ impl<'thir, 'tcx> thir::visit::Visitor<'thir, 'tcx> for FunctionCalls<'thir, 'tc thir::visit::walk_expr(self, expr); } } + +struct TermCalls<'tcx> { + results: IndexSet<(DefId, &'tcx GenericArgs<'tcx>, Span)>, +} + +impl<'tcx> TermVisitor<'tcx> for TermCalls<'tcx> { + fn visit_term(&mut self, term: &crate::pearlite::Term<'tcx>) { + crate::pearlite::super_visit_term(term, self); + if let TermKind::Call { id, subst, args: _ } = &term.kind { + self.results.insert((*id, subst, term.span)); + } + } +} From cec2880cce2d0bd0588cb32b4d919cc6593e8b62 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Mon, 11 Nov 2024 14:05:13 +0100 Subject: [PATCH 2/6] Handle default implementations of logical functions --- creusot/src/translation/traits.rs | 4 +- creusot/src/validate_terminates.rs | 273 +++++++++++++++++++---------- 2 files changed, 187 insertions(+), 90 deletions(-) diff --git a/creusot/src/translation/traits.rs b/creusot/src/translation/traits.rs index 3c443cfa54..22433bc43e 100644 --- a/creusot/src/translation/traits.rs +++ b/creusot/src/translation/traits.rs @@ -261,7 +261,7 @@ impl<'tcx> TraitResolved<'tcx> { return TraitResolved::NoInstance; } }; - trace!("resolve_assoc_item_opt {source:?}",); + trace!("TraitResolved::resolve {source:?}",); match source { ImplSource::UserDefined(impl_data) => { @@ -319,7 +319,7 @@ impl<'tcx> TraitResolved<'tcx> { let Ok(source) = tcx.codegen_select_candidate((param_env, trait_ref)) else { return None; }; - trace!("resolve_assoc_item_opt {source:?}",); + trace!("TraitResolved::impl_id_of_trait {source:?}",); match source { ImplSource::UserDefined(impl_data) => Some(impl_data.impl_def_id), ImplSource::Param(_) => None, diff --git a/creusot/src/validate_terminates.rs b/creusot/src/validate_terminates.rs index a65d5ab496..164fcc0573 100644 --- a/creusot/src/validate_terminates.rs +++ b/creusot/src/validate_terminates.rs @@ -24,6 +24,12 @@ //! The main idea is that `#[terminates]` functions must be ordonnable: if there exists //! an order, such that no function can refer to a function defined before, then there //! can be no cycles. +//! +//! # Default function +//! +//! Default function in traits, as well as `impl` blocks marked with `default`, are +//! special-cased when handling logical functions: see the documentation in +//! [`ImplDefaultTransparent`] for more details. use crate::{ backend::is_trusted_function, @@ -36,13 +42,16 @@ use crate::{ use indexmap::{IndexMap, IndexSet}; use petgraph::{graph, visit::EdgeRef as _}; use rustc_hir::def_id::{DefId, LocalDefId}; +use rustc_infer::{infer::TyCtxtInferExt as _, traits::ObligationCause}; use rustc_middle::{ thir, ty::{ - EarlyBinder, FnDef, GenericArgKind, GenericArgs, GenericArgsRef, ParamEnv, TyCtxt, TyKind, + Clauses, EarlyBinder, FnDef, GenericArgKind, GenericArgs, GenericArgsRef, ParamEnv, TyCtxt, + TyKind, }, }; use rustc_span::Span; +use rustc_trait_selection::traits::normalize_param_env_or_error; /// Validate that a `#[terminates]` function cannot loop indefinitely. This includes: /// - forbidding program function from using loops of any kind (this should be relaxed @@ -180,49 +189,65 @@ struct CallGraph { additional_data: IndexMap, } +#[derive(Default)] +struct BuildFunctionsGraph<'tcx> { + graph: graph::DiGraph, + additional_data: IndexMap, + graph_node_to_index: IndexMap, + /// Stores the generic bounds that are left when instantiating the default method in + /// the impl block. + /// + /// This is used to retrieve all the bounds when calling this function. + default_functions_bounds: IndexMap>, + is_default_function: IndexSet, +} + +/// This node is used in the following case: +/// ``` +/// # macro_rules! ignore { ($($t:tt)*) => {}; } +/// # ignore! { +/// trait Tr { // possibly in another crate +/// #[logic] #[open] fn f() { /* ... */ } +/// } +/// impl Tr {} // in the current crate +/// # } +/// ``` +/// In this case, we create an additional node in the graph, corresponding to the +/// implementation of the default function. +/// +/// # Why though? +/// +/// First, this is sound, because it acts as if the function was actually written in +/// the impl block (with the same definition as the default one). +/// +/// Then we feel this is justified to do this transformation, precisely because the +/// default function is transparent at the point of the impl, so the user can 'see' +/// its definition. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +struct ImplDefaultTransparent { + /// The default implementation selected for the impl block. + default_function: DefId, + impl_block: LocalDefId, +} + #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] enum GraphNode { /// A normal function. Function(DefId), - /// This node is used in the following case: - /// ``` - /// # macro_rules! ignore { ($($t:tt)*) => {}; } - /// # ignore! { - /// trait Tr { // possibly in another crate - /// #[logic] #[open] fn f() { /* ... */ } - /// } - /// impl Tr {} // in the current crate - /// # } - /// ``` - /// In this case, we create an additional node in the graph, corresponding to the - /// implementation of the default function. - /// - /// # Why though? - /// - /// First, this is sound, because it acts as if the function was actually written in - /// the impl block (with the same definition as the default one). - /// - /// Then we feel this is justified to do this transformation, precisely because the - /// default function is transparent at the point of the impl, so the user can 'see' - /// its definition. - ImplDefaultTransparent { default_function: DefId, impl_block: LocalDefId }, + + ImplDefaultTransparent(ImplDefaultTransparent), } impl GraphNode { fn def_id(&self) -> DefId { match self { GraphNode::Function(def_id) => *def_id, - GraphNode::ImplDefaultTransparent { default_function, .. } => *default_function, + GraphNode::ImplDefaultTransparent(ImplDefaultTransparent { + default_function, .. + }) => *default_function, } } } -#[derive(Default)] -struct BuildFunctionsGraph { - graph: graph::DiGraph, - additional_data: IndexMap, - graph_node_to_index: IndexMap, -} - #[derive(Clone, Copy, Debug)] enum CallKind { /// Call of a function. @@ -255,7 +280,7 @@ struct FunctionData { has_loops: Option, } -impl BuildFunctionsGraph { +impl<'tcx> BuildFunctionsGraph<'tcx> { /// Insert a new node in the graph, or fetch an existing node id. fn insert_function(&mut self, tcx: TyCtxt, graph_node: GraphNode) -> graph::NodeIndex { let def_id = graph_node.def_id(); @@ -278,7 +303,7 @@ impl BuildFunctionsGraph { } /// Process the call from `node` to `called_id`. - fn function_call<'tcx>( + fn function_call( &mut self, tcx: TyCtxt<'tcx>, node: graph::NodeIndex, @@ -308,52 +333,68 @@ impl BuildFunctionsGraph { return; } - let (called_node, skip_self_bounds) = if TraitResolved::is_trait_item(tcx, called_id) - && let Some(called_node) = TraitResolved::impl_id_of_trait( - tcx, - param_env, - tcx.trait_of_item(called_id).unwrap(), - generic_args, - ) - .and_then(|id| { - self.graph_node_to_index.get(&GraphNode::ImplDefaultTransparent { + let (called_node, bounds, impl_self_bound) = 'bl: { + // this checks if we are calling a function with a default implementation, + // as processed at the beginning of `CallGraph::build`. + 'not_default: { + if !self.is_default_function.contains(&called_id) { + break 'not_default; + }; + let trait_id = match tcx.impl_of_method(called_id) { + Some(id) => { + if let Some(trait_id) = tcx.trait_id_of_impl(id) { + trait_id + } else { + break 'not_default; + } + } + None => { + if let Some(trait_id) = tcx.trait_of_item(called_id) { + trait_id + } else { + break 'not_default; + } + } + }; + let Some(spec_impl_id) = + TraitResolved::impl_id_of_trait(tcx, param_env, trait_id, generic_args) + .and_then(|id| id.as_local()) + else { + break 'not_default; + }; + let default_node = ImplDefaultTransparent { default_function: called_id, - impl_block: id.as_local()?, - }) - }) { - (*called_node, true) - } else { - (self.insert_function(tcx, GraphNode::Function(called_id)), false) + impl_block: spec_impl_id, + }; + let Some(node) = + self.graph_node_to_index.get(&GraphNode::ImplDefaultTransparent(default_node)) + else { + break 'not_default; + }; + let bounds = self.default_functions_bounds[&default_node]; + let self_bound = tcx.impl_trait_header(spec_impl_id); + break 'bl (*node, bounds, self_bound); + } + ( + self.insert_function(tcx, GraphNode::Function(called_id)), + tcx.param_env(called_id).caller_bounds(), + None, + ) }; self.graph.update_edge(node, called_node, CallKind::Direct(call_span)); // Iterate over the trait bounds of the called function, and assume we call all functions of the corresponding trait if they are specialized. - for bound in tcx.param_env(called_id).caller_bounds() { + for bound in bounds { let Some(clause) = bound.as_trait_clause() else { continue }; let clause = tcx.instantiate_bound_regions_with_erased(clause); let trait_ref = clause.trait_ref; - let subst = trait_ref.args; - let subst = EarlyBinder::bind(subst).instantiate(tcx, generic_args); - - match clause.self_ty().kind() { - rustc_type_ir::TyKind::Param(ty) => { - if ty.index == 0 && skip_self_bounds { - // trait Tr { - // #[logic] fn f() {} - // } - // impl Tr for i32 {} - // - // #[logic] fn g() { - // ::f::() - // } - // - // ==> T: Tr should appear in the bounds, but not Self: Tr. - // TODO: Is this only true for Self? - continue; - } + if let Some(self_bound) = &impl_self_bound { + let self_trait_ref = self_bound.trait_ref.instantiate_identity(); + if trait_ref == self_trait_ref { + continue; } - _ => {} } + let subst = EarlyBinder::bind(trait_ref.args).instantiate(tcx, generic_args); for &item in tcx.associated_item_def_ids(trait_ref.def_id) { let (item_id, _) = match TraitResolved::resolve_item(tcx, param_env, item, subst) { @@ -380,53 +421,109 @@ impl CallGraph { let tcx = ctx.tcx; let mut build_call_graph = BuildFunctionsGraph::default(); - // Create the `GraphNode::ImplDefaultTransparent` nodes + let mut specialization_nodes = IndexMap::new(); + // Create the `GraphNode::ImplDefaultTransparent` nodes. for (trait_id, impls) in tcx.all_local_trait_impls(()) { - for &impl_id in impls { - let items_in_impl = tcx.impl_item_implementor_ids(impl_id.to_def_id()); + for &impl_local_id in impls { + let module_id = tcx.parent_module_from_def_id(impl_local_id).to_def_id(); + let impl_id = impl_local_id.to_def_id(); + let items_in_impl = tcx.impl_item_implementor_ids(impl_id); + for &item_id in tcx.associated_item_def_ids(trait_id) { if items_in_impl.contains_key(&item_id) { + // The function is explicitely implemented, skip continue; } - let is_transparent = ctx.is_transparent_from( - item_id, - tcx.parent_module_from_def_id(impl_id).to_def_id(), - ); - if !is_transparent || !contracts_items::is_pearlite(tcx, item_id) { + + let default_item = { + let trait_def = tcx.trait_def(trait_id); + let leaf_def = trait_def + .ancestors(tcx, impl_id) + .unwrap() + .leaf_def(tcx, item_id) + .unwrap_or_else(|| { + unreachable!( + "no definition found for item {} in impl {}", + tcx.def_path_str(item_id), + tcx.def_path_str(impl_id) + ); + }); + leaf_def + }; + let default_item_id = default_item.item.def_id; + + let is_transparent = ctx.is_transparent_from(default_item_id, module_id); + if !is_transparent || !contracts_items::is_pearlite(tcx, default_item_id) { + // only consider item that are: + // - transparent from the POV of the impl block + // - logical items continue; } + specialization_nodes.insert((default_item_id, impl_local_id), default_item); build_call_graph.insert_function( tcx, - GraphNode::ImplDefaultTransparent { - default_function: item_id, - impl_block: impl_id, - }, + GraphNode::ImplDefaultTransparent(ImplDefaultTransparent { + default_function: default_item_id, + impl_block: impl_local_id, + }), ); } } } for (graph_node, node) in build_call_graph.graph_node_to_index.clone() { - let GraphNode::ImplDefaultTransparent { default_function: item_id, impl_block: _ } = - graph_node - else { + let GraphNode::ImplDefaultTransparent(graph_node) = graph_node else { continue; }; + let ImplDefaultTransparent { default_function: item_id, impl_block: impl_id } = + graph_node; + let specialization_node = &specialization_nodes[&(item_id, impl_id)]; - let param_env = tcx.param_env(item_id); + let impl_id = impl_id.to_def_id(); + let param_env = tcx.param_env(impl_id); let term = ctx.term(item_id).unwrap(); let mut visitor = TermCalls { results: IndexSet::new() }; visitor.visit_term(term); + // Instantiate the generic args according to the specialization of the impl. + + let trait_id = tcx.trait_id_of_impl(impl_id).unwrap(); + + // Now, translate the args to match the trait. + let infcx = tcx.infer_ctxt().build(); + let impl_args = rustc_trait_selection::traits::translate_args( + &infcx, + param_env, + impl_id, + GenericArgs::identity_for_item(tcx, impl_id), + specialization_node.defining_node, + ); + + // Take the generic arguments of the default function, instantiated with + // the type parameters from the impl block. + let func_impl_args = + GenericArgs::identity_for_item(tcx, item_id).rebase_onto(tcx, trait_id, impl_args); + + // data for when we call this function + build_call_graph.is_default_function.insert(item_id); + let item_param_env = tcx.param_env(item_id); + let item_param_env = EarlyBinder::bind(item_param_env).instantiate(tcx, func_impl_args); + let bounds = + normalize_param_env_or_error(tcx, item_param_env, ObligationCause::dummy()) + .caller_bounds(); + build_call_graph.default_functions_bounds.insert(graph_node, bounds); + for (called_id, generic_args, call_span) in visitor.results { - // FIXME: weird, why does taking the param_env/generic_args of item_id (aka the function in the *trait*, not the one specialized in the *impl*) works? - // This may not be sound. + // Instantiate the args for the call with the context we just built up. + let actual_args = EarlyBinder::bind(tcx.erase_regions(generic_args)) + .instantiate(tcx, func_impl_args); + build_call_graph.function_call( tcx, node, param_env, called_id, - generic_args, + actual_args, call_span, ); } From ac129444eee8142360eb920b119c0c67512d9b26 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Tue, 12 Nov 2024 15:03:56 +0100 Subject: [PATCH 3/6] Forbid `default` on logical and terminates functions --- creusot-contracts-proc/src/lib.rs | 29 ++++++++++++++++++++++++++++- 1 file changed, 28 insertions(+), 1 deletion(-) diff --git a/creusot-contracts-proc/src/lib.rs b/creusot-contracts-proc/src/lib.rs index d8513120bb..a5a1a36d8b 100644 --- a/creusot-contracts-proc/src/lib.rs +++ b/creusot-contracts-proc/src/lib.rs @@ -426,6 +426,17 @@ pub fn snapshot(assertion: TS1) -> TS1 { #[proc_macro_attribute] pub fn terminates(_: TS1, tokens: TS1) -> TS1 { let documentation = document_spec("terminates", TS1::new()); + if let Ok(item) = syn::parse::(tokens.clone()) { + if let Some(def) = item.defaultness { + return syn::Error::new( + def.span(), + "`terminates` functions cannot use the `default` modifier", + ) + .into_compile_error() + .into(); + } + }; + let mut result = TS1::from(quote! { #[creusot::clause::terminates] #documentation }); result.extend(tokens); result @@ -434,6 +445,16 @@ pub fn terminates(_: TS1, tokens: TS1) -> TS1 { #[proc_macro_attribute] pub fn pure(_: TS1, tokens: TS1) -> TS1 { let documentation = document_spec("pure", TS1::new()); + if let Ok(item) = syn::parse::(tokens.clone()) { + if let Some(def) = item.defaultness { + return syn::Error::new( + def.span(), + "`pure` functions cannot use the `default` modifier", + ) + .into_compile_error() + .into(); + } + }; let mut result = TS1::from( quote! { #[creusot::clause::no_panic] #[creusot::clause::terminates] #documentation }, ); @@ -474,7 +495,13 @@ impl Parse for LogicInput { let attrs = input.call(Attribute::parse_outer)?; // Infalliable, no visibility = inherited let vis: Visibility = input.parse()?; - let default = input.parse()?; + let default: Option<_> = input.parse()?; + if default.is_some() { + return Err(syn::Error::new( + input.span(), + "logical functions cannot use the `default` modifier", + )); + } let sig: Signature = input.parse()?; let lookahead = input.lookahead1(); if lookahead.peek(Token![;]) { From 2433a4203e15c7476c5c6fe516755bf35922afb8 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Tue, 12 Nov 2024 15:05:50 +0100 Subject: [PATCH 4/6] Add tests --- .../terminates/default_function_non_logic.rs | 16 +++++++ .../default_function_non_logic.stderr | 14 ++++++ .../terminates/default_function_non_open.rs | 21 +++++++++ .../default_function_non_open.stderr | 14 ++++++ .../terminates/loop_through_default_impl.rs | 35 +++++++++++++++ .../loop_through_default_impl.stderr | 24 ++++++++++ .../termination/call_in_contract.coma | 16 +++++++ .../termination/call_in_contract.rs | 17 +++++++ .../termination/default_impl.coma | 6 +++ .../termination/default_impl.rs | 28 ++++++++++++ .../termination/default_impl_in_trait.coma | 9 ++++ .../termination/default_impl_in_trait.rs | 45 +++++++++++++++++++ 12 files changed, 245 insertions(+) create mode 100644 creusot/tests/should_fail/terminates/default_function_non_logic.rs create mode 100644 creusot/tests/should_fail/terminates/default_function_non_logic.stderr create mode 100644 creusot/tests/should_fail/terminates/default_function_non_open.rs create mode 100644 creusot/tests/should_fail/terminates/default_function_non_open.stderr create mode 100644 creusot/tests/should_fail/terminates/loop_through_default_impl.rs create mode 100644 creusot/tests/should_fail/terminates/loop_through_default_impl.stderr create mode 100644 creusot/tests/should_succeed/termination/call_in_contract.coma create mode 100644 creusot/tests/should_succeed/termination/call_in_contract.rs create mode 100644 creusot/tests/should_succeed/termination/default_impl.coma create mode 100644 creusot/tests/should_succeed/termination/default_impl.rs create mode 100644 creusot/tests/should_succeed/termination/default_impl_in_trait.coma create mode 100644 creusot/tests/should_succeed/termination/default_impl_in_trait.rs diff --git a/creusot/tests/should_fail/terminates/default_function_non_logic.rs b/creusot/tests/should_fail/terminates/default_function_non_logic.rs new file mode 100644 index 0000000000..6ebdfd7adf --- /dev/null +++ b/creusot/tests/should_fail/terminates/default_function_non_logic.rs @@ -0,0 +1,16 @@ +extern crate creusot_contracts; +use creusot_contracts::*; + +trait Foo { + #[terminates] + fn f() {} + #[terminates] + fn g(); +} + +impl Foo for i32 { + #[terminates] + fn g() { + Self::f(); // this assumes f could call g + } +} diff --git a/creusot/tests/should_fail/terminates/default_function_non_logic.stderr b/creusot/tests/should_fail/terminates/default_function_non_logic.stderr new file mode 100644 index 0000000000..ea1dc75740 --- /dev/null +++ b/creusot/tests/should_fail/terminates/default_function_non_logic.stderr @@ -0,0 +1,14 @@ +error: Mutually recursive functions: when calling `::g`... + --> default_function_non_logic.rs:13:5 + | +13 | fn g() { + | ^^^^^^ + | +note: then `::g` might call `::g` via the call to `Foo::f`. + --> default_function_non_logic.rs:14:9 + | +14 | Self::f(); // this assumes f could call g + | ^^^^^^^^^ + +error: aborting due to 1 previous error + diff --git a/creusot/tests/should_fail/terminates/default_function_non_open.rs b/creusot/tests/should_fail/terminates/default_function_non_open.rs new file mode 100644 index 0000000000..7832b56875 --- /dev/null +++ b/creusot/tests/should_fail/terminates/default_function_non_open.rs @@ -0,0 +1,21 @@ +extern crate creusot_contracts; +use creusot_contracts::*; + +mod inner { + use super::*; + pub(super) trait Foo { + #[open(self)] + #[logic] + fn f() {} + #[logic] + fn g(); + } +} + +impl inner::Foo for i32 { + #[open(self)] + #[logic] + fn g() { + Self::f(); // this assumes f could call g + } +} diff --git a/creusot/tests/should_fail/terminates/default_function_non_open.stderr b/creusot/tests/should_fail/terminates/default_function_non_open.stderr new file mode 100644 index 0000000000..976b5fb5cd --- /dev/null +++ b/creusot/tests/should_fail/terminates/default_function_non_open.stderr @@ -0,0 +1,14 @@ +error: Mutually recursive functions: when calling `::g`... + --> default_function_non_open.rs:18:5 + | +18 | fn g() { + | ^^^^^^ + | +note: then `::g` might call `::g` via the call to `inner::Foo::f`. + --> default_function_non_open.rs:19:9 + | +19 | Self::f(); // this assumes f could call g + | ^^^^^^^^^ + +error: aborting due to 1 previous error + diff --git a/creusot/tests/should_fail/terminates/loop_through_default_impl.rs b/creusot/tests/should_fail/terminates/loop_through_default_impl.rs new file mode 100644 index 0000000000..bb874c190d --- /dev/null +++ b/creusot/tests/should_fail/terminates/loop_through_default_impl.rs @@ -0,0 +1,35 @@ +#![allow(incomplete_features)] +#![feature(specialization)] + +extern crate creusot_contracts; +use creusot_contracts::*; + +pub trait Foo { + #[logic] + fn f(); + #[logic] + fn g(); +} +default impl Foo for T { + #[logic] + #[open] + fn f() { + h(); + } + #[logic] + #[open] + fn g() {} +} +impl Foo for i32 { + #[logic] + #[open] + fn g() { + Self::f(); + } +} + +#[logic] +#[open] +pub fn h() { + ::g(); +} diff --git a/creusot/tests/should_fail/terminates/loop_through_default_impl.stderr b/creusot/tests/should_fail/terminates/loop_through_default_impl.stderr new file mode 100644 index 0000000000..0a8dd93193 --- /dev/null +++ b/creusot/tests/should_fail/terminates/loop_through_default_impl.stderr @@ -0,0 +1,24 @@ +error: Mutually recursive functions: when calling `::f`... + --> loop_through_default_impl.rs:16:5 + | +16 | fn f() { + | ^^^^^^ + | +note: then `::f` calls `h`... + --> loop_through_default_impl.rs:17:9 + | +17 | h(); + | ^^^ +note: then `h` calls `::g`... + --> loop_through_default_impl.rs:34:5 + | +34 | ::g(); + | ^^^^^^^^^^^^^^^^^ +note: finally `::g` calls `::f`. + --> loop_through_default_impl.rs:27:9 + | +27 | Self::f(); + | ^^^^^^^^^ + +error: aborting due to 1 previous error + diff --git a/creusot/tests/should_succeed/termination/call_in_contract.coma b/creusot/tests/should_succeed/termination/call_in_contract.coma new file mode 100644 index 0000000000..611d1b972e --- /dev/null +++ b/creusot/tests/should_succeed/termination/call_in_contract.coma @@ -0,0 +1,16 @@ +module M_call_in_contract__qyi17587776295821317810__g [#"call_in_contract.rs" 16 4 16 10] (* <() as Foo> *) + let%span scall_in_contract0 = "call_in_contract.rs" 14 14 14 29 + let%span scall_in_contract1 = "call_in_contract.rs" 5 4 5 12 + + function f'0 [#"call_in_contract.rs" 7 4 7 10] (_1 : ()) : () = + [%#scall_in_contract1] () + + constant _1 : () + + function g [#"call_in_contract.rs" 16 4 16 10] (_1 : ()) : () + + goal vc_g : [%#scall_in_contract0] f'0 () = () +end +module M_call_in_contract__qyi17587776295821317810 [#"call_in_contract.rs" 12 0 12 15] (* <() as Foo> *) + +end diff --git a/creusot/tests/should_succeed/termination/call_in_contract.rs b/creusot/tests/should_succeed/termination/call_in_contract.rs new file mode 100644 index 0000000000..6401457c1d --- /dev/null +++ b/creusot/tests/should_succeed/termination/call_in_contract.rs @@ -0,0 +1,17 @@ +extern crate creusot_contracts; +use creusot_contracts::*; + +pub trait Foo { + #[logic] + #[open(self)] + fn f() {} + #[logic] + fn g(); +} + +impl Foo for () { + #[logic] + #[ensures(Self::f() == ())] + #[open(self)] + fn g() {} +} diff --git a/creusot/tests/should_succeed/termination/default_impl.coma b/creusot/tests/should_succeed/termination/default_impl.coma new file mode 100644 index 0000000000..7f2e6866b6 --- /dev/null +++ b/creusot/tests/should_succeed/termination/default_impl.coma @@ -0,0 +1,6 @@ +module M_default_impl__qyi15103138194754375473 [#"default_impl.rs" 13 0 13 25] (* *) + type t +end +module M_default_impl__qyi10933213094149945493 [#"default_impl.rs" 22 0 22 15] (* <() as Foo> *) + +end diff --git a/creusot/tests/should_succeed/termination/default_impl.rs b/creusot/tests/should_succeed/termination/default_impl.rs new file mode 100644 index 0000000000..f0e59d5221 --- /dev/null +++ b/creusot/tests/should_succeed/termination/default_impl.rs @@ -0,0 +1,28 @@ +#![allow(incomplete_features)] +#![feature(specialization)] + +extern crate creusot_contracts; +use creusot_contracts::*; + +pub trait Foo { + #[logic] + fn f(); + #[logic] + fn g(); +} +default impl Foo for T { + #[logic] + #[open] + fn f() {} + #[logic] + #[open] + fn g() {} +} + +impl Foo for () { + #[logic] + #[open] + fn g() { + Self::f(); + } +} diff --git a/creusot/tests/should_succeed/termination/default_impl_in_trait.coma b/creusot/tests/should_succeed/termination/default_impl_in_trait.coma new file mode 100644 index 0000000000..2f76ec5d26 --- /dev/null +++ b/creusot/tests/should_succeed/termination/default_impl_in_trait.coma @@ -0,0 +1,9 @@ +module M_default_impl_in_trait__qyi3507169229755221981 [#"default_impl_in_trait.rs" 23 0 23 15] (* <() as Foo> *) + +end +module M_default_impl_in_trait__qyi3449993250961155471 [#"default_impl_in_trait.rs" 31 0 31 22] (* as Foo> *) + type t +end +module M_default_impl_in_trait__qyi7271716577078185416 [#"default_impl_in_trait.rs" 39 0 39 22] (* <() as inner::Bar> *) + +end diff --git a/creusot/tests/should_succeed/termination/default_impl_in_trait.rs b/creusot/tests/should_succeed/termination/default_impl_in_trait.rs new file mode 100644 index 0000000000..6ab98ba3ef --- /dev/null +++ b/creusot/tests/should_succeed/termination/default_impl_in_trait.rs @@ -0,0 +1,45 @@ +extern crate creusot_contracts; +use creusot_contracts::*; + +pub trait Foo { + #[logic] + #[open(self)] + fn f() {} + #[logic] + fn g(); +} + +pub mod inner { + use super::*; + pub trait Bar { + #[logic] + #[open(super)] + fn f() {} + #[logic] + fn g(); + } +} + +impl Foo for () { + #[logic] + #[open(self)] + fn g() { + ::f(); + } +} + +impl Foo for Box { + #[logic] + #[open(self)] + fn g() { + ::f(); + } +} + +impl inner::Bar for () { + #[logic] + #[open(self)] + fn g() { + ::f(); + } +} From d9a63c00821139d5722c6f8209b8e2931648b644 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Tue, 12 Nov 2024 15:06:03 +0100 Subject: [PATCH 5/6] Update tests --- creusot/tests/should_fail/cycle.stderr | 20 ++++----- .../should_fail/ghost/non_terminating.stderr | 20 ++++----- .../complicated_traits_recursion.stderr | 18 +++----- .../terminates/mutual_recursion.stderr | 20 ++++----- .../terminates/mutual_recursion_trait.stderr | 20 ++++----- .../recursion_through_contract.stderr | 40 +++++++++--------- .../call_in_contract/why3session.xml | 14 ++++++ .../call_in_contract/why3shapes.gz | Bin 0 -> 105 bytes .../termination/default_impl/why3session.xml | 8 ++++ .../termination/default_impl/why3shapes.gz | Bin 0 -> 45 bytes .../default_impl_in_trait/why3session.xml | 8 ++++ .../default_impl_in_trait/why3shapes.gz | Bin 0 -> 45 bytes 12 files changed, 95 insertions(+), 73 deletions(-) create mode 100644 creusot/tests/should_succeed/termination/call_in_contract/why3session.xml create mode 100644 creusot/tests/should_succeed/termination/call_in_contract/why3shapes.gz create mode 100644 creusot/tests/should_succeed/termination/default_impl/why3session.xml create mode 100644 creusot/tests/should_succeed/termination/default_impl/why3shapes.gz create mode 100644 creusot/tests/should_succeed/termination/default_impl_in_trait/why3session.xml create mode 100644 creusot/tests/should_succeed/termination/default_impl_in_trait/why3shapes.gz diff --git a/creusot/tests/should_fail/cycle.stderr b/creusot/tests/should_fail/cycle.stderr index cdc6ee11ae..9a066437f3 100644 --- a/creusot/tests/should_fail/cycle.stderr +++ b/creusot/tests/should_fail/cycle.stderr @@ -1,19 +1,19 @@ -error: Mutually recursive functions: when calling `g`... - --> cycle.rs:12:1 +error: Mutually recursive functions: when calling `f`... + --> cycle.rs:6:1 | -12 | pub fn g(x: bool) { - | ^^^^^^^^^^^^^^^^^ +6 | pub fn f() { + | ^^^^^^^^^^ | -note: then `g` calls `f`... - --> cycle.rs:14:9 - | -14 | f(); - | ^^^ -note: finally `f` calls `g`. +note: then `f` calls `g`... --> cycle.rs:7:5 | 7 | g(true); | ^^^^^^^ +note: finally `g` calls `f`. + --> cycle.rs:14:9 + | +14 | f(); + | ^^^ error: aborting due to 1 previous error diff --git a/creusot/tests/should_fail/ghost/non_terminating.stderr b/creusot/tests/should_fail/ghost/non_terminating.stderr index 068db4028b..a31f2b69fa 100644 --- a/creusot/tests/should_fail/ghost/non_terminating.stderr +++ b/creusot/tests/should_fail/ghost/non_terminating.stderr @@ -27,22 +27,22 @@ note: looping occurs here | ^^^^^^^ = note: this error originates in the macro `ghost` (in Nightly builds, run with -Z macro-backtrace for more info) -error: Mutually recursive functions: when calling `f`... - --> non_terminating.rs:13:1 +error: Mutually recursive functions: when calling `recursive`... + --> non_terminating.rs:5:1 | -13 | fn f() { - | ^^^^^^ +5 | pub fn recursive() { + | ^^^^^^^^^^^^^^^^^^ | -note: then `f` calls `recursive`... - --> non_terminating.rs:14:5 - | -14 | recursive(); - | ^^^^^^^^^^^ -note: finally `recursive` calls `f`. +note: then `recursive` calls `f`... --> non_terminating.rs:7:9 | 7 | f(); | ^^^ +note: finally `f` calls `recursive`. + --> non_terminating.rs:14:5 + | +14 | recursive(); + | ^^^^^^^^^^^ error: aborting due to 2 previous errors; 1 warning emitted diff --git a/creusot/tests/should_fail/terminates/complicated_traits_recursion.stderr b/creusot/tests/should_fail/terminates/complicated_traits_recursion.stderr index bef6bfefea..7c53ccb0bf 100644 --- a/creusot/tests/should_fail/terminates/complicated_traits_recursion.stderr +++ b/creusot/tests/should_fail/terminates/complicated_traits_recursion.stderr @@ -1,18 +1,10 @@ -error: Mutually recursive functions: when calling `bar`... - --> complicated_traits_recursion.rs:18:1 +error: Mutually recursive functions: when calling `::foo`... + --> complicated_traits_recursion.rs:12:5 | -18 | / fn bar(_: I) -19 | | where -20 | | I: Iterator, -21 | | I::Item: Foo, - | |_________________^ +12 | fn foo() { + | ^^^^^^^^ | -note: then `bar` calls `::foo`... - --> complicated_traits_recursion.rs:23:5 - | -23 | I::Item::foo() - | ^^^^^^^^^^^^^^ -note: finally `::foo` calls `bar`. +note: then `::foo` might call `::foo` via the call to `bar`. --> complicated_traits_recursion.rs:13:9 | 13 | bar::>(std::iter::once(1i32)); diff --git a/creusot/tests/should_fail/terminates/mutual_recursion.stderr b/creusot/tests/should_fail/terminates/mutual_recursion.stderr index 8ecf6c8920..46599986fb 100644 --- a/creusot/tests/should_fail/terminates/mutual_recursion.stderr +++ b/creusot/tests/should_fail/terminates/mutual_recursion.stderr @@ -1,24 +1,24 @@ -error: Mutually recursive functions: when calling `f3`... - --> mutual_recursion.rs:18:1 +error: Mutually recursive functions: when calling `m::f1`... + --> mutual_recursion.rs:7:5 | -18 | fn f3() { - | ^^^^^^^ +7 | pub fn f1() { + | ^^^^^^^^^^^ | -note: then `f3` calls `m::f1`... - --> mutual_recursion.rs:19:5 - | -19 | m::f1(); - | ^^^^^^^ note: then `m::f1` calls `f2`... --> mutual_recursion.rs:8:9 | 8 | super::f2(); | ^^^^^^^^^^^ -note: finally `f2` calls `f3`. +note: then `f2` calls `f3`... --> mutual_recursion.rs:14:5 | 14 | f3(); | ^^^^ +note: finally `f3` calls `m::f1`. + --> mutual_recursion.rs:19:5 + | +19 | m::f1(); + | ^^^^^^^ error: aborting due to 1 previous error diff --git a/creusot/tests/should_fail/terminates/mutual_recursion_trait.stderr b/creusot/tests/should_fail/terminates/mutual_recursion_trait.stderr index 7724627ac2..6c41fe4b88 100644 --- a/creusot/tests/should_fail/terminates/mutual_recursion_trait.stderr +++ b/creusot/tests/should_fail/terminates/mutual_recursion_trait.stderr @@ -1,19 +1,19 @@ -error: Mutually recursive functions: when calling `bar`... - --> mutual_recursion_trait.rs:18:1 +error: Mutually recursive functions: when calling `::foo`... + --> mutual_recursion_trait.rs:12:5 | -18 | fn bar() { - | ^^^^^^^^ +12 | fn foo() { + | ^^^^^^^^ | -note: then `bar` calls `::foo`... - --> mutual_recursion_trait.rs:19:5 - | -19 | ::foo(); - | ^^^^^^^^^^^^^^^^^^^ -note: finally `::foo` calls `bar`. +note: then `::foo` calls `bar`... --> mutual_recursion_trait.rs:13:9 | 13 | bar(); | ^^^^^ +note: finally `bar` calls `::foo`. + --> mutual_recursion_trait.rs:19:5 + | +19 | ::foo(); + | ^^^^^^^^^^^^^^^^^^^ error: aborting due to 1 previous error diff --git a/creusot/tests/should_fail/terminates/recursion_through_contract.stderr b/creusot/tests/should_fail/terminates/recursion_through_contract.stderr index 7e5a38ec8c..3703aa321e 100644 --- a/creusot/tests/should_fail/terminates/recursion_through_contract.stderr +++ b/creusot/tests/should_fail/terminates/recursion_through_contract.stderr @@ -1,36 +1,36 @@ -error: Mutually recursive functions: when calling `f2`... - --> recursion_through_contract.rs:23:1 +error: Mutually recursive functions: when calling `with_requires`... + --> recursion_through_contract.rs:20:1 | -23 | fn f2() -> Int { - | ^^^^^^^^^^^^^^ +20 | fn with_requires(x: Int) {} + | ^^^^^^^^^^^^^^^^^^^^^^^^ | -note: then `f2` calls `with_requires`... - --> recursion_through_contract.rs:24:5 - | -24 | with_requires(5); - | ^^^^^^^^^^^^^^^^ -note: finally `with_requires` calls `f2`. +note: then `with_requires` calls `f2`... --> recursion_through_contract.rs:19:17 | 19 | #[requires(x == f2())] | ^^^^ - -error: Mutually recursive functions: when calling `f1`... - --> recursion_through_contract.rs:13:1 +note: finally `f2` calls `with_requires`. + --> recursion_through_contract.rs:24:5 | -13 | fn f1() -> Int { - | ^^^^^^^^^^^^^^ +24 | with_requires(5); + | ^^^^^^^^^^^^^^^^ + +error: Mutually recursive functions: when calling `with_proof_assert`... + --> recursion_through_contract.rs:6:1 | -note: then `f1` calls `with_proof_assert`... - --> recursion_through_contract.rs:14:5 +6 | fn with_proof_assert(x: Int) { + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | -14 | with_proof_assert(5); - | ^^^^^^^^^^^^^^^^^^^^ -note: finally `with_proof_assert` calls `f1`. +note: then `with_proof_assert` calls `f1`... --> recursion_through_contract.rs:8:14 | 8 | x == f1() | ^^^^ +note: finally `f1` calls `with_proof_assert`. + --> recursion_through_contract.rs:14:5 + | +14 | with_proof_assert(5); + | ^^^^^^^^^^^^^^^^^^^^ error: aborting due to 2 previous errors diff --git a/creusot/tests/should_succeed/termination/call_in_contract/why3session.xml b/creusot/tests/should_succeed/termination/call_in_contract/why3session.xml new file mode 100644 index 0000000000..848fefd858 --- /dev/null +++ b/creusot/tests/should_succeed/termination/call_in_contract/why3session.xml @@ -0,0 +1,14 @@ + + + + + + + + + + + + + diff --git a/creusot/tests/should_succeed/termination/call_in_contract/why3shapes.gz b/creusot/tests/should_succeed/termination/call_in_contract/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..6c062414134dec9aca0f933e6f0706a6768e0b72 GIT binary patch literal 105 zcmb2|=3oGW|CcWWX`J)W@z4#^@YdBjcjo-&AcNowm!5cS@%0Hd_u$dgJ>l6J7_)LG ztLoH`314Gko~cb+sX6VLm>L^fXWKKilVY80Zkp4kO*?t) + + + + + + diff --git a/creusot/tests/should_succeed/termination/default_impl/why3shapes.gz b/creusot/tests/should_succeed/termination/default_impl/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..8039d107e60d7999ed0f63df0240e8d413a7ba34 GIT binary patch literal 45 xcmb2|=3oGW|CcWWX`J)W@z4#^@YdBjcjo-&AcNowm!3RgVo;m=MqCo83IJJ{58wa* literal 0 HcmV?d00001 diff --git a/creusot/tests/should_succeed/termination/default_impl_in_trait/why3session.xml b/creusot/tests/should_succeed/termination/default_impl_in_trait/why3session.xml new file mode 100644 index 0000000000..420c651bbd --- /dev/null +++ b/creusot/tests/should_succeed/termination/default_impl_in_trait/why3session.xml @@ -0,0 +1,8 @@ + + + + + + + diff --git a/creusot/tests/should_succeed/termination/default_impl_in_trait/why3shapes.gz b/creusot/tests/should_succeed/termination/default_impl_in_trait/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..8039d107e60d7999ed0f63df0240e8d413a7ba34 GIT binary patch literal 45 xcmb2|=3oGW|CcWWX`J)W@z4#^@YdBjcjo-&AcNowm!3RgVo;m=MqCo83IJJ{58wa* literal 0 HcmV?d00001 From 1af5b74fc03d13eb82cf77d0be4b3c51efce582c Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Tue, 12 Nov 2024 19:27:17 +0100 Subject: [PATCH 6/6] Fix a crash in creusot-contracts --- creusot/src/validate_terminates.rs | 153 ++++++++++++++++------------- 1 file changed, 84 insertions(+), 69 deletions(-) diff --git a/creusot/src/validate_terminates.rs b/creusot/src/validate_terminates.rs index 164fcc0573..6350077140 100644 --- a/creusot/src/validate_terminates.rs +++ b/creusot/src/validate_terminates.rs @@ -198,8 +198,11 @@ struct BuildFunctionsGraph<'tcx> { /// the impl block. /// /// This is used to retrieve all the bounds when calling this function. - default_functions_bounds: IndexMap>, + default_functions_bounds: IndexMap>, is_default_function: IndexSet, + visited_default_specialization: IndexSet, + specialization_nodes: + IndexMap, } /// This node is used in the following case: @@ -305,13 +308,14 @@ impl<'tcx> BuildFunctionsGraph<'tcx> { /// Process the call from `node` to `called_id`. fn function_call( &mut self, - tcx: TyCtxt<'tcx>, + ctx: &mut TranslationCtx<'tcx>, node: graph::NodeIndex, param_env: ParamEnv<'tcx>, called_id: DefId, generic_args: GenericArgsRef<'tcx>, call_span: Span, ) { + let tcx = ctx.tcx; let (called_id, generic_args) = if TraitResolved::is_trait_item(tcx, called_id) { match TraitResolved::resolve_item(tcx, param_env, called_id, generic_args) { TraitResolved::Instance(def_id, subst) => (def_id, subst), @@ -333,6 +337,7 @@ impl<'tcx> BuildFunctionsGraph<'tcx> { return; } + // TODO: this code is kind of a soup, rework or refactor into a function let (called_node, bounds, impl_self_bound) = 'bl: { // this checks if we are calling a function with a default implementation, // as processed at the beginning of `CallGraph::build`. @@ -366,14 +371,12 @@ impl<'tcx> BuildFunctionsGraph<'tcx> { default_function: called_id, impl_block: spec_impl_id, }; - let Some(node) = - self.graph_node_to_index.get(&GraphNode::ImplDefaultTransparent(default_node)) - else { + let Some(node) = self.visit_specialized_default_function(ctx, default_node) else { break 'not_default; }; - let bounds = self.default_functions_bounds[&default_node]; + let bounds = self.default_functions_bounds[&node]; let self_bound = tcx.impl_trait_header(spec_impl_id); - break 'bl (*node, bounds, self_bound); + break 'bl (node, bounds, self_bound); } ( self.insert_function(tcx, GraphNode::Function(called_id)), @@ -410,6 +413,75 @@ impl<'tcx> BuildFunctionsGraph<'tcx> { } } } + + /// This visit the special function that is called when calling: + /// - a default function in a trait (or in a default impl) + /// - that is logical + /// - and visible at the point of implementation, that is + /// ``` + /// # use creusot_contracts::*; + /// trait Tr { + /// #[logic] #[open(self)] fn f() {} + /// } + /// impl Tr for i32 { } + /// #[logic] #[open(self)] fn g() { ::f(); } + /// ``` + /// Here the implementation `` generates an additional node in the + /// termination graph, which is "`f` but specialized in `impl Tr for i32`". + /// + /// We use this function, so that only those specialization that are actually called are visited. + fn visit_specialized_default_function( + &mut self, + ctx: &mut TranslationCtx<'tcx>, + graph_node: ImplDefaultTransparent, + ) -> Option { + let node = *self.graph_node_to_index.get(&GraphNode::ImplDefaultTransparent(graph_node))?; + if !self.visited_default_specialization.insert(node) { + return Some(node); + } + let tcx = ctx.tcx; + let ImplDefaultTransparent { default_function: item_id, impl_block: impl_id } = graph_node; + let specialization_node = &self.specialization_nodes[&node]; + + let impl_id = impl_id.to_def_id(); + let param_env = tcx.param_env(impl_id); + let term = ctx.term(item_id).unwrap(); + let mut visitor = TermCalls { results: IndexSet::new() }; + visitor.visit_term(term); + + let trait_id = tcx.trait_id_of_impl(impl_id).unwrap(); + + // translate the args of the impl to match the trait. + let infcx = tcx.infer_ctxt().build(); + let impl_args = rustc_trait_selection::traits::translate_args( + &infcx, + param_env, + impl_id, + GenericArgs::identity_for_item(tcx, impl_id), + specialization_node.defining_node, + ); + + // Take the generic arguments of the default function, instantiated with + // the type parameters from the impl block. + let func_impl_args = + GenericArgs::identity_for_item(tcx, item_id).rebase_onto(tcx, trait_id, impl_args); + + // data for when we call this function + let item_param_env = tcx.param_env(item_id); + let item_param_env = EarlyBinder::bind(item_param_env).instantiate(tcx, func_impl_args); + let bounds = normalize_param_env_or_error(tcx, item_param_env, ObligationCause::dummy()) + .caller_bounds(); + self.default_functions_bounds.insert(node, bounds); + + for (called_id, generic_args, call_span) in visitor.results { + // Instantiate the args for the call with the context we just built up. + let actual_args = + EarlyBinder::bind(tcx.erase_regions(generic_args)).instantiate(tcx, func_impl_args); + + self.function_call(ctx, node, param_env, called_id, actual_args, call_span); + } + Some(node) + } } impl CallGraph { @@ -421,7 +493,6 @@ impl CallGraph { let tcx = ctx.tcx; let mut build_call_graph = BuildFunctionsGraph::default(); - let mut specialization_nodes = IndexMap::new(); // Create the `GraphNode::ImplDefaultTransparent` nodes. for (trait_id, impls) in tcx.all_local_trait_impls(()) { for &impl_local_id in impls { @@ -459,76 +530,20 @@ impl CallGraph { // - logical items continue; } - specialization_nodes.insert((default_item_id, impl_local_id), default_item); - build_call_graph.insert_function( + + let node = build_call_graph.insert_function( tcx, GraphNode::ImplDefaultTransparent(ImplDefaultTransparent { default_function: default_item_id, impl_block: impl_local_id, }), ); + build_call_graph.specialization_nodes.insert(node, default_item); + build_call_graph.is_default_function.insert(default_item_id); } } } - for (graph_node, node) in build_call_graph.graph_node_to_index.clone() { - let GraphNode::ImplDefaultTransparent(graph_node) = graph_node else { - continue; - }; - let ImplDefaultTransparent { default_function: item_id, impl_block: impl_id } = - graph_node; - let specialization_node = &specialization_nodes[&(item_id, impl_id)]; - - let impl_id = impl_id.to_def_id(); - let param_env = tcx.param_env(impl_id); - let term = ctx.term(item_id).unwrap(); - let mut visitor = TermCalls { results: IndexSet::new() }; - visitor.visit_term(term); - - // Instantiate the generic args according to the specialization of the impl. - - let trait_id = tcx.trait_id_of_impl(impl_id).unwrap(); - - // Now, translate the args to match the trait. - let infcx = tcx.infer_ctxt().build(); - let impl_args = rustc_trait_selection::traits::translate_args( - &infcx, - param_env, - impl_id, - GenericArgs::identity_for_item(tcx, impl_id), - specialization_node.defining_node, - ); - - // Take the generic arguments of the default function, instantiated with - // the type parameters from the impl block. - let func_impl_args = - GenericArgs::identity_for_item(tcx, item_id).rebase_onto(tcx, trait_id, impl_args); - - // data for when we call this function - build_call_graph.is_default_function.insert(item_id); - let item_param_env = tcx.param_env(item_id); - let item_param_env = EarlyBinder::bind(item_param_env).instantiate(tcx, func_impl_args); - let bounds = - normalize_param_env_or_error(tcx, item_param_env, ObligationCause::dummy()) - .caller_bounds(); - build_call_graph.default_functions_bounds.insert(graph_node, bounds); - - for (called_id, generic_args, call_span) in visitor.results { - // Instantiate the args for the call with the context we just built up. - let actual_args = EarlyBinder::bind(tcx.erase_regions(generic_args)) - .instantiate(tcx, func_impl_args); - - build_call_graph.function_call( - tcx, - node, - param_env, - called_id, - actual_args, - call_span, - ); - } - } - for local_id in ctx.hir().body_owners() { if !(contracts_items::is_pearlite(ctx.tcx, local_id.to_def_id()) || contract_of(ctx, local_id.to_def_id()).terminates) @@ -558,7 +573,7 @@ impl CallGraph { for (called_id, generic_args, call_span) in visitor.calls { build_call_graph.function_call( - tcx, + ctx, node, param_env, called_id,