Remove ty_has_regions and use ty_has_borrows instead

8 files changed, 34 insertions, 39 deletions

diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 8b039510..0842dee7 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -535,7 +535,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) (ctx : C.eval_ctx)
       inherit [_] C.iter_eval_ctx
 
       method! visit_Symbolic _ sv =
-        if ty_has_regions (Subst.erase_regions sv.V.sv_ty) then
+        if ty_has_borrows ctx.type_context.type_infos sv.V.sv_ty then
           raise (FoundSymbolicValue sv)
         else ()
 
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index f15c7558..60918bac 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -35,7 +35,10 @@ let expand_primitively_copyable_at_place (config : C.config)
   (* Small helper *)
   let rec expand ctx =
     let v = read_place_unwrap config access p ctx in
-    match find_first_primitively_copyable_sv v with
+    match
+      find_first_primitively_copyable_sv_with_borrows
+        ctx.type_context.type_infos v
+    with
     | None -> ctx
     | Some sv ->
         let ctx = expand_symbolic_value_no_branching config sv ctx in
@@ -178,7 +181,10 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
       let ctx, v = prepare_rplace config expand_prim_copy access p ctx in
       (* Copy the value *)
       assert (not (bottom_in_value ctx.ended_regions v));
-      assert (Option.is_none (find_first_primitively_copyable_sv v));
+      assert (
+        Option.is_none
+          (find_first_primitively_copyable_sv_with_borrows
+             ctx.type_context.type_infos v));
       let allow_adt_copy = false in
       copy_value allow_adt_copy config ctx v
   | Expressions.Move p -> (
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 85c3acb4..74886bf9 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -945,7 +945,10 @@ and eval_non_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx)
     C.eval_ctx =
   (* Sanity check: make sure the type parameters don't contain regions -
    * this is a current limitation of our synthesis *)
-  assert (List.for_all (fun ty -> not (ty_has_regions ty)) type_params);
+  assert (
+    List.for_all
+      (fun ty -> not (ty_has_borrows ctx.type_context.type_infos ty))
+      type_params);
 
   (* There are two cases (and this is extremely annoying):
      - the function is not box_free
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index e00e7dcf..ca437593 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -81,6 +81,8 @@ let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
     
     Checks if the projector will actually project some regions. If not,
     returns [AIgnored] (`_`).
+    
+    TODO: update to handle 'static
  *)
 let mk_aproj_loans_value_from_symbolic_value (regions : T.RegionId.Set.t)
     (svalue : V.symbolic_value) : V.typed_avalue =
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 5b77e13c..67084684 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -707,7 +707,8 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit =
   (* Check *)
   let check_info _id info =
     assert (info.env_count = 0 || info.aproj_borrows = []);
-    if ty_has_regions info.ty then assert (info.env_count <= 1);
+    if ty_has_borrows ctx.type_context.type_infos info.ty then
+      assert (info.env_count <= 1);
     assert (info.env_count <= 1 || ty_is_primitively_copyable info.ty)
   in
   M.iter check_info !infos
diff --git a/src/TypesAnalysis.ml b/src/TypesAnalysis.ml
index f49b49ac..acb0f963 100644
--- a/src/TypesAnalysis.ml
+++ b/src/TypesAnalysis.ml
@@ -80,8 +80,9 @@ let partial_type_info_to_ty_info (info : partial_type_info) : ty_info =
     param_infos = ();
   }
 
