Merge pull request #387 from Nadrieril/pre-debruijn

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.
-7744bf94275e2ba3e7a2e4163c1fa062225d7a75
+4f5cb493fd5e02976f51eb6aa636f615d7b96fcf

src/interp/InterpreterBorrows.ml

@@ -1813,7 +1813,7 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
                 let ty =
                   (* Take the first region of the abstraction - this doesn't really matter *)
                   let r = RegionId.Set.min_elt abs0.regions in
-                  TRef (RFVar r, ty, RShared)
+                  TRef (RVar (Free r), ty, RShared)
                 in
                 { value; ty }
               in
@@ -1935,7 +1935,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
         | VSharedBorrow bid ->
             cassert __FILE__ __LINE__ (ty_no_regions ref_ty) span
               "Nested borrows are not supported yet";
-            let ty = TRef (RFVar r_id, ref_ty, kind) in
+            let ty = TRef (RVar (Free r_id), ref_ty, kind) in
             let value = ABorrow (ASharedBorrow (PNone, bid)) in
             ([ { value; ty } ], v)
         | VMutBorrow (bid, bv) ->
@@ -1945,7 +1945,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
               (not (value_has_borrows (Some span) ctx bv.value))
               span "Nested borrows are not supported yet";
             (* Create an avalue to push - note that we use [AIgnore] for the inner avalue *)
-            let ty = TRef (RFVar r_id, ref_ty, kind) in
+            let ty = TRef (RVar (Free r_id), ref_ty, kind) in
             let ignored = mk_aignored span ref_ty None in
             let av = ABorrow (AMutBorrow (PNone, bid, ignored)) in
             let av = { value = av; ty } in
@@ -1971,7 +1971,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
             (* We use [AIgnore] for the inner value *)
             let ignored = mk_aignored span ty None in
             (* For avalues, a loan has the type borrow (see the comments in [avalue]) *)
-            let ty = mk_ref_ty (RFVar r_id) ty RShared in
+            let ty = mk_ref_ty (RVar (Free r_id)) ty RShared in
             (* Rem.: the shared value might contain loans *)
             let avl, sv = to_avalues false true true r_id sv in
             let av = ALoan (ASharedLoan (PNone, bids, sv, ignored)) in
@@ -1991,7 +1991,7 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
             (* We use [AIgnore] for the inner value *)
             let ignored = mk_aignored span ty in
             (* For avalues, a loan has the type borrow (see the comments in [avalue]) *)
-            let ty = mk_ref_ty (RFVar r_id) ty RMut in
+            let ty = mk_ref_ty (RVar (Free r_id)) ty RMut in
             let av = ALoan (AMutLoan (PNone, bid, ignored None)) in
             let av = { value = av; ty } in
             ([ av ], v))

src/interp/InterpreterLoopsFixedPoint.ml

@@ -231,7 +231,7 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
     let child_av = mk_aignored span child_rty None in
 
     (* Create the shared loan *)
-    let loan_rty = TRef (RFVar nrid, rty, RShared) in
+    let loan_rty = TRef (RVar (Free nrid), rty, RShared) in
     let loan_value =
       ALoan (ASharedLoan (PNone, BorrowId.Set.singleton nlid, nsv, child_av))
     in

src/interp/InterpreterLoopsMatchCtxs.ml

@@ -520,7 +520,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
 
       (* Update the type of the shared loan to use the fresh region *)
       let _, bv_ty, kind = ty_as_ref ty in
-      let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
+      let borrow_ty = mk_ref_ty (RVar (Free rid)) bv_ty kind in
 
       (* Generate the avalues for the abstraction *)
       let mk_aborrow (pm : proj_marker) (bid : borrow_id) : typed_avalue =
@@ -633,7 +633,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
         let bv_ty = bv.ty in
         cassert __FILE__ __LINE__ (ty_no_regions bv_ty) span
           "Nested borrows are not supported yet";
-        let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
+        let borrow_ty = mk_ref_ty (RVar (Free rid)) bv_ty kind in
 
         let borrow_av =
           let ty = borrow_ty in
@@ -685,7 +685,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
       let _, bv_ty, kind = ty_as_ref ty in
       let sv = mk_fresh_symbolic_typed_value_from_no_regions_ty span bv_ty in
 
-      let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
+      let borrow_ty = mk_ref_ty (RVar (Free rid)) bv_ty kind in
 
       (* Generate the avalues for the abstraction *)
       let mk_aborrow (pm : proj_marker) (bid : borrow_id) (bv : typed_value) :
@@ -1110,9 +1110,9 @@ struct
     let match_regions r0 r1 =
       match (r0, r1) with
       | RStatic, RStatic -> r1
