summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-14 12:17:59 +0100
committerSon Ho2022-01-14 12:17:59 +0100
commitdfafe05012a46d58168f90fc34baa1bdd1f4b52e (patch)
tree71930f0ee36aa6957b3915496873c4728a89c124
parent8bb54af58aad7c4a09afcc13d9e7125d722d2426 (diff)
Implement give_back_symbolic_value
-rw-r--r--src/InterpreterBorrows.ml31
-rw-r--r--src/InterpreterBorrowsCore.ml47
-rw-r--r--src/InterpreterUtils.ml8
3 files changed, 26 insertions, 60 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 3391a497..c4c090e3 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -454,8 +454,9 @@ let give_back_symbolic_value (_config : C.config) (sv : V.symbolic_value)
end abstraction when ending this abstraction. When doing this, we need
to convert the [avalue] to a [value] by introducing the proper symbolic values.
*)
-let give_back_avalue (_config : C.config) (bid : V.BorrowId.id)
- (nv : V.typed_avalue) (ctx : C.eval_ctx) : C.eval_ctx =
+let give_back_avalue_to_same_abstraction (_config : C.config)
+ (bid : V.BorrowId.id) (nv : V.typed_avalue) (ctx : C.eval_ctx) : C.eval_ctx
+ =
(* We use a reference to check that we updated exactly one loan *)
let replaced : bool ref = ref false in
let set_replaced () =
@@ -490,8 +491,8 @@ let give_back_avalue (_config : C.config) (bid : V.BorrowId.id)
let _, expected_ty, _ = ty_get_ref ty in
if nv.V.ty <> expected_ty then (
log#serror
- ("give_back_avalue: improper type:\n- expected: "
- ^ rty_to_string ctx ty ^ "\n- received: "
+ ("give_back_avalue_to_same_abstraction: improper type:\n\
+ - expected: " ^ rty_to_string ctx ty ^ "\n- received: "
^ rty_to_string ctx nv.V.ty);
failwith "Value given back doesn't have the proper type");
(* This is the loan we are looking for: apply the projection to
@@ -712,7 +713,7 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
(* Check that the corresponding loan is somewhere - purely a sanity check *)
assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
(* Update the context *)
- give_back_avalue config l av ctx
+ give_back_avalue_to_same_abstraction config l av ctx
| Abstract (V.ASharedBorrow l') ->
(* Sanity check *)
assert (l' = l);
@@ -745,13 +746,7 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
a reference whose region has already ended).
*)
let convert_avalue_to_value (av : V.typed_avalue) : V.typed_value =
- (* Convert the type *)
- let ty = Subst.erase_regions av.V.ty in
- (* Generate the fresh a symbolic value *)
- let sv_id = C.fresh_symbolic_value_id () in
- let svalue : V.symbolic_value = { V.sv_id; sv_ty = av.V.ty } in
- let value = V.Symbolic svalue in
- { V.value; V.ty }
+ mk_fresh_symbolic_typed_value av.V.sv_ty
(** End a borrow identified by its borrow id in a context
@@ -1138,7 +1133,17 @@ and end_abstraction_borrows (config : C.config) (abs_id : V.AbstractionId.id)
(* Reexplore *)
end_abstraction_borrows config abs_id ctx
(* There are symbolic borrows: end them, then reexplore *)
- | FoundAProjBorrows (_sv, _proj_ty) -> raise Errors.Unimplemented
+ | FoundAProjBorrows (sv, proj_ty) ->
+ (* Replace the proj_borrows - there should be exactly one *)
+ let ctx =
+ update_intersecting_aproj_borrows_non_shared regions sv
+ V.AEndedProjBorrows ctx
+ in
+ (* Give back a fresh symbolic value *)
+ let nsv = mk_fresh_symbolic_typed_value proj_ty in
+ let ctx = give_back_symbolic_value config sv nsv ctx in
+ (* Reexplore *)
+ end_abstraction_borrows config abs_id ctx
(** Remove an abstraction from the context, as well as all its references *)
and end_abstraction_remove_from_context (_config : C.config)
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index e3789273..00d2cbb3 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -800,53 +800,6 @@ let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t)
update_intersecting_aproj_borrows can_update_shared update_shared
update_non_shared regions sv ctx
-(*
-(** Updates the proj_loans intersecting some projection.
-
- Note that in practice, when we update a proj_loans, we always update exactly
- one aproj_loans, in a specific abstraction.
-
- We make this function more general, by checking projection intersections
- (rather than simply checking the abstraction and symbolic value ids)
- for sanity checking: we check whether we need to update a loan based
- on intersection criteria, but also check at the same time that we update
- *exactly one* projector.
- *)
-let update_intersecting_aproj_loans (regions : T.RegionId.Set.t)
- (sv : V.symbolic_value) (nv : V.aproj) (ctx : C.eval_ctx) : C.eval_ctx =
- (* Small helpers for sanity checks *)
- let updated = ref false in
- let update () : V.aproj =
- assert (not !updated);
- updated := true;
- nv
- in
- (* The visitor *)
- let obj =
- object
- inherit [_] C.map_eval_ctx as super
-
- method! visit_abs _ abs = super#visit_abs (Some abs) abs
-
- method! visit_aproj abs sproj =
- match sproj with
- | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows ->
- super#visit_aproj abs sproj
- | AProjLoans sv' ->
- let abs = Option.get abs in
- if proj_loans_intersect (regions, sv) (abs.regions, sv') then
- update ()
- else super#visit_aproj (Some abs) sproj
- end
- in
- (* Apply *)
- let ctx = obj#visit_eval_ctx None ctx in
- (* Check that we updated the context at least once *)
- assert !updated;
- (* Return *)
- ctx
- *)
-
(** Substitute the proj_loans based an a symbolic id *)
let substitute_aproj_loans_with_id (sv : V.symbolic_value)
(subst : T.RegionId.Set.t -> V.aproj) (ctx : C.eval_ctx) : C.eval_ctx =
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index e431aa30..2886f642 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -58,6 +58,14 @@ let mk_fresh_symbolic_value (ty : T.rty) : V.symbolic_value =
let svalue = { V.sv_id; V.sv_ty = ty } in
svalue
+(** Create a fresh symbolic value *)
+let mk_fresh_symbolic_value (rty : T.rty) : V.symbolic_value =
+ let ty = Subst.erase_regions ty in
+ (* Generate the fresh a symbolic value *)
+ let value = mk_fresh_symbolic_value rty in
+ let value = V.Symbolic svalue in
+ { V.value; V.ty }
+
(** Create a typed value from a symbolic value. *)
let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
V.typed_value =