summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Interpreter.ml68
-rw-r--r--src/Values.ml9
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