From eb385bfdaefc494c018ce02190b13eb08cf066a4 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jan 2022 10:01:50 +0100
Subject: Fix a small bug in projections_intersect and add more debugging
 output

---
 src/InterpreterBorrowsCore.ml | 52 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)

(limited to 'src/InterpreterBorrowsCore.ml')

diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 1d75bffb..3e402d88 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -7,6 +7,7 @@ module V = Values
 module C = Contexts
 module Subst = Substitute
 module L = Logging
+open TypesUtils
 open InterpreterUtils
 
 (** The local logger *)
@@ -51,6 +52,57 @@ type loan_or_borrow_content =
   | BorrowContent of V.borrow_content
 [@@deriving show]
 
+(** 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 =
+  match (ty1, ty2) with
+  | T.Bool, T.Bool | T.Char, T.Char | T.Str, T.Str -> false
+  | T.Integer int_ty1, T.Integer int_ty2 ->
+      assert (int_ty1 = int_ty2);
+      false
+  | 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
+       * 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. *)
+      let regions = List.combine regions1 regions2 in
+      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
+  | 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
+  | T.TypeVar id1, T.TypeVar id2 ->
+      assert (id1 = id2);
+      false
+  | _ ->
+      log#lerror
+        (lazy
+          ("projections_intersect: unexpected inputs:" ^ "\n- ty1: "
+         ^ T.show_rty ty1 ^ "\n- ty2: " ^ T.show_rty ty2));
+      failwith "Unreachable"
+
 (** Lookup a loan content.
 
     The loan is referred to by a borrow id.
-- 
cgit v1.2.3