diff options
| -rw-r--r-- | src/Interpreter.ml | 68 | ||||
| -rw-r--r-- | src/Values.ml | 9 |
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 |