summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Driver.ml1
-rw-r--r--compiler/Interpreter.ml8
-rw-r--r--compiler/InterpreterBorrows.ml80
-rw-r--r--compiler/InterpreterBorrows.mli34
-rw-r--r--compiler/InterpreterBorrowsCore.ml17
-rw-r--r--compiler/InterpreterExpansion.ml66
-rw-r--r--compiler/InterpreterExpansion.mli73
-rw-r--r--compiler/InterpreterExpressions.ml126
-rw-r--r--compiler/InterpreterExpressions.mli37
-rw-r--r--compiler/InterpreterPaths.ml170
-rw-r--r--compiler/InterpreterPaths.mli105
-rw-r--r--compiler/InterpreterProjectors.ml54
-rw-r--r--compiler/InterpreterProjectors.mli115
-rw-r--r--compiler/InterpreterStatements.ml71
-rw-r--r--compiler/InterpreterStatements.mli63
-rw-r--r--compiler/Logging.ml3
16 files changed, 642 insertions, 381 deletions
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index bd9396c0..d19aca93 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -138,6 +138,7 @@ let () =
paths_log#set_level EL.Info;
expressions_log#set_level EL.Info;
expansion_log#set_level EL.Info;
+ projectors_log#set_level EL.Info;
borrows_log#set_level EL.Info;
invariants_log#set_level EL.Info;
pure_utils_log#set_level EL.Info;
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index cf40c5b8..d3b3c7e6 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -131,7 +131,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
let ret_inst_sg = instantiate_fun_sig type_params sg in
let ret_rty = ret_inst_sg.output in
(* Move the return value out of the return variable *)
- let cf_pop_frame = ctx_pop_frame config in
+ let cf_pop_frame = pop_frame config in
(* We need to find the parents regions/abstractions of the region we
* will end - this will allow us to, first, mark the other return
@@ -191,7 +191,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
let target_abs_ids = List.append parent_input_abs_ids [ current_abs_id ] in
let cf_end_target_abs cf =
List.fold_left
- (fun cf id -> end_abstraction config [] id cf)
+ (fun cf id -> end_abstraction config id cf)
cf target_abs_ids
in
(* Generate the Return node *)
@@ -244,7 +244,7 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
| None ->
(* Forward translation *)
(* Pop the frame and retrieve the returned value at the same time*)
- let cf_pop = ctx_pop_frame config in
+ let cf_pop = pop_frame config in
(* Generate the Return node *)
let cf_return ret_value : m_fun =
fun _ -> Some (SA.Return (Some ret_value))
@@ -309,7 +309,7 @@ module Test = struct
match res with
| Return ->
(* Ok: drop the local variables and finish *)
- ctx_pop_frame config (fun _ _ -> None) ctx
+ pop_frame config (fun _ _ -> None) ctx
| _ ->
raise
(Failure
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 288ebc27..1b4907ac 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -12,21 +12,21 @@ open InterpreterBorrowsCore
open InterpreterProjectors
(** The local logger *)
-let log = InterpreterBorrowsCore.log
+let log = L.borrows_log
(** Auxiliary function to end borrows: lookup a borrow in the environment,
update it (by returning an updated environment where the borrow has been
replaced by {!V.Bottom})) if we can end the borrow (for instance, it is not
an outer borrow...) or return the reason why we couldn't update the borrow.
- [end_borrow] then simply performs a loop: as long as we need to end (outer)
+ [end_borrow_aux] then simply performs a loop: as long as we need to end (outer)
borrows, we end them, before finally ending the borrow we wanted to end in the
first place.
[allowed_abs]: if not [None], allows to get a borrow in the given
abstraction without ending the whole abstraction first. This parameter
- allows us to use {!end_borrow} as an auxiliary function for
- {!end_abstraction} (we end all the borrows in the abstraction one by one
+ allows us to use {!end_borrow_aux} as an auxiliary function for
+ {!end_abstraction_aux} (we end all the borrows in the abstraction one by one
before removing the abstraction from the context).
*)
let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
@@ -705,7 +705,7 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id)
assert !r;
{ ctx with env }
-(** Auxiliary function: see {!end_borrow} *)
+(** Auxiliary function: see {!end_borrow_aux} *)
let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
(ctx : C.eval_ctx) : C.eval_ctx =
(* Debug *)
@@ -796,8 +796,8 @@ let convert_avalue_to_given_back_value (abs_kind : V.abs_kind)
[allowed_abs]: see the comment for {!end_borrow_get_borrow}.
- [chain]: contains the list of borrows/abstraction ids on which {!end_borrow}
- and {!end_abstraction} were called, to remember the chain of calls. This is
+ [chain]: contains the list of borrows/abstraction ids on which {!end_borrow_aux}
+ and {!end_abstraction_aux} were called, to remember the chain of calls. This is
useful for debugging purposes, and also for sanity checks to detect cycles
(which shouldn't happen if the environment is well-formed).
@@ -809,12 +809,14 @@ let convert_avalue_to_given_back_value (abs_kind : V.abs_kind)
perform anything smart and is trusted, and another function for the
book-keeping.
*)
-let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids)
+let rec end_borrow_aux (config : C.config) (chain : borrow_or_abs_ids)
(allowed_abs : V.AbstractionId.id option) (l : V.BorrowId.id) : cm_fun =
fun cf ctx ->
(* Check that we don't loop *)
let chain0 = chain in
- let chain = add_borrow_or_abs_id_to_chain "end_borrow: " (BorrowId l) chain in
+ let chain =
+ add_borrow_or_abs_id_to_chain "end_borrow_aux: " (BorrowId l) chain
+ in
log#ldebug
(lazy
("end borrow: " ^ V.BorrowId.to_string l ^ ":\n- original context:\n"
@@ -884,22 +886,22 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids)
* inside another borrow *)
let allowed_abs' = None in
(* End the outer borrows *)
- let cc = end_borrows config chain allowed_abs' bids in
+ let cc = end_borrows_aux config chain allowed_abs' bids in
(* Retry to end the borrow *)
- let cc = comp cc (end_borrow config chain0 allowed_abs l) in
+ let cc = comp cc (end_borrow_aux config chain0 allowed_abs l) in
(* Check and apply *)
comp cc cf_check cf ctx
| OuterBorrows (Borrow bid) | InnerLoans (Borrow bid) ->
let allowed_abs' = None in
(* End the outer borrow *)
- let cc = end_borrow config chain allowed_abs' bid in
+ let cc = end_borrow_aux config chain allowed_abs' bid in
(* Retry to end the borrow *)
- let cc = comp cc (end_borrow config chain0 allowed_abs l) in
+ let cc = comp cc (end_borrow_aux config chain0 allowed_abs l) in
(* Check and apply *)
comp cc cf_check cf ctx
| OuterAbs abs_id ->
(* The borrow is inside an abstraction: end the whole abstraction *)
- let cf_end_abs = end_abstraction config chain abs_id in
+ let cf_end_abs = end_abstraction_aux config chain abs_id in
(* Compose with a sanity check *)
comp cf_end_abs cf_check cf ctx)
| Ok (ctx, None) ->
@@ -922,7 +924,7 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids)
(* Do a sanity check and continue *)
cf_check cf ctx
-and end_borrows (config : C.config) (chain : borrow_or_abs_ids)
+and end_borrows_aux (config : C.config) (chain : borrow_or_abs_ids)
(allowed_abs : V.AbstractionId.id option) (lset : V.BorrowId.Set.t) : cm_fun
=
fun cf ->
@@ -930,20 +932,22 @@ and end_borrows (config : C.config) (chain : borrow_or_abs_ids)
* so that we actually end from the smallest id to the highest id - just
* a matter of taste, and may make debugging easier *)
let ids = V.BorrowId.Set.fold (fun id ids -> id :: ids) lset [] in
- List.fold_left (fun cf id -> end_borrow config chain allowed_abs id cf) cf ids
+ List.fold_left
+ (fun cf id -> end_borrow_aux config chain allowed_abs id cf)
+ cf ids
-and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
+and end_abstraction_aux (config : C.config) (chain : borrow_or_abs_ids)
(abs_id : V.AbstractionId.id) : cm_fun =
fun cf ctx ->
(* Check that we don't loop *)
let chain =
- add_borrow_or_abs_id_to_chain "end_abstraction: " (AbsId abs_id) chain
+ add_borrow_or_abs_id_to_chain "end_abstraction_aux: " (AbsId abs_id) chain
in
(* Remember the original context for printing purposes *)
let ctx0 = ctx in
log#ldebug
(lazy
- ("end_abstraction: "
+ ("end_abstraction_aux: "
^ V.AbstractionId.to_string abs_id
^ "\n- original context:\n" ^ eval_ctx_to_string ctx0));
@@ -954,12 +958,12 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
assert abs.can_end;
(* End the parent abstractions first *)
- let cc = end_abstractions config chain abs.parents in
+ let cc = end_abstractions_aux config chain abs.parents in
let cc =
comp_unit cc (fun ctx ->
log#ldebug
(lazy
- ("end_abstraction: "
+ ("end_abstraction_aux: "
^ V.AbstractionId.to_string abs_id
^ "\n- context after parent abstractions ended:\n"
^ eval_ctx_to_string ctx)))
@@ -971,7 +975,7 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
comp_unit cc (fun ctx ->
log#ldebug
(lazy
- ("end_abstraction: "
+ ("end_abstraction_aux: "
^ V.AbstractionId.to_string abs_id
^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ctx)))
in
@@ -1000,7 +1004,7 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
comp_unit cc (fun ctx ->
log#ldebug
(lazy
- ("end_abstraction: "
+ ("end_abstraction_aux: "
^ V.AbstractionId.to_string abs_id
^ "\n- original context:\n" ^ eval_ctx_to_string ctx0
^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx)))
@@ -1012,14 +1016,16 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
(* Apply the continuation *)
cc cf ctx
-and end_abstractions (config : C.config) (chain : borrow_or_abs_ids)
+and end_abstractions_aux (config : C.config) (chain : borrow_or_abs_ids)
(abs_ids : V.AbstractionId.Set.t) : cm_fun =
fun cf ->
(* This is not necessary, but we prefer to reorder the abstraction ids,
* so that we actually end from the smallest id to the highest id - just
* a matter of taste, and may make debugging easier *)
let abs_ids = V.AbstractionId.Set.fold (fun id ids -> id :: ids) abs_ids [] in
- List.fold_left (fun cf id -> end_abstraction config chain id cf) cf abs_ids
+ List.fold_left
+ (fun cf id -> end_abstraction_aux config chain id cf)
+ cf abs_ids
and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids)
(abs_id : V.AbstractionId.id) : cm_fun =
@@ -1039,8 +1045,8 @@ and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids)
(* There are loans: end the corresponding borrows, then recheck *)
let cc : cm_fun =
match bids with
- | Borrow bid -> end_borrow config chain None bid
- | Borrows bids -> end_borrows config chain None bids
+ | Borrow bid -> end_borrow_aux config chain None bid
+ | Borrows bids -> end_borrows_aux config chain None bids
in
(* Reexplore, looking for loans *)
let cc = comp cc (end_abstraction_loans config chain abs_id) in
@@ -1326,7 +1332,7 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids)
V.AbstractionId.Set.empty abs_ids
in
(* End the abstractions and continue *)
- end_abstractions config chain abs_ids cf ctx
+ end_abstractions_aux config chain abs_ids cf ctx
in
(* End the internal borrows projectors and the loans projector *)
let cf_end_internal : cm_fun =
@@ -1379,7 +1385,7 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids)
cf ctx)
else
(* The borrows proj comes from a different abstraction: end it. *)
- let cc = end_abstraction config chain abs_id' in
+ let cc = end_abstraction_aux config chain abs_id' in
(* Retry ending the projector of loans *)
let cc =
comp cc (end_proj_loans_symbolic config chain abs_id regions sv)
@@ -1389,11 +1395,13 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids)
(* Continue *)
cc cf ctx
-let end_outer_borrow config : V.BorrowId.id -> cm_fun =
- end_borrow config [] None
+let end_borrow config : V.BorrowId.id -> cm_fun = end_borrow_aux config [] None
+
+let end_borrows config : V.BorrowId.Set.t -> cm_fun =
+ end_borrows_aux config [] None
-let end_outer_borrows config : V.BorrowId.Set.t -> cm_fun =
- end_borrows config [] None
+let end_abstraction config = end_abstraction_aux config []
+let end_abstractions config = end_abstractions_aux config []
(** Helper function: see {!activate_inactivated_mut_borrow}.
@@ -1504,8 +1512,8 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id)
(* End the loans *)
let cc =
match lc with
- | V.SharedLoan (bids, _) -> end_outer_borrows config bids
- | V.MutLoan bid -> end_outer_borrow config bid
+ | V.SharedLoan (bids, _) -> end_borrows config bids
+ | V.MutLoan bid -> end_borrow config bid
in
(* Recursive call *)
let cc = comp cc (activate_inactivated_mut_borrow config l) in
@@ -1524,7 +1532,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id)
(* End the borrows which borrow from the value, at the exception of
the borrow we want to promote *)
let bids = V.BorrowId.Set.remove l bids in
- let cc = end_outer_borrows config bids in
+ let cc = end_borrows config bids in
(* Promote the loan - TODO: this will fail if the value contains
* any loans. In practice, it shouldn't, but we could also
* look for loans inside the value and end them before promoting
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli
new file mode 100644
index 00000000..0733a15b
--- /dev/null
+++ b/compiler/InterpreterBorrows.mli
@@ -0,0 +1,34 @@
+module T = Types
+module V = Values
+module C = Contexts
+module Subst = Substitute
+module L = Logging
+module S = SynthesizeSymbolic
+open Cps
+open InterpreterProjectors
+
+(** When copying values, we duplicate the shared borrows. This is tantamount to
+ reborrowing the shared value. The [reborrow_shared original_id new_bid ctx]
+ applies this change to an environment [ctx] by inserting a new borrow id in
+ the set of borrows tracked by a shared value, referenced by the
+ [original_bid] argument. *)
+val reborrow_shared : V.BorrowId.id -> V.BorrowId.id -> C.eval_ctx -> C.eval_ctx
+
+(** End a borrow identified by its id, while preserving the invariants.
+
+ If the borrow is inside another borrow/an abstraction or contains loans,
+ [end_borrow] will end those borrows/abstractions/loans first.
+ *)
+val end_borrow : C.config -> V.BorrowId.id -> cm_fun
+
+(** End a set of borrows identified by their ids, while preserving the invariants. *)
+val end_borrows : C.config -> V.BorrowId.Set.t -> cm_fun
+
+(** End an abstraction while preserving the invariants. *)
+val end_abstraction : C.config -> V.AbstractionId.id -> cm_fun
+
+(** End a set of abstractions while preserving the invariants. *)
+val end_abstractions : C.config -> V.AbstractionId.Set.t -> cm_fun
+
+(** Activate a reserved borrow into a mutable borrow, while preserving the invariants. *)
+val activate_inactivated_mut_borrow : C.config -> V.BorrowId.id -> cm_fun
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 214f2cda..7cd447c3 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -1,6 +1,7 @@
-(* This file defines the basic blocks to implement the semantics of borrows.
- * Note that those functions are not only used in InterpreterBorrows, but
- * also in Invariants or InterpreterProjectors *)
+(** This file defines the basic blocks to implement the semantics of borrows.
+ Note that those functions are not only used in InterpreterBorrows, but
+ also in Invariants or InterpreterProjectors
+ *)
module T = Types
module V = Values
@@ -35,6 +36,11 @@ let ek_all : exploration_kind =
type borrow_ids = Borrows of V.BorrowId.Set.t | Borrow of V.BorrowId.id
[@@deriving show]
+type borrow_ids_or_symbolic_value =
+ | BorrowIds of borrow_ids
+ | SymbolicValue of V.symbolic_value
+[@@deriving show]
+
exception FoundBorrowIds of borrow_ids
type priority_borrows_or_abs =
@@ -43,11 +49,6 @@ type priority_borrows_or_abs =
| InnerLoans of borrow_ids
[@@deriving show]
-type borrow_ids_or_symbolic_value =
- | BorrowIds of borrow_ids
- | SymbolicValue of V.symbolic_value
-[@@deriving show]
-
let update_if_none opt x = match opt with None -> Some x | _ -> opt
(** Utility exception *)
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index cd6df2b0..c2807311 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -468,13 +468,12 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config)
let seel = List.map fst see_cf_l in
S.synthesize_symbolic_expansion sv sv_place seel subterms
-(** Expand a symbolic boolean *)
-let expand_symbolic_bool (config : C.config) (sp : V.symbolic_value)
- (sp_place : SA.mplace option) (cf_true : m_fun) (cf_false : m_fun) : m_fun =
+let expand_symbolic_bool (config : C.config) (sv : V.symbolic_value)
+ (sv_place : SA.mplace option) (cf_true : m_fun) (cf_false : m_fun) : m_fun =
fun ctx ->
(* Compute the expanded value *)
- let original_sv = sp in
- let original_sv_place = sp_place in
+ let original_sv = sv in
+ let original_sv_place = sv_place in
let rty = original_sv.V.sv_ty in
assert (rty = T.Bool);
(* Expand the symbolic value to true or false and continue execution *)
@@ -485,24 +484,17 @@ let expand_symbolic_bool (config : C.config) (sp : V.symbolic_value)
apply_branching_symbolic_expansions_non_borrow config original_sv
original_sv_place seel ctx
-(** Expand a symbolic value.
-
- [allow_branching]: if [true] we can branch (by expanding enumerations with
- stricly more than one variant), otherwise we can't.
-
- TODO: rename [sp] to [sv]
- *)
let expand_symbolic_value (config : C.config) (allow_branching : bool)
- (sp : V.symbolic_value) (sp_place : SA.mplace option) : cm_fun =
+ (sv : V.symbolic_value) (sv_place : SA.mplace option) : cm_fun =
fun cf ctx ->
(* Debug *)
- log#ldebug (lazy ("expand_symbolic_value:" ^ symbolic_value_to_string ctx sp));
+ log#ldebug (lazy ("expand_symbolic_value:" ^ symbolic_value_to_string ctx sv));
(* Remember the initial context for printing purposes *)
let ctx0 = ctx in
(* Compute the expanded value - note that when doing so, we may introduce
* fresh symbolic values in the context (which thus gets updated) *)
- let original_sv = sp in
- let original_sv_place = sp_place in
+ let original_sv = sv in
+ let original_sv_place = sv_place in
let rty = original_sv.V.sv_ty in
let cc : cm_fun =
fun cf ctx ->
@@ -512,7 +504,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
| T.Adt (T.AdtId def_id, regions, types) ->
(* Compute the expanded value *)
let seel =
- compute_expanded_symbolic_adt_value allow_branching sp.sv_kind def_id
+ compute_expanded_symbolic_adt_value allow_branching sv.sv_kind def_id
regions types ctx
in
(* Check for branching *)
@@ -528,7 +520,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
let ty = Collections.List.to_cons_nil types in
(* Compute the expanded value *)
let seel =
- compute_expanded_symbolic_option_value allow_branching sp.sv_kind ty
+ compute_expanded_symbolic_option_value allow_branching sv.sv_kind ty
in
(* Check for branching *)
@@ -540,7 +532,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
(* Tuples *)
| T.Adt (T.Tuple, [], tys) ->
(* Generate the field values *)
- let see = compute_expanded_symbolic_tuple_value sp.sv_kind tys in
+ let see = compute_expanded_symbolic_tuple_value sv.sv_kind tys in
(* Apply in the context *)
let ctx =
apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -552,7 +544,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
original_sv_place see expr
(* Boxes *)
| T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
- let see = compute_expanded_symbolic_box_value sp.sv_kind boxed_ty in
+ let see = compute_expanded_symbolic_box_value sv.sv_kind boxed_ty in
(* Apply in the context *)
let ctx =
apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -569,7 +561,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
(* Booleans *)
| T.Bool ->
assert allow_branching;
- expand_symbolic_bool config sp sp_place cf cf ctx
+ expand_symbolic_bool config sv sv_place cf cf ctx
| _ ->
raise
(Failure ("expand_symbolic_value: unexpected type: " ^ T.show_rty rty))
@@ -580,7 +572,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
log#ldebug
(lazy
("expand_symbolic_value: "
- ^ symbolic_value_to_string ctx0 sp
+ ^ symbolic_value_to_string ctx0 sv
^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
(* Sanity check: the symbolic value has disappeared *)
@@ -589,32 +581,6 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
(* Continue *)
cc cf ctx
-(** Symbolic integers are expanded upon evaluating a [switch], when the integer
- is not an enumeration discriminant.
- Note that a discriminant is never symbolic: we evaluate discriminant values
- upon evaluating [eval_discriminant], which always generates a concrete value
- (because if we call it on a symbolic enumeration, we expand the enumeration
- *then* evaluate the discriminant). This is how we can spot "regular" switches
- over integers.
-
-
- When expanding a boolean upon evaluating an [if ... then ... else ...],
- or an enumeration just before matching over it, we can simply expand the
- boolean/enumeration (generating a list of contexts from which to execute)
- then retry evaluating the [if ... then ... else ...] or the [match]: as
- the scrutinee will then have a concrete value, the interpreter will switch
- to the proper branch.
-
- However, when expanding a "regular" integer for a switch, there is always an
- *otherwise* branch that we can take, for which the integer must remain symbolic
- (because in this branch the scrutinee can take a range of values). We thus
- can't simply expand then retry to evaluate the [switch], because then we
- would loop...
-
- For this reason, we take the list of branches to execute as parameters, and
- directly jump to those branches after the expansion, without reevaluating the
- switch. The continuation is thus for the execution *after* the switch.
-*)
let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
(sv_place : SA.mplace option) (int_type : T.integer_type)
(tgts : (V.scalar_value * m_fun) list) (otherwise : m_fun) : m_fun =
@@ -636,7 +602,6 @@ let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
(* Then expand and evaluate - this generates the proper symbolic AST *)
apply_branching_symbolic_expansions_non_borrow config sv sv_place tgts
-(** See [expand_symbolic_value] *)
let expand_symbolic_value_no_branching (config : C.config)
(sv : V.symbolic_value) (sv_place : SA.mplace option) : cm_fun =
let allow_branching = false in
@@ -723,9 +688,6 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
(* Apply *)
expand cf ctx
-(** If this mode is activated through the [config], greedily expand the symbolic
- values which need to be expanded. See [config] for more information.
- *)
let greedy_expand_symbolic_values (config : C.config) : cm_fun =
fun cf ctx ->
if config.greedy_expand_symbolics_with_borrows then (
diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli
new file mode 100644
index 00000000..ee9f9e44
--- /dev/null
+++ b/compiler/InterpreterExpansion.mli
@@ -0,0 +1,73 @@
+module T = Types
+module PV = PrimitiveValues
+module V = Values
+module E = Expressions
+module C = Contexts
+module Subst = Substitute
+module L = Logging
+module Inv = Invariants
+module S = SynthesizeSymbolic
+module SA = SymbolicAst
+open Cps
+open InterpreterBorrows
+
+type proj_kind = LoanProj | BorrowProj
+
+(** Expand a symbolic boolean *)
+val expand_symbolic_bool :
+ C.config -> V.symbolic_value -> SA.mplace option -> m_fun -> m_fun -> m_fun
+
+(** Expand a symbolic value.
+
+ Parameters:
+ - [config]
+ - [allow_branching]: if [true] we can branch (by expanding enumerations with
+ stricly more than one variant), otherwise we can't.
+ - [sv]
+ - [sv_place]
+ *)
+val expand_symbolic_value :
+ C.config -> bool -> V.symbolic_value -> SA.mplace option -> cm_fun
+
+(** Symbolic integers are expanded upon evaluating a [switch], when the integer
+ is not an enumeration discriminant.
+ Note that a discriminant is never symbolic: we evaluate discriminant values
+ upon evaluating [eval_discriminant], which always generates a concrete value
+ (because if we call it on a symbolic enumeration, we expand the enumeration
+ *then* evaluate the discriminant). This is how we can spot "regular" switches
+ over integers.
+
+ When expanding a boolean upon evaluating an [if ... then ... else ...],
+ or an enumeration just before matching over it, we can simply expand the
+ boolean/enumeration (generating a list of contexts from which to execute)
+ then retry evaluating the [if ... then ... else ...] or the [match]: as
+ the scrutinee will then have a concrete value, the interpreter will switch
+ to the proper branch.
+
+ However, when expanding a "regular" integer for a switch, there is always an
+ *otherwise* branch that we can take, for which the integer must remain symbolic
+ (because in this branch the scrutinee can take a range of values). We thus
+ can't simply expand then retry to evaluate the [switch], because then we
+ would loop...
+
+ For this reason, we take the list of branches to execute as parameters, and
+ directly jump to those branches after the expansion, without reevaluating the
+ switch. The continuation is thus for the execution *after* the switch.
+ *)
+val expand_symbolic_int :
+ C.config ->
+ V.symbolic_value ->
+ SA.mplace option ->
+ T.integer_type ->
+ (V.scalar_value * m_fun) list ->
+ m_fun ->
+ m_fun
+
+(** See {!expand_symbolic_value} *)
+val expand_symbolic_value_no_branching :
+ C.config -> V.symbolic_value -> SA.mplace option -> cm_fun
+
+(** If this mode is activated through the [config], greedily expand the symbolic
+ values which need to be expanded. See {!C.config} for more information.
+ *)
+val greedy_expand_symbolic_values : C.config -> cm_fun
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index c604bb00..a7c17a45 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -34,7 +34,7 @@ let expand_primitively_copyable_at_place (config : C.config)
(* Small helper *)
let rec expand : cm_fun =
fun cf ctx ->
- let v = read_place_unwrap config access p ctx in
+ let v = read_place config access p ctx in
match
find_first_primitively_copyable_sv_with_borrows
ctx.type_context.type_infos v
@@ -53,12 +53,12 @@ let expand_primitively_copyable_at_place (config : C.config)
(** Read a place (CPS-style function).
We also check that the value *doesn't contain bottoms or inactivated
- borrows.
+ borrows*.
*)
let read_place (config : C.config) (access : access_kind) (p : E.place)
(cf : V.typed_value -> m_fun) : m_fun =
fun ctx ->
- let v = read_place_unwrap config access p ctx in
+ let v = read_place config access p ctx in
(* Check that there are no bottoms in the value *)
assert (not (bottom_in_value ctx.ended_regions v));
(* Check that there are no inactivated borrows in the value *)
@@ -79,8 +79,8 @@ let read_place (config : C.config) (access : access_kind) (p : E.place)
We also check, after the reorganization, that the value at the place
*doesn't contain any bottom nor inactivated borrows*.
- [expand_prim_copy]: if true, expand the symbolic values which are primitively
- copyable and contain borrows.
+ [expand_prim_copy]: if [true], expand the symbolic values which are
+ primitively copyable and contain borrows.
*)
let access_rplace_reorganize_and_read (config : C.config)
(expand_prim_copy : bool) (access : access_kind) (p : E.place)
@@ -131,6 +131,77 @@ let primitive_to_typed_value (ty : T.ety) (cv : V.primitive_value) :
(* Remaining cases (invalid) *)
| _, _ -> raise (Failure "Improperly typed constant value")
+(** Copy a value, and return the resulting value.
+
+ Note that copying values might update the context. For instance, when
+ copying shared borrows, we need to insert new shared borrows in the context.
+
+ Also, this function is actually more general than it should be: it can be
+ used to copy concrete ADT values, while ADT copy should be done through the
+ Copy trait (i.e., by calling a dedicated function). This is why we added a
+ parameter to control this copy ([allow_adt_copy]). Note that here by ADT we
+ mean the user-defined ADTs (not tuples or assumed types).
+ *)
+let rec copy_value (allow_adt_copy : bool) (config : C.config)
+ (ctx : C.eval_ctx) (v : V.typed_value) : C.eval_ctx * V.typed_value =
+ log#ldebug
+ (lazy
+ ("copy_value: "
+ ^ typed_value_to_string ctx v
+ ^ "\n- context:\n" ^ eval_ctx_to_string ctx));
+ (* Remark: at some point we rewrote this function to use iterators, but then
+ * 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.Primitive _ -> (ctx, v)
+ | V.Adt av ->
+ (* Sanity check *)
+ (match v.V.ty with
+ | T.Adt (T.Assumed (T.Box | Vec), _, _) ->
+ raise (Failure "Can't copy an assumed value other than Option")
+ | T.Adt (T.AdtId _, _, _) -> assert allow_adt_copy
+ | T.Adt ((T.Assumed Option | T.Tuple), _, _) -> () (* Ok *)
+ | _ -> raise (Failure "Unreachable"));
+ let ctx, fields =
+ List.fold_left_map
+ (copy_value allow_adt_copy config)
+ ctx av.field_values
+ in
+ (ctx, { v with V.value = V.Adt { av with field_values = fields } })
+ | V.Bottom -> raise (Failure "Can't copy ⊥")
+ | V.Borrow bc -> (
+ (* We can only copy shared borrows *)
+ match bc with
+ | SharedBorrow (mv, bid) ->
+ (* We need to create a new borrow id for the copied borrow, and
+ * update the context accordingly *)
+ let bid' = C.fresh_borrow_id () in
+ let ctx = InterpreterBorrows.reborrow_shared bid bid' ctx in
+ (ctx, { v with V.value = V.Borrow (SharedBorrow (mv, bid')) })
+ | MutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow")
+ | V.InactivatedMutBorrow _ ->
+ raise (Failure "Can't copy an inactivated mut borrow"))
+ | V.Loan lc -> (
+ (* We can only copy shared loans *)
+ match lc with
+ | V.MutLoan _ -> raise (Failure "Can't copy a mutable loan")
+ | V.SharedLoan (_, sv) ->
+ (* We don't copy the shared loan: only the shared value inside *)
+ copy_value allow_adt_copy config ctx sv)
+ | V.Symbolic 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));
+ (* 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
+ * borrows: when doing so, every occurrence of the same symbolic value
+ * must use a fresh borrow id. *)
+ (ctx, v)
+
(** Reorganize the environment in preparation for the evaluation of an operand.
Evaluating an operand requires reorganizing the environment to get access
@@ -148,7 +219,7 @@ let primitive_to_typed_value (ty : T.ety) (cv : V.primitive_value) :
dest <- f(move x, move y);
...
]}
- Because of the way [end_borrow] is implemented, when giving back the borrow
+ Because of the way {!end_borrow} is implemented, when giving back the borrow
[l0] upon evaluating [move y], we won't notice that [shared_borrow l0] has
disappeared from the environment (it has been moved and not assigned yet,
and so is hanging in "thin air").
@@ -158,13 +229,15 @@ let primitive_to_typed_value (ty : T.ety) (cv : V.primitive_value) :
by access *and* move operations have already been applied.
Rk.: in the formalization, we always have an explicit "reorganization" step
- in the rule premises, before the actual operand evaluation.
+ in the rule premises, before the actual operand evaluation, that allows to
+ reorganize the environment so that it satisfies the proper conditions. This
+ function's role is to do the reorganization.
Rk.: doing this is actually not completely necessary because when
generating MIR, rustc introduces intermediate assignments for all the function
parameters. Still, it is better for soundness purposes, and corresponds to
- what we do in the formalization (because we don't enforce constraints
- in the formalization).
+ what we do in the formalization (because we don't enforce the same constraints
+ as MIR in the formalization).
*)
let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) :
cm_fun =
@@ -234,22 +307,12 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
(* 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
- match write_place config access p bottom ctx with
- | Error _ -> raise (Failure "Unreachable")
- | Ok ctx -> cf v ctx
+ let ctx = write_place config access p bottom ctx in
+ cf v ctx
in
(* Compose and apply *)
comp cc move cf ctx
-(** Evaluate an operand.
-
- Reorganize the context, then evaluate the operand.
-
- **Warning**: this function shouldn't be used to evaluate a list of
- operands (for a function call, for instance): we must do *one* reorganization
- of the environment, before evaluating all the operands at once.
- Use [eval_operands] instead.
- *)
let eval_operand (config : C.config) (op : E.operand)
(cf : V.typed_value -> m_fun) : m_fun =
fun ctx ->
@@ -602,7 +665,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
({ v with V.value = v' }, v)
in
(* Update the borrowed value in the context *)
- let ctx = write_place_unwrap config access p nv ctx in
+ let ctx = write_place config access p nv ctx in
(* Compute the rvalue - simply a shared borrow with a the fresh id.
* Note that the reference is *mutable* if we do a two-phase borrow *)
let rv_ty =
@@ -637,7 +700,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
(* Compute the value with which to replace the value at place p *)
let nv = { v with V.value = V.Loan (V.MutLoan bid) } in
(* Update the value in the context *)
- let ctx = write_place_unwrap config access p nv ctx in
+ let ctx = write_place config access p nv ctx in
(* Continue *)
cf rv ctx
in
@@ -699,10 +762,6 @@ let eval_rvalue_aggregate (config : C.config)
(* Compose and apply *)
comp eval_ops compute cf
-(** Evaluate an rvalue which is not a global.
-
- Transmits the computed rvalue to the received continuation.
- *)
let eval_rvalue_not_global (config : C.config) (rvalue : E.rvalue)
(cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
fun ctx ->
@@ -723,3 +782,16 @@ let eval_rvalue_not_global (config : C.config) (rvalue : E.rvalue)
comp_wrap (eval_rvalue_aggregate config aggregate_kind ops) ctx
| E.Discriminant p -> comp_wrap (eval_rvalue_discriminant config p) ctx
| E.Global _ -> raise (Failure "Unreachable")
+
+let eval_fake_read (config : C.config) (p : E.place) : cm_fun =
+ fun cf ctx ->
+ let expand_prim_copy = false in
+ let cf_prepare cf =
+ access_rplace_reorganize_and_read config expand_prim_copy Read p cf
+ in
+ let cf_continue cf v : m_fun =
+ fun ctx ->
+ assert (not (bottom_in_value ctx.ended_regions v));
+ cf ctx
+ in
+ comp cf_prepare cf_continue cf ctx
diff --git a/compiler/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli
new file mode 100644
index 00000000..c610e939
--- /dev/null
+++ b/compiler/InterpreterExpressions.mli
@@ -0,0 +1,37 @@
+module T = Types
+module PV = PrimitiveValues
+module V = Values
+module LA = LlbcAst
+module E = Expressions
+module C = Contexts
+module Subst = Substitute
+module L = Logging
+module Inv = Invariants
+module S = SynthesizeSymbolic
+open Cps
+open InterpreterPaths
+
+(** Evaluate an operand.
+
+ Reorganize the context, then evaluate the operand.
+
+ **Warning**: this function shouldn't be used to evaluate a list of
+ operands (for a function call, for instance): we must do *one* reorganization
+ of the environment, before evaluating all the operands at once.
+ Use {!eval_operands} instead.
+ *)
+val eval_operand : C.config -> E.operand -> (V.typed_value -> m_fun) -> m_fun
+
+(** Evaluate several operands at once. *)
+val eval_operands :
+ C.config -> E.operand list -> (V.typed_value list -> m_fun) -> m_fun
+
+(** Evaluate an rvalue which is not a global.
+
+ Transmits the computed rvalue to the received continuation.
+ *)
+val eval_rvalue_not_global :
+ C.config -> E.rvalue -> ((V.typed_value, eval_error) result -> m_fun) -> m_fun
+
+(** Evaluate a fake read (update the context so that we can read a place) *)
+val eval_fake_read : C.config -> E.place -> cm_fun
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index cc5b5864..73b446da 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -5,7 +5,6 @@ module C = Contexts
module Subst = Substitute
module L = Logging
open Cps
-open TypesUtils
open ValuesUtils
open InterpreterUtils
open InterpreterBorrowsCore
@@ -307,12 +306,12 @@ let access_kind_to_projection_access (access : access_kind) : projection_access
lookup_shared_borrows = false;
}
-(** Read the value at a given place.
+(** Attempt to read the value at a given place.
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 read_place (config : C.config) (access : access_kind) (p : E.place)
+let try_read_place (config : C.config) (access : access_kind) (p : E.place)
(ctx : C.eval_ctx) : V.typed_value path_access_result =
let access = access_kind_to_projection_access access in
(* The update function is the identity *)
@@ -334,14 +333,14 @@ let read_place (config : C.config) (access : access_kind) (p : E.place)
raise (Failure "Unexpected environment update"));
Ok read_value
-let read_place_unwrap (config : C.config) (access : access_kind) (p : E.place)
+let read_place (config : C.config) (access : access_kind) (p : E.place)
(ctx : C.eval_ctx) : V.typed_value =
- match read_place config access p ctx with
+ match try_read_place config access p ctx with
| Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e))
| Ok v -> v
-(** Update the value at a given place *)
-let write_place (_config : C.config) (access : access_kind) (p : E.place)
+(** Attempt to update the value at a given place *)
+let try_write_place (_config : C.config) (access : access_kind) (p : E.place)
(nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx path_access_result =
let access = access_kind_to_projection_access access in
(* The update function substitutes the value with the new value *)
@@ -352,13 +351,12 @@ let write_place (_config : C.config) (access : access_kind) (p : E.place)
(* We ignore the read value *)
Ok ctx
-let write_place_unwrap (config : C.config) (access : access_kind) (p : E.place)
+let write_place (config : C.config) (access : access_kind) (p : E.place)
(nv : V.typed_value) (ctx : C.eval_ctx) : C.eval_ctx =
- match write_place config access p nv ctx with
+ match try_write_place config access p nv ctx with
| Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e))
| Ok ctx -> ctx
-(** Compute an expanded ADT bottom value *)
let compute_expanded_bottom_adt_value (tyctx : T.type_decl T.TypeDeclId.Map.t)
(def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
(regions : T.erased_region list) (types : T.ety list) : V.typed_value =
@@ -378,7 +376,6 @@ let compute_expanded_bottom_adt_value (tyctx : T.type_decl T.TypeDeclId.Map.t)
let ty = T.Adt (T.AdtId def_id, regions, types) in
{ V.value = av; V.ty }
-(** Compute an expanded Option bottom value *)
let compute_expanded_bottom_option_value (variant_id : T.VariantId.id)
(param_ty : T.ety) : V.typed_value =
(* Note that the variant can be [Some] or [None]: we expand bottom values
@@ -392,7 +389,6 @@ let compute_expanded_bottom_option_value (variant_id : T.VariantId.id)
let ty = T.Adt (T.Assumed T.Option, [], [ param_ty ]) in
{ V.value = av; ty }
-(** Compute an expanded tuple bottom value *)
let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
V.typed_value =
(* Generate the field values *)
@@ -469,29 +465,21 @@ let expand_bottom_value_from_projection (config : C.config)
("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_ety ty))
in
(* Update the context by inserting the expanded value at the proper place *)
- match write_place config access p' nv ctx with
+ match try_write_place config access p' nv ctx with
| Ok ctx -> ctx
| Error _ -> raise (Failure "Unreachable")
-(** Update the environment to be able to read a place.
-
- When reading a place, we may be stuck along the way because some value
- is borrowed, we reach a symbolic value, etc. In this situation [read_place]
- fails while returning precise information about the failure. This function
- uses this information to update the environment (by ending borrows,
- expanding symbolic values) until we manage to fully read the place.
- *)
let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
(p : E.place) : cm_fun =
fun cf ctx ->
(* Attempt to read the place: if it fails, update the environment and retry *)
- match read_place config access p ctx with
+ match try_read_place config access p ctx with
| Ok _ -> cf ctx
| Error err ->
let cc =
match err with
- | FailSharedLoan bids -> end_outer_borrows config bids
- | FailMutLoan bid -> end_outer_borrow config bid
+ | FailSharedLoan bids -> end_borrows config bids
+ | FailMutLoan bid -> end_borrow config bid
| FailInactivatedMutBorrow bid ->
activate_inactivated_mut_borrow config bid
| FailSymbolic (i, sp) ->
@@ -510,23 +498,19 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
in
comp cc (update_ctx_along_read_place config access p) cf ctx
-(** Update the environment to be able to write to a place.
-
- See {!update_ctx_along_read_place}.
-*)
let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
(p : E.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 *)
- match read_place config access p ctx with
+ match try_read_place config access p ctx with
| Ok _ -> cf ctx
| Error err ->
(* Update the context *)
let cc =
match err with
- | FailSharedLoan bids -> end_outer_borrows config bids
- | FailMutLoan bid -> end_outer_borrow config bid
+ | FailSharedLoan bids -> end_borrows config bids
+ | FailMutLoan bid -> end_borrow config bid
| FailInactivatedMutBorrow bid ->
activate_inactivated_mut_borrow config bid
| FailSymbolic (_pe, sp) ->
@@ -549,15 +533,6 @@ 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
-(** End the loans at a given place: read the value, if it contains a loan,
- end this loan, repeat.
-
- This is used when reading or borrowing values. We typically
- first call {!update_ctx_along_read_place} or {!update_ctx_along_write_place}
- to get access to the value, then call this function to "prepare" the value:
- when moving values, we can't move a value which contains loans and thus need
- to end them, etc.
- *)
let rec end_loans_at_place (config : C.config) (access : access_kind)
(p : E.place) : cm_fun =
fun cf ctx ->
@@ -587,17 +562,17 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
match access with
| Read -> super#visit_SharedLoan env bids v
| Write | Move ->
- let cc = end_outer_borrows config bids in
+ let cc = end_borrows config bids in
raise (UpdateCtx cc))
| V.MutLoan bid ->
(* We always need to end mutable borrows *)
- let cc = end_outer_borrow config bid in
+ let cc = end_borrow config bid in
raise (UpdateCtx cc)
end
in
(* First, retrieve the value *)
- match read_place config access p ctx with
+ match try_read_place config access p ctx with
| Error _ -> raise (Failure "Unreachable")
| Ok v -> (
(* Inspect the value and update the context while doing so.
@@ -615,26 +590,13 @@ 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)
-(** Drop (end) outer loans at a given place, which should be seen as an l-value
- (we will write to it later, but need to drop the loans before writing).
-
- This is used to drop values when evaluating the drop statement or before
- writing to a place.
-
- Note that we don't do what is defined in the formalization: we move the
- value to a temporary dummy value, then explore this value and end the outer
- loans which are inside as long as we find some, then move the resulting
- value back to where it was. This shouldn't make any difference, really (note
- that the place is *inside* a borrow, if we end the borrow, we won't be able
- to reinsert the value back).
- *)
let drop_outer_loans_at_lplace (config : C.config) (p : E.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_unwrap config access p ctx in
- let ctx = write_place_unwrap config access p (mk_bottom v.V.ty) ctx in
+ let v = read_place config access p ctx in
+ let ctx = write_place config 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
(* Auxiliary function *)
@@ -652,9 +614,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_outer_borrows config bids
- | LoanContent (V.MutLoan bid) -> end_outer_borrow config bid
+ | LoanContent (V.SharedLoan (bids, _)) -> end_borrows config bids
+ | LoanContent (V.MutLoan bid) -> end_borrow config bid
| BorrowContent _ -> raise (Failure "Unreachable")
in
(* Retry *)
@@ -668,7 +629,7 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
(* Pop *)
let ctx, v = C.ctx_remove_dummy_var ctx dummy_id in
(* Reinsert *)
- let ctx = write_place_unwrap config access p v ctx in
+ let ctx = write_place config access p v ctx in
(* Sanity check *)
assert (not (outer_loans_in_value v));
(* Continue *)
@@ -677,89 +638,6 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
(* Continue *)
cc cf ctx
-(** Copy a value, and return the resulting value.
-
- Note that copying values might update the context. For instance, when
- copying shared borrows, we need to insert new shared borrows in the context.
-
- Also, this function is actually more general than it should be: it can be used
- to copy concrete ADT values, while ADT copy should be done through the Copy
- trait (i.e., by calling a dedicated function). This is why we added a parameter
- to control this copy. Note that here by ADT we mean the user-defined ADTs
- (not tuples or assumed types).
-
- TODO: move
- *)
-let rec copy_value (allow_adt_copy : bool) (config : C.config)
- (ctx : C.eval_ctx) (v : V.typed_value) : C.eval_ctx * V.typed_value =
- log#ldebug
- (lazy
- ("copy_value: "
- ^ typed_value_to_string ctx v
- ^ "\n- context:\n" ^ eval_ctx_to_string ctx));
- (* Remark: at some point we rewrote this function to use iterators, but then
- * 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.Primitive _ -> (ctx, v)
- | V.Adt av ->
- (* Sanity check *)
- (match v.V.ty with
- | T.Adt (T.Assumed (T.Box | Vec), _, _) ->
- raise (Failure "Can't copy an assumed value other than Option")
- | T.Adt (T.AdtId _, _, _) -> assert allow_adt_copy
- | T.Adt ((T.Assumed Option | T.Tuple), _, _) -> () (* Ok *)
- | _ -> raise (Failure "Unreachable"));
- let ctx, fields =
- List.fold_left_map
- (copy_value allow_adt_copy config)
- ctx av.field_values
- in
- (ctx, { v with V.value = V.Adt { av with field_values = fields } })
- | V.Bottom -> raise (Failure "Can't copy ⊥")
- | V.Borrow bc -> (
- (* We can only copy shared borrows *)
- match bc with
- | SharedBorrow (mv, bid) ->
- (* We need to create a new borrow id for the copied borrow, and
- * update the context accordingly *)
- let bid' = C.fresh_borrow_id () in
- let ctx = reborrow_shared bid bid' ctx in
- (ctx, { v with V.value = V.Borrow (SharedBorrow (mv, bid')) })
- | MutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow")
- | V.InactivatedMutBorrow _ ->
- raise (Failure "Can't copy an inactivated mut borrow"))
- | V.Loan lc -> (
- (* We can only copy shared loans *)
- match lc with
- | V.MutLoan _ -> raise (Failure "Can't copy a mutable loan")
- | V.SharedLoan (_, sv) ->
- (* We don't copy the shared loan: only the shared value inside *)
- copy_value allow_adt_copy config ctx sv)
- | V.Symbolic 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));
- (* 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
- * borrows: when doing so, every occurrence of the same symbolic value
- * must use a fresh borrow id. *)
- (ctx, v)
-
-(** Small utility.
-
- Prepare a place which is to be used as the destination of an assignment:
- update the environment along the paths, end the outer loans at this place, etc.
-
- Return the updated context and the (updated) value at the end of the
- place. This value should not contain any outer loan (and we check
- it is the case). Note that this value is very likely to contain {!V.Bottom}
- subvalues.
- *)
let prepare_lplace (config : C.config) (p : E.place)
(cf : V.typed_value -> m_fun) : m_fun =
fun ctx ->
@@ -775,7 +653,7 @@ let prepare_lplace (config : C.config) (p : E.place)
(* Read the value and check it *)
let read_check cf : m_fun =
fun ctx ->
- let v = read_place_unwrap config access p ctx in
+ let v = read_place config access p ctx in
(* Sanity checks *)
assert (not (outer_loans_in_value v));
(* Continue *)
diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli
new file mode 100644
index 00000000..ed00b7c5
--- /dev/null
+++ b/compiler/InterpreterPaths.mli
@@ -0,0 +1,105 @@
+module T = Types
+module V = Values
+module E = Expressions
+module C = Contexts
+module Subst = Substitute
+module L = Logging
+open Cps
+open InterpreterExpansion
+module Synth = SynthesizeSymbolic
+
+type access_kind = Read | Write | Move
+
+(** Update the environment to be able to read a place.
+
+ When reading a place, we may be stuck along the way because some value
+ is borrowed, we reach a symbolic value, etc. This function repeatedly
+ updates the environment (by ending borrows, expanding symbolic values, etc.)
+ until it manages to fully access the provided place.
+ *)
+val update_ctx_along_read_place : C.config -> access_kind -> E.place -> cm_fun
+
+(** Update the environment to be able to write to a place.
+
+ See {!update_ctx_along_read_place}.
+*)
+val update_ctx_along_write_place : C.config -> access_kind -> E.place -> cm_fun
+
+(** Read the value at a given place.
+
+ 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).
+ *)
+val read_place :
+ C.config -> access_kind -> E.place -> C.eval_ctx -> V.typed_value
+
+(** Update the value at a given place.
+
+ This function is an auxiliary function and is not safe: it will not check if
+ the overwritten value contains borrows, loans, etc. and will simply
+ overwrite it.
+ *)
+val write_place :
+ C.config ->
+ access_kind ->
+ E.place ->
+ V.typed_value ->
+ C.eval_ctx ->
+ C.eval_ctx
+
+(** Compute an expanded tuple ⊥ value.
+
+ [compute_expanded_bottom_tuple_value [ty0, ..., tyn]] returns
+ [(⊥:ty0, ..., ⊥:tyn)]
+ *)
+val compute_expanded_bottom_tuple_value : T.ety list -> V.typed_value
+
+(** Compute an expanded ADT ⊥ value *)
+val compute_expanded_bottom_adt_value :
+ T.type_decl T.TypeDeclId.Map.t ->
+ T.TypeDeclId.id ->
+ T.VariantId.id option ->
+ T.erased_region list ->
+ T.ety list ->
+ V.typed_value
+
+(** Compute an expanded [Option] ⊥ value *)
+val compute_expanded_bottom_option_value :
+ T.VariantId.id -> T.ety -> V.typed_value
+
+(** Drop (end) outer loans at a given place, which should be seen as an l-value
+ (we will write to it later, but need to drop the loans before writing).
+
+ This is used to drop values when evaluating the drop statement or before
+ writing to a place.
+
+ Note that we don't do what is defined in the formalization: we move the
+ value to a temporary dummy value, then explore this value and end the outer
+ loans which are inside as long as we find some, then move the resulting
+ value back to where it was. This shouldn't make any difference, really (note
+ that the place is *inside* a borrow, if we end the borrow, we won't be able
+ to reinsert the value back).
+ *)
+val drop_outer_loans_at_lplace : C.config -> E.place -> cm_fun
+
+(** End the loans at a given place: read the value, if it contains a loan,
+ end this loan, repeat.
+
+ This is used when reading or borrowing values. We typically
+ first call {!update_ctx_along_read_place} or {!update_ctx_along_write_place}
+ to get access to the value, then call this function to "prepare" the value:
+ when moving values, we can't move a value which contains loans and thus need
+ to end them, etc.
+ *)
+val end_loans_at_place : C.config -> access_kind -> E.place -> cm_fun
+
+(** Small utility.
+
+ Prepare a place which is to be used as the destination of an assignment:
+ update the environment along the paths, end the outer loans at this place, etc.
+
+ Return the updated context and the (updated) value at the end of the
+ place. This value should not contain any outer loan (and we check it is the
+ case). Note that this value is very likely to contain ⊥ subvalues.
+ *)
+val prepare_lplace : C.config -> E.place -> (V.typed_value -> m_fun) -> m_fun
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index b77a94c4..67bbe21f 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -8,12 +8,9 @@ open TypesUtils
open InterpreterUtils
open InterpreterBorrowsCore
-(** Auxiliary function.
+(** The local logger *)
+let log = L.projectors_log
- Apply a proj_borrows on a shared borrow.
- Note that when projecting over shared values, we generate
- {!V.abstract_shared_borrows}, not {!V.avalue}s.
-*)
let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
(fresh_reborrow : V.BorrowId.id -> V.BorrowId.id)
(regions : T.RegionId.Set.t) (v : V.typed_value) (ty : T.rty) :
@@ -93,38 +90,6 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
[ V.AsbProjReborrows (s, ty) ]
| _ -> raise (Failure "Unreachable")
-(** Apply (and reduce) a projector over borrows to a value.
-
- - [regions]: the regions we project
- - [v]: the value over which we project
- - [ty]: the projection type (is used to map borrows to regions, or to
- interpret the borrows as belonging to some regions...). Remember that
- [v] doesn't contain region information.
- For instance, if we have:
- [v <: ty] where:
- - [v = mut_borrow l ...]
- - [ty = Ref (r, ...)]
- then we interpret the borrow [l] as belonging to region [r]
-
- Also, when applying projections on shared values, we need to apply
- reborrows. This is a bit annoying because, with the way we compute
- the projection on borrows, we can't update the context immediately.
- Instead, we remember the list of borrows we have to insert in the
- context *afterwards*.
-
- [check_symbolic_no_ended] controls whether we check or not whether
- symbolic values don't contain already ended regions.
- This check is activated when applying projectors upon calling a function
- (because we need to check that function arguments don't contain ⊥),
- but deactivated when expanding symbolic values:
- {[
- fn f<'a,'b>(x : &'a mut u32, y : &'b mut u32) -> (&'a mut u32, &'b mut u32);
-
- let p = f(&mut x, &mut y); // p -> @s0
- assert(x == ...); // end 'a
- let z = p.1; // HERE: the symbolic expansion of @s0 contains ended regions
- ]}
-*)
let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
(fresh_reborrow : V.BorrowId.id -> V.BorrowId.id)
(regions : T.RegionId.Set.t) (ancestors_regions : T.RegionId.Set.t)
@@ -251,7 +216,6 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
in
{ V.value; V.ty }
-(** Convert a symbolic expansion *which is not a borrow* to a value *)
let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
(see : V.symbolic_expansion) : V.typed_value =
let ty = Subst.erase_regions sv.V.sv_ty in
@@ -268,12 +232,6 @@ let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
in
{ V.value; V.ty }
-(** Convert a symbolic expansion to a value.
-
- If the expansion is a mutable reference expansion, it converts it to a borrow.
- This function is meant to be used when reducing projectors over borrows,
- during a symbolic expansion.
- *)
let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value)
(see : V.symbolic_expansion) : V.typed_value =
match see with
@@ -497,14 +455,6 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
(* Return *)
ctx
-(** Auxiliary function to prepare reborrowing operations (used when
- applying projectors).
-
- Returns two functions:
- - a function to generate fresh re-borrow ids, and register the reborrows
- - a function to apply the reborrows in a context
- Those functions are of course stateful.
- *)
let prepare_reborrows (config : C.config) (allow_reborrows : bool) :
(V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx) =
let reborrows : (V.BorrowId.id * V.BorrowId.id) list ref = ref [] in
diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli
new file mode 100644
index 00000000..a6d8bd5c
--- /dev/null
+++ b/compiler/InterpreterProjectors.mli
@@ -0,0 +1,115 @@
+module T = Types
+module V = Values
+module E = Expressions
+module C = Contexts
+module Subst = Substitute
+module L = Logging
+open InterpreterBorrowsCore
+
+(** Auxiliary function.
+
+ Apply a proj_borrows on a shared borrow.
+ Note that when projecting over shared values, we generate
+ {!V.abstract_shared_borrows}, not {!V.avalue}s.
+*)
+val apply_proj_loans_on_symbolic_expansion :
+ T.RegionId.Set.t -> V.symbolic_expansion -> T.rty -> V.typed_avalue
+
+(** Convert a symbolic expansion *which is not a borrow* to a value *)
+val symbolic_expansion_non_borrow_to_value :
+ V.symbolic_value -> V.symbolic_expansion -> V.typed_value
+
+(** Convert a symbolic expansion *which is not a shared borrow* to a value.
+
+ If the expansion is a mutable reference expansion, it converts it to a borrow.
+ This function is meant to be used when reducing projectors over borrows,
+ during a symbolic expansion.
+ *)
+val symbolic_expansion_non_shared_borrow_to_value :
+ V.symbolic_value -> V.symbolic_expansion -> V.typed_value
+
+(** Auxiliary function to prepare reborrowing operations (used when
+ applying projectors).
+
+ Returns two functions:
+ - a function to generate fresh re-borrow ids, and register the reborrows
+ - a function to apply the reborrows in a context
+ Those functions are of course stateful.
+
+ Parameters:
+ - [config]
+ - [allow_reborrows]
+ *)
+val prepare_reborrows :
+ C.config ->
+ bool ->
+ (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx)
+
+(** Apply (and reduce) a projector over borrows to a value.
+
+ Parameters:
+ - [check_symbolic_no_ended]: controls whether we check or not whether
+ symbolic values don't contain already ended regions.
+ This check is activated when applying projectors upon calling a function
+ (because we need to check that function arguments don't contain ⊥),
+ but deactivated when expanding symbolic values:
+ {[
+ fn f<'a,'b>(x : &'a mut u32, y : &'b mut u32) -> (&'a mut u32, &'b mut u32);
+
+ let p = f(&mut x, &mut y); // p -> @s0
+ assert(x == ...); // end 'a
+ let z = p.1; // HERE: the symbolic expansion of @s0 contains ended regions
+ ]}
+ - [ctx]
+
+ - [fresh_reborrow]: a function which generates fresh ids for reborrows, and
+ registers the reborrows (to be applied later to the context).
+
+ When applying projections on shared values, we need to apply
+ reborrows. This is a bit annoying because, with the way we compute
+ the projection on borrows, we can't update the context immediately.
+ Instead, we remember the list of borrows we have to insert in the
+ context *afterwards*.
+
+ See {!prepare_reborrows}
+
+ - [regions]: the regions to project
+ - [ancestor_regions]
+ - [v]: the value on which to apply the projection
+
+ - [ty]: the projection type (is used to map borrows to regions, or in other
+ words to interpret the borrows as belonging to some regions). Remember that
+ [v] doesn't contain region information.
+ For instance, if we have:
+ [v <: ty] where:
+ - [v = mut_borrow l ...]
+ - [ty = Ref (r, ...)]
+ then we interpret the borrow [l] as belonging to region [r]
+*)
+val apply_proj_borrows :
+ bool ->
+ C.eval_ctx ->
+ (V.BorrowId.id -> V.BorrowId.id) ->
+ T.RegionId.Set.t ->
+ T.RegionId.Set.t ->
+ V.typed_value ->
+ T.rty ->
+ V.typed_avalue
+
+(** Parameters:
+ - [config]
+ - [ctx]
+ - [regions]: the regions to project
+ - [ancestors_regions]
+ - [v]: the value on which to apply the projection
+ - [ty]: the type (with regions) to use for the projection
+
+ *)
+val apply_proj_borrows_on_input_value :
+ C.config ->
+ C.eval_ctx ->
+ T.RegionId.Set.t ->
+ T.RegionId.Set.t ->
+ V.typed_value ->
+ T.rty ->
+ C.eval_ctx * V.typed_avalue
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 4d447ffe..66196349 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -39,12 +39,12 @@ let drop_value (config : C.config) (p : E.place) : cm_fun =
let replace cf (v : V.typed_value) ctx =
(* Move the value at destination (that we will overwrite) to a dummy variable
* to preserve the borrows it may contain *)
- let mv = read_place_unwrap config access p ctx in
+ let mv = InterpreterPaths.read_place config access p ctx in
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 ctx = write_place_unwrap config access p nv ctx in
+ let ctx = write_place config access p nv ctx in
log#ldebug
(lazy
("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n"
@@ -119,14 +119,14 @@ let assign_to_place (config : C.config) (rv : V.typed_value) (p : E.place) :
fun ctx ->
(* Move the value at destination (that we will overwrite) to a dummy variable
* to preserve the borrows *)
- let mv = read_place_unwrap config Write p ctx in
+ let mv = InterpreterPaths.read_place config Write p ctx in
let dest_vid = C.fresh_dummy_var_id () in
let ctx = C.ctx_push_dummy_var ctx dest_vid mv in
(* Write to the destination *)
(* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *)
assert (not (bottom_in_value ctx.ended_regions rv));
(* Update the destination *)
- let ctx = write_place_unwrap config Write p rv ctx in
+ let ctx = write_place config Write p rv ctx in
(* Debug *)
log#ldebug
(lazy
@@ -322,19 +322,10 @@ let move_return_value (config : C.config) (cf : V.typed_value -> m_fun) : m_fun
let cc = eval_operand config (E.Move (mk_place_from_var_id ret_vid)) in
cc cf ctx
-(** Pop the current frame.
-
- Drop all the local variables but the return variable, move the return
- value out of the return variable, remove all the local variables (but not the
- abstractions!) from the context, remove the {!C.Frame} indicator delimiting the
- current frame and handle the return value to the continuation.
-
- TODO: rename (remove the "ctx_")
- *)
-let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
+let pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
fun ctx ->
(* Debug *)
- log#ldebug (lazy ("ctx_pop_frame:\n" ^ eval_ctx_to_string ctx));
+ log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ctx));
(* List the local variables, but the return variable *)
let ret_vid = E.VarId.zero in
@@ -352,7 +343,7 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
(* Debug *)
log#ldebug
(lazy
- ("ctx_pop_frame: locals in which to drop the outer loans: ["
+ ("pop_frame: locals in which to drop the outer loans: ["
^ String.concat "," (List.map E.VarId.to_string locals)
^ "]"));
@@ -383,7 +374,7 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
comp_check_value cc (fun _ ctx ->
log#ldebug
(lazy
- ("ctx_pop_frame: after dropping outer loans in local variables:\n"
+ ("pop_frame: after dropping outer loans in local variables:\n"
^ eval_ctx_to_string ctx)))
in
@@ -410,7 +401,7 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
(** Pop the current frame and assign the returned value to its destination. *)
let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun =
- let cf_pop = ctx_pop_frame config in
+ let cf_pop = pop_frame config in
let cf_assign cf ret_value : m_fun =
assign_to_place config ret_value dest cf
in
@@ -547,7 +538,9 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list)
match (region_params, type_params, args) with
| [], [ boxed_ty ], [ E.Move input_box_place ] ->
(* Required type checking *)
- let input_box = read_place_unwrap config Write input_box_place ctx in
+ let input_box =
+ InterpreterPaths.read_place config Write input_box_place ctx
+ in
(let input_ty = ty_get_box input_box.V.ty in
assert (input_ty = boxed_ty));
@@ -642,15 +635,6 @@ let eval_non_local_function_call_concrete (config : C.config)
(* Compose and apply *)
comp cf_eval_ops cf_eval_call
-(** Instantiate a function signature, introducing fresh abstraction ids and
- region ids. This is mostly used in preparation of function calls, when
- evaluating in symbolic mode of course.
-
- Note: there are no region parameters, because they should be erased.
-
- **Rk.:** this function is **stateful** and generates fresh abstraction ids
- for the region groups.
- *)
let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) :
A.inst_fun_sig =
(* Generate fresh abstraction ids and create a substitution from region
@@ -757,20 +741,6 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
(* Apply *)
T.RegionGroupId.mapi create_abs rgl
-(** Helper.
-
- Create a list of abstractions from a list of regions groups, and insert
- them in the context.
-
- [region_can_end]: gives the region groups from which we generate functions
- which can end or not.
-
- [compute_abs_avalues]: this function must compute, given an initialized,
- empty (i.e., with no avalues) abstraction, compute the avalues which
- should be inserted in this abstraction before we insert it in the context.
- Note that this function may update the context: it is necessary when
- computing borrow projections, for instance.
-*)
let create_push_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
(kind : V.abs_kind) (rgl : A.abs_region_group list)
(region_can_end : T.RegionGroupId.id -> bool)
@@ -857,17 +827,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
(* Compose and apply *)
comp cf_eval_rvalue cf_assign cf ctx)
- | A.FakeRead p ->
- let expand_prim_copy = false in
- let cf_prepare cf =
- access_rplace_reorganize_and_read config expand_prim_copy Read p cf
- in
- let cf_continue cf v : m_fun =
- fun ctx ->
- assert (not (bottom_in_value ctx.ended_regions v));
- cf ctx
- in
- comp cf_prepare cf_continue (cf Unit) ctx
+ | A.FakeRead p -> eval_fake_read config p (cf Unit) ctx
| A.SetDiscriminant (p, variant_id) ->
set_discriminant config p variant_id cf ctx
| A.Drop p -> drop_value config p (cf Unit) ctx
@@ -1256,7 +1216,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
abs_ids := with_loans_abs;
(* End the abstractions which can be ended *)
let no_loans_abs = V.AbstractionId.Set.of_list no_loans_abs in
- let cc = InterpreterBorrows.end_abstractions config [] no_loans_abs in
+ let cc = InterpreterBorrows.end_abstractions config no_loans_abs in
(* Recursive call *)
let cc = comp cc end_abs_with_no_loans in
(* Continue *)
@@ -1362,8 +1322,7 @@ and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id)
eval_local_function_call_symbolic config fid region_args type_args args
dest
-(** Evaluate a statement seen as a function body (auxiliary helper for
- [eval_statement]) *)
+(** Evaluate a statement seen as a function body *)
and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun =
fun cf ctx ->
let cc = eval_statement config body in
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
new file mode 100644
index 00000000..1bfd1c78
--- /dev/null
+++ b/compiler/InterpreterStatements.mli
@@ -0,0 +1,63 @@
+module T = Types
+module PV = PrimitiveValues
+module V = Values
+module E = Expressions
+module C = Contexts
+module Subst = Substitute
+module A = LlbcAst
+module L = Logging
+module Inv = Invariants
+module S = SynthesizeSymbolic
+open Cps
+open InterpreterExpressions
+
+(** Pop the current frame.
+
+ Drop all the local variables (which has the effect of moving their values to
+ dummy variables, after ending the proper borrows of course) but the return
+ variable, move the return value out of the return variable, remove all the
+ local variables (but preserve the abstractions!), remove the {!C.Frame} indicator
+ delimiting the current frame and handle the return value to the continuation.
+ *)
+val pop_frame : C.config -> (V.typed_value -> m_fun) -> m_fun
+
+(** Instantiate a function signature, introducing **fresh** abstraction ids and
+ region ids. This is mostly used in preparation of function calls, when
+ evaluating in symbolic mode of course.
+
+ Note: there are no region parameters, because they should be erased.
+ *)
+val instantiate_fun_sig : T.ety list -> LA.fun_sig -> LA.inst_fun_sig
+
+(** Helper.
+
+ Create a list of abstractions from a list of regions groups, and insert
+ them in the context.
+
+ Parameters:
+ - [call_id]
+ - [kind]
+ - [rgl]: "region group list"
+ - [region_can_end]: gives the region groups from which we generate functions
+ which can end or not.
+ - [compute_abs_avalues]: this function must compute, given an initialized,
+ empty (i.e., with no avalues) abstraction, compute the avalues which
+ should be inserted in this abstraction before we insert it in the context.
+ Note that this function may update the context: it is necessary when
+ computing borrow projections, for instance.
+ - [ctx]
+*)
+val create_push_abstractions_from_abs_region_groups :
+ V.FunCallId.id ->
+ V.abs_kind ->
+ LA.abs_region_group list ->
+ (T.RegionGroupId.id -> bool) ->
+ (V.abs -> C.eval_ctx -> C.eval_ctx * V.typed_avalue list) ->
+ C.eval_ctx ->
+ C.eval_ctx
+
+(** Evaluate a statement *)
+val eval_statement : C.config -> LA.statement -> st_cm_fun
+
+(** Evaluate a statement seen as a function body *)
+val eval_function_body : C.config -> LA.statement -> st_cm_fun
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index 7b95f41d..5f22506b 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -36,6 +36,9 @@ let paths_log = L.get_logger "MainLogger.Interpreter.Paths"
(** Logger for InterpreterExpansion *)
let expansion_log = L.get_logger "MainLogger.Interpreter.Expansion"
+(** Logger for InterpreterProjectors *)
+let projectors_log = L.get_logger "MainLogger.Interpreter.Projectors"
+
(** Logger for InterpreterBorrows *)
let borrows_log = L.get_logger "MainLogger.Interpreter.Borrows"