-let analyze_full_ty (updated : bool ref) (infos : type_infos)
-    (ty_info : partial_type_info) (ty : 'r gr_ty) : partial_type_info =
+let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
+    (infos : type_infos) (ty_info : partial_type_info) (ty : 'r ty) :
+    partial_type_info =
   (* Small utility *)
   let check_update_bool (original : bool) (nv : bool) : bool =
     if nv && not original then (
@@ -107,7 +108,7 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos)
 
   (* The recursive function which explores the type *)
   let rec analyze (expl_info : expl_info) (ty_info : partial_type_info)
-      (ty : 'r gr_ty) : partial_type_info =
+      (ty : 'r ty) : partial_type_info =
     match ty with
     | Bool | Char | Never | Integer _ | Str -> ty_info
     | TypeVar var_id -> (
@@ -142,7 +143,7 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos)
         in
         (* Set `contains_static` *)
         let contains_static =
-          check_update_bool ty_info.contains_static (r = Static)
+          check_update_bool ty_info.contains_static (r_is_static r)
         in
         let ty_info = { ty_info with contains_static } in
         (* Update the type info *)
@@ -164,7 +165,7 @@ let analyze_full_ty (updated : bool ref) (infos : type_infos)
               {
                 ty_info with
                 contains_static =
-                  check_update_bool ty_info.contains_static (r = Static);
+                  check_update_bool ty_info.contains_static (r_is_static r);
               })
             ty_info regions
         in
@@ -207,11 +208,13 @@ let analyze_type_def (updated : bool ref) (infos : type_infos) (def : type_def)
           (List.map (fun v -> List.map (fun f -> f.field_ty) v.fields) variants)
   in
   (* Explore the types and accumulate information *)
+  let r_is_static r = r = Static in
   let type_def_info = TypeDefId.Map.find def.def_id infos in
   let type_def_info = type_def_info_to_partial_type_info type_def_info in
   let type_def_info =
     List.fold_left
-      (fun type_def_info ty -> analyze_full_ty updated infos type_def_info ty)
+      (fun type_def_info ty ->
+        analyze_full_ty r_is_static updated infos type_def_info ty)
       type_def_info fields_tys
   in
   let type_def_info = partial_type_info_to_type_def_info type_def_info in
@@ -263,10 +266,12 @@ let analyze_type_declarations (type_defs : type_def TypeDefId.Map.t)
 (** Analyze a type to check whether it contains borrows, etc., provided
     we have already analyzed the type definitions in the context.
  *)
-let analyze_ty (infos : type_infos) (ty : 'r gr_ty) : ty_info =
+let analyze_ty (infos : type_infos) (ty : 'r ty) : ty_info =
   (* We don't use `updated` but need to give it as parameter *)
   let updated = ref false in
+  (* We don't need to compute whether the type contains 'static or not *)
+  let r_is_static _ = false in
   let ty_info = initialize_g_type_info None in
-  let ty_info = analyze_full_ty updated infos ty_info ty in
+  let ty_info = analyze_full_ty r_is_static updated infos ty_info ty in
   (* Convert the ty_info *)
   partial_type_info_to_ty_info ty_info
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index 10bd286c..ef260830 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -92,29 +92,6 @@ let rec ety_no_regions_to_rty (ty : ety) : rty =
         "Can't convert a ref with erased regions to a ref with non-erased \
          regions"
 
-(** Check if a [ty] contains regions.
-
-    TODO: rename to "has_borrows"?
-    TODO: update, and check the usage.
-  *)
-let ty_has_regions (ty : 'r ty) : bool =
-  let obj =
-    object
-      inherit [_] iter_ty as super
-
-      method! visit_Adt env type_id regions tys =
-        if regions = [] then super#visit_Adt env type_id regions tys
-        else raise Found
-
-      method! visit_Ref _ _ _ _ = raise Found
-    end
-  in
-  raise Errors.Unimplemented;
-  try
-    obj#visit_ty () ty;
-    false
-  with Found -> true
-
 (** Retuns true if a type contains borrows.
 
     Note that we can't simply explore the type and look for regions: sometimes
diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml
index 4555fd50..f3876f53 100644
--- a/src/ValuesUtils.ml
+++ b/src/ValuesUtils.ml
@@ -2,6 +2,7 @@ open Utils
 open TypesUtils
 open Types
 open Values
+module TA = TypesAnalysis
 
 exception FoundSymbolicValue of symbolic_value
 (** Utility exception *)
@@ -88,8 +89,8 @@ let outer_loans_in_value (v : typed_value) : bool =
     false
   with Found -> true
 
-let find_first_primitively_copyable_sv (v : typed_value) : symbolic_value option
-    =
+let find_first_primitively_copyable_sv_with_borrows (type_infos : TA.type_infos)
+    (v : typed_value) : symbolic_value option =
   (* The visitor *)
   let obj =
     object
@@ -97,7 +98,7 @@ let find_first_primitively_copyable_sv (v : typed_value) : symbolic_value option
 
       method! visit_Symbolic _ sv =
         let ty = sv.sv_ty in
-        if ty_is_primitively_copyable ty && ty_has_regions ty then
+        if ty_is_primitively_copyable ty && ty_has_borrows type_infos ty then
           raise (FoundSymbolicValue sv)
         else ()
     end