Update charon

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.
-ba7db7e30304485e74d9e529da808403f7d72492
+85a1ee1cdfe1d7f2672bece3d190425e1f06c881

src/PrePasses.ml

@@ -189,20 +189,19 @@ let update_array_default (crate : crate) : crate =
                   in
                   let generics =
                     {
-                      sg.generics with
+                      fdecl.generics with
                       const_generics =
                         [ { index = cg_id; name = "N"; ty = TUInt Usize } ];
                     }
                   in
                   let sg =
                     {
                       sg with
-                      generics;
                       output =
                         TAdt { id = TBuiltin TArray; generics = array_generics };
                     }
                   in
-                  let fdecl = { fdecl with signature = sg } in
+                  let fdecl = { fdecl with signature = sg; generics } in
                   Some fdecl
               | _ -> [%internal_error] fdecl.item_meta.span)
             else (* Filter *)

src/Translate.ml

@@ -355,7 +355,7 @@ let translate_crate_to_pure (crate : crate) (marked_ids : marked_ids) :
       (fun (info : builtin_fun_info) ->
         SymbolicToPureTypes.translate_fun_sig trans_ctx (FBuiltin info.fun_id)
           info.name info.fun_sig
-          (List.map (fun _ -> None) info.fun_sig.inputs))
+          (List.map (fun _ -> None) info.fun_sig.item_binder_value.inputs))
       builtin_fun_infos
   in
 

src/interp/Interp.ml

@@ -121,11 +121,12 @@ let compute_contexts (crate : crate) : decls_ctx =
     We return a new context because we compute and add the type normalization
     map in the same step. *)
 let symbolic_instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx)
-    (sg : fun_sig) (regions_hierarchy : region_var_groups) (_kind : item_source)
-    : eval_ctx * inst_fun_sig =
+    (sg : bound_fun_sig) (regions_hierarchy : region_var_groups)
+    (_kind : item_source) : eval_ctx * inst_fun_sig =
   let tr_self = UnknownTrait "symbolic_instantiate_fun_sig" in
   let generics =
-    Substitute.generic_args_of_params_erase_regions (Some span) sg.generics
+    Substitute.generic_args_of_params_erase_regions (Some span)
+      sg.item_binder_params
   in
   let inst_sg =
     instantiate_fun_sig span ctx generics tr_self sg regions_hierarchy
@@ -177,15 +178,16 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx)
     List.map (fun (g : region_var_group) -> g.id) regions_hierarchy
   in
   let ctx =
-    initialize_eval_ctx (Some span) ctx region_groups sg.generics.types
-      sg.generics.const_generics marked_ids
+    initialize_eval_ctx (Some span) ctx region_groups fdef.generics.types
+      fdef.generics.const_generics marked_ids
   in
   (* Instantiate the signature. This updates the context because we compute
      at the same time the normalization map for the associated types.
   *)
   let ctx, inst_sg =
-    symbolic_instantiate_fun_sig span ctx fdef.signature regions_hierarchy
-      fdef.src
+    symbolic_instantiate_fun_sig span ctx
+      (bound_fun_sig_of_decl fdef)
+      regions_hierarchy fdef.src
   in
   (* Create fresh symbolic values for the inputs *)
   let input_svs =
@@ -268,8 +270,9 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
     FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
   in
   let _, ret_inst_sg =
-    symbolic_instantiate_fun_sig span ctx fdef.signature regions_hierarchy
-      fdef.src
+    symbolic_instantiate_fun_sig span ctx
+      (bound_fun_sig_of_decl fdef)
+      regions_hierarchy fdef.src
   in
   let ret_rty = ret_inst_sg.output in
 
@@ -486,7 +489,7 @@ module Test = struct
         fdef.item_meta.name];
 
     (* Sanity check - *)
-    [%sanity_check] span (fdef.signature.generics = empty_generic_params);
+    [%sanity_check] span (fdef.generics = empty_generic_params);
     [%sanity_check] span (body.locals.arg_count = 0);
 
     (* Create the evaluation context *)
@@ -521,7 +524,7 @@ module Test = struct
       (no parameters, no arguments) - TODO: move *)
   let fun_decl_is_transparent_unit (def : fun_decl) : bool =
     Option.is_some def.body
