Clarify the use of region_id_set (#397)

* Make minor modifications

* Introduce the abs_regions helper type

src/interp/Interpreter.ml

@@ -209,7 +209,9 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
       eval_ctx * typed_avalue list =
     (* Project over the values - we use *loan* projectors, as explained above *)
     let avalues =
-      List.map (mk_aproj_loans_value_from_symbolic_value abs.regions) input_svs
+      List.map
+        (mk_aproj_loans_value_from_symbolic_value abs.regions.owned)
+        input_svs
     in
     (ctx, avalues)
   in
@@ -308,8 +310,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
       let compute_abs_avalues (abs : abs) (ctx : eval_ctx) :
           eval_ctx * typed_avalue list =
         let ctx, avalue =
-          apply_proj_borrows_on_input_value config span ctx abs.regions
-            abs.ancestors_regions ret_value ret_rty
+          apply_proj_borrows_on_input_value config span ctx abs.regions.owned
+            abs.regions.ancestors ret_value ret_rty
         in
         (ctx, [ avalue ])
       in

src/interp/InterpreterBorrows.ml

@@ -348,7 +348,8 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id)
                   let given_back_meta = as_symbolic span nv.value in
                   (* The loan projector *)
                   let given_back =
-                    mk_aproj_loans_value_from_symbolic_value abs.regions sv
+                    mk_aproj_loans_value_from_symbolic_value abs.regions.owned
+                      sv
                   in
                   (* Continue giving back in the child value *)
                   let child = super#visit_typed_avalue opt_abs child in
@@ -372,7 +373,7 @@ let give_back_value (config : config) (span : Meta.span) (bid : BorrowId.id)
         let regions, ancestors_regions =
           match opt_abs with
           | None -> craise __FILE__ __LINE__ span "Unreachable"
-          | Some abs -> (abs.regions, abs.ancestors_regions)
+          | Some abs -> (abs.regions.owned, abs.regions.ancestors)
         in
         (* Rk.: there is a small issue with the types of the aloan values.
          * See the comment at the level of definition of {!typed_avalue} *)
@@ -1069,7 +1070,9 @@ and end_abstraction_aux (config : config) (span : Meta.span)
          relookup the abstraction: the set of regions in an abstraction never
          changes... *)
       let ctx =
-        let ended_regions = RegionId.Set.union ctx.ended_regions abs.regions in
+        let ended_regions =
+          RegionId.Set.union ctx.ended_regions abs.regions.owned
+        in
         { ctx with ended_regions }
       in
 
@@ -1137,7 +1140,8 @@ and end_abstraction_loans (config : config) (span : Meta.span)
       (* There is a proj_loans over a symbolic value: end the proj_borrows
          which intersect this proj_loans, then end the proj_loans itself *)
       let ctx, cc =
-        end_proj_loans_symbolic config span chain abs_id abs.regions sv ctx
+        end_proj_loans_symbolic config span chain abs_id abs.regions.owned sv
+          ctx
       in
       (* Reexplore, looking for loans *)
       comp cc (end_abstraction_loans config span chain abs_id ctx)
@@ -1287,7 +1291,8 @@ and end_abstraction_borrows (config : config) (span : Meta.span)
       let ctx = update_aproj_borrows span abs.abs_id sv ended_borrow ctx in
       (* Give back the symbolic value *)
       let ctx =
-        give_back_symbolic_value config span abs.regions proj_ty sv nsv ctx
+        give_back_symbolic_value config span abs.regions.owned proj_ty sv nsv
+          ctx
       in
       (* Reexplore *)
       end_abstraction_borrows config span chain abs_id ctx
