diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Driver.ml | 1 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 8 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 80 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.mli | 34 | ||||
| -rw-r--r-- | compiler/InterpreterBorrowsCore.ml | 17 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 66 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.mli | 73 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 126 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.mli | 37 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.ml | 170 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.mli | 105 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.ml | 54 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.mli | 115 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 71 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.mli | 63 | ||||
| -rw-r--r-- | compiler/Logging.ml | 3 |
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" |