Improve further the errors for mixed declaration groups

src/interp/Interpreter.ml

@@ -11,7 +11,6 @@ open LlbcAst
 open Contexts
 open SynthesizeSymbolic
 open Errors
-open Meta
 module SA = SymbolicAst
 
 (** The local logger *)
@@ -36,66 +35,38 @@ let compute_contexts (m : crate) : decls_ctx =
       locals = [];
     }
   in
+  (* Split the declaration groups between the declaration kinds (types, functions, etc.) *)
   let type_decls_groups =
     match split_declarations_to_group_maps m.declarations with
     | Ok (type_decls_groups, _, _, _, _) -> type_decls_groups
     | Error mixed_groups ->
+        (* We detected mixed groups: print a nice error message *)
         let any_decl_id_to_string (id : any_decl_id) : string =
-          let get_meta :
-                'a. ('a -> item_meta) -> 'a option -> (span * name) option =
-           fun get x ->
-            match x with
-            | None -> None
-            | Some d ->
-                let meta = get d in
-                Some (meta.span, meta.name)
-          in
-          let kind, info =
-            match id with
-            | IdType id ->
-                ( "type decl",
-                  get_meta
-                    (fun (d : type_decl) -> d.item_meta)
-                    (TypeDeclId.Map.find_opt id type_decls) )
-            | IdFun id ->
-                ( "fun decl",
-                  get_meta
-                    (fun (d : fun_decl) -> d.item_meta)
-                    (FunDeclId.Map.find_opt id fun_decls) )
-            | IdGlobal id ->
-                ( "global decl",
-                  get_meta
-                    (fun (d : global_decl) -> d.item_meta)
-                    (GlobalDeclId.Map.find_opt id global_decls) )
-            | IdTraitDecl id ->
-                ( "trait decl",
-                  get_meta
-                    (fun (d : trait_decl) -> d.item_meta)
-                    (TraitDeclId.Map.find_opt id trait_decls) )
-            | IdTraitImpl id ->
-                ( "trait impl",
-                  get_meta
-                    (fun (d : trait_impl) -> d.item_meta)
-                    (TraitImplId.Map.find_opt id trait_impls) )
-          in
+          let kind = any_decl_id_to_kind_name id in
+          let meta = LlbcAstUtils.crate_get_item_meta m id in
           let s =
-            match info with
+            match meta with
             | None -> show_any_decl_id id
-            | Some (span, name) ->
-                kind ^ "(" ^ span_to_string span ^ "): "
-                ^ Print.name_to_string fmt_env name
+            | Some meta ->
+                kind ^ "(" ^ span_to_string meta.span ^ "): "
+                ^ Print.name_to_string fmt_env meta.name
           in
           "- " ^ s
         in
-        let msgs =
-          List.map
-            (fun (g : mixed_declaration_group) ->
-              let decls =
-                List.map any_decl_id_to_string (g_declaration_group_to_list g)
-              in
-              String.concat "\n" decls)
-            mixed_groups
+        let group_to_msg (g : mixed_declaration_group) : string =
+          let ids = g_declaration_group_to_list g in
+          let decls = List.map any_decl_id_to_string ids in
+          let local_requires =
+            LlbcAstUtils.find_local_transitive_dep m (AnyDeclIdSet.of_list ids)
+          in
+          let local_requires = List.map span_to_string local_requires in
+          "# Group:\n" ^ String.concat "\n" decls
+          ^ "\n\n\
+             The declarations in this group are (transitively) used at the \
+             following location(s):\n"
+          ^ String.concat "\n" local_requires
         in
+        let msgs = List.map group_to_msg mixed_groups in
         let msgs =
           String.concat "\n\n" (List.map (fun s -> "Group:\n" ^ s) msgs)
         in

src/interp/InterpreterExpansion.ml

@@ -649,7 +649,7 @@ let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) :
                       > 1 variants (option \
                       [greedy_expand_symbolics_with_borrows] of [config]): "
                     ^ name_to_string ctx def.item_meta.name)
-              | Alias _ | Opaque | Error _ ->
+              | Alias _ | Opaque | TError _ ->
                   craise __FILE__ __LINE__ span
                     "Attempted to greedily expand an alias or opaque type"
               | Union _ ->

src/interp/InterpreterLoopsCore.ml

@@ -23,9 +23,6 @@ exception Distinct of string
 
 type ctx_or_update = (eval_ctx, updt_env_kind) result
 
