Add more information to cycle detection error messages

Chris-Hawblitzel · Chris-Hawblitzel · commit 9e351c871e99 · 2024-01-23T12:48:13.000-08:00
diff --git a/source/rust_verify/src/rust_to_vir.rs b/source/rust_verify/src/rust_to_vir.rs
@@ -344,6 +344,7 @@ fn check_item<'tcx>(
                     )?);
                 }
                 let types = Arc::new(types);
+                let path_span = path.span.to(impll.self_ty.span);
                 let path = def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, path.res.def_id());
                 let (typ_params, typ_bounds) = crate::rust_to_vir_base::check_generics_bounds_fun(
                     ctxt.tcx,
@@ -358,7 +359,7 @@ fn check_item<'tcx>(
                     typ_bounds,
                     trait_path: path.clone(),
                     trait_typ_args: types.clone(),
-                    trait_typ_arg_impls: impl_paths,
+                    trait_typ_arg_impls: ctxt.spanned_new(path_span, impl_paths),
                 };
                 vir.trait_impls.push(ctxt.spanned_new(item.span, trait_impl));
                 Some((trait_ref, path, types))
@@ -498,7 +499,7 @@ fn check_item<'tcx>(
                                     typ,
                                     impl_paths: Arc::new(impl_paths),
                                 };
