summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-11-12 20:41:58 +0100
committerSon Ho2023-11-12 20:41:58 +0100
commit746239e8f29de85f848d14e44eac8690e2065a1d (patch)
tree523b1e82385b4f41501ae98099d9f3d3a8092b63
parent6ef68fa9ffd4caec09677ee2800a778080d6da34 (diff)
Add the "V" prefix to most variants related to values
Diffstat (limited to '')
-rw-r--r--compiler/InterpreterBorrows.ml338
-rw-r--r--compiler/InterpreterBorrowsCore.ml105
-rw-r--r--compiler/InterpreterExpansion.ml29
-rw-r--r--compiler/InterpreterExpressions.ml106
-rw-r--r--compiler/InterpreterLoopsFixedPoint.ml18
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.ml76
-rw-r--r--compiler/InterpreterPaths.ml84
-rw-r--r--compiler/InterpreterProjectors.ml112
-rw-r--r--compiler/InterpreterStatements.ml38
-rw-r--r--compiler/InterpreterUtils.ml8
-rw-r--r--compiler/Invariants.ml277
-rw-r--r--compiler/Print.ml25
-rw-r--r--compiler/SymbolicToPure.ml20
-rw-r--r--compiler/Values.ml18
-rw-r--r--compiler/ValuesUtils.ml20
15 files changed, 629 insertions, 645 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index c54d55d4..566061c2 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -79,10 +79,10 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
| None -> ()
| Some c -> (
match c with
- | V.SharedLoan (bids, _) ->
+ | VSharedLoan (bids, _) ->
raise (FoundPriority (InnerLoans (Borrows bids)))
- | V.MutLoan bid -> raise (FoundPriority (InnerLoans (Borrow bid)))
- ))
+ | VMutLoan bid -> raise (FoundPriority (InnerLoans (Borrow bid))))
+ )
in
(* The environment is used to keep track of the outer loans *)
@@ -92,18 +92,18 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
(** We reimplement {!visit_Loan} because we may have to update the
outer borrows *)
- method! visit_Loan (outer : V.AbstractionId.id option * borrow_ids option)
- lc =
+ method! visit_VLoan
+ (outer : V.AbstractionId.id option * borrow_ids option) lc =
match lc with
- | V.MutLoan bid -> V.Loan (super#visit_MutLoan outer bid)
- | V.SharedLoan (bids, v) ->
+ | VMutLoan bid -> VLoan (super#visit_VMutLoan outer bid)
+ | VSharedLoan (bids, v) ->
(* Update the outer borrows before diving into the shared value *)
let outer = update_outer_borrows outer (Borrows bids) in
- V.Loan (super#visit_SharedLoan outer bids v)
+ VLoan (super#visit_VSharedLoan outer bids v)
- method! visit_Borrow outer bc =
+ method! visit_VBorrow outer bc =
match bc with
- | SharedBorrow l' | ReservedMutBorrow l' ->
+ | VSharedBorrow l' | VReservedMutBorrow 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 *)
@@ -111,9 +111,9 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
(* Register the update *)
set_replaced_bc (fst outer) (Concrete bc);
(* Update the value *)
- V.Bottom)
- else super#visit_Borrow outer bc
- | V.MutBorrow (l', bv) ->
+ VBottom)
+ else super#visit_VBorrow outer bc
+ | VMutBorrow (l', bv) ->
(* 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 *)
@@ -121,11 +121,11 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
(* Register the update *)
set_replaced_bc (fst outer) (Concrete bc);
(* Update the value *)
- V.Bottom)
+ VBottom)
else
(* Update the outer borrows before diving into the borrowed value *)
let outer = update_outer_borrows outer (Borrow l') in
- V.Borrow (super#visit_MutBorrow outer l' bv)
+ VBorrow (super#visit_VMutBorrow outer l' bv)
(** We reimplement {!visit_ALoan} because we may have to update the
outer borrows *)
@@ -136,31 +136,31 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
* need it to properly instantiate the backward functions when generating
* the pure translation. *)
match lc with
- | V.AMutLoan (_, _) ->
+ | AMutLoan (_, _) ->
(* Nothing special to do *)
super#visit_ALoan outer lc
- | V.ASharedLoan (bids, v, av) ->
+ | ASharedLoan (bids, v, av) ->
(* Explore the shared value - we need to update the outer borrows *)
let souter = update_outer_borrows outer (Borrows bids) in
let v = super#visit_typed_value souter v in
(* Explore the child avalue - we keep the same outer borrows *)
let av = super#visit_typed_avalue outer av in
(* Reconstruct *)
- V.ALoan (V.ASharedLoan (bids, v, av))
- | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
- | V.AEndedSharedLoan _
+ ALoan (ASharedLoan (bids, v, av))
+ | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+ | AEndedSharedLoan _
(* The loan has ended, so no need to update the outer borrows *)
- | V.AIgnoredMutLoan _ (* Nothing special to do *)
- | V.AEndedIgnoredMutLoan
+ | AIgnoredMutLoan _ (* Nothing special to do *)
+ | AEndedIgnoredMutLoan
{ given_back = _; child = _; given_back_meta = _ }
(* Nothing special to do *)
- | V.AIgnoredSharedLoan _ ->
+ | AIgnoredSharedLoan _ ->
(* Nothing special to do *)
super#visit_ALoan outer lc
method! visit_ABorrow outer bc =
match bc with
- | V.AMutBorrow (bid, _) ->
+ | AMutBorrow (bid, _) ->
(* Check if this is the borrow we are looking for *)
if bid = l then (
(* TODO: treat this case differently. We should not introduce
@@ -184,12 +184,12 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
* abstraction (and not really giving the value back to the context)
* we do not insert {!AEndedMutBorrow} but rather {!ABottom} *)
raise (Failure "Unimplemented")
- (* V.ABottom *))
+ (* ABottom *))
else
(* Update the outer borrows before diving into the child avalue *)
let outer = update_outer_borrows outer (Borrow bid) in
super#visit_ABorrow outer bc
- | V.ASharedBorrow bid ->
+ | ASharedBorrow bid ->
(* Check if this is the borrow we are looking for *)
if bid = l then (
(* Check there are outer borrows, or if we need to end the whole
@@ -199,16 +199,16 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
set_replaced_bc (fst outer) (Abstract bc);
(* Update the value - note that we are necessarily in the second
* of the two cases described above *)
- V.ABottom)
+ ABottom)
else super#visit_ABorrow outer bc
- | V.AIgnoredMutBorrow (_, _)
- | V.AEndedMutBorrow _
- | V.AEndedIgnoredMutBorrow
+ | AIgnoredMutBorrow (_, _)
+ | AEndedMutBorrow _
+ | AEndedIgnoredMutBorrow
{ given_back = _; child = _; given_back_meta = _ }
- | V.AEndedSharedBorrow ->
+ | AEndedSharedBorrow ->
(* Nothing special to do *)
super#visit_ABorrow outer bc
- | V.AProjSharedBorrow asb ->
+ | AProjSharedBorrow asb ->
(* Check if the borrow we are looking for is in the asb *)
if borrow_in_asb l asb then (
(* Check there are outer borrows, or if we need to end the whole
@@ -219,7 +219,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
(* Update the value - note that we are necessarily in the second
* of the two cases described above *)
let asb = remove_borrow_from_asb l asb in
- V.ABorrow (V.AProjSharedBorrow asb))
+ ABorrow (AProjSharedBorrow asb))
else (* Nothing special to do *)
super#visit_ABorrow outer bc
@@ -282,32 +282,32 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
overriding {!visit_ALoan} *)
method! visit_typed_value opt_abs (v : V.typed_value) : V.typed_value =
match v.V.value with
- | V.Loan lc ->
+ | VLoan lc ->
let value = self#visit_typed_Loan opt_abs v.V.ty lc in
({ v with V.value } : V.typed_value)
| _ -> super#visit_typed_value opt_abs v
method visit_typed_Loan opt_abs ty lc =
match lc with
- | V.SharedLoan (bids, v) ->
+ | VSharedLoan (bids, v) ->
(* We are giving back a value (i.e., the content of a *mutable*
* borrow): nothing special to do *)
- V.Loan (super#visit_SharedLoan opt_abs bids v)
- | V.MutLoan bid' ->
+ VLoan (super#visit_VSharedLoan opt_abs bids v)
+ | VMutLoan bid' ->
(* Check if this is the loan we are looking for *)
if bid' = bid then (
(* Sanity check *)
let expected_ty = ty in
- if nv.V.ty <> expected_ty then (
+ if nv.ty <> expected_ty then (
log#serror
("give_back_value: improper type:\n- expected: "
^ PA.ty_to_string ctx ty ^ "\n- received: "
- ^ PA.ty_to_string ctx nv.V.ty);
+ ^ PA.ty_to_string ctx nv.ty);
raise (Failure "Value given back doesn't have the proper type"));
(* Replace *)
set_replaced ();
- nv.V.value)
- else V.Loan (super#visit_MutLoan opt_abs bid')
+ nv.value)
+ else VLoan (super#visit_VMutLoan opt_abs bid')
(** This is a bit annoying, but as we need the type of the avalue we
are exploring, in order to be able to project the value we give
@@ -333,7 +333,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
* it is necessarily because we ended a parent abstraction,
* and the given back value is thus a symbolic value *)
match nv.V.value with
- | V.Symbolic sv ->
+ | VSymbolic sv ->
let abs = Option.get opt_abs in
(* Remember the given back value as a meta-value
* TODO: it is a bit annoying to have to deconstruct
@@ -374,7 +374,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
ty
in
match lc with
- | V.AMutLoan (bid', child) ->
+ | AMutLoan (bid', child) ->
if bid' = bid then (
(* This is the loan we are looking for: apply the projection to
* the value we give back and replaced this mutable loan with
@@ -391,17 +391,17 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
(* Continue giving back in the child value *)
let child = super#visit_typed_avalue opt_abs child in
(* Return the new value *)
- V.ALoan (V.AEndedMutLoan { child; given_back; given_back_meta }))
+ ALoan (AEndedMutLoan { child; given_back; given_back_meta }))
else (* Continue exploring *)
super#visit_ALoan opt_abs lc
- | V.ASharedLoan (_, _, _) ->
+ | ASharedLoan (_, _, _) ->
(* We are giving back a value to a *mutable* loan: nothing special to do *)
super#visit_ALoan opt_abs lc
- | V.AEndedMutLoan { child = _; given_back = _; given_back_meta = _ }
- | V.AEndedSharedLoan (_, _) ->
+ | AEndedMutLoan { child = _; given_back = _; given_back_meta = _ }
+ | AEndedSharedLoan (_, _) ->
(* Nothing special to do *)
super#visit_ALoan opt_abs lc
- | V.AIgnoredMutLoan (opt_bid, child) ->
+ | AIgnoredMutLoan (opt_bid, child) ->
(* This loan is ignored, but we may have to project on a subvalue
* of the value which is given back *)
if opt_bid = Some bid then
@@ -417,12 +417,12 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
in
(* Continue giving back in the child value *)
let child = super#visit_typed_avalue opt_abs child in
- V.ALoan
- (V.AEndedIgnoredMutLoan { given_back; child; given_back_meta })
+ ALoan
+ (AEndedIgnoredMutLoan { given_back; child; given_back_meta })
else super#visit_ALoan opt_abs lc
- | V.AEndedIgnoredMutLoan
+ | AEndedIgnoredMutLoan
{ given_back = _; child = _; given_back_meta = _ }
- | V.AIgnoredSharedLoan _ ->
+ | AIgnoredSharedLoan _ ->
(* Nothing special to do *)
super#visit_ALoan opt_abs lc
@@ -624,9 +624,9 @@ let give_back_shared _config (bid : V.BorrowId.id) (ctx : C.eval_ctx) :
object
inherit [_] C.map_eval_ctx as super
- method! visit_Loan opt_abs lc =
+ method! visit_VLoan opt_abs lc =
match lc with
- | V.SharedLoan (bids, shared_value) ->
+ | VSharedLoan (bids, shared_value) ->
if V.BorrowId.Set.mem bid bids then (
(* This is the loan we are looking for *)
set_replaced ();
@@ -635,21 +635,21 @@ let give_back_shared _config (bid : V.BorrowId.id) (ctx : C.eval_ctx) :
* loan identifier *)
if V.BorrowId.Set.cardinal bids = 1 then shared_value.V.value
else
- V.Loan
- (V.SharedLoan (V.BorrowId.Set.remove bid bids, shared_value)))
+ VLoan
+ (VSharedLoan (V.BorrowId.Set.remove bid bids, shared_value)))
else
(* Not the loan we are looking for: continue exploring *)
- V.Loan (super#visit_SharedLoan opt_abs bids shared_value)
- | V.MutLoan bid' ->
+ VLoan (super#visit_VSharedLoan opt_abs bids shared_value)
+ | VMutLoan bid' ->
(* We are giving back a *shared* borrow: nothing special to do *)
- V.Loan (super#visit_MutLoan opt_abs bid')
+ VLoan (super#visit_VMutLoan opt_abs bid')
method! visit_ALoan opt_abs lc =
match lc with
- | V.AMutLoan (bid, av) ->
+ | AMutLoan (bid, av) ->
(* Nothing special to do (we are giving back a *shared* borrow) *)
- V.ALoan (super#visit_AMutLoan opt_abs bid av)
- | V.ASharedLoan (bids, shared_value, child) ->
+ ALoan (super#visit_AMutLoan opt_abs bid av)
+ | ASharedLoan (bids, shared_value, child) ->
if V.BorrowId.Set.mem bid bids then (
(* This is the loan we are looking for *)
set_replaced ();
@@ -657,24 +657,24 @@ let give_back_shared _config (bid : V.BorrowId.id) (ctx : C.eval_ctx) :
* to end the loan. Otherwise, we just remove the current
* loan identifier *)
if V.BorrowId.Set.cardinal bids = 1 then
- V.ALoan (V.AEndedSharedLoan (shared_value, child))
+ ALoan (AEndedSharedLoan (shared_value, child))
else
- V.ALoan
- (V.ASharedLoan
+ ALoan
+ (ASharedLoan
(V.BorrowId.Set.remove bid bids, shared_value, child)))
else
(* Not the loan we are looking for: continue exploring *)
super#visit_ALoan opt_abs lc
- | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+ | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
(* Nothing special to do (the loan has ended) *)
- | V.AEndedSharedLoan (_, _)
+ | AEndedSharedLoan (_, _)
(* Nothing special to do (the loan has ended) *)
- | V.AIgnoredMutLoan (_, _)
+ | AIgnoredMutLoan (_, _)
(* Nothing special to do (we are giving back a *shared* borrow) *)
- | V.AEndedIgnoredMutLoan
+ | AEndedIgnoredMutLoan
{ given_back = _; child = _; given_back_meta = _ }
(* Nothing special to do *)
- | V.AIgnoredSharedLoan _ ->
+ | AIgnoredSharedLoan _ ->
(* Nothing special to do *)
super#visit_ALoan opt_abs lc
end
@@ -705,15 +705,15 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id)
object
inherit [_] C.map_env as super
- method! visit_SharedLoan env bids sv =
+ method! visit_VSharedLoan env bids sv =
(* Shared loan: check if the borrow id we are looking for is in the
set of borrow ids. If yes, insert the new borrow id, otherwise
explore inside the shared value *)
if V.BorrowId.Set.mem original_bid bids then (
set_ref ();
let bids' = V.BorrowId.Set.add new_bid bids in
- V.SharedLoan (bids', sv))
- else super#visit_SharedLoan env bids sv
+ VSharedLoan (bids', sv))
+ else super#visit_VSharedLoan env bids sv
method! visit_ASharedLoan env bids v av =
(* This case is similar to the {!SharedLoan} case *)
@@ -794,7 +794,7 @@ let give_back (config : C.config) (abs_id_opt : V.AbstractionId.id option)
{ enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
in
match bc with
- | Concrete (V.MutBorrow (l', tv)) ->
+ | Concrete (VMutBorrow (l', tv)) ->
(* Sanity check *)
assert (l' = l);
assert (not (loans_in_value tv));
@@ -802,14 +802,14 @@ let give_back (config : C.config) (abs_id_opt : V.AbstractionId.id option)
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.ReservedMutBorrow l') ->
+ | Concrete (VSharedBorrow l' | VReservedMutBorrow l') ->
(* Sanity check *)
assert (l' = l);
(* Check that the borrow is somewhere - purely a sanity check *)
assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
(* Update the context *)
give_back_shared config l ctx
- | Abstract (V.AMutBorrow (l', av)) ->
+ | Abstract (AMutBorrow (l', av)) ->
(* Sanity check *)
assert (l' = l);
(* Check that the corresponding loan is somewhere - purely a sanity check *)
@@ -826,21 +826,21 @@ let give_back (config : C.config) (abs_id_opt : V.AbstractionId.id option)
give_back_avalue_to_same_abstraction config l av
(mk_typed_value_from_symbolic_value sv)
ctx
- | Abstract (V.ASharedBorrow l') ->
+ | Abstract (ASharedBorrow l') ->
(* Sanity check *)
assert (l' = l);
(* Check that the borrow is somewhere - purely a sanity check *)
assert (Option.is_some (lookup_loan_opt sanity_ek l ctx));
(* Update the context *)
give_back_shared config l ctx
- | Abstract (V.AProjSharedBorrow asb) ->
+ | Abstract (AProjSharedBorrow asb) ->
(* Sanity check *)
assert (borrow_in_asb l asb);
(* Update the context *)
give_back_shared config l ctx
| Abstract
- ( V.AEndedMutBorrow _ | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _
- | V.AEndedSharedBorrow ) ->
+ ( AEndedMutBorrow _ | AIgnoredMutBorrow _ | AEndedIgnoredMutBorrow _
+ | AEndedSharedBorrow ) ->
raise (Failure "Unreachable")
let check_borrow_disappeared (fun_name : string) (l : V.BorrowId.id)
@@ -970,7 +970,7 @@ let rec end_borrow_aux (config : C.config) (chain : borrow_or_abs_ids)
| Ok (ctx, Some (abs_id_opt, bc)) ->
(* Sanity check: the borrowed value shouldn't contain loans *)
(match bc with
- | Concrete (V.MutBorrow (_, bv)) ->
+ | Concrete (VMutBorrow (_, bv)) ->
assert (Option.is_none (get_first_loan_in_value bv))
| _ -> ());
(* Give back the value *)
@@ -1182,8 +1182,8 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
(** We may need to end borrows in "regular" values, because of shared values *)
method! visit_borrow_content _ bc =
match bc with
- | V.SharedBorrow _ | V.MutBorrow (_, _) -> raise (FoundBorrowContent bc)
- | V.ReservedMutBorrow _ -> raise (Failure "Unreachable")
+ | VSharedBorrow _ | VMutBorrow (_, _) -> raise (FoundBorrowContent bc)
+ | VReservedMutBorrow _ -> raise (Failure "Unreachable")
end
in
(* Lookup the abstraction *)
@@ -1272,7 +1272,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
^ borrow_content_to_string ctx bc));
let ctx =
match bc with
- | V.SharedBorrow bid -> (
+ | VSharedBorrow bid -> (
(* Replace the shared borrow with bottom *)
let allow_inner_loans = false in
match
@@ -1282,7 +1282,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
| Ok (ctx, _) ->
(* Give back *)
give_back_shared config bid ctx)
- | V.MutBorrow (bid, v) -> (
+ | VMutBorrow (bid, v) -> (
(* Replace the mut borrow with bottom *)
let allow_inner_loans = false in
match
@@ -1293,7 +1293,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
(* Give the value back - note that the mut borrow was below a
* shared borrow: the value is thus unchanged *)
give_back_value config bid v ctx)
- | V.ReservedMutBorrow _ -> raise (Failure "Unreachable")
+ | VReservedMutBorrow _ -> raise (Failure "Unreachable")
in
(* Reexplore *)
end_abstraction_borrows config chain abs_id cf ctx
@@ -1501,9 +1501,9 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id)
{ enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
in
match lookup_loan ek l ctx with
- | _, Concrete (V.MutLoan _) ->
+ | _, Concrete (VMutLoan _) ->
raise (Failure "Expected a shared loan, found a mut loan")
- | _, Concrete (V.SharedLoan (bids, sv)) ->
+ | _, Concrete (VSharedLoan (bids, sv)) ->
(* Check that there is only one borrow id (l) and update the loan *)
assert (V.BorrowId.Set.mem l bids && V.BorrowId.Set.cardinal bids = 1);
(* We need to check that there aren't any loans in the value:
@@ -1515,7 +1515,7 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id)
(* Check there aren't reserved borrows *)
assert (not (reserved_in_value sv));
(* Update the loan content *)
- let ctx = update_loan ek l (V.MutLoan l) ctx in
+ let ctx = update_loan ek l (VMutLoan l) ctx in
(* Continue *)
cf sv ctx
| _, Abstract _ ->
@@ -1542,11 +1542,11 @@ let replace_reserved_borrow_with_mut_borrow (l : V.BorrowId.id) (cf : m_fun)
in
let ctx =
match lookup_borrow ek l ctx with
- | Concrete (V.SharedBorrow _ | V.MutBorrow (_, _)) ->
+ | Concrete (VSharedBorrow _ | VMutBorrow (_, _)) ->
raise (Failure "Expected a reserved mutable borrow")
- | Concrete (V.ReservedMutBorrow _) ->
+ | Concrete (VReservedMutBorrow _) ->
(* Update it *)
- update_borrow ek l (V.MutBorrow (l, borrowed_value)) ctx
+ update_borrow ek l (VMutBorrow (l, borrowed_value)) ctx
| Abstract _ ->
(* This can't happen for sure *)
raise
@@ -1566,8 +1566,8 @@ let rec promote_reserved_mut_borrow (config : C.config) (l : V.BorrowId.id) :
{ enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
in
match lookup_loan ek l ctx with
- | _, Concrete (V.MutLoan _) -> raise (Failure "Unreachable")
- | _, Concrete (V.SharedLoan (bids, sv)) -> (
+ | _, Concrete (VMutLoan _) -> raise (Failure "Unreachable")
+ | _, Concrete (VSharedLoan (bids, sv)) -> (
(* If there are loans inside the value, end them. Note that there can't be
reserved borrows inside the value.
If we perform an update, do a recursive call to lookup the updated value *)
@@ -1576,8 +1576,8 @@ let rec promote_reserved_mut_borrow (config : C.config) (l : V.BorrowId.id) :
(* End the loans *)
let cc =
match lc with
- | V.SharedLoan (bids, _) -> end_borrows config bids
- | V.MutLoan bid -> end_borrow config bid
+ | VSharedLoan (bids, _) -> end_borrows config bids
+ | VMutLoan bid -> end_borrow config bid
in
(* Recursive call *)
let cc = comp cc (promote_reserved_mut_borrow config l) in
@@ -1637,8 +1637,8 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
(* Function to explore an avalue and destructure it *)
let rec list_avalues (allow_borrows : bool) (push : V.typed_avalue -> unit)
(av : V.typed_avalue) : unit =
- let ty = av.V.ty in
- match av.V.value with
+ let ty = av.ty in
+ match av.value with
| ABottom | AIgnored -> ()
| AAdt adt ->
(* Simply explore the children *)
@@ -1646,17 +1646,17 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
| ALoan lc -> (
(* Explore the loan content *)
match lc with
- | V.ASharedLoan (bids, sv, child_av) ->
+ | ASharedLoan (bids, sv, child_av) ->
(* We don't support nested borrows for now *)
- assert (not (value_has_borrows ctx sv.V.value));
+ assert (not (value_has_borrows ctx sv.value));
(* Destructure the shared value *)
let avl, sv =
if destructure_shared_values then list_values sv else ([], sv)
in
(* Push a value *)
- let ignored = mk_aignored child_av.V.ty in
- let value = V.ALoan (V.ASharedLoan (bids, sv, ignored)) in
- push { V.value; ty };
+ let ignored = mk_aignored child_av.ty in
+ let value = V.ALoan (ASharedLoan (bids, sv, ignored)) in
+ push { value; ty };
(* Explore the child *)
list_avalues false push_fail child_av;
(* Push the avalues introduced because we decomposed the inner loans -
@@ -1666,25 +1666,25 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
exactly the same way as [list_avalues] (i.e., with a similar
signature) *)
List.iter push avl
- | V.AMutLoan (bid, child_av) ->
+ | AMutLoan (bid, child_av) ->
(* Explore the child *)
list_avalues false push_fail child_av;
(* Explore the whole loan *)
- let ignored = mk_aignored child_av.V.ty in
- let value = V.ALoan (V.AMutLoan (bid, ignored)) in
- push { V.value; ty }
- | V.AIgnoredMutLoan (opt_bid, child_av) ->
+ let ignored = mk_aignored child_av.ty in
+ let value = V.ALoan (AMutLoan (bid, ignored)) in
+ push { value; ty }
+ | AIgnoredMutLoan (opt_bid, child_av) ->
(* We don't support nested borrows for now *)
assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
assert (opt_bid = None);
(* Simply explore the child *)
list_avalues false push_fail child_av
- | V.AEndedMutLoan
+ | AEndedMutLoan
{ child = child_av; given_back = _; given_back_meta = _ }
- | V.AEndedSharedLoan (_, child_av)
- | V.AEndedIgnoredMutLoan
+ | AEndedSharedLoan (_, child_av)
+ | AEndedIgnoredMutLoan
{ child = child_av; given_back = _; given_back_meta = _ }
- | V.AIgnoredSharedLoan child_av ->
+ | AIgnoredSharedLoan child_av ->
(* We don't support nested borrows for now *)
assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
(* Simply explore the child *)
@@ -1694,34 +1694,34 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
assert allow_borrows;
(* Explore the borrow content *)
match bc with
- | V.AMutBorrow (bid, child_av) ->
+ | AMutBorrow (bid, child_av) ->
(* Explore the child *)
list_avalues false push_fail child_av;
(* Explore the borrow *)
- let ignored = mk_aignored child_av.V.ty in
- let value = V.ABorrow (V.AMutBorrow (bid, ignored)) in
- push { V.value; ty }
- | V.ASharedBorrow _ ->
+ let ignored = mk_aignored child_av.ty in
+ let value = V.ABorrow (AMutBorrow (bid, ignored)) in
+ push { value; ty }
+ | ASharedBorrow _ ->
(* Nothing specific to do: keep the value as it is *)
push av
- | V.AIgnoredMutBorrow (opt_bid, child_av) ->
+ | AIgnoredMutBorrow (opt_bid, child_av) ->
(* We don't support nested borrows for now *)
assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
assert (opt_bid = None);
(* Just explore the child *)
list_avalues false push_fail child_av
- | V.AEndedIgnoredMutBorrow
+ | AEndedIgnoredMutBorrow
{ child = child_av; given_back = _; given_back_meta = _ } ->
(* We don't support nested borrows for now *)
assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
(* Just explore the child *)
list_avalues false push_fail child_av
- | V.AProjSharedBorrow asb ->
+ | AProjSharedBorrow asb ->
(* We don't support nested borrows *)
assert (asb = []);
(* Nothing specific to do *)
()
- | V.AEndedMutBorrow _ | V.AEndedSharedBorrow ->
+ | AEndedMutBorrow _ | AEndedSharedBorrow ->
(* If we get there it means the abstraction ended: it should not
be in the context anymore (if we end *one* borrow in an abstraction,
we have to end them all and remove the abstraction from the context)
@@ -1732,29 +1732,29 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
expanded *)
assert (not (ty_has_borrows ctx.type_context.type_infos ty))
and list_values (v : V.typed_value) : V.typed_avalue list * V.typed_value =
- let ty = v.V.ty in
- match v.V.value with
+ let ty = v.ty in
+ match v.value with
| VLiteral _ -> ([], v)
| VAdt adt ->
let avll, field_values =
List.split (List.map list_values adt.field_values)
in
let avl = List.concat avll in
- let adt = { adt with V.field_values } in
- (avl, { v with V.value = VAdt adt })
- | Bottom -> raise (Failure "Unreachable")
- | Borrow _ ->
+ let adt = { adt with field_values } in
+ (avl, { v with value = VAdt adt })
+ | VBottom -> raise (Failure "Unreachable")
+ | VBorrow _ ->
(* We don't support nested borrows for now *)
raise (Failure "Unreachable")
- | Loan lc -> (
+ | VLoan lc -> (
match lc with
- | SharedLoan (bids, sv) ->
+ | VSharedLoan (bids, sv) ->
let avl, sv = list_values sv in
if destructure_shared_values then (
(* Rem.: the shared value can't contain loans nor borrows *)
assert (ty_no_regions ty);
let av : V.typed_avalue =
- assert (not (value_has_loans_or_borrows ctx sv.V.value));
+ assert (not (value_has_loans_or_borrows ctx sv.value));
(* We introduce fresh ids for the symbolic values *)
let mk_value_with_fresh_sids (v : V.typed_value) : V.typed_value
=
@@ -1770,16 +1770,14 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
in
let sv = mk_value_with_fresh_sids sv in
(* Create the new avalue *)
- let value =
- V.ALoan (V.ASharedLoan (bids, sv, mk_aignored ty))
- in
- { V.value; ty }
+ let value = V.ALoan (ASharedLoan (bids, sv, mk_aignored ty)) in
+ { value; ty }
in
let avl = List.append [ av ] avl in
(avl, sv))
- else (avl, { v with V.value = V.Loan (V.SharedLoan (bids, sv)) })
- | MutLoan _ -> raise (Failure "Unreachable"))
- | Symbolic _ ->
+ else (avl, { v with value = VLoan (VSharedLoan (bids, sv)) })
+ | VMutLoan _ -> raise (Failure "Unreachable"))
+ | VSymbolic _ ->
(* For now, we fore all symbolic values containing borrows to be eagerly
expanded *)
assert (not (ty_has_borrows ctx.type_context.type_infos ty));
@@ -1787,10 +1785,10 @@ let destructure_abs (abs_kind : V.abs_kind) (can_end : bool)
in
(* Destructure the avalues *)
- List.iter (list_avalues true push_avalue) abs0.V.avalues;
+ List.iter (list_avalues true push_avalue) abs0.avalues;
let avalues = !avalues in
(* Update *)
- { abs0 with V.avalues; kind = abs_kind; can_end }
+ { abs0 with avalues; kind = abs_kind; can_end }
let abs_is_destructured (destructure_shared_values : bool) (ctx : C.eval_ctx)
(abs : V.abs) : bool =
@@ -1840,14 +1838,14 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
("convert_value_to_abstractions: to_avalues:\n- value: "
^ typed_value_to_string ctx v));
- let ty = v.V.ty in
- match v.V.value with
- | V.VLiteral _ -> ([], v)
- | V.Bottom ->
+ let ty = v.ty in
+ match v.value with
+ | VLiteral _ -> ([], v)
+ | VBottom ->
(* Can happen: we *do* convert dummy values to abstractions, and dummy
values can contain bottoms *)
([], v)
- | V.VAdt adt ->
+ | VAdt adt ->
(* Two cases, depending on whether we have to group all the borrows/loans
inside one abstraction or not *)
let avl, field_values =
@@ -1879,72 +1877,72 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
([], field_values)
in
let adt = { adt with field_values } in
- (avl, { v with V.value = V.VAdt adt })
- | V.Borrow bc -> (
+ (avl, { v with value = VAdt adt })
+ | VBorrow bc -> (
let _, ref_ty, kind = ty_as_ref ty in
assert (ty_no_regions ref_ty);
(* Sanity check *)
assert allow_borrows;
(* Convert the borrow content *)
match bc with
- | SharedBorrow bid ->
+ | VSharedBorrow bid ->
assert (ty_no_regions ref_ty);
- let ty = T.TRef (T.RVar r_id, ref_ty, kind) in
- let value = V.ABorrow (V.ASharedBorrow bid) in
+ let ty = T.TRef (RVar r_id, ref_ty, kind) in
+ let value = V.ABorrow (ASharedBorrow bid) in
([ { V.value; ty } ], v)
- | MutBorrow (bid, bv) ->
+ | VMutBorrow (bid, bv) ->
let r_id = if group then r_id else C.fresh_region_id () in
(* We don't support nested borrows for now *)
- assert (not (value_has_borrows ctx bv.V.value));
+ assert (not (value_has_borrows ctx bv.value));
(* Create an avalue to push - note that we use [AIgnore] for the inner avalue *)
- let ty = T.TRef (T.RVar r_id, ref_ty, kind) in
+ let ty = T.TRef (RVar r_id, ref_ty, kind) in
let ignored = mk_aignored ref_ty in
- let av = V.ABorrow (V.AMutBorrow (bid, ignored)) in
+ let av = V.ABorrow (AMutBorrow (bid, ignored)) in
let av = { V.value = av; ty } in
(* Continue exploring, looking for loans (and forbidding borrows,
because we don't support nested borrows for now) *)
let avl, bv = to_avalues false true true r_id bv in
- let value = { v with V.value = V.Borrow (V.MutBorrow (bid, bv)) } in
+ let value = { v with value = VBorrow (VMutBorrow (bid, bv)) } in
(av :: avl, value)
- | ReservedMutBorrow _ ->
+ | VReservedMutBorrow _ ->
(* This borrow should have been activated *)
raise (Failure "Unexpected"))
- | V.Loan lc -> (
+ | VLoan lc -> (
match lc with
- | V.SharedLoan (bids, sv) ->
+ | VSharedLoan (bids, sv) ->
let r_id = if group then r_id else C.fresh_region_id () in
(* We don't support nested borrows for now *)
- assert (not (value_has_borrows ctx sv.V.value));
+ assert (not (value_has_borrows ctx sv.value));
(* Push the avalue - note that we use [AIgnore] for the inner avalue *)
(* For avalues, a loan has the borrow type *)
assert (ty_no_regions ty);
- let ty = mk_ref_ty (T.RVar r_id) ty T.Shared in
+ let ty = mk_ref_ty (RVar r_id) ty Shared in
let ignored = mk_aignored ty in
(* Rem.: the shared value might contain loans *)
let avl, sv = to_avalues false true true r_id sv in
- let av = V.ALoan (V.ASharedLoan (bids, sv, ignored)) in
+ let av = V.ALoan (ASharedLoan (bids, sv, ignored)) in
let av = { V.value = av; ty } in
(* Continue exploring, looking for loans (and forbidding borrows,
because we don't support nested borrows for now) *)
let value : V.value =
- if destructure_shared_values then sv.V.value
- else V.Loan (V.SharedLoan (bids, sv))
+ if destructure_shared_values then sv.value
+ else VLoan (VSharedLoan (bids, sv))
in
- let value = { v with V.value } in
+ let value = { v with value } in
(av :: avl, value)
- | V.MutLoan bid ->
+ | VMutLoan bid ->
(* Push the avalue - note that we use [AIgnore] for the inner avalue *)
(* For avalues, a loan has the borrow type *)
assert (ty_no_regions ty);
- let ty = mk_ref_ty (T.RVar r_id) ty T.Mut in
+ let ty = mk_ref_ty (RVar r_id) ty Mut in
let ignored = mk_aignored ty in
- let av = V.ALoan (V.AMutLoan (bid, ignored)) in
+ let av = V.ALoan (AMutLoan (bid, ignored)) in
let av = { V.value = av; ty } in
([ av ], v))
- | V.Symbolic _ ->
+ | VSymbolic _ ->
(* For now, we force all the symbolic values containing borrows to
be eagerly expanded, and we don't support nested borrows *)
- assert (not (value_has_borrows ctx v.V.value));
+ assert (not (value_has_borrows ctx v.value));
(* Return nothing *)
([], v)
in
@@ -2043,8 +2041,8 @@ let compute_merge_abstraction_info (ctx : C.eval_ctx) (abs : V.abs) :
| Abstract _ -> raise (Failure "Unreachable")
in
(match lc with
- | SharedLoan (bids, _) -> push_loans bids (Concrete (ty, lc))
- | MutLoan _ -> raise (Failure "Unreachable"));
+ | VSharedLoan (bids, _) -> push_loans bids (Concrete (ty, lc))
+ | VMutLoan _ -> raise (Failure "Unreachable"));
(* Continue *)
super#visit_loan_content env lc
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 8807f3ef..cde39e9b 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -222,15 +222,15 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
method! visit_borrow_content env bc =
match bc with
- | V.SharedBorrow bid ->
+ | V.VSharedBorrow bid ->
(* Nothing specific to do *)
- super#visit_SharedBorrow env bid
- | V.ReservedMutBorrow bid ->
+ super#visit_VSharedBorrow env bid
+ | V.VReservedMutBorrow bid ->
(* Nothing specific to do *)
- super#visit_ReservedMutBorrow env bid
- | V.MutBorrow (bid, mv) ->
+ super#visit_VReservedMutBorrow env bid
+ | V.VMutBorrow (bid, mv) ->
(* Control the dive *)
- if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
+ if ek.enter_mut_borrows then super#visit_VMutBorrow env bid mv
else ()
(** We reimplement {!visit_Loan} (rather than the more precise functions
@@ -240,17 +240,17 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
*)
method! visit_loan_content env lc =
match lc with
- | V.SharedLoan (bids, sv) ->
+ | V.VSharedLoan (bids, sv) ->
(* Check if this is the loan we are looking for, and control the dive *)
if V.BorrowId.Set.mem l bids then
raise (FoundGLoanContent (Concrete lc))
else if ek.enter_shared_loans then
- super#visit_SharedLoan env bids sv
+ super#visit_VSharedLoan env bids sv
else ()
- | V.MutLoan bid ->
+ | V.VMutLoan bid ->
(* Check if this is the loan we are looking for *)
if bid = l then raise (FoundGLoanContent (Concrete lc))
- else super#visit_MutLoan env bid
+ else super#visit_VMutLoan env bid
(** Note that we don't control diving inside the abstractions: if we
allow to dive inside abstractions, we allow to go anywhere
@@ -335,28 +335,28 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id)
method! visit_borrow_content env bc =
match bc with
- | V.SharedBorrow _ | V.ReservedMutBorrow _ ->
+ | VSharedBorrow _ | VReservedMutBorrow _ ->
(* Nothing specific to do *)
super#visit_borrow_content env bc
- | V.MutBorrow (bid, mv) ->
+ | VMutBorrow (bid, mv) ->
(* Control the dive into mutable borrows *)
- if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
- else V.MutBorrow (bid, mv)
+ if ek.enter_mut_borrows then super#visit_VMutBorrow env bid mv
+ else VMutBorrow (bid, mv)
(** We reimplement {!visit_loan_content} (rather than one of the sub-
functions) on purpose: exhaustive matches are good for maintenance *)
method! visit_loan_content env lc =
match lc with
- | V.SharedLoan (bids, sv) ->
+ | VSharedLoan (bids, sv) ->
(* Shared loan: check if this is the loan we are looking for, and
control the dive. *)
if V.BorrowId.Set.mem l bids then update ()
else if ek.enter_shared_loans then
- super#visit_SharedLoan env bids sv
- else V.SharedLoan (bids, sv)
- | V.MutLoan bid ->
+ super#visit_VSharedLoan env bids sv
+ else VSharedLoan (bids, sv)
+ | VMutLoan bid ->
(* Mut loan: checks if this is the loan we are looking for *)
- if bid = l then update () else super#visit_MutLoan env bid
+ if bid = l then update () else super#visit_VMutLoan env bid
(** Note that once inside the abstractions, we don't control diving
(there are no use cases requiring finer control).
@@ -432,42 +432,42 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id)
method! visit_borrow_content env bc =
match bc with
- | V.MutBorrow (bid, mv) ->
+ | VMutBorrow (bid, mv) ->
(* Check the borrow id and control the dive *)
if bid = l then raise (FoundGBorrowContent (Concrete bc))
- else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
+ else if ek.enter_mut_borrows then super#visit_VMutBorrow env bid mv
else ()
- | V.SharedBorrow bid ->
+ | VSharedBorrow bid ->
(* Check the borrow id *)
if bid = l then raise (FoundGBorrowContent (Concrete bc)) else ()
- | V.ReservedMutBorrow bid ->
+ | VReservedMutBorrow bid ->
(* Check the borrow id *)
if bid = l then raise (FoundGBorrowContent (Concrete bc)) else ()
method! visit_loan_content env lc =
match lc with
- | V.MutLoan bid ->
- (* Nothing special to do *) super#visit_MutLoan env bid
- | V.SharedLoan (bids, sv) ->
+ | VMutLoan bid ->
+ (* Nothing special to do *) super#visit_VMutLoan env bid
+ | VSharedLoan (bids, sv) ->
(* Control the dive *)
- if ek.enter_shared_loans then super#visit_SharedLoan env bids sv
+ if ek.enter_shared_loans then super#visit_VSharedLoan env bids sv
else ()
method! visit_aborrow_content env bc =
match bc with
- | V.AMutBorrow (bid, av) ->
+ | AMutBorrow (bid, av) ->
if bid = l then raise (FoundGBorrowContent (Abstract bc))
else super#visit_AMutBorrow env bid av
- | V.ASharedBorrow bid ->
+ | ASharedBorrow bid ->
if bid = l then raise (FoundGBorrowContent (Abstract bc))
else super#visit_ASharedBorrow env bid
- | V.AIgnoredMutBorrow (_, _)
- | V.AEndedMutBorrow _
- | V.AEndedIgnoredMutBorrow
+ | AIgnoredMutBorrow (_, _)
+ | AEndedMutBorrow _
+ | AEndedIgnoredMutBorrow
{ given_back = _; child = _; given_back_meta = _ }
- | V.AEndedSharedBorrow ->
+ | AEndedSharedBorrow ->
super#visit_aborrow_content env bc
- | V.AProjSharedBorrow asb ->
+ | AProjSharedBorrow asb ->
if borrow_in_asb l asb then
raise (FoundGBorrowContent (Abstract bc))
else ()
@@ -516,27 +516,28 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id)
method! visit_borrow_content env bc =
match bc with
- | V.MutBorrow (bid, mv) ->
+ | VMutBorrow (bid, mv) ->
(* Check the id and control dive *)
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 ->
+ else if ek.enter_mut_borrows then super#visit_VMutBorrow env bid mv
+ else VMutBorrow (bid, mv)
+ | VSharedBorrow bid ->
(* Check the id *)
- if bid = l then update () else super#visit_SharedBorrow env bid
- | V.ReservedMutBorrow bid ->
+ if bid = l then update () else super#visit_VSharedBorrow env bid
+ | VReservedMutBorrow bid ->
(* Check the id *)
- if bid = l then update () else super#visit_ReservedMutBorrow env bid
+ if bid = l then update ()
+ else super#visit_VReservedMutBorrow env bid
method! visit_loan_content env lc =
match lc with
- | V.SharedLoan (bids, sv) ->
+ | VSharedLoan (bids, sv) ->
(* Control the dive *)
- if ek.enter_shared_loans then super#visit_SharedLoan env bids sv
- else V.SharedLoan (bids, sv)
- | V.MutLoan bid ->
+ if ek.enter_shared_loans then super#visit_VSharedLoan env bids sv
+ else VSharedLoan (bids, sv)
+ | VMutLoan bid ->
(* Nothing specific to do *)
- super#visit_MutLoan env bid
+ super#visit_VMutLoan env bid
method! visit_abs env abs =
if ek.enter_abs then super#visit_abs env abs else abs
@@ -1192,18 +1193,18 @@ let get_first_non_ignored_aloan_in_abstraction (abs : V.abs) :
(** We may need to visit loan contents because of shared values *)
method! visit_loan_content _ lc =
match lc with
- | V.MutLoan _ ->
+ | VMutLoan _ ->
(* The mut loan linked to the mutable borrow present in a shared
* value in an abstraction should be in an AProjBorrows *)
raise (Failure "Unreachable")
- | V.SharedLoan (bids, _) -> raise (FoundBorrowIds (Borrows bids))
+ | VSharedLoan (bids, _) -> raise (FoundBorrowIds (Borrows bids))
method! visit_aproj env sproj =
(match sproj with
- | V.AProjBorrows (_, _)
- | V.AEndedProjLoans _ | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows ->
+ | AProjBorrows (_, _)
+ | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows ->
()
- | V.AProjLoans (sv, _) -> raise (ValuesUtils.FoundSymbolicValue sv));
+ | AProjLoans (sv, _) -> raise (ValuesUtils.FoundSymbolicValue sv));
super#visit_aproj env sproj
end
in
@@ -1225,7 +1226,7 @@ let lookup_shared_value_opt (ctx : C.eval_ctx) (bid : V.BorrowId.id) :
| None -> None
| Some (_, lc) -> (
match lc with
- | Concrete (SharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) ->
+ | Concrete (VSharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) ->
Some sv
| _ -> None)
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index b07f2629..2b7ff7d0 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -183,9 +183,9 @@ let replace_symbolic_values (at_most_once : bool)
object
inherit [_] C.map_eval_ctx as super
- method! visit_Symbolic env spc =
+ method! visit_VSymbolic env spc =
if same_symbolic_id spc original_sv then replace ()
- else super#visit_Symbolic env spc
+ else super#visit_VSymbolic env spc
end
in
(* Apply the substitution *)
@@ -326,11 +326,11 @@ let expand_symbolic_value_shared_borrow (config : C.config)
object (self)
inherit [_] C.map_eval_ctx as super
- method! visit_Symbolic env sv =
+ method! visit_VSymbolic env sv =
if same_symbolic_id sv original_sv then
let bid = fresh_borrow () in
- V.Borrow (V.SharedBorrow bid)
- else super#visit_Symbolic env sv
+ VBorrow (VSharedBorrow bid)
+ else super#visit_VSymbolic env sv
method! visit_EAbs proj_regions abs =
assert (Option.is_none proj_regions);
@@ -639,7 +639,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
object
inherit [_] C.iter_eval_ctx
- method! visit_Symbolic _ sv =
+ method! visit_VSymbolic _ sv =
if ty_has_borrows ctx.type_context.type_infos sv.V.sv_ty then
raise (FoundSymbolicValue sv)
else ()
@@ -664,22 +664,22 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
("greedy_expand_symbolics_with_borrows: about to expand: "
^ symbolic_value_to_string ctx sv));
let cc : cm_fun =
- match sv.V.sv_ty with
- | T.TAdt (TAdtId def_id, _) ->
+ match sv.sv_ty with
+ | TAdt (TAdtId def_id, _) ->
(* {!expand_symbolic_value_no_branching} checks if there are branchings,
* but we prefer to also check it here - this leads to cleaner messages
* and debugging *)
let def = C.ctx_lookup_type_decl ctx def_id in
(match def.kind with
- | T.Struct _ | T.Enum ([] | [ _ ]) -> ()
- | T.Enum (_ :: _) ->
+ | Struct _ | Enum ([] | [ _ ]) -> ()
+ | Enum (_ :: _) ->
raise
(Failure
("Attempted to greedily expand a symbolic enumeration \
with > 1 variants (option \
[greedy_expand_symbolics_with_borrows] of [config]): "
^ Print.name_to_string def.name))
- | T.Opaque ->
+ | Opaque ->
raise (Failure "Attempted to greedily expand an opaque type"));
(* Also, we need to check if the definition is recursive *)
if C.ctx_type_decl_is_rec ctx def_id then
@@ -690,16 +690,15 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
[config]): "
^ Print.name_to_string def.name))
else expand_symbolic_value_no_branching config sv None
- | T.TAdt ((TTuple | TAssumed TBox), _) | T.TRef (_, _, _) ->
+ | TAdt ((TTuple | TAssumed TBox), _) | TRef (_, _, _) ->
(* Ok *)
expand_symbolic_value_no_branching config sv None
- | T.TAdt (TAssumed (TArray | TSlice | TStr), _) ->
+ | TAdt (TAssumed (TArray | TSlice | TStr), _) ->
(* We can't expand those *)
raise
(Failure
"Attempted to greedily expand an ADT which can't be expanded ")
- | T.TVar _ | T.TLiteral _ | TNever | T.TTraitType _ | T.TArrow _
- | T.TRawPtr _ ->
+ | TVar _ | TLiteral _ | TNever | TTraitType _ | TArrow _ | TRawPtr _ ->
raise (Failure "Unreachable")
in
(* Compose and continue *)
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 7865d7be..58426cad 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -137,18 +137,18 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
* we reverted the changes: the result was less clear actually. In particular,
* the fact that we have exhaustive matches below makes very obvious the cases
* in which we need to fail *)
- match v.V.value with
- | V.VLiteral _ -> (ctx, v)
- | V.VAdt av ->
+ match v.value with
+ | VLiteral _ -> (ctx, v)
+ | VAdt av ->
(* Sanity check *)
- (match v.V.ty with
- | T.TAdt (T.TAssumed T.TBox, _) ->
+ (match v.ty with
+ | TAdt (TAssumed TBox, _) ->
raise (Failure "Can't copy an assumed value other than Option")
- | T.TAdt (T.TAdtId _, _) as ty ->
+ | TAdt (TAdtId _, _) as ty ->
assert (allow_adt_copy || ty_is_primitively_copyable ty)
- | T.TAdt (T.TTuple, _) -> () (* Ok *)
- | T.TAdt
- ( T.TAssumed (TSlice | T.TArray),
+ | TAdt (TTuple, _) -> () (* Ok *)
+ | TAdt
+ ( TAssumed (TSlice | TArray),
{
regions = [];
types = [ ty ];
@@ -162,33 +162,33 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
(copy_value allow_adt_copy config)
ctx av.field_values
in
- (ctx, { v with V.value = V.VAdt { av with field_values = fields } })
- | V.Bottom -> raise (Failure "Can't copy ⊥")
- | V.Borrow bc -> (
+ (ctx, { v with value = VAdt { av with field_values = fields } })
+ | VBottom -> raise (Failure "Can't copy ⊥")
+ | VBorrow bc -> (
(* We can only copy shared borrows *)
match bc with
- | SharedBorrow bid ->
+ | VSharedBorrow 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 = InterpreterBorrows.reborrow_shared bid bid' ctx in
- (ctx, { v with V.value = V.Borrow (SharedBorrow bid') })
- | MutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow")
- | V.ReservedMutBorrow _ ->
+ (ctx, { v with value = VBorrow (VSharedBorrow bid') })
+ | VMutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow")
+ | VReservedMutBorrow _ ->
raise (Failure "Can't copy a reserved mut borrow"))
- | V.Loan lc -> (
+ | VLoan lc -> (
(* We can only copy shared loans *)
match lc with
- | V.MutLoan _ -> raise (Failure "Can't copy a mutable loan")
- | V.SharedLoan (_, sv) ->
+ | VMutLoan _ -> raise (Failure "Can't copy a mutable loan")
+ | VSharedLoan (_, sv) ->
(* We don't copy the shared loan: only the shared value inside *)
copy_value allow_adt_copy config ctx sv)
- | V.Symbolic sp ->
+ | VSymbolic sp ->
(* We can copy only if the type is "primitively" copyable.
* Note that in the general case, copy is a trait: copying values
* thus requires calling the proper function. Here, we copy values
* for very simple types such as integers, shared borrows, etc. *)
- assert (ty_is_primitively_copyable (Subst.erase_regions sp.V.sv_ty));
+ assert (ty_is_primitively_copyable (Subst.erase_regions sp.sv_ty));
(* If the type is copyable, we simply return the current value. Side
* remark: what is important to look at when copying symbolic values
* is symbolic expansion. The important subcase is the expansion of shared
@@ -239,16 +239,16 @@ let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) :
let prepare : cm_fun =
fun cf ctx ->
match op with
- | E.Constant _ ->
+ | Constant _ ->
(* No need to reorganize the context *)
cf ctx
- | E.Copy p ->
+ | Copy p ->
(* Access the value *)
let access = Read in
(* Expand the symbolic values, if necessary *)
let expand_prim_copy = true in
access_rplace_reorganize config expand_prim_copy access p cf ctx
- | E.Move p ->
+ | Move p ->
(* Access the value *)
let access = Move in
let expand_prim_copy = false in
@@ -268,11 +268,11 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n"));
(* Evaluate *)
match op with
- | E.Constant cv -> (
+ | Constant cv -> (
match cv.value with
- | E.CLiteral lit ->
+ | CLiteral lit ->
cf (literal_to_typed_value (TypesUtils.ty_as_literal cv.ty) lit) ctx
- | E.CTraitConst (trait_ref, generics, const_name) -> (
+ | CTraitConst (trait_ref, generics, const_name) -> (
assert (generics = TypesUtils.mk_empty_generic_args);
match trait_ref.trait_id with
| T.TraitImpl _ ->
@@ -307,7 +307,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
SymbolicAst.VaTraitConstValue
(trait_ref, generics, const_name),
e ))))
- | E.CVar vid -> (
+ | CVar vid -> (
let ctx0 = ctx in
(* Lookup the const generic value *)
let cv = C.ctx_lookup_const_generic_value ctx vid in
@@ -331,8 +331,8 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
value_as_symbolic v.value,
SymbolicAst.VaCGValue vid,
e )))
- | E.CFnPtr _ -> raise (Failure "TODO"))
- | E.Copy p ->
+ | CFnPtr _ -> raise (Failure "TODO"))
+ | Copy p ->
(* Access the value *)
let access = Read in
let cc = read_place access p in
@@ -353,7 +353,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
in
(* Compose and apply *)
comp cc copy cf ctx
- | E.Move p ->
+ | Move p ->
(* Access the value *)
let access = Move in
let cc = read_place access p in
@@ -362,7 +362,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
fun ctx ->
(* Check that there are no bottoms in the value we are about to move *)
assert (not (bottom_in_value ctx.ended_regions v));
- let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in
+ let bottom : V.typed_value = { V.value = VBottom; ty = v.ty } in
let ctx = write_place access p bottom ctx in
cf v ctx
in
@@ -622,18 +622,18 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
(cf : V.typed_value -> m_fun) : m_fun =
fun ctx ->
match bkind with
- | E.Shared | E.TwoPhaseMut | E.Shallow ->
+ | Shared | TwoPhaseMut | Shallow ->
(* **REMARK**: we initially treated shallow borrows like shared borrows.
In practice this restricted the behaviour too much, so for now we
forbid them.
*)
- assert (bkind <> E.Shallow);
+ assert (bkind <> Shallow);
(* Access the value *)
let access =
match bkind with
- | E.Shared | E.Shallow -> Read
- | E.TwoPhaseMut -> Write
+ | Shared | Shallow -> Read
+ | TwoPhaseMut -> Write
| _ -> raise (Failure "Unreachable")
in
@@ -648,17 +648,17 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
let bid = C.fresh_borrow_id () in
(* Compute the loan value, with which to replace the value at place p *)
let nv =
- match v.V.value with
- | V.Loan (V.SharedLoan (bids, sv)) ->
+ match v.value with
+ | VLoan (VSharedLoan (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 value = VLoan (VSharedLoan (bids1, sv)) }
| _ ->
(* Not a shared loan: add a wrapper *)
let v' =
- V.Loan (V.SharedLoan (V.BorrowId.Set.singleton bid, v))
+ V.VLoan (VSharedLoan (V.BorrowId.Set.singleton bid, v))
in
- { v with V.value = v' }
+ { v with value = v' }
in
(* Update the borrowed value in the context *)
let ctx = write_place access p nv ctx in
@@ -666,27 +666,27 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
* Note that the reference is *mutable* if we do a two-phase borrow *)
let ref_kind =
match bkind with
- | E.Shared | E.Shallow -> T.Shared
- | E.TwoPhaseMut -> T.Mut
+ | Shared | Shallow -> T.Shared
+ | TwoPhaseMut -> T.Mut
| _ -> raise (Failure "Unreachable")
in
let rv_ty = T.TRef (T.RErased, v.ty, ref_kind) in
let bc =
match bkind with
- | E.Shared | E.Shallow ->
+ | Shared | Shallow ->
(* See the remark at the beginning of the match branch: we
handle shallow borrows like shared borrows *)
- V.SharedBorrow bid
- | E.TwoPhaseMut -> V.ReservedMutBorrow bid
+ V.VSharedBorrow bid
+ | TwoPhaseMut -> VReservedMutBorrow bid
| _ -> raise (Failure "Unreachable")
in
- let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in
+ let rv : V.typed_value = { value = VBorrow bc; ty = rv_ty } in
(* Continue *)
cf rv ctx
in
(* Compose and apply *)
comp prepare eval cf ctx
- | E.Mut ->
+ | Mut ->
(* Access the value *)
let access = Write in
let expand_prim_copy = false in
@@ -698,12 +698,12 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
fun ctx ->
(* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *)
let bid = C.fresh_borrow_id () in
- let rv_ty = T.TRef (T.RErased, v.ty, Mut) in
+ let rv_ty = T.TRef (RErased, v.ty, Mut) in
let rv : V.typed_value =
- { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty }
+ { V.value = VBorrow (VMutBorrow (bid, v)); ty = rv_ty }
in
(* Compute the value with which to replace the value at place p *)
- let nv = { v with V.value = V.Loan (V.MutLoan bid) } in
+ let nv = { v with value = VLoan (VMutLoan bid) } in
(* Update the value in the context *)
let ctx = write_place access p nv ctx in
(* Continue *)
@@ -723,7 +723,7 @@ let eval_rvalue_aggregate (config : C.config)
fun ctx ->
(* Match on the aggregate kind *)
match aggregate_kind with
- | E.AggregatedAdt (type_id, opt_variant_id, generics) -> (
+ | AggregatedAdt (type_id, opt_variant_id, generics) -> (
match type_id with
| TTuple ->
let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
@@ -755,7 +755,7 @@ let eval_rvalue_aggregate (config : C.config)
(* Call the continuation *)
cf aggregated ctx
| TAssumed _ -> raise (Failure "Unreachable"))
- | E.AggregatedArray (ety, cg) -> (
+ | AggregatedArray (ety, cg) -> (
(* Sanity check: all the values have the proper type *)
assert (List.for_all (fun (v : V.typed_value) -> v.V.ty = ety) values);
(* Sanity check: the number of values is consistent with the length *)
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 2f7e8f3d..a35b2716 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -227,17 +227,17 @@ let prepare_ashared_loans (loop_id : V.LoopId.id option) : cm_fun =
object
inherit [_] V.iter_typed_avalue as super
- method! visit_SharedLoan env lids sv =
+ method! visit_VSharedLoan env lids sv =
collect_shared_value lids sv;
(* Continue the exploration *)
- super#visit_SharedLoan env lids sv
+ super#visit_VSharedLoan env lids sv
- method! visit_ASharedLoan env lids sv _ =
+ method! visit_ASharedLoan env lids sv av =
collect_shared_value lids sv;
(* Continue the exploration *)
- super#visit_SharedLoan env lids sv
+ super#visit_ASharedLoan env lids sv av
(** Check that there are no symbolic values with *borrows* inside the
abstraction - shouldn't happen if the symbolic values are greedily
@@ -743,8 +743,8 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets)
let open InterpreterBorrowsCore in
let lookup_shared_loan lid ctx : V.typed_value =
match snd (lookup_loan ek_all lid ctx) with
- | Concrete (V.SharedLoan (_, v)) -> v
- | Abstract (V.ASharedLoan (_, v, _)) -> v
+ | Concrete (VSharedLoan (_, v)) -> v
+ | Abstract (ASharedLoan (_, v, _)) -> v
| _ -> raise (Failure "Unreachable")
in
let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in
@@ -927,12 +927,12 @@ let compute_fp_ctx_symbolic_values (ctx : C.eval_ctx) (fp_ctx : C.eval_ctx) :
inherit [_] C.iter_env
(** We lookup the shared values *)
- method! visit_SharedBorrow env bid =
+ method! visit_VSharedBorrow env bid =
let open InterpreterBorrowsCore in
let v =
match snd (lookup_loan ek_all bid fp_ctx) with
- | Concrete (V.SharedLoan (_, v)) -> v
- | Abstract (V.ASharedLoan (_, v, _)) -> v
+ | Concrete (VSharedLoan (_, v)) -> v
+ | Abstract (ASharedLoan (_, v, _)) -> v
| _ -> raise (Failure "Unreachable")
in
self#visit_typed_value env v
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 27020efb..7741abbc 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -212,66 +212,66 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
assert (not (value_has_borrows ctx v1.V.value));
(* Merge *)
M.match_distinct_adts ty av0 av1)
- | Bottom, Bottom -> v0
- | Borrow bc0, Borrow bc1 ->
+ | VBottom, VBottom -> v0
+ | VBorrow bc0, VBorrow bc1 ->
let bc =
match (bc0, bc1) with
- | SharedBorrow bid0, SharedBorrow bid1 ->
+ | VSharedBorrow bid0, VSharedBorrow bid1 ->
let bid = M.match_shared_borrows match_rec ty bid0 bid1 in
- V.SharedBorrow bid
- | MutBorrow (bid0, bv0), MutBorrow (bid1, bv1) ->
+ V.VSharedBorrow bid
+ | VMutBorrow (bid0, bv0), VMutBorrow (bid1, bv1) ->
let bv = match_rec bv0 bv1 in
assert (not (value_has_borrows ctx bv.V.value));
let bid, bv = M.match_mut_borrows ty bid0 bv0 bid1 bv1 bv in
- V.MutBorrow (bid, bv)
- | ReservedMutBorrow _, _
- | _, ReservedMutBorrow _
- | SharedBorrow _, MutBorrow _
- | MutBorrow _, SharedBorrow _ ->
+ VMutBorrow (bid, bv)
+ | VReservedMutBorrow _, _
+ | _, VReservedMutBorrow _
+ | VSharedBorrow _, VMutBorrow _
+ | VMutBorrow _, VSharedBorrow _ ->
(* If we get here, either there is a typing inconsistency, or we are
trying to match a reserved borrow, which shouldn't happen because
reserved borrow should be eliminated very quickly - they are introduced
just before function calls which activate them *)
raise (Failure "Unexpected")
in
- { V.value = V.Borrow bc; ty }
- | Loan lc0, Loan lc1 ->
+ { V.value = VBorrow bc; ty }
+ | VLoan lc0, VLoan lc1 ->
(* TODO: maybe we should enforce that the ids are always exactly the same -
without matching *)
let lc =
match (lc0, lc1) with
- | SharedLoan (ids0, sv0), SharedLoan (ids1, sv1) ->
+ | VSharedLoan (ids0, sv0), VSharedLoan (ids1, sv1) ->
let sv = match_rec sv0 sv1 in
assert (not (value_has_borrows ctx sv.V.value));
let ids, sv = M.match_shared_loans ty ids0 ids1 sv in
- V.SharedLoan (ids, sv)
- | MutLoan id0, MutLoan id1 ->
+ V.VSharedLoan (ids, sv)
+ | VMutLoan id0, VMutLoan id1 ->
let id = M.match_mut_loans ty id0 id1 in
- V.MutLoan id
- | SharedLoan _, MutLoan _ | MutLoan _, SharedLoan _ ->
+ VMutLoan id
+ | VSharedLoan _, VMutLoan _ | VMutLoan _, VSharedLoan _ ->
raise (Failure "Unreachable")
in
- { V.value = Loan lc; ty = v1.V.ty }
- | Symbolic sv0, Symbolic sv1 ->
+ { V.value = VLoan lc; ty = v1.V.ty }
+ | VSymbolic sv0, VSymbolic sv1 ->
(* For now, we force all the symbolic values containing borrows to
be eagerly expanded, and we don't support nested borrows *)
assert (not (value_has_borrows ctx v0.V.value));
assert (not (value_has_borrows ctx v1.V.value));
(* Match *)
let sv = M.match_symbolic_values sv0 sv1 in
- { v1 with V.value = V.Symbolic sv }
- | Loan lc, _ -> (
+ { v1 with V.value = VSymbolic sv }
+ | VLoan lc, _ -> (
match lc with
- | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids))
- | MutLoan id -> raise (ValueMatchFailure (LoanInLeft id)))
- | _, Loan lc -> (
+ | VSharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInLeft ids))
+ | VMutLoan id -> raise (ValueMatchFailure (LoanInLeft id)))
+ | _, VLoan lc -> (
match lc with
- | SharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids))
- | MutLoan id -> raise (ValueMatchFailure (LoanInRight id)))
- | Symbolic sv, _ -> M.match_symbolic_with_other true sv v1
- | _, Symbolic sv -> M.match_symbolic_with_other false sv v0
- | Bottom, _ -> M.match_bottom_with_other true v1
- | _, Bottom -> M.match_bottom_with_other false v0
+ | VSharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids))
+ | VMutLoan id -> raise (ValueMatchFailure (LoanInRight id)))
+ | VSymbolic sv, _ -> M.match_symbolic_with_other true sv v1
+ | _, VSymbolic sv -> M.match_symbolic_with_other false sv v0
+ | VBottom, _ -> M.match_bottom_with_other true v1
+ | _, VBottom -> M.match_bottom_with_other false v0
| _ ->
log#ldebug
(lazy
@@ -414,10 +414,10 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
(* Check if there are loans: we request to end them *)
let check_loans (left : bool) (fields : V.typed_value list) : unit =
match InterpreterBorrowsCore.get_first_loan_in_values fields with
- | Some (V.SharedLoan (ids, _)) ->
+ | Some (VSharedLoan (ids, _)) ->
if left then raise (ValueMatchFailure (LoansInLeft ids))
else raise (ValueMatchFailure (LoansInRight ids))
- | Some (V.MutLoan id) ->
+ | Some (VMutLoan id) ->
if left then raise (ValueMatchFailure (LoanInLeft id))
else raise (ValueMatchFailure (LoanInRight id))
| None -> ()
@@ -688,10 +688,10 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
let value_is_left = not left in
(match InterpreterBorrowsCore.get_first_loan_in_value v with
| None -> ()
- | Some (SharedLoan (ids, _)) ->
+ | Some (VSharedLoan (ids, _)) ->
if value_is_left then raise (ValueMatchFailure (LoansInLeft ids))
else raise (ValueMatchFailure (LoansInRight ids))
- | Some (MutLoan id) ->
+ | Some (VMutLoan id) ->
if value_is_left then raise (ValueMatchFailure (LoanInLeft id))
else raise (ValueMatchFailure (LoanInRight id)));
(* Return a fresh symbolic value *)
@@ -711,10 +711,10 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
| Some (BorrowContent _) -> raise (Failure "Unreachable")
| Some (LoanContent lc) -> (
match lc with
- | V.SharedLoan (ids, _) ->
+ | VSharedLoan (ids, _) ->
if value_is_left then raise (ValueMatchFailure (LoansInLeft ids))
else raise (ValueMatchFailure (LoansInRight ids))
- | V.MutLoan id ->
+ | VMutLoan id ->
if value_is_left then raise (ValueMatchFailure (LoanInLeft id))
else raise (ValueMatchFailure (LoanInRight id)))
| None ->
@@ -1366,8 +1366,8 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
let open InterpreterBorrowsCore in
let lookup_shared_loan lid ctx : V.typed_value =
match snd (lookup_loan ek_all lid ctx) with
- | Concrete (V.SharedLoan (_, v)) -> v
- | Abstract (V.ASharedLoan (_, v, _)) -> v
+ | Concrete (VSharedLoan (_, v)) -> v
+ | Abstract (ASharedLoan (_, v, _)) -> v
| _ -> raise (Failure "Unreachable")
in
let lookup_in_src id = lookup_shared_loan id src_ctx in
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 36af1db4..9158f2c1 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -95,13 +95,13 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
Ok (ctx, { read = v; updated = nv })
| pe :: p' -> (
(* Match on the projection element and the value *)
- match (pe, v.V.value, v.V.ty) with
+ match (pe, v.value, v.ty) with
| ( Field ((ProjAdt (_, _) as proj_kind), field_id),
- V.VAdt adt,
- T.TAdt (type_id, _) ) -> (
+ VAdt adt,
+ TAdt (type_id, _) ) -> (
(* Check consistency *)
(match (proj_kind, type_id) with
- | ProjAdt (def_id, opt_variant_id), T.TAdtId def_id' ->
+ | ProjAdt (def_id, opt_variant_id), TAdtId def_id' ->
assert (def_id = def_id');
assert (opt_variant_id = adt.variant_id)
| _ -> raise (Failure "Unreachable"));
@@ -114,11 +114,11 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
let nvalues =
T.FieldId.update_nth adt.field_values field_id res.updated
in
- let nadt = V.VAdt { adt with V.field_values = nvalues } in
+ let nadt = V.VAdt { adt with field_values = nvalues } in
let updated = { v with value = nadt } in
Ok (ctx, { res with updated }))
(* Tuples *)
- | Field (ProjTuple arity, field_id), V.VAdt adt, T.TAdt (T.TTuple, _) -> (
+ | Field (ProjTuple arity, field_id), VAdt adt, TAdt (TTuple, _) -> (
assert (arity = List.length adt.field_values);
let fv = T.FieldId.nth adt.field_values field_id in
(* Project *)
@@ -134,16 +134,16 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
Ok (ctx, { res with updated })
(* If we reach Bottom, it may mean we need to expand an uninitialized
* enumeration value *))
- | Field ((ProjAdt (_, _) | ProjTuple _), _), V.Bottom, _ ->
+ | Field ((ProjAdt (_, _) | ProjTuple _), _), VBottom, _ ->
Error (FailBottom (1 + List.length p', pe, v.ty))
(* Symbolic value: needs to be expanded *)
- | _, Symbolic sp, _ ->
+ | _, VSymbolic sp, _ ->
(* Expand the symbolic value *)
Error (FailSymbolic (1 + List.length p', sp))
(* Box dereferencement *)
| ( DerefBox,
VAdt { variant_id = None; field_values = [ bv ] },
- T.TAdt (T.TAssumed T.TBox, _) ) -> (
+ TAdt (TAssumed TBox, _) ) -> (
(* We allow moving outside of boxes. In practice, this kind of
* manipulations should happen only inside unsafe code, so
* it shouldn't happen due to user code, and we leverage it
@@ -156,20 +156,20 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
{
v with
value =
- V.VAdt { variant_id = None; field_values = [ res.updated ] };
+ VAdt { variant_id = None; field_values = [ res.updated ] };
}
in
Ok (ctx, { res with updated = nv }))
(* Borrows *)
- | Deref, V.Borrow bc, _ -> (
+ | Deref, VBorrow bc, _ -> (
match bc with
- | V.SharedBorrow bid ->
+ | VSharedBorrow bid ->
(* Lookup the loan content, and explore from there *)
if access.lookup_shared_borrows then
match lookup_loan ek bid ctx with
- | _, Concrete (V.MutLoan _) ->
+ | _, Concrete (VMutLoan _) ->
raise (Failure "Expected a shared loan")
- | _, Concrete (V.SharedLoan (bids, sv)) -> (
+ | _, Concrete (VSharedLoan (bids, sv)) -> (
(* Explore the shared value *)
match access_projection access ctx update p' sv with
| Error err -> Error err
@@ -178,23 +178,23 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
by {!access_projection} *)
let ctx =
update_loan ek bid
- (V.SharedLoan (bids, res.updated))
+ (VSharedLoan (bids, res.updated))
ctx
in
(* Return - note that we don't need to update the borrow itself *)
Ok (ctx, { res with updated = v }))
| ( _,
Abstract
- ( V.AMutLoan (_, _)
- | V.AEndedMutLoan
+ ( AMutLoan (_, _)
+ | AEndedMutLoan
{ given_back = _; child = _; given_back_meta = _ }
- | V.AEndedSharedLoan (_, _)
- | V.AIgnoredMutLoan (_, _)
- | V.AEndedIgnoredMutLoan
+ | AEndedSharedLoan (_, _)
+ | AIgnoredMutLoan (_, _)
+ | AEndedIgnoredMutLoan
{ given_back = _; child = _; given_back_meta = _ }
- | V.AIgnoredSharedLoan _ ) ) ->
+ | AIgnoredSharedLoan _ ) ) ->
raise (Failure "Expected a shared (abstraction) loan")
- | _, Abstract (V.ASharedLoan (bids, sv, _av)) -> (
+ | _, Abstract (ASharedLoan (bids, sv, _av)) -> (
(* Explore the shared value *)
match access_projection access ctx update p' sv with
| Error err -> Error err
@@ -202,37 +202,34 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
(* Relookup the child avalue *)
let av =
match lookup_loan ek bid ctx with
- | _, Abstract (V.ASharedLoan (_, _, av)) -> av
+ | _, Abstract (ASharedLoan (_, _, av)) -> av
| _ -> raise (Failure "Unexpected")
in
(* Update the shared loan with the new value returned
by {!access_projection} *)
let ctx =
update_aloan ek bid
- (V.ASharedLoan (bids, res.updated, av))
+ (ASharedLoan (bids, res.updated, av))
ctx
in
(* Return - note that we don't need to update the borrow itself *)
Ok (ctx, { res with updated = v }))
else Error (FailBorrow bc)
- | V.ReservedMutBorrow bid -> Error (FailReservedMutBorrow bid)
- | V.MutBorrow (bid, bv) ->
+ | VReservedMutBorrow bid -> Error (FailReservedMutBorrow bid)
+ | VMutBorrow (bid, bv) ->
if access.enter_mut_borrows then
match access_projection access ctx update p' bv with
| Error err -> Error err
| Ok (ctx, res) ->
let nv =
- {
- v with
- value = V.Borrow (V.MutBorrow (bid, res.updated));
- }
+ { v with value = VBorrow (VMutBorrow (bid, res.updated)) }
in
Ok (ctx, { res with updated = nv })
else Error (FailBorrow bc))
- | _, V.Loan lc, _ -> (
+ | _, VLoan lc, _ -> (
match lc with
- | V.MutLoan bid -> Error (FailMutLoan bid)
- | V.SharedLoan (bids, sv) ->
+ | VMutLoan bid -> Error (FailMutLoan bid)
+ | VSharedLoan (bids, sv) ->
(* If we can enter shared loan, we ignore the loan. Pay attention
to the fact that we need to reexplore the *whole* place (i.e,
we mustn't ignore the current projection element *)
@@ -241,14 +238,11 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
| Error err -> Error err
| Ok (ctx, res) ->
let nv =
- {
- v with
- value = V.Loan (V.SharedLoan (bids, res.updated));
- }
+ { v with value = VLoan (VSharedLoan (bids, res.updated)) }
in
Ok (ctx, { res with updated = nv })
else Error (FailSharedLoan bids))
- | (_, (V.VLiteral _ | V.VAdt _ | V.Bottom | V.Borrow _), _) as r ->
+ | (_, (VLiteral _ | VAdt _ | VBottom | VBorrow _), _) as r ->
let pe, v, ty = r in
let pe = "- pe: " ^ E.show_projection_elem pe in
let v = "- v:\n" ^ V.show_value v in
@@ -531,24 +525,24 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
method! visit_borrow_content env bc =
match bc with
- | V.SharedBorrow _ | V.MutBorrow (_, _) ->
+ | VSharedBorrow _ | VMutBorrow (_, _) ->
(* Nothing special to do *) super#visit_borrow_content env bc
- | V.ReservedMutBorrow bid ->
+ | VReservedMutBorrow bid ->
(* We need to activate reserved borrows *)
let cc = promote_reserved_mut_borrow config bid in
raise (UpdateCtx cc)
method! visit_loan_content env lc =
match lc with
- | V.SharedLoan (bids, v) -> (
+ | VSharedLoan (bids, v) -> (
(* End the loans if we need a modification access, otherwise dive into
the shared value *)
match access with
- | Read -> super#visit_SharedLoan env bids v
+ | Read -> super#visit_VSharedLoan env bids v
| Write | Move ->
let cc = end_borrows config bids in
raise (UpdateCtx cc))
- | V.MutLoan bid ->
+ | VMutLoan bid ->
(* We always need to end mutable borrows *)
let cc = end_borrow config bid in
raise (UpdateCtx cc)
@@ -596,8 +590,8 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
(* There are: end them then retry *)
let cc =
match c with
- | LoanContent (V.SharedLoan (bids, _)) -> end_borrows config bids
- | LoanContent (V.MutLoan bid) -> end_borrow config bid
+ | LoanContent (VSharedLoan (bids, _)) -> end_borrows config bids
+ | LoanContent (VMutLoan bid) -> end_borrow config bid
| BorrowContent _ -> raise (Failure "Unreachable")
in
(* Retry *)
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index e47886ec..8a4b0b4c 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -20,20 +20,20 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
(* Sanity check - TODO: move those elsewhere (here we perform the check at every
* recursive call which is a bit overkill...) *)
let ety = Subst.erase_regions ty in
- assert (ty_is_rty ty && ety = v.V.ty);
+ assert (ty_is_rty ty && ety = v.ty);
(* Project - if there are no regions from the abstraction in the type, return [_] *)
if not (ty_has_regions_in_set regions ty) then []
else
- match (v.V.value, ty) with
- | V.VLiteral _, T.TLiteral _ -> []
- | V.VAdt adt, T.TAdt (id, generics) ->
+ match (v.value, ty) with
+ | VLiteral _, TLiteral _ -> []
+ | VAdt adt, TAdt (id, generics) ->
(* Retrieve the types of the fields *)
let field_types =
Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics
in
(* Project over the field values *)
- let fields_types = List.combine adt.V.field_values field_types in
+ let fields_types = List.combine adt.field_values field_types in
let proj_fields =
List.map
(fun (fv, fty) ->
@@ -42,33 +42,33 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
fields_types
in
List.concat proj_fields
- | V.Bottom, _ -> raise (Failure "Unreachable")
- | V.Borrow bc, TRef (r, ref_ty, kind) ->
+ | VBottom, _ -> raise (Failure "Unreachable")
+ | VBorrow bc, TRef (r, ref_ty, kind) ->
(* Retrieve the bid of the borrow and the asb of the projected borrowed value *)
let bid, asb =
(* Not in the set: dive *)
match (bc, kind) with
- | V.MutBorrow (bid, bv), T.Mut ->
+ | VMutBorrow (bid, bv), Mut ->
(* Apply the projection on the borrowed value *)
let asb =
apply_proj_borrows_on_shared_borrow ctx fresh_reborrow regions
bv ref_ty
in
(bid, asb)
- | V.SharedBorrow bid, T.Shared ->
+ | VSharedBorrow bid, Shared ->
(* Lookup the shared value *)
let ek = ek_all in
let sv = lookup_loan ek bid ctx in
let asb =
match sv with
- | _, Concrete (V.SharedLoan (_, sv))
- | _, Abstract (V.ASharedLoan (_, sv, _)) ->
+ | _, Concrete (VSharedLoan (_, sv))
+ | _, Abstract (ASharedLoan (_, sv, _)) ->
apply_proj_borrows_on_shared_borrow ctx fresh_reborrow
regions sv ref_ty
| _ -> raise (Failure "Unexpected")
in
(bid, asb)
- | V.ReservedMutBorrow _, _ ->
+ | VReservedMutBorrow _, _ ->
raise
(Failure
"Can't apply a proj_borrow over a reserved mutable borrow")
@@ -83,8 +83,8 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
else asb
in
asb
- | V.Loan _, _ -> raise (Failure "Unreachable")
- | V.Symbolic s, _ ->
+ | VLoan _, _ -> raise (Failure "Unreachable")
+ | VSymbolic s, _ ->
(* Check that the projection doesn't contain ended regions *)
assert (
not (projections_intersect s.V.sv_ty ctx.ended_regions ty regions));
@@ -103,15 +103,15 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
if not (ty_has_regions_in_set regions ty) then { V.value = V.AIgnored; ty }
else
let value : V.avalue =
- match (v.V.value, ty) with
- | V.VLiteral _, T.TLiteral _ -> V.AIgnored
- | V.VAdt adt, T.TAdt (id, generics) ->
+ match (v.value, ty) with
+ | VLiteral _, T.TLiteral _ -> V.AIgnored
+ | VAdt adt, T.TAdt (id, generics) ->
(* Retrieve the types of the fields *)
let field_types =
Assoc.ctx_adt_value_get_inst_norm_field_rtypes ctx adt id generics
in
(* Project over the field values *)
- let fields_types = List.combine adt.V.field_values field_types in
+ let fields_types = List.combine adt.field_values field_types in
let proj_fields =
List.map
(fun (fv, fty) ->
@@ -119,9 +119,9 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
regions ancestors_regions fv fty)
fields_types
in
- V.AAdt { V.variant_id = adt.V.variant_id; field_values = proj_fields }
- | V.Bottom, _ -> raise (Failure "Unreachable")
- | V.Borrow bc, TRef (r, ref_ty, kind) ->
+ V.AAdt { variant_id = adt.variant_id; field_values = proj_fields }
+ | VBottom, _ -> raise (Failure "Unreachable")
+ | VBorrow bc, TRef (r, ref_ty, kind) ->
if
(* Check if the region is in the set of projected regions (note that
* we never project over static regions) *)
@@ -130,14 +130,14 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
(* In the set *)
let bc =
match (bc, kind) with
- | V.MutBorrow (bid, bv), T.Mut ->
+ | VMutBorrow (bid, bv), T.Mut ->
(* Apply the projection on the borrowed value *)
let bv =
apply_proj_borrows check_symbolic_no_ended ctx
fresh_reborrow regions ancestors_regions bv ref_ty
in
V.AMutBorrow (bid, bv)
- | V.SharedBorrow bid, T.Shared ->
+ | VSharedBorrow bid, T.Shared ->
(* Rem.: we don't need to also apply the projection on the
borrowed value, because for as long as the abstraction
lives then the shared borrow lives, which means that the
@@ -150,7 +150,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
other branch of the [if then else]).
*)
V.ASharedBorrow bid
- | V.ReservedMutBorrow _, _ ->
+ | VReservedMutBorrow _, _ ->
raise
(Failure
"Can't apply a proj_borrow over a reserved mutable \
@@ -164,7 +164,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
the region set) *)
let bc =
match (bc, kind) with
- | V.MutBorrow (bid, bv), T.Mut ->
+ | VMutBorrow (bid, bv), T.Mut ->
(* Apply the projection on the borrowed value *)
let bv =
apply_proj_borrows check_symbolic_no_ended ctx
@@ -177,20 +177,20 @@ 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 ->
+ | VSharedBorrow bid, T.Shared ->
(* Lookup the shared value *)
let ek = ek_all in
let sv = lookup_loan ek bid ctx in
let asb =
match sv with
- | _, Concrete (V.SharedLoan (_, sv))
- | _, Abstract (V.ASharedLoan (_, sv, _)) ->
+ | _, Concrete (VSharedLoan (_, sv))
+ | _, Abstract (ASharedLoan (_, sv, _)) ->
apply_proj_borrows_on_shared_borrow ctx fresh_reborrow
regions sv ref_ty
| _ -> raise (Failure "Unexpected")
in
V.AProjSharedBorrow asb
- | V.ReservedMutBorrow _, _ ->
+ | VReservedMutBorrow _, _ ->
raise
(Failure
"Can't apply a proj_borrow over a reserved mutable \
@@ -198,12 +198,12 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
| _ -> raise (Failure "Unreachable")
in
V.ABorrow bc
- | V.Loan _, _ -> raise (Failure "Unreachable")
- | V.Symbolic s, _ ->
+ | VLoan _, _ -> raise (Failure "Unreachable")
+ | VSymbolic s, _ ->
(* Check that the projection doesn't contain already ended regions,
* if necessary *)
if check_symbolic_no_ended then (
- let ty1 = s.V.sv_ty in
+ let ty1 = s.sv_ty in
let rset1 = ctx.ended_regions in
let ty2 = ty in
let rset2 = regions in
@@ -216,7 +216,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
^ T.RegionId.Set.to_string None rset2
^ "\n"));
assert (not (projections_intersect ty1 rset1 ty2 rset2)));
- V.ASymbolic (V.AProjBorrows (s, ty))
+ V.ASymbolic (AProjBorrows (s, ty))
| _ ->
log#lerror
(lazy
@@ -225,7 +225,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
^ "\n- proj rty: " ^ PA.ty_to_string ctx ty));
raise (Failure "Unreachable")
in
- { V.value; V.ty }
+ { value; ty }
let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
(see : V.symbolic_expansion) : V.typed_value =
@@ -249,7 +249,7 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value)
| SeMutRef (bid, bv) ->
let ty = Subst.erase_regions sv.V.sv_ty in
let bv = mk_typed_value_from_symbolic_value bv in
- let value = V.Borrow (V.MutBorrow (bid, bv)) in
+ let value = V.VBorrow (VMutBorrow (bid, bv)) in
{ V.value; ty }
| SeSharedRef (_, _) ->
raise (Failure "Unexpected symbolic shared reference expansion")
@@ -346,11 +346,11 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
(* Check if a value is a mutable borrow, and return its identifier if
it is the case *)
let get_borrow_in_mut_borrow (v : V.typed_value) : V.BorrowId.id option =
- match v.V.value with
- | V.Borrow lc -> (
+ match v.value with
+ | VBorrow lc -> (
match lc with
- | V.SharedBorrow _ | V.ReservedMutBorrow _ -> None
- | V.MutBorrow (id, _) -> Some id)
+ | VSharedBorrow _ | VReservedMutBorrow _ -> None
+ | VMutBorrow (id, _) -> Some id)
| _ -> None
in
@@ -397,18 +397,18 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
(** We may need to reborrow mutable borrows. Note that this doesn't
happen for aborrows *)
method! visit_typed_value env v =
- match v.V.value with
- | V.Borrow (V.MutBorrow (bid, bv)) ->
+ match v.value with
+ | VBorrow (VMutBorrow (bid, bv)) ->
let insert = get_reborrows_for_bid bid in
- let nbc = super#visit_MutBorrow env bid bv in
- let nbc = { v with V.value = V.Borrow nbc } in
+ let nbc = super#visit_VMutBorrow env bid bv in
+ let nbc = { v with value = VBorrow nbc } in
if insert = [] then (* No reborrows: do nothing special *)
nbc
else
(* There are reborrows: insert a shared loan *)
let insert = borrows_to_set insert in
- let value = V.Loan (V.SharedLoan (insert, nbc)) in
- let ty = v.V.ty in
+ let value = V.VLoan (VSharedLoan (insert, nbc)) in
+ let ty = v.ty in
{ V.value; ty }
| _ -> super#visit_typed_value env v
@@ -416,7 +416,7 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
functions) on purpose: exhaustive matches are good for maintenance *)
method! visit_loan_content env lc =
match lc with
- | V.SharedLoan (bids, sv) ->
+ | VSharedLoan (bids, sv) ->
(* Insert the reborrows *)
let bids = insert_reborrows bids in
(* Check if the contained value is a mutable borrow, in which
@@ -432,14 +432,14 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
| Some bid -> insert_reborrows_for_bid bids bid
in
(* Update and explore *)
- super#visit_SharedLoan env bids sv
- | V.MutLoan bid ->
+ super#visit_VSharedLoan env bids sv
+ | VMutLoan bid ->
(* Nothing special to do *)
- super#visit_MutLoan env bid
+ super#visit_VMutLoan env bid
method! visit_aloan_content env lc =
match lc with
- | V.ASharedLoan (bids, sv, av) ->
+ | ASharedLoan (bids, sv, av) ->
(* Insert the reborrows *)
let bids = insert_reborrows bids in
(* Similarly to the non-abstraction case: check if the shared
@@ -452,12 +452,12 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
in
(* Update and explore *)
super#visit_ASharedLoan env bids sv av
- | V.AIgnoredSharedLoan _
- | V.AMutLoan (_, _)
- | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
- | V.AEndedSharedLoan (_, _)
- | V.AIgnoredMutLoan (_, _)
- | V.AEndedIgnoredMutLoan
+ | AIgnoredSharedLoan _
+ | AMutLoan (_, _)
+ | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+ | AEndedSharedLoan (_, _)
+ | AIgnoredMutLoan (_, _)
+ | AEndedIgnoredMutLoan
{ given_back = _; child = _; given_back_meta = _ } ->
(* Nothing particular to do *)
super#visit_aloan_content env lc
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index cf9b840b..cbc09c29 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -43,7 +43,7 @@ let drop_value (config : C.config) (p : E.place) : cm_fun =
let dummy_id = C.fresh_dummy_var_id () in
let ctx = C.ctx_push_dummy_var ctx dummy_id mv in
(* Update the destination to ⊥ *)
- let nv = { v with value = V.Bottom } in
+ let nv = { v with value = VBottom } in
let ctx = write_place access p nv ctx in
log#ldebug
(lazy
@@ -172,7 +172,7 @@ let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun =
(* Evaluate the assertion *)
let eval_assert cf (v : V.typed_value) : m_fun =
fun ctx ->
- assert (v.ty = T.TLiteral PV.TBool);
+ assert (v.ty = TLiteral TBool);
(* We make a choice here: we could completely decouple the concrete and
* symbolic executions here but choose not to. In the case where we
* know the concrete value of the boolean we test, we use this value
@@ -182,16 +182,16 @@ let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun =
| VLiteral (VBool _) ->
(* Delegate to the concrete evaluation function *)
eval_assertion_concrete config assertion cf ctx
- | Symbolic sv ->
- assert (config.mode = C.SymbolicMode);
- assert (sv.V.sv_ty = T.TLiteral PV.TBool);
+ | VSymbolic sv ->
+ assert (config.mode = SymbolicMode);
+ assert (sv.sv_ty = TLiteral TBool);
(* We continue the execution as if the test had succeeded, and thus
* perform the symbolic expansion: sv ~~> true.
* We will of course synthesize an assertion in the generated code
* (see below). *)
let ctx =
- apply_symbolic_expansion_non_borrow config sv
- (V.SeLiteral (PV.VBool true)) ctx
+ apply_symbolic_expansion_non_borrow config sv (SeLiteral (VBool true))
+ ctx
in
(* Continue *)
let expr = cf Unit ctx in
@@ -231,8 +231,8 @@ let set_discriminant (config : C.config) (p : E.place)
(* Update the value *)
let update_value cf (v : V.typed_value) : m_fun =
fun ctx ->
- match (v.V.ty, v.V.value) with
- | T.TAdt ((T.TAdtId _ as type_id), generics), V.VAdt av -> (
+ match (v.ty, v.value) with
+ | TAdt ((TAdtId _ as type_id), generics), VAdt av -> (
(* There are two situations:
- either the discriminant is already the proper one (in which case we
don't do anything)
@@ -248,22 +248,22 @@ let set_discriminant (config : C.config) (p : E.place)
(* Replace the value *)
let bottom_v =
match type_id with
- | T.TAdtId def_id ->
+ | TAdtId def_id ->
compute_expanded_bottom_adt_value ctx def_id
(Some variant_id) generics
| _ -> raise (Failure "Unreachable")
in
assign_to_place config bottom_v p (cf Unit) ctx)
- | T.TAdt ((T.TAdtId _ as type_id), generics), V.Bottom ->
+ | TAdt ((TAdtId _ as type_id), generics), VBottom ->
let bottom_v =
match type_id with
- | T.TAdtId def_id ->
+ | TAdtId def_id ->
compute_expanded_bottom_adt_value ctx def_id (Some variant_id)
generics
| _ -> raise (Failure "Unreachable")
in
assign_to_place config bottom_v p (cf Unit) ctx
- | _, V.Symbolic _ ->
+ | _, VSymbolic _ ->
assert (config.mode = SymbolicMode);
(* This is a bit annoying: in theory we should expand the symbolic value
* then set the discriminant, because in the case the discriminant is
@@ -273,8 +273,8 @@ let set_discriminant (config : C.config) (p : E.place)
* setting a discriminant should only be used to initialize a value,
* or reset an already initialized value, really. *)
raise (Failure "Unexpected value")
- | _, (V.VAdt _ | V.Bottom) -> raise (Failure "Inconsistent state")
- | _, (V.VLiteral _ | V.Borrow _ | V.Loan _) ->
+ | _, (VAdt _ | VBottom) -> raise (Failure "Inconsistent state")
+ | _, (VLiteral _ | VBorrow _ | VLoan _) ->
raise (Failure "Unexpected value")
in
(* Compose and apply *)
@@ -817,7 +817,7 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
in
(* Compose the continuations *)
cf_branch cf ctx
- | V.Symbolic sv ->
+ | VSymbolic sv ->
(* Expand the symbolic boolean, and continue by evaluating
* the branches *)
let cf_true : st_cm_fun = eval_statement config st1 in
@@ -848,7 +848,7 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
in
(* Compose *)
cf_eval_branch cf ctx
- | V.Symbolic sv ->
+ | VSymbolic sv ->
(* Expand the symbolic value and continue by evaluating the
* proper branches *)
let stgts =
@@ -891,14 +891,14 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
let p_v = value_strip_shared_loans p_v in
(* Match *)
match p_v.value with
- | V.VAdt adt -> (
+ | VAdt adt -> (
(* Evaluate the discriminant *)
let dv = Option.get adt.variant_id in
(* Find the branch, evaluate and continue *)
match List.find_opt (fun (svl, _) -> List.mem dv svl) stgts with
| None -> eval_statement config otherwise cf ctx
| Some (_, tgt) -> eval_statement config tgt cf ctx)
- | V.Symbolic sv ->
+ | VSymbolic sv ->
(* Expand the symbolic value - may lead to branching *)
let cf_expand =
expand_symbolic_adt config sv (Some (S.mk_mplace p ctx))
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 6f62b577..60747b2a 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -90,7 +90,7 @@ let mk_fresh_symbolic_typed_value (sv_kind : V.sv_kind) (rty : T.ty) :
let ty = Subst.erase_regions rty in
(* Generate the fresh a symbolic value *)
let value = mk_fresh_symbolic_value sv_kind rty in
- let value = V.Symbolic value in
+ let value = V.VSymbolic value in
{ V.value; V.ty }
let mk_fresh_symbolic_typed_value_from_no_regions_ty (sv_kind : V.sv_kind)
@@ -101,7 +101,7 @@ let mk_fresh_symbolic_typed_value_from_no_regions_ty (sv_kind : V.sv_kind)
(** Create a typed value from a symbolic value. *)
let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
V.typed_value =
- let av = V.Symbolic svalue in
+ let av = V.VSymbolic svalue in
let av : V.typed_value =
{ V.value = av; V.ty = Subst.erase_regions svalue.V.sv_ty }
in
@@ -204,7 +204,7 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
object
inherit [_] C.iter_eval_ctx as super
- method! visit_Symbolic _ sv =
+ method! visit_VSymbolic _ sv =
if sv.V.sv_id = sv_id then raise Found else ()
method! visit_aproj env aproj =
@@ -251,7 +251,7 @@ let bottom_in_value (ended_regions : T.RegionId.Set.t) (v : V.typed_value) :
let obj =
object
inherit [_] V.iter_typed_value
- method! visit_Bottom _ = raise Found
+ method! visit_VBottom _ = raise Found
method! visit_symbolic_value _ s =
if symbolic_value_has_ended_regions ended_regions s then raise Found
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 8895bd8e..7830099f 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -150,8 +150,8 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
(* Register the loan *)
let _ =
match lc with
- | V.SharedLoan (bids, _) -> register_shared_loan inside_abs bids
- | V.MutLoan bid -> register_mut_loan inside_abs bid
+ | VSharedLoan (bids, _) -> register_shared_loan inside_abs bids
+ | VMutLoan bid -> register_mut_loan inside_abs bid
in
(* Continue exploring *)
super#visit_loan_content inside_abs lc
@@ -159,14 +159,14 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
method! visit_aloan_content inside_abs lc =
let _ =
match lc with
- | V.AMutLoan (bid, _) -> register_mut_loan inside_abs bid
- | V.ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids
- | V.AIgnoredMutLoan (Some bid, _) -> register_ignored_loan T.Mut bid
- | V.AIgnoredMutLoan (None, _)
- | V.AIgnoredSharedLoan _
- | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
- | V.AEndedSharedLoan (_, _)
- | V.AEndedIgnoredMutLoan
+ | AMutLoan (bid, _) -> register_mut_loan inside_abs bid
+ | ASharedLoan (bids, _, _) -> register_shared_loan inside_abs bids
+ | AIgnoredMutLoan (Some bid, _) -> register_ignored_loan T.Mut bid
+ | AIgnoredMutLoan (None, _)
+ | AIgnoredSharedLoan _
+ | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
+ | AEndedSharedLoan (_, _)
+ | AEndedIgnoredMutLoan
{ given_back = _; child = _; given_back_meta = _ } ->
(* Do nothing *)
()
@@ -244,9 +244,9 @@ 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.MutBorrow (bid, _) -> register_borrow Mut bid
- | V.ReservedMutBorrow bid -> register_borrow Reserved bid
+ | VSharedBorrow bid -> register_borrow Shared bid
+ | VMutBorrow (bid, _) -> register_borrow Mut bid
+ | VReservedMutBorrow bid -> register_borrow Reserved bid
in
(* Continue exploring *)
super#visit_borrow_content env bc
@@ -254,12 +254,12 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
method! visit_aborrow_content env bc =
let _ =
match bc with
- | V.AMutBorrow (bid, _) -> register_borrow Mut bid
- | V.ASharedBorrow bid -> register_borrow Shared bid
- | V.AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid
- | V.AIgnoredMutBorrow (None, _)
- | V.AEndedMutBorrow _ | V.AEndedIgnoredMutBorrow _
- | V.AEndedSharedBorrow | V.AProjSharedBorrow _ ->
+ | AMutBorrow (bid, _) -> register_borrow Mut bid
+ | ASharedBorrow bid -> register_borrow Shared bid
+ | AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid
+ | AIgnoredMutBorrow (None, _)
+ | AEndedMutBorrow _ | AEndedIgnoredMutBorrow _ | AEndedSharedBorrow
+ | AProjSharedBorrow _ ->
(* Do nothing *)
()
in
@@ -305,7 +305,7 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
object
inherit [_] C.iter_eval_ctx as super
- method! visit_Bottom info =
+ method! visit_VBottom info =
(* No ⊥ inside borrowed values *)
assert (Config.allow_bottom_below_borrow || not info.outer_borrow)
@@ -317,8 +317,8 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
(* Update the info *)
let info =
match lc with
- | V.SharedLoan (_, _) -> set_outer_shared info
- | V.MutLoan _ ->
+ | VSharedLoan (_, _) -> set_outer_shared info
+ | VMutLoan _ ->
(* No mutable loan inside a shared loan *)
assert (not info.outer_shared);
set_outer_mut info
@@ -330,11 +330,11 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
(* Update the info *)
let info =
match bc with
- | V.SharedBorrow _ -> set_outer_shared info
- | V.ReservedMutBorrow _ ->
+ | VSharedBorrow _ -> set_outer_shared info
+ | VReservedMutBorrow _ ->
assert (not info.outer_borrow);
set_outer_shared info
- | V.MutBorrow (_, _) -> set_outer_mut info
+ | VMutBorrow (_, _) -> set_outer_mut info
in
(* Continue exploring *)
super#visit_borrow_content info bc
@@ -343,17 +343,16 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
(* Update the info *)
let info =
match lc with
- | V.AMutLoan (_, _) -> set_outer_mut info
- | V.ASharedLoan (_, _, _) -> set_outer_shared info
- | V.AEndedMutLoan { given_back = _; child = _; given_back_meta = _ }
- ->
+ | AMutLoan (_, _) -> set_outer_mut info
+ | ASharedLoan (_, _, _) -> set_outer_shared info
+ | AEndedMutLoan { given_back = _; child = _; given_back_meta = _ } ->
set_outer_mut info
- | V.AEndedSharedLoan (_, _) -> set_outer_shared info
- | V.AIgnoredMutLoan (_, _) -> set_outer_mut info
- | V.AEndedIgnoredMutLoan
+ | AEndedSharedLoan (_, _) -> set_outer_shared info
+ | AIgnoredMutLoan (_, _) -> set_outer_mut info
+ | AEndedIgnoredMutLoan
{ given_back = _; child = _; given_back_meta = _ } ->
set_outer_mut info
- | V.AIgnoredSharedLoan _ -> set_outer_shared info
+ | AIgnoredSharedLoan _ -> set_outer_shared info
in
(* Continue exploring *)
super#visit_aloan_content info lc
@@ -362,12 +361,12 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
(* Update the info *)
let info =
match bc with
- | V.AMutBorrow (_, _) -> set_outer_mut info
- | V.ASharedBorrow _ | V.AEndedSharedBorrow -> set_outer_shared info
- | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _
- | V.AEndedIgnoredMutBorrow _ ->
+ | AMutBorrow (_, _) -> set_outer_mut info
+ | ASharedBorrow _ | AEndedSharedBorrow -> set_outer_shared info
+ | AIgnoredMutBorrow _ | AEndedMutBorrow _ | AEndedIgnoredMutBorrow _
+ ->
set_outer_mut info
- | V.AProjSharedBorrow _ -> set_outer_shared info
+ | AProjSharedBorrow _ -> set_outer_shared info
in
(* Continue exploring *)
super#visit_aborrow_content info bc
@@ -416,10 +415,10 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
(* Check that the types have erased regions *)
assert (ty_is_ety tv.ty);
(* Check the current pair (value, type) *)
- (match (tv.V.value, tv.V.ty) with
- | V.VLiteral cv, T.TLiteral ty -> check_literal_type cv ty
+ (match (tv.value, tv.ty) with
+ | VLiteral cv, TLiteral ty -> check_literal_type cv ty
(* ADT case *)
- | V.VAdt av, T.TAdt (T.TAdtId def_id, generics) ->
+ | VAdt av, TAdt (TAdtId def_id, generics) ->
(* Retrieve the definition to check the variant id, the number of
* parameters, etc. *)
let def = C.ctx_lookup_type_decl ctx def_id in
@@ -428,53 +427,51 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
List.length generics.regions = List.length def.generics.regions);
assert (List.length generics.types = List.length def.generics.types);
(* Check that the variant id is consistent *)
- (match (av.V.variant_id, def.T.kind) with
- | Some variant_id, T.Enum variants ->
+ (match (av.variant_id, def.kind) with
+ | Some variant_id, Enum variants ->
assert (T.VariantId.to_int variant_id < List.length variants)
- | None, T.Struct _ -> ()
+ | None, Struct _ -> ()
| _ -> raise (Failure "Erroneous typing"));
(* Check that the field types are correct *)
let field_types =
- Assoc.type_decl_get_inst_norm_field_etypes ctx def av.V.variant_id
+ Assoc.type_decl_get_inst_norm_field_etypes ctx def av.variant_id
generics
in
- let fields_with_types =
- List.combine av.V.field_values field_types
- in
+ let fields_with_types = List.combine av.field_values field_types in
List.iter
- (fun ((v, ty) : V.typed_value * T.ty) -> assert (v.V.ty = ty))
+ (fun ((v, ty) : V.typed_value * T.ty) -> assert (v.ty = ty))
fields_with_types
(* Tuple case *)
- | V.VAdt av, T.TAdt (T.TTuple, generics) ->
+ | VAdt av, TAdt (TTuple, generics) ->
assert (generics.regions = []);
assert (generics.const_generics = []);
- assert (av.V.variant_id = None);
+ assert (av.variant_id = None);
(* Check that the fields have the proper values - and check that there
* are as many fields as field types at the same time *)
let fields_with_types =
- List.combine av.V.field_values generics.types
+ List.combine av.field_values generics.types
in
List.iter
- (fun ((v, ty) : V.typed_value * T.ty) -> assert (v.V.ty = ty))
+ (fun ((v, ty) : V.typed_value * T.ty) -> assert (v.ty = ty))
fields_with_types
(* Assumed type case *)
- | V.VAdt av, T.TAdt (T.TAssumed aty_id, generics) -> (
- assert (av.V.variant_id = None);
+ | VAdt av, TAdt (TAssumed aty_id, generics) -> (
+ assert (av.variant_id = None);
match
( aty_id,
- av.V.field_values,
+ av.field_values,
generics.regions,
generics.types,
generics.const_generics )
with
(* Box *)
- | T.TBox, [ inner_value ], [], [ inner_ty ], [] ->
- assert (inner_value.V.ty = inner_ty)
- | T.TArray, inner_values, _, [ inner_ty ], [ cg ] ->
+ | TBox, [ inner_value ], [], [ inner_ty ], [] ->
+ assert (inner_value.ty = inner_ty)
+ | TArray, inner_values, _, [ inner_ty ], [ cg ] ->
(* *)
assert (
List.for_all
- (fun (v : V.typed_value) -> v.V.ty = inner_ty)
+ (fun (v : V.typed_value) -> v.ty = inner_ty)
inner_values);
(* The length is necessarily concrete *)
let len =
@@ -483,37 +480,37 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
.value
in
assert (Z.of_int (List.length inner_values) = len)
- | (T.TSlice | T.TStr), _, _, _, _ -> raise (Failure "Unexpected")
+ | (TSlice | TStr), _, _, _, _ -> raise (Failure "Unexpected")
| _ -> raise (Failure "Erroneous type"))
- | V.Bottom, _ -> (* Nothing to check *) ()
- | V.Borrow bc, T.TRef (_, ref_ty, rkind) -> (
+ | VBottom, _ -> (* Nothing to check *) ()
+ | VBorrow bc, TRef (_, ref_ty, rkind) -> (
match (bc, rkind) with
- | V.SharedBorrow bid, T.Shared | V.ReservedMutBorrow bid, T.Mut -> (
+ | VSharedBorrow bid, Shared | VReservedMutBorrow bid, Mut -> (
(* Lookup the borrowed value to check it has the proper type *)
let _, glc = lookup_loan ek_all bid ctx in
match glc with
- | Concrete (V.SharedLoan (_, sv))
- | Abstract (V.ASharedLoan (_, sv, _)) ->
- assert (sv.V.ty = ref_ty)
+ | Concrete (VSharedLoan (_, sv))
+ | Abstract (ASharedLoan (_, sv, _)) ->
+ assert (sv.ty = ref_ty)
| _ -> raise (Failure "Inconsistent context"))
- | V.MutBorrow (_, bv), T.Mut ->
+ | VMutBorrow (_, bv), Mut ->
assert (
(* Check that the borrowed value has the proper type *)
- bv.V.ty = ref_ty)
+ bv.ty = ref_ty)
| _ -> raise (Failure "Erroneous typing"))
- | V.Loan lc, ty -> (
+ | VLoan lc, ty -> (
match lc with
- | V.SharedLoan (_, sv) -> assert (sv.V.ty = ty)
- | V.MutLoan bid -> (
+ | VSharedLoan (_, sv) -> assert (sv.ty = ty)
+ | VMutLoan bid -> (
(* Lookup the borrowed value to check it has the proper type *)
let glc = lookup_borrow ek_all bid ctx in
match glc with
- | Concrete (V.MutBorrow (_, bv)) -> assert (bv.V.ty = ty)
- | Abstract (V.AMutBorrow (_, sv)) ->
- assert (Subst.erase_regions sv.V.ty = ty)
+ | Concrete (VMutBorrow (_, bv)) -> assert (bv.ty = ty)
+ | Abstract (AMutBorrow (_, sv)) ->
+ assert (Subst.erase_regions sv.ty = ty)
| _ -> raise (Failure "Inconsistent context")))
- | V.Symbolic sv, ty ->
- let ty' = Subst.erase_regions sv.V.sv_ty in
+ | VSymbolic sv, ty ->
+ let ty' = Subst.erase_regions sv.sv_ty in
assert (ty' = ty)
| _ -> raise (Failure "Erroneous typing"));
(* Continue exploring to inspect the subterms *)
@@ -531,9 +528,9 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
(* Check that the types have regions *)
assert (ty_is_rty atv.ty);
(* Check the current pair (value, type) *)
- (match (atv.V.value, atv.V.ty) with
+ (match (atv.value, atv.ty) with
(* ADT case *)
- | V.AAdt av, T.TAdt (T.TAdtId def_id, generics) ->
+ | AAdt av, TAdt (TAdtId def_id, generics) ->
(* Retrieve the definition to check the variant id, the number of
* parameters, etc. *)
let def = C.ctx_lookup_type_decl ctx def_id in
@@ -545,132 +542,126 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
List.length generics.const_generics
= List.length def.generics.const_generics);
(* Check that the variant id is consistent *)
- (match (av.V.variant_id, def.T.kind) with
- | Some variant_id, T.Enum variants ->
+ (match (av.variant_id, def.kind) with
+ | Some variant_id, Enum variants ->
assert (T.VariantId.to_int variant_id < List.length variants)
- | None, T.Struct _ -> ()
+ | None, Struct _ -> ()
| _ -> raise (Failure "Erroneous typing"));
(* Check that the field types are correct *)
let field_types =
- Assoc.type_decl_get_inst_norm_field_rtypes ctx def av.V.variant_id
+ Assoc.type_decl_get_inst_norm_field_rtypes ctx def av.variant_id
generics
in
- let fields_with_types =
- List.combine av.V.field_values field_types
- in
+ let fields_with_types = List.combine av.field_values field_types in
List.iter
- (fun ((v, ty) : V.typed_avalue * T.ty) -> assert (v.V.ty = ty))
+ (fun ((v, ty) : V.typed_avalue * T.ty) -> assert (v.ty = ty))
fields_with_types
(* Tuple case *)
- | V.AAdt av, T.TAdt (T.TTuple, generics) ->
+ | AAdt av, TAdt (TTuple, generics) ->
assert (generics.regions = []);
assert (generics.const_generics = []);
- assert (av.V.variant_id = None);
+ assert (av.variant_id = None);
(* Check that the fields have the proper values - and check that there
* are as many fields as field types at the same time *)
let fields_with_types =
- List.combine av.V.field_values generics.types
+ List.combine av.field_values generics.types
in
List.iter
- (fun ((v, ty) : V.typed_avalue * T.ty) -> assert (v.V.ty = ty))
+ (fun ((v, ty) : V.typed_avalue * T.ty) -> assert (v.ty = ty))
fields_with_types
(* Assumed type case *)
- | V.AAdt av, T.TAdt (T.TAssumed aty_id, generics) -> (
- assert (av.V.variant_id = None);
+ | AAdt av, TAdt (TAssumed aty_id, generics) -> (
+ assert (av.variant_id = None);
match
( aty_id,
- av.V.field_values,
+ av.field_values,
generics.regions,
generics.types,
generics.const_generics )
with
(* Box *)
- | T.TBox, [ boxed_value ], [], [ boxed_ty ], [] ->
- assert (boxed_value.V.ty = boxed_ty)
+ | TBox, [ boxed_value ], [], [ boxed_ty ], [] ->
+ assert (boxed_value.ty = boxed_ty)
| _ -> raise (Failure "Erroneous type"))
- | V.ABottom, _ -> (* Nothing to check *) ()
- | V.ABorrow bc, T.TRef (_, ref_ty, rkind) -> (
+ | ABottom, _ -> (* Nothing to check *) ()
+ | ABorrow bc, TRef (_, ref_ty, rkind) -> (
match (bc, rkind) with
- | V.AMutBorrow (_, av), T.Mut ->
+ | AMutBorrow (_, av), Mut ->
(* Check that the child value has the proper type *)
- assert (av.V.ty = ref_ty)
- | V.ASharedBorrow bid, T.Shared -> (
+ assert (av.ty = ref_ty)
+ | ASharedBorrow bid, Shared -> (
(* Lookup the borrowed value to check it has the proper type *)
let _, glc = lookup_loan ek_all bid ctx in
match glc with
- | Concrete (V.SharedLoan (_, sv))
- | Abstract (V.ASharedLoan (_, sv, _)) ->
- assert (sv.V.ty = Subst.erase_regions ref_ty)
+ | Concrete (VSharedLoan (_, sv))
+ | Abstract (ASharedLoan (_, sv, _)) ->
+ assert (sv.ty = Subst.erase_regions ref_ty)
| _ -> raise (Failure "Inconsistent context"))
- | V.AIgnoredMutBorrow (_opt_bid, av), T.Mut ->
- assert (av.V.ty = ref_ty)
- | ( V.AEndedIgnoredMutBorrow
- { given_back; child; given_back_meta = _ },
- T.Mut ) ->
- assert (given_back.V.ty = ref_ty);
- assert (child.V.ty = ref_ty)
- | V.AProjSharedBorrow _, T.Shared -> ()
+ | AIgnoredMutBorrow (_opt_bid, av), Mut -> assert (av.ty = ref_ty)
+ | ( AEndedIgnoredMutBorrow { given_back; child; given_back_meta = _ },
+ Mut ) ->
+ assert (given_back.ty = ref_ty);
+ assert (child.ty = ref_ty)
+ | AProjSharedBorrow _, Shared -> ()
| _ -> raise (Failure "Inconsistent context"))
- | V.ALoan lc, aty -> (
+ | ALoan lc, aty -> (
match lc with
- | V.AMutLoan (bid, child_av) | V.AIgnoredMutLoan (Some bid, child_av)
+ | AMutLoan (bid, child_av) | AIgnoredMutLoan (Some bid, child_av)
-> (
let borrowed_aty = aloan_get_expected_child_type aty in
- assert (child_av.V.ty = borrowed_aty);
+ assert (child_av.ty = borrowed_aty);
(* Lookup the borrowed value to check it has the proper type *)
let glc = lookup_borrow ek_all bid ctx in
match glc with
- | Concrete (V.MutBorrow (_, bv)) ->
- assert (bv.V.ty = Subst.erase_regions borrowed_aty)
- | Abstract (V.AMutBorrow (_, sv)) ->
+ | Concrete (VMutBorrow (_, bv)) ->
+ assert (bv.ty = Subst.erase_regions borrowed_aty)
+ | Abstract (AMutBorrow (_, sv)) ->
assert (
- Subst.erase_regions sv.V.ty
+ Subst.erase_regions sv.ty
= Subst.erase_regions borrowed_aty)
| _ -> raise (Failure "Inconsistent context"))
- | V.AIgnoredMutLoan (None, child_av) ->
+ | AIgnoredMutLoan (None, child_av) ->
let borrowed_aty = aloan_get_expected_child_type aty in
- assert (child_av.V.ty = borrowed_aty)
- | V.ASharedLoan (_, sv, child_av) | V.AEndedSharedLoan (sv, child_av)
- ->
+ assert (child_av.ty = borrowed_aty)
+ | ASharedLoan (_, sv, child_av) | AEndedSharedLoan (sv, child_av) ->
let borrowed_aty = aloan_get_expected_child_type aty in
- assert (sv.V.ty = Subst.erase_regions borrowed_aty);
+ assert (sv.ty = Subst.erase_regions borrowed_aty);
(* TODO: the type of aloans doesn't make sense, see above *)
- assert (child_av.V.ty = borrowed_aty)
- | V.AEndedMutLoan { given_back; child; given_back_meta = _ }
- | V.AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ }
- ->
+ assert (child_av.ty = borrowed_aty)
+ | AEndedMutLoan { given_back; child; given_back_meta = _ }
+ | AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ } ->
let borrowed_aty = aloan_get_expected_child_type aty in
- assert (given_back.V.ty = borrowed_aty);
- assert (child.V.ty = borrowed_aty)
- | V.AIgnoredSharedLoan child_av ->
- assert (child_av.V.ty = aloan_get_expected_child_type aty))
- | V.ASymbolic aproj, ty -> (
+ assert (given_back.ty = borrowed_aty);
+ assert (child.ty = borrowed_aty)
+ | AIgnoredSharedLoan child_av ->
+ assert (child_av.ty = aloan_get_expected_child_type aty))
+ | ASymbolic aproj, ty -> (
let ty1 = Subst.erase_regions ty in
match aproj with
- | V.AProjLoans (sv, _) ->
- let ty2 = Subst.erase_regions sv.V.sv_ty in
+ | AProjLoans (sv, _) ->
+ let ty2 = Subst.erase_regions sv.sv_ty in
assert (ty1 = ty2);
(* Also check that the symbolic values contain regions of interest -
* otherwise they should have been reduced to [_] *)
let abs = Option.get info in
- assert (ty_has_regions_in_set abs.regions sv.V.sv_ty)
- | V.AProjBorrows (sv, proj_ty) ->
- let ty2 = Subst.erase_regions sv.V.sv_ty in
+ assert (ty_has_regions_in_set abs.regions sv.sv_ty)
+ | AProjBorrows (sv, proj_ty) ->
+ let ty2 = Subst.erase_regions sv.sv_ty in
assert (ty1 = ty2);
(* Also check that the symbolic values contain regions of interest -
* otherwise they should have been reduced to [_] *)
let abs = Option.get info in
assert (ty_has_regions_in_set abs.regions proj_ty)
- | V.AEndedProjLoans (_msv, given_back_ls) ->
+ | AEndedProjLoans (_msv, given_back_ls) ->
List.iter
(fun (_, proj) ->
match proj with
| V.AProjBorrows (_sv, ty') -> assert (ty' = ty)
- | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows -> ()
+ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ()
| _ -> raise (Failure "Unexpected"))
given_back_ls
- | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows -> ())
- | V.AIgnored, _ -> ()
+ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ())
+ | AIgnored, _ -> ()
| _ ->
log#lerror
(lazy
@@ -757,7 +748,7 @@ let check_symbolic_values (ctx : C.eval_ctx) : unit =
object
inherit [_] C.iter_eval_ctx as super
method! visit_abs _ abs = super#visit_abs (Some abs) abs
- method! visit_Symbolic _ sv = add_env_sv sv
+ method! visit_VSymbolic _ sv = add_env_sv sv
method! visit_abstract_shared_borrow abs asb =
let abs = Option.get abs in
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 7494dc2a..28e940ba 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -73,10 +73,10 @@ module Values = struct
List.map (typed_value_to_string fmt) av.field_values
in
match v.ty with
- | T.TAdt (T.TTuple, _) ->
+ | TAdt (TTuple, _) ->
(* Tuple *)
"(" ^ String.concat ", " field_values ^ ")"
- | T.TAdt (T.TAdtId def_id, _) ->
+ | TAdt (TAdtId def_id, _) ->
(* "Regular" ADT *)
let adt_ident =
match av.variant_id with
@@ -98,7 +98,7 @@ module Values = struct
let field_values = String.concat " " field_values in
adt_ident ^ " { " ^ field_values ^ " }"
else adt_ident
- | T.TAdt (T.TAssumed aty, _) -> (
+ | TAdt (TAssumed aty, _) -> (
(* Assumed type *)
match (aty, field_values) with
| TBox, [ bv ] -> "@Box(" ^ bv ^ ")"
@@ -108,28 +108,29 @@ module Values = struct
| _ ->
raise (Failure ("Inconsistent value: " ^ V.show_typed_value v)))
| _ -> raise (Failure "Inconsistent typed value"))
- | Bottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty
- | Borrow bc -> borrow_content_to_string fmt bc
- | Loan lc -> loan_content_to_string fmt lc
- | Symbolic s -> symbolic_value_to_string ty_fmt s
+ | VBottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty
+ | VBorrow bc -> borrow_content_to_string fmt bc
+ | VLoan lc -> loan_content_to_string fmt lc
+ | VSymbolic s -> symbolic_value_to_string ty_fmt s
and borrow_content_to_string (fmt : value_formatter) (bc : V.borrow_content) :
string =
match bc with
- | SharedBorrow bid -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋"
- | MutBorrow (bid, tv) ->
+ | VSharedBorrow bid -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋"
+ | VMutBorrow (bid, tv) ->
"&mut@" ^ V.BorrowId.to_string bid ^ " ("
^ typed_value_to_string fmt tv
^ ")"
- | ReservedMutBorrow bid -> "⌊reserved_mut@" ^ V.BorrowId.to_string bid ^ "⌋"
+ | VReservedMutBorrow bid ->
+ "⌊reserved_mut@" ^ V.BorrowId.to_string bid ^ "⌋"
and loan_content_to_string (fmt : value_formatter) (lc : V.loan_content) :
string =
match lc with
- | SharedLoan (loans, v) ->
+ | VSharedLoan (loans, v) ->
let loans = V.BorrowId.Set.to_string None loans in
"@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string fmt v ^ ")"
- | MutLoan bid -> "⌊mut@" ^ V.BorrowId.to_string bid ^ "⌋"
+ | VMutLoan bid -> "⌊mut@" ^ V.BorrowId.to_string bid ^ "⌋"
let abstract_shared_borrow_to_string (fmt : value_formatter)
(abs : V.abstract_shared_borrow) : string =
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 60020d9a..258b1cf2 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1149,7 +1149,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
(* Translate the value *)
let value =
match v.value with
- | V.VLiteral cv -> { e = Const cv; ty }
+ | VLiteral cv -> { e = Const cv; ty }
| VAdt av -> (
let variant_id = av.variant_id in
let field_values = List.map translate av.field_values in
@@ -1173,27 +1173,27 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
let cons = { e = cons_e; ty = cons_ty } in
(* Apply the constructor *)
mk_apps cons field_values)
- | Bottom -> raise (Failure "Unreachable")
- | Loan lc -> (
+ | VBottom -> raise (Failure "Unreachable")
+ | VLoan lc -> (
match lc with
- | SharedLoan (_, v) -> translate v
- | MutLoan _ -> raise (Failure "Unreachable"))
- | Borrow bc -> (
+ | VSharedLoan (_, v) -> translate v
+ | VMutLoan _ -> raise (Failure "Unreachable"))
+ | VBorrow bc -> (
match bc with
- | V.SharedBorrow bid ->
+ | VSharedBorrow bid ->
(* Lookup the shared value in the context, and continue *)
let sv = InterpreterBorrowsCore.lookup_shared_value ectx bid in
translate sv
- | V.ReservedMutBorrow bid ->
+ | VReservedMutBorrow bid ->
(* Same as for shared borrows. However, note that we use reserved borrows
* only in *meta-data*: a value *actually used* in the translation can't come
* from an unpromoted reserved borrow *)
let sv = InterpreterBorrowsCore.lookup_shared_value ectx bid in
translate sv
- | V.MutBorrow (_, v) ->
+ | VMutBorrow (_, v) ->
(* Borrows are the identity in the extraction *)
translate v)
- | Symbolic sv -> symbolic_value_to_texpression ctx sv
+ | VSymbolic sv -> symbolic_value_to_texpression ctx sv
in
(* Debugging *)
log#ldebug
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 8526ea66..932530ff 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -115,10 +115,10 @@ type symbolic_value = {
and value =
| VLiteral of literal (** Non-symbolic primitive value *)
| VAdt of adt_value (** Enumerations and structures *)
- | Bottom (** No value (uninitialized or moved value) *)
- | Borrow of borrow_content (** A borrowed value *)
- | Loan of loan_content (** A loaned value *)
- | Symbolic of symbolic_value
+ | VBottom (** No value (uninitialized or moved value) *)
+ | VBorrow of borrow_content (** A borrowed value *)
+ | VLoan of loan_content (** A loaned value *)
+ | VSymbolic of symbolic_value
(** Borrow projector over a symbolic value.
Note that contrary to the abstraction-values case, symbolic values
@@ -132,9 +132,9 @@ and adt_value = {
}
and borrow_content =
- | SharedBorrow of borrow_id (** A shared borrow. *)
- | MutBorrow of borrow_id * typed_value (** A mutably borrowed value. *)
- | ReservedMutBorrow of borrow_id
+ | VSharedBorrow of borrow_id (** A shared borrow. *)
+ | VMutBorrow of borrow_id * typed_value (** A mutably borrowed value. *)
+ | VReservedMutBorrow of borrow_id
(** A reserved mut borrow.
This is used to model {{: https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html} two-phase borrows}.
@@ -172,8 +172,8 @@ and borrow_content =
*)
and loan_content =
- | SharedLoan of loan_id_set * typed_value
- | MutLoan of loan_id
+ | VSharedLoan of loan_id_set * typed_value
+ | VMutLoan of loan_id
(** "Regular" typed value (we map variables to typed values) *)
and typed_value = { value : value; ty : ty }
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 24485002..7880fc3a 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -21,7 +21,7 @@ let mk_typed_avalue (ty : ty) (value : avalue) : typed_avalue =
let mk_bottom (ty : ty) : typed_value =
assert (ty_is_ety ty);
- { value = Bottom; ty }
+ { value = VBottom; ty }
let mk_abottom (ty : ty) : typed_avalue =
assert (ty_is_rty ty);
@@ -32,7 +32,7 @@ let mk_aignored (ty : ty) : typed_avalue =
{ value = AIgnored; ty }
let value_as_symbolic (v : value) : symbolic_value =
- match v with Symbolic v -> v | _ -> raise (Failure "Unexpected")
+ match v with VSymbolic v -> v | _ -> raise (Failure "Unexpected")
(** Box a value *)
let mk_box_value (v : typed_value) : typed_value =
@@ -40,20 +40,20 @@ let mk_box_value (v : typed_value) : typed_value =
let box_v = VAdt { variant_id = None; field_values = [ v ] } in
mk_typed_value box_ty box_v
-let is_bottom (v : value) : bool = match v with Bottom -> true | _ -> false
+let is_bottom (v : value) : bool = match v with VBottom -> true | _ -> false
let is_aignored (v : avalue) : bool =
match v with AIgnored -> true | _ -> false
let is_symbolic (v : value) : bool =
- match v with Symbolic _ -> true | _ -> false
+ match v with VSymbolic _ -> true | _ -> false
let as_symbolic (v : value) : symbolic_value =
- match v with Symbolic s -> s | _ -> raise (Failure "Unexpected")
+ match v with VSymbolic s -> s | _ -> raise (Failure "Unexpected")
let as_mut_borrow (v : typed_value) : BorrowId.id * typed_value =
match v.value with
- | Borrow (MutBorrow (bid, bv)) -> (bid, bv)
+ | VBorrow (VMutBorrow (bid, bv)) -> (bid, bv)
| _ -> raise (Failure "Unexpected")
let is_unit (v : typed_value) : bool =
@@ -86,7 +86,7 @@ let reserved_in_value (v : typed_value) : bool =
let obj =
object
inherit [_] iter_typed_value
- method! visit_ReservedMutBorrow _env _ = raise Found
+ method! visit_VReservedMutBorrow _env _ = raise Found
end
in
(* We use exceptions *)
@@ -151,7 +151,7 @@ let find_first_primitively_copyable_sv_with_borrows (type_infos : TA.type_infos)
object
inherit [_] iter_typed_value
- method! visit_Symbolic _ sv =
+ method! visit_VSymbolic _ sv =
let ty = sv.sv_ty in
if ty_is_primitively_copyable ty && ty_has_borrows type_infos ty then
raise (FoundSymbolicValue sv)
@@ -171,7 +171,7 @@ let find_first_primitively_copyable_sv_with_borrows (type_infos : TA.type_infos)
*)
let rec value_strip_shared_loans (v : typed_value) : typed_value =
match v.value with
- | Loan (SharedLoan (_, v')) -> value_strip_shared_loans v'
+ | VLoan (VSharedLoan (_, v')) -> value_strip_shared_loans v'
| _ -> v
(** Check if a symbolic value has borrows *)
@@ -251,7 +251,7 @@ let value_remove_shared_loans (v : typed_value) : typed_value =
method! visit_typed_value env v =
match v.value with
- | Loan (SharedLoan (_, sv)) -> self#visit_typed_value env sv
+ | VLoan (VSharedLoan (_, sv)) -> self#visit_typed_value env sv
| _ -> super#visit_typed_value env v
end
in
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 16:09:40 +0000