Filter out type aliases

7 files changed, 56 insertions, 12 deletions

diff --git a/charon-pin b/charon-pin
index 3e646b13..2f35e2cf 100644
--- a/charon-pin
+++ b/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.
-3f3c013cbe726c2f3ae83e8a589eca47bce21a01
+335f6d7423c2c2a3863440bfd19507b5d2452aac
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 41190618..1690aa80 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -648,9 +648,9 @@ 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.name)
-            | Opaque ->
+            | Alias _ | Opaque ->
                 craise __FILE__ __LINE__ span
-                  "Attempted to greedily expand an opaque type");
+                  "Attempted to greedily expand an alias or opaque type");
             (* Also, we need to check if the definition is recursive *)
             if ctx_type_decl_is_rec ctx def_id then
               craise __FILE__ __LINE__ span
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 9eb3b712..5cef8b05 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -435,10 +435,47 @@ let remove_shallow_borrows (crate : crate) (f : fun_decl) : fun_decl =
       ^ "\n"));
   f
 
+(* Remove the type aliases from the type declarations and declaration groups *)
+let filter_type_aliases (crate : crate) : crate =
+  let type_decl_is_alias (ty : type_decl) =
+    match ty.kind with Alias _ -> true | _ -> false
+  in
+  (* Whether the declaration group has a single entry that is a type alias.
+     Type aliases should not be in recursive groups so we also ensure this doesn't
+     happen. *)
+  let decl_group_is_single_alias = function
+    | TypeGroup (NonRecGroup id) ->
+        type_decl_is_alias (TypeDeclId.Map.find id crate.type_decls)
+    | TypeGroup (RecGroup ids) ->
+        List.iter
+          (fun id ->
+            let ty = TypeDeclId.Map.find id crate.type_decls in
+            if type_decl_is_alias ty then
+              craise __FILE__ __LINE__ ty.item_meta.span
+                "found a type alias within a recursive group; this is \
+                 unexpected")
+          ids;
+        false
+    | _ -> false
+  in
+  {
+    crate with
+    type_decls =
+      TypeDeclId.Map.filter
+        (fun _id ty -> not (type_decl_is_alias ty))
+        crate.type_decls;
+    declarations =
+      List.filter
+        (fun decl -> not (decl_group_is_single_alias decl))
+        crate.declarations;
+  }
+
 let apply_passes (crate : crate) : crate =
-  let passes = [ remove_loop_breaks crate; remove_shallow_borrows crate ] in
+  let function_passes =
+    [ remove_loop_breaks crate; remove_shallow_borrows crate ]
+  in
   (* Attempt to apply a pass: if it fails we replace the body by [None] *)
-  let apply_pass (pass : fun_decl -> fun_decl) (f : fun_decl) =
+  let apply_function_pass (pass : fun_decl -> fun_decl) (f : fun_decl) =
     try pass f
     with CFailure (_, _) ->
       (* The error was already registered, we don't need to register it twice.
@@ -452,10 +489,11 @@ let apply_passes (crate : crate) : crate =
   in
   let fun_decls =
     List.fold_left
-      (fun fl pass -> FunDeclId.Map.map (apply_pass pass) fl)
-      crate.fun_decls passes
+      (fun fl pass -> FunDeclId.Map.map (apply_function_pass pass) fl)
+      crate.fun_decls function_passes
   in
   let crate = { crate with fun_decls } in
+  let crate = filter_type_aliases crate in
   log#ldebug
     (lazy ("After pre-passes:\n" ^ Print.Crate.crate_to_string crate ^ "\n"));
   crate
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index a22a39ab..b0cba250 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1202,7 +1202,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                 in
                 let fields =
                   match adt_decl.kind with
-                  | Enum _ | Opaque ->
+                  | Enum _ | Alias _ | Opaque ->
                       craise __FILE__ __LINE__ def.span "Unreachable"
                   | Struct fields -> fields
                 in
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index ba6bba68..3975107a 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -564,6 +564,9 @@ let translate_type_decl_kind (span : Meta.span) (kind : T.type_decl_kind) :
   match kind with
   | T.Struct fields -> Struct (translate_fields span fields)
   | T.Enum variants -> Enum (translate_variants span variants)
+  | Alias _ ->
+      craise __FILE__ __LINE__ span
+        "type aliases should have been removed earlier"
   | T.Opaque -> Opaque
 
 (** Translate a type definition from LLBC
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index 0be3a0d4..86baa392 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -272,7 +272,7 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos)
   analyze expl_info_init ty_info ty
 
 let type_decl_is_opaque (d : type_decl) : bool =
-  match d.kind with Struct _ | Enum _ -> false | Opaque -> true
+  match d.kind with Opaque -> true | _ -> false
 
 let analyze_type_decl (updated : bool ref) (infos : type_infos)
     (def : type_decl) : type_infos =
@@ -289,6 +289,9 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos)
             (List.map
                (fun v -> List.map (fun f -> f.field_ty) v.fields)
                variants)
+      | Alias _ ->
+          craise __FILE__ __LINE__ def.item_meta.span
+            "type aliases should have been removed earlier"
       | Opaque -> craise __FILE__ __LINE__ def.item_meta.span "unreachable"
     in
     (* Explore the types and accumulate information *)
diff --git a/flake.lock b/flake.lock
index 35e5e9cd..fa417e87 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1717573223,
-        "narHash": "sha256-56arhtgTmdFFLV/BnO3GQC0FEiWdEmzM4CakeSulT+k=",
+        "lastModified": 1717573936,
+        "narHash": "sha256-PDfOISJ5hmlbM4j4jy8k0BTBYF6hPikM3ob4TbKCE/A=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "3f3c013cbe726c2f3ae83e8a589eca47bce21a01",
+        "rev": "335f6d7423c2c2a3863440bfd19507b5d2452aac",
         "type": "github"
       },
       "original": {