Rework how charon represents regions

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.
-b487babe3ae3021b484373ce59196896e3b43448
+c114a3aabc989b5ea3d72c3eccbde9869834460e

src/interp/InterpreterLoopsMatchCtxs.ml

@@ -1992,7 +1992,19 @@ let match_ctx_with_target (config : config) (span : Meta.span)
 
       method! visit_symbolic_value_id _ _ = fresh_symbolic_value_id ()
       method! visit_abstraction_id _ id = get_abs_id id
-      method! visit_region_id _ id = get_region_id id
+
+      method! visit_region_id _ _ =
+        craise_opt_span __FILE__ __LINE__ None
+          "Region ids should not be visited directly; the visitor should catch \
+           cases that contain region ids earlier."
+
+      method! visit_RVar _ var =
+        match var with
+        | Free id -> RVar (Free (get_region_id id))
+        | Bound _ -> RVar var
+
+      method! visit_region_id_set _ (ids : region_id_set) : region_id_set =
+        RegionId.Set.map get_region_id ids
 
       (** We also need to change the abstraction kind *)
       method! visit_abs env abs =

src/interp/InterpreterStatements.ml

@@ -287,13 +287,8 @@ let get_builtin_function_return_type (span : Meta.span) (ctx : eval_ctx)
   (* There shouldn't be any reference to Self *)
   let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in
   let generics = Subst.generic_args_erase_regions generics in
-  let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } =
-    Subst.make_subst_from_generics sg.generics generics tr_self
-  in
-  let ty =
-    Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
-      sg.output
-  in
+  let subst = Subst.make_subst_from_generics sg.generics generics tr_self in
+  let ty = Subst.erase_regions_substitute_types subst sg.output in
   AssociatedTypes.ctx_normalize_erase_ty span ctx ty
 
 let move_return_value (config : config) (span : Meta.span)
@@ -845,13 +840,8 @@ let eval_global_as_fresh_symbolic_value (span : Meta.span)
   (* There shouldn't be any reference to Self *)
   let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in
   let generics = Subst.generic_args_erase_regions generics in
-  let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } =
-    Subst.make_subst_from_generics global.generics generics tr_self
-  in
-  let ty =
-    Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
-      global.ty
-  in
+  let subst = Subst.make_subst_from_generics global.generics generics tr_self in
+  let ty = Subst.erase_regions_substitute_types subst global.ty in
   mk_fresh_symbolic_value span ty
 
 (** Evaluate a statement *)

src/interp/InterpreterUtils.ml

@@ -388,7 +388,19 @@ let compute_ids () =
         loan_ids := BorrowId.Set.add id !loan_ids
 
       method! visit_abstraction_id _ id = aids := AbstractionId.Set.add id !aids
-      method! visit_region_id _ id = rids := RegionId.Set.add id !rids
+
+      method! visit_region_id _ _ =
+        craise_opt_span __FILE__ __LINE__ None
+          "Region ids should not be visited directly; the visitor should catch \
+           cases that contain region ids earlier."
+
+      method! visit_RVar _ var =
+        match var with
+        | Free id -> rids := RegionId.Set.add id !rids
+        | Bound _ -> ()
+
+      method! visit_region_id_set _ (ids : region_id_set) : unit =
+        rids := RegionId.Set.union ids !rids
 
       method! visit_symbolic_value env sv =
         sids := SymbolicValueId.Set.add sv.sv_id !sids;
@@ -502,8 +514,8 @@ let instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx)
   let asubst (rg_id : RegionGroupId.id) : AbstractionId.id =
     RegionGroupId.Map.find rg_id asubst_map
   in
-  (* Generate fresh regions and their substitutions *)
-  let _, rsubst, _ =
+  (* Refresh the region ids so that we can subsequently generate more fresh regions without clash *)
+  let rsubst =
     Substitute.fresh_regions_with_substs_from_vars sg.generics.regions
       fresh_region_id
   in

src/llbc/AssociatedTypes.ml

@@ -499,7 +499,7 @@ let ctx_adt_get_inst_norm_field_etypes (span : Meta.span) (ctx : eval_ctx)
 (** Same as [substitute_signature] but normalizes the types *)
 let ctx_subst_norm_signature (span : Meta.span) (ctx : eval_ctx)
     (asubst : RegionGroupId.id -> AbstractionId.id)
