diff options
Diffstat (limited to '')
| -rw-r--r-- | charon-pin | 2 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 4 | ||||
| -rw-r--r-- | compiler/PrePasses.ml | 46 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 2 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 3 | ||||
| -rw-r--r-- | compiler/TypesAnalysis.ml | 5 | ||||
| -rw-r--r-- | flake.lock | 6 |
7 files changed, 56 insertions, 12 deletions
@@ -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 *) @@ -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": { |