diff options
| -rw-r--r-- | TODO.md | 1 | ||||
| -rw-r--r-- | src/Identifiers.ml | 2 | ||||
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 52 | ||||
| -rw-r--r-- | src/InterpreterProjectors.ml | 25 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 43 |
5 files changed, 75 insertions, 48 deletions
@@ -9,7 +9,6 @@ * remove the rule which says that we can end a borrow under an abstraction if the corresponding loan is in the same abstraction. - Also remove the io parameter from "end_borrow". * add a `allow_borrow_overwrites` in the loan projectors. diff --git a/src/Identifiers.ml b/src/Identifiers.ml index d3e5b83e..18b8edee 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -63,6 +63,8 @@ module type Id = sig module Map : Map.S with type key = id + (* TODO: map_to_string *) + val id_of_json : Yojson.Basic.t -> (id, string) result end 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. diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml index cbd07f3e..18316610 100644 --- a/src/InterpreterProjectors.ml +++ b/src/InterpreterProjectors.ml @@ -219,11 +219,28 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) | V.Symbolic s, _ -> (* Check that the projection doesn't contain already ended regions, * if necessary *) - if check_symbolic_no_ended then - assert ( - not (projections_intersect s.V.sv_ty ctx.ended_regions ty regions)); + if check_symbolic_no_ended then ( + let ty1 = s.V.sv_ty in + let rset1 = ctx.ended_regions in + let ty2 = ty in + let rset2 = regions in + log#ldebug + (lazy + ("projections_intersect:" ^ "\n- ty1: " ^ rty_to_string ctx ty1 + ^ "\n- rset1: " + ^ T.RegionId.set_to_string rset1 + ^ "\n- ty2: " ^ rty_to_string ctx ty2 ^ "\n- rset2: " + ^ T.RegionId.set_to_string rset2 + ^ "\n")); + assert (not (projections_intersect ty1 rset1 ty2 rset2))); V.ASymbolic (V.AProjBorrows (s, ty)) - | _ -> failwith "Unreachable" + | _ -> + log#lerror + (lazy + ("apply_proj_borrows: unexpected inputs:\n- input value: " + ^ typed_value_to_string ctx v + ^ "\n- proj rty: " ^ rty_to_string ctx ty)); + failwith "Unreachable" in { V.value; V.ty } diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 315459fc..6f4e5bc5 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -160,49 +160,6 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) : false with Found -> true -(** 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 - | _ -> failwith "Unreachable" - (** Check that a symbolic value doesn't contain ended regions. Note that we don't check that the set of ended regions is empty: we |