-    (r_subst : BoundRegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty)
+    (r_subst : RegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty)
     (cg_subst : ConstGenericVarId.id -> const_generic)
     (tr_subst : TraitClauseId.id -> trait_instance_id)
     (tr_self : trait_instance_id) (sg : fun_sig)

src/llbc/Builtin.ml

@@ -36,8 +36,8 @@ open LlbcAst
 module Sig = struct
   (** A few utilities *)
 
-  let rvar_id_0 = BoundRegionId.of_int 0
-  let rvar_0 : region = RVar (zero_db_var rvar_id_0)
+  let rvar_id_0 = RegionId.of_int 0
+  let rvar_0 : region = RVar (Free rvar_id_0)
   let rg_id_0 = RegionGroupId.of_int 0
   let tvar_id_0 = TypeVarId.of_int 0
   let tvar_0 : ty = TVar (Free tvar_id_0)

src/llbc/RegionsHierarchy.ml

@@ -80,27 +80,15 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
      - the static region
      - edges from the region variables to the static region
 
-     Note that we introduce free variables for all the regions bound at the
+     Note that we only consider the regions bound at the
      level of the signature (this excludes the regions locally bound inside
      the types, for instance at the level of an arrow type).
   *)
-  let region_var_to_id_map, bound_regions_id_subst, bound_regions_subst =
-    Subst.fresh_regions_with_substs_from_vars sg.generics.regions
-      (snd (RegionId.fresh_stateful_generator ()))
-  in
-  let region_id_to_var_map : BoundRegionId.id RegionId.Map.t =
-    RegionId.Map.of_list
-      (List.map
-         (fun (var_id, id) -> (id, var_id))
-         (BoundRegionId.Map.bindings region_var_to_id_map))
-  in
-  let subst = { Subst.empty_subst with r_subst = bound_regions_subst } in
   let g : RegionSet.t RegionMap.t ref =
     let s_set = RegionSet.singleton RStatic in
     let m =
       List.map
-        (fun (r : region_var) ->
-          (RVar (Free (bound_regions_id_subst r.index)), s_set))
+        (fun (r : region_var) -> (RVar (Free r.index), s_set))
         sg.generics.regions
     in
     let s = (RStatic, RegionSet.empty) in
@@ -214,10 +202,7 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
   in
 
   (* Substitute the regions in a type, then explore *)
-  let explore_ty_subst ty =
-    let ty = Subst.ty_substitute subst ty in
-    explore_ty [] ty
-  in
+  let explore_ty_subst ty = explore_ty [] ty in
 
   (* Normalize the types then explore *)
   let tys =
@@ -298,11 +283,11 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
       let id = RegionGroupId.of_int i in
 
       (* Retrieve the set of regions in the group *)
-      let regions : BoundRegionId.id list =
+      let regions : RegionId.id list =
         List.map
           (fun r ->
             match r with
-            | RVar (Free rid) -> RegionId.Map.find rid region_id_to_var_map
+            | RVar (Free rid) -> rid
             | _ -> craise __FILE__ __LINE__ (Option.get span) "Unreachable")
           scc
       in

src/llbc/Substitute.ml

@@ -10,50 +10,24 @@ open ContextsBase
 open Errors
 
 (* Fails if the variable is bound *)
