Start working on projections_intersect and apply_proj_borrows

2 files changed, 75 insertions, 2 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index caac0de7..8b929b0f 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -577,12 +577,76 @@ type outer_borrows_or_abs =
 exception FoundOuter of outer_borrows_or_abs
 (** Utility exception *)
 
+(** 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 : V.RegionId.set_t) (ty2 : T.rty)
+    (rset2 : V.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) ->
+      (* The intersection set 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) ->
+          V.RegionId.Set.mem r1 rset1 && V.RegionId.Set.mem 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 *)
+      (V.RegionId.Set.mem r1 rset1 && V.RegionId.Set.mem r2 rset2)
+      || projections_intersect ty1 rset1 ty2 rset2
+  | _ -> failwith "Unreachable"
+
+(** Apply (and reduce) a projector over borrows to a value.
+
+    - [regions]: the regions we project
+    - [v]: the value over which we project
+    - [ty]: the type with regions which we use for the projection (to
+      map borrows to regions - or to interpret the borrows as belonging
+      to some regions...)
+*)
 let apply_proj_borrows (regions : V.RegionId.set_t) (v : V.typed_value)
     (ty : T.rty) : V.typed_avalue =
-  (* Sanity check *)
+  (* Sanity check - TODO: move this elsewhere (here we perform the check at every
+   * recursive call which is a bit overkill...) *)
   let ety = Substitute.erase_regions ty in
   assert (ety = v.V.ty);
-  raise Unimplemented
+  (* Match *)
+  match (v.V.value, ty) with
+  | V.Concrete cv, (T.Bool | T.Char | T.Integer _ | T.Str) ->
+      raise Unimplemented
+  | V.Adt v, T.Adt (id, regions, tys) -> raise Unimplemented
+  | V.Bottom, _ -> failwith "Unreachable"
+  | V.Borrow bc, _ -> raise Unimplemented
+  | V.Loan lc, _ -> failwith "Unreachable"
+  | V.Symbolic s, _ ->
+      (* Check that the symbolic value doesn't contain already ended regions *)
+      raise Unimplemented;
+      { V.value = V.ASymbolic (V.AProjBorrows (s.V.svalue, ty)); V.ty }
+  | _ -> failwith "Unreachable" raise Unimplemented
 
 (** Auxiliary function to end borrows: lookup a borrow in the environment,
     update it (by returning an updated environment where the borrow has been
diff --git a/src/Values.ml b/src/Values.ml
index 09cf8aa6..4b5b9b4e 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -205,6 +205,15 @@ class ['self] map_typed_avalue_base =
 *)
 type avalue =
   | AConcrete of constant_value
+      (** Note that this case is not used in the projections to keep track of the
+          borrow graph (because there are no borrows in "concrete" values!) but
+          to correctly instantiate the backward functions (we may give back some
+          values at different moments: we need to remember what those values were
+          precisely). Also note that even though avalues and values are not the
+          same, once values are projected to avalues, those avalues still have
+          the structure of the original values (this is necessary, again, to
+          correctly instantiate the backward functions)
+       *)
   | AAdt of adt_avalue
   | ABottom
   | ALoan of aloan_content