-    && def.signature.generics = empty_generic_params
+    && def.generics = empty_generic_params
     && def.signature.inputs = []
 
   (** Test all the unit functions in a list of function definitions *)

src/interp/InterpBorrowsCore.ml

@@ -1820,16 +1820,26 @@ let rec norm_proj_tys_union (span : Meta.span) (ty1 : rty) (ty2 : rty) : rty =
       [%sanity_check] span (item1 = item2);
       TTraitType (norm_proj_trait_refs_union span tr1 tr2, item1)
   | ( TFnPtr
-        { binder_regions = binder_regions1; binder_value = inputs1, output1 },
+        {
+          binder_regions = binder_regions1;
+          binder_value =
+            { is_unsafe = false; inputs = inputs1; output = output1 };
+        },
       TFnPtr
-        { binder_regions = binder_regions2; binder_value = inputs2, output2 } )
-    ->
+        {
+          binder_regions = binder_regions2;
+          binder_value =
+            { is_unsafe = false; inputs = inputs2; output = output2 };
+        } ) ->
       (* TODO: general case *)
       [%sanity_check] span (binder_regions1 = []);
       [%sanity_check] span (binder_regions2 = []);
       let binder_value =
-        ( List.map2 (norm_proj_tys_union span) inputs1 inputs2,
-          norm_proj_tys_union span output1 output2 )
+        {
+          is_unsafe = false;
+          inputs = List.map2 (norm_proj_tys_union span) inputs1 inputs2;
+          output = norm_proj_tys_union span output1 output2;
+        }
       in
       TFnPtr { binder_regions = []; binder_value }
   | _ -> [%internal_error] span

src/interp/InterpStatements.ml

@@ -274,8 +274,8 @@ let get_builtin_function_return_type (span : Meta.span) (fid : builtin_fun_id)
   let sg = Builtin.get_builtin_fun_sig fid in
   (* Instantiate the return type  *)
   let generics = Subst.generic_args_erase_regions generics in
-  let subst = Subst.make_subst_from_generics sg.generics generics in
-  Subst.erase_regions_substitute_types subst sg.output
+  let subst = Subst.make_subst_from_generics sg.item_binder_params generics in
+  Subst.erase_regions_substitute_types subst sg.item_binder_value.output
 
 let move_return_value (config : config) (span : Meta.span)
     (pop_return_value : bool) (ctx : eval_ctx) :
@@ -659,19 +659,20 @@ let eval_non_builtin_function_call_symbolic_inst (span : Meta.span)
       in
       (* Lookup the declaration *)
       let def = ctx_lookup_fun_decl span ctx fid in
+      let signature = bound_fun_sig_of_decl def in
       [%ltrace
         "- call: " ^ call_to_string ctx call ^ "\n- call.generics:\n"
         ^ generic_args_to_string ctx func.generics
         ^ "\n- def.signature:\n"
-        ^ fun_sig_to_string ctx def.signature];
+        ^ fun_sig_to_string ctx signature];
       (* Instantiate *)
       let regions_hierarchy =
         [%silent_unwrap] span
           (LlbcAstUtils.FunIdMap.find_opt (FRegular fid)
              ctx.fun_ctx.regions_hierarchies)
       in
       let inst_sg =
-        instantiate_fun_sig span ctx generics tr_self def.signature
+        instantiate_fun_sig span ctx generics tr_self signature
           regions_hierarchy
       in
       (func.kind, func.generics, def, inst_sg)
@@ -1321,9 +1322,7 @@ and eval_non_builtin_function_call_concrete (config : config) (span : Meta.span)
       (* TODO: we need to normalize the types if we want to correctly support traits *)
       [%cassert] body.span (generics.trait_refs = [])
         "Traits are not supported yet in concrete mode";
-      let subst =
-        Subst.make_subst_from_generics def.signature.generics generics
-      in
+      let subst = Subst.make_subst_from_generics def.generics generics in
       let locals, body_st = Subst.fun_body_substitute_in_body subst body in
 
       (* Evaluate the input operands *)
@@ -1608,7 +1607,7 @@ and eval_builtin_function_call_symbolic (config : config) (span : Meta.span)
 
     (* Evaluate the function call *)
     eval_function_call_symbolic_from_inst_sig config span (FunId (FBuiltin fid))