-let expect_free_var span (var : ('b, 'f) de_bruijn_var) : 'f =
+let expect_free_var span (var : 'id de_bruijn_var) : 'id =
   match var with
   | Bound _ ->
       craise_opt_span __FILE__ __LINE__ span "Found unexpected bound variable"
   | Free id -> id
 
-(** Substitute regions at the binding level where we start to substitute *)
-let make_region_subst_from_fn (subst : BoundRegionId.id -> region) :
-    region_db_var -> region = function
-  (* The DeBruijn index is kept correct wrt the start of the substituttion *)
-  | Bound (bdid, rid) when bdid = 0 -> subst rid
-  | r -> RVar r
-
-(** Generate fresh regions for region variables.
-
-    Return the list of new regions and appropriate substitutions from the
-    original region variables to the fresh regions.
-
-    TODO: simplify? we only need the subst [BoundRegionId.id -> RegionId.id]
-  *)
-let fresh_regions_with_substs (region_vars : BoundRegionId.id list)
-    (fresh_region_id : unit -> region_id) :
-    RegionId.id BoundRegionId.Map.t
-    * (BoundRegionId.id -> RegionId.id)
-    * (region_db_var -> region) =
+(** Generate fresh regions for region variables. *)
+let fresh_regions_with_substs (region_vars : RegionId.id list)
+    (fresh_region_id : unit -> region_id) : RegionId.id -> RegionId.id =
   (* Map each region var id to a fresh region *)
   let rid_map =
-    BoundRegionId.Map.of_list
+    RegionId.Map.of_list
       (List.map (fun var -> (var, fresh_region_id ())) region_vars)
   in
-  (* Generate the substitution from region var id to region *)
-  let rid_subst id = BoundRegionId.Map.find id rid_map in
-  (* Generate the substitution from region to region *)
-  let r_subst =
-    make_region_subst_from_fn (fun id -> RVar (Free (rid_subst id)))
-  in
-  (* Return *)
-  (rid_map, rid_subst, r_subst)
+  fun id -> RegionId.Map.find id rid_map
 
 let fresh_regions_with_substs_from_vars (region_vars : region_var list)
-    (fresh_region_id : unit -> region_id) :
-    RegionId.id BoundRegionId.Map.t
-    * (BoundRegionId.id -> RegionId.id)
-    * (region_db_var -> region) =
+    (fresh_region_id : unit -> region_id) : RegionId.id -> RegionId.id =
   fresh_regions_with_substs
     (List.map (fun (r : region_var) -> r.index) region_vars)
     fresh_region_id
@@ -64,20 +38,21 @@ let fresh_regions_with_substs_from_vars (region_vars : region_var list)
     **IMPORTANT:** this function doesn't normalize the types.
  *)
 let substitute_signature (asubst : RegionGroupId.id -> AbstractionId.id)
-    (r_subst : BoundRegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty)
-    (cg_subst : ConstGenericVarId.id -> const_generic)
-    (tr_subst : TraitClauseId.id -> trait_instance_id)
-    (tr_self : trait_instance_id) (sg : fun_sig)
+    (r_id_subst : RegionId.id -> RegionId.id) (ty_sb_subst : TypeVarId.id -> ty)
+    (cg_sb_subst : ConstGenericVarId.id -> const_generic)
+    (tr_sb_subst : TraitClauseId.id -> trait_instance_id)
+    (tr_sb_self : trait_instance_id) (sg : fun_sig)
     (regions_hierarchy : region_var_groups) : inst_fun_sig =
-  let r_subst' =
-    make_region_subst_from_fn (fun id -> RVar (Free (r_subst id)))
+  let r_sb_subst id = RVar (Free (r_id_subst id)) in
+  let subst =
+    subst_free_vars
+      { r_sb_subst; ty_sb_subst; cg_sb_subst; tr_sb_subst; tr_sb_self }
   in
-  let subst = { r_subst = r_subst'; ty_subst; cg_subst; tr_subst; tr_self } in
   let inputs = List.map (ty_substitute subst) sg.inputs in
   let output = ty_substitute subst sg.output in
   let subst_region_group (rg : region_var_group) : abs_region_group =
     let id = asubst rg.id in
-    let regions = List.map r_subst rg.regions in
+    let regions = List.map r_id_subst rg.regions in
     let parents = List.map asubst rg.parents in
     ({ id; regions; parents } : abs_region_group)
   in
@@ -118,7 +93,20 @@ let subst_ids_visitor (subst : id_subst) =
     inherit [_] map_env
     method! visit_type_var_id _ id = subst.ty_subst id
     method! visit_const_generic_var_id _ id = subst.cg_subst id
-    method! visit_region_id _ rid = subst.r_subst rid
+
+    method! visit_region_id _ _ =
+      craise_opt_span __FILE__ __LINE__ None
+        "Region ids should not be visited directly; the visitor should catch \
+         cases that contain region ids earlier."
+
+    method! visit_region_id_set _ (ids : region_id_set) : region_id_set =
+      RegionId.Set.map subst.r_subst ids
+
+    method! visit_RVar _ var =
+      match var with
+      | Free rid -> RVar (Free (subst.r_subst rid))
+      | Bound _ -> RVar var
+
     method! visit_borrow_id _ bid = subst.bsubst bid
     method! visit_loan_id _ bid = subst.bsubst bid
     method! visit_symbolic_value_id _ id = subst.ssubst id

src/llbc/Types.ml

@@ -1,6 +1,3 @@
 include Charon.Types
-module RegionId = FreeRegionId
 
-type bound_region_id = BoundRegionId.id [@@deriving show, ord]
-type region_id = RegionId.id [@@deriving show, ord]
 type region_id_set = RegionId.Set.t [@@deriving show, ord]

src/llbc/TypesAnalysis.ml

@@ -35,7 +35,7 @@ type 'p g_type_info = {
       (** If true, it means the type is a record that we should extract as a tuple.
           This field is only valid for type declarations.
       *)
-  mut_regions : BoundRegionId.Set.t;
+  mut_regions : RegionId.Set.t;
       (** The set of regions used in mutable borrows *)
 }
 [@@deriving show]