-      | RFVar rid0, RFVar rid1 ->
+      | RVar (Free rid0), RVar (Free rid1) ->
           let rid = match_rid rid0 rid1 in
-          RFVar rid
+          RVar (Free rid)
       | _ -> raise (Distinct "match_rtys")
     in
     match_types span ctx0 ctx1 match_distinct_types match_regions ty0 ty1

src/llbc/AssociatedTypes.ml

@@ -221,13 +221,14 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
   | TRawPtr (ty, rkind) ->
       let ty = norm_ctx_normalize_ty ctx ty in
       TRawPtr (ty, rkind)
-  | TArrow (regions, inputs, output) ->
+  | TArrow binder ->
       (* TODO: for now it works because we don't support predicates with
          bound regions. If we do support them, we probably need to do
          something smarter here. *)
+      let { binder_regions; binder_value = inputs, output } = binder in
       let inputs = List.map (norm_ctx_normalize_ty ctx) inputs in
       let output = norm_ctx_normalize_ty ctx output in
-      TArrow (regions, inputs, output)
+      TArrow { binder_regions; binder_value = (inputs, output) }
   | TTraitType (trait_ref, type_name) -> (
       log#ldebug
         (lazy
@@ -512,7 +513,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 : RegionVarId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty)
+    (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)

src/llbc/Builtin.ml

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

src/llbc/RegionsHierarchy.ml

@@ -88,19 +88,19 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
     Subst.fresh_regions_with_substs_from_vars sg.generics.regions
       (snd (RegionId.fresh_stateful_generator ()))
   in
-  let region_id_to_var_map : RegionVarId.id RegionId.Map.t =
+  let region_id_to_var_map : BoundRegionId.id RegionId.Map.t =
     RegionId.Map.of_list
       (List.map
          (fun (var_id, id) -> (id, var_id))
-         (RegionVarId.Map.bindings region_var_to_id_map))
+         (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) ->
-          (RFVar (bound_regions_id_subst r.index), s_set))
+          (RVar (Free (bound_regions_id_subst r.index)), s_set))
         sg.generics.regions
     in
     let s = (RStatic, RegionSet.empty) in
@@ -113,7 +113,7 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
     sanity_check_opt_span __FILE__ __LINE__ (long <> RErased) span;
     (* Ignore the locally bound regions (at the level of arrow types for instance *)
     match (short, long) with
-    | RBVar _, _ | _, RBVar _ -> ()
+    | RVar (Bound _), _ | _, RVar (Bound _) -> ()
     | _, _ ->
         let m = !g in
         let s = RegionMap.find short !g in
@@ -196,11 +196,13 @@ let compute_regions_hierarchy_for_sig (span : Meta.span option)
           span;
         (* We have nothing to do *)
         ()
-    | TArrow (regions, inputs, output) ->
+    | TArrow binder ->
         (* TODO: *)
-        cassert_opt_span __FILE__ __LINE__ (regions = []) span
-          "We don't support arrow types with locally quantified regions";
+        cassert_opt_span __FILE__ __LINE__
+          (binder.binder_regions = [])
+          span "We don't support arrow types with locally quantified regions";
         (* We can ignore the outer regions *)
+        let inputs, output = binder.binder_value in
         List.iter (explore_ty []) (output :: inputs)
     | TDynTrait _ ->
         craise_opt_span __FILE__ __LINE__ span
@@ -296,11 +298,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 : RegionVarId.id list =
+      let regions : BoundRegionId.id list =
         List.map
           (fun r ->
             match r with
-            | RFVar rid -> RegionId.Map.find rid region_id_to_var_map
+            | RVar (Free rid) -> RegionId.Map.find rid region_id_to_var_map
             | _ -> craise __FILE__ __LINE__ (Option.get span) "Unreachable")
           scc
       in

src/llbc/Substitute.ml

@@ -10,41 +10,43 @@ open ContextsBase
 open Errors
 
 (** Substitute regions at the binding level where we start to substitute *)
-let make_region_subst_from_fn (subst : RegionVarId.id -> region) :
-    region -> region = function
+let make_region_subst_from_fn (subst : BoundRegionId.id -> region) :
+    de_bruijn_var -> region = function
   (* The DeBruijn index is kept correct wrt the start of the substituttion *)
-  | RBVar (bdid, rid) when bdid = 0 -> subst rid
-  | r -> r
+  | 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 [RegionVarId.id -> RegionId.id]
+    TODO: simplify? we only need the subst [BoundRegionId.id -> RegionId.id]
   *)