-(** Union Find *)
-module UF = UnionFind.Make (UnionFind.StoreMap)
-
 (** A small utility.
 
     Remark: we use projection markers, meaning we compute maps from/to

src/llbc/LlbcAstUtils.ml

@@ -2,6 +2,8 @@ open Types
 open LlbcAst
 include Charon.LlbcAstUtils
 open Collections
+open Utils
+open Meta
 
 module FunIdOrderedType : OrderedType with type t = fun_id = struct
   type t = fun_id
@@ -66,3 +68,155 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_builtin : bool) :
 let crate_has_opaque_non_builtin_decls (k : crate) (filter_builtin : bool) :
     bool =
   crate_get_opaque_non_builtin_decls k filter_builtin <> ([], [])
+
+(** For error reporting: compute which local definitions (transitively) depend
+    on a set of external definitions. This allows us to pinpoint to the user
+    which parts of the code are responsible for an error stemming from a
+    dependency. *)
+let find_local_transitive_dep (m : crate) (marked_externals : AnyDeclIdSet.t) :
+    span list =
+  (* Compute the edges from: (decl_id, span) to (decl_id) *)
+  let edges = ref [] in
+  let visitor =
+    object
+      inherit [_] iter_statement as super
+
+      method! visit_statement decl_span_info st =
+        let decl_span_info =
+          Option.map (fun (decl_id, _) -> (decl_id, st.span)) decl_span_info
+        in
+        super#visit_statement decl_span_info st
+
+      method! visit_type_decl_id decl_span_info id =
+        Option.iter
+          (fun info -> edges := (info, IdType id) :: !edges)
+          decl_span_info
+
+      method! visit_fun_decl_id decl_span_info id =
+        Option.iter
+          (fun info -> edges := (info, IdFun id) :: !edges)
+          decl_span_info
+
+      method! visit_global_decl_id decl_span_info id =
+        Option.iter
+          (fun info -> edges := (info, IdGlobal id) :: !edges)
+          decl_span_info
+
+      method! visit_trait_decl_id decl_span_info id =
+        Option.iter
+          (fun info -> edges := (info, IdTraitDecl id) :: !edges)
+          decl_span_info
+
+      method! visit_trait_impl_id decl_span_info id =
+        Option.iter
+          (fun info -> edges := (info, IdTraitImpl id) :: !edges)
+          decl_span_info
+    end
+  in
+  (* Visit each kind of definition *)
+  TypeDeclId.Map.iter
+    (fun _ (d : type_decl) ->
+      let decl_span_info = Some (IdType d.def_id, d.item_meta.span) in
+      visitor#visit_type_decl decl_span_info d)
+    m.type_decls;
+  FunDeclId.Map.iter
+    (fun _ (d : fun_decl) ->
+      let decl_span_info = Some (IdFun d.def_id, d.item_meta.span) in
+      visitor#visit_fun_sig decl_span_info d.signature;
+      Option.iter
+        (fun (body : expr_body) ->
+          visitor#visit_statement decl_span_info body.body)
+        d.body)
+    m.fun_decls;
+  (* We don't need to visit the globals (it is redundant with visiting the functions) *)
+  TraitDeclId.Map.iter
+    (fun _ (d : trait_decl) ->
+      let decl_span_info = Some (IdTraitDecl d.def_id, d.item_meta.span) in
+      visitor#visit_trait_decl decl_span_info d)
+    m.trait_decls;
+  TraitImplId.Map.iter
+    (fun _ (d : trait_impl) ->
+      let decl_span_info = Some (IdTraitImpl d.def_id, d.item_meta.span) in
+      visitor#visit_trait_impl decl_span_info d)
+    m.trait_impls;
+  (* We're using a union-find data-structure.
+
+     All external dependencies which are in the set [external] or which
+     transitively depend on declarations in this set are put in the same
+     equivalence class.
+  *)
+  let ids =
+    List.map (fun id -> IdType id) (TypeDeclId.Map.keys m.type_decls)
+    @ List.map (fun id -> IdFun id) (FunDeclId.Map.keys m.fun_decls)
+    @ List.map (fun id -> IdGlobal id) (GlobalDeclId.Map.keys m.global_decls)
+    @ List.map (fun id -> IdTraitDecl id) (TraitDeclId.Map.keys m.trait_decls)
+    @ List.map (fun id -> IdTraitImpl id) (TraitImplId.Map.keys m.trait_impls)
+  in
+  let uf_store = UF.new_store () in
+  let external_ids =
+    AnyDeclIdMap.of_list
+      (List.filter_map
+         (fun id ->
+           let meta = crate_get_item_meta m id in
+           match meta with
+           | None -> None
+           | Some meta ->
+               if meta.is_local then None else Some (id, UF.make uf_store id))
+         ids)
+  in
+  (* Merge the classes of the marked externals *)
+  let marked_class =
+    match AnyDeclIdSet.elements marked_externals with
+    | id0 :: ids ->
+        let c0 = AnyDeclIdMap.find id0 external_ids in
+        List.iter
+          (fun id ->
+            let c = AnyDeclIdMap.find id external_ids in
+            let _ = UF.union uf_store c0 c in
+            ())
+          ids;
+        c0
+    | _ -> raise (Failure "Unreachable")
+  in
+  (* Merge the classes by using the edges *)
+  List.iter
+    (fun ((id0, _), id1) ->
+      match (crate_get_item_meta m id0, crate_get_item_meta m id1) with
+      | Some meta0, Some meta1 ->
+          if (not meta0.is_local) && not meta1.is_local then
+            let c0 = AnyDeclIdMap.find id0 external_ids in
+            let c1 = AnyDeclIdMap.find id1 external_ids in
+            let _ = UF.union uf_store c0 c1 in
+            ()
+          else ()
+      | _ -> ())
+    !edges;
+  (* We now compute a map from external id in the set to set of local
+     declarations (and spans) which depend on this external id *)
+  List.iter
+    (fun ((id0, _), id1) ->
+      match (crate_get_item_meta m id0, crate_get_item_meta m id1) with
+      | Some meta0, Some meta1 ->
+          if (not meta0.is_local) && not meta1.is_local then
+            let c0 = AnyDeclIdMap.find id0 external_ids in
+            let c1 = AnyDeclIdMap.find id1 external_ids in
+            let _ = UF.union uf_store c0 c1 in
+            ()
+          else ()
+      | _ -> ())
+    !edges;
+  (* The spans at which we transitively refer to a marked external definition *)
+  let spans = ref Charon.MetaUtils.SpanSet.empty in
+  List.iter
+    (fun ((id0, span), id1) ->
+      match (crate_get_item_meta m id0, crate_get_item_meta m id1) with
+      | Some meta0, Some meta1 ->
+          if meta0.is_local && not meta1.is_local then
+            let c1 = AnyDeclIdMap.find id1 external_ids in
+            if UF.eq uf_store marked_class c1 then
+              spans := Charon.MetaUtils.SpanSet.add span !spans
+            else ()
+      | _ -> ())
+    !edges;
+  (* Return the spans *)
+  Charon.MetaUtils.SpanSet.elements !spans

src/llbc/TypesAnalysis.ml

@@ -385,7 +385,7 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos)
             "type aliases should have been removed earlier"
       | Union _ ->
           craise __FILE__ __LINE__ def.item_meta.span "unions are not supported"
-      | Opaque | Error _ ->
+      | Opaque | TError _ ->
           craise __FILE__ __LINE__ def.item_meta.span "unreachable"
     in
     (* Substitute the regions in the fields *)

src/pure/PureMicroPasses.ml

@@ -1385,7 +1385,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                 in
                 let fields =
                   match adt_decl.kind with
-                  | Enum _ | Alias _ | Opaque | Error _ ->
+                  | Enum _ | Alias _ | Opaque | TError _ ->
                       craise __FILE__ __LINE__ def.item_meta.span "Unreachable"
                   | Union _ ->
                       craise __FILE__ __LINE__ def.item_meta.span

src/symbolic/SymbolicToPure.ml

@@ -595,7 +595,7 @@ let translate_type_decl_kind (span : Meta.span) (kind : T.type_decl_kind) :
   | Alias _ ->
       craise __FILE__ __LINE__ span
         "type aliases should have been removed earlier"
-  | T.Union _ | T.Opaque | T.Error _ -> Opaque
+  | T.Union _ | T.Opaque | T.TError _ -> Opaque
 
 (** Compute which input parameters should be implicit or explicit.
 

src/utils/Utils.ml

@@ -1 +1,4 @@
 include Charon.Utils
+
+(** Union Find *)
+module UF = UnionFind.Make (UnionFind.StoreMap)