@@ -1812,7 +1817,7 @@ let destructure_abs (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
                    have the type `& ...` - TODO: this is annoying and not very clean... *)
                 let ty =
                   (* Take the first region of the abstraction - this doesn't really matter *)
-                  let r = RegionId.Set.min_elt abs0.regions in
+                  let r = RegionId.Set.min_elt abs0.regions.owned in
                   TRef (RVar (Free r), ty, RShared)
                 in
                 { value; ty }
@@ -1860,8 +1865,11 @@ let convert_value_to_abstractions (span : Meta.span) (abs_kind : abs_kind)
           can_end;
           parents = AbstractionId.Set.empty;
           original_parents = [];
-          regions = RegionId.Set.singleton r_id;
-          ancestors_regions = RegionId.Set.empty;
+          regions =
+            {
+              owned = RegionId.Set.singleton r_id;
+              ancestors = RegionId.Set.empty;
+            };
           avalues;
         }
       in
@@ -2924,9 +2932,14 @@ let merge_abstractions (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
       (AbstractionId.Set.of_list [ abs0.abs_id; abs1.abs_id ])
   in
   let original_parents = AbstractionId.Set.elements parents in
-  let regions = RegionId.Set.union abs0.regions abs1.regions in
-  let ancestors_regions =
-    RegionId.Set.diff (RegionId.Set.union abs0.regions abs1.regions) regions
+  let regions =
+    let owned = RegionId.Set.union abs0.regions.owned abs1.regions.owned in
+    let ancestors =
+      RegionId.Set.diff
+        (RegionId.Set.union abs0.regions.ancestors abs1.regions.ancestors)
+        owned
+    in
+    { owned; ancestors }
   in
   let abs =
     {
@@ -2936,7 +2949,6 @@ let merge_abstractions (span : Meta.span) (abs_kind : abs_kind) (can_end : bool)
       parents;
       original_parents;
       regions;
-      ancestors_regions;
       avalues;
     }
   in
@@ -2978,7 +2990,7 @@ let merge_into_first_abstraction (span : Meta.span) (abs_kind : abs_kind)
      is not the case if there are no nested borrows, but we anticipate).
   *)
   let ctx =
-    let regions = nabs.regions in
+    let regions = nabs.regions.owned in
     (* Pick the first region id (this is the smallest) *)
     let rid = RegionId.Set.min_elt regions in
     (* If there is only one region, do nothing *)

src/interp/InterpreterBorrowsCore.ml

@@ -738,7 +738,7 @@ let lookup_intersecting_aproj_borrows_opt (span : Meta.span)
   let check_add_proj_borrows (is_shared : bool) abs sv' proj_ty =
     if
       proj_borrows_intersects_proj_loans span
