From 525c5a301e538bc0527560a9ae6e35d073004648 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 1 Jul 2024 10:11:30 +0200 Subject: [PATCH] Update charon --- charon-pin | 2 +- compiler/AssociatedTypes.ml | 8 +++++++- compiler/InterpreterExpansion.ml | 3 ++- compiler/RegionsHierarchy.ml | 3 +++ compiler/SymbolicToPure.ml | 12 +++++++++++- compiler/SynthesizeSymbolic.ml | 4 +++- compiler/TypesAnalysis.ml | 2 +- flake.lock | 6 +++--- 8 files changed, 31 insertions(+), 9 deletions(-) diff --git a/charon-pin b/charon-pin index ceea1ef11..645a5ad78 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. -7fb1eaada218a3f010a3dbeb337aad30beac417f +aeeae1d46704810bf498db552a75dff15aa3abcc diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index 4de5382aa..558cfacfd 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -95,7 +95,7 @@ let rec trait_instance_id_is_local_clause (id : trait_instance_id) : bool = match id with | Self | Clause _ -> true | TraitImpl _ | BuiltinOrAuto _ | TraitRef _ | UnknownTrait _ | FnPointer _ - | Closure _ | Unsolved _ -> + | Closure _ | Unsolved _ | Dyn _ -> false | ParentClause (id, _, _) | ItemClause (id, _, _, _) -> trait_instance_id_is_local_clause id @@ -294,6 +294,9 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty = let tr : trait_type_ref = { trait_ref; type_name } in (* Lookup the representative, if there is *) match norm_ctx_get_ty_repr ctx tr with None -> ty | Some ty -> ty) + | TDynTrait _ -> + craise_opt_span __FILE__ __LINE__ ctx.span + "Dynamic trait types are not supported yet" (** This returns the normalized trait instance id together with an optional reference to a trait **implementation** (the `trait_ref` we return has @@ -449,6 +452,9 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) | Unsolved _ | UnknownTrait _ -> (* This is actually an error case *) (id, None) + | Dyn _ -> + craise_opt_span __FILE__ __LINE__ ctx.span + "Dynamic trait types are not supported yet" and norm_ctx_normalize_generic_args (ctx : norm_ctx) (generics : generic_args) : generic_args = diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index c4e37646d..b14331fd9 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -665,7 +665,8 @@ let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) : (* We can't expand those *) craise __FILE__ __LINE__ span "Attempted to greedily expand an ADT which can't be expanded " - | TVar _ | TLiteral _ | TNever | TTraitType _ | TArrow _ | TRawPtr _ -> + | TVar _ | TLiteral _ | TNever | TTraitType _ | TArrow _ | TRawPtr _ + | TDynTrait _ -> craise __FILE__ __LINE__ span "Unreachable" in (* *) diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml index 61fa37d95..f58af48ef 100644 --- a/compiler/RegionsHierarchy.ml +++ b/compiler/RegionsHierarchy.ml @@ -186,6 +186,9 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option) "We don't support arrow types with locally quantified regions"; (* We can ignore the outer regions *) List.iter (explore_ty []) (output :: inputs) + | TDynTrait _ -> + craise_opt_span __FILE__ __LINE__ span + "Dynamic trait types are not supported yet" and explore_generics (outer : region list) (generics : generic_args) = let { regions; types; const_generics = _; trait_refs = _ } = generics in List.iter (fun long -> add_edges ~long ~shorts:outer) regions; diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index e829ed302..3d657ebf0 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -456,6 +456,8 @@ and translate_trait_instance_id (span : Meta.span) (translate_ty : T.ty -> ty) | TraitRef tr -> TraitRef (translate_trait_ref span translate_ty tr) | FnPointer _ | Closure _ -> craise __FILE__ __LINE__ span "Closures are not supported yet" + | Dyn _ -> + craise __FILE__ __LINE__ span "Dynamic trait types are not supported yet" | Unsolved _ -> craise __FILE__ __LINE__ span "Couldn't solve trait bound" | UnknownTrait s -> craise __FILE__ __LINE__ span ("Unknown trait found: " ^ s) @@ -496,6 +498,8 @@ let rec translate_sty (span : Meta.span) (ty : T.ty) : ty = TTraitType (trait_ref, type_name) | TArrow _ -> craise __FILE__ __LINE__ span "Arrow types are not supported yet" + | TDynTrait _ -> + craise __FILE__ __LINE__ span "Dynamic trait types are not supported yet" and translate_sgeneric_args (span : Meta.span) (generics : T.generic_args) : generic_args = @@ -672,6 +676,8 @@ let rec translate_fwd_ty (span : Meta.span) (type_infos : type_infos) TTraitType (trait_ref, type_name) | TArrow _ -> craise __FILE__ __LINE__ span "Arrow types are not supported yet" + | TDynTrait _ -> + craise __FILE__ __LINE__ span "Dynamic trait types are not supported yet" and translate_fwd_generic_args (span : Meta.span) (type_infos : type_infos) (generics : T.generic_args) : generic_args = @@ -782,6 +788,8 @@ let rec translate_back_ty (span : Meta.span) (type_infos : type_infos) else None | TArrow _ -> craise __FILE__ __LINE__ span "Arrow types are not supported yet" + | TDynTrait _ -> + craise __FILE__ __LINE__ span "Dynamic trait types are not supported yet" (** Simply calls [translate_back_ty] *) let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool) @@ -2306,7 +2314,9 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : let dest = mk_typed_pattern_from_var dest dest_mplace in (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, dest) | CastFnPtr _ -> - craise __FILE__ __LINE__ ctx.span "TODO: function casts") + craise __FILE__ __LINE__ ctx.span "TODO: function casts" + | CastUnsize _ -> + craise __FILE__ __LINE__ ctx.span "TODO: unsize coercions") | S.Binop binop -> ( match args with | [ arg0; arg1 ] -> diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index b15ab38ac..d0b0b7d65 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -83,7 +83,9 @@ let synthesize_symbolic_expansion (span : Meta.span) (sv : symbolic_value) match ls with | [ (Some see, exp) ] -> ExpandNoBranch (see, exp) | _ -> craise __FILE__ __LINE__ span "Ill-formed borrow expansion") - | TVar _ | TLiteral TChar | TNever | TTraitType _ | TArrow _ | TRawPtr _ -> + | TVar _ + | TLiteral TChar + | TNever | TTraitType _ | TArrow _ | TRawPtr _ | TDynTrait _ -> craise __FILE__ __LINE__ span "Ill-formed symbolic expansion" in Expansion (place, sv, expansion) diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml index 86baa3921..7fb8f7ead 100644 --- a/compiler/TypesAnalysis.ml +++ b/compiler/TypesAnalysis.ml @@ -147,7 +147,7 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos) let rec analyze (expl_info : expl_info) (ty_info : partial_type_info) (ty : ty) : partial_type_info = match ty with - | TLiteral _ | TNever | TTraitType _ -> ty_info + | TLiteral _ | TNever | TTraitType _ | TDynTrait _ -> ty_info | TVar var_id -> ( (* Update the information for the proper parameter, if necessary *) match ty_info.param_infos with diff --git a/flake.lock b/flake.lock index 907aae55e..6772358d1 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1719733805, - "narHash": "sha256-kXtKdgbqm4PEZRmi4Rg7RRtFdlb+7HcV7N1SEeHIsBU=", + "lastModified": 1719829160, + "narHash": "sha256-M9APcqyQtLfteKUqePDt+jgio4OzQ7EvRuBwXgkCQWA=", "owner": "aeneasverif", "repo": "charon", - "rev": "7fb1eaada218a3f010a3dbeb337aad30beac417f", + "rev": "aeeae1d46704810bf498db552a75dff15aa3abcc", "type": "github" }, "original": {