From 0727595a26b7bbe03568c7e556a09ff449acaf87 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 21 Jan 2022 10:47:15 +0100
Subject: Update projections_intersect to write it in terms of a more generic
 function

---
 src/InterpreterBorrowsCore.ml | 102 ++++++++++++++++++++++++++++++------------
 src/Invariants.ml             |   5 +++
 2 files changed, 79 insertions(+), 28 deletions(-)

(limited to 'src')

diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 6e582e92..1bcff935 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -78,57 +78,103 @@ let add_borrow_or_abs_id_to_chain (msg : string) (id : borrow_or_abs_id)
       ^ borrow_or_abs_ids_chain_to_string (id :: ids))
   else id :: ids
 
-(** Check if two different projections intersect. This is necessary when
-    giving a symbolic value to an abstraction: we need to check that
-    the regions which are already ended inside the abstraction don't
-    intersect the regions over which we project in the new abstraction.
-    Note that the two abstractions have different views (in terms of regions)
-    of the symbolic value (hence the two region types).
-*)
-let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.Set.t)
-    (ty2 : T.rty) (rset2 : T.RegionId.Set.t) : bool =
+(** Helper function.
+  
+    This function allows to define in a generic way a comparison of region types.
+    See [projections_interesect] for instance.
+    
+    [default]: default boolean to return, when comparing types with no regions
+    [combine]: how to combine booleans
+    [compare_regions]: how to compare regions
+ *)
+let rec compare_rtys (default : bool) (combine : bool -> bool -> bool)
+    (compare_regions : T.RegionId.id T.region -> T.RegionId.id T.region -> bool)
+    (ty1 : T.rty) (ty2 : T.rty) : bool =
+  let compare = compare_rtys default combine compare_regions in
   match (ty1, ty2) with
-  | T.Bool, T.Bool | T.Char, T.Char | T.Str, T.Str -> false
+  | T.Bool, T.Bool | T.Char, T.Char | T.Str, T.Str -> default
   | T.Integer int_ty1, T.Integer int_ty2 ->
       assert (int_ty1 = int_ty2);
-      false
+      default
   | T.Adt (id1, regions1, tys1), T.Adt (id2, regions2, tys2) ->
       assert (id1 = id2);
-      (* The intersection check for the ADTs is very crude: 
-       * we check if some arguments intersect. As all the type and region
+
+      (* The check for the ADTs is very crude: we simply compare the arguments
+       * two by two.
+       *
+       * For instance, when checking if some projections intersect, we simply
+       * check if some arguments intersect. As all the type and region
        * parameters should be used somewhere in the ADT (otherwise rustc
        * generates an error), it means that it should be equivalent to checking
        * whether two fields intersect (and anyway comparing the field types is
        * difficult in case of enumerations...).
        * If we didn't have the above property enforced by the rust compiler,
        * this check would still be a reasonable conservative approximation. *)
+
+      (* Check the region parameters *)
       let regions = List.combine regions1 regions2 in
+      let params_b =
+        List.fold_left
+          (fun b (r1, r2) -> combine b (compare_regions r1 r2))
+          default regions
+      in
+      (* Check the type parameters *)
       let tys = List.combine tys1 tys2 in
-      List.exists
-        (fun (r1, r2) -> region_in_set r1 rset1 && region_in_set r2 rset2)
-        regions
-      || List.exists
-           (fun (ty1, ty2) -> projections_intersect ty1 rset1 ty2 rset2)
-           tys
-  | T.Array ty1, T.Array ty2 | T.Slice ty1, T.Slice ty2 ->
-      projections_intersect ty1 rset1 ty2 rset2
+      let tys_b =
+        List.fold_left
+          (fun b (ty1, ty2) -> combine b (compare ty1 ty2))
+          default tys
+      in
+      (* Combine *)
+      combine params_b tys_b
+  | T.Array ty1, T.Array ty2 | T.Slice ty1, T.Slice ty2 -> compare ty1 ty2
   | T.Ref (r1, ty1, kind1), T.Ref (r2, ty2, kind2) ->
       (* Sanity check *)
       assert (kind1 = kind2);
-      (* The projections intersect if the borrows intersect or their contents
-       * intersect *)
-      (region_in_set r1 rset1 && region_in_set r2 rset2)
-      || projections_intersect ty1 rset1 ty2 rset2
+      (* Explanation for the case where we check if projections intersect:
+       * the projections intersect if the borrows intersect or their contents
+       * intersect. *)
+      let regions_b = compare_regions r1 r2 in
+      let tys_b = compare ty1 ty2 in
+      combine regions_b tys_b
   | T.TypeVar id1, T.TypeVar id2 ->
       assert (id1 = id2);
-      false
+      default
   | _ ->
       log#lerror
         (lazy
-          ("projections_intersect: unexpected inputs:" ^ "\n- ty1: "
-         ^ T.show_rty ty1 ^ "\n- ty2: " ^ T.show_rty ty2));
+          ("compare_rtys: unexpected inputs:" ^ "\n- ty1: " ^ T.show_rty ty1
+         ^ "\n- ty2: " ^ T.show_rty ty2));
       failwith "Unreachable"
 
+(** Check if two different projections intersect. This is necessary when
+    giving a symbolic value to an abstraction: we need to check that
+    the regions which are already ended inside the abstraction don't
+    intersect the regions over which we project in the new abstraction.
+    Note that the two abstractions have different views (in terms of regions)
+    of the symbolic value (hence the two region types).
+*)
+let projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.Set.t) (ty2 : T.rty)
+    (rset2 : T.RegionId.Set.t) : bool =
+  let default = false in
+  let combine b1 b2 = b1 || b2 in
+  let compare_regions r1 r2 =
+    region_in_set r1 rset1 && region_in_set r2 rset2
+  in
+  compare_rtys default combine compare_regions ty1 ty2
+
+(** Check if the first projection contains the second projection.
+    We use this function when checking invariants.
+*)
+let projection_contains (ty1 : T.rty) (rset1 : T.RegionId.Set.t) (ty2 : T.rty)
+    (rset2 : T.RegionId.Set.t) : bool =
+  let default = true in
+  let combine b1 b2 = b1 && b2 in
+  let compare_regions r1 r2 =
+    region_in_set r1 rset1 || not (region_in_set r2 rset2)
+  in
+  compare_rtys default combine compare_regions ty1 ty2
+
 (** Lookup a loan content.
 
     The loan is referred to by a borrow id.
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 8582722d..fc3ab07a 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -721,9 +721,14 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit =
      * - the borrows are mutually disjoint
      * - the unions of the loans/borrows give everything
      *)
+    (* A symbolic value can't be both in the regular environment and inside
+     * projectors of borrows in abstractions *)
     assert (info.env_count = 0 || info.aproj_borrows = []);
+    (* A symbolic value containing borrows can't be duplicated (i.e., copied):
+     * it must be expanded first *)
     if ty_has_borrows ctx.type_context.type_infos info.ty then
       assert (info.env_count <= 1);
+    (* A duplicated symbolic value is necessarily primitively copyable *)
     assert (info.env_count <= 1 || ty_is_primitively_copyable info.ty)
   in
 
-- 
cgit v1.2.3