-let fresh_regions_with_substs (region_vars : RegionVarId.id list)
+let fresh_regions_with_substs (region_vars : BoundRegionId.id list)
     (fresh_region_id : unit -> region_id) :
-    RegionId.id RegionVarId.Map.t
-    * (RegionVarId.id -> RegionId.id)
-    * (region -> region) =
+    RegionId.id BoundRegionId.Map.t
+    * (BoundRegionId.id -> RegionId.id)
+    * (de_bruijn_var -> region) =
   (* Map each region var id to a fresh region *)
   let rid_map =
-    RegionVarId.Map.of_list
+    BoundRegionId.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 = RegionVarId.Map.find id rid_map in
+  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 -> RFVar (rid_subst id)) in
+  let r_subst =
+    make_region_subst_from_fn (fun id -> RVar (Free (rid_subst id)))
+  in
   (* Return *)
   (rid_map, rid_subst, r_subst)
 
 let fresh_regions_with_substs_from_vars (region_vars : region_var list)
     (fresh_region_id : unit -> region_id) :
-    RegionId.id RegionVarId.Map.t
-    * (RegionVarId.id -> RegionId.id)
-    * (region -> region) =
+    RegionId.id BoundRegionId.Map.t
+    * (BoundRegionId.id -> RegionId.id)
+    * (de_bruijn_var -> region) =
   fresh_regions_with_substs
     (List.map (fun (r : region_var) -> r.index) region_vars)
     fresh_region_id
@@ -55,12 +57,14 @@ 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 : RegionVarId.id -> RegionId.id) (ty_subst : TypeVarId.id -> ty)
+    (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)
     (regions_hierarchy : region_var_groups) : inst_fun_sig =
-  let r_subst' = make_region_subst_from_fn (fun id -> RFVar (r_subst id)) in
+  let r_subst' =
+    make_region_subst_from_fn (fun id -> RVar (Free (r_subst id)))
+  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

src/llbc/Types.ml

@@ -1 +1,6 @@
 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 : RegionVarId.Set.t;
+  mut_regions : BoundRegionId.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 = RegionVarId.Set.empty;
+    mut_regions = BoundRegionId.Set.empty;
   }
 
 let initialize_type_decl_info (is_rec : bool) (def : type_decl) : type_decl_info
@@ -138,18 +138,18 @@ 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 = RegionVarId.of_int (RegionId.to_int rid) in
-    if RegionVarId.Set.mem rid mut_regions then ty_info.mut_regions
+    let rid = BoundRegionId.of_int (RegionId.to_int rid) in
+    if BoundRegionId.Set.mem rid mut_regions then ty_info.mut_regions
     else (
       updated := true;
-      RegionVarId.Set.add rid mut_regions)
+      BoundRegionId.Set.add rid mut_regions)
   in
   let update_mut_regions mut_regions mut_region =
     match mut_region with
-    | RStatic | RBVar _ ->
+    | RStatic | RVar (Bound _) ->
         mut_regions (* We can have bound vars because of arrows *)
     | RErased -> craise_opt_span __FILE__ __LINE__ span "Unreachable"
-    | RFVar rid -> update_mut_regions_with_rid mut_regions rid
+    | RVar (Free rid) -> update_mut_regions_with_rid mut_regions rid
   in
 
   (* Update a partial_type_info, while registering if we actually performed an update *)
@@ -336,19 +336,22 @@ let analyze_full_ty (span : Meta.span option) (updated : bool ref)
             (fun mut_regions (adt_rid, r) ->
               (* Check if the region is a variable and is used for mutable borrows *)
               match r with
-              | RStatic | RBVar _ | RErased -> mut_regions
+              | RStatic | RVar (Bound _) | RErased -> mut_regions
               (* We can have bound vars because of arrows, and erased regions
                  when analyzing types appearing in function bodies *)
-              | RFVar rid ->
-                  if RegionVarId.Set.mem adt_rid adt_info.mut_regions then
+              | RVar (Free rid) ->
+                  if BoundRegionId.Set.mem adt_rid adt_info.mut_regions then
                     update_mut_regions_with_rid mut_regions rid
                   else mut_regions)
             ty_info.mut_regions
-            (RegionVarId.mapi (fun adt_rid r -> (adt_rid, r)) generics.regions)
+            (BoundRegionId.mapi
+               (fun adt_rid r -> (adt_rid, r))
+               generics.regions)
         in
         (* Return *)
         { ty_info with mut_regions }
-    | TArrow (_regions, inputs, output) ->
+    | TArrow binder ->
+        let inputs, output = binder.binder_value in
         (* Just dive into the arrow *)
         let ty_info =
           List.fold_left