summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorNadrieril2024-06-05 10:08:56 +0200
committerGuillaume Boisseau2024-06-06 09:36:36 +0200
commit7f2b8bf304f9c21f34c4be44a087cc15c56d6b07 (patch)
treefe3f354c716c17f217da7ec15a5d4630f5390d2e /compiler
parent961cc880311aed3319b08755c5a43816e2490d7f (diff)
Filter out type aliases
Diffstat (limited to '')
-rw-r--r--compiler/InterpreterExpansion.ml4
-rw-r--r--compiler/PrePasses.ml46
-rw-r--r--compiler/PureMicroPasses.ml2
-rw-r--r--compiler/SymbolicToPure.ml3
-rw-r--r--compiler/TypesAnalysis.ml5
5 files changed, 52 insertions, 8 deletions
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 *)