Merge pull request #372 from AeneasVerif/son/features

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.

charon-pin

@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-04d97dd849d7a69239e28aa64859d3a4f86b4162
+1172606b471b5d9913f95cfbf944d3b943736667

flake.nix

@@ -64,7 +64,6 @@
             yojson
             zarith
             ocamlgraph
-            unionFind
           ]);
           afterBuild = ''
             echo charon.packages.${system}.tests

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

@@ -23,8 +23,61 @@ let compute_contexts (m : crate) : decls_ctx =
   let global_decls = m.global_decls in
   let trait_decls = m.trait_decls in
   let trait_impls = m.trait_impls in
-  let type_decls_groups, _, _, _, _ =
-    split_declarations_to_group_maps m.declarations
+  let fmt_env : Print.fmt_env =
+    {
+      type_decls;
+      fun_decls;
+      global_decls;
+      trait_decls;
+      trait_impls;
+      regions = [];
+      generics = empty_generic_params;
+      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 kind = any_decl_id_to_kind_name id in
+          let meta = LlbcAstUtils.crate_get_item_meta m id in
+          let s =
+            match meta with
+            | None -> show_any_decl_id id
+            | Some meta ->
+                kind ^ "(" ^ span_to_string meta.span ^ "): "
+                ^ Print.name_to_string fmt_env meta.name
+          in
+          "- " ^ s
+        in
+        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 =
+            LlbcAstUtils.find_local_transitive_dep m (AnyDeclIdSet.of_list ids)
+          in
+          let local_requires = List.map span_to_string local_requires in
+          let local_requires =
+            if local_requires <> [] then
+              "\n\n\
+               The declarations in this group are (transitively) used at the \
+               following location(s):\n"
+              ^ String.concat "\n" local_requires
+            else ""
+          in
+          "# 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 \
+            recursive with a trait implementation):\n\n" ^ msgs)
   in
   let type_infos =
     TypesAnalysis.analyze_type_declarations type_decls type_decls_list

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/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.