-                                vir.assoc_type_impls.push(ctxt.spanned_new(item.span, assocx));
+                                vir.assoc_type_impls.push(ctxt.spanned_new(impl_item.span, assocx));
                             } else {
                                 unsupported_err!(
                                     item.span,
diff --git a/source/vir/src/ast.rs b/source/vir/src/ast.rs
@@ -988,7 +988,7 @@ pub struct TraitImplX {
     pub typ_bounds: GenericBounds,
     pub trait_path: Path,
     pub trait_typ_args: Typs,
-    pub trait_typ_arg_impls: ImplPaths,
+    pub trait_typ_arg_impls: Arc<Spanned<ImplPaths>>,
 }
 
 #[derive(Clone, Debug, Hash, Serialize, Deserialize, ToDebugSNode, PartialEq, Eq)]
diff --git a/source/vir/src/context.rs b/source/vir/src/context.rs
@@ -41,6 +41,7 @@ pub struct GlobalCtx {
     pub func_call_graph: Arc<Graph<Node>>,
     pub func_call_sccs: Arc<Vec<Node>>,
     pub(crate) datatype_graph: Arc<Graph<crate::recursive_types::TypNode>>,
+    pub(crate) datatype_graph_span_infos: Vec<Span>,
     /// Connects quantifier identifiers to the original expression
     pub qid_map: RefCell<HashMap<String, BndInfo>>,
     pub(crate) rlimit: f32,
@@ -256,14 +257,24 @@ impl GlobalCtx {
             func_call_graph.add_node(Node::TraitImpl(t.x.impl_path.clone()));
         }
 
+        let mut span_infos: Vec<Span> = Vec::new();
         for t in &krate.trait_impls {
-            crate::recursive_types::add_trait_impl_to_graph(&mut func_call_graph, t);
+            crate::recursive_types::add_trait_impl_to_graph(
+                &mut span_infos,
+                &mut func_call_graph,
+                t,
+            );
         }
 
         for f in &krate.functions {
             fun_bounds.insert(f.x.name.clone(), f.x.typ_bounds.clone());
             func_call_graph.add_node(Node::Fun(f.x.name.clone()));
-            crate::recursion::expand_call_graph(&func_map, &mut func_call_graph, f)?;
+            crate::recursion::expand_call_graph(
+                &func_map,
+                &mut func_call_graph,
+                &mut span_infos,
+                f,
+            )?;
         }
 
         func_call_graph.compute_sccs();
@@ -292,7 +303,7 @@ impl GlobalCtx {
         }
         let qid_map = RefCell::new(HashMap::new());
 
-        let datatype_graph = crate::recursive_types::build_datatype_graph(krate);
+        let datatype_graph = crate::recursive_types::build_datatype_graph(krate, &mut span_infos);
 
         Ok(GlobalCtx {
             chosen_triggers,
@@ -302,6 +313,7 @@ impl GlobalCtx {
             func_call_graph: Arc::new(func_call_graph),
             func_call_sccs: Arc::new(func_call_sccs),
             datatype_graph: Arc::new(datatype_graph),
+            datatype_graph_span_infos: span_infos,
             qid_map,
             rlimit,
             interpreter_log,
@@ -322,6 +334,7 @@ impl GlobalCtx {
             no_span: self.no_span.clone(),
             func_call_graph: self.func_call_graph.clone(),
             datatype_graph: self.datatype_graph.clone(),
+            datatype_graph_span_infos: self.datatype_graph_span_infos.clone(),
             func_call_sccs: self.func_call_sccs.clone(),
             qid_map,
             rlimit: self.rlimit,
diff --git a/source/vir/src/recursion.rs b/source/vir/src/recursion.rs
@@ -33,6 +33,9 @@ pub enum Node {
     Datatype(Path),
     Trait(Path),
     TraitImpl(Path),
+    // This is used to replace an X --> Y edge with X --> SpanInfo --> Y edges
+    // to give more precise span information than X or Y alone provide
+    SpanInfo { span_infos_index: usize, text: String },
 }
 
 #[derive(Clone)]
@@ -420,6 +423,7 @@ pub(crate) fn check_termination_stm(
 pub(crate) fn expand_call_graph(
     func_map: &HashMap<Fun, Function>,
     call_graph: &mut Graph<Node>,
+    span_infos: &mut Vec<Span>,
     function: &Function,
 ) -> Result<(), VirErr> {
     // See recursive_types::check_traits for more documentation
@@ -488,7 +492,15 @@ pub(crate) fn expand_call_graph(
                             continue;
                         }
                     }
-                    call_graph.add_edge(f_node.clone(), Node::TraitImpl(impl_path.clone()));
+                    let expr_node = crate::recursive_types::new_span_info_node(
+                        span_infos,
+                        expr.span.clone(),
+                        ": application of a function to some type arguments, which may depend on \
+                            other trait implementations to satisfy trait bounds"
+                            .to_string(),
+                    );
+                    call_graph.add_edge(f_node.clone(), expr_node.clone());
+                    call_graph.add_edge(expr_node.clone(), Node::TraitImpl(impl_path.clone()));
                 }
 
                 // f --> f2
diff --git a/source/vir/src/recursive_types.rs b/source/vir/src/recursive_types.rs
@@ -126,12 +126,16 @@ fn check_well_founded_typ(
 pub(crate) enum TypNode {
     Datatype(Path),
     TraitImpl(Path),
+    // This is used to replace an X --> Y edge with X --> SpanInfo --> Y edges
+    // to give more precise span information than X or Y alone provide
+    SpanInfo { span_infos_index: usize, text: String },
 }
 
 struct CheckPositiveGlobal {
     krate: Krate,
     datatypes: HashMap<Path, Datatype>,
     type_graph: Graph<TypNode>,
+    span_infos: Vec<Span>,
 }
 
 struct CheckPositiveLocal {
@@ -140,6 +144,18 @@ struct CheckPositiveLocal {
     tparams: HashMap<Ident, AcceptRecursiveType>,
 }
 
+pub(crate) fn new_span_info_node(span_infos: &mut Vec<Span>, span: Span, text: String) -> Node {
+    let node = Node::SpanInfo { span_infos_index: span_infos.len(), text };
+    span_infos.push(span);
+    node
+}
+
+fn new_span_info_typ_node(span_infos: &mut Vec<Span>, span: Span, text: String) -> TypNode {
+    let node = TypNode::SpanInfo { span_infos_index: span_infos.len(), text };
+    span_infos.push(span);
+    node
+}
+
 // polarity = Some(true) for positive, Some(false) for negative, None for neither
 fn check_positive_uses(
     global: &CheckPositiveGlobal,
@@ -208,7 +224,12 @@ fn check_positive_uses(
                 if global.type_graph.in_same_scc(&impl_node, &my_node) {
                     let scc_rep = global.type_graph.get_scc_rep(&my_node);
                     let scc_nodes = global.type_graph.shortest_cycle_back_to_self(&scc_rep);
-                    return Err(type_scc_error(&global.krate, &my_node, &scc_nodes));
+                    return Err(type_scc_error(
+                        &global.krate,
+                        &global.span_infos,
+                        &my_node,
+                        &scc_nodes,
+                    ));
                 }
             }
             Ok(())
@@ -256,7 +277,7 @@ fn add_one_type_to_graph(type_graph: &mut Graph<TypNode>, src: &TypNode, typ: &T
     }
 }
 
-pub(crate) fn build_datatype_graph(krate: &Krate) -> Graph<TypNode> {
+pub(crate) fn build_datatype_graph(krate: &Krate, span_infos: &mut Vec<Span>) -> Graph<TypNode> {
     let mut type_graph: Graph<TypNode> = Graph::new();
 
     // If datatype D1 has a field whose type mentions datatype D2, create a graph edge D1 --> D2
@@ -270,7 +291,15 @@ pub(crate) fn build_datatype_graph(krate: &Krate) -> Graph<TypNode> {
     }
 
     for a in &krate.assoc_type_impls {
-        let src = TypNode::TraitImpl(a.x.impl_path.clone());
+        let trait_impl_src = TypNode::TraitImpl(a.x.impl_path.clone());
+        let src = new_span_info_typ_node(
+            span_infos,
+            a.span.clone(),
+            ": associated type definition, which may depend on other trait implementations \
+                to satisfy type bounds"
+                .to_string(),
+        );
+        type_graph.add_edge(trait_impl_src, src.clone());
         for impl_path in a.x.impl_paths.iter() {
             let dst = TypNode::TraitImpl(impl_path.clone());
             type_graph.add_edge(src.clone(), dst);
@@ -284,19 +313,21 @@ pub(crate) fn build_datatype_graph(krate: &Krate) -> Graph<TypNode> {
     }
 
     type_graph.compute_sccs();
-    return type_graph;
+
+    type_graph
 }
 
 pub(crate) fn check_recursive_types(krate: &Krate) -> Result<(), VirErr> {
-    let type_graph = build_datatype_graph(krate);
+    let mut span_infos: Vec<Span> = Vec::new();
+    let type_graph = build_datatype_graph(krate, &mut span_infos);
     let mut datatypes: HashMap<Path, Datatype> = HashMap::new();
     let mut datatypes_well_founded: HashSet<Path> = HashSet::new();
 
     for datatype in &krate.datatypes {
         datatypes.insert(datatype.x.path.clone(), datatype.clone());
     }
 
-    let global = CheckPositiveGlobal { krate: krate.clone(), datatypes, type_graph };
+    let global = CheckPositiveGlobal { krate: krate.clone(), datatypes, type_graph, span_infos };
 
     for function in &krate.functions {
         if let FunctionKind::TraitMethodDecl { .. } = function.x.kind {
@@ -343,6 +374,7 @@ pub(crate) fn check_recursive_types(krate: &Krate) -> Result<(), VirErr> {
                 TypNode::TraitImpl(_) if global.type_graph.node_is_in_cycle(node) => {
                     return Err(type_scc_error(
                         krate,
+                        &global.span_infos,
                         node,
                         &global.type_graph.shortest_cycle_back_to_self(scc),
                     ));
@@ -377,75 +409,96 @@ pub(crate) fn check_recursive_types(krate: &Krate) -> Result<(), VirErr> {
     Ok(())
 }
 
-fn type_scc_error(krate: &Krate, head: &TypNode, nodes: &Vec<TypNode>) -> VirErr {
+fn type_scc_error(
+    krate: &Krate,
+    span_infos: &Vec<Span>,
+    head: &TypNode,
+    nodes: &Vec<TypNode>,
+) -> VirErr {
     let msg =
         "found a cyclic self-reference in a trait definition, which may result in nontermination"
             .to_string();
     let mut err = crate::messages::error_bare(msg);
     for (i, node) in nodes.iter().enumerate() {
-        let mut push = |node: &TypNode, span: Span| {
+        let mut push = |node: &TypNode, span: Span, text: &str| {
             if node == head {
                 err = err.primary_span(&span);
             }
-            let msg = format!("may be part of cycle (node {} of {} in cycle)", i + 1, nodes.len());
+            let msg = format!(
+                "may be part of cycle (node {} of {} in cycle){}",
+                i + 1,
+                nodes.len(),
+                text
+            );
             err = err.secondary_label(&span, msg);
         };
         match node {
             TypNode::Datatype(path) => {
                 if let Some(d) = krate.datatypes.iter().find(|t| t.x.path == *path) {
                     let span = d.span.clone();
-                    push(node, span);
+                    push(node, span, ": type definition");
                 }
             }
             TypNode::TraitImpl(impl_path) => {
                 if let Some(t) = krate.trait_impls.iter().find(|t| t.x.impl_path == *impl_path) {
                     let span = t.span.clone();
-                    push(node, span);
+                    push(node, span, ": implementation of trait for a type");
                 }
             }
+            TypNode::SpanInfo { span_infos_index, text } => {
+                push(node, span_infos[*span_infos_index].clone(), text);
+            }
         }
     }
     err
 }
 
-fn scc_error(krate: &Krate, head: &Node, nodes: &Vec<Node>) -> VirErr {
+fn scc_error(krate: &Krate, span_infos: &Vec<Span>, head: &Node, nodes: &Vec<Node>) -> VirErr {
     let msg =
         "found a cyclic self-reference in a trait definition, which may result in nontermination"
             .to_string();
     let mut err = crate::messages::error_bare(msg);
     for (i, node) in nodes.iter().enumerate() {
-        let mut push = |node: &Node, span: Span| {
+        let mut push = |node: &Node, span: Span, text: &str| {
             if node == head {
                 err = err.primary_span(&span);
             }
-            let msg = format!("may be part of cycle (node {} of {} in cycle)", i + 1, nodes.len());
+            let msg = format!(
+                "may be part of cycle (node {} of {} in cycle){}",
+                i + 1,
+                nodes.len(),
+                text
+            );
             err = err.secondary_label(&span, msg);
         };
         match node {
             Node::Fun(fun) => {
                 if let Some(f) = krate.functions.iter().find(|f| f.x.name == *fun) {
                     let span = f.span.clone();
-                    push(node, span);
+                    push(node, span, ": function definition, whose body may have dependencies");
                 }
             }
             Node::Datatype(path) => {
                 if let Some(d) = krate.datatypes.iter().find(|t| t.x.path == *path) {
                     let span = d.span.clone();
-                    push(node, span);
+                    push(node, span, ": type definition");
                 }
             }
             Node::Trait(trait_path) => {
                 if let Some(t) = krate.traits.iter().find(|t| t.x.name == *trait_path) {
                     let span = t.span.clone();
-                    push(node, span);
+                    push(node, span, ": declaration of trait");
                 }
             }
             Node::TraitImpl(impl_path) => {
                 if let Some(t) = krate.trait_impls.iter().find(|t| t.x.impl_path == *impl_path) {
                     let span = t.span.clone();
-                    push(node, span);
+                    push(node, span, ": implementation of trait for a type");
                 }
             }
+            Node::SpanInfo { span_infos_index, text } => {
+                push(node, span_infos[*span_infos_index].clone(), text);
+            }
         }
     }
     err
@@ -495,14 +548,27 @@ pub(crate) fn add_trait_to_graph(call_graph: &mut Graph<Node>, trt: &Trait) {
     }
 }
 
-pub(crate) fn add_trait_impl_to_graph(call_graph: &mut Graph<Node>, t: &crate::ast::TraitImpl) {
+pub(crate) fn add_trait_impl_to_graph(
+    span_infos: &mut Vec<Span>,
+    call_graph: &mut Graph<Node>,
+    t: &crate::ast::TraitImpl,
+) {
     // For
     //   trait T<...> where ...: U1(...), ..., ...: Un(...)
     //   impl T<t1...tn> for ... { ... }
     // Add necessary impl_T_for_* --> impl_Ui_for_* edges
     // This corresponds to instantiating the a: Dictionary_U<A> field in the comments below
-    let src_node = Node::TraitImpl(t.x.impl_path.clone());
-    for imp in t.x.trait_typ_arg_impls.iter() {
+    let trait_impl_src_node = Node::TraitImpl(t.x.impl_path.clone());
+    let src_node = new_span_info_node(
+        span_infos,
+        t.x.trait_typ_arg_impls.span.clone(),
+        ": an implementation of a trait, applying the trait to some type arguments, \
+            for some `Self` type, where applying the trait to type arguments and declaring \
+            the `Self` type may depend on other trait implementations to satisfy type bounds"
+            .to_string(),
+    );
+    call_graph.add_edge(trait_impl_src_node, src_node.clone());
+    for imp in t.x.trait_typ_arg_impls.x.iter() {
         if &t.x.impl_path != imp {
             call_graph.add_edge(src_node.clone(), Node::TraitImpl(imp.clone()));
         }
@@ -648,6 +714,7 @@ pub fn check_traits(krate: &Krate, ctx: &GlobalCtx) -> Result<(), VirErr> {
                 _ if ctx.func_call_graph.node_is_in_cycle(node) => {
                     return Err(scc_error(
                         krate,
+                        &ctx.datatype_graph_span_infos,
                         node,
                         &ctx.func_call_graph.shortest_cycle_back_to_self(node),
                     ));

Original file line number	Diff line number	Diff line change
`@@ -988,7 +988,7 @@ pub struct TraitImplX {`
`988`	`988`	`pub typ_bounds: GenericBounds,`
`989`	`989`	`pub trait_path: Path,`
`990`	`990`	`pub trait_typ_args: Typs,`
`991`		`- pub trait_typ_arg_impls: ImplPaths,`
	`991`	`+ pub trait_typ_arg_impls: Arc<Spanned<ImplPaths>>,`
`992`	`992`	`}`
`993`	`993`
`994`	`994`	`#[derive(Clone, Debug, Hash, Serialize, Deserialize, ToDebugSNode, PartialEq, Eq)]`