@@ -83,7 +83,7 @@ let initialize_g_type_info (is_tuple_struct : bool) (param_infos : 'p) :
     borrows_info = type_borrows_info_init;
     is_tuple_struct;
     param_infos;
-    mut_regions = BoundRegionId.Set.empty;
+    mut_regions = RegionId.Set.empty;
   }
 
 let initialize_type_decl_info (is_rec : bool) (def : type_decl) : type_decl_info
@@ -137,11 +137,11 @@ let analyze_full_ty (span : Meta.span option) (updated : bool ref)
   in
   let r_is_static (r : region) : bool = r = RStatic in
   let update_mut_regions_with_rid mut_regions rid =
-    let rid = BoundRegionId.of_int (RegionId.to_int rid) in
-    if BoundRegionId.Set.mem rid mut_regions then ty_info.mut_regions
+    let rid = RegionId.of_int (RegionId.to_int rid) in
+    if RegionId.Set.mem rid mut_regions then ty_info.mut_regions
     else (
       updated := true;
-      BoundRegionId.Set.add rid mut_regions)
+      RegionId.Set.add rid mut_regions)
   in
   let update_mut_regions mut_regions mut_region =
     match mut_region with
@@ -343,13 +343,11 @@ let analyze_full_ty (span : Meta.span option) (updated : bool ref)
               (* We can have bound vars because of arrows, and erased regions
                  when analyzing types appearing in function bodies *)
               | RVar (Free rid) ->
-                  if BoundRegionId.Set.mem adt_rid adt_info.mut_regions then
+                  if RegionId.Set.mem adt_rid adt_info.mut_regions then
                     update_mut_regions_with_rid mut_regions rid
                   else mut_regions)
             ty_info.mut_regions
-            (BoundRegionId.mapi
-               (fun adt_rid r -> (adt_rid, r))
-               generics.regions)
+            (RegionId.mapi (fun adt_rid r -> (adt_rid, r)) generics.regions)
         in
         (* Return *)
         { ty_info with mut_regions }
@@ -394,13 +392,6 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos)
       | Opaque | TError _ ->
           craise __FILE__ __LINE__ def.item_meta.span "unreachable"
     in
-    (* Substitute the regions in the fields *)
-    let _, _, r_subst =
-      Substitute.fresh_regions_with_substs_from_vars def.generics.regions
-        (snd (RegionId.fresh_stateful_generator ()))
-    in
-    let subst = { Substitute.empty_subst with r_subst } in
-    let fields_tys = List.map (Substitute.ty_substitute subst) fields_tys in
     (* Explore the types and accumulate information *)
     let type_decl_info = TypeDeclId.Map.find def.def_id infos in
     let type_decl_info = type_decl_info_to_partial_type_info type_decl_info in

src/llbc/TypesUtils.ml

@@ -92,10 +92,10 @@ let ty_has_mut_borrow_for_region_in_pred (infos : TypesAnalysis.type_infos)
           | TTuple | TBuiltin (TBox | TArray | TSlice | TStr) -> ()
           | TAdtId adt_id ->
               let info = TypeDeclId.Map.find adt_id infos in
-              BoundRegionId.iteri
+              RegionId.iteri
                 (fun adt_rid r ->
-                  if BoundRegionId.Set.mem adt_rid info.mut_regions && pred r
-                  then raise Found
+                  if RegionId.Set.mem adt_rid info.mut_regions && pred r then
+                    raise Found
                   else ())
                 generics.regions
         end;