summaryrefslogtreecommitdiff
path: root/compiler/InterpreterPaths.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/InterpreterPaths.ml')
-rw-r--r--compiler/InterpreterPaths.ml258
1 files changed, 124 insertions, 134 deletions
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 2a277c91..729a3577 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -1,10 +1,7 @@
-module T = Types
-module V = Values
-module E = Expressions
-module C = Contexts
-module Subst = Substitute
-module Assoc = AssociatedTypes
-module L = Logging
+open Types
+open Values
+open Expressions
+open Contexts
open Cps
open ValuesUtils
open InterpreterUtils
@@ -14,7 +11,7 @@ open InterpreterExpansion
module Synth = SynthesizeSymbolic
(** The local logger *)
-let log = L.paths_log
+let log = Logging.paths_log
(** Paths *)
@@ -25,26 +22,26 @@ let log = L.paths_log
TODO: compare with borrow_lres?
*)
type path_fail_kind =
- | FailSharedLoan of V.BorrowId.Set.t
+ | FailSharedLoan of BorrowId.Set.t
(** Failure because we couldn't go inside a shared loan *)
- | FailMutLoan of V.BorrowId.id
+ | FailMutLoan of BorrowId.id
(** Failure because we couldn't go inside a mutable loan *)
- | FailReservedMutBorrow of V.BorrowId.id
+ | FailReservedMutBorrow of BorrowId.id
(** Failure because we couldn't go inside a reserved mutable borrow
(which should get activated) *)
- | FailSymbolic of int * V.symbolic_value
+ | FailSymbolic of int * symbolic_value
(** Failure because we need to enter a symbolic value (and thus need to
expand it).
We return the number of elements which remained in the path when we
reached the error - this allows to retrieve the path prefix, which
is useful for the synthesis. *)
- | FailBottom of int * E.projection_elem * T.ety
+ | FailBottom of int * projection_elem * ety
(** Failure because we need to enter an any value - we can expand Bottom
values if they are left values. We return the number of elements which
remained in the path when we reached the error - this allows to
properly update the Bottom value, if needs be.
*)
- | FailBorrow of V.borrow_content
+ | FailBorrow of borrow_content
(** We got stuck because we couldn't enter a borrow *)
[@@deriving show]
@@ -56,7 +53,7 @@ type path_fail_kind =
type 'a path_access_result = ('a, path_fail_kind) result
(** The result of reading from/writing to a place *)
-type updated_read_value = { read : V.typed_value; updated : V.typed_value }
+type updated_read_value = { read : typed_value; updated : typed_value }
type projection_access = {
enter_shared_loans : bool;
@@ -71,10 +68,10 @@ type projection_access = {
TODO: use exceptions?
*)
-let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
+let rec access_projection (access : projection_access) (ctx : eval_ctx)
(* Function to (eventually) update the value we find *)
- (update : V.typed_value -> V.typed_value) (p : E.projection)
- (v : V.typed_value) : (C.eval_ctx * updated_read_value) path_access_result =
+ (update : typed_value -> typed_value) (p : projection) (v : typed_value) :
+ (eval_ctx * updated_read_value) path_access_result =
(* For looking up/updating shared loans *)
let ek : exploration_kind =
{ enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
@@ -86,8 +83,8 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
if nv.ty <> v.ty then (
log#lerror
(lazy
- ("Not the same type:\n- nv.ty: " ^ T.show_ety nv.ty ^ "\n- v.ty: "
- ^ T.show_ety v.ty));
+ ("Not the same type:\n- nv.ty: " ^ show_ety nv.ty ^ "\n- v.ty: "
+ ^ show_ety v.ty));
raise
(Failure
"Assertion failed: new value doesn't have the same type as its \
@@ -95,55 +92,55 @@ 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.Adt adt,
- T.Adt (type_id, _) ) -> (
+ VAdt adt,
+ TAdt (type_id, _) ) -> (
(* Check consistency *)
(match (proj_kind, type_id) with
- | ProjAdt (def_id, opt_variant_id), T.AdtId 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"));
(* Actually project *)
- let fv = T.FieldId.nth adt.field_values field_id in
+ let fv = FieldId.nth adt.field_values field_id in
match access_projection access ctx update p' fv with
| Error err -> Error err
| Ok (ctx, res) ->
(* Update the field value *)
let nvalues =
- T.FieldId.update_nth adt.field_values field_id res.updated
+ FieldId.update_nth adt.field_values field_id res.updated
in
- let nadt = V.Adt { adt with V.field_values = nvalues } in
+ let nadt = 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.Adt adt, T.Adt (T.Tuple, _) -> (
+ | 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
+ let fv = FieldId.nth adt.field_values field_id in
(* Project *)
match access_projection access ctx update p' fv with
| Error err -> Error err
| Ok (ctx, res) ->
(* Update the field value *)
let nvalues =
- T.FieldId.update_nth adt.field_values field_id res.updated
+ FieldId.update_nth adt.field_values field_id res.updated
in
- let ntuple = V.Adt { adt with field_values = nvalues } in
+ let ntuple = VAdt { adt with field_values = nvalues } in
let updated = { v with value = ntuple } in
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,
- Adt { variant_id = None; field_values = [ bv ] },
- T.Adt (T.Assumed T.Box, _) ) -> (
+ VAdt { variant_id = None; field_values = [ bv ] },
+ 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 +153,20 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
{
v with
value =
- V.Adt { 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 +175,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 +199,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,18 +235,15 @@ 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.Literal _ | V.Adt _ | 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
- let ty = "- ty:\n" ^ T.show_ety ty in
+ let pe = "- pe: " ^ show_projection_elem pe in
+ let v = "- v:\n" ^ show_value v in
+ let ty = "- ty:\n" ^ show_ety ty in
log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty);
raise (Failure "Inconsistent projection"))
@@ -264,16 +255,16 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
*)
let access_place (access : projection_access)
(* Function to (eventually) update the value we find *)
- (update : V.typed_value -> V.typed_value) (p : E.place) (ctx : C.eval_ctx)
- : (C.eval_ctx * V.typed_value) path_access_result =
+ (update : typed_value -> typed_value) (p : place) (ctx : eval_ctx) :
+ (eval_ctx * typed_value) path_access_result =
(* Lookup the variable's value *)
- let value = C.ctx_lookup_var_value ctx p.var_id in
+ let value = ctx_lookup_var_value ctx p.var_id in
(* Apply the projection *)
match access_projection access ctx update p.projection value with
| Error err -> Error err
| Ok (ctx, res) ->
(* Update the value *)
- let ctx = C.ctx_update_var_value ctx p.var_id res.updated in
+ let ctx = ctx_update_var_value ctx p.var_id res.updated in
(* Return *)
Ok (ctx, res.read)
@@ -309,8 +300,8 @@ let access_kind_to_projection_access (access : access_kind) : projection_access
Note that we only access the value at the place, and do not check that
the value is "well-formed" (for instance that it doesn't contain bottoms).
*)
-let try_read_place (access : access_kind) (p : E.place) (ctx : C.eval_ctx) :
- V.typed_value path_access_result =
+let try_read_place (access : access_kind) (p : place) (ctx : eval_ctx) :
+ typed_value path_access_result =
let access = access_kind_to_projection_access access in
(* The update function is the identity *)
let update v = v in
@@ -324,22 +315,21 @@ let try_read_place (access : access_kind) (p : E.place) (ctx : C.eval_ctx) :
if ctx1 <> ctx then (
let msg =
"Unexpected environment update:\nNew environment:\n"
- ^ C.show_env ctx1.env ^ "\n\nOld environment:\n"
- ^ C.show_env ctx.env
+ ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env
in
log#serror msg;
raise (Failure "Unexpected environment update"));
Ok read_value
-let read_place (access : access_kind) (p : E.place) (ctx : C.eval_ctx) :
- V.typed_value =
+let read_place (access : access_kind) (p : place) (ctx : eval_ctx) : typed_value
+ =
match try_read_place access p ctx with
| Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e))
| Ok v -> v
(** Attempt to update the value at a given place *)
-let try_write_place (access : access_kind) (p : E.place) (nv : V.typed_value)
- (ctx : C.eval_ctx) : C.eval_ctx path_access_result =
+let try_write_place (access : access_kind) (p : place) (nv : typed_value)
+ (ctx : eval_ctx) : eval_ctx path_access_result =
let access = access_kind_to_projection_access access in
(* The update function substitutes the value with the new value *)
let update _ = nv in
@@ -349,41 +339,42 @@ let try_write_place (access : access_kind) (p : E.place) (nv : V.typed_value)
(* We ignore the read value *)
Ok ctx
-let write_place (access : access_kind) (p : E.place) (nv : V.typed_value)
- (ctx : C.eval_ctx) : C.eval_ctx =
+let write_place (access : access_kind) (p : place) (nv : typed_value)
+ (ctx : eval_ctx) : eval_ctx =
match try_write_place access p nv ctx with
| Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e))
| Ok ctx -> ctx
-let compute_expanded_bottom_adt_value (ctx : C.eval_ctx)
- (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
- (generics : T.egeneric_args) : V.typed_value =
+let compute_expanded_bottom_adt_value (ctx : eval_ctx) (def_id : TypeDeclId.id)
+ (opt_variant_id : VariantId.id option) (generics : generic_args) :
+ typed_value =
+ assert (TypesUtils.generic_args_only_erased_regions generics);
(* Lookup the definition and check if it is an enumeration - it
should be an enumeration if and only if the projection element
is a field projection with *some* variant id. Retrieve the list
of fields at the same time. *)
- let def = C.ctx_lookup_type_decl ctx def_id in
- assert (List.length generics.regions = List.length def.T.generics.regions);
+ let def = ctx_lookup_type_decl ctx def_id in
+ assert (List.length generics.regions = List.length def.generics.regions);
(* Compute the field types *)
let field_types =
- Assoc.type_decl_get_inst_norm_field_etypes ctx def opt_variant_id generics
+ AssociatedTypes.type_decl_get_inst_norm_field_etypes ctx def opt_variant_id
+ generics
in
(* Initialize the expanded value *)
let fields = List.map mk_bottom field_types in
- let av = V.Adt { variant_id = opt_variant_id; field_values = fields } in
- let ty = T.Adt (T.AdtId def_id, generics) in
- { V.value = av; V.ty }
+ let av = VAdt { variant_id = opt_variant_id; field_values = fields } in
+ let ty = TAdt (TAdtId def_id, generics) in
+ { value = av; ty }
-let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
- V.typed_value =
+let compute_expanded_bottom_tuple_value (field_types : ety list) : typed_value =
(* Generate the field values *)
let fields = List.map mk_bottom field_types in
- let v = V.Adt { variant_id = None; field_values = fields } in
+ let v = VAdt { variant_id = None; field_values = fields } in
let generics = TypesUtils.mk_generic_args [] field_types [] [] in
- let ty = T.Adt (T.Tuple, generics) in
- { V.value = v; V.ty }
+ let ty = TAdt (TTuple, generics) in
+ { value = v; ty }
-(** Auxiliary helper to expand {!V.Bottom} values.
+(** Auxiliary helper to expand {!Bottom} values.
During compilation, rustc desaggregates the ADT initializations. The
consequence is that the following rust code:
@@ -399,19 +390,19 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
]}
The consequence is that we may sometimes need to write fields to values
- which are currently {!V.Bottom}. When doing this, we first expand the value
+ which are currently {!Bottom}. When doing this, we first expand the value
to, say, [Cons Bottom Bottom] (note that field projection contains information
about which variant we should project to, which is why we *can* set the
variant index when writing one of its fields).
*)
-let expand_bottom_value_from_projection (access : access_kind) (p : E.place)
- (remaining_pes : int) (pe : E.projection_elem) (ty : T.ety)
- (ctx : C.eval_ctx) : C.eval_ctx =
+let expand_bottom_value_from_projection (access : access_kind) (p : place)
+ (remaining_pes : int) (pe : projection_elem) (ty : ety) (ctx : eval_ctx) :
+ eval_ctx =
(* Debugging *)
log#ldebug
(lazy
("expand_bottom_value_from_projection:\n" ^ "pe: "
- ^ E.show_projection_elem pe ^ "\n" ^ "ty: " ^ T.show_ety ty));
+ ^ show_projection_elem pe ^ "\n" ^ "ty: " ^ show_ety ty));
(* Prepare the update: we need to take the proper prefix of the place
during whose evaluation we got stuck *)
let projection' =
@@ -421,41 +412,40 @@ let expand_bottom_value_from_projection (access : access_kind) (p : E.place)
in
let p' = { p with projection = projection' } in
(* Compute the expanded value.
- The type of the {!V.Bottom} value should be a tuple or an ADT.
+ The type of the {!Bottom} value should be a tuple or an AD
Note that the projection element we got stuck at should be a
- field projection, and gives the variant id if the {!V.Bottom} value
+ field projection, and gives the variant id if the {!Bottom} value
is an enumeration value.
Also, the expanded value should be the proper ADT variant or a tuple
- with the proper arity, with all the fields initialized to {!V.Bottom}
+ with the proper arity, with all the fields initialized to {!Bottom}
*)
let nv =
match (pe, ty) with
(* "Regular" ADTs *)
| ( Field (ProjAdt (def_id, opt_variant_id), _),
- T.Adt (T.AdtId def_id', generics) ) ->
+ TAdt (TAdtId def_id', generics) ) ->
assert (def_id = def_id');
compute_expanded_bottom_adt_value ctx def_id opt_variant_id generics
(* Tuples *)
| ( Field (ProjTuple arity, _),
- T.Adt
- ( T.Tuple,
- { T.regions = []; types; const_generics = []; trait_refs = [] } ) )
- ->
+ TAdt
+ (TTuple, { regions = []; types; const_generics = []; trait_refs = [] })
+ ) ->
assert (arity = List.length types);
(* Generate the field values *)
compute_expanded_bottom_tuple_value types
| _ ->
raise
(Failure
- ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_ety ty))
+ ("Unreachable: " ^ show_projection_elem pe ^ ", " ^ show_ety ty))
in
(* Update the context by inserting the expanded value at the proper place *)
match try_write_place access p' nv ctx with
| Ok ctx -> ctx
| Error _ -> raise (Failure "Unreachable")
-let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
- (p : E.place) : cm_fun =
+let rec update_ctx_along_read_place (config : config) (access : access_kind)
+ (p : place) : cm_fun =
fun cf ctx ->
(* Attempt to read the place: if it fails, update the environment and retry *)
match try_read_place access p ctx with
@@ -476,14 +466,14 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
expand_symbolic_value_no_branching config sp
(Some (Synth.mk_mplace prefix ctx))
| FailBottom (_, _, _) ->
- (* We can't expand {!V.Bottom} values while reading them *)
+ (* We can't expand {!Bottom} values while reading them *)
raise (Failure "Found [Bottom] while reading a place")
| FailBorrow _ -> raise (Failure "Could not read a borrow")
in
comp cc (update_ctx_along_read_place config access p) cf ctx
-let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
- (p : E.place) : cm_fun =
+let rec update_ctx_along_write_place (config : config) (access : access_kind)
+ (p : place) : cm_fun =
fun cf ctx ->
(* Attempt to *read* (yes, *read*: we check the access to the place, and
write to it later) the place: if it fails, update the environment and retry *)
@@ -501,7 +491,7 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
expand_symbolic_value_no_branching config sp
(Some (Synth.mk_mplace p ctx))
| FailBottom (remaining_pes, pe, ty) ->
- (* Expand the {!V.Bottom} value *)
+ (* Expand the {!Bottom} value *)
fun cf ctx ->
let ctx =
expand_bottom_value_from_projection access p remaining_pes pe ty
@@ -516,8 +506,8 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
(** Small utility used to break control-flow *)
exception UpdateCtx of cm_fun
-let rec end_loans_at_place (config : C.config) (access : access_kind)
- (p : E.place) : cm_fun =
+let rec end_loans_at_place (config : config) (access : access_kind) (p : place)
+ : cm_fun =
fun cf ctx ->
(* Iterator to explore a value and update the context whenever we find
* loans.
@@ -526,28 +516,28 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
* *)
let obj =
object
- inherit [_] V.iter_typed_value as super
+ inherit [_] iter_typed_value as super
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)
@@ -571,20 +561,20 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
* a recursive call to reinspect the value *)
comp cc (end_loans_at_place config access p) cf ctx
-let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
+let drop_outer_loans_at_lplace (config : config) (p : place) : cm_fun =
fun cf ctx ->
(* Move the current value in the place outside of this place and into
* a dummy variable *)
let access = Write in
let v = read_place access p ctx in
- let ctx = write_place access p (mk_bottom v.V.ty) ctx in
- let dummy_id = C.fresh_dummy_var_id () in
- let ctx = C.ctx_push_dummy_var ctx dummy_id v in
+ let ctx = write_place access p (mk_bottom v.ty) ctx in
+ let dummy_id = fresh_dummy_var_id () in
+ let ctx = ctx_push_dummy_var ctx dummy_id v in
(* Auxiliary function *)
let rec drop : cm_fun =
fun cf ctx ->
(* Read the value *)
- let v = C.ctx_lookup_dummy_var ctx dummy_id in
+ let v = ctx_lookup_dummy_var ctx dummy_id in
(* Check if there are loans or borrows to end *)
let with_borrows = false in
match get_first_outer_loan_or_borrow_in_value with_borrows v with
@@ -595,8 +585,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 *)
@@ -608,7 +598,7 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
let cc =
comp cc (fun cf ctx ->
(* Pop *)
- let ctx, v = C.ctx_remove_dummy_var ctx dummy_id in
+ let ctx, v = ctx_remove_dummy_var ctx dummy_id in
(* Reinsert *)
let ctx = write_place access p v ctx in
(* Sanity check *)
@@ -619,8 +609,8 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
(* Continue *)
cc cf ctx
-let prepare_lplace (config : C.config) (p : E.place)
- (cf : V.typed_value -> m_fun) : m_fun =
+let prepare_lplace (config : config) (p : place) (cf : typed_value -> m_fun) :
+ m_fun =
fun ctx ->
log#ldebug
(lazy