summaryrefslogtreecommitdiff
path: root/compiler/InterpreterPaths.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/InterpreterPaths.ml')
-rw-r--r--compiler/InterpreterPaths.ml173
1 files changed, 84 insertions, 89 deletions
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 9158f2c1..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 \
@@ -106,30 +103,30 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
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.VAdt { adt with 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), 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.VAdt { 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
@@ -244,9 +241,9 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
else Error (FailSharedLoan bids))
| (_, (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"))
@@ -258,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)
@@ -303,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
@@ -318,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
@@ -343,42 +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.generic_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.VAdt { variant_id = opt_variant_id; field_values = fields } in
- let ty = T.TAdt (TAdtId 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.VAdt { 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.TAdt (TTuple, 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:
@@ -394,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' =
@@ -416,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.TAdt (TAdtId 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.TAdt
- ( TTuple,
- { 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
@@ -471,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 *)
@@ -496,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
@@ -511,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.
@@ -521,7 +516,7 @@ 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
@@ -566,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
@@ -603,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 *)
@@ -614,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
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 19:25:57 +0000