diff --git a/creusot/src/translation/traits.rs b/creusot/src/translation/traits.rs index befc985f1a..513e942b1b 100644 --- a/creusot/src/translation/traits.rs +++ b/creusot/src/translation/traits.rs @@ -304,6 +304,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..193249611d 100644 --- a/creusot/src/validate_terminates.rs +++ b/creusot/src/validate_terminates.rs @@ -20,6 +20,10 @@ //! 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, @@ -27,7 +31,7 @@ use crate::{ }; use indexmap::{IndexMap, IndexSet}; use petgraph::{graph, visit::EdgeRef as _}; -use rustc_hir::def_id::{DefId, LocalDefId}; +use rustc_hir::def_id::DefId; use rustc_middle::{ thir, ty::{EarlyBinder, FnDef, GenericArgKind, GenericArgs, ParamEnv, TyCtxt, TyKind}, @@ -48,16 +52,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(); + 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()); + if function_data.is_pearlite { + // Allow simple recursion in logic functions call_graph.remove_edge(self_edge); continue; } + let span = match call { + CallKind::Direct(span) => span, + _ => 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 +74,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 +89,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(); + 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 +123,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(); let mut error = ctx.error( ctx.def_span(root_def_id), &format!( @@ -123,39 +131,36 @@ 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()); + let f2 = ctx.tcx.def_path_str(call_graph.node_weight(next_node).unwrap()); + + 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 +168,36 @@ 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>, -} - #[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)>, + def_id_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,38 +212,21 @@ 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_node(&mut self, tcx: TyCtxt, def_id: DefId) -> graph::NodeIndex { + match self.def_id_to_index.entry(def_id) { 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(def_id); 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 } @@ -236,159 +234,117 @@ impl<'tcx> BuildFunctionsGraph<'tcx> { } } -#[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, - } - } -} - -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 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) + 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) { + continue; // 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 }, - ); } - } + let def_id = local_id.to_def_id(); + let node = build_call_graph.insert_node(ctx.tcx, def_id); - 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) + if is_trusted_function(ctx.tcx, def_id) + || contracts_items::is_no_translate(ctx.tcx, def_id) { - // 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); + // Cut all arcs from this function. + continue; + } - for (function_def_id, span, subst) in visited_calls { - if !ctx.tcx.is_mir_available(function_def_id) { - continue; - } + let param_env = ctx.tcx.param_env(def_id); + let tcx = ctx.tcx; + 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, + param_env, + calls: IndexSet::new(), + has_loops: None, + }; + ::visit_expr(&mut visitor, &thir[expr]); - 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.additional_data[&node].has_loops = visitor.has_loops; - build_call_graph.graph.add_edge(caller_node, next_node, span); + for (called_id, generic_args, call_span) in visitor.calls { + if contracts_items::is_ghost_from_fn(ctx.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 = build_call_graph.insert_node(ctx.tcx, *ghost_def_id); + build_call_graph.graph.update_edge(node, ghost_node, CallKind::Ghost); + continue; + } + let called_node = build_call_graph.insert_node(tcx, called_id); + build_call_graph.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. + for bound in tcx.param_env(called_id).caller_bounds() { + let Some(clause) = bound.as_trait_clause() else { continue }; + let tcx = ctx.tcx; + let trait_ref = tcx.instantiate_bound_regions_with_erased(clause).trait_ref; + let subst = trait_ref.args; + let subst = EarlyBinder::bind(subst).instantiate(tcx, generic_args); + + let block_id = match TraitResolved::impl_id_of_trait( + tcx, + param_env, + trait_ref.def_id, + subst, + ) { + Some(impl_id) => impl_id, + None => trait_ref.def_id, + }; + + // Does the impl block contain `def_id`? + let mut from_impl_block = false; + // Does the impl block contain `called_id`? + let mut to_impl_block = false; + // if both are true, then do not automatically add an arc to the + // functions in `block_id`, we are calling a known monomorphized + // version anyways. + + for &item_id in tcx.associated_item_def_ids(trait_ref.def_id) { + if called_id == item_id { + to_impl_block = true; // This can happen when `called_id` is inside a closure. } - 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, - }, + + let mut items = Vec::new(); + for &item_id in tcx.associated_item_def_ids(block_id) { + if def_id == item_id { + from_impl_block = true; + } + if called_id == item_id { + to_impl_block = true; + } + if tcx.def_kind(item_id).is_fn_like() { + let item_node = build_call_graph.insert_node(tcx, item_id); + items.push(item_node); + } + } + if !(from_impl_block && to_impl_block) { + // Add edges to all the functions defined inside the `impl` block. + for item_node in items { + build_call_graph.graph.update_edge( + node, + item_node, + CallKind::GenericBound(called_id, call_span), ); - } 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 }; } } } @@ -402,15 +358,13 @@ 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 +376,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 +390,13 @@ 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), _ => {} 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..44d01a2913 100644 --- a/creusot/tests/should_fail/terminates/mutual_recursion_trait.stderr +++ b/creusot/tests/should_fail/terminates/mutual_recursion_trait.stderr @@ -4,7 +4,7 @@ error: Mutually recursive functions: when calling `bar`... 18 | fn bar() { | ^^^^^^^^ | -note: then `bar` calls `::foo`... +note: then `bar` might call `::foo` via the call to `Foo::foo`... --> mutual_recursion_trait.rs:19:5 | 19 | ::foo(); 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