-      sg inst_sig func.generics args dest ctx
+      sg.item_binder_value inst_sig func.generics args dest ctx
   end
   else begin
     (* Sanity check: make sure the type parameters don't contain regions -
@@ -1634,7 +1633,7 @@ and eval_builtin_function_call_symbolic (config : config) (span : Meta.span)
 
     (* Evaluate the function call *)
     eval_function_call_symbolic_from_inst_sig config span (FunId (FBuiltin fid))
-      sg inst_sig func.generics args dest ctx
+      sg.item_binder_value inst_sig func.generics args dest ctx
   end
 
 (** Evaluate a statement seen as a function body *)

src/interp/InterpUtils.ml

@@ -747,7 +747,7 @@ let initialize_eval_ctx (span : Meta.span option) (ctx : decls_ctx)
     region ids. This is mostly used in preparation of function calls (when
     evaluating in symbolic mode). *)
 let instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx)
-    (generics : generic_args) (tr_self : trait_ref_kind) (sg : fun_sig)
+    (generics : generic_args) (tr_self : trait_ref_kind) (sg : bound_fun_sig)
     (regions_hierarchy : region_var_groups) : inst_fun_sig =
   [%ldebug
     "- generics: "
@@ -769,20 +769,21 @@ let instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx)
   in
   (* Generate fresh regions *)
   let rsubst =
-    Substitute.fresh_regions_with_substs_from_vars sg.generics.regions
+    Substitute.fresh_regions_with_substs_from_vars sg.item_binder_params.regions
       ctx.fresh_region_id
   in
   (* Generate the type substitution. *)
   [%sanity_check] span (TypesUtils.trait_instance_id_no_regions tr_self);
   let tsubst =
-    Substitute.make_type_subst_from_vars sg.generics.types generics.types
+    Substitute.make_type_subst_from_vars sg.item_binder_params.types
+      generics.types
   in
   let cgsubst =
-    Substitute.make_const_generic_subst_from_vars sg.generics.const_generics
-      generics.const_generics
+    Substitute.make_const_generic_subst_from_vars
+      sg.item_binder_params.const_generics generics.const_generics
   in
   let tr_subst =
-    Substitute.make_trait_subst_from_clauses sg.generics.trait_clauses
+    Substitute.make_trait_subst_from_clauses sg.item_binder_params.trait_clauses
       generics.trait_refs
   in
   (* Substitute the signature *)
@@ -808,15 +809,20 @@ let compute_regions_hierarchy_for_fun_call fresh_abs_id
     (span : Meta.span option) (crate : crate) (fun_name : string)
     (type_vars : type_param list)
     (const_generic_vars : const_generic_param list)
-    (generic_args : generic_args) (sg : fun_sig) : inst_fun_sig =
+    (generic_args : generic_args) (sg : bound_fun_sig) : inst_fun_sig =
   (* We simply put everything into a "fake" signature, then call
      [compute_regions_hierarchy_for_sig].
 
      The important point is that we need to introduce fresh regions for
      the erased regions. When doing so, in order to make sure there are
      no collisions, we also refresh the other regions. *)
   (* Decompose the signature *)
-  let { is_unsafe; generics; inputs; output } = sg in
+  let {
+    item_binder_params = generics;
+    item_binder_value = { is_unsafe; inputs; output };
+  } =
+    sg
+  in
   (* Introduce the fresh regions *)
   let region_map = ref RegionId.Map.empty in
   let fresh_regions = ref RegionId.Set.empty in
@@ -872,7 +878,7 @@ let compute_regions_hierarchy_for_fun_call fresh_abs_id
         (* Keeping the same trait refs: it shouldn't have an impact *);
       }
     in
-    Substitute.make_subst_from_generics sg.generics generic_args
+    Substitute.make_subst_from_generics sg.item_binder_params generic_args
   in
 
   (* Substitute the inputs and outputs *)
@@ -931,7 +937,12 @@ let compute_regions_hierarchy_for_fun_call fresh_abs_id
       }
     in
 
-    let sg = { is_unsafe; generics; inputs; output } in
+    let sg =
+      {
+        item_binder_params = generics;
+        item_binder_value = { is_unsafe; inputs; output };
+      }
+    in
     let regions_hierarchy =
       RegionsHierarchy.compute_regions_hierarchy_for_sig span crate fun_name sg
     in

