summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-26 10:04:52 +0100
committerSon Ho2022-01-26 10:04:52 +0100
commit14833cb33792703bf87c7e7d933687f289886294 (patch)
treeb7c18f894854372dbd318f9b5dd3b6c54696aa7e
parent144b660f7cfb8b65672f5872c05272a9caa0de78 (diff)
Add a meta-value in SharedBorrow to carry the shared value
Diffstat (limited to '')
-rw-r--r--src/InterpreterBorrows.ml4
-rw-r--r--src/InterpreterBorrowsCore.ml12
-rw-r--r--src/InterpreterExpansion.ml6
-rw-r--r--src/InterpreterExpressions.ml31
-rw-r--r--src/InterpreterPaths.ml8
-rw-r--r--src/InterpreterProjectors.ml8
-rw-r--r--src/Invariants.ml6
-rw-r--r--src/Print.ml2
-rw-r--r--src/Values.ml54
9 files changed, 78 insertions, 53 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index f87d053c..b231722d 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -89,7 +89,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
method! visit_Borrow outer bc =
match bc with
- | SharedBorrow l' | InactivatedMutBorrow l' ->
+ | SharedBorrow (_, l') | InactivatedMutBorrow l' ->
(* Check if this is the borrow we are looking for *)
if l = l' then (
(* Check if there are outer borrows or if we are inside an abstraction *)
@@ -713,7 +713,7 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
(* Update the context *)
give_back_value config l tv ctx
- | Concrete (V.SharedBorrow l' | V.InactivatedMutBorrow l') ->
+ | Concrete (V.SharedBorrow (_, l') | V.InactivatedMutBorrow l') ->
(* Sanity check *)
assert (l' = l);
(* Check that the borrow is somewhere - purely a sanity check *)
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 81f9d0d3..b4ab7706 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -194,9 +194,9 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
method! visit_borrow_content env bc =
match bc with
- | V.SharedBorrow bid ->
+ | V.SharedBorrow (mv, bid) ->
(* Nothing specific to do *)
- super#visit_SharedBorrow env bid
+ super#visit_SharedBorrow env mv bid
| V.InactivatedMutBorrow bid ->
(* Nothing specific to do *)
super#visit_InactivatedMutBorrow env bid
@@ -305,7 +305,7 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id)
method! visit_borrow_content env bc =
match bc with
- | V.SharedBorrow _ | V.InactivatedMutBorrow _ ->
+ | V.SharedBorrow (_, _) | V.InactivatedMutBorrow _ ->
(* Nothing specific to do *)
super#visit_borrow_content env bc
| V.MutBorrow (bid, mv) ->
@@ -407,7 +407,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id)
if bid = l then raise (FoundGBorrowContent (Concrete bc))
else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
else ()
- | V.SharedBorrow bid ->
+ | V.SharedBorrow (_, bid) ->
(* Check the borrow id *)
if bid = l then raise (FoundGBorrowContent (Concrete bc)) else ()
| V.InactivatedMutBorrow bid ->
@@ -490,9 +490,9 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id)
if bid = l then update ()
else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
else V.MutBorrow (bid, mv)
- | V.SharedBorrow bid ->
+ | V.SharedBorrow (mv, bid) ->
(* Check the id *)
- if bid = l then update () else super#visit_SharedBorrow env bid
+ if bid = l then update () else super#visit_SharedBorrow env mv bid
| V.InactivatedMutBorrow bid ->
(* Check the id *)
if bid = l then update ()
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 69e12545..2dd36535 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -298,6 +298,8 @@ let expand_symbolic_value_shared_borrow (config : C.config)
| _ -> failwith "Unexpected"
else None
in
+ (* The fresh symbolic value for the shared value *)
+ let shared_sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
(* Visitor to replace the projectors on borrows *)
let obj =
object (self)
@@ -306,7 +308,8 @@ let expand_symbolic_value_shared_borrow (config : C.config)
method! visit_Symbolic env sv =
if same_symbolic_id sv original_sv then
let bid = fresh_borrow () in
- V.Borrow (V.SharedBorrow bid)
+ V.Borrow
+ (V.SharedBorrow (mk_typed_value_from_symbolic_value shared_sv, bid))
else super#visit_Symbolic env sv
method! visit_Abs proj_regions abs =
@@ -362,7 +365,6 @@ let expand_symbolic_value_shared_borrow (config : C.config)
(* Finally, replace the projectors on loans *)
let bids = !borrows in
assert (not (V.BorrowId.Set.is_empty bids));
- let shared_sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
let see = V.SeSharedRef (bids, shared_sv) in
let allow_reborrows = true in
let ctx =
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 3ebce9bf..84f51c94 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -508,33 +508,34 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
(* Evaluate the borrowing operation *)
let eval (cf : V.typed_value -> m_fun) (v : V.typed_value) : m_fun =
fun ctx ->
- (* Compute the rvalue - simply a shared borrow with a fresh id *)
+ (* Generate the fresh borrow id *)
let bid = C.fresh_borrow_id () in
- (* Note that the reference is *mutable* if we do a two-phase borrow *)
- let rv_ty =
- T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut)
- in
- let bc =
- if bkind = E.Shared then V.SharedBorrow bid
- else V.InactivatedMutBorrow bid
- in
- let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in
- (* Compute the value with which to replace the value at place p *)
- let nv =
+ (* Compute the loan value, with which to replace the value at place p *)
+ let nv, shared_mvalue =
match v.V.value with
| V.Loan (V.SharedLoan (bids, sv)) ->
(* Shared loan: insert the new borrow id *)
let bids1 = V.BorrowId.Set.add bid bids in
- { v with V.value = V.Loan (V.SharedLoan (bids1, sv)) }
+ ({ v with V.value = V.Loan (V.SharedLoan (bids1, sv)) }, sv)
| _ ->
(* Not a shared loan: add a wrapper *)
let v' =
V.Loan (V.SharedLoan (V.BorrowId.Set.singleton bid, v))
in
- { v with V.value = v' }
+ ({ v with V.value = v' }, v)
in
- (* Update the value in the context *)
+ (* Update the borrowed value in the context *)
let ctx = write_place_unwrap config access p nv ctx in
+ (* Compute the rvalue - simply a shared borrow with a the fresh id.
+ * Note that the reference is *mutable* if we do a two-phase borrow *)
+ let rv_ty =
+ T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut)
+ in
+ let bc =
+ if bkind = E.Shared then V.SharedBorrow (shared_mvalue, bid)
+ else V.InactivatedMutBorrow bid
+ in
+ let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in
(* Continue *)
cf rv ctx
in
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index e45dbb3a..300e50c5 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -160,7 +160,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
(* Borrows *)
| Deref, V.Borrow bc, _ -> (
match bc with
- | V.SharedBorrow bid ->
+ | V.SharedBorrow (_, bid) ->
(* Lookup the loan content, and explore from there *)
if access.lookup_shared_borrows then
match lookup_loan ek bid ctx with
@@ -643,7 +643,7 @@ let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool)
| LoanContent (V.SharedLoan (bids, _)) ->
end_outer_borrows config bids
| LoanContent (V.MutLoan bid)
- | BorrowContent (V.MutBorrow (bid, _) | SharedBorrow bid) ->
+ | BorrowContent (V.MutBorrow (bid, _) | SharedBorrow (_, bid)) ->
end_outer_borrow config bid
| BorrowContent (V.InactivatedMutBorrow bid) ->
(* First activate the borrow *)
@@ -715,12 +715,12 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
| V.Borrow bc -> (
(* We can only copy shared borrows *)
match bc with
- | SharedBorrow bid ->
+ | SharedBorrow (mv, bid) ->
(* We need to create a new borrow id for the copied borrow, and
* update the context accordingly *)
let bid' = C.fresh_borrow_id () in
let ctx = reborrow_shared bid bid' ctx in
- (ctx, { v with V.value = V.Borrow (SharedBorrow bid') })
+ (ctx, { v with V.value = V.Borrow (SharedBorrow (mv, bid')) })
| MutBorrow (_, _) -> failwith "Can't copy a mutable borrow"
| V.InactivatedMutBorrow _ ->
failwith "Can't copy an inactivated mut borrow")
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index 946bacea..76b7d6ae 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -56,7 +56,7 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
bv ref_ty
in
(bid, asb)
- | V.SharedBorrow bid, T.Shared ->
+ | V.SharedBorrow (_, bid), T.Shared ->
(* Lookup the shared value *)
let ek = ek_all in
let sv = lookup_loan ek bid ctx in
@@ -172,7 +172,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
fresh_reborrow regions ancestors_regions bv ref_ty
in
V.AMutBorrow (mv, bid, bv)
- | V.SharedBorrow bid, T.Shared -> V.ASharedBorrow bid
+ | V.SharedBorrow (_, bid), T.Shared -> V.ASharedBorrow bid
| V.InactivatedMutBorrow _, _ ->
failwith
"Can't apply a proj_borrow over an inactivated mutable \
@@ -197,7 +197,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
in
(* Return *)
V.AIgnoredMutBorrow (opt_bid, bv)
- | V.SharedBorrow bid, T.Shared ->
+ | V.SharedBorrow (_, bid), T.Shared ->
(* Lookup the shared value *)
let ek = ek_all in
let sv = lookup_loan ek bid ctx in
@@ -370,7 +370,7 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
match v.V.value with
| V.Borrow lc -> (
match lc with
- | V.SharedBorrow _ | V.InactivatedMutBorrow _ -> None
+ | V.SharedBorrow (_, _) | V.InactivatedMutBorrow _ -> None
| V.MutBorrow (id, _) -> Some id)
| _ -> None
in
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 6ebd3375..ee58a1a3 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -242,7 +242,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
(* Register the loan *)
let _ =
match bc with
- | V.SharedBorrow bid -> register_borrow Shared bid
+ | V.SharedBorrow (_, bid) -> register_borrow Shared bid
| V.MutBorrow (bid, _) -> register_borrow Mut bid
| V.InactivatedMutBorrow bid -> register_borrow Inactivated bid
in
@@ -451,8 +451,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| V.Bottom, _ -> (* Nothing to check *) ()
| V.Borrow bc, T.Ref (_, ref_ty, rkind) -> (
match (bc, rkind) with
- | V.SharedBorrow bid, T.Shared | V.InactivatedMutBorrow bid, T.Mut
- -> (
+ | V.SharedBorrow (_, bid), T.Shared
+ | V.InactivatedMutBorrow bid, T.Mut -> (
(* Lookup the borrowed value to check it has the proper type *)
let _, glc = lookup_loan ek_all bid ctx in
match glc with
diff --git a/src/Print.ml b/src/Print.ml
index cefa3ea5..da6158b5 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -278,7 +278,7 @@ module Values = struct
and borrow_content_to_string (fmt : value_formatter) (bc : V.borrow_content) :
string =
match bc with
- | SharedBorrow bid -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋"
+ | SharedBorrow (_, bid) -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋"
| MutBorrow (bid, tv) ->
"&mut@" ^ V.BorrowId.to_string bid ^ " ("
^ typed_value_to_string fmt tv
diff --git a/src/Values.ml b/src/Values.ml
index 90250c63..57d188da 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -131,7 +131,17 @@ and adt_value = {
}
and borrow_content =
- | SharedBorrow of (BorrowId.id[@opaque]) (** A shared value *)
+ | SharedBorrow of mvalue * (BorrowId.id[@opaque])
+ (** A shared borrow.
+
+ We remember the shared value which was borrowed as a meta value.
+ This is necessary for synthesis: upon translating to "pure" values,
+ we can't perform any lookup because we don't have an environment
+ anymore. Note that it is ok to keep the shared value and copy
+ the shared value this way, because shared values are immutable
+ for as long as they are shared (i.e., as long as we can use the
+ shared borrow).
+ *)
| MutBorrow of (BorrowId.id[@opaque]) * typed_value
(** A mutably borrowed value. *)
| InactivatedMutBorrow of (BorrowId.id[@opaque])
@@ -168,12 +178,23 @@ and loan_content =
borrows, and extremely useful when giving shared values to abstractions).
*)
+and mvalue = typed_value
+(** "Meta"-value: information we store for the synthesis.
+
+ Note that we never automatically visit the meta-values with the
+ visitors: they really are meta information, and shouldn't be considered
+ as part of the environment during a symbolic execution.
+
+ TODO: we may want to create wrappers, to prevent accidently mixing meta
+ values and regular values.
+ *)
+
and typed_value = { value : value; ty : ety }
[@@deriving
show,
visitors
{
- name = "iter_typed_value";
+ name = "iter_typed_value_visit_mvalue";
variety = "iter";
ancestors = [ "iter_typed_value_base" ];
nude = true (* Don't inherit [VisitorsRuntime.iter] *);
@@ -181,7 +202,7 @@ and typed_value = { value : value; ty : ety }
},
visitors
{
- name = "map_typed_value";
+ name = "map_typed_value_visit_mvalue";
variety = "map";
ancestors = [ "map_typed_value_base" ];
nude = true (* Don't inherit [VisitorsRuntime.iter] *);
@@ -189,16 +210,21 @@ and typed_value = { value : value; ty : ety }
}]
(** "Regular" typed value (we map variables to typed values) *)
-type mvalue = typed_value [@@deriving show]
-(** "Meta"-value: information we store for the synthesis.
+(** We have to override the [visit_mvalue] method, to ignore meta-values *)
+class ['self] iter_typed_value =
+ object (_self : 'self)
+ inherit [_] iter_typed_value_visit_mvalue
- Note that we never automatically visit the meta-values with the
- visitors: they really are meta information, and shouldn't be considered
- as part of the environment during a symbolic execution.
-
- TODO: we may want to create wrappers, to prevent mixing meta values
- and regular values.
- *)
+ method! visit_mvalue : 'env -> mvalue -> unit = fun _ _ -> ()
+ end
+
+(** We have to override the [visit_mvalue] method, to ignore meta-values *)
+class ['self] map_typed_value =
+ object (_self : 'self)
+ inherit [_] map_typed_value_visit_mvalue
+
+ method! visit_mvalue : 'env -> mvalue -> mvalue = fun _ x -> x
+ end
type msymbolic_value = symbolic_value [@@deriving show]
(** "Meta"-symbolic value.
@@ -238,8 +264,6 @@ class ['self] iter_aproj_base =
method visit_rty : 'env -> rty -> unit = fun _ _ -> ()
- method visit_mvalue : 'env -> mvalue -> unit = fun _ _ -> ()
-
method visit_msymbolic_value : 'env -> msymbolic_value -> unit =
fun _ _ -> ()
end
@@ -251,8 +275,6 @@ class ['self] map_aproj_base =
method visit_rty : 'env -> rty -> rty = fun _ ty -> ty
- method visit_mvalue : 'env -> mvalue -> mvalue = fun _ v -> v
-
method visit_msymbolic_value : 'env -> msymbolic_value -> msymbolic_value =
fun _ m -> m
end