summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-13 10:01:50 +0100
committerSon Ho2022-01-13 10:01:50 +0100
commiteb385bfdaefc494c018ce02190b13eb08cf066a4 (patch)
tree782b53f3a357877fc39bd8c5d48067388d36d306
parent7ddb32b347c56c98d81b3584f5a53bfeff284c01 (diff)
Fix a small bug in projections_intersect and add more debugging output
Diffstat (limited to '')
-rw-r--r--TODO.md1
-rw-r--r--src/Identifiers.ml2
-rw-r--r--src/InterpreterBorrowsCore.ml52
-rw-r--r--src/InterpreterProjectors.ml25
-rw-r--r--src/InterpreterUtils.ml43
5 files changed, 75 insertions, 48 deletions
diff --git a/TODO.md b/TODO.md
index 37c18131..f7f44383 100644
--- a/TODO.md
+++ b/TODO.md
@@ -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