src/llbc/Builtin.ml

@@ -85,11 +85,14 @@ module Sig = struct
   let mk_slice_ty (ty : ty) : ty =
     TAdt { id = TBuiltin TSlice; generics = mk_generic_args [] [ ty ] [] }
 
-  let mk_sig generics inputs output : fun_sig =
-    { is_unsafe = false; generics; inputs; output }
+  let mk_sig generics inputs output : bound_fun_sig =
+    {
+      item_binder_params = generics;
+      item_binder_value = { inputs; output; is_unsafe = false };
+    }
 
   (** [fn<T>(T) -> Box<T>] *)
-  let box_new_sig : fun_sig =
+  let box_new_sig : bound_fun_sig =
     let generics =
       mk_generic_params [] [ type_param_0 ] []
       (* <T> *)
@@ -102,7 +105,7 @@ module Sig = struct
     mk_sig generics inputs output
 
   (** [fn<T>(Box<T>) -> ()] *)
-  let box_free_sig : fun_sig =
+  let box_free_sig : bound_fun_sig =
     let generics =
       mk_generic_params [] [ type_param_0 ] []
       (* <T> *)
@@ -128,7 +131,7 @@ module Sig = struct
       a mutable borrow. *)
   let mk_array_slice_borrow_sig (cgs : const_generic_param list)
       (input_ty : ty -> ty) (index_ty : ty option) (output_ty : ty -> ty)
-      (is_mut : bool) : fun_sig =
+      (is_mut : bool) : bound_fun_sig =
     let generics =
       mk_generic_params [ region_param_0 ] [ type_param_0 ] cgs (* <'a, T> *)
     in
@@ -146,7 +149,8 @@ module Sig = struct
     in
     mk_sig generics inputs output
 
-  let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : fun_sig =
+  let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : bound_fun_sig
+      =
     (* Array<T, N> *)
     let input_ty ty =
       if is_array then mk_array_ty ty cgvar_0 else mk_slice_ty ty
@@ -161,7 +165,7 @@ module Sig = struct
   let array_index_sig (is_mut : bool) = mk_array_slice_index_sig true is_mut
   let slice_index_sig (is_mut : bool) = mk_array_slice_index_sig false is_mut
 
-  let array_to_slice_sig (is_mut : bool) : fun_sig =
+  let array_to_slice_sig (is_mut : bool) : bound_fun_sig =
     (* Array<T, N> *)
     let input_ty ty = mk_array_ty ty cgvar_0 in
     (* Slice<T> *)
@@ -182,7 +186,7 @@ module Sig = struct
     mk_sig generics inputs output
 
   (** Helper: [fn<T>(&'a [T]) -> usize] *)
-  let slice_len_sig : fun_sig =
+  let slice_len_sig : bound_fun_sig =
     let generics =
       mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
     in
@@ -196,11 +200,12 @@ module Sig = struct
     mk_sig generics inputs output
 end
 
-type raw_builtin_fun_info = builtin_fun_id * fun_sig * bool * bool list option
+type raw_builtin_fun_info =
+  builtin_fun_id * bound_fun_sig * bool * bool list option
 
 type builtin_fun_info = {
   fun_id : builtin_fun_id;
-  fun_sig : fun_sig;
+  fun_sig : bound_fun_sig;
   can_fail : bool;
   name : string;
   keep_types : bool list option;
@@ -278,7 +283,7 @@ let get_builtin_fun_info (id : builtin_fun_id) : builtin_fun_info =
       raise
         (Failure ("get_builtin_fun_info: not found: " ^ show_builtin_fun_id id))
 
-let get_builtin_fun_sig (id : builtin_fun_id) : fun_sig =
+let get_builtin_fun_sig (id : builtin_fun_id) : bound_fun_sig =
   (get_builtin_fun_info id).fun_sig
 
 let get_builtin_fun_name (id : builtin_fun_id) : string =

src/llbc/LlbcAst.ml

@@ -2,6 +2,7 @@ open Types
 open Values
 include Charon.LlbcAst
 
+type bound_fun_sig = Charon.TypesUtils.bound_fun_sig
 type abs_region_group = (RegionId.id, AbsId.id) g_region_group [@@deriving show]
 type abs_region_groups = abs_region_group list [@@deriving show]