Move some definitions and helpers to Charon-ML

README.md

@@ -45,7 +45,7 @@ You can then install the dependencies with the following command:
 
 ```
 opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc \
-  unionFind ocamlgraph menhir ocamlformat
+  ocamlgraph menhir ocamlformat
 ```
 
 Moreover, Aeneas uses the [Charon](https://github.com/AeneasVerif/charon) project and library.

src/dune

@@ -14,7 +14,7 @@
  (public_name aeneas) ;; The name as revealed to the projects importing this library
  (preprocess
   (pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
- (libraries charon core_unix unionFind ocamlgraph str)
+ (libraries charon core_unix ocamlgraph str)
  (modules
   AssociatedTypes
   BorrowCheck

src/interp/Interpreter.ml

@@ -53,7 +53,7 @@ let compute_contexts (m : crate) : decls_ctx =
           in
           "- " ^ s
         in
-        let group_to_msg (g : mixed_declaration_group) : string =
+        let group_to_msg (i : int) (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 =
@@ -68,12 +68,12 @@ let compute_contexts (m : crate) : decls_ctx =
               ^ String.concat "\n" local_requires
             else ""
           in
-          "# Group:\n" ^ String.concat "\n" decls ^ 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)
+          "# Group "
+          ^ string_of_int (i + 1)
+          ^ ":\n" ^ String.concat "\n" decls ^ local_requires
         in
+        let msgs = List.mapi group_to_msg mixed_groups in
+        let msgs = String.concat "\n\n" msgs in
         craise_opt_span __FILE__ __LINE__ None
           ("Detected groups of mixed mutually recursive definitions (such as a \
             type mutually recursive with a function, or a function mutually \

src/llbc/LlbcAstUtils.ml

@@ -2,8 +2,6 @@ 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
@@ -68,177 +66,3 @@ 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_variant decl_span_info (variant : variant) =
-        let decl_span_info =
-          Option.map
-            (fun (decl_id, _) -> (decl_id, variant.span))
-            decl_span_info
-        in
-        super#visit_variant decl_span_info variant
-
-      method! visit_trait_clause decl_span_info (clause : trait_clause) =
-        let decl_span_info =
-          match (decl_span_info, clause.span) with
-          | Some (decl_id, _), Some span -> Some (decl_id, span)
-          | _ -> decl_span_info
-        in
-        super#visit_trait_clause decl_span_info clause
-
-      method! visit_field decl_span_info (field : field) =
-        let decl_span_info =
-          Option.map (fun (decl_id, _) -> (decl_id, field.span)) decl_span_info
-        in
-        super#visit_field decl_span_info field
-
-      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/utils/Utils.ml

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