-        (abs.regions, sv', proj_ty)
+        (abs.regions.owned, sv', proj_ty)
         (regions, sv)
     then
       let x = (abs.abs_id, proj_ty) in
@@ -832,7 +832,7 @@ let update_intersecting_aproj_borrows (span : Meta.span)
   let check_proj_borrows is_shared abs sv' proj_ty =
     if
       proj_borrows_intersects_proj_loans span
-        (abs.regions, sv', proj_ty)
+        (abs.regions.owned, sv', proj_ty)
         (regions, sv)
     then (
       if is_shared then add_shared () else set_non_shared ();
@@ -994,7 +994,7 @@ let update_intersecting_aproj_loans (span : Meta.span)
               sanity_check __FILE__ __LINE__ (sv.sv_ty = sv'.sv_ty) span;
               if
                 projections_intersect span proj_ty proj_regions sv'.sv_ty
-                  abs.regions
+                  abs.regions.owned
               then update abs given_back
               else super#visit_aproj (Some abs) sproj)
             else super#visit_aproj (Some abs) sproj

src/interp/InterpreterExpansion.ml

@@ -86,8 +86,8 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
 
       method! visit_ASymbolic current_abs aproj =
         let current_abs = Option.get current_abs in
-        let proj_regions = current_abs.regions in
-        let ancestors_regions = current_abs.ancestors_regions in
+        let proj_regions = current_abs.regions.owned in
+        let ancestors_regions = current_abs.regions.ancestors in
         (* Explore in depth first - we won't update anything: we simply
          * want to check we don't have to expand inner symbolic value *)
         match (aproj, proj_kind) with
@@ -336,7 +336,7 @@ let expand_symbolic_value_shared_borrow (config : config) (span : Meta.span)
 
       method! visit_EAbs proj_regions abs =
         sanity_check __FILE__ __LINE__ (Option.is_none proj_regions) span;
-        let proj_regions = Some abs.regions in
+        let proj_regions = Some abs.regions.owned in
         super#visit_EAbs proj_regions abs
 
       method! visit_AProjSharedBorrow proj_regions asb =

src/interp/InterpreterLoopsFixedPoint.ml

@@ -209,7 +209,9 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
     let nrid = fresh_region_id () in
 
     (* Prepare the shared value *)
-    let nsv = mk_value_with_fresh_sids_no_shared_loans abs.regions nrid sv in
+    let nsv =
+      mk_value_with_fresh_sids_no_shared_loans abs.regions.owned nrid sv
+    in
 
     (* Save the borrow substitution, to apply it to the context later *)
     borrow_substs := (lid, nlid) :: !borrow_substs;
@@ -218,7 +220,7 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
     sanity_check __FILE__ __LINE__ (AbstractionId.Set.is_empty abs.parents) span;
     sanity_check __FILE__ __LINE__ (abs.original_parents = []) span;
     sanity_check __FILE__ __LINE__
-      (RegionId.Set.is_empty abs.ancestors_regions)
+      (RegionId.Set.is_empty abs.regions.ancestors)
       span;
 
     (* Introduce the new abstraction for the shared values *)
@@ -250,15 +252,17 @@ let prepare_ashared_loans (span : Meta.span) (loop_id : LoopId.id option) :
       | None -> Identity
     in
     let can_end = true in
+    let regions : abs_regions =
+      { owned = RegionId.Set.singleton nrid; ancestors = RegionId.Set.empty }
+    in
     let fresh_abs =
       {
         abs_id = fresh_abstraction_id ();
         kind;
         can_end;
         parents = AbstractionId.Set.empty;
         original_parents = [];
-        regions = RegionId.Set.singleton nrid;
-        ancestors_regions = RegionId.Set.empty;
+        regions;
         avalues;
       }
     in

src/interp/InterpreterLoopsMatchCtxs.ml

@@ -546,8 +546,11 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
           can_end = true;
           parents = AbstractionId.Set.empty;
           original_parents = [];
-          regions = RegionId.Set.singleton rid;
-          ancestors_regions = RegionId.Set.empty;
+          regions =
+            {
+              owned = RegionId.Set.singleton rid;
+              ancestors = RegionId.Set.empty;
+            };
           avalues;
         }
       in
@@ -661,8 +664,11 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
             can_end = true;
             parents = AbstractionId.Set.empty;
             original_parents = [];
-            regions = RegionId.Set.singleton rid;
-            ancestors_regions = RegionId.Set.empty;
+            regions =
+              {
+                owned = RegionId.Set.singleton rid;
+                ancestors = RegionId.Set.empty;
+              };
             avalues;
           }
         in
@@ -714,8 +720,11 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
           can_end = true;
           parents = AbstractionId.Set.empty;
           original_parents = [];
-          regions = RegionId.Set.singleton rid;
-          ancestors_regions = RegionId.Set.empty;
+          regions =
+            {
+              owned = RegionId.Set.singleton rid;
+              ancestors = RegionId.Set.empty;
+            };
           avalues;
         }
       in
@@ -1388,8 +1397,7 @@ let match_ctxs (span : Meta.span) (check_equiv : bool) (fixed_ids : ids_sets)
       can_end = can_end0;
       parents = parents0;
       original_parents = original_parents0;
-      regions = regions0;
-      ancestors_regions = ancestors_regions0;
+      regions = { owned = regions0; ancestors = ancestors_regions0 };
       avalues = avalues0;
     } =
       abs0
@@ -1401,8 +1409,7 @@ let match_ctxs (span : Meta.span) (check_equiv : bool) (fixed_ids : ids_sets)
       can_end = can_end1;
       parents = parents1;
       original_parents = original_parents1;
-      regions = regions1;
-      ancestors_regions = ancestors_regions1;
+      regions = { owned = regions1; ancestors = ancestors_regions1 };
       avalues = avalues1;
     } =
       abs1
@@ -1995,16 +2002,23 @@ let match_ctx_with_target (config : config) (span : Meta.span)
 
       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."
+          "Internal error: 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))
+        | Free id ->
+            (* If the bound region is free, then it is a region owned
+               by an abstraction, so we do the same as for the case
+               [abs_region_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
+      method! visit_abs_regions _ regions =
+        let { owned; ancestors } = regions in
+        let owned = RegionId.Set.map get_region_id owned in
+        let ancestors = RegionId.Set.map get_region_id ancestors in
+        { owned; ancestors }
 
       (** We also need to change the abstraction kind *)
       method! visit_abs env abs =

src/interp/InterpreterStatements.ml

@@ -514,19 +514,18 @@ let create_empty_abstractions_from_abs_region_groups
         AbstractionId.Set.empty rg.parents
     in
     let regions =
-      List.fold_left
-        (fun s rid -> RegionId.Set.add rid s)
-        RegionId.Set.empty rg.regions
-    in
-    let ancestors_regions =
-      List.fold_left
-        (fun acc parent_id ->
-          RegionId.Set.union acc
-            (AbstractionId.Map.find parent_id !abs_to_ancestors_regions))
-        RegionId.Set.empty rg.parents
+      let owned = RegionId.Set.of_list rg.regions in
+      let ancestors =
+        List.fold_left
+          (fun acc parent_id ->
+            RegionId.Set.union acc
+              (AbstractionId.Map.find parent_id !abs_to_ancestors_regions))
+          RegionId.Set.empty rg.parents
+      in
+      { owned; ancestors }
     in
     let ancestors_regions_union_current_regions =
-      RegionId.Set.union ancestors_regions regions
+      RegionId.Set.union regions.owned regions.owned
     in
     let can_end = region_can_end rg_id in
     abs_to_ancestors_regions :=
@@ -540,7 +539,6 @@ let create_empty_abstractions_from_abs_region_groups
       parents;
       original_parents;
       regions;
-      ancestors_regions;
       avalues = [];
     }
   in
@@ -1443,12 +1441,12 @@ and eval_function_call_symbolic_from_inst_sig (config : config)
     let ctx, args_projs =
       List.fold_left_map
         (fun ctx (arg, arg_rty) ->
-          apply_proj_borrows_on_input_value config span ctx abs.regions
-            abs.ancestors_regions arg arg_rty)
+          apply_proj_borrows_on_input_value config span ctx abs.regions.owned
+            abs.regions.ancestors arg arg_rty)
         ctx args_with_rtypes
     in
     (* Group the input and output values *)
-    (ctx, List.append args_projs [ ret_av abs.regions ])
+    (ctx, List.append args_projs [ ret_av abs.regions.owned ])
   in
   (* Actually initialize and insert the abstractions *)
   let call_id = fresh_fun_call_id () in

src/interp/InterpreterUtils.ml

@@ -342,6 +342,9 @@ type ids_sets = {
   loan_ids : BorrowId.Set.t;  (** Only the loan ids *)
   dids : DummyVarId.Set.t;
   rids : RegionId.Set.t;
+      (** This should only contain **free** region ids (note that we have to be
+          careful because we use the same index type for bound regions and free
+          regions - see the implementation of [compute_ids] below) *)
   sids : SymbolicValueId.Set.t;
 }
 [@@deriving show]
@@ -399,8 +402,9 @@ let compute_ids () =
         | 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_abs_regions _ (regions : abs_regions) : unit =
+        let { owned; ancestors } = regions in
+        rids := RegionId.Set.union (RegionId.Set.union owned ancestors) !rids
 
       method! visit_symbolic_value env sv =
         sids := SymbolicValueId.Set.add sv.sv_id !sids;
@@ -514,7 +518,7 @@ 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
-  (* Refresh the region ids so that we can subsequently generate more fresh regions without clash *)
+  (* Generate fresh regions *)
   let rsubst =
     Substitute.fresh_regions_with_substs_from_vars sg.generics.regions
       fresh_region_id