diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Cps.ml | 262 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 338 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 362 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 239 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.mli | 46 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 654 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.mli | 39 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.ml | 239 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.mli | 8 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.ml | 193 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.mli | 4 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 567 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.ml | 140 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.mli | 6 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 1280 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.mli | 10 | ||||
| -rw-r--r-- | compiler/InterpreterUtils.ml | 14 | ||||
| -rw-r--r-- | compiler/Invariants.ml | 7 | ||||
| -rw-r--r-- | compiler/SynthesizeSymbolic.ml | 2 |
19 files changed, 2116 insertions, 2294 deletions
diff --git a/compiler/Cps.ml b/compiler/Cps.ml index a3c8f1e1..3f2e2eaa 100644 --- a/compiler/Cps.ml +++ b/compiler/Cps.ml @@ -3,6 +3,7 @@ open Values open Contexts +open Errors (** TODO: change the name *) type eval_error = EPanic @@ -36,172 +37,111 @@ type statement_eval_res = type eval_result = SymbolicAst.expression option -(** Continuation function *) -type m_fun = eval_ctx -> eval_result - -(** Continuation taking another continuation as parameter *) -type cm_fun = m_fun -> m_fun - -(** Continuation taking a typed value as parameter - TODO: use more *) -type typed_value_m_fun = typed_value -> m_fun - -(** Continuation taking another continuation as parameter and a typed - value as parameter. - *) -type typed_value_cm_fun = typed_value -> cm_fun - -(** Type of a continuation used when evaluating a statement *) -type st_m_fun = statement_eval_res -> m_fun - -(** Type of a continuation used when evaluating a statement *) -type st_cm_fun = st_m_fun -> m_fun - -(** Convert a unit function to a cm function *) -let unit_to_cm_fun (f : eval_ctx -> unit) : cm_fun = - fun cf ctx -> - f ctx; - cf ctx - -(** *) -let update_to_cm_fun (f : eval_ctx -> eval_ctx) : cm_fun = - fun cf ctx -> - let ctx = f ctx in - cf ctx - -(** Composition of functions taking continuations as parameters. - We tried to make this as general as possible. *) -let comp (f : 'c -> 'd -> 'e) (g : ('a -> 'b) -> 'c) : ('a -> 'b) -> 'd -> 'e = - fun cf ctx -> f (g cf) ctx - -let comp_unit (f : cm_fun) (g : eval_ctx -> unit) : cm_fun = - comp f (unit_to_cm_fun g) - -let comp_update (f : cm_fun) (g : eval_ctx -> eval_ctx) : cm_fun = - comp f (update_to_cm_fun g) - -(** This is just a test, to check that {!comp} is general enough to handle a case - where a function must compute a value and give it to the continuation. - It happens for functions like {!val:InterpreterExpressions.eval_operand}. - - Keeping this here also makes it a good reference, when one wants to figure - out the signatures he should use for such a composition. - *) -let comp_ret_val (f : (typed_value -> m_fun) -> m_fun) - (g : m_fun -> typed_value -> m_fun) : cm_fun = - comp f g - -let apply (f : cm_fun) (g : m_fun) : m_fun = fun ctx -> f g ctx -let id_cm_fun : cm_fun = fun cf ctx -> cf ctx - -(** If we have a list of [inputs] of type ['a list] and a function [f] which - evaluates one element of type ['a] to compute a result of type ['b] before - giving it to a continuation, the following function performs a fold operation: - it evaluates all the inputs one by one by accumulating the results in a list, - and gives the list to a continuation. - - Note that we make sure that the results are listed in the order in - which they were computed (the first element of the list is the result - of applying [f] to the first element of the inputs). - - See the unit test below for an illustration. - *) -let fold_left_apply_continuation (f : 'a -> ('c -> 'd) -> 'c -> 'd) - (inputs : 'a list) (cf : 'c -> 'd) : 'c -> 'd = - let rec eval_list (inputs : 'a list) (cf : 'c -> 'd) : 'c -> 'd = +(** Function which takes a context as input, and evaluates to: + - a new context + - a continuation with which to build the execution trace, provided the + trace for the end of the execution. + *) +type cm_fun = eval_ctx -> eval_ctx * (eval_result -> eval_result) + +type st_cm_fun = + eval_ctx -> (eval_ctx * statement_eval_res) * (eval_result -> eval_result) + +(** Type of a function used when evaluating a statement *) +type stl_cm_fun = + eval_ctx -> + (eval_ctx * statement_eval_res) list + * (SymbolicAst.expression list option -> eval_result) + +(** Compose continuations that we use to compute execution traces *) +let cc_comp (f : 'b -> 'c) (g : 'a -> 'b) : 'a -> 'c = fun e -> f (g e) + +let comp (f : 'b -> 'c) (g : 'x * ('a -> 'b)) : 'x * ('a -> 'c) = + let x, g = g in + (x, cc_comp f g) + +let comp2 (f : 'b -> 'c) (g : 'x * 'y * ('a -> 'b)) : 'x * 'y * ('a -> 'c) = + let x, y, g = g in + (x, y, cc_comp f g) + +(** [fold] operation for functions which thread a context and return a continuation *) +let fold_left_apply_continuation (f : 'a -> 'c -> 'c * ('e -> 'e)) + (inputs : 'a list) (ctx : 'c) : 'c * ('e -> 'e) = + let rec eval_list (inputs : 'a list) : 'c -> 'b = fun ctx -> match inputs with - | [] -> cf ctx - | x :: inputs -> comp (f x) (fun cf -> eval_list inputs cf) cf ctx + | [] -> (ctx, fun x -> x) + | x :: inputs -> + let ctx, cc = f x ctx in + comp cc (eval_list inputs ctx) in - eval_list inputs cf - -(** Unit test/example for {!fold_left_apply_continuation} *) -let _ = - fold_left_apply_continuation - (fun x cf (ctx : int) -> cf (ctx + x)) - [ 1; 20; 300; 4000 ] - (fun (ctx : int) -> assert (ctx = 4321)) - 0 - -(** If we have a list of [inputs] of type ['a list] and a function [f] which - evaluates one element of type ['a] to compute a result of type ['b] before - giving it to a continuation, the following function performs a fold operation: - it evaluates all the inputs one by one by accumulating the results in a list, - and gives the list to a continuation. - - Note that we make sure that the results are listed in the order in - which they were computed (the first element of the list is the result - of applying [f] to the first element of the inputs). - - See the unit test below for an illustration. - *) -let fold_left_list_apply_continuation (f : 'a -> ('b -> 'c -> 'd) -> 'c -> 'd) - (inputs : 'a list) (cf : 'b list -> 'c -> 'd) : 'c -> 'd = - let rec eval_list (inputs : 'a list) (cf : 'b list -> 'c -> 'd) - (outputs : 'b list) : 'c -> 'd = - fun ctx -> + eval_list inputs ctx + +(** [map] operation for functions which thread a context and return a continuation *) +let map_apply_continuation (f : 'a -> 'c -> 'b * 'c * ('e -> 'e)) + (inputs : 'a list) (ctx : 'c) : 'b list * 'c * ('e -> 'e) = + let rec eval_list (inputs : 'a list) (ctx : 'c) : 'b list * 'c * ('e -> 'e) = match inputs with - | [] -> cf (List.rev outputs) ctx + | [] -> ([], ctx, fun e -> e) | x :: inputs -> - comp (f x) (fun cf v -> eval_list inputs cf (v :: outputs)) cf ctx + let v, ctx, cc1 = f x ctx in + let vl, ctx, cc2 = eval_list inputs ctx in + (v :: vl, ctx, cc_comp cc1 cc2) in - eval_list inputs cf [] - -(** Unit test/example for {!fold_left_list_apply_continuation} *) -let _ = - fold_left_list_apply_continuation - (fun x cf (ctx : unit) -> cf (10 + x) ctx) - [ 0; 1; 2; 3; 4 ] - (fun values _ctx -> assert (values = [ 10; 11; 12; 13; 14 ])) - () - -(** Composition of functions taking continuations as parameters. - - We sometimes have the following situation, where we want to compose three - functions [send], [transmit] and [receive] such that: - - those three functions take continuations as parameters - - [send] generates a value and gives it to its continuation - - [receive] expects a value (so we can compose [send] and [receive] like - so: [comp send receive]) - - [transmit] doesn't expect any value and needs to be called between [send] - and [receive] - - In this situation, we need to take the value given by [send] and "transmit" - it to [receive]. - - This is what this function does (see the unit test below for an illustration). - *) -let comp_transmit (f : ('v -> 'm) -> 'n) (g : 'm -> 'm) : ('v -> 'm) -> 'n = - fun cf -> f (fun v -> g (cf v)) - -(** Example of use of {!comp_transmit} - TODO: make "real" unit tests *) -let () = - let return3 (cf : int -> unit -> unit) (ctx : unit) = cf 3 ctx in - let do_nothing (cf : unit -> unit) (ctx : unit) = cf ctx in - let consume3 (x : int) (ctx : unit) : unit = - assert (x = 3); - ctx + eval_list inputs ctx + +let opt_list_to_list_opt (len : int) (el : 'a option list) : 'a list option = + let expr_list = + List.rev + (List.fold_left + (fun acc a -> match a with Some b -> b :: acc | None -> []) + [] el) in - let cc = comp_transmit return3 do_nothing in - let cc = cc consume3 in - cc () - -(** Sometimes, we want to compose a function with a continuation which checks - its computed value and its updated context, before transmitting them + let _ = assert (List.length expr_list = len) in + if Option.is_none (List.hd expr_list) then None else Some expr_list + +let cc_singleton file line meta cf el = + match el with + | Some [ e ] -> cf (Some e) + | Some _ -> internal_error file line meta + | _ -> None + +(** It happens that we need to concatenate lists of results, for + instance when evaluating the branches of a match. When applying + the continuations to build the symbolic expressions, we need + to decompose the list of expressions we get to give it to the + individual continuations for the branches. *) -let comp_check_value (f : ('v -> 'ctx -> 'a) -> 'ctx -> 'b) - (g : 'v -> 'ctx -> unit) : ('v -> 'ctx -> 'a) -> 'ctx -> 'b = - fun cf -> - f (fun v ctx -> - g v ctx; - cf v ctx) - -(** This case is similar to {!comp_check_value}, but even simpler (we only check - the context) - *) -let comp_check_ctx (f : ('ctx -> 'a) -> 'ctx -> 'b) (g : 'ctx -> unit) : - ('ctx -> 'a) -> 'ctx -> 'b = - fun cf -> - f (fun ctx -> - g ctx; - cf ctx) +let comp_seqs (file : string) (line : int) (meta : Meta.meta) + (ls : + ('a list + * (SymbolicAst.expression list option -> SymbolicAst.expression option)) + list) : + 'a list + * (SymbolicAst.expression list option -> SymbolicAst.expression list option) + = + (* Auxiliary function: given a list of expressions el, build the expressions + corresponding to the different branches *) + let rec cc_aux ls el = + match ls with + | [] -> + (* End of the list of branches: there shouldn't be any expression remaining *) + sanity_check file line (el = []) meta; + [] + | (resl, cf) :: ls -> + (* Split the list of expressions between: + - the expressions for the current branch + - the expressions for the remaining branches *) + let el0, el = Collections.List.split_at el (List.length resl) in + (* Compute the expression for the current branch *) + let e0 = cf (Some el0) in + let e0 = + match e0 with None -> internal_error file line meta | Some e -> e + in + (* Compute the expressions for the remaining branches *) + let e = cc_aux ls el in + (* Concatenate *) + e0 :: e + in + let cc el = match el with None -> None | Some el -> Some (cc_aux ls el) in + (List.flatten (fst (List.split ls)), cc) diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index f10c8d3e..aa54ec6c 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -307,7 +307,9 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) let ret_rty = ret_inst_sg.output in (* Move the return value out of the return variable *) let pop_return_value = is_regular_return in - let cf_pop_frame = pop_frame config fdef.item_meta.meta pop_return_value in + let ret_value, ctx, cc = + pop_frame config fdef.item_meta.meta pop_return_value ctx + 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 @@ -328,163 +330,158 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) (* Insert the return value in the return abstractions (by applying * borrow projections) *) - let cf_consume_ret (ret_value : typed_value option) ctx = - let ctx = - if is_regular_return then ( - let ret_value = Option.get ret_value in - let compute_abs_avalues (abs : abs) (ctx : eval_ctx) : - eval_ctx * typed_avalue list = - let ctx, avalue = - apply_proj_borrows_on_input_value config fdef.item_meta.meta ctx - abs.regions abs.ancestors_regions ret_value ret_rty - in - (ctx, [ avalue ]) + let ctx = + if is_regular_return then ( + let ret_value = Option.get ret_value in + let compute_abs_avalues (abs : abs) (ctx : eval_ctx) : + eval_ctx * typed_avalue list = + let ctx, avalue = + apply_proj_borrows_on_input_value config fdef.item_meta.meta ctx + abs.regions abs.ancestors_regions ret_value ret_rty in + (ctx, [ avalue ]) + in - (* Initialize and insert the abstractions in the context. - * - * We take care of allowing to end only the regions which should end (note - * that this is important for soundness: this is part of the borrow checking). - * Also see the documentation of the [can_end] field of [abs] for more - * information. *) - let parent_and_current_rgs = RegionGroupId.Set.add back_id parent_rgs in - let region_can_end rid = - RegionGroupId.Set.mem rid parent_and_current_rgs - in - sanity_check __FILE__ __LINE__ (region_can_end back_id) - fdef.item_meta.meta; - let ctx = - create_push_abstractions_from_abs_region_groups - (fun rg_id -> SynthRet rg_id) - ret_inst_sg.regions_hierarchy region_can_end compute_abs_avalues ctx - in - ctx) - else ctx - in + (* Initialize and insert the abstractions in the context. + * + * We take care of allowing to end only the regions which should end (note + * that this is important for soundness: this is part of the borrow checking). + * Also see the documentation of the [can_end] field of [abs] for more + * information. *) + let parent_and_current_rgs = RegionGroupId.Set.add back_id parent_rgs in + let region_can_end rid = + RegionGroupId.Set.mem rid parent_and_current_rgs + in + sanity_check __FILE__ __LINE__ (region_can_end back_id) + fdef.item_meta.meta; + let ctx = + create_push_abstractions_from_abs_region_groups + (fun rg_id -> SynthRet rg_id) + ret_inst_sg.regions_hierarchy region_can_end compute_abs_avalues ctx + in + ctx) + else ctx + in - (* We now need to end the proper *input* abstractions - pay attention - * to the fact that we end the *input* abstractions, not the *return* - * abstractions (of course, the corresponding return abstractions will - * automatically be ended, because they consumed values coming from the - * input abstractions...) *) - (* End the parent abstractions and the current abstraction - note that we - * end them in an order which follows the regions hierarchy: it should lead - * to generated code which has a better consistency between the parent - * and children backward functions. - * - * Note that we don't end the same abstraction if we are *inside* a loop (i.e., - * we are evaluating an [EndContinue]) or not. - *) - let current_abs_id, end_fun_synth_input = - let fun_abs_id = - (RegionGroupId.nth inst_sg.regions_hierarchy back_id).id + (* We now need to end the proper *input* abstractions - pay attention + * to the fact that we end the *input* abstractions, not the *return* + * abstractions (of course, the corresponding return abstractions will + * automatically be ended, because they consumed values coming from the + * input abstractions...) *) + (* End the parent abstractions and the current abstraction - note that we + * end them in an order which follows the regions hierarchy: it should lead + * to generated code which has a better consistency between the parent + * and children backward functions. + * + * Note that we don't end the same abstraction if we are *inside* a loop (i.e., + * we are evaluating an [EndContinue]) or not. + *) + let current_abs_id, end_fun_synth_input = + let fun_abs_id = (RegionGroupId.nth inst_sg.regions_hierarchy back_id).id in + if not inside_loop then (Some fun_abs_id, true) + else + (* We are inside a loop *) + let pred (abs : abs) = + match abs.kind with + | Loop (_, rg_id', kind) -> + let rg_id' = Option.get rg_id' in + let is_ret = + match kind with LoopSynthInput -> true | LoopCall -> false + in + rg_id' = back_id && is_ret + | _ -> false in - if not inside_loop then (Some fun_abs_id, true) - else - (* We are inside a loop *) - let pred (abs : abs) = + (* There is not necessarily an input synthesis abstraction specifically + for the loop. + If there is none, the input synthesis abstraction is actually the + function input synthesis abstraction. + + Example: + ======== + {[ + fn clear(v: &mut Vec<u32>) { + let mut i = 0; + while i < v.len() { + v[i] = 0; + i += 1; + } + } + ]} + *) + match ctx_find_abs ctx pred with + | None -> + (* The loop gives back nothing for this region group. + Ex.: + {[ + pub fn ignore_input_mut_borrow(_a: &mut u32) { + loop {} + } + ]} + *) + (None, false) + | Some abs -> (Some abs.abs_id, false) + in + log#ldebug + (lazy + ("evaluate_function_symbolic_synthesize_backward_from_return: ending \ + input abstraction: " + ^ Print.option_to_string AbstractionId.to_string current_abs_id)); + + (* Set the proper abstractions as endable *) + let ctx = + let visit_loop_abs = + object + inherit [_] map_eval_ctx + + method! visit_abs _ abs = match abs.kind with - | Loop (_, rg_id', kind) -> + | Loop (loop_id', rg_id', LoopSynthInput) -> + (* We only allow to end the loop synth input abs for the region + group [rg_id] *) + sanity_check __FILE__ __LINE__ + (if Option.is_some loop_id then loop_id = Some loop_id' + else true) + fdef.item_meta.meta; + (* Loop abstractions *) let rg_id' = Option.get rg_id' in - let is_ret = - match kind with LoopSynthInput -> true | LoopCall -> false - in - rg_id' = back_id && is_ret - | _ -> false - in - (* There is not necessarily an input synthesis abstraction specifically - for the loop. - If there is none, the input synthesis abstraction is actually the - function input synthesis abstraction. - - Example: - ======== - {[ - fn clear(v: &mut Vec<u32>) { - let mut i = 0; - while i < v.len() { - v[i] = 0; - i += 1; - } - } - ]} - *) - match ctx_find_abs ctx pred with - | None -> - (* The loop gives back nothing for this region group. - Ex.: - {[ - pub fn ignore_input_mut_borrow(_a: &mut u32) { - loop {} - } - ]} - *) - (None, false) - | Some abs -> (Some abs.abs_id, false) - in - log#ldebug - (lazy - ("evaluate_function_symbolic_synthesize_backward_from_return: ending \ - input abstraction: " - ^ Print.option_to_string AbstractionId.to_string current_abs_id)); - - (* Set the proper abstractions as endable *) - let ctx = - let visit_loop_abs = - object - inherit [_] map_eval_ctx - - method! visit_abs _ abs = - match abs.kind with - | Loop (loop_id', rg_id', LoopSynthInput) -> - (* We only allow to end the loop synth input abs for the region - group [rg_id] *) - sanity_check __FILE__ __LINE__ - (if Option.is_some loop_id then loop_id = Some loop_id' - else true) - fdef.item_meta.meta; - (* Loop abstractions *) - let rg_id' = Option.get rg_id' in - if rg_id' = back_id && inside_loop then - { abs with can_end = true } - else abs - | Loop (loop_id', _, LoopCall) -> - (* We can end all the loop call abstractions *) - sanity_check __FILE__ __LINE__ (loop_id = Some loop_id') - fdef.item_meta.meta; + if rg_id' = back_id && inside_loop then { abs with can_end = true } - | SynthInput rg_id' -> - if rg_id' = back_id && end_fun_synth_input then - { abs with can_end = true } - else abs - | _ -> - (* Other abstractions *) - abs - end - in - visit_loop_abs#visit_eval_ctx () ctx + else abs + | Loop (loop_id', _, LoopCall) -> + (* We can end all the loop call abstractions *) + sanity_check __FILE__ __LINE__ (loop_id = Some loop_id') + fdef.item_meta.meta; + { abs with can_end = true } + | SynthInput rg_id' -> + if rg_id' = back_id && end_fun_synth_input then + { abs with can_end = true } + else abs + | _ -> + (* Other abstractions *) + abs + end in + visit_loop_abs#visit_eval_ctx () ctx + in - let current_abs_id = - match current_abs_id with None -> [] | Some id -> [ id ] - in - 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 fdef.item_meta.meta id cf) - cf target_abs_ids - in - (* Generate the Return node *) - let cf_return : m_fun = - fun ctx -> - match loop_id with - | None -> Some (SA.Return (ctx, None)) - | Some loop_id -> Some (SA.ReturnWithLoop (loop_id, inside_loop)) - in - (* Apply *) - cf_end_target_abs cf_return ctx + let current_abs_id = + match current_abs_id with None -> [] | Some id -> [ id ] + in + let target_abs_ids = List.append parent_input_abs_ids current_abs_id in + let ctx, cc = + comp cc + (fold_left_apply_continuation + (fun id ctx -> end_abstraction config fdef.item_meta.meta id ctx) + target_abs_ids ctx) + in + (* Generate the Return node *) + let return_expr = + match loop_id with + | None -> Some (SA.Return (ctx, None)) + | Some loop_id -> Some (SA.ReturnWithLoop (loop_id, inside_loop)) in - cf_pop_frame cf_consume_ret ctx + (* Apply *) + cc return_expr (** Evaluate a function with the symbolic interpreter. @@ -512,7 +509,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) (* Create the continuation to finish the evaluation *) let config = mk_config SymbolicMode in - let cf_finish (res : statement_eval_res) (ctx : eval_ctx) = + let finish (res : statement_eval_res) (ctx : eval_ctx) = let ctx0 = ctx in log#ldebug (lazy @@ -535,17 +532,13 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) *) (* Forward translation: retrieve the returned value *) let fwd_e = - (* Pop the frame and retrieve the returned value at the same time*) + (* Pop the frame and retrieve the returned value at the same time *) let pop_return_value = true in - let cf_pop = - pop_frame config fdef.item_meta.meta pop_return_value + let ret_value, ctx, cc_pop = + pop_frame config fdef.item_meta.meta pop_return_value ctx in (* Generate the Return node *) - let cf_return ret_value : m_fun = - fun ctx -> Some (SA.Return (ctx, ret_value)) - in - (* Apply *) - cf_pop cf_return ctx + cc_pop (Some (SA.Return (ctx, ret_value))) in let fwd_e = Option.get fwd_e in (* Backward translation: introduce "return" @@ -589,15 +582,11 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) (* Pop the frame - there is no returned value to pop: in the translation we will simply call the loop function *) let pop_return_value = false in - let cf_pop = - pop_frame config fdef.item_meta.meta pop_return_value + let _ret_value, _ctx, cc_pop = + pop_frame config fdef.item_meta.meta pop_return_value ctx in (* Generate the Return node *) - let cf_return _ret_value : m_fun = - fun _ctx -> Some (SA.ReturnWithLoop (loop_id, inside_loop)) - in - (* Apply *) - cf_pop cf_return ctx + cc_pop (Some (SA.ReturnWithLoop (loop_id, inside_loop))) in let fwd_e = Option.get fwd_e in (* Backward translation: introduce "return" @@ -631,10 +620,17 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) (* Evaluate the function *) let symbolic = - try eval_function_body config (Option.get fdef.body).body cf_finish ctx + try + let ctx_resl, cc = + eval_function_body config (Option.get fdef.body).body ctx + in + let el = + List.map Option.get + (List.map (fun (ctx, res) -> finish res ctx) ctx_resl) + in + cc (Some el) with CFailure (meta, msg) -> Some (Error (meta, msg)) in - (* Return *) (input_svs, symbolic) @@ -670,14 +666,12 @@ module Test = struct (* Create the continuation to check the function's result *) let config = mk_config ConcreteMode in - let cf_check (res : statement_eval_res) (ctx : eval_ctx) = + let check (res : statement_eval_res) (ctx : eval_ctx) = match res with | Return -> (* Ok: drop the local variables and finish *) let pop_return_value = true in - pop_frame config fdef.item_meta.meta pop_return_value - (fun _ _ -> None) - ctx + pop_frame config fdef.item_meta.meta pop_return_value ctx | _ -> craise __FILE__ __LINE__ fdef.item_meta.meta ("Unit test failed (concrete execution) on: " @@ -685,9 +679,9 @@ module Test = struct (Print.Contexts.decls_ctx_to_fmt_env decls_ctx) fdef.name) in - (* Evaluate the function *) - let _ = eval_function_body config body.body cf_check ctx in + let ctx_resl, _ = eval_function_body config body.body ctx in + let _ = List.map (fun (ctx, res) -> check res ctx) ctx_resl in () (** Small helper: return true if the function is a *transparent* unit function diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index a158ed9a..f49d39d0 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -826,34 +826,29 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id) craise __FILE__ __LINE__ meta "Unreachable" let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) - (l : BorrowId.id) (ctx0 : eval_ctx) : cm_fun = - let check_disappeared (ctx : eval_ctx) : unit = - let _ = - match lookup_borrow_opt ek_all l ctx with - | None -> () (* Ok *) - | Some _ -> - log#ltrace - (lazy - (fun_name ^ ": " ^ BorrowId.to_string l - ^ ": borrow didn't disappear:\n- original context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx0 - ^ "\n\n- new context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - internal_error __FILE__ __LINE__ meta - in - match lookup_loan_opt meta ek_all l ctx with - | None -> () (* Ok *) - | Some _ -> - log#ltrace - (lazy - (fun_name ^ ": " ^ BorrowId.to_string l - ^ ": loan didn't disappear:\n- original context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx0 - ^ "\n\n- new context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - internal_error __FILE__ __LINE__ meta - in - unit_to_cm_fun check_disappeared + (l : BorrowId.id) (ctx0 : eval_ctx) (ctx : eval_ctx) : unit = + (match lookup_borrow_opt ek_all l ctx with + | None -> () (* Ok *) + | Some _ -> + log#ltrace + (lazy + (fun_name ^ ": " ^ BorrowId.to_string l + ^ ": borrow didn't disappear:\n- original context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ "\n\n- new context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + internal_error __FILE__ __LINE__ meta); + match lookup_loan_opt meta ek_all l ctx with + | None -> () (* Ok *) + | Some _ -> + log#ltrace + (lazy + (fun_name ^ ": " ^ BorrowId.to_string l + ^ ": loan didn't disappear:\n- original context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ "\n\n- new context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + internal_error __FILE__ __LINE__ meta (** End a borrow identified by its borrow id in a context. @@ -879,7 +874,7 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) let rec end_borrow_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids) (allowed_abs : AbstractionId.id option) (l : BorrowId.id) : cm_fun = - fun cf ctx -> + fun ctx -> (* Check that we don't loop *) let chain0 = chain in let chain = @@ -893,7 +888,7 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) (* Utility function for the sanity checks: check that the borrow disappeared * from the context *) let ctx0 = ctx in - let cf_check : cm_fun = check_borrow_disappeared meta "end borrow" l ctx0 in + let check = check_borrow_disappeared meta "end borrow" l ctx0 in (* Start by ending the borrow itself (we lookup it up and replace it with [Bottom] *) let allow_inner_loans = false in match end_borrow_get_borrow meta allowed_abs allow_inner_loans l ctx with @@ -925,31 +920,41 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) * inside another borrow *) let allowed_abs' = None in (* End the outer borrows *) - let cc = end_borrows_aux config meta chain allowed_abs' bids in + let ctx, cc = + end_borrows_aux config meta chain allowed_abs' bids ctx + in (* Retry to end the borrow *) - let cc = comp cc (end_borrow_aux config meta chain0 allowed_abs l) in - (* Check and apply *) - comp cc cf_check cf ctx + let ctx, cc = + comp cc (end_borrow_aux config meta chain0 allowed_abs l ctx) + in + (* Check and continue *) + check ctx; + (ctx, cc) | OuterBorrows (Borrow bid) | InnerLoans (Borrow bid) -> let allowed_abs' = None in (* End the outer borrow *) - let cc = end_borrow_aux config meta chain allowed_abs' bid in + let ctx, cc = end_borrow_aux config meta chain allowed_abs' bid ctx in (* Retry to end the borrow *) - let cc = comp cc (end_borrow_aux config meta chain0 allowed_abs l) in - (* Check and apply *) - comp cc cf_check cf ctx + let ctx, cc = + comp cc (end_borrow_aux config meta chain0 allowed_abs l ctx) + in + (* Check and continue *) + check ctx; + (ctx, cc) | OuterAbs abs_id -> (* The borrow is inside an abstraction: end the whole abstraction *) - let cf_end_abs = end_abstraction_aux config meta chain abs_id in - (* Compose with a sanity check *) - comp cf_end_abs cf_check cf ctx) + let ctx, end_abs = end_abstraction_aux config meta chain abs_id ctx in + (* Sanity check *) + check ctx; + (ctx, end_abs)) | Ok (ctx, None) -> log#ldebug (lazy "End borrow: borrow not found"); (* It is possible that we can't find a borrow in symbolic mode (ending * an abstraction may end several borrows at once *) sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta; (* Do a sanity check and continue *) - cf_check cf ctx + check ctx; + (ctx, fun e -> e) (* We found a borrow and replaced it with [Bottom]: give it back (i.e., update the corresponding loan) *) | Ok (ctx, Some (_, bc)) -> @@ -963,27 +968,27 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) (* Give back the value *) let ctx = give_back config meta l bc ctx in (* Do a sanity check and continue *) - let cc = cf_check in + check ctx; (* Save a snapshot of the environment for the name generation *) - let cc = comp cc SynthesizeSymbolic.cf_save_snapshot in + let cc = SynthesizeSymbolic.save_snapshot ctx in (* Compose *) - cc cf ctx + (ctx, cc) and end_borrows_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids) (allowed_abs : AbstractionId.id option) (lset : BorrowId.Set.t) : cm_fun = - fun cf -> + fun ctx -> (* This is not necessary, but we prefer to reorder the borrow ids, - * so that we actually end from the smallest id to the highest id - just - * a matter of taste, and may make debugging easier *) + 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 = BorrowId.Set.fold (fun id ids -> id :: ids) lset [] in - List.fold_left - (fun cf id -> end_borrow_aux config meta chain allowed_abs id cf) - cf ids + fold_left_apply_continuation + (fun id ctx -> end_borrow_aux config meta chain allowed_abs id ctx) + ids ctx and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun = - fun cf ctx -> + fun ctx -> (* Check that we don't loop *) let chain = add_borrow_or_abs_id_to_chain meta "end_abstraction_aux: " (AbsId abs_id) @@ -1009,7 +1014,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) ("abs not found (already ended): " ^ AbstractionId.to_string abs_id ^ "\n")); - cf ctx + (ctx, fun e -> e) | Some abs -> (* Check that we can end the abstraction *) if abs.can_end then () @@ -1020,86 +1025,78 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) ^ " as it is set as non-endable"); (* End the parent abstractions first *) - let cc = end_abstractions_aux config meta chain abs.parents in - let cc = - comp_unit cc (fun ctx -> - log#ldebug - (lazy - ("end_abstraction_aux: " - ^ AbstractionId.to_string abs_id - ^ "\n- context after parent abstractions ended:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx))) - in + let ctx, cc = end_abstractions_aux config meta chain abs.parents ctx in + log#ldebug + (lazy + ("end_abstraction_aux: " + ^ AbstractionId.to_string abs_id + ^ "\n- context after parent abstractions ended:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* End the loans inside the abstraction *) - let cc = comp cc (end_abstraction_loans config meta chain abs_id) in - let cc = - comp_unit cc (fun ctx -> - log#ldebug - (lazy - ("end_abstraction_aux: " - ^ AbstractionId.to_string abs_id - ^ "\n- context after loans ended:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx))) + let ctx, cc = + comp cc (end_abstraction_loans config meta chain abs_id ctx) in + log#ldebug + (lazy + ("end_abstraction_aux: " + ^ AbstractionId.to_string abs_id + ^ "\n- context after loans ended:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* End the abstraction itself by redistributing the borrows it contains *) - let cc = comp cc (end_abstraction_borrows config meta chain abs_id) in + let ctx, cc = + comp cc (end_abstraction_borrows config meta chain abs_id ctx) + in (* End the regions owned by the abstraction - note that we don't need to - * relookup the abstraction: the set of regions in an abstraction never - * changes... *) - let cc = - comp_update cc (fun ctx -> - let ended_regions = - RegionId.Set.union ctx.ended_regions abs.regions - in - { ctx with ended_regions }) + relookup the abstraction: the set of regions in an abstraction never + changes... *) + let ctx = + let ended_regions = RegionId.Set.union ctx.ended_regions abs.regions in + { ctx with ended_regions } in (* Remove all the references to the id of the current abstraction, and remove - * the abstraction itself. - * **Rk.**: this is where we synthesize the updated symbolic AST *) - let cc = - comp cc (end_abstraction_remove_from_context config meta abs_id) + the abstraction itself. + **Rk.**: this is where we synthesize the updated symbolic AST *) + let ctx, cc = + comp cc (end_abstraction_remove_from_context config meta abs_id ctx) in (* Debugging *) - let cc = - comp_unit cc (fun ctx -> - log#ldebug - (lazy - ("end_abstraction_aux: " - ^ AbstractionId.to_string abs_id - ^ "\n- original context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx0 - ^ "\n\n- new context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx))) - in + log#ldebug + (lazy + ("end_abstraction_aux: " + ^ AbstractionId.to_string abs_id + ^ "\n- original context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ "\n\n- new context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Sanity check: ending an abstraction must preserve the invariants *) - let cc = comp cc (Invariants.cf_check_invariants meta) in + Invariants.check_invariants meta ctx; (* Save a snapshot of the environment for the name generation *) - let cc = comp cc SynthesizeSymbolic.cf_save_snapshot in + let cc = cc_comp cc (SynthesizeSymbolic.save_snapshot ctx) in - (* Apply the continuation *) - cc cf ctx + (* Return *) + (ctx, cc) and end_abstractions_aux (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids) (abs_ids : AbstractionId.Set.t) : cm_fun = - fun cf -> + fun ctx -> (* 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 = AbstractionId.Set.fold (fun id ids -> id :: ids) abs_ids [] in - List.fold_left - (fun cf id -> end_abstraction_aux config meta chain id cf) - cf abs_ids + fold_left_apply_continuation + (fun id ctx -> end_abstraction_aux config meta chain id ctx) + abs_ids ctx and end_abstraction_loans (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun = - fun cf ctx -> + fun ctx -> (* Lookup the abstraction *) let abs = ctx_lookup_abs ctx abs_id in (* End the first loan we find. @@ -1110,32 +1107,28 @@ and end_abstraction_loans (config : config) (meta : Meta.meta) match opt_loan with | None -> (* No loans: nothing to update *) - cf ctx + (ctx, fun e -> e) | Some (BorrowIds bids) -> (* There are loans: end the corresponding borrows, then recheck *) - let cc : cm_fun = + let ctx, cc = match bids with - | Borrow bid -> end_borrow_aux config meta chain None bid - | Borrows bids -> end_borrows_aux config meta chain None bids + | Borrow bid -> end_borrow_aux config meta chain None bid ctx + | Borrows bids -> end_borrows_aux config meta chain None bids ctx in (* Reexplore, looking for loans *) - let cc = comp cc (end_abstraction_loans config meta chain abs_id) in - (* Continue *) - cc cf ctx + comp cc (end_abstraction_loans config meta chain abs_id ctx) | Some (SymbolicValue sv) -> (* There is a proj_loans over a symbolic value: end the proj_borrows - * which intersect this proj_loans, then end the proj_loans itself *) - let cc = - end_proj_loans_symbolic config meta chain abs_id abs.regions sv + which intersect this proj_loans, then end the proj_loans itself *) + let ctx, cc = + end_proj_loans_symbolic config meta chain abs_id abs.regions sv ctx in (* Reexplore, looking for loans *) - let cc = comp cc (end_abstraction_loans config meta chain abs_id) in - (* Continue *) - cc cf ctx + comp cc (end_abstraction_loans config meta chain abs_id ctx) and end_abstraction_borrows (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) : cm_fun = - fun cf ctx -> + fun ctx -> log#ldebug (lazy ("end_abstraction_borrows: abs_id: " ^ AbstractionId.to_string abs_id)); @@ -1202,7 +1195,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) (* Explore the abstraction, looking for borrows *) obj#visit_abs () abs; (* No borrows: nothing to update *) - cf ctx + (ctx, fun e -> e) with (* There are concrete (i.e., not symbolic) borrows: end them, then reexplore *) | FoundABorrowContent bc -> @@ -1256,7 +1249,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) craise __FILE__ __LINE__ meta "Unexpected" in (* Reexplore *) - end_abstraction_borrows config meta chain abs_id cf ctx + end_abstraction_borrows config meta chain abs_id ctx (* There are symbolic borrows: end them, then reexplore *) | FoundAProjBorrows (sv, proj_ty) -> log#ldebug @@ -1273,7 +1266,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) give_back_symbolic_value config meta abs.regions proj_ty sv nsv ctx in (* Reexplore *) - end_abstraction_borrows config meta chain abs_id cf ctx + end_abstraction_borrows config meta chain abs_id ctx (* There are concrete (i.e., not symbolic) borrows in shared values: end them, then reexplore *) | FoundBorrowContent bc -> log#ldebug @@ -1306,18 +1299,16 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) | VReservedMutBorrow _ -> craise __FILE__ __LINE__ meta "Unreachable" in (* Reexplore *) - end_abstraction_borrows config meta chain abs_id cf ctx + end_abstraction_borrows config meta chain abs_id ctx (** Remove an abstraction from the context, as well as all its references *) and end_abstraction_remove_from_context (_config : config) (meta : Meta.meta) (abs_id : AbstractionId.id) : cm_fun = - fun cf ctx -> + fun ctx -> let ctx, abs = ctx_remove_abs meta ctx abs_id in let abs = Option.get abs in - (* Apply the continuation *) - let expr = cf ctx in (* Synthesize the symbolic AST *) - SynthesizeSymbolic.synthesize_end_abstraction ctx abs expr + (ctx, SynthesizeSymbolic.synthesize_end_abstraction ctx abs) (** End a proj_loan over a symbolic value by ending the proj_borrows which intersect this proj_loans. @@ -1336,14 +1327,9 @@ and end_abstraction_remove_from_context (_config : config) (meta : Meta.meta) and end_proj_loans_symbolic (config : config) (meta : Meta.meta) (chain : borrow_or_abs_ids) (abs_id : AbstractionId.id) (regions : RegionId.Set.t) (sv : symbolic_value) : cm_fun = - fun cf ctx -> + fun ctx -> (* Small helpers for sanity checks *) let check ctx = no_aproj_over_symbolic_in_context meta sv ctx in - let cf_check (cf : m_fun) : m_fun = - fun ctx -> - check ctx; - cf ctx - in (* Find the first proj_borrows which intersects the proj_loans *) let explore_shared = true in match @@ -1358,7 +1344,7 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta) (* Sanity check *) check ctx; (* Continue *) - cf ctx + (ctx, fun e -> e) | Some (SharedProjs projs) -> (* We found projectors over shared values - split between the projectors which belong to the current abstraction and the others. @@ -1389,8 +1375,7 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta) List.partition (fun (abs_id', _) -> abs_id' = abs_id) projs in (* End the external borrow projectors (end their abstractions) *) - let cf_end_external : cm_fun = - fun cf ctx -> + let ctx, cc = let abs_ids = List.map fst external_projs in let abs_ids = List.fold_left @@ -1398,25 +1383,20 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta) AbstractionId.Set.empty abs_ids in (* End the abstractions and continue *) - end_abstractions_aux config meta chain abs_ids cf ctx + end_abstractions_aux config meta chain abs_ids ctx in (* End the internal borrows projectors and the loans projector *) - let cf_end_internal : cm_fun = - fun cf ctx -> + let ctx = (* All the proj_borrows are owned: simply erase them *) let ctx = remove_intersecting_aproj_borrows_shared meta regions sv ctx in (* End the loan itself *) - let ctx = update_aproj_loans_to_ended meta abs_id sv ctx in - (* Sanity check *) - check ctx; - (* Continue *) - cf ctx + update_aproj_loans_to_ended meta abs_id sv ctx in - (* Compose and apply *) - let cc = comp cf_end_external cf_end_internal in - cc cf ctx + (* Sanity check *) + check ctx; + (ctx, cc) | Some (NonSharedProj (abs_id', _proj_ty)) -> (* We found one projector of borrows in an abstraction: if it comes * from this abstraction, we can end it directly, otherwise we need @@ -1452,18 +1432,19 @@ and end_proj_loans_symbolic (config : config) (meta : Meta.meta) (* Sanity check *) check ctx; (* Continue *) - cf ctx) + (ctx, fun e -> e)) else (* The borrows proj comes from a different abstraction: end it. *) - let cc = end_abstraction_aux config meta chain abs_id' in + let ctx, cc = end_abstraction_aux config meta chain abs_id' ctx in (* Retry ending the projector of loans *) - let cc = - comp cc (end_proj_loans_symbolic config meta chain abs_id regions sv) + let ctx, cc = + comp cc + (end_proj_loans_symbolic config meta chain abs_id regions sv ctx) in (* Sanity check *) - let cc = comp cc cf_check in - (* Continue *) - cc cf ctx + check ctx; + (* Return *) + (ctx, cc) let end_borrow config (meta : Meta.meta) : BorrowId.id -> cm_fun = end_borrow_aux config meta [] None @@ -1473,18 +1454,16 @@ let end_borrows config (meta : Meta.meta) : BorrowId.Set.t -> cm_fun = let end_abstraction config meta = end_abstraction_aux config meta [] let end_abstractions config meta = end_abstractions_aux config meta [] - -let end_borrow_no_synth config meta id ctx = - get_cf_ctx_no_synth meta (end_borrow config meta id) ctx +let end_borrow_no_synth config meta id ctx = fst (end_borrow config meta id ctx) let end_borrows_no_synth config meta ids ctx = - get_cf_ctx_no_synth meta (end_borrows config meta ids) ctx + fst (end_borrows config meta ids ctx) let end_abstraction_no_synth config meta id ctx = - get_cf_ctx_no_synth meta (end_abstraction config meta id) ctx + fst (end_abstraction config meta id ctx) let end_abstractions_no_synth config meta ids ctx = - get_cf_ctx_no_synth meta (end_abstractions config meta ids) ctx + fst (end_abstractions config meta ids ctx) (** Helper function: see {!activate_reserved_mut_borrow}. @@ -1503,8 +1482,7 @@ let end_abstractions_no_synth config meta ids ctx = The loan to update mustn't be a borrowed value. *) let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id) - (cf : typed_value -> m_fun) : m_fun = - fun ctx -> + (ctx : eval_ctx) : typed_value * eval_ctx = (* Debug *) log#ldebug (lazy @@ -1541,11 +1519,11 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id) meta "There shouldn't be reserved borrows"; (* Update the loan content *) let ctx = update_loan meta ek l (VMutLoan l) ctx in - (* Continue *) - cf sv ctx + (* Return *) + (sv, ctx) | _, Abstract _ -> (* I don't think it is possible to have two-phase borrows involving borrows - * returned by abstractions. I'm not sure how we could handle that anyway. *) + returned by abstractions. I'm not sure how we could handle that anyway. *) craise __FILE__ __LINE__ meta "Can't promote a shared loan to a mutable loan if the loan is inside a \ region abstraction" @@ -1556,34 +1534,29 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id) all: it doesn't touch the corresponding loan). *) let replace_reserved_borrow_with_mut_borrow (meta : Meta.meta) (l : BorrowId.id) - (cf : m_fun) (borrowed_value : typed_value) : m_fun = - fun ctx -> + (borrowed_value : typed_value) (ctx : eval_ctx) : eval_ctx = (* Lookup the reserved borrow - note that we don't go inside borrows/loans: there can't be reserved borrows inside other borrows/loans *) let ek = { enter_shared_loans = false; enter_mut_borrows = false; enter_abs = false } in - let ctx = - match lookup_borrow meta ek l ctx with - | Concrete (VSharedBorrow _ | VMutBorrow (_, _)) -> - craise __FILE__ __LINE__ meta "Expected a reserved mutable borrow" - | Concrete (VReservedMutBorrow _) -> - (* Update it *) - update_borrow meta ek l (VMutBorrow (l, borrowed_value)) ctx - | Abstract _ -> - (* This can't happen for sure *) - craise __FILE__ __LINE__ meta - "Can't promote a shared borrow to a mutable borrow if the borrow is \ - inside a region abstraction" - in - (* Continue *) - cf ctx + match lookup_borrow meta ek l ctx with + | Concrete (VSharedBorrow _ | VMutBorrow (_, _)) -> + craise __FILE__ __LINE__ meta "Expected a reserved mutable borrow" + | Concrete (VReservedMutBorrow _) -> + (* Update it *) + update_borrow meta ek l (VMutBorrow (l, borrowed_value)) ctx + | Abstract _ -> + (* This can't happen for sure *) + craise __FILE__ __LINE__ meta + "Can't promote a shared borrow to a mutable borrow if the borrow is \ + inside a region abstraction" (** Promote a reserved mut borrow to a mut borrow. *) let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) (l : BorrowId.id) : cm_fun = - fun cf ctx -> + fun ctx -> (* Lookup the value *) let ek = { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false } @@ -1597,15 +1570,13 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) match get_first_loan_in_value sv with | Some lc -> (* End the loans *) - let cc = + let ctx, cc = match lc with - | VSharedLoan (bids, _) -> end_borrows config meta bids - | VMutLoan bid -> end_borrow config meta bid + | VSharedLoan (bids, _) -> end_borrows config meta bids ctx + | VMutLoan bid -> end_borrow config meta bid ctx in (* Recursive call *) - let cc = comp cc (promote_reserved_mut_borrow config meta l) in - (* Continue *) - cc cf ctx + comp cc (promote_reserved_mut_borrow config meta l ctx) | None -> (* No loan to end inside the value *) (* Some sanity checks *) @@ -1621,21 +1592,18 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) (* End the borrows which borrow from the value, at the exception of the borrow we want to promote *) let bids = BorrowId.Set.remove l bids in - let cc = end_borrows config meta bids in + let ctx, cc = end_borrows config meta bids ctx 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 * the borrow. *) - let cc = comp cc (promote_shared_loan_to_mut_loan meta l) in + let v, ctx = promote_shared_loan_to_mut_loan meta l ctx in (* Promote the borrow - the value should have been checked by {!promote_shared_loan_to_mut_loan} *) - let cc = - comp cc (fun cf borrowed_value -> - replace_reserved_borrow_with_mut_borrow meta l cf borrowed_value) - in - (* Continue *) - cc cf ctx) + let ctx = replace_reserved_borrow_with_mut_borrow meta l v ctx in + (* Return *) + (ctx, cc)) | _, Abstract _ -> (* I don't think it is possible to have two-phase borrows involving borrows * returned by abstractions. I'm not sure how we could handle that anyway. *) diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index e47fbfbe..39c9bd4a 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -191,8 +191,8 @@ let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool) ctx let apply_symbolic_expansion_non_borrow (config : config) (meta : Meta.meta) - (original_sv : symbolic_value) (expansion : symbolic_expansion) - (ctx : eval_ctx) : eval_ctx = + (original_sv : symbolic_value) (ctx : eval_ctx) + (expansion : symbolic_expansion) : eval_ctx = (* Apply the expansion to non-abstraction values *) let nv = symbolic_expansion_non_borrow_to_value meta original_sv expansion in let at_most_once = false in @@ -288,7 +288,7 @@ let compute_expanded_symbolic_adt_value (meta : Meta.meta) let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta) (original_sv : symbolic_value) (original_sv_place : SA.mplace option) (ref_ty : rty) : cm_fun = - fun cf ctx -> + fun ctx -> (* First, replace the projectors on borrows. * The important point is that the symbolic value to expand may appear * several times, if it has been copied. In this case, we need to introduce @@ -395,17 +395,16 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta) apply_symbolic_expansion_to_avalues config meta allow_reborrows original_sv see ctx in - (* Call the continuation *) - let expr = cf ctx in - (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching meta original_sv - original_sv_place see expr + ( ctx, + (* Update the synthesized program *) + S.synthesize_symbolic_expansion_no_branching meta original_sv + original_sv_place see ) (** TODO: simplify and merge with the other expansion function *) let expand_symbolic_value_borrow (config : config) (meta : Meta.meta) (original_sv : symbolic_value) (original_sv_place : SA.mplace option) (region : region) (ref_ty : rty) (rkind : ref_kind) : cm_fun = - fun cf ctx -> + fun ctx -> sanity_check __FILE__ __LINE__ (region <> RErased) meta; (* Check that we are allowed to expand the reference *) sanity_check __FILE__ __LINE__ @@ -435,99 +434,47 @@ let expand_symbolic_value_borrow (config : config) (meta : Meta.meta) original_sv see ctx in (* Apply the continuation *) - let expr = cf ctx in - (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching meta original_sv - original_sv_place see expr + ( ctx, + fun e -> + (* Update the synthesized program *) + S.synthesize_symbolic_expansion_no_branching meta original_sv + original_sv_place see e ) | RShared -> expand_symbolic_value_shared_borrow config meta original_sv - original_sv_place ref_ty cf ctx - -(** A small helper. - - Apply a branching symbolic expansion to a context and execute all the - branches. Note that the expansion is optional for every branch (this is - used for integer expansion: see {!expand_symbolic_int}). - - [see_cf_l]: list of pairs (optional symbolic expansion, continuation). - We use [None] for the symbolic expansion for the [_] (default) case of the - integer expansions. - The continuation are used to execute the content of the branches, but not - what comes after. - - [cf_after_join]: this continuation is called *after* the branches have been evaluated. - We need this continuation separately (i.e., we can't compose it with the - continuations in [see_cf_l]) because we perform a join *before* calling it. -*) -let apply_branching_symbolic_expansions_non_borrow (config : config) - (meta : Meta.meta) (sv : symbolic_value) (sv_place : SA.mplace option) - (see_cf_l : (symbolic_expansion option * st_cm_fun) list) - (cf_after_join : st_m_fun) : m_fun = - fun ctx -> - sanity_check __FILE__ __LINE__ (see_cf_l <> []) meta; - (* Apply the symbolic expansion in the context and call the continuation *) - let resl = - List.map - (fun (see_opt, cf_br) -> - (* Remember the initial context for printing purposes *) - let ctx0 = ctx in - (* Expansion *) - let ctx = - match see_opt with - | None -> ctx - | Some see -> - apply_symbolic_expansion_non_borrow config meta sv see ctx - in - (* Debug *) - log#ldebug - (lazy - ("apply_branching_symbolic_expansions_non_borrow: " - ^ symbolic_value_to_string ctx0 sv - ^ "\n\n- original context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx0 - ^ "\n\n- new context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx - ^ "\n")); - (* Continuation *) - cf_br cf_after_join ctx) - see_cf_l - in - (* Collect the result: either we computed no subterm, or we computed all - * of them *) - let subterms = - match resl with - | Some _ :: _ -> Some (List.map Option.get resl) - | None :: _ -> - List.iter - (fun res -> sanity_check __FILE__ __LINE__ (res = None) meta) - resl; - None - | _ -> craise __FILE__ __LINE__ meta "Unreachable" - in - (* Synthesize and return *) - let seel = List.map fst see_cf_l in - S.synthesize_symbolic_expansion meta sv sv_place seel subterms + original_sv_place ref_ty ctx let expand_symbolic_bool (config : config) (meta : Meta.meta) - (sv : symbolic_value) (sv_place : SA.mplace option) (cf_true : st_cm_fun) - (cf_false : st_cm_fun) (cf_after_join : st_m_fun) : m_fun = + (sv : symbolic_value) (sv_place : SA.mplace option) : + eval_ctx -> + (eval_ctx * eval_ctx) + * ((SymbolicAst.expression * SymbolicAst.expression) option -> eval_result) + = fun ctx -> (* Compute the expanded value *) let original_sv = sv in - let original_sv_place = sv_place in let rty = original_sv.sv_ty in sanity_check __FILE__ __LINE__ (rty = TLiteral TBool) meta; (* Expand the symbolic value to true or false and continue execution *) let see_true = SeLiteral (VBool true) in let see_false = SeLiteral (VBool false) in - let seel = [ (Some see_true, cf_true); (Some see_false, cf_false) ] in - (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *) - apply_branching_symbolic_expansions_non_borrow config meta original_sv - original_sv_place seel cf_after_join ctx + let seel = [ Some see_true; Some see_false ] in + (* Apply the symbolic expansion *) + let apply_expansion = + apply_symbolic_expansion_non_borrow config meta sv ctx + in + let ctx_true = apply_expansion see_true in + let ctx_false = apply_expansion see_false in + (* Compute the continuation to build the expression *) + let cf e = + let el = match e with Some (a, b) -> Some [ a; b ] | None -> None in + S.synthesize_symbolic_expansion meta sv sv_place seel el + in + (* Return *) + ((ctx_true, ctx_false), cf) let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv : symbolic_value) (sv_place : SA.mplace option) : cm_fun = - fun cf ctx -> + fun ctx -> (* Debug *) log#ldebug (lazy @@ -539,8 +486,7 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) let original_sv = sv in let original_sv_place = sv_place in let rty = original_sv.sv_ty in - let cc : cm_fun = - fun cf ctx -> + let ctx, cc = match rty with (* ADTs *) | TAdt (adt_id, generics) -> @@ -554,45 +500,43 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) let see = Collections.List.to_cons_nil seel in (* Apply in the context *) let ctx = - apply_symbolic_expansion_non_borrow config meta original_sv see ctx + apply_symbolic_expansion_non_borrow config meta original_sv ctx see in - (* Call the continuation *) - let expr = cf ctx in - (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching meta original_sv - original_sv_place see expr + (* Return*) + ( ctx, + (* Update the synthesized program *) + S.synthesize_symbolic_expansion_no_branching meta original_sv + original_sv_place see ) (* Borrows *) | TRef (region, ref_ty, rkind) -> expand_symbolic_value_borrow config meta original_sv original_sv_place - region ref_ty rkind cf ctx + region ref_ty rkind ctx | _ -> craise __FILE__ __LINE__ meta ("expand_symbolic_value_no_branching: unexpected type: " ^ show_rty rty) in (* Debug *) - let cc = - comp_unit cc (fun ctx -> - log#ldebug - (lazy - ("expand_symbolic_value_no_branching: " - ^ symbolic_value_to_string ctx0 sv - ^ "\n\n- original context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx0 - ^ "\n\n- new context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx - ^ "\n")); - (* Sanity check: the symbolic value has disappeared *) - sanity_check __FILE__ __LINE__ - (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) - meta) - in - (* Continue *) - cc cf ctx + log#ldebug + (lazy + ("expand_symbolic_value_no_branching: " + ^ symbolic_value_to_string ctx0 sv + ^ "\n\n- original context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx0 + ^ "\n\n- new context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx + ^ "\n")); + (* Sanity check: the symbolic value has disappeared *) + sanity_check __FILE__ __LINE__ + (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) + meta; + (* Return *) + (ctx, cc) let expand_symbolic_adt (config : config) (meta : Meta.meta) - (sv : symbolic_value) (sv_place : SA.mplace option) - (cf_branches : st_cm_fun) (cf_after_join : st_m_fun) : m_fun = + (sv : symbolic_value) (sv_place : SA.mplace option) : + eval_ctx -> + eval_ctx list * (SymbolicAst.expression list option -> eval_result) = fun ctx -> (* Debug *) log#ldebug (lazy ("expand_symbolic_adt:" ^ symbolic_value_to_string ctx sv)); @@ -612,17 +556,24 @@ let expand_symbolic_adt (config : config) (meta : Meta.meta) ctx in (* Apply *) - let seel = List.map (fun see -> (Some see, cf_branches)) seel in - apply_branching_symbolic_expansions_non_borrow config meta original_sv - original_sv_place seel cf_after_join ctx + let ctx_branches = + List.map (apply_symbolic_expansion_non_borrow config meta sv ctx) seel + in + ( ctx_branches, + S.synthesize_symbolic_expansion meta sv original_sv_place + (List.map (fun el -> Some el) seel) ) | _ -> craise __FILE__ __LINE__ meta ("expand_symbolic_adt: unexpected type: " ^ show_rty rty) let expand_symbolic_int (config : config) (meta : Meta.meta) (sv : symbolic_value) (sv_place : SA.mplace option) - (int_type : integer_type) (tgts : (scalar_value * st_cm_fun) list) - (otherwise : st_cm_fun) (cf_after_join : st_m_fun) : m_fun = + (int_type : integer_type) (tgts : scalar_value list) : + eval_ctx -> + (eval_ctx list * eval_ctx) + * ((SymbolicAst.expression list * SymbolicAst.expression) option -> + eval_result) = + fun ctx -> (* Sanity check *) sanity_check __FILE__ __LINE__ (sv.sv_ty = TLiteral (TInteger int_type)) meta; (* For all the branches of the switch, we expand the symbolic value @@ -630,17 +581,23 @@ let expand_symbolic_int (config : config) (meta : Meta.meta) * For the otherwise branch, we leave the symbolic value as it is * (because this branch doesn't precisely define which should be the * value of the scrutinee...) and simply execute the otherwise statement. - * - * First, generate the list of pairs: - * (optional expansion, statement to execute) *) - let seel = - List.map (fun (v, cf) -> (Some (SeLiteral (VScalar v)), cf)) tgts + (* Substitute the symbolic values to generate the contexts in the branches *) + let seel = List.map (fun v -> SeLiteral (VScalar v)) tgts in + let ctx_branches = + List.map (apply_symbolic_expansion_non_borrow config meta sv ctx) seel in - let seel = List.append seel [ (None, otherwise) ] in - (* Then expand and evaluate - this generates the proper symbolic AST *) - apply_branching_symbolic_expansions_non_borrow config meta sv sv_place seel - cf_after_join + let ctx_otherwise = ctx in + (* Update the symbolic ast *) + let cf e = + match e with + | None -> None + | Some (el, e) -> + let seel = List.map (fun x -> Some x) seel in + S.synthesize_symbolic_expansion meta sv sv_place (seel @ [ None ]) + (Some (el @ [ e ])) + in + ((ctx_branches, ctx_otherwise), cf) (** Expand all the symbolic values which contain borrows. Allows us to restrict ourselves to a simpler model for the projectors over @@ -652,7 +609,7 @@ let expand_symbolic_int (config : config) (meta : Meta.meta) *) let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : cm_fun = - fun cf ctx -> + fun ctx -> (* The visitor object, to look for symbolic values in the concrete environment *) let obj = object @@ -669,20 +626,20 @@ let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : in let rec expand : cm_fun = - fun cf ctx -> + fun ctx -> try (* We reverse the environment before exploring it - this way the values get expanded in a more "logical" order (this is only for convenience) *) obj#visit_env () (List.rev ctx.env); (* Nothing to expand: continue *) - cf ctx + (ctx, fun e -> e) with FoundSymbolicValue sv -> (* Expand and recheck the environment *) log#ldebug (lazy ("greedy_expand_symbolics_with_borrows: about to expand: " ^ symbolic_value_to_string ctx sv)); - let cc : cm_fun = + let ctx, cc = match sv.sv_ty with | TAdt (TAdtId def_id, _) -> (* {!expand_symbolic_value_no_branching} checks if there are branchings, @@ -706,10 +663,10 @@ let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : ("Attempted to greedily expand a recursive definition (option \ [greedy_expand_symbolics_with_borrows] of [config]): " ^ name_to_string ctx def.name) - else expand_symbolic_value_no_branching config meta sv None + else expand_symbolic_value_no_branching config meta sv None ctx | TAdt ((TTuple | TAssumed TBox), _) | TRef (_, _, _) -> (* Ok *) - expand_symbolic_value_no_branching config meta sv None + expand_symbolic_value_no_branching config meta sv None ctx | TAdt (TAssumed (TArray | TSlice | TStr), _) -> (* We can't expand those *) craise __FILE__ __LINE__ meta @@ -718,15 +675,15 @@ let greedy_expand_symbolics_with_borrows (config : config) (meta : Meta.meta) : craise __FILE__ __LINE__ meta "Unreachable" in (* Compose and continue *) - comp cc expand cf ctx + comp cc (expand ctx) in (* Apply *) - expand cf ctx + expand ctx let greedy_expand_symbolic_values (config : config) (meta : Meta.meta) : cm_fun = - fun cf ctx -> + fun ctx -> if Config.greedy_expand_symbolics_with_borrows then ( log#ldebug (lazy "greedy_expand_symbolic_values"); - greedy_expand_symbolics_with_borrows config meta cf ctx) - else cf ctx + greedy_expand_symbolics_with_borrows config meta ctx) + else (ctx, fun e -> e) diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli index 2ea27ea6..7140d55f 100644 --- a/compiler/InterpreterExpansion.mli +++ b/compiler/InterpreterExpansion.mli @@ -15,8 +15,8 @@ val apply_symbolic_expansion_non_borrow : config -> Meta.meta -> symbolic_value -> - symbolic_expansion -> eval_ctx -> + symbolic_expansion -> eval_ctx (** Expand a symhbolic value, without branching *) @@ -28,38 +28,30 @@ val expand_symbolic_value_no_branching : Parameters: - [config] + - [meta] - [sv] - [sv_place] - - [cf_branches]: the continuation to evaluate the branches. This continuation - typically evaluates a [match] statement *after* we have performed the symbolic - expansion (in particular, we can have one continuation for all the branches). - - [cf_after_join]: the continuation for *after* the match (we perform a join - then call it). *) val expand_symbolic_adt : config -> Meta.meta -> symbolic_value -> SA.mplace option -> - st_cm_fun -> - st_m_fun -> - m_fun + eval_ctx -> + eval_ctx list * (SymbolicAst.expression list option -> eval_result) (** Expand a symbolic boolean. Parameters: see {!expand_symbolic_adt}. - The two parameters of type [st_cm_fun] correspond to the [cf_branches] - parameter (here, there are exactly two branches). *) val expand_symbolic_bool : config -> Meta.meta -> symbolic_value -> SA.mplace option -> - st_cm_fun -> - st_cm_fun -> - st_m_fun -> - m_fun + eval_ctx -> + (eval_ctx * eval_ctx) + * ((SymbolicAst.expression * SymbolicAst.expression) option -> eval_result) (** Symbolic integers are expanded upon evaluating a [SwitchInt]. @@ -69,16 +61,11 @@ val expand_symbolic_bool : 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. + + When expanding a "regular" integer for a switch there is always an *otherwise* + branch. We treat it separately: for this reason we return a pair of a list + of evaluation contexts (for the branches which are not the otherwise branch) + and an additional evaluation context for the otherwise branch. *) val expand_symbolic_int : config -> @@ -86,10 +73,11 @@ val expand_symbolic_int : symbolic_value -> SA.mplace option -> integer_type -> - (scalar_value * st_cm_fun) list -> - st_cm_fun -> - st_m_fun -> - m_fun + scalar_value list -> + eval_ctx -> + (eval_ctx list * eval_ctx) + * ((SymbolicAst.expression list * SymbolicAst.expression) option -> + eval_result) (** If this mode is activated through the [config], greedily expand the symbolic values which need to be expanded. See {!type:Contexts.config} for more information. diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 5a4fe7da..5b05dce8 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -26,33 +26,33 @@ let log = Logging.expressions_log *) let expand_primitively_copyable_at_place (config : config) (meta : Meta.meta) (access : access_kind) (p : place) : cm_fun = - fun cf ctx -> + fun ctx -> (* Small helper *) let rec expand : cm_fun = - fun cf ctx -> + fun ctx -> let v = read_place meta access p ctx in match find_first_primitively_copyable_sv_with_borrows ctx.type_ctx.type_infos v with - | None -> cf ctx + | None -> (ctx, fun e -> e) | Some sv -> - let cc = + let ctx, cc = expand_symbolic_value_no_branching config meta sv (Some (mk_mplace meta p ctx)) + ctx in - comp cc expand cf ctx + comp cc (expand ctx) in (* Apply *) - expand cf ctx + expand ctx -(** Read a place (CPS-style function). +(** Read a place. - We also check that the value *doesn't contain bottoms or reserved + We check that the value *doesn't contain bottoms or reserved borrows*. *) -let read_place (meta : Meta.meta) (access : access_kind) (p : place) - (cf : typed_value -> m_fun) : m_fun = - fun ctx -> +let read_place_check (meta : Meta.meta) (access : access_kind) (p : place) + (ctx : eval_ctx) : typed_value = let v = read_place meta access p ctx in (* Check that there are no bottoms in the value *) cassert __FILE__ __LINE__ @@ -62,35 +62,36 @@ let read_place (meta : Meta.meta) (access : access_kind) (p : place) cassert __FILE__ __LINE__ (not (reserved_in_value v)) meta "There should be no reserved borrows in the value"; - (* Call the continuation *) - cf v ctx + (* Return *) + v let access_rplace_reorganize_and_read (config : config) (meta : Meta.meta) (expand_prim_copy : bool) (access : access_kind) (p : place) - (cf : typed_value -> m_fun) : m_fun = - fun ctx -> + (ctx : eval_ctx) : typed_value * eval_ctx * (eval_result -> eval_result) = (* Make sure we can evaluate the path *) - let cc = update_ctx_along_read_place config meta access p in + let ctx, cc = update_ctx_along_read_place config meta access p ctx in (* End the proper loans at the place itself *) - let cc = comp cc (end_loans_at_place config meta access p) in + let ctx, cc = comp cc (end_loans_at_place config meta access p ctx) in (* Expand the copyable values which contain borrows (which are necessarily shared * borrows) *) - let cc = - if expand_prim_copy then - comp cc (expand_primitively_copyable_at_place config meta access p) - else cc + let ctx, cc = + comp cc + (if expand_prim_copy then + expand_primitively_copyable_at_place config meta access p ctx + else (ctx, fun e -> e)) in (* Read the place - note that this checks that the value doesn't contain bottoms *) - let read_place = read_place meta access p in + let ty_value = read_place_check meta access p ctx in (* Compose *) - comp cc read_place cf ctx + (ty_value, ctx, cc) let access_rplace_reorganize (config : config) (meta : Meta.meta) (expand_prim_copy : bool) (access : access_kind) (p : place) : cm_fun = - fun cf ctx -> - access_rplace_reorganize_and_read config meta expand_prim_copy access p - (fun _v -> cf) - ctx + fun ctx -> + let _, ctx, f = + access_rplace_reorganize_and_read config meta expand_prim_copy access p ctx + in + (ctx, f) (** Convert an operand constant operand value to a typed value *) let literal_to_typed_value (meta : Meta.meta) (ty : literal_type) (cv : literal) @@ -220,21 +221,22 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) dest <- f(move x, move y); ... ]} + 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"). + [l0] upon evaluating [move y], if we have already moved the value of x, + 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"). By first "preparing" the operands evaluation, we make sure no such thing happens. To be more precise, we make sure all the updates to borrows triggered by access *and* move operations have already been applied. - Rk.: in the formalization, we always have an explicit "reorganization" step + Rem.: in the formalization, we always have an explicit "reorganization" step 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 + Rem.: 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 the same constraints @@ -242,32 +244,27 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config) *) let prepare_eval_operand_reorganize (config : config) (meta : Meta.meta) (op : operand) : cm_fun = - fun cf ctx -> - let prepare : cm_fun = - fun cf ctx -> - match op with - | Constant _ -> - (* No need to reorganize the context *) - cf ctx - | Copy p -> - (* Access the value *) - let access = Read in - (* Expand the symbolic values, if necessary *) - let expand_prim_copy = true in - access_rplace_reorganize config meta expand_prim_copy access p cf ctx - | Move p -> - (* Access the value *) - let access = Move in - let expand_prim_copy = false in - access_rplace_reorganize config meta expand_prim_copy access p cf ctx - in - (* Apply *) - prepare cf ctx + fun ctx -> + match op with + | Constant _ -> + (* No need to reorganize the context *) + (ctx, fun e -> e) + | Copy p -> + (* Access the value *) + let access = Read in + (* Expand the symbolic values, if necessary *) + let expand_prim_copy = true in + access_rplace_reorganize config meta expand_prim_copy access p ctx + | Move p -> + (* Access the value *) + let access = Move in + let expand_prim_copy = false in + access_rplace_reorganize config meta expand_prim_copy access p ctx (** Evaluate an operand, without reorganizing the context before *) let eval_operand_no_reorganize (config : config) (meta : Meta.meta) - (op : operand) (cf : typed_value -> m_fun) : m_fun = - fun ctx -> + (op : operand) (ctx : eval_ctx) : + typed_value * eval_ctx * (eval_result -> eval_result) = (* Debug *) log#ldebug (lazy @@ -280,26 +277,29 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) | Constant cv -> ( match cv.value with | CLiteral lit -> - cf (literal_to_typed_value meta (ty_as_literal cv.ty) lit) ctx - | CTraitConst (trait_ref, const_name) -> ( + ( literal_to_typed_value meta (ty_as_literal cv.ty) lit, + ctx, + fun e -> e ) + | CTraitConst (trait_ref, const_name) -> let ctx0 = ctx in (* Simply introduce a fresh symbolic value *) let ty = cv.ty in let v = mk_fresh_symbolic_typed_value meta ty in - (* Continue the evaluation *) - let e = cf v ctx in (* Wrap the generated expression *) - match e with - | None -> None - | Some e -> - Some - (SymbolicAst.IntroSymbolic - ( ctx0, - None, - value_as_symbolic meta v.value, - SymbolicAst.VaTraitConstValue (trait_ref, const_name), - e ))) - | CVar vid -> ( + let cf e = + match e with + | None -> None + | Some e -> + Some + (SymbolicAst.IntroSymbolic + ( ctx0, + None, + value_as_symbolic meta v.value, + SymbolicAst.VaTraitConstValue (trait_ref, const_name), + e )) + in + (v, ctx, cf) + | CVar vid -> let ctx0 = ctx in (* In concrete mode: lookup the const generic value. In symbolic mode: introduce a fresh symbolic value. @@ -319,74 +319,59 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) let v = mk_fresh_symbolic_typed_value meta cv.ty in (ctx, v) in - (* Continue *) - let e = cf cv ctx in - (* If we are synthesizing a symbolic AST, it means that we are in symbolic - mode: the value of the const generic is necessarily symbolic. *) - sanity_check __FILE__ __LINE__ (e = None || is_symbolic cv.value) meta; (* We have to wrap the generated expression *) - match e with - | None -> None - | Some e -> - (* If we are synthesizing a symbolic AST, it means that we are in symbolic - mode: the value of the const generic is necessarily symbolic. *) - sanity_check __FILE__ __LINE__ (is_symbolic cv.value) meta; - (* *) - Some - (SymbolicAst.IntroSymbolic - ( ctx0, - None, - value_as_symbolic meta cv.value, - SymbolicAst.VaCgValue vid, - e ))) + let cf e = + match e with + | None -> None + | Some e -> + (* If we are synthesizing a symbolic AST, it means that we are in symbolic + mode: the value of the const generic is necessarily symbolic. *) + sanity_check __FILE__ __LINE__ (is_symbolic cv.value) meta; + (* *) + Some + (SymbolicAst.IntroSymbolic + ( ctx0, + None, + value_as_symbolic meta cv.value, + SymbolicAst.VaCgValue vid, + e )) + in + (cv, ctx, cf) | CFnPtr _ -> craise __FILE__ __LINE__ meta "Function pointers are not supported yet") | Copy p -> (* Access the value *) let access = Read in - let cc = read_place meta access p in + let v = read_place_check meta access p ctx in + (* Sanity checks *) + exec_assert __FILE__ __LINE__ + (not (bottom_in_value ctx.ended_regions v)) + meta "Can not copy a value containing bottom"; + sanity_check __FILE__ __LINE__ + (Option.is_none + (find_first_primitively_copyable_sv_with_borrows + ctx.type_ctx.type_infos v)) + meta; (* Copy the value *) - let copy cf v : m_fun = - fun ctx -> - (* Sanity checks *) - exec_assert __FILE__ __LINE__ - (not (bottom_in_value ctx.ended_regions v)) - meta "Can not copy a value containing bottom"; - sanity_check __FILE__ __LINE__ - (Option.is_none - (find_first_primitively_copyable_sv_with_borrows - ctx.type_ctx.type_infos v)) - meta; - (* Actually perform the copy *) - let allow_adt_copy = false in - let ctx, v = copy_value meta allow_adt_copy config ctx v in - (* Continue *) - cf v ctx - in - (* Compose and apply *) - comp cc copy cf ctx + let allow_adt_copy = false in + let ctx, v = copy_value meta allow_adt_copy config ctx v in + (v, ctx, fun e -> e) | Move p -> (* Access the value *) let access = Move in - let cc = read_place meta access p in + let v = read_place_check meta access p ctx in + (* Check that there are no bottoms in the value we are about to move *) + exec_assert __FILE__ __LINE__ + (not (bottom_in_value ctx.ended_regions v)) + meta "There should be no bottoms in the value we are about to move"; (* Move the value *) - let move cf v : m_fun = - fun ctx -> - (* Check that there are no bottoms in the value we are about to move *) - exec_assert __FILE__ __LINE__ - (not (bottom_in_value ctx.ended_regions v)) - meta "There should be no bottoms in the value we are about to move"; - let bottom : typed_value = { value = VBottom; ty = v.ty } in - let ctx = write_place meta access p bottom ctx in - cf v ctx - in - (* Compose and apply *) - comp cc move cf ctx + let bottom : typed_value = { value = VBottom; ty = v.ty } in + let ctx = write_place meta access p bottom ctx in + (v, ctx, fun e -> e) let eval_operand (config : config) (meta : Meta.meta) (op : operand) - (cf : typed_value -> m_fun) : m_fun = - fun ctx -> + (ctx : eval_ctx) : typed_value * eval_ctx * (eval_result -> eval_result) = (* Debug *) log#ldebug (lazy @@ -394,10 +379,8 @@ let eval_operand (config : config) (meta : Meta.meta) (op : operand) ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n")); (* We reorganize the context, then evaluate the operand *) - comp - (prepare_eval_operand_reorganize config meta op) - (eval_operand_no_reorganize config meta op) - cf ctx + let ctx, cc = prepare_eval_operand_reorganize config meta op ctx in + comp2 cc (eval_operand_no_reorganize config meta op ctx) (** Small utility. @@ -409,63 +392,59 @@ let prepare_eval_operands_reorganize (config : config) (meta : Meta.meta) (** Evaluate several operands. *) let eval_operands (config : config) (meta : Meta.meta) (ops : operand list) - (cf : typed_value list -> m_fun) : m_fun = - fun ctx -> + (ctx : eval_ctx) : + typed_value list * eval_ctx * (eval_result -> eval_result) = (* Prepare the operands *) - let prepare = prepare_eval_operands_reorganize config meta ops in + let ctx, cc = prepare_eval_operands_reorganize config meta ops ctx in (* Evaluate the operands *) - let eval = - fold_left_list_apply_continuation - (eval_operand_no_reorganize config meta) - ops - in - (* Compose and apply *) - comp prepare eval cf ctx + comp2 cc + (map_apply_continuation (eval_operand_no_reorganize config meta) ops ctx) let eval_two_operands (config : config) (meta : Meta.meta) (op1 : operand) - (op2 : operand) (cf : typed_value * typed_value -> m_fun) : m_fun = - let eval_op = eval_operands config meta [ op1; op2 ] in - let use_res cf res = + (op2 : operand) (ctx : eval_ctx) : + (typed_value * typed_value) * eval_ctx * (eval_result -> eval_result) = + let res, ctx, cc = eval_operands config meta [ op1; op2 ] ctx in + let res = match res with - | [ v1; v2 ] -> cf (v1, v2) + | [ v1; v2 ] -> (v1, v2) | _ -> craise __FILE__ __LINE__ meta "Unreachable" in - comp eval_op use_res cf + (res, ctx, cc) let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop) - (op : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun = + (op : operand) (ctx : eval_ctx) : + (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) = (* Evaluate the operand *) - let eval_op = eval_operand config meta op in + let v, ctx, cc = eval_operand config meta op ctx in (* Apply the unop *) - let apply cf (v : typed_value) : m_fun = + let r = match (unop, v.value) with - | Not, VLiteral (VBool b) -> - cf (Ok { v with value = VLiteral (VBool (not b)) }) + | Not, VLiteral (VBool b) -> Ok { v with value = VLiteral (VBool (not b)) } | Neg, VLiteral (VScalar sv) -> ( let i = Z.neg sv.value in match mk_scalar sv.int_ty i with - | Error _ -> cf (Error EPanic) - | Ok sv -> cf (Ok { v with value = VLiteral (VScalar sv) })) + | Error _ -> Error EPanic + | Ok sv -> Ok { v with value = VLiteral (VScalar sv) }) | ( Cast (CastScalar (TInteger src_ty, TInteger tgt_ty)), VLiteral (VScalar sv) ) -> ( (* Cast between integers *) sanity_check __FILE__ __LINE__ (src_ty = sv.int_ty) meta; let i = sv.value in match mk_scalar tgt_ty i with - | Error _ -> cf (Error EPanic) + | Error _ -> Error EPanic | Ok sv -> let ty = TLiteral (TInteger tgt_ty) in let value = VLiteral (VScalar sv) in - cf (Ok { ty; value })) + Ok { ty; value }) | Cast (CastScalar (TBool, TInteger tgt_ty)), VLiteral (VBool sv) -> ( (* Cast bool -> int *) let i = Z.of_int (if sv then 1 else 0) in match mk_scalar tgt_ty i with - | Error _ -> cf (Error EPanic) + | Error _ -> Error EPanic | Ok sv -> let ty = TLiteral (TInteger tgt_ty) in let value = VLiteral (VScalar sv) in - cf (Ok { ty; value })) + Ok { ty; value }) | Cast (CastScalar (TInteger _, TBool)), VLiteral (VScalar sv) -> (* Cast int -> bool *) let b = @@ -477,43 +456,43 @@ let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop) in let value = VLiteral (VBool b) in let ty = TLiteral TBool in - cf (Ok { ty; value }) + Ok { ty; value } | _ -> exec_raise __FILE__ __LINE__ meta "Invalid input for unop" in - comp eval_op apply cf + (r, ctx, cc) let eval_unary_op_symbolic (config : config) (meta : Meta.meta) (unop : unop) - (op : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun = - fun ctx -> + (op : operand) (ctx : eval_ctx) : + (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) = (* Evaluate the operand *) - let eval_op = eval_operand config meta op in + let v, ctx, cc = eval_operand config meta op ctx in (* Generate a fresh symbolic value to store the result *) - let apply cf (v : typed_value) : m_fun = - fun ctx -> - let res_sv_id = fresh_symbolic_value_id () in - let res_sv_ty = - match (unop, v.ty) with - | Not, (TLiteral TBool as lty) -> lty - | Neg, (TLiteral (TInteger _) as lty) -> lty - | Cast (CastScalar (_, tgt_ty)), _ -> TLiteral tgt_ty - | _ -> exec_raise __FILE__ __LINE__ meta "Invalid input for unop" - in - let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in - (* Call the continuation *) - let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in - (* Synthesize the symbolic AST *) - synthesize_unary_op ctx unop v - (mk_opt_place_from_op meta op ctx) - res_sv None expr + let res_sv_id = fresh_symbolic_value_id () in + let res_sv_ty = + match (unop, v.ty) with + | Not, (TLiteral TBool as lty) -> lty + | Neg, (TLiteral (TInteger _) as lty) -> lty + | Cast (CastScalar (_, tgt_ty)), _ -> TLiteral tgt_ty + | _ -> exec_raise __FILE__ __LINE__ meta "Invalid input for unop" in - (* Compose and apply *) - comp eval_op apply cf ctx + let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in + (* Compute the result *) + let res = Ok (mk_typed_value_from_symbolic_value res_sv) in + (* Synthesize the symbolic AST *) + let cc = + cc_comp cc + (synthesize_unary_op ctx unop v + (mk_opt_place_from_op meta op ctx) + res_sv None) + in + (res, ctx, cc) let eval_unary_op (config : config) (meta : Meta.meta) (unop : unop) - (op : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun = + (op : operand) (ctx : eval_ctx) : + (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) = match config.mode with - | ConcreteMode -> eval_unary_op_concrete config meta unop op cf - | SymbolicMode -> eval_unary_op_symbolic config meta unop op cf + | ConcreteMode -> eval_unary_op_concrete config meta unop op ctx + | SymbolicMode -> eval_unary_op_symbolic config meta unop op ctx (** Small helper for [eval_binary_op_concrete]: computes the result of applying the binop *after* the operands have been successfully evaluated @@ -593,86 +572,81 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) | _ -> craise __FILE__ __LINE__ meta "Invalid inputs for binop" let eval_binary_op_concrete (config : config) (meta : Meta.meta) (binop : binop) - (op1 : operand) (op2 : operand) - (cf : (typed_value, eval_error) result -> m_fun) : m_fun = + (op1 : operand) (op2 : operand) (ctx : eval_ctx) : + (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) = (* Evaluate the operands *) - let eval_ops = eval_two_operands config meta op1 op2 in + let (v1, v2), ctx, cc = eval_two_operands config meta op1 op2 ctx in (* Compute the result of the binop *) - let compute cf (res : typed_value * typed_value) = - let v1, v2 = res in - cf (eval_binary_op_concrete_compute meta binop v1 v2) - in - (* Compose and apply *) - comp eval_ops compute cf + let r = eval_binary_op_concrete_compute meta binop v1 v2 in + (* Return *) + (r, ctx, cc) let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop) - (op1 : operand) (op2 : operand) - (cf : (typed_value, eval_error) result -> m_fun) : m_fun = - fun ctx -> + (op1 : operand) (op2 : operand) (ctx : eval_ctx) : + (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) = (* Evaluate the operands *) - let eval_ops = eval_two_operands config meta op1 op2 in - (* Compute the result of applying the binop *) - let compute cf ((v1, v2) : typed_value * typed_value) : m_fun = - fun ctx -> - (* Generate a fresh symbolic value to store the result *) - let res_sv_id = fresh_symbolic_value_id () in - let res_sv_ty = - if binop = Eq || binop = Ne then ( - (* Equality operations *) - sanity_check __FILE__ __LINE__ (v1.ty = v2.ty) meta; - (* Equality/inequality check is primitive only for a subset of types *) - exec_assert __FILE__ __LINE__ (ty_is_copyable v1.ty) meta - "The type is not primitively copyable"; - TLiteral TBool) - else - (* Other operations: input types are integers *) - match (v1.ty, v2.ty) with - | TLiteral (TInteger int_ty1), TLiteral (TInteger int_ty2) -> ( - match binop with - | Lt | Le | Ge | Gt -> - sanity_check __FILE__ __LINE__ (int_ty1 = int_ty2) meta; - TLiteral TBool - | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr -> - sanity_check __FILE__ __LINE__ (int_ty1 = int_ty2) meta; - TLiteral (TInteger int_ty1) - (* These return `(int, bool)` which isn't a literal type *) - | CheckedAdd | CheckedSub | CheckedMul -> - craise __FILE__ __LINE__ meta - "Checked operations are not implemented" - | Shl | Shr -> - (* The number of bits can be of a different integer type - than the operand *) - TLiteral (TInteger int_ty1) - | Ne | Eq -> craise __FILE__ __LINE__ meta "Unreachable") - | _ -> craise __FILE__ __LINE__ meta "Invalid inputs for binop" - in - let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in - (* Call the continuattion *) - let v = mk_typed_value_from_symbolic_value res_sv in - let expr = cf (Ok v) ctx in - (* Synthesize the symbolic AST *) - let p1 = mk_opt_place_from_op meta op1 ctx in - let p2 = mk_opt_place_from_op meta op2 ctx in - synthesize_binary_op ctx binop v1 p1 v2 p2 res_sv None expr + let (v1, v2), ctx, cc = eval_two_operands config meta op1 op2 ctx in + (* Generate a fresh symbolic value to store the result *) + let res_sv_id = fresh_symbolic_value_id () in + let res_sv_ty = + if binop = Eq || binop = Ne then ( + (* Equality operations *) + sanity_check __FILE__ __LINE__ (v1.ty = v2.ty) meta; + (* Equality/inequality check is primitive only for a subset of types *) + exec_assert __FILE__ __LINE__ (ty_is_copyable v1.ty) meta + "The type is not primitively copyable"; + TLiteral TBool) + else + (* Other operations: input types are integers *) + match (v1.ty, v2.ty) with + | TLiteral (TInteger int_ty1), TLiteral (TInteger int_ty2) -> ( + match binop with + | Lt | Le | Ge | Gt -> + sanity_check __FILE__ __LINE__ (int_ty1 = int_ty2) meta; + TLiteral TBool + | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr -> + sanity_check __FILE__ __LINE__ (int_ty1 = int_ty2) meta; + TLiteral (TInteger int_ty1) + (* These return `(int, bool)` which isn't a literal type *) + | CheckedAdd | CheckedSub | CheckedMul -> + craise __FILE__ __LINE__ meta + "Checked operations are not implemented" + | Shl | Shr -> + (* The number of bits can be of a different integer type + than the operand *) + TLiteral (TInteger int_ty1) + | Ne | Eq -> craise __FILE__ __LINE__ meta "Unreachable") + | _ -> craise __FILE__ __LINE__ meta "Invalid inputs for binop" + in + let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in + let v = mk_typed_value_from_symbolic_value res_sv in + (* Synthesize the symbolic AST *) + let p1 = mk_opt_place_from_op meta op1 ctx in + let p2 = mk_opt_place_from_op meta op2 ctx in + let cc = + cc_comp cc (synthesize_binary_op ctx binop v1 p1 v2 p2 res_sv None) in (* Compose and apply *) - comp eval_ops compute cf ctx + (Ok v, ctx, cc) let eval_binary_op (config : config) (meta : Meta.meta) (binop : binop) - (op1 : operand) (op2 : operand) - (cf : (typed_value, eval_error) result -> m_fun) : m_fun = + (op1 : operand) (op2 : operand) (ctx : eval_ctx) : + (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) = match config.mode with - | ConcreteMode -> eval_binary_op_concrete config meta binop op1 op2 cf - | SymbolicMode -> eval_binary_op_symbolic config meta binop op1 op2 cf + | ConcreteMode -> eval_binary_op_concrete config meta binop op1 op2 ctx + | SymbolicMode -> eval_binary_op_symbolic config meta binop op1 op2 ctx +(** Evaluate an rvalue which creates a reference (i.e., an rvalue which is + `&p` or `&mut p` or `&two-phase p`) *) let eval_rvalue_ref (config : config) (meta : Meta.meta) (p : place) - (bkind : borrow_kind) (cf : typed_value -> m_fun) : m_fun = - fun ctx -> + (bkind : borrow_kind) (ctx : eval_ctx) : + typed_value * eval_ctx * (eval_result -> eval_result) = match bkind with | BShared | BTwoPhaseMut | BShallow -> (* **REMARK**: we initially treated shallow borrows like shared borrows. In practice this restricted the behaviour too much, so for now we - forbid them. + forbid them and remove them in the prepasses (see the comments there + as to why this is sound). *) sanity_check __FILE__ __LINE__ (bkind <> BShallow) meta; @@ -685,86 +659,75 @@ let eval_rvalue_ref (config : config) (meta : Meta.meta) (p : place) in let expand_prim_copy = false in - let prepare = + let v, ctx, cc = access_rplace_reorganize_and_read config meta expand_prim_copy access p + ctx in - (* Evaluate the borrowing operation *) - let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun = - fun ctx -> - (* Generate the fresh borrow id *) - let bid = fresh_borrow_id () in - (* Compute the loan value, with which to replace the value at place p *) - let nv = - match v.value with - | VLoan (VSharedLoan (bids, sv)) -> - (* Shared loan: insert the new borrow id *) - let bids1 = BorrowId.Set.add bid bids in - { v with value = VLoan (VSharedLoan (bids1, sv)) } - | _ -> - (* Not a shared loan: add a wrapper *) - let v' = VLoan (VSharedLoan (BorrowId.Set.singleton bid, v)) in - { v with value = v' } - in - (* Update the borrowed value in the context *) - let ctx = write_place meta 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 ref_kind = - match bkind with - | BShared | BShallow -> RShared - | BTwoPhaseMut -> RMut - | _ -> craise __FILE__ __LINE__ meta "Unreachable" - in - let rv_ty = TRef (RErased, v.ty, ref_kind) in - let bc = - match bkind with - | BShared | BShallow -> - (* See the remark at the beginning of the match branch: we - handle shallow borrows like shared borrows *) - VSharedBorrow bid - | BTwoPhaseMut -> VReservedMutBorrow bid - | _ -> craise __FILE__ __LINE__ meta "Unreachable" - in - let rv : typed_value = { value = VBorrow bc; ty = rv_ty } in - (* Continue *) - cf rv ctx + (* Generate the fresh borrow id *) + let bid = fresh_borrow_id () in + (* Compute the loan value, with which to replace the value at place p *) + let nv = + match v.value with + | VLoan (VSharedLoan (bids, sv)) -> + (* Shared loan: insert the new borrow id *) + let bids1 = BorrowId.Set.add bid bids in + { v with value = VLoan (VSharedLoan (bids1, sv)) } + | _ -> + (* Not a shared loan: add a wrapper *) + let v' = VLoan (VSharedLoan (BorrowId.Set.singleton bid, v)) in + { v with value = v' } in - (* Compose and apply *) - comp prepare eval cf ctx + (* Update the value in the context to replace it with the loan *) + let ctx = write_place meta access p nv ctx in + (* Compute the rvalue - simply a shared borrow with the fresh id. + * Note that the reference is *mutable* if we do a two-phase borrow *) + let ref_kind = + match bkind with + | BShared | BShallow -> RShared + | BTwoPhaseMut -> RMut + | _ -> craise __FILE__ __LINE__ meta "Unreachable" + in + let rv_ty = TRef (RErased, v.ty, ref_kind) in + let bc = + match bkind with + | BShared | BShallow -> + (* See the remark at the beginning of the match branch: we + handle shallow borrows like shared borrows *) + VSharedBorrow bid + | BTwoPhaseMut -> VReservedMutBorrow bid + | _ -> craise __FILE__ __LINE__ meta "Unreachable" + in + let rv : typed_value = { value = VBorrow bc; ty = rv_ty } in + (* Return *) + (rv, ctx, cc) | BMut -> (* Access the value *) let access = Write in let expand_prim_copy = false in - let prepare = + let v, ctx, cc = access_rplace_reorganize_and_read config meta expand_prim_copy access p + ctx in - (* Evaluate the borrowing operation *) - let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun = - fun ctx -> - (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *) - let bid = fresh_borrow_id () in - let rv_ty = TRef (RErased, v.ty, RMut) in - let rv : typed_value = - { value = VBorrow (VMutBorrow (bid, v)); ty = rv_ty } - in - (* Compute the value with which to replace the value at place p *) - let nv = { v with value = VLoan (VMutLoan bid) } in - (* Update the value in the context *) - let ctx = write_place meta access p nv ctx in - (* Continue *) - cf rv ctx + (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *) + let bid = fresh_borrow_id () in + let rv_ty = TRef (RErased, v.ty, RMut) in + let rv : typed_value = + { value = VBorrow (VMutBorrow (bid, v)); ty = rv_ty } in - (* Compose and apply *) - comp prepare eval cf ctx + (* Compute the loan value with which to replace the value at place p *) + let nv = { v with value = VLoan (VMutLoan bid) } in + (* Update the value in the context to replace it with the loan *) + let ctx = write_place meta access p nv ctx in + (* Return *) + (rv, ctx, cc) let eval_rvalue_aggregate (config : config) (meta : Meta.meta) - (aggregate_kind : aggregate_kind) (ops : operand list) - (cf : typed_value -> m_fun) : m_fun = + (aggregate_kind : aggregate_kind) (ops : operand list) (ctx : eval_ctx) : + typed_value * eval_ctx * (eval_result -> eval_result) = (* Evaluate the operands *) - let eval_ops = eval_operands config meta ops in + let values, ctx, cc = eval_operands config meta ops ctx in (* Compute the value *) - let compute (cf : typed_value -> m_fun) (values : typed_value list) : m_fun = - fun ctx -> + let v, cf_compute = (* Match on the aggregate kind *) match aggregate_kind with | AggregatedAdt (type_id, opt_variant_id, generics) -> ( @@ -775,8 +738,7 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) let generics = mk_generic_args [] tys [] [] in let ty = TAdt (TTuple, generics) in let aggregated : typed_value = { value = v; ty } in - (* Call the continuation *) - cf aggregated ctx + (aggregated, fun e -> e) | TAdtId def_id -> (* Sanity checks *) let type_decl = ctx_lookup_type_decl ctx def_id in @@ -799,9 +761,9 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) let aty = TAdt (TAdtId def_id, generics) in let aggregated : typed_value = { value = VAdt av; ty = aty } in (* Call the continuation *) - cf aggregated ctx + (aggregated, fun e -> e) | TAssumed _ -> craise __FILE__ __LINE__ meta "Unreachable") - | AggregatedArray (ety, cg) -> ( + | AggregatedArray (ety, cg) -> (* Sanity check: all the values have the proper type *) sanity_check __FILE__ __LINE__ (List.for_all (fun (v : typed_value) -> v.ty = ety) values) @@ -819,38 +781,36 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) code: by introducing a symbolic value we introduce a let-binding in the generated code. *) let saggregated = mk_fresh_symbolic_typed_value meta ty in - (* Call the continuation *) - match cf saggregated ctx with - | None -> None - | Some e -> - (* Introduce the symbolic value in the AST *) - let sv = ValuesUtils.value_as_symbolic meta saggregated.value in - Some (SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e))) + (* Update the symbolic ast *) + let cf e = + match e with + | None -> None + | Some e -> + (* Introduce the symbolic value in the AST *) + let sv = ValuesUtils.value_as_symbolic meta saggregated.value in + Some + (SymbolicAst.IntroSymbolic (ctx, None, sv, VaArray values, e)) + in + (saggregated, cf) | AggregatedClosure _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet" in - (* Compose and apply *) - comp eval_ops compute cf + (v, ctx, cc_comp cc cf_compute) let eval_rvalue_not_global (config : config) (meta : Meta.meta) - (rvalue : rvalue) (cf : (typed_value, eval_error) result -> m_fun) : m_fun = - fun ctx -> + (rvalue : rvalue) (ctx : eval_ctx) : + (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) = log#ldebug (lazy "eval_rvalue"); - (* Small helpers *) - let wrap_in_result (cf : (typed_value, eval_error) result -> m_fun) - (v : typed_value) : m_fun = - cf (Ok v) - in - let comp_wrap f = comp f wrap_in_result cf in + (* Small helper *) + let wrap_in_result (v, ctx, cc) = (Ok v, ctx, cc) in (* Delegate to the proper auxiliary function *) match rvalue with - | Use op -> comp_wrap (eval_operand config meta op) ctx - | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config meta p bkind) ctx - | UnaryOp (unop, op) -> eval_unary_op config meta unop op cf ctx - | BinaryOp (binop, op1, op2) -> - eval_binary_op config meta binop op1 op2 cf ctx + | Use op -> wrap_in_result (eval_operand config meta op ctx) + | RvRef (p, bkind) -> wrap_in_result (eval_rvalue_ref config meta p bkind ctx) + | UnaryOp (unop, op) -> eval_unary_op config meta unop op ctx + | BinaryOp (binop, op1, op2) -> eval_binary_op config meta binop op1 op2 ctx | Aggregate (aggregate_kind, ops) -> - comp_wrap (eval_rvalue_aggregate config meta aggregate_kind ops) ctx + wrap_in_result (eval_rvalue_aggregate config meta aggregate_kind ops ctx) | Discriminant _ -> craise __FILE__ __LINE__ meta "Unreachable: discriminant reads should have been eliminated from the \ @@ -858,16 +818,12 @@ let eval_rvalue_not_global (config : config) (meta : Meta.meta) | Global _ -> craise __FILE__ __LINE__ meta "Unreachable" let eval_fake_read (config : config) (meta : Meta.meta) (p : place) : cm_fun = - fun cf ctx -> + fun ctx -> let expand_prim_copy = false in - let cf_prepare cf = - access_rplace_reorganize_and_read config meta expand_prim_copy Read p cf + let v, ctx, cc = + access_rplace_reorganize_and_read config meta expand_prim_copy Read p ctx in - let cf_continue cf v : m_fun = - fun ctx -> - cassert __FILE__ __LINE__ - (not (bottom_in_value ctx.ended_regions v)) - meta "Fake read: the value contains bottom"; - cf ctx - in - comp cf_prepare cf_continue cf ctx + cassert __FILE__ __LINE__ + (not (bottom_in_value ctx.ended_regions v)) + meta "Fake read: the value contains bottom"; + (ctx, cc) diff --git a/compiler/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli index 0fb12180..049cee95 100644 --- a/compiler/InterpreterExpressions.mli +++ b/compiler/InterpreterExpressions.mli @@ -4,30 +4,17 @@ open Contexts open Cps open InterpreterPaths -(** Read a place (CPS-style function). - - We also check that the value *doesn't contain bottoms or reserved - borrows*. - - This function doesn't reorganize the context to make sure we can read - the place. If needs be, you should call {!InterpreterPaths.update_ctx_along_read_place} first. - *) -val read_place : - Meta.meta -> access_kind -> place -> (typed_value -> m_fun) -> m_fun - (** Auxiliary function. - Prepare the access to a place in a right-value (typically an operand) by - reorganizing the environment. + Prepare the access to a place in a right-value (typically an operand) by reorganizing + the environment to end outer loans, then read the value and check that this value + *doesn't contain any bottom nor reserved borrows*. We reorganize the environment so that: - we can access the place (we prepare *along* the path) - the value at the place itself doesn't contain loans (the [access_kind] controls whether we only end mutable loans, or also shared loans). - We also check, after the reorganization, that the value at the place - *doesn't contain any bottom nor reserved borrows*. - [expand_prim_copy]: if [true], expand the symbolic values which are primitively copyable and contain borrows. *) @@ -37,8 +24,8 @@ val access_rplace_reorganize_and_read : bool -> access_kind -> place -> - (typed_value -> m_fun) -> - m_fun + eval_ctx -> + typed_value * eval_ctx * (eval_result -> eval_result) (** Evaluate an operand. @@ -50,11 +37,19 @@ val access_rplace_reorganize_and_read : Use {!eval_operands} instead. *) val eval_operand : - config -> Meta.meta -> operand -> (typed_value -> m_fun) -> m_fun + config -> + Meta.meta -> + operand -> + eval_ctx -> + typed_value * eval_ctx * (eval_result -> eval_result) (** Evaluate several operands at once. *) val eval_operands : - config -> Meta.meta -> operand list -> (typed_value list -> m_fun) -> m_fun + config -> + Meta.meta -> + operand list -> + eval_ctx -> + typed_value list * eval_ctx * (eval_result -> eval_result) (** Evaluate an rvalue which is not a global (globals are handled elsewhere). @@ -67,8 +62,8 @@ val eval_rvalue_not_global : config -> Meta.meta -> rvalue -> - ((typed_value, eval_error) result -> m_fun) -> - m_fun + eval_ctx -> + (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) (** Evaluate a fake read (update the context so that we can read a place) *) val eval_fake_read : config -> Meta.meta -> place -> cm_fun diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index e4370367..3264bd18 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -15,37 +15,37 @@ open Errors let log = Logging.loops_log (** Evaluate a loop in concrete mode *) -let eval_loop_concrete (meta : Meta.meta) (eval_loop_body : st_cm_fun) : - st_cm_fun = - fun cf ctx -> +let eval_loop_concrete (meta : Meta.meta) (eval_loop_body : stl_cm_fun) : + stl_cm_fun = + fun ctx -> (* We need a loop id for the [LoopReturn]. In practice it won't be used (it is useful only for the symbolic execution *) let loop_id = fresh_loop_id () in - (* Continuation for after we evaluate the loop body: depending the result - of doing one loop iteration: - - redoes a loop iteration - - exits the loop - - other... + (* Function to recursively evaluate the loop We need a specific function because of the {!Continue} case: in case we continue, we might have to reevaluate the current loop body with the new context (and repeat this an indefinite number of times). *) - let rec reeval_loop_body (res : statement_eval_res) : m_fun = + let rec rec_eval_loop_body (ctx : eval_ctx) (res : statement_eval_res) = log#ldebug (lazy "eval_loop_concrete: reeval_loop_body"); match res with - | Return -> cf (LoopReturn loop_id) - | Panic -> cf Panic + | Return -> [ (ctx, LoopReturn loop_id) ] + | Panic -> [ (ctx, Panic) ] | Break i -> - (* Break out of the loop by calling the continuation *) + (* Break out of the loop *) let res = if i = 0 then Unit else Break (i - 1) in - cf res + [ (ctx, res) ] | Continue 0 -> (* Re-evaluate the loop body *) - eval_loop_body reeval_loop_body + let ctx_resl, _ = eval_loop_body ctx in + let ctx_res_cfl = + List.map (fun (ctx, res) -> rec_eval_loop_body ctx res) ctx_resl + in + List.flatten ctx_res_cfl | Continue i -> (* Continue to an outer loop *) - cf (Continue (i - 1)) + [ (ctx, Continue (i - 1)) ] | Unit -> (* We can't get there. * Note that if we decide not to fail here but rather do @@ -60,13 +60,20 @@ let eval_loop_concrete (meta : Meta.meta) (eval_loop_body : st_cm_fun) : craise __FILE__ __LINE__ meta "Unreachable" in - (* Apply *) - eval_loop_body reeval_loop_body ctx + (* Apply - for the first iteration, we use the result `Continue 0` to evaluate + the loop body at least once *) + let ctx_resl = rec_eval_loop_body ctx (Continue 0) in + (* If we evaluate in concrete mode, we shouldn't have to generate any symbolic expression *) + let cf el = + sanity_check __FILE__ __LINE__ (el = None) meta; + None + in + (ctx_resl, cf) (** Evaluate a loop in symbolic mode *) let eval_loop_symbolic (config : config) (meta : meta) - (eval_loop_body : st_cm_fun) : st_cm_fun = - fun cf ctx -> + (eval_loop_body : stl_cm_fun) : stl_cm_fun = + fun ctx -> (* Debug *) log#ldebug (lazy @@ -100,21 +107,22 @@ let eval_loop_symbolic (config : config) (meta : meta) loop entry with the fixed point: in the synthesized code, the function will end with a call to the loop translation *) - (* First, preemptively end borrows/move values by matching the current - context with the target context *) - let cf_prepare_ctx cf ctx = - log#ldebug - (lazy - ("eval_loop_symbolic: about to reorganize the original context to \ - match the fixed-point ctx with it:\n\ - - src ctx (fixed-point ctx):\n" ^ eval_ctx_to_string fp_ctx - ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ctx)); + let ((res_fun_end, cf_fun_end), fp_bl_corresp) : + ((eval_ctx * statement_eval_res) * (eval_result -> eval_result)) * _ = + (* First, preemptively end borrows/move values by matching the current + context with the target context *) + let ctx, cf_prepare = + log#ldebug + (lazy + ("eval_loop_symbolic: about to reorganize the original context to \ + match the fixed-point ctx with it:\n\ + - src ctx (fixed-point ctx):\n" ^ eval_ctx_to_string fp_ctx + ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ctx)); - prepare_match_ctx_with_target config meta loop_id fixed_ids fp_ctx cf ctx - in + prepare_match_ctx_with_target config meta loop_id fixed_ids fp_ctx ctx + in - (* Actually match *) - let cf_match_ctx cf ctx = + (* Actually match *) log#ldebug (lazy ("eval_loop_symbolic: about to compute the id correspondance between \ @@ -134,30 +142,42 @@ let eval_loop_symbolic (config : config) (meta : meta) ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - let end_expr : SymbolicAst.expression option = - match_ctx_with_target config meta loop_id true fp_bl_corresp - fp_input_svalues fixed_ids fp_ctx cf ctx + + (* Compute the end expression, that is the expresion corresponding to the + end of the functin where we call the loop (for now, when calling a loop + we never get out) *) + let res_fun_end = + comp cf_prepare + (match_ctx_with_target config meta loop_id true fp_bl_corresp + fp_input_svalues fixed_ids fp_ctx ctx) in - log#ldebug - (lazy - "eval_loop_symbolic: matched the fixed-point context with the original \ - context"); - - (* Synthesize the loop body by evaluating it, with the continuation for - after the loop starting at the *fixed point*, but with a special - treatment for the [Break] and [Continue] cases *) - let cf_loop : st_m_fun = - fun res ctx -> - log#ldebug (lazy "eval_loop_symbolic: cf_loop"); + (res_fun_end, fp_bl_corresp) + in + log#ldebug + (lazy + "eval_loop_symbolic: matched the fixed-point context with the original \ + context"); + + (* Synthesize the loop body *) + let (resl_loop_body, cf_loop_body) : + (eval_ctx * statement_eval_res) list + * (SymbolicAst.expression list option -> eval_result) = + (* First, evaluate the loop body starting from the **fixed-point** context *) + let ctx_resl, cf_loop = eval_loop_body fp_ctx in + + (* Then, do a special treatment of the break and continue cases. + For now, we forbid having breaks in loops (and eliminate breaks + in the prepasses) *) + let eval_after_loop_iter (ctx, res) = + log#ldebug (lazy "eval_loop_symbolic: eval_after_loop_iter"); match res with | Return -> (* We replace the [Return] with a [LoopReturn] *) - cf (LoopReturn loop_id) ctx - | Panic -> cf res ctx - | Break i -> - (* Break out of the loop by calling the continuation *) - let res = if i = 0 then Unit else Break (i - 1) in - cf res ctx + ((ctx, LoopReturn loop_id), fun e -> e) + | Panic -> ((ctx, res), fun e -> e) + | Break _ -> + (* Breaks should have been eliminated in the prepasses *) + craise __FILE__ __LINE__ meta "Unexpected break" | Continue i -> (* We don't support nested loops for now *) cassert __FILE__ __LINE__ (i = 0) meta @@ -170,44 +190,58 @@ let eval_loop_symbolic (config : config) (meta : meta) ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx ^ "\n\n-tgt ctx (ctx at continue):\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - let cc = - match_ctx_with_target config meta loop_id false fp_bl_corresp - fp_input_svalues fixed_ids fp_ctx - in - cc cf ctx + match_ctx_with_target config meta loop_id false fp_bl_corresp + fp_input_svalues fixed_ids fp_ctx ctx | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}. For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now. *) craise __FILE__ __LINE__ meta "Unreachable" in - let loop_expr = eval_loop_body cf_loop fp_ctx in - log#ldebug - (lazy - ("eval_loop_symbolic: result:" ^ "\n- src context:\n" - ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx - ^ "\n- fixed point:\n" - ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp_ctx - ^ "\n- fixed_sids: " - ^ SymbolicValueId.Set.show fixed_ids.sids - ^ "\n- fresh_sids: " - ^ SymbolicValueId.Set.show fresh_sids - ^ "\n- input_svalues: " - ^ Print.list_to_string (symbolic_value_to_string ctx) input_svalues - ^ "\n\n")); - - (* For every abstraction introduced by the fixed-point, compute the - types of the given back values. - - We need to explore the abstractions, looking for the mutable borrows. - Moreover, we list the borrows in the same order as the loans (this - is important in {!SymbolicToPure}, where we expect the given back - values to have a specific order. - - Also, we filter the backward functions which and - return nothing. - *) + (* Apply and compose *) + let ctx_resl, cfl = List.split (List.map eval_after_loop_iter ctx_resl) in + let cc (el : SymbolicAst.expression list option) : eval_result = + match el with + | None -> None + | Some el -> + let el = + List.map + (fun (cf, e) -> Option.get (cf (Some e))) + (List.combine cfl el) + in + cf_loop (Some el) + in + + (ctx_resl, cc) + in + + log#ldebug + (lazy + ("eval_loop_symbolic: result:" ^ "\n- src context:\n" + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx + ^ "\n- fixed point:\n" + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp_ctx + ^ "\n- fixed_sids: " + ^ SymbolicValueId.Set.show fixed_ids.sids + ^ "\n- fresh_sids: " + ^ SymbolicValueId.Set.show fresh_sids + ^ "\n- input_svalues: " + ^ Print.list_to_string (symbolic_value_to_string ctx) input_svalues + ^ "\n\n")); + + (* For every abstraction introduced by the fixed-point, compute the + types of the given back values. + + We need to explore the abstractions, looking for the mutable borrows. + Moreover, we list the borrows in the same order as the loans (this + is important in {!SymbolicToPure}, where we expect the given back + values to have a specific order. + + Also, we filter the backward functions which and + return nothing. + *) + let rg_to_given_back = let compute_abs_given_back_tys (abs : abs) : rty list = let is_borrow (av : typed_avalue) : bool = match av.value with @@ -258,26 +292,35 @@ let eval_loop_symbolic (config : config) (meta : meta) given_back_tys in - let rg_to_given_back = - RegionGroupId.Map.map compute_abs_given_back_tys rg_to_abs - in + RegionGroupId.Map.map compute_abs_given_back_tys rg_to_abs + in - (* Put together *) - S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back end_expr - loop_expr meta + (* Put everything together *) + let cc (el : SymbolicAst.expression list option) = + match el with + | None -> None + | Some el -> ( + match el with + | [] -> internal_error __FILE__ __LINE__ meta + | e :: el -> + let fun_end_expr = cf_fun_end (Some e) in + let loop_expr = cf_loop_body (Some el) in + S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back + fun_end_expr loop_expr meta) in - (* Compose *) - comp cf_prepare_ctx cf_match_ctx cf ctx + (res_fun_end :: resl_loop_body, cc) -let eval_loop (config : config) (meta : meta) (eval_loop_body : st_cm_fun) : - st_cm_fun = - fun cf ctx -> +let eval_loop (config : config) (meta : meta) (eval_loop_body : stl_cm_fun) : + stl_cm_fun = + fun ctx -> match config.mode with - | ConcreteMode -> eval_loop_concrete meta eval_loop_body cf ctx + | ConcreteMode -> (eval_loop_concrete meta eval_loop_body) ctx | SymbolicMode -> (* Simplify the context by ending the unnecessary borrows/loans and getting rid of the useless symbolic values (which are in anonymous variables) *) - let cc = cleanup_fresh_values_and_abs config meta empty_ids_set in + let ctx, cc = + cleanup_fresh_values_and_abs config meta empty_ids_set ctx + in (* We want to make sure the loop will *not* manipulate shared avalues containing themselves shared loans (i.e., nested shared loans in @@ -297,5 +340,5 @@ let eval_loop (config : config) (meta : meta) (eval_loop_body : st_cm_fun) : introduce *fixed* abstractions, and again later to introduce *non-fixed* abstractions. *) - let cc = comp cc (prepare_ashared_loans meta None) in - comp cc (eval_loop_symbolic config meta eval_loop_body) cf ctx + let ctx, cc = comp cc (prepare_ashared_loans meta None ctx) in + comp cc (eval_loop_symbolic config meta eval_loop_body ctx) diff --git a/compiler/InterpreterLoops.mli b/compiler/InterpreterLoops.mli index 03633861..630e1e12 100644 --- a/compiler/InterpreterLoops.mli +++ b/compiler/InterpreterLoops.mli @@ -60,5 +60,9 @@ open Contexts open Cps open Meta -(** Evaluate a loop *) -val eval_loop : config -> meta -> st_cm_fun -> st_cm_fun +(** Evaluate a loop. + + The `stl_cm_fun` required as input must be the function to evaluate the + loop body (i.e., `eval_statement` applied to the loop body). + *) +val eval_loop : config -> meta -> stl_cm_fun -> stl_cm_fun diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 9ff2fe38..329abcf3 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -25,7 +25,7 @@ exception FoundAbsId of AbstractionId.id *) let rec end_useless_fresh_borrows_and_abs (config : config) (meta : Meta.meta) (fixed_ids : ids_sets) : cm_fun = - fun cf ctx -> + fun ctx -> let rec explore_env (env : env) : unit = match env with | [] -> () (* Done *) @@ -70,20 +70,19 @@ let rec end_useless_fresh_borrows_and_abs (config : config) (meta : Meta.meta) try (* Explore the environment *) explore_env ctx.env; - (* No exception raised: call the continuation *) - cf ctx + (* No exception raised: simply continue *) + (ctx, fun e -> e) with | FoundAbsId abs_id -> - let cc = end_abstraction config meta abs_id in - comp cc rec_call cf ctx + let ctx, cc = end_abstraction config meta abs_id ctx in + comp cc (rec_call ctx) | FoundBorrowId bid -> - let cc = end_borrow config meta bid in - comp cc rec_call cf ctx + let ctx, cc = end_borrow config meta bid ctx in + comp cc (rec_call ctx) (* Explore the fresh anonymous values and replace all the values which are not borrows/loans with ⊥ *) -let cleanup_fresh_values (fixed_ids : ids_sets) : cm_fun = - fun cf ctx -> +let cleanup_fresh_values (fixed_ids : ids_sets) (ctx : eval_ctx) : eval_ctx = let rec explore_env (env : env) : env = match env with | [] -> [] (* Done *) @@ -112,8 +111,7 @@ let cleanup_fresh_values (fixed_ids : ids_sets) : cm_fun = EBinding (BDummy vid, v) :: env | x :: env -> x :: explore_env env in - let ctx = { ctx with env = explore_env ctx.env } in - cf ctx + { ctx with env = explore_env ctx.env } (* Repeat until we can't simplify the context anymore: - explore the fresh anonymous values and replace all the values which are not @@ -123,11 +121,10 @@ let cleanup_fresh_values (fixed_ids : ids_sets) : cm_fun = *) let cleanup_fresh_values_and_abs (config : config) (meta : Meta.meta) (fixed_ids : ids_sets) : cm_fun = - fun cf ctx -> - comp - (end_useless_fresh_borrows_and_abs config meta fixed_ids) - (cleanup_fresh_values fixed_ids) - cf ctx + fun ctx -> + let ctx, cc = end_useless_fresh_borrows_and_abs config meta fixed_ids ctx in + let ctx = cleanup_fresh_values fixed_ids ctx in + (ctx, cc) (** Reorder the loans and borrows in the fresh abstractions. @@ -189,7 +186,7 @@ let reorder_loans_borrows_in_fresh_abs (meta : Meta.meta) let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_fun = - fun cf ctx0 -> + fun ctx0 -> let ctx = ctx0 in (* Compute the set of borrows which appear in the abstractions, so that we can filter the borrows that we reborrow. @@ -427,34 +424,30 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : let _, new_ctx_ids_map = compute_ctx_ids ctx in (* Synthesize *) - match cf ctx with - | None -> None - | Some e -> - (* Add the let-bindings which introduce the fresh symbolic values *) - Some - (List.fold_left - (fun e (sid, v) -> - let v = mk_typed_value_from_symbolic_value v in - let sv = - SymbolicValueId.Map.find sid new_ctx_ids_map.sids_to_values - in - SymbolicAst.IntroSymbolic (ctx, None, sv, VaSingleValue v, e)) - e !sid_subst) + let cf e = + match e with + | None -> None + | Some e -> + (* Add the let-bindings which introduce the fresh symbolic values *) + Some + (List.fold_left + (fun e (sid, v) -> + let v = mk_typed_value_from_symbolic_value v in + let sv = + SymbolicValueId.Map.find sid new_ctx_ids_map.sids_to_values + in + SymbolicAst.IntroSymbolic (ctx, None, sv, VaSingleValue v, e)) + e !sid_subst) + in + (ctx, cf) let prepare_ashared_loans_no_synth (meta : Meta.meta) (loop_id : LoopId.id) (ctx : eval_ctx) : eval_ctx = - get_cf_ctx_no_synth meta (prepare_ashared_loans meta (Some loop_id)) ctx + fst (prepare_ashared_loans meta (Some loop_id) ctx) let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) - (loop_id : LoopId.id) (eval_loop_body : st_cm_fun) (ctx0 : eval_ctx) : + (loop_id : LoopId.id) (eval_loop_body : stl_cm_fun) (ctx0 : eval_ctx) : eval_ctx * ids_sets * abs RegionGroupId.Map.t = - (* The continuation for when we exit the loop - we register the - environments upon loop *reentry*, and synthesize nothing by - returning [None] - *) - let ctxs = ref [] in - let register_ctx ctx = ctxs := ctx :: !ctxs in - (* Introduce "reborrows" for the shared values in the abstractions, so that the shared values in the fixed abstractions never get modified (technically, they are immutable, but in practice we can introduce more shared loans, or @@ -474,25 +467,6 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx ^ "\n\n")); - let cf_exit_loop_body (res : statement_eval_res) : m_fun = - fun ctx -> - log#ldebug (lazy "compute_loop_entry_fixed_point: cf_exit_loop_body"); - match res with - | Return | Panic | Break _ -> None - | Unit -> - (* See the comment in {!eval_loop} *) - craise __FILE__ __LINE__ meta "Unreachable" - | Continue i -> - (* For now we don't support continues to outer loops *) - cassert __FILE__ __LINE__ (i = 0) meta - "Continues to outer loops not supported yet"; - register_ctx ctx; - None - | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> - (* We don't support nested loops for now *) - craise __FILE__ __LINE__ meta "Nested loops are not supported for now" - in - (* The fixed ids. They are the ids of the original ctx, after we ended the borrows/loans which end during the first loop iteration (we do one loop iteration, then set it to [Some]). @@ -502,18 +476,21 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (* Join the contexts at the loop entry - ctx1 is the current joined context (the context at the loop entry, after we called {!prepare_ashared_loans}, if this is the first iteration) *) - let join_ctxs (ctx1 : eval_ctx) : eval_ctx = + let join_ctxs (ctx1 : eval_ctx) (ctxs : eval_ctx list) : eval_ctx = log#ldebug (lazy "compute_loop_entry_fixed_point: join_ctxs"); (* If this is the first iteration, end the borrows/loans/abs which appear in ctx1 and not in the other contexts, then compute the set of fixed ids. This means those borrows/loans have to end - in the loop, and we rather end them *before* the loop. *) - let ctx1 = + in the loop, and we rather end them *before* the loop. + + We also end those borrows in the collected contexts. + *) + let ctx1, ctxs = match !fixed_ids with - | Some _ -> ctx1 + | Some _ -> (ctx1, ctxs) | None -> let old_ids, _ = compute_ctx_ids ctx1 in - let new_ids, _ = compute_ctxs_ids !ctxs in + let new_ids, _ = compute_ctxs_ids ctxs in let blids = BorrowId.Set.diff old_ids.blids new_ids.blids in let aids = AbstractionId.Set.diff old_ids.aids new_ids.aids in (* End those borrows and abstractions *) @@ -542,11 +519,11 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) others didn't. As we need to end those borrows anyway (the join will detect them and ask to end them) we do it preemptively. *) - ctxs := List.map (end_borrows_abs blids aids) !ctxs; + let ctxs = List.map (end_borrows_abs blids aids) ctxs in (* Note that the fixed ids are given by the original context, from *before* we introduce fresh abstractions/reborrows for the shared values *) fixed_ids := Some (fst (compute_ctx_ids ctx0)); - ctx1 + (ctx1, ctxs) in let fixed_ids = Option.get !fixed_ids in @@ -554,9 +531,8 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (* Join the context with the context at the loop entry *) let (_, _), ctx2 = loop_join_origin_with_continue_ctxs config meta loop_id fixed_ids ctx1 - !ctxs + ctxs in - ctxs := []; ctx2 in log#ldebug (lazy "compute_loop_entry_fixed_point: after join_ctxs"); @@ -597,10 +573,30 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) ^ " iterations") else (* Evaluate the loop body to register the different contexts upon reentry *) - let _ = eval_loop_body cf_exit_loop_body ctx in + let ctx_resl, _ = eval_loop_body ctx in + (* Keep only the contexts which reached a `continue`. *) + let keep_continue_ctx (ctx, res) = + log#ldebug + (lazy "compute_loop_entry_fixed_point: register_continue_ctx"); + match res with + | Return | Panic | Break _ -> None + | Unit -> + (* See the comment in {!eval_loop} *) + craise __FILE__ __LINE__ meta "Unreachable" + | Continue i -> + (* For now we don't support continues to outer loops *) + cassert __FILE__ __LINE__ (i = 0) meta + "Continues to outer loops not supported yet"; + Some ctx + | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> + (* We don't support nested loops for now *) + craise __FILE__ __LINE__ meta + "Nested loops are not supported for now" + in + let continue_ctxs = List.filter_map keep_continue_ctx ctx_resl in (* Compute the join between the original contexts and the contexts computed upon reentry *) - let ctx1 = join_ctxs ctx in + let ctx1 = join_ctxs ctx continue_ctxs in (* Debug *) log#ldebug @@ -670,13 +666,10 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) let aids = AbstractionId.Set.union aids aids' in fp_ended_aids := RegionGroupId.Map.add rg_id aids !fp_ended_aids in - let cf_loop : st_m_fun = - fun res ctx -> + let end_at_return (ctx, res) = log#ldebug (lazy "compute_loop_entry_fixed_point: cf_loop"); match res with - | Continue _ | Panic -> - (* We don't want to generate anything *) - None + | Continue _ | Panic -> () | Break _ -> (* We enforce that we can't get there: see {!PrePasses.remove_loop_breaks} *) craise __FILE__ __LINE__ meta "Unreachable" @@ -692,36 +685,30 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) * indeed the correct one, I think it is sound to under-approximate here * (and it shouldn't make any difference). *) - let _ = - List.iter - (fun rg_id -> - (* Lookup the input abstraction - we use the fact that the - abstractions should have been introduced in a specific - order (and we check that it is indeed the case) *) - let abs_id = - AbstractionId.of_int (RegionGroupId.to_int rg_id) - in - (* By default, the [SynthInput] abs can't end *) - let ctx = ctx_set_abs_can_end meta ctx abs_id true in - sanity_check __FILE__ __LINE__ - (let abs = ctx_lookup_abs ctx abs_id in - abs.kind = SynthInput rg_id) - meta; - (* End this abstraction *) - let ctx = - InterpreterBorrows.end_abstraction_no_synth config meta abs_id - ctx - in - (* Explore the context, and check which abstractions are not there anymore *) - let ids, _ = compute_ctx_ids ctx in - let ended_ids = AbstractionId.Set.diff !fp_aids ids.aids in - add_ended_aids rg_id ended_ids) - ctx.region_groups - in - (* We don't want to generate anything *) - None + List.iter + (fun rg_id -> + (* Lookup the input abstraction - we use the fact that the + abstractions should have been introduced in a specific + order (and we check that it is indeed the case) *) + let abs_id = AbstractionId.of_int (RegionGroupId.to_int rg_id) in + (* By default, the [SynthInput] abs can't end *) + let ctx = ctx_set_abs_can_end meta ctx abs_id true in + sanity_check __FILE__ __LINE__ + (let abs = ctx_lookup_abs ctx abs_id in + abs.kind = SynthInput rg_id) + meta; + (* End this abstraction *) + let ctx = + InterpreterBorrows.end_abstraction_no_synth config meta abs_id + ctx + in + (* Explore the context, and check which abstractions are not there anymore *) + let ids, _ = compute_ctx_ids ctx in + let ended_ids = AbstractionId.Set.diff !fp_aids ids.aids in + add_ended_aids rg_id ended_ids) + ctx.region_groups in - let _ = eval_loop_body cf_loop fp in + List.iter end_at_return (fst (eval_loop_body fp)); (* Check that the sets of abstractions we need to end per region group are pairwise * disjoint *) diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli index 4fc36598..d367c94c 100644 --- a/compiler/InterpreterLoopsFixedPoint.mli +++ b/compiler/InterpreterLoopsFixedPoint.mli @@ -80,7 +80,9 @@ val compute_loop_entry_fixed_point : config -> Meta.meta -> loop_id -> - Cps.st_cm_fun -> + (* This function is the function to evaluate the loop body (eval_statement applied + to the proper arguments) *) + Cps.stl_cm_fun -> eval_ctx -> eval_ctx * ids_sets * abs SymbolicAst.region_group_id_map diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 3db68f5d..b95148bd 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -1500,7 +1500,7 @@ let ctxs_are_equivalent (meta : Meta.meta) (fixed_ids : ids_sets) let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (src_ctx : eval_ctx) : cm_fun = - fun cf tgt_ctx -> + fun tgt_ctx -> (* Debug *) log#ldebug (lazy @@ -1510,8 +1510,8 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) ^ "\n- tgt_ctx: " ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx)); (* End the loans which lead to mismatches when joining *) - let rec cf_reorganize_join_tgt : cm_fun = - fun cf tgt_ctx -> + let rec reorganize_join_tgt : cm_fun = + fun tgt_ctx -> (* Collect fixed values in the source and target contexts: end the loans in the source context which don't appear in the target context *) let filt_src_env, _, _ = ctx_split_fixed_new meta fixed_ids src_ctx in @@ -1519,8 +1519,9 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) log#ldebug (lazy - ("cf_reorganize_join_tgt: match_ctx_with_target:\n" ^ "\n- fixed_ids: " - ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- filt_src_ctx: " + ("prepare_match_ctx_with_target: reorganize_join_tgt:\n" + ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids ^ "\n" + ^ "\n- filt_src_ctx: " ^ env_to_string meta src_ctx filt_src_env ^ "\n- filt_tgt_ctx: " ^ env_to_string meta tgt_ctx filt_tgt_env)); @@ -1561,9 +1562,9 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (* No exception was thrown: continue *) log#ldebug (lazy - ("cf_reorganize_join_tgt: done with borrows/loans:\n" - ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids ^ "\n" - ^ "\n- filt_src_ctx: " + ("prepare_match_ctx_with_target: reorganize_join_tgt: done with \ + borrows/loans:\n" ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids + ^ "\n" ^ "\n- filt_src_ctx: " ^ env_to_string meta src_ctx filt_src_env ^ "\n- filt_tgt_ctx: " ^ env_to_string meta tgt_ctx filt_tgt_env)); @@ -1619,33 +1620,36 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) log#ldebug (lazy - ("cf_reorganize_join_tgt: done with borrows/loans and moves:\n" - ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: " + ("prepare_match_ctx_with_target: reorganize_join_tgt: done with \ + borrows/loans and moves:\n" ^ "\n- fixed_ids: " + ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: " ^ eval_ctx_to_string ~meta:(Some meta) src_ctx ^ "\n- tgt_ctx: " ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx)); - cf tgt_ctx + (tgt_ctx, fun e -> e) with ValueMatchFailure e -> (* Exception: end the corresponding borrows, and continue *) - let cc = + let ctx, cc = match e with - | LoanInRight bid -> InterpreterBorrows.end_borrow config meta bid - | LoansInRight bids -> InterpreterBorrows.end_borrows config meta bids + | LoanInRight bid -> + InterpreterBorrows.end_borrow config meta bid tgt_ctx + | LoansInRight bids -> + InterpreterBorrows.end_borrows config meta bids tgt_ctx | AbsInRight _ | AbsInLeft _ | LoanInLeft _ | LoansInLeft _ -> craise __FILE__ __LINE__ meta "Unexpected" in - comp cc cf_reorganize_join_tgt cf tgt_ctx + comp cc (reorganize_join_tgt ctx) in (* Apply the reorganization *) - cf_reorganize_join_tgt cf tgt_ctx + reorganize_join_tgt tgt_ctx let match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id : LoopId.id) (is_loop_entry : bool) (fp_bl_maps : borrow_loan_corresp) (fp_input_svalues : SymbolicValueId.id list) (fixed_ids : ids_sets) (src_ctx : eval_ctx) : st_cm_fun = - fun cf tgt_ctx -> + fun tgt_ctx -> (* Debug *) log#ldebug (lazy @@ -1658,8 +1662,8 @@ let match_ctx_with_target (config : config) (meta : Meta.meta) context, which results from joins during which we ended the loans which were introduced during the loop iterations) *) - let cf_reorganize_join_tgt = - prepare_match_ctx_with_target config meta loop_id fixed_ids src_ctx + let tgt_ctx, cc = + prepare_match_ctx_with_target config meta loop_id fixed_ids src_ctx tgt_ctx in (* Introduce the "identity" abstractions for the loop re-entry. @@ -1679,290 +1683,285 @@ let match_ctx_with_target (config : config) (meta : Meta.meta) We should rely on a more primitive and safer function [add_identity_abs] to add the identity abstractions one by one. *) - let cf_introduce_loop_fp_abs : m_fun = - fun tgt_ctx -> - (* Match the source and target contexts *) - log#ldebug - (lazy - ("cf_introduce_loop_fp_abs:\n" ^ "\n- fixed_ids: " - ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: " - ^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: " - ^ eval_ctx_to_string tgt_ctx)); + (* Match the source and target contexts *) + log#ldebug + (lazy + ("cf_introduce_loop_fp_abs:\n" ^ "\n- fixed_ids: " + ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: " + ^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: " ^ eval_ctx_to_string tgt_ctx + )); - let filt_tgt_env, _, _ = ctx_split_fixed_new meta fixed_ids tgt_ctx in - let filt_src_env, new_absl, new_dummyl = - ctx_split_fixed_new meta fixed_ids src_ctx - in - sanity_check __FILE__ __LINE__ (new_dummyl = []) meta; - let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in - let filt_src_ctx = { src_ctx with env = filt_src_env } in - - let src_to_tgt_maps = - let check_equiv = false in - let fixed_ids = ids_sets_empty_borrows_loans fixed_ids in - let open InterpreterBorrowsCore in - let lookup_shared_loan lid ctx : typed_value = - match snd (lookup_loan meta ek_all lid ctx) with - | Concrete (VSharedLoan (_, v)) -> v - | Abstract (ASharedLoan (_, v, _)) -> v - | _ -> craise __FILE__ __LINE__ meta "Unreachable" - in - let lookup_in_src id = lookup_shared_loan id src_ctx in - let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in - (* Match *) - Option.get - (match_ctxs meta check_equiv fixed_ids lookup_in_src lookup_in_tgt - filt_src_ctx filt_tgt_ctx) - in - let tgt_to_src_borrow_map = - BorrowId.Map.of_list - (List.map - (fun (x, y) -> (y, x)) - (BorrowId.InjSubst.bindings src_to_tgt_maps.borrow_id_map)) + let filt_tgt_env, _, _ = ctx_split_fixed_new meta fixed_ids tgt_ctx in + let filt_src_env, new_absl, new_dummyl = + ctx_split_fixed_new meta fixed_ids src_ctx + in + sanity_check __FILE__ __LINE__ (new_dummyl = []) meta; + let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in + let filt_src_ctx = { src_ctx with env = filt_src_env } in + + let src_to_tgt_maps = + let check_equiv = false in + let fixed_ids = ids_sets_empty_borrows_loans fixed_ids in + let open InterpreterBorrowsCore in + let lookup_shared_loan lid ctx : typed_value = + match snd (lookup_loan meta ek_all lid ctx) with + | Concrete (VSharedLoan (_, v)) -> v + | Abstract (ASharedLoan (_, v, _)) -> v + | _ -> craise __FILE__ __LINE__ meta "Unreachable" in + let lookup_in_src id = lookup_shared_loan id src_ctx in + let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in + (* Match *) + Option.get + (match_ctxs meta check_equiv fixed_ids lookup_in_src lookup_in_tgt + filt_src_ctx filt_tgt_ctx) + in + let tgt_to_src_borrow_map = + BorrowId.Map.of_list + (List.map + (fun (x, y) -> (y, x)) + (BorrowId.InjSubst.bindings src_to_tgt_maps.borrow_id_map)) + in - (* Debug *) - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs:" ^ "\n\n- src_ctx: " - ^ eval_ctx_to_string ~meta:(Some meta) src_ctx - ^ "\n\n- tgt_ctx: " - ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx - ^ "\n\n- filt_tgt_ctx: " - ^ eval_ctx_to_string_no_filter ~meta:(Some meta) filt_tgt_ctx - ^ "\n\n- filt_src_ctx: " - ^ eval_ctx_to_string_no_filter ~meta:(Some meta) filt_src_ctx - ^ "\n\n- new_absl:\n" - ^ eval_ctx_to_string ~meta:(Some meta) - { src_ctx with env = List.map (fun abs -> EAbs abs) new_absl } - ^ "\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids ^ "\n\n- fp_bl_maps:\n" - ^ show_borrow_loan_corresp fp_bl_maps - ^ "\n\n- src_to_tgt_maps: " - ^ show_ids_maps src_to_tgt_maps)); - - (* Update the borrows and symbolic ids in the source context. - - Going back to the [list_nth_mut_example], the original environment upon - re-entering the loop is: - - {[ + (* Debug *) + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs:" ^ "\n\n- src_ctx: " + ^ eval_ctx_to_string ~meta:(Some meta) src_ctx + ^ "\n\n- tgt_ctx: " + ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx + ^ "\n\n- filt_tgt_ctx: " + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) filt_tgt_ctx + ^ "\n\n- filt_src_ctx: " + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) filt_src_ctx + ^ "\n\n- new_absl:\n" + ^ eval_ctx_to_string ~meta:(Some meta) + { src_ctx with env = List.map (fun abs -> EAbs abs) new_absl } + ^ "\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids ^ "\n\n- fp_bl_maps:\n" + ^ show_borrow_loan_corresp fp_bl_maps + ^ "\n\n- src_to_tgt_maps: " + ^ show_ids_maps src_to_tgt_maps)); + + (* Update the borrows and symbolic ids in the source context. + + Going back to the [list_nth_mut_example], the original environment upon + re-entering the loop is: + + {[ + abs@0 { ML l0 } + ls -> MB l5 (s@6 : loops::List<T>) + i -> s@7 : u32 + _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2)) + _@2 -> MB l2 (@Box (ML l4)) // tail + _@3 -> MB l1 (s@3 : T) // hd + abs@1 { MB l4, ML l5 } + ]} + + The fixed-point environment is: + {[ + env_fp = { abs@0 { ML l0 } - ls -> MB l5 (s@6 : loops::List<T>) - i -> s@7 : u32 - _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2)) - _@2 -> MB l2 (@Box (ML l4)) // tail - _@3 -> MB l1 (s@3 : T) // hd - abs@1 { MB l4, ML l5 } - ]} - - The fixed-point environment is: - {[ - env_fp = { - abs@0 { ML l0 } - ls -> MB l1 (s3 : loops::List<T>) - i -> s4 : u32 - abs@fp { - MB l0 // this borrow appears in [env0] - ML l1 - } + ls -> MB l1 (s3 : loops::List<T>) + i -> s4 : u32 + abs@fp { + MB l0 // this borrow appears in [env0] + ML l1 } - ]} + } + ]} + + Through matching, we detect that in [env_fp], [l1] is matched + to [l5]. We introduce a fresh borrow [l6] for [l1], and remember + in the map [src_fresh_borrows_map] that: [{ l1 -> l6}]. + + We get: + {[ + abs@0 { ML l0 } + ls -> MB l6 (s@6 : loops::List<T>) // l6 is fresh and doesn't have a corresponding loan + i -> s@7 : u32 + _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2)) + _@2 -> MB l2 (@Box (ML l4)) // tail + _@3 -> MB l1 (s@3 : T) // hd + abs@1 { MB l4, ML l5 } + ]} + + Later, we will introduce the identity abstraction: + {[ + abs@2 { MB l5, ML l6 } + ]} + *) + (* First, compute the set of borrows which appear in the fresh abstractions + of the fixed-point: we want to introduce fresh ids only for those. *) + let new_absl_ids, _ = compute_absl_ids new_absl in + let src_fresh_borrows_map = ref BorrowId.Map.empty in + let visit_tgt = + object + inherit [_] map_eval_ctx + + method! visit_borrow_id _ id = + (* Map the borrow, if it needs to be mapped *) + if + (* We map the borrows for which we computed a mapping *) + BorrowId.InjSubst.Set.mem id + (BorrowId.InjSubst.elements src_to_tgt_maps.borrow_id_map) + (* And which have corresponding loans in the fresh fixed-point abstractions *) + && BorrowId.Set.mem + (BorrowId.Map.find id tgt_to_src_borrow_map) + new_absl_ids.loan_ids + then ( + let src_id = BorrowId.Map.find id tgt_to_src_borrow_map in + let nid = fresh_borrow_id () in + src_fresh_borrows_map := + BorrowId.Map.add src_id nid !src_fresh_borrows_map; + nid) + else id + end + in - Through matching, we detect that in [env_fp], [l1] is matched - to [l5]. We introduce a fresh borrow [l6] for [l1], and remember - in the map [src_fresh_borrows_map] that: [{ l1 -> l6}]. + let tgt_ctx = visit_tgt#visit_eval_ctx () tgt_ctx in - We get: - {[ - abs@0 { ML l0 } - ls -> MB l6 (s@6 : loops::List<T>) // l6 is fresh and doesn't have a corresponding loan - i -> s@7 : u32 - _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2)) - _@2 -> MB l2 (@Box (ML l4)) // tail - _@3 -> MB l1 (s@3 : T) // hd - abs@1 { MB l4, ML l5 } - ]} - - Later, we will introduce the identity abstraction: - {[ - abs@2 { MB l5, ML l6 } - ]} - *) - (* First, compute the set of borrows which appear in the fresh abstractions - of the fixed-point: we want to introduce fresh ids only for those. *) - let new_absl_ids, _ = compute_absl_ids new_absl in - let src_fresh_borrows_map = ref BorrowId.Map.empty in - let visit_tgt = - object - inherit [_] map_eval_ctx - - method! visit_borrow_id _ id = - (* Map the borrow, if it needs to be mapped *) - if - (* We map the borrows for which we computed a mapping *) - BorrowId.InjSubst.Set.mem id - (BorrowId.InjSubst.elements src_to_tgt_maps.borrow_id_map) - (* And which have corresponding loans in the fresh fixed-point abstractions *) - && BorrowId.Set.mem - (BorrowId.Map.find id tgt_to_src_borrow_map) - new_absl_ids.loan_ids - then ( - let src_id = BorrowId.Map.find id tgt_to_src_borrow_map in - let nid = fresh_borrow_id () in - src_fresh_borrows_map := - BorrowId.Map.add src_id nid !src_fresh_borrows_map; - nid) - else id - end - in - let tgt_ctx = visit_tgt#visit_eval_ctx () tgt_ctx in + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: src_fresh_borrows_map:\n" + ^ BorrowId.Map.show BorrowId.to_string !src_fresh_borrows_map + ^ "\n")); - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ - src_fresh_borrows_map:\n" - ^ BorrowId.Map.show BorrowId.to_string !src_fresh_borrows_map - ^ "\n")); + (* Rem.: we don't update the symbolic values. It is not necessary + because there shouldn't be any symbolic value containing borrows. - (* Rem.: we don't update the symbolic values. It is not necessary - because there shouldn't be any symbolic value containing borrows. + Rem.: we will need to do something about the symbolic values in the + abstractions and in the *variable bindings* once we allow symbolic + values containing borrows to not be eagerly expanded. + *) + sanity_check __FILE__ __LINE__ Config.greedy_expand_symbolics_with_borrows + meta; + + (* Update the borrows and loans in the abstractions of the target context. + + Going back to the [list_nth_mut] example and by using [src_fresh_borrows_map], + we instantiate the fixed-point abstractions that we will insert into the + context. + The abstraction is [abs { MB l0, ML l1 }]. + Because of [src_fresh_borrows_map], we substitute [l1] with [l6]. + Because of the match between the contexts, we substitute [l0] with [l5]. + We get: + {[ + abs@2 { MB l5, ML l6 } + ]} + *) + let region_id_map = ref RegionId.Map.empty in + let get_rid rid = + match RegionId.Map.find_opt rid !region_id_map with + | Some rid -> rid + | None -> + let nid = fresh_region_id () in + region_id_map := RegionId.Map.add rid nid !region_id_map; + nid + in + let visit_src = + object + inherit [_] map_eval_ctx as super - Rem.: we will need to do something about the symbolic values in the - abstractions and in the *variable bindings* once we allow symbolic - values containing borrows to not be eagerly expanded. - *) - sanity_check __FILE__ __LINE__ Config.greedy_expand_symbolics_with_borrows - meta; - - (* Update the borrows and loans in the abstractions of the target context. - - Going back to the [list_nth_mut] example and by using [src_fresh_borrows_map], - we instantiate the fixed-point abstractions that we will insert into the - context. - The abstraction is [abs { MB l0, ML l1 }]. - Because of [src_fresh_borrows_map], we substitute [l1] with [l6]. - Because of the match between the contexts, we substitute [l0] with [l5]. - We get: - {[ - abs@2 { MB l5, ML l6 } - ]} - *) - let region_id_map = ref RegionId.Map.empty in - let get_rid rid = - match RegionId.Map.find_opt rid !region_id_map with - | Some rid -> rid - | None -> - let nid = fresh_region_id () in - region_id_map := RegionId.Map.add rid nid !region_id_map; - nid - in - let visit_src = - object - inherit [_] map_eval_ctx as super + method! visit_borrow_id _ bid = + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ + visit_borrow_id: " ^ BorrowId.to_string bid ^ "\n")); - method! visit_borrow_id _ bid = - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ - visit_borrow_id: " ^ BorrowId.to_string bid ^ "\n")); + (* Lookup the id of the loan corresponding to this borrow *) + let src_lid = + BorrowId.InjSubst.find bid fp_bl_maps.borrow_to_loan_id_map + in - (* Lookup the id of the loan corresponding to this borrow *) - let src_lid = - BorrowId.InjSubst.find bid fp_bl_maps.borrow_to_loan_id_map - in + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: looked up \ + src_lid: " ^ BorrowId.to_string src_lid ^ "\n")); - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs: looked up \ - src_lid: " ^ BorrowId.to_string src_lid ^ "\n")); + (* Lookup the tgt borrow id to which this borrow was mapped *) + let tgt_bid = + BorrowId.InjSubst.find src_lid src_to_tgt_maps.borrow_id_map + in - (* Lookup the tgt borrow id to which this borrow was mapped *) - let tgt_bid = - BorrowId.InjSubst.find src_lid src_to_tgt_maps.borrow_id_map - in + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: looked up \ + tgt_bid: " ^ BorrowId.to_string tgt_bid ^ "\n")); - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs: looked up \ - tgt_bid: " ^ BorrowId.to_string tgt_bid ^ "\n")); + tgt_bid - tgt_bid + method! visit_loan_id _ id = + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: visit_loan_id: " + ^ BorrowId.to_string id ^ "\n")); + (* Map the borrow - rem.: we mapped the borrows *in the values*, + meaning we know how to map the *corresponding loans in the + abstractions* *) + match BorrowId.Map.find_opt id !src_fresh_borrows_map with + | None -> + (* No mapping: this means that the borrow was mapped when + we matched values (it doesn't come from a fresh abstraction) + and because of this, it should actually be mapped to itself *) + sanity_check __FILE__ __LINE__ + (BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id) + meta; + id + | Some id -> id + + method! visit_symbolic_value_id _ _ = fresh_symbolic_value_id () + method! visit_abstraction_id _ _ = fresh_abstraction_id () + method! visit_region_id _ id = get_rid id + + (** We also need to change the abstraction kind *) + method! visit_abs env abs = + match abs.kind with + | Loop (loop_id', rg_id, kind) -> + sanity_check __FILE__ __LINE__ (loop_id' = loop_id) meta; + sanity_check __FILE__ __LINE__ (kind = LoopSynthInput) meta; + let can_end = false in + let kind : abs_kind = Loop (loop_id, rg_id, LoopCall) in + let abs = { abs with kind; can_end } in + super#visit_abs env abs + | _ -> super#visit_abs env abs + end + in + let new_absl = List.map (visit_src#visit_abs ()) new_absl in + let new_absl = List.map (fun abs -> EAbs abs) new_absl in - method! visit_loan_id _ id = - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ - visit_loan_id: " ^ BorrowId.to_string id ^ "\n")); - (* Map the borrow - rem.: we mapped the borrows *in the values*, - meaning we know how to map the *corresponding loans in the - abstractions* *) - match BorrowId.Map.find_opt id !src_fresh_borrows_map with - | None -> - (* No mapping: this means that the borrow was mapped when - we matched values (it doesn't come from a fresh abstraction) - and because of this, it should actually be mapped to itself *) - sanity_check __FILE__ __LINE__ - (BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id) - meta; - id - | Some id -> id - - method! visit_symbolic_value_id _ _ = fresh_symbolic_value_id () - method! visit_abstraction_id _ _ = fresh_abstraction_id () - method! visit_region_id _ id = get_rid id - - (** We also need to change the abstraction kind *) - method! visit_abs env abs = - match abs.kind with - | Loop (loop_id', rg_id, kind) -> - sanity_check __FILE__ __LINE__ (loop_id' = loop_id) meta; - sanity_check __FILE__ __LINE__ (kind = LoopSynthInput) meta; - let can_end = false in - let kind : abs_kind = Loop (loop_id, rg_id, LoopCall) in - let abs = { abs with kind; can_end } in - super#visit_abs env abs - | _ -> super#visit_abs env abs - end - in - let new_absl = List.map (visit_src#visit_abs ()) new_absl in - let new_absl = List.map (fun abs -> EAbs abs) new_absl in + (* Add the abstractions from the target context to the source context *) + let nenv = List.append new_absl tgt_ctx.env in + let tgt_ctx = { tgt_ctx with env = nenv } in - (* Add the abstractions from the target context to the source context *) - let nenv = List.append new_absl tgt_ctx.env in - let tgt_ctx = { tgt_ctx with env = nenv } in + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: done:\n- result ctx:\n" + ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx)); - log#ldebug - (lazy - ("match_ctx_with_target: cf_introduce_loop_fp_abs: done:\n\ - - result ctx:\n" - ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx)); - - (* Sanity check *) - if !Config.sanity_checks then - Invariants.check_borrowed_values_invariant meta tgt_ctx; - (* End all the borrows which appear in the *new* abstractions *) - let new_borrows = - BorrowId.Set.of_list - (List.map snd (BorrowId.Map.bindings !src_fresh_borrows_map)) - in - let cc = InterpreterBorrows.end_borrows config meta new_borrows in - - (* Compute the loop input values *) - let input_values = - SymbolicValueId.Map.of_list - (List.map - (fun sid -> - (sid, SymbolicValueId.Map.find sid src_to_tgt_maps.sid_to_value_map)) - fp_input_svalues) - in + (* Sanity check *) + if !Config.sanity_checks then + Invariants.check_borrowed_values_invariant meta tgt_ctx; + (* End all the borrows which appear in the *new* abstractions *) + let new_borrows = + BorrowId.Set.of_list + (List.map snd (BorrowId.Map.bindings !src_fresh_borrows_map)) + in + let tgt_ctx, cc = + comp cc (InterpreterBorrows.end_borrows config meta new_borrows tgt_ctx) + in + + (* Compute the loop input values *) + let input_values = + SymbolicValueId.Map.of_list + (List.map + (fun sid -> + (sid, SymbolicValueId.Map.find sid src_to_tgt_maps.sid_to_value_map)) + fp_input_svalues) + in - (* Continue *) - cc - (cf - (if is_loop_entry then EndEnterLoop (loop_id, input_values) - else EndContinue (loop_id, input_values))) - tgt_ctx + let res = + if is_loop_entry then EndEnterLoop (loop_id, input_values) + else EndContinue (loop_id, input_values) in - (* Compose and continue *) - cf_reorganize_join_tgt cf_introduce_loop_fp_abs tgt_ctx + ((tgt_ctx, res), cc) diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index ab3daa72..a76ebfeb 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -460,17 +460,17 @@ let expand_bottom_value_from_projection (meta : Meta.meta) let rec update_ctx_along_read_place (config : config) (meta : Meta.meta) (access : access_kind) (p : place) : cm_fun = - fun cf ctx -> + fun ctx -> (* Attempt to read the place: if it fails, update the environment and retry *) match try_read_place meta access p ctx with - | Ok _ -> cf ctx + | Ok _ -> (ctx, fun e -> e) | Error err -> - let cc = + let ctx, cc = match err with - | FailSharedLoan bids -> end_borrows config meta bids - | FailMutLoan bid -> end_borrow config meta bid + | FailSharedLoan bids -> end_borrows config meta bids ctx + | FailMutLoan bid -> end_borrow config meta bid ctx | FailReservedMutBorrow bid -> - promote_reserved_mut_borrow config meta bid + promote_reserved_mut_borrow config meta bid ctx | FailSymbolic (i, sp) -> (* Expand the symbolic value *) let proj, _ = @@ -480,53 +480,54 @@ let rec update_ctx_along_read_place (config : config) (meta : Meta.meta) let prefix = { p with projection = proj } in expand_symbolic_value_no_branching config meta sp (Some (Synth.mk_mplace meta prefix ctx)) + ctx | FailBottom (_, _, _) -> (* We can't expand {!Bottom} values while reading them *) craise __FILE__ __LINE__ meta "Found bottom while reading a place" | FailBorrow _ -> craise __FILE__ __LINE__ meta "Could not read a borrow" in - comp cc (update_ctx_along_read_place config meta access p) cf ctx + comp cc (update_ctx_along_read_place config meta access p ctx) let rec update_ctx_along_write_place (config : config) (meta : Meta.meta) (access : access_kind) (p : place) : cm_fun = - fun cf ctx -> + fun 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 try_read_place meta access p ctx with - | Ok _ -> cf ctx + | Ok _ -> (ctx, fun e -> e) | Error err -> (* Update the context *) - let cc = + let ctx, cc = match err with - | FailSharedLoan bids -> end_borrows config meta bids - | FailMutLoan bid -> end_borrow config meta bid + | FailSharedLoan bids -> end_borrows config meta bids ctx + | FailMutLoan bid -> end_borrow config meta bid ctx | FailReservedMutBorrow bid -> - promote_reserved_mut_borrow config meta bid + promote_reserved_mut_borrow config meta bid ctx | FailSymbolic (_pe, sp) -> (* Expand the symbolic value *) expand_symbolic_value_no_branching config meta sp (Some (Synth.mk_mplace meta p ctx)) + ctx | FailBottom (remaining_pes, pe, ty) -> (* Expand the {!Bottom} value *) - fun cf ctx -> - let ctx = - expand_bottom_value_from_projection meta access p remaining_pes - pe ty ctx - in - cf ctx + let ctx = + expand_bottom_value_from_projection meta access p remaining_pes pe + ty ctx + in + (ctx, fun e -> e) | FailBorrow _ -> craise __FILE__ __LINE__ meta "Could not write to a borrow" in (* Retry *) - comp cc (update_ctx_along_write_place config meta access p) cf ctx + comp cc (update_ctx_along_write_place config meta access p ctx) (** Small utility used to break control-flow *) -exception UpdateCtx of cm_fun +exception UpdateCtx of (eval_ctx * (eval_result -> eval_result)) let rec end_loans_at_place (config : config) (meta : Meta.meta) (access : access_kind) (p : place) : cm_fun = - fun cf ctx -> + fun ctx -> (* Iterator to explore a value and update the context whenever we find * loans. * We use exceptions to make it handy: whenever we update the @@ -542,8 +543,8 @@ let rec end_loans_at_place (config : config) (meta : Meta.meta) (* Nothing special to do *) super#visit_borrow_content env bc | VReservedMutBorrow bid -> (* We need to activate reserved borrows *) - let cc = promote_reserved_mut_borrow config meta bid in - raise (UpdateCtx cc) + let res = promote_reserved_mut_borrow config meta bid ctx in + raise (UpdateCtx res) method! visit_loan_content env lc = match lc with @@ -553,12 +554,12 @@ let rec end_loans_at_place (config : config) (meta : Meta.meta) match access with | Read -> super#visit_VSharedLoan env bids v | Write | Move -> - let cc = end_borrows config meta bids in - raise (UpdateCtx cc)) + let res = end_borrows config meta bids ctx in + raise (UpdateCtx res)) | VMutLoan bid -> (* We always need to end mutable borrows *) - let cc = end_borrow config meta bid in - raise (UpdateCtx cc) + let res = end_borrow config meta bid ctx in + raise (UpdateCtx res) end in @@ -573,64 +574,62 @@ let rec end_loans_at_place (config : config) (meta : Meta.meta) try obj#visit_typed_value () v; (* No context update required: apply the continuation *) - cf ctx - with UpdateCtx cc -> + (ctx, fun e -> e) + with UpdateCtx (ctx, cc) -> (* We need to update the context: compose the caugth continuation with * a recursive call to reinspect the value *) - comp cc (end_loans_at_place config meta access p) cf ctx + comp cc (end_loans_at_place config meta access p ctx) let drop_outer_loans_at_lplace (config : config) (meta : Meta.meta) (p : place) : cm_fun = - fun cf ctx -> + fun ctx -> (* Move the current value in the place outside of this place and into - * a dummy variable *) + * a temporary dummy variable *) let access = Write in let v = read_place meta access p ctx in let ctx = write_place meta access p (mk_bottom meta v.ty) ctx in let dummy_id = fresh_dummy_var_id () in let ctx = ctx_push_dummy_var ctx dummy_id v in - (* Auxiliary function *) + (* Auxiliary function: while there are loans to end in the + temporary value, end them *) let rec drop : cm_fun = - fun cf ctx -> + fun ctx -> (* Read the value *) let v = ctx_lookup_dummy_var meta ctx dummy_id in - (* Check if there are loans or borrows to end *) + (* Check if there are loans (and only loans) to end *) let with_borrows = false in match get_first_outer_loan_or_borrow_in_value with_borrows v with | None -> - (* We are done: simply call the continuation *) - cf ctx + (* We are done *) + (ctx, fun e -> e) | Some c -> - (* There are: end them then retry *) - let cc = + (* End the loans and retry *) + let ctx, cc = match c with - | LoanContent (VSharedLoan (bids, _)) -> end_borrows config meta bids - | LoanContent (VMutLoan bid) -> end_borrow config meta bid - | BorrowContent _ -> craise __FILE__ __LINE__ meta "Unreachable" + | LoanContent (VSharedLoan (bids, _)) -> + end_borrows config meta bids ctx + | LoanContent (VMutLoan bid) -> end_borrow config meta bid ctx + | BorrowContent _ -> + (* Can't get there: we are only looking up the loans *) + craise __FILE__ __LINE__ meta "Unreachable" in (* Retry *) - comp cc drop cf ctx + comp cc (drop ctx) in (* Apply the drop function *) - let cc = drop in + let ctx, cc = drop ctx in (* Pop the temporary value and reinsert it *) - let cc = - comp cc (fun cf ctx -> - (* Pop *) - let ctx, v = ctx_remove_dummy_var meta ctx dummy_id in - (* Reinsert *) - let ctx = write_place meta access p v ctx in - (* Sanity check *) - sanity_check __FILE__ __LINE__ (not (outer_loans_in_value v)) meta; - (* Continue *) - cf ctx) - in - (* Continue *) - cc cf ctx + (* Pop *) + let ctx, v = ctx_remove_dummy_var meta ctx dummy_id in + (* Sanity check *) + sanity_check __FILE__ __LINE__ (not (outer_loans_in_value v)) meta; + (* Reinsert *) + let ctx = write_place meta access p v ctx in + (* Return *) + (ctx, cc) let prepare_lplace (config : config) (meta : Meta.meta) (p : place) - (cf : typed_value -> m_fun) : m_fun = - fun ctx -> + (ctx : eval_ctx) : typed_value * eval_ctx * (eval_result -> eval_result) = log#ldebug (lazy ("prepare_lplace:" ^ "\n- p: " ^ place_to_string ctx p @@ -638,17 +637,12 @@ let prepare_lplace (config : config) (meta : Meta.meta) (p : place) ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Access the place *) let access = Write in - let cc = update_ctx_along_write_place config meta access p in - (* End the borrows and loans, starting with the borrows *) - let cc = comp cc (drop_outer_loans_at_lplace config meta p) in + let ctx, cc = update_ctx_along_write_place config meta access p ctx in + (* End the loans at the place we are about to overwrite *) + let ctx, cc = comp cc (drop_outer_loans_at_lplace config meta p ctx) in (* Read the value and check it *) - let read_check cf : m_fun = - fun ctx -> - let v = read_place meta access p ctx in - (* Sanity checks *) - sanity_check __FILE__ __LINE__ (not (outer_loans_in_value v)) meta; - (* Continue *) - cf v ctx - in - (* Compose and apply the continuations *) - comp cc read_check cf ctx + let v = read_place meta access p ctx in + (* Sanity checks *) + sanity_check __FILE__ __LINE__ (not (outer_loans_in_value v)) meta; + (* Return *) + (v, ctx, cc) diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli index 260f07bf..c266e7ae 100644 --- a/compiler/InterpreterPaths.mli +++ b/compiler/InterpreterPaths.mli @@ -100,4 +100,8 @@ val end_loans_at_place : config -> Meta.meta -> access_kind -> place -> cm_fun case). Note that this value is very likely to contain ⊥ subvalues. *) val prepare_lplace : - config -> Meta.meta -> place -> (typed_value -> m_fun) -> m_fun + config -> + Meta.meta -> + place -> + eval_ctx -> + typed_value * eval_ctx * (eval_result -> eval_result) diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 9ad6487b..66677eff 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -20,7 +20,7 @@ let log = L.statements_log (** Drop a value at a given place - TODO: factorize this with [assign_to_place] *) let drop_value (config : config) (meta : Meta.meta) (p : place) : cm_fun = - fun cf ctx -> + fun ctx -> log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Initial context:\n" @@ -29,11 +29,11 @@ let drop_value (config : config) (meta : Meta.meta) (p : place) : cm_fun = let access = Write in (* First make sure we can access the place, by ending loans or expanding * symbolic values along the path, for instance *) - let cc = update_ctx_along_read_place config meta access p in + let ctx, cc = update_ctx_along_read_place config meta access p ctx in (* Prepare the place (by ending the outer loans *at* the place). *) - let cc = comp cc (prepare_lplace config meta p) in + let v, ctx, cc = comp2 cc (prepare_lplace config meta p ctx) in (* Replace the value with {!Bottom} *) - let replace cf (v : typed_value) ctx = + let ctx = (* Move the value at destination (that we will overwrite) to a dummy variable * to preserve the borrows it may contain *) let mv = InterpreterPaths.read_place meta access p ctx in @@ -46,47 +46,41 @@ let drop_value (config : config) (meta : Meta.meta) (p : place) : cm_fun = (lazy ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - cf ctx + ctx in (* Compose and apply *) - comp cc replace cf ctx + (ctx, cc) (** Push a dummy variable to the environment *) -let push_dummy_var (vid : DummyVarId.id) (v : typed_value) : cm_fun = - fun cf ctx -> - let ctx = ctx_push_dummy_var ctx vid v in - cf ctx +let push_dummy_var (vid : DummyVarId.id) (v : typed_value) (ctx : eval_ctx) : + eval_ctx = + ctx_push_dummy_var ctx vid v (** Remove a dummy variable from the environment *) -let remove_dummy_var (meta : Meta.meta) (vid : DummyVarId.id) - (cf : typed_value -> m_fun) : m_fun = - fun ctx -> +let remove_dummy_var (meta : Meta.meta) (vid : DummyVarId.id) (ctx : eval_ctx) : + typed_value * eval_ctx = let ctx, v = ctx_remove_dummy_var meta ctx vid in - cf v ctx + (v, ctx) (** Push an uninitialized variable to the environment *) -let push_uninitialized_var (meta : Meta.meta) (var : var) : cm_fun = - fun cf ctx -> - let ctx = ctx_push_uninitialized_var meta ctx var in - cf ctx +let push_uninitialized_var (meta : Meta.meta) (var : var) (ctx : eval_ctx) : + eval_ctx = + ctx_push_uninitialized_var meta ctx var (** Push a list of uninitialized variables to the environment *) -let push_uninitialized_vars (meta : Meta.meta) (vars : var list) : cm_fun = - fun cf ctx -> - let ctx = ctx_push_uninitialized_vars meta ctx vars in - cf ctx +let push_uninitialized_vars (meta : Meta.meta) (vars : var list) + (ctx : eval_ctx) : eval_ctx = + ctx_push_uninitialized_vars meta ctx vars (** Push a variable to the environment *) -let push_var (meta : Meta.meta) (var : var) (v : typed_value) : cm_fun = - fun cf ctx -> - let ctx = ctx_push_var meta ctx var v in - cf ctx +let push_var (meta : Meta.meta) (var : var) (v : typed_value) (ctx : eval_ctx) : + eval_ctx = + ctx_push_var meta ctx var v (** Push a list of variables to the environment *) -let push_vars (meta : Meta.meta) (vars : (var * typed_value) list) : cm_fun = - fun cf ctx -> - let ctx = ctx_push_vars meta ctx vars in - cf ctx +let push_vars (meta : Meta.meta) (vars : (var * typed_value) list) + (ctx : eval_ctx) : eval_ctx = + ctx_push_vars meta ctx vars (** Assign a value to a given place. @@ -97,7 +91,7 @@ let push_vars (meta : Meta.meta) (vars : (var * typed_value) list) : cm_fun = *) let assign_to_place (config : config) (meta : Meta.meta) (rv : typed_value) (p : place) : cm_fun = - fun cf ctx -> + fun ctx -> log#ldebug (lazy ("assign_to_place:" ^ "\n- rv: " @@ -106,58 +100,51 @@ let assign_to_place (config : config) (meta : Meta.meta) (rv : typed_value) ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Push the rvalue to a dummy variable, for bookkeeping *) let rvalue_vid = fresh_dummy_var_id () in - let cc = push_dummy_var rvalue_vid rv in + let ctx = push_dummy_var rvalue_vid rv ctx in (* Prepare the destination *) - let cc = comp cc (prepare_lplace config meta p) in + let _, ctx, cc = prepare_lplace config meta p ctx in (* Retrieve the rvalue from the dummy variable *) - let cc = comp cc (fun cf _lv -> remove_dummy_var meta rvalue_vid cf) in + let rv, ctx = remove_dummy_var meta rvalue_vid ctx in + (* Move the value at destination (that we will overwrite) to a dummy variable + to preserve the borrows *) + let mv = InterpreterPaths.read_place meta Write p ctx in + let dest_vid = fresh_dummy_var_id () in + let ctx = ctx_push_dummy_var ctx dest_vid mv in + (* Write to the destination *) + (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *) + exec_assert __FILE__ __LINE__ + (not (bottom_in_value ctx.ended_regions rv)) + meta "The value to move contains bottom"; (* Update the destination *) - let move_dest cf (rv : typed_value) : m_fun = - fun ctx -> - (* Move the value at destination (that we will overwrite) to a dummy variable - * to preserve the borrows *) - let mv = InterpreterPaths.read_place meta Write p ctx in - let dest_vid = fresh_dummy_var_id () in - let ctx = ctx_push_dummy_var ctx dest_vid mv in - (* Write to the destination *) - (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *) - exec_assert __FILE__ __LINE__ - (not (bottom_in_value ctx.ended_regions rv)) - meta "The value to move contains bottom"; - (* Update the destination *) - let ctx = write_place meta Write p rv ctx in - (* Debug *) - log#ldebug - (lazy - ("assign_to_place:" ^ "\n- rv: " - ^ typed_value_to_string ~meta:(Some meta) ctx rv - ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Final context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - (* Continue *) - cf ctx - in - (* Compose and apply *) - comp cc move_dest cf ctx + let ctx = write_place meta Write p rv ctx in + (* Debug *) + log#ldebug + (lazy + ("assign_to_place:" ^ "\n- rv: " + ^ typed_value_to_string ~meta:(Some meta) ctx rv + ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Final context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + (* Return *) + (ctx, cc) (** Evaluate an assertion, when the scrutinee is not symbolic *) let eval_assertion_concrete (config : config) (meta : Meta.meta) (assertion : assertion) : st_cm_fun = - fun cf ctx -> + fun ctx -> (* There won't be any symbolic expansions: fully evaluate the operand *) - let eval_op = eval_operand config meta assertion.cond in - let eval_assert cf (v : typed_value) : m_fun = - fun ctx -> + let v, ctx, eval_op = eval_operand config meta assertion.cond ctx in + let st = match v.value with | VLiteral (VBool b) -> (* Branch *) - if b = assertion.expected then cf Unit ctx else cf Panic ctx + if b = assertion.expected then Unit else Panic | _ -> craise __FILE__ __LINE__ meta ("Expected a boolean, got: " ^ typed_value_to_string ~meta:(Some meta) ctx v) in (* Compose and apply *) - comp eval_op eval_assert cf ctx + ((ctx, st), eval_op) (** Evaluates an assertion. @@ -167,13 +154,12 @@ let eval_assertion_concrete (config : config) (meta : Meta.meta) *) let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion) : st_cm_fun = - fun cf ctx -> + fun ctx -> (* Evaluate the operand *) - let eval_op = eval_operand config meta assertion.cond in + let v, ctx, cf_eval_op = eval_operand config meta assertion.cond ctx in (* Evaluate the assertion *) - let eval_assert cf (v : typed_value) : m_fun = - fun ctx -> - sanity_check __FILE__ __LINE__ (v.ty = TLiteral TBool) meta; + sanity_check __FILE__ __LINE__ (v.ty = TLiteral TBool) meta; + let st, cf_eval_assert = (* We make a choice here: we could completely decouple the concrete and * symbolic executions here but choose not to. In the case where we * know the concrete value of the boolean we test, we use this value @@ -182,7 +168,7 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion) match v.value with | VLiteral (VBool _) -> (* Delegate to the concrete evaluation function *) - eval_assertion_concrete config meta assertion cf ctx + eval_assertion_concrete config meta assertion ctx | VSymbolic sv -> sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta; sanity_check __FILE__ __LINE__ (sv.sv_ty = TLiteral TBool) meta; @@ -191,20 +177,18 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion) * We will of course synthesize an assertion in the generated code * (see below). *) let ctx = - apply_symbolic_expansion_non_borrow config meta sv - (SeLiteral (VBool true)) ctx + apply_symbolic_expansion_non_borrow config meta sv ctx + (SeLiteral (VBool true)) in - (* Continue *) - let expr = cf Unit ctx in (* Add the synthesized assertion *) - S.synthesize_assertion ctx v expr + ((ctx, Unit), S.synthesize_assertion ctx v) | _ -> craise __FILE__ __LINE__ meta ("Expected a boolean, got: " ^ typed_value_to_string ~meta:(Some meta) ctx v) in (* Compose and apply *) - comp eval_op eval_assert cf ctx + (st, cc_comp cf_eval_op cf_eval_assert) (** Updates the discriminant of a value at a given place. @@ -219,7 +203,7 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion) *) let set_discriminant (config : config) (meta : Meta.meta) (p : place) (variant_id : VariantId.id) : st_cm_fun = - fun cf ctx -> + fun ctx -> log#ldebug (lazy ("set_discriminant:" ^ "\n- p: " ^ place_to_string ctx p @@ -229,69 +213,67 @@ let set_discriminant (config : config) (meta : Meta.meta) (p : place) ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Access the value *) let access = Write in - let cc = update_ctx_along_read_place config meta access p in - let cc = comp cc (prepare_lplace config meta p) in + let ctx, cc = update_ctx_along_read_place config meta access p ctx in + let v, ctx, cc = comp2 cc (prepare_lplace config meta p ctx) in (* Update the value *) - let update_value cf (v : typed_value) : m_fun = - fun ctx -> - match (v.ty, v.value) with - | TAdt ((TAdtId _ as type_id), generics), VAdt av -> ( - (* There are two situations: - - either the discriminant is already the proper one (in which case we - don't do anything) - - or it is not the proper one, in which case we replace the value with - a variant with all its fields set to {!Bottom} - *) - match av.variant_id with - | None -> - craise __FILE__ __LINE__ meta - "Found a struct value while expected an enum" - | Some variant_id' -> - if variant_id' = variant_id then (* Nothing to do *) - cf Unit ctx - else - (* Replace the value *) - let bottom_v = - match type_id with - | TAdtId def_id -> - compute_expanded_bottom_adt_value meta ctx def_id - (Some variant_id) generics - | _ -> craise __FILE__ __LINE__ meta "Unreachable" - in - assign_to_place config meta bottom_v p (cf Unit) ctx) - | TAdt ((TAdtId _ as type_id), generics), VBottom -> - let bottom_v = - match type_id with - | TAdtId def_id -> - compute_expanded_bottom_adt_value meta ctx def_id - (Some variant_id) generics - | _ -> craise __FILE__ __LINE__ meta "Unreachable" - in - assign_to_place config meta bottom_v p (cf Unit) ctx - | _, VSymbolic _ -> - sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta; - (* This is a bit annoying: in theory we should expand the symbolic value - * then set the discriminant, because in the case the discriminant is - * exactly the one we set, the fields are left untouched, and in the - * other cases they are set to Bottom. - * For now, we forbid setting the discriminant of a symbolic value: - * setting a discriminant should only be used to initialize a value, - * or reset an already initialized value, really. *) - craise __FILE__ __LINE__ meta "Unexpected value" - | _, (VAdt _ | VBottom) -> - craise __FILE__ __LINE__ meta "Inconsistent state" - | _, (VLiteral _ | VBorrow _ | VLoan _) -> - craise __FILE__ __LINE__ meta "Unexpected value" - in - (* Compose and apply *) - comp cc update_value cf ctx + match (v.ty, v.value) with + | TAdt ((TAdtId _ as type_id), generics), VAdt av -> ( + (* There are two situations: + - either the discriminant is already the proper one (in which case we + don't do anything) + - or it is not the proper one, in which case we replace the value with + a variant with all its fields set to {!Bottom} + *) + match av.variant_id with + | None -> + craise __FILE__ __LINE__ meta + "Found a struct value while expecting an enum" + | Some variant_id' -> + if variant_id' = variant_id then (* Nothing to do *) + ((ctx, Unit), cc) + else + (* Replace the value *) + let bottom_v = + match type_id with + | TAdtId def_id -> + compute_expanded_bottom_adt_value meta ctx def_id + (Some variant_id) generics + | _ -> craise __FILE__ __LINE__ meta "Unreachable" + in + let ctx, cc = + comp cc (assign_to_place config meta bottom_v p ctx) + in + ((ctx, Unit), cc)) + | TAdt ((TAdtId _ as type_id), generics), VBottom -> + let bottom_v = + match type_id with + | TAdtId def_id -> + compute_expanded_bottom_adt_value meta ctx def_id (Some variant_id) + generics + | _ -> craise __FILE__ __LINE__ meta "Unreachable" + in + let ctx, cc = comp cc (assign_to_place config meta bottom_v p ctx) in + ((ctx, Unit), cc) + | _, VSymbolic _ -> + sanity_check __FILE__ __LINE__ (config.mode = SymbolicMode) meta; + (* This is a bit annoying: in theory we should expand the symbolic value + * then set the discriminant, because in the case the discriminant is + * exactly the one we set, the fields are left untouched, and in the + * other cases they are set to Bottom. + * For now, we forbid setting the discriminant of a symbolic value: + * setting a discriminant should only be used to initialize a value, + * or reset an already initialized value, really. *) + craise __FILE__ __LINE__ meta "Unexpected value" + | _, (VAdt _ | VBottom) -> craise __FILE__ __LINE__ meta "Inconsistent state" + | _, (VLiteral _ | VBorrow _ | VLoan _) -> + craise __FILE__ __LINE__ meta "Unexpected value" (** Push a frame delimiter in the context's environment *) let ctx_push_frame (ctx : eval_ctx) : eval_ctx = { ctx with env = EFrame :: ctx.env } (** Push a frame delimiter in the context's environment *) -let push_frame : cm_fun = fun cf ctx -> cf (ctx_push_frame ctx) +let push_frame (ctx : eval_ctx) : eval_ctx = ctx_push_frame ctx (** Small helper: compute the type of the return value for a specific instantiation of an assumed function. @@ -323,17 +305,19 @@ let get_assumed_function_return_type (meta : Meta.meta) (ctx : eval_ctx) AssociatedTypes.ctx_normalize_erase_ty meta ctx ty let move_return_value (config : config) (meta : Meta.meta) - (pop_return_value : bool) (cf : typed_value option -> m_fun) : m_fun = - fun ctx -> + (pop_return_value : bool) (ctx : eval_ctx) : + typed_value option * eval_ctx * (eval_result -> eval_result) = if pop_return_value then let ret_vid = VarId.zero in - let cc = eval_operand config meta (Move (mk_place_from_var_id ret_vid)) in - cc (fun v ctx -> cf (Some v) ctx) ctx - else cf None ctx + let v, ctx, cc = + eval_operand config meta (Move (mk_place_from_var_id ret_vid)) ctx + in + (Some v, ctx, cc) + else (None, ctx, fun e -> e) let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool) - (cf : typed_value option -> m_fun) : m_fun = - fun ctx -> + (ctx : eval_ctx) : + typed_value option * eval_ctx * (eval_result -> eval_result) = (* Debug *) log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); @@ -358,40 +342,31 @@ let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool) ^ "]")); (* Move the return value out of the return variable *) - let cc = move_return_value config meta pop_return_value in - (* Sanity check *) - let cc = - comp_check_value cc (fun ret_value ctx -> - match ret_value with - | None -> () - | Some ret_value -> - sanity_check __FILE__ __LINE__ - (not (bottom_in_value ctx.ended_regions ret_value)) - meta) + let v, ctx, cc = move_return_value config meta pop_return_value ctx in + let _ = + match v with + | None -> () + | Some ret_value -> + sanity_check __FILE__ __LINE__ + (not (bottom_in_value ctx.ended_regions ret_value)) + meta in (* Drop the outer *loans* we find in the local variables *) - let cf_drop_loans_in_locals cf (ret_value : typed_value option) : m_fun = - (* Drop the loans *) - let locals = List.rev locals in - let cf_drop = - List.fold_left - (fun cf lid -> - drop_outer_loans_at_lplace config meta (mk_place_from_var_id lid) cf) - (cf ret_value) locals - in - (* Apply *) - cf_drop + let ctx, cc = + comp cc + ((* Drop the loans *) + let locals = List.rev locals in + fold_left_apply_continuation + (fun lid ctx -> + drop_outer_loans_at_lplace config meta (mk_place_from_var_id lid) ctx) + locals ctx) in - let cc = comp cc cf_drop_loans_in_locals in (* Debug *) - let cc = - comp_check_value cc (fun _ ctx -> - log#ldebug - (lazy - ("pop_frame: after dropping outer loans in local variables:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx))) - in + log#ldebug + (lazy + ("pop_frame: after dropping outer loans in local variables:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); (* Pop the frame - we remove the [Frame] delimiter, and reintroduce all * the local variables (which may still contain borrow permissions - but @@ -405,28 +380,22 @@ let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool) EBinding (BDummy vid, v) :: pop env | EFrame :: env -> (* Stop here *) env in - let cf_pop cf (ret_value : typed_value option) : m_fun = - fun ctx -> - let env = pop ctx.env in - let ctx = { ctx with env } in - cf ret_value ctx - in - (* Compose and apply *) - comp cc cf_pop cf ctx + let env = pop ctx.env in + let ctx = { ctx with env } in + (* Return *) + (v, ctx, cc) (** Pop the current frame and assign the returned value to its destination. *) let pop_frame_assign (config : config) (meta : Meta.meta) (dest : place) : cm_fun = - let cf_pop = pop_frame config meta true in - let cf_assign cf ret_value : m_fun = - assign_to_place config meta (Option.get ret_value) dest cf - in - comp cf_pop cf_assign + fun ctx -> + let v, ctx, cc = pop_frame config meta true ctx in + comp cc (assign_to_place config meta (Option.get v) dest ctx) (** Auxiliary function - see {!eval_assumed_function_call} *) let eval_box_new_concrete (config : config) (meta : Meta.meta) (generics : generic_args) : cm_fun = - fun cf ctx -> + fun ctx -> (* Check and retrieve the arguments *) match (generics.regions, generics.types, generics.const_generics, ctx.env) @@ -443,30 +412,22 @@ let eval_box_new_concrete (config : config) (meta : Meta.meta) meta "The input given to Box::new doesn't have the proper type"; (* Move the input value *) - let cf_move = - eval_operand config meta (Move (mk_place_from_var_id input_var.index)) + let v, ctx, cc = + eval_operand config meta + (Move (mk_place_from_var_id input_var.index)) + ctx in (* Create the new box *) - let cf_create cf (moved_input_value : typed_value) : m_fun = - (* Create the box value *) - let generics = TypesUtils.mk_generic_args_from_types [ boxed_ty ] in - let box_ty = TAdt (TAssumed TBox, generics) in - let box_v = - VAdt { variant_id = None; field_values = [ moved_input_value ] } - in - let box_v = mk_typed_value meta box_ty box_v in - - (* Move this value to the return variable *) - let dest = mk_place_from_var_id VarId.zero in - let cf_assign = assign_to_place config meta box_v dest in - - (* Continue *) - cf_assign cf - in - - (* Compose and apply *) - comp cf_move cf_create cf ctx + (* Create the box value *) + let generics = TypesUtils.mk_generic_args_from_types [ boxed_ty ] in + let box_ty = TAdt (TAssumed TBox, generics) in + let box_v = VAdt { variant_id = None; field_values = [ v ] } in + let box_v = mk_typed_value meta box_ty box_v in + + (* Move this value to the return variable *) + let dest = mk_place_from_var_id VarId.zero in + comp cc (assign_to_place config meta box_v dest ctx) | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" (** Auxiliary function - see {!eval_assumed_function_call}. @@ -490,7 +451,7 @@ let eval_box_new_concrete (config : config) (meta : Meta.meta) *) let eval_box_free (config : config) (meta : Meta.meta) (generics : generic_args) (args : operand list) (dest : place) : cm_fun = - fun cf ctx -> + fun ctx -> match (generics.regions, generics.types, generics.const_generics, args) with | [], [ boxed_ty ], [], [ Move input_box_place ] -> (* Required type checking *) @@ -502,18 +463,16 @@ let eval_box_free (config : config) (meta : Meta.meta) (generics : generic_args) meta; (* Drop the value *) - let cc = drop_value config meta input_box_place in + let ctx, cc = drop_value config meta input_box_place ctx in (* Update the destination by setting it to [()] *) - let cc = comp cc (assign_to_place config meta mk_unit_value dest) in - - (* Continue *) - cc cf ctx + comp cc (assign_to_place config meta mk_unit_value dest ctx) | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" (** Evaluate a non-local function call in concrete mode *) let eval_assumed_function_call_concrete (config : config) (meta : Meta.meta) (fid : assumed_fun_id) (call : call) : cm_fun = + fun ctx -> let args = call.args in let dest = call.dest in match call.func with @@ -533,12 +492,12 @@ let eval_assumed_function_call_concrete (config : config) (meta : Meta.meta) match fid with | BoxFree -> (* Degenerate case: box_free *) - eval_box_free config meta generics args dest + eval_box_free config meta generics args dest ctx | _ -> (* "Normal" case: not box_free *) (* Evaluate the operands *) (* let ctx, args_vl = eval_operands config ctx args in *) - let cf_eval_ops = eval_operands config meta args in + let args_vl, ctx, cc = eval_operands config meta args ctx in (* Evaluate the call * @@ -547,53 +506,42 @@ let eval_assumed_function_call_concrete (config : config) (meta : Meta.meta) * below, without having to introduce an intermediary function call, * but it made it less clear where the computed values came from, * so we reversed the modifications. *) - let cf_eval_call cf (args_vl : typed_value list) : m_fun = - fun ctx -> - (* Push the stack frame: we initialize the frame with the return variable, - and one variable per input argument *) - let cc = push_frame in - - (* Create and push the return variable *) - let ret_vid = VarId.zero in - let ret_ty = - get_assumed_function_return_type meta ctx fid generics - in - let ret_var = mk_var ret_vid (Some "@return") ret_ty in - let cc = comp cc (push_uninitialized_var meta ret_var) in - - (* Create and push the input variables *) - let input_vars = - VarId.mapi_from1 - (fun id (v : typed_value) -> (mk_var id None v.ty, v)) - args_vl - in - let cc = comp cc (push_vars meta input_vars) in - - (* "Execute" the function body. As the functions are assumed, here we call - * custom functions to perform the proper manipulations: we don't have - * access to a body. *) - let cf_eval_body : cm_fun = - match fid with - | BoxNew -> eval_box_new_concrete config meta generics - | BoxFree -> - (* Should have been treated above *) - craise __FILE__ __LINE__ meta "Unreachable" - | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared - | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut - -> - craise __FILE__ __LINE__ meta "Unimplemented" - in - - let cc = comp cc cf_eval_body in - - (* Pop the frame *) - let cc = comp cc (pop_frame_assign config meta dest) in - - (* Continue *) - cc cf ctx + (* Push the stack frame: we initialize the frame with the return variable, + and one variable per input argument *) + let ctx = push_frame ctx in + + (* Create and push the return variable *) + let ret_vid = VarId.zero in + let ret_ty = get_assumed_function_return_type meta ctx fid generics in + let ret_var = mk_var ret_vid (Some "@return") ret_ty in + let ctx = push_uninitialized_var meta ret_var ctx in + + (* Create and push the input variables *) + let input_vars = + VarId.mapi_from1 + (fun id (v : typed_value) -> (mk_var id None v.ty, v)) + args_vl in - (* Compose and apply *) - comp cf_eval_ops cf_eval_call) + let ctx = push_vars meta input_vars ctx in + + (* "Execute" the function body. As the functions are assumed, here we call + * custom functions to perform the proper manipulations: we don't have + * access to a body. *) + let ctx, cf_eval_body = + match fid with + | BoxNew -> eval_box_new_concrete config meta generics ctx + | BoxFree -> + (* Should have been treated above *) + craise __FILE__ __LINE__ meta "Unreachable" + | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared + | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut + -> + craise __FILE__ __LINE__ meta "Unimplemented" + in + let cc = cc_comp cc cf_eval_body in + + (* Pop the frame *) + comp cc (pop_frame_assign config meta dest ctx)) (** Helper @@ -947,8 +895,8 @@ let eval_transparent_function_call_symbolic_inst (meta : Meta.meta) inst_sg ))) (** Evaluate a statement *) -let rec eval_statement (config : config) (st : statement) : st_cm_fun = - fun cf ctx -> +let rec eval_statement (config : config) (st : statement) : stl_cm_fun = + fun ctx -> (* Debugging *) log#ldebug (lazy @@ -959,16 +907,15 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = ^ "\n\n")); (* Take a snapshot of the current context for the purpose of generating pretty names *) - let cc = S.cf_save_snapshot in + let cc = S.save_snapshot ctx in (* Expand the symbolic values if necessary - we need to do that before - * checking the invariants *) - let cc = comp cc (greedy_expand_symbolic_values config st.meta) in + checking the invariants *) + let ctx, cc = comp cc (greedy_expand_symbolic_values config st.meta ctx) in (* Sanity check *) - let cc = comp cc (Invariants.cf_check_invariants st.meta) in + Invariants.check_invariants st.meta ctx; (* Evaluate *) - let cf_eval_st cf : m_fun = - fun ctx -> + let stl, cf_eval_st = log#ldebug (lazy ("\neval_statement: cf_eval_st: statement:\n" @@ -980,96 +927,118 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = match rvalue with | Global (gid, generics) -> (* Evaluate the global *) - eval_global config p gid generics cf ctx + eval_global config st.meta p gid generics ctx | _ -> (* Evaluate the rvalue *) - let cf_eval_rvalue = eval_rvalue_not_global config st.meta rvalue in + let res, ctx, cc = + eval_rvalue_not_global config st.meta rvalue ctx + in (* Assign *) - let cf_assign cf (res : (typed_value, eval_error) result) ctx = - log#ldebug - (lazy - ("about to assign to place: " ^ place_to_string ctx p - ^ "\n- Context:\n" - ^ eval_ctx_to_string ~meta:(Some st.meta) ctx)); + log#ldebug + (lazy + ("about to assign to place: " ^ place_to_string ctx p + ^ "\n- Context:\n" + ^ eval_ctx_to_string ~meta:(Some st.meta) ctx)); + let (ctx, res), cf_assign = match res with - | Error EPanic -> cf Panic ctx - | Ok rv -> ( - let expr = - assign_to_place config st.meta rv p (cf Unit) ctx - in - (* Update the synthesized AST - here we store meta-information. + | Error EPanic -> ((ctx, Panic), fun e -> e) + | Ok rv -> + (* Update the synthesized AST - here we store additional meta-information. * We do it only in specific cases (it is not always useful, and * also it can lead to issues - for instance, if we borrow a * reserved borrow, we later can't translate it to pure values...) *) - match rvalue with - | Global _ -> craise __FILE__ __LINE__ st.meta "Unreachable" - | Use _ - | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow)) - | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> - let rp = rvalue_get_place rvalue in - let rp = - match rp with - | Some rp -> Some (S.mk_mplace st.meta rp ctx) - | None -> None - in - S.synthesize_assignment ctx - (S.mk_mplace st.meta p ctx) - rv rp expr) + let cc = + match rvalue with + | Global _ -> craise __FILE__ __LINE__ st.meta "Unreachable" + | Use _ + | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow)) + | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> + let rp = rvalue_get_place rvalue in + let rp = + match rp with + | Some rp -> Some (S.mk_mplace st.meta rp ctx) + | None -> None + in + S.synthesize_assignment ctx + (S.mk_mplace st.meta p ctx) + rv rp + in + let ctx, cc = + comp cc (assign_to_place config st.meta rv p ctx) + in + ((ctx, Unit), cc) in - + let cc = cc_comp cc cf_assign in (* Compose and apply *) - comp cf_eval_rvalue cf_assign cf ctx) - | FakeRead p -> eval_fake_read config st.meta p (cf Unit) ctx + ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.meta cc)) + | FakeRead p -> + let ctx, cc = eval_fake_read config st.meta p ctx in + ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.meta cc) | SetDiscriminant (p, variant_id) -> - set_discriminant config st.meta p variant_id cf ctx - | Drop p -> drop_value config st.meta p (cf Unit) ctx - | Assert assertion -> eval_assertion config st.meta assertion cf ctx - | Call call -> eval_function_call config st.meta call cf ctx - | Panic -> cf Panic ctx - | Return -> cf Return ctx - | Break i -> cf (Break i) ctx - | Continue i -> cf (Continue i) ctx - | Nop -> cf Unit ctx + let (ctx, res), cc = set_discriminant config st.meta p variant_id ctx in + ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.meta cc) + | Drop p -> + let ctx, cc = drop_value config st.meta p ctx in + ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.meta cc) + | Assert assertion -> + let (ctx, res), cc = eval_assertion config st.meta assertion ctx in + ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.meta cc) + | Call call -> eval_function_call config st.meta call ctx + | Panic -> ([ (ctx, Panic) ], cc_singleton __FILE__ __LINE__ st.meta cc) + | Return -> ([ (ctx, Return) ], cc_singleton __FILE__ __LINE__ st.meta cc) + | Break i -> ([ (ctx, Break i) ], cc_singleton __FILE__ __LINE__ st.meta cc) + | Continue i -> + ([ (ctx, Continue i) ], cc_singleton __FILE__ __LINE__ st.meta cc) + | Nop -> ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ st.meta cc) | Sequence (st1, st2) -> (* Evaluate the first statement *) - let cf_st1 = eval_statement config st1 in - (* Evaluate the sequence *) - let cf_st2 cf res = - match res with - (* Evaluation successful: evaluate the second statement *) - | Unit -> eval_statement config st2 cf - (* Control-flow break: transmit. We enumerate the cases on purpose *) - | Panic | Break _ | Continue _ | Return | LoopReturn _ - | EndEnterLoop _ | EndContinue _ -> - cf res + let ctx_resl, cf_st1 = eval_statement config st1 ctx in + (* Evaluate the sequence (evaluate the second statement if the first + statement successfully evaluated, otherwise transfmit the control-flow + break) *) + let ctx_res_cfl = + List.map + (fun (ctx, res) -> + match res with + (* Evaluation successful: evaluate the second statement *) + | Unit -> eval_statement config st2 ctx + (* Control-flow break: transmit. We enumerate the cases on purpose *) + | Panic | Break _ | Continue _ | Return | LoopReturn _ + | EndEnterLoop _ | EndContinue _ -> + ([ (ctx, res) ], cc_singleton __FILE__ __LINE__ st.meta cc)) + ctx_resl + in + (* Put everything together: + - we return the flattened list of contexts and results + - we need to build the continuation which will build the whole + expression from the continuations for the individual branches + *) + let ctx_resl, cf_st2 = + comp_seqs __FILE__ __LINE__ st.meta ctx_res_cfl in - (* Compose and apply *) - comp cf_st1 cf_st2 cf ctx + (ctx_resl, cc_comp cf_st1 cf_st2) | Loop loop_body -> - InterpreterLoops.eval_loop config st.meta - (eval_statement config loop_body) - cf ctx - | Switch switch -> eval_switch config st.meta switch cf ctx + let eval_loop_body = eval_statement config loop_body in + InterpreterLoops.eval_loop config st.meta eval_loop_body ctx + | Switch switch -> eval_switch config st.meta switch ctx in (* Compose and apply *) - comp cc cf_eval_st cf ctx + (stl, cc_comp cc cf_eval_st) -and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) - (generics : generic_args) : st_cm_fun = - fun cf ctx -> +and eval_global (config : config) (meta : Meta.meta) (dest : place) + (gid : GlobalDeclId.id) (generics : generic_args) : stl_cm_fun = + fun ctx -> let global = ctx_lookup_global_decl ctx gid in match config.mode with | ConcreteMode -> (* Treat the evaluation of the global as a call to the global body *) let func = { func = FunId (FRegular global.body); generics } in let call = { func = FnOpRegular func; args = []; dest } in - (eval_transparent_function_call_concrete config global.item_meta.meta - global.body call) - cf ctx - | SymbolicMode -> + eval_transparent_function_call_concrete config meta global.body call ctx + | SymbolicMode -> ( (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *) - cassert __FILE__ __LINE__ (ty_no_regions global.ty) global.item_meta.meta + cassert __FILE__ __LINE__ (ty_no_regions global.ty) meta "Const globals should not contain regions"; (* Instantiate the type *) (* There shouldn't be any reference to Self *) @@ -1082,19 +1051,24 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self global.ty in - let sval = mk_fresh_symbolic_value global.item_meta.meta ty in - let cc = - assign_to_place config global.item_meta.meta + let sval = mk_fresh_symbolic_value meta ty in + let ctx, cc = + assign_to_place config meta (mk_typed_value_from_symbolic_value sval) - dest + dest ctx in - let e = cc (cf Unit) ctx in - S.synthesize_global_eval gid generics sval e + ( [ (ctx, Unit) ], + fun el -> + match el with + | Some [ e ] -> + (cc_comp (S.synthesize_global_eval gid generics sval) cc) (Some e) + | Some _ -> internal_error __FILE__ __LINE__ meta + | _ -> None )) (** Evaluate a switch *) and eval_switch (config : config) (meta : Meta.meta) (switch : switch) : - st_cm_fun = - fun cf ctx -> + stl_cm_fun = + fun ctx -> (* We evaluate the operand in two steps: * first we prepare it, then we check if its value is concrete or * symbolic. If it is concrete, we can then evaluate the operand @@ -1104,130 +1078,147 @@ and eval_switch (config : config) (meta : Meta.meta) (switch : switch) : * (and would thus floating in thin air...)! * *) (* Match on the targets *) - let cf_match : st_cm_fun = - fun cf ctx -> - match switch with - | If (op, st1, st2) -> - (* Evaluate the operand *) - let cf_eval_op = eval_operand config meta op in - (* Switch on the value *) - let cf_if (cf : st_m_fun) (op_v : typed_value) : m_fun = - fun ctx -> - match op_v.value with - | VLiteral (VBool b) -> - (* Evaluate the if and the branch body *) - let cf_branch cf : m_fun = - (* Branch *) - if b then eval_statement config st1 cf - else eval_statement config st2 cf - in - (* Compose the continuations *) - cf_branch cf ctx - | VSymbolic sv -> - (* Expand the symbolic boolean, and continue by evaluating - * the branches *) - let cf_true : st_cm_fun = eval_statement config st1 in - let cf_false : st_cm_fun = eval_statement config st2 in + match switch with + | If (op, st1, st2) -> + (* Evaluate the operand *) + let op_v, ctx, cf_eval_op = eval_operand config meta op ctx in + (* Switch on the value *) + let ctx_resl, cf_if = + match op_v.value with + | VLiteral (VBool b) -> + (* Branch *) + if b then eval_statement config st1 ctx + else eval_statement config st2 ctx + | VSymbolic sv -> + (* Expand the symbolic boolean, and continue by evaluating + the branches *) + let (ctx_true, ctx_false), cf_bool = expand_symbolic_bool config meta sv (S.mk_opt_place_from_op meta op ctx) - cf_true cf_false cf ctx - | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" - in - (* Compose *) - comp cf_eval_op cf_if cf ctx - | SwitchInt (op, int_ty, stgts, otherwise) -> - (* Evaluate the operand *) - let cf_eval_op = eval_operand config meta op in - (* Switch on the value *) - let cf_switch (cf : st_m_fun) (op_v : typed_value) : m_fun = - fun ctx -> - match op_v.value with - | VLiteral (VScalar sv) -> - (* Evaluate the branch *) - let cf_eval_branch cf = - (* Sanity check *) - sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) meta; - (* Find the branch *) - match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with - | None -> eval_statement config otherwise cf - | Some (_, tgt) -> eval_statement config tgt cf - in - (* Compose *) - cf_eval_branch cf ctx - | VSymbolic sv -> - (* Expand the symbolic value and continue by evaluating the - * proper branches *) - let stgts = - List.map - (fun (cv, tgt_st) -> (cv, eval_statement config tgt_st)) - stgts - in - (* Several branches may be grouped together: every branch is described - * by a pair (list of values, branch expression). - * In order to do a symbolic evaluation, we make this "flat" by - * de-grouping the branches. *) - let stgts = - List.concat - (List.map - (fun (vl, st) -> List.map (fun v -> (v, st)) vl) - stgts) - in - (* Translate the otherwise branch *) - let otherwise = eval_statement config otherwise in - (* Expand and continue *) + ctx + in + let resl_true = eval_statement config st1 ctx_true in + let resl_false = eval_statement config st2 ctx_false in + let ctx_resl, cf_branches = + comp_seqs __FILE__ __LINE__ meta [ resl_true; resl_false ] + in + let cc el = + match cf_branches el with + | None -> None + | Some [ e_true; e_false ] -> cf_bool (Some (e_true, e_false)) + | _ -> internal_error __FILE__ __LINE__ meta + in + (ctx_resl, cc) + | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" + in + (* Compose *) + (ctx_resl, cc_comp cf_eval_op cf_if) + | SwitchInt (op, int_ty, stgts, otherwise) -> + (* Evaluate the operand *) + let op_v, ctx, cf_eval_op = eval_operand config meta op ctx in + (* Switch on the value *) + let ctx_resl, cf_switch = + match op_v.value with + | VLiteral (VScalar sv) -> ( + (* Sanity check *) + sanity_check __FILE__ __LINE__ (sv.int_ty = int_ty) meta; + (* Find the branch *) + match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with + | None -> eval_statement config otherwise ctx + | Some (_, tgt) -> eval_statement config tgt ctx) + | VSymbolic sv -> + (* Several branches may be grouped together: every branch is described + by a pair (list of values, branch expression). + In order to do a symbolic evaluation, we make this "flat" by + de-grouping the branches. *) + let values, branches = + List.split + (List.concat + (List.map + (fun (vl, st) -> List.map (fun v -> (v, st)) vl) + stgts)) + in + (* Expand the symbolic value *) + let (ctx_branches, ctx_otherwise), cf_int = expand_symbolic_int config meta sv (S.mk_opt_place_from_op meta op ctx) - int_ty stgts otherwise cf ctx - | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" - in - (* Compose *) - comp cf_eval_op cf_switch cf ctx - | Match (p, stgts, otherwise) -> - (* Access the place *) - let access = Read in - let expand_prim_copy = false in - let cf_read_p cf : m_fun = - access_rplace_reorganize_and_read config meta expand_prim_copy access - p cf - in - (* Match on the value *) - let cf_match (cf : st_m_fun) (p_v : typed_value) : m_fun = - fun ctx -> - (* The value may be shared: we need to ignore the shared loans - to read the value itself *) - let p_v = value_strip_shared_loans p_v in - (* Match *) - match p_v.value with - | VAdt adt -> ( - (* Evaluate the discriminant *) - let dv = Option.get adt.variant_id in - (* Find the branch, evaluate and continue *) - match List.find_opt (fun (svl, _) -> List.mem dv svl) stgts with - | None -> ( - match otherwise with - | None -> craise __FILE__ __LINE__ meta "No otherwise branch" - | Some otherwise -> eval_statement config otherwise cf ctx) - | Some (_, tgt) -> eval_statement config tgt cf ctx) - | VSymbolic sv -> - (* Expand the symbolic value - may lead to branching *) - let cf_expand = - expand_symbolic_adt config meta sv - (Some (S.mk_mplace meta p ctx)) - in - (* Re-evaluate the switch - the value is not symbolic anymore, - which means we will go to the other branch *) - cf_expand (eval_switch config meta switch) cf ctx - | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" - in - (* Compose *) - comp cf_read_p cf_match cf ctx - in - (* Compose the continuations *) - cf_match cf ctx + int_ty values ctx + in + (* Evaluate the branches: first the "regular" branches *) + let resl_branches = + List.map + (fun (ctx, branch) -> eval_statement config branch ctx) + (List.combine ctx_branches branches) + in + (* Then evaluate the "otherwise" branch *) + let resl_otherwise = + eval_statement config otherwise ctx_otherwise + in + (* Compose the continuations *) + let resl, cf = + comp_seqs __FILE__ __LINE__ meta + (resl_branches @ [ resl_otherwise ]) + in + let cc el = + match el with + | None -> None + | Some el -> + let el, e_otherwise = Collections.List.pop_last el in + cf_int (Some (el, e_otherwise)) + in + (resl, cc_comp cc cf) + | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" + in + (* Compose *) + (ctx_resl, cc_comp cf_eval_op cf_switch) + | Match (p, stgts, otherwise) -> + (* Access the place *) + let access = Read in + let expand_prim_copy = false in + let p_v, ctx, cf_read_p = + access_rplace_reorganize_and_read config meta expand_prim_copy access p + ctx + in + (* Match on the value *) + let ctx_resl, cf_match = + (* The value may be shared: we need to ignore the shared loans + to read the value itself *) + let p_v = value_strip_shared_loans p_v in + (* Match *) + match p_v.value with + | VAdt adt -> ( + (* Evaluate the discriminant *) + let dv = Option.get adt.variant_id in + (* Find the branch, evaluate and continue *) + match List.find_opt (fun (svl, _) -> List.mem dv svl) stgts with + | None -> ( + match otherwise with + | None -> craise __FILE__ __LINE__ meta "No otherwise branch" + | Some otherwise -> eval_statement config otherwise ctx) + | Some (_, tgt) -> eval_statement config tgt ctx) + | VSymbolic sv -> + (* Expand the symbolic value - may lead to branching *) + let ctxl, cf_expand = + expand_symbolic_adt config meta sv + (Some (S.mk_mplace meta p ctx)) + ctx + in + (* Re-evaluate the switch - the value is not symbolic anymore, + which means we will go to the other branch *) + let resl = + List.map (fun ctx -> (eval_switch config meta switch) ctx) ctxl + in + (* Compose the continuations *) + let ctx_resl, cf = comp_seqs __FILE__ __LINE__ meta resl in + (ctx_resl, cc_comp cf_expand cf) + | _ -> craise __FILE__ __LINE__ meta "Inconsistent state" + in + (* Compose *) + (ctx_resl, cc_comp cf_read_p cf_match) (** Evaluate a function call (auxiliary helper for [eval_statement]) *) and eval_function_call (config : config) (meta : Meta.meta) (call : call) : - st_cm_fun = + stl_cm_fun = (* There are several cases: - this is a local function, in which case we execute its body - this is an assumed function, in which case there is a special treatment @@ -1238,24 +1229,32 @@ and eval_function_call (config : config) (meta : Meta.meta) (call : call) : | SymbolicMode -> eval_function_call_symbolic config meta call and eval_function_call_concrete (config : config) (meta : Meta.meta) - (call : call) : st_cm_fun = - fun cf ctx -> + (call : call) : stl_cm_fun = + fun ctx -> match call.func with | FnOpMove _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet" | FnOpRegular func -> ( match func.func with | FunId (FRegular fid) -> - eval_transparent_function_call_concrete config meta fid call cf ctx - | FunId (FAssumed fid) -> + eval_transparent_function_call_concrete config meta fid call ctx + | FunId (FAssumed fid) -> ( (* Continue - note that we do as if the function call has been successful, * by giving {!Unit} to the continuation, because we place us in the case * where we haven't panicked. Of course, the translation needs to take the * panic case into account... *) - eval_assumed_function_call_concrete config meta fid call (cf Unit) ctx + let ctx, cc = + eval_assumed_function_call_concrete config meta fid call ctx + in + ( [ (ctx, Unit) ], + fun el -> + match el with + | Some [ e ] -> cc (Some e) + | Some _ -> internal_error __FILE__ __LINE__ meta + | _ -> None )) | TraitMethod _ -> craise __FILE__ __LINE__ meta "Unimplemented") and eval_function_call_symbolic (config : config) (meta : Meta.meta) - (call : call) : st_cm_fun = + (call : call) : stl_cm_fun = match call.func with | FnOpMove _ -> craise __FILE__ __LINE__ meta "Closures are not supported yet" | FnOpRegular func -> ( @@ -1267,7 +1266,8 @@ and eval_function_call_symbolic (config : config) (meta : Meta.meta) (** Evaluate a local (i.e., non-assumed) function call in concrete mode *) and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta) - (fid : FunDeclId.id) (call : call) : st_cm_fun = + (fid : FunDeclId.id) (call : call) : stl_cm_fun = + fun ctx -> let args = call.args in let dest = call.dest in match call.func with @@ -1277,91 +1277,96 @@ and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta) (* Sanity check: we don't fully handle the const generic vars environment in concrete mode yet *) sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; - fun cf ctx -> - (* Retrieve the (correctly instantiated) body *) - let def = ctx_lookup_fun_decl ctx fid in - (* We can evaluate the function call only if it is not opaque *) - let body = - match def.body with - | None -> - craise __FILE__ __LINE__ meta - ("Can't evaluate a call to an opaque function: " - ^ name_to_string ctx def.name) - | Some body -> body - in - (* TODO: we need to normalize the types if we want to correctly support traits *) - cassert __FILE__ __LINE__ (generics.trait_refs = []) body.meta - "Traits are not supported yet in concrete mode"; - (* There shouldn't be any reference to Self *) - let tr_self = UnknownTrait __FUNCTION__ in - let subst = - Subst.make_subst_from_generics def.signature.generics generics tr_self - in - let locals, body_st = Subst.fun_body_substitute_in_body subst body in - - (* Evaluate the input operands *) - sanity_check __FILE__ __LINE__ - (List.length args = body.arg_count) - body.meta; - let cc = eval_operands config body.meta args in - - (* Push a frame delimiter - we use {!comp_transmit} to transmit the result - * of the operands evaluation from above to the functions afterwards, while - * ignoring it in this function *) - let cc = comp_transmit cc push_frame in - - (* Compute the initial values for the local variables *) - (* 1. Push the return value *) - let ret_var, locals = - match locals with - | ret_ty :: locals -> (ret_ty, locals) - | _ -> craise __FILE__ __LINE__ meta "Unreachable" - in - let input_locals, locals = - Collections.List.split_at locals body.arg_count - in + (* Retrieve the (correctly instantiated) body *) + let def = ctx_lookup_fun_decl ctx fid in + (* We can evaluate the function call only if it is not opaque *) + let body = + match def.body with + | None -> + craise __FILE__ __LINE__ meta + ("Can't evaluate a call to an opaque function: " + ^ name_to_string ctx def.name) + | Some body -> body + in + (* TODO: we need to normalize the types if we want to correctly support traits *) + cassert __FILE__ __LINE__ (generics.trait_refs = []) body.meta + "Traits are not supported yet in concrete mode"; + (* There shouldn't be any reference to Self *) + let tr_self = UnknownTrait __FUNCTION__ in + let subst = + Subst.make_subst_from_generics def.signature.generics generics tr_self + in + let locals, body_st = Subst.fun_body_substitute_in_body subst body in + + (* Evaluate the input operands *) + sanity_check __FILE__ __LINE__ + (List.length args = body.arg_count) + body.meta; + let vl, ctx, cc = eval_operands config body.meta args ctx in + + (* Push a frame delimiter - we use {!comp_transmit} to transmit the result + * of the operands evaluation from above to the functions afterwards, while + * ignoring it in this function *) + let ctx = push_frame ctx in + + (* Compute the initial values for the local variables *) + (* 1. Push the return value *) + let ret_var, locals = + match locals with + | ret_ty :: locals -> (ret_ty, locals) + | _ -> craise __FILE__ __LINE__ meta "Unreachable" + in + let input_locals, locals = + Collections.List.split_at locals body.arg_count + in - let cc = - comp_transmit cc - (push_var meta ret_var (mk_bottom meta ret_var.var_ty)) - in + let ctx = push_var meta ret_var (mk_bottom meta ret_var.var_ty) ctx in - (* 2. Push the input values *) - let cf_push_inputs cf args = - let inputs = List.combine input_locals args in - (* Note that this function checks that the variables and their values - * have the same type (this is important) *) - push_vars meta inputs cf - in - let cc = comp cc cf_push_inputs in - - (* 3. Push the remaining local variables (initialized as {!Bottom}) *) - let cc = comp cc (push_uninitialized_vars meta locals) in - - (* Execute the function body *) - let cc = comp cc (eval_function_body config body_st) in - - (* Pop the stack frame and move the return value to its destination *) - let cf_finish cf res = - match res with - | Panic -> cf Panic - | Return -> - (* Pop the stack frame, retrieve the return value, move it to - * its destination and continue *) - pop_frame_assign config meta dest (cf Unit) - | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _ - | EndContinue _ -> - craise __FILE__ __LINE__ meta "Unreachable" - in - let cc = comp cc cf_finish in + (* 2. Push the input values *) + let ctx = + let inputs = List.combine input_locals vl in + (* Note that this function checks that the variables and their values + * have the same type (this is important) *) + push_vars meta inputs ctx + in - (* Continue *) - cc cf ctx + (* 3. Push the remaining local variables (initialized as {!Bottom}) *) + let ctx = push_uninitialized_vars meta locals ctx in + + (* Execute the function body *) + let ctx_resl, cc = comp cc (eval_function_body config body_st ctx) in + + (* Pop the stack frame and move the return value to its destination *) + let ctx_resl_cfl = + List.map + (fun (ctx, res) -> + match res with + | Panic -> ((ctx, Panic), fun e -> e) + | Return -> + (* Pop the stack frame, retrieve the return value, move it to + its destination and continue *) + let ctx, cf = pop_frame_assign config meta dest ctx in + ((ctx, Unit), cf) + | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _ + | EndContinue _ -> + craise __FILE__ __LINE__ meta "Unreachable") + ctx_resl + in + let ctx_resl, cfl = List.split ctx_resl_cfl in + let cf_pop el = + match el with + | None -> None + | Some el -> + Some + (List.map Option.get (List.map2 (fun cf e -> cf (Some e)) cfl el)) + in + (* Continue *) + (ctx_resl, cc_comp cc cf_pop) (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *) and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta) - (call : call) : st_cm_fun = - fun cf ctx -> + (call : call) : stl_cm_fun = + fun ctx -> let func, generics, trait_method_generics, def, regions_hierarchy, inst_sg = eval_transparent_function_call_symbolic_inst meta call ctx in @@ -1383,7 +1388,7 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta) (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config def.item_meta.meta func def.signature regions_hierarchy inst_sg generics trait_method_generics - call.args call.dest cf ctx + call.args call.dest ctx (** Evaluate a function call in symbolic mode by using the function signature. @@ -1401,8 +1406,8 @@ and eval_function_call_symbolic_from_inst_sig (config : config) (regions_hierarchy : region_var_groups) (inst_sg : inst_fun_sig) (generics : generic_args) (trait_method_generics : (generic_args * trait_instance_id) option) - (args : operand list) (dest : place) : st_cm_fun = - fun cf ctx -> + (args : operand list) (dest : place) : stl_cm_fun = + fun ctx -> log#ldebug (lazy ("eval_function_call_symbolic_from_inst_sig:\n- fid: " @@ -1428,70 +1433,65 @@ and eval_function_call_symbolic_from_inst_sig (config : config) let dest_place = Some (S.mk_mplace meta dest ctx) in (* Evaluate the input operands *) - let cc = eval_operands config meta args in + let args, ctx, cc = eval_operands config meta args ctx in (* Generate the abstractions and insert them in the context *) let abs_ids = List.map (fun rg -> rg.id) inst_sg.regions_hierarchy in - let cf_call cf (args : typed_value list) : m_fun = - fun ctx -> - let args_with_rtypes = List.combine args inst_sg.inputs in - - (* Check the type of the input arguments *) - cassert __FILE__ __LINE__ - (List.for_all - (fun ((arg, rty) : typed_value * rty) -> - arg.ty = Subst.erase_regions rty) - args_with_rtypes) - meta "The input arguments don't have the proper type"; - (* Check that the input arguments don't contain symbolic values that can't - * be fed to functions (i.e., symbolic values output from function return - * values and which contain borrows of borrows can't be used as function - * inputs *) - sanity_check __FILE__ __LINE__ - (List.for_all - (fun arg -> - not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) - args) - meta; - - (* Initialize the abstractions and push them in the context. - * First, we define the function which, given an initialized, empty - * abstraction, computes the avalues which should be inserted inside. - *) - let compute_abs_avalues (abs : abs) (ctx : eval_ctx) : - eval_ctx * typed_avalue list = - (* Project over the input values *) - let ctx, args_projs = - List.fold_left_map - (fun ctx (arg, arg_rty) -> - apply_proj_borrows_on_input_value config meta ctx abs.regions - abs.ancestors_regions arg arg_rty) - ctx args_with_rtypes - in - (* Group the input and output values *) - (ctx, List.append args_projs [ ret_av abs.regions ]) - in - (* Actually initialize and insert the abstractions *) - let call_id = fresh_fun_call_id () in - let region_can_end _ = true in - let ctx = - create_push_abstractions_from_abs_region_groups - (fun rg_id -> FunCall (call_id, rg_id)) - inst_sg.regions_hierarchy region_can_end compute_abs_avalues ctx - in + let args_with_rtypes = List.combine args inst_sg.inputs in - (* Apply the continuation *) - let expr = cf ctx in + (* Check the type of the input arguments *) + cassert __FILE__ __LINE__ + (List.for_all + (fun ((arg, rty) : typed_value * rty) -> + arg.ty = Subst.erase_regions rty) + args_with_rtypes) + meta "The input arguments don't have the proper type"; + (* Check that the input arguments don't contain symbolic values that can't + * be fed to functions (i.e., symbolic values output from function return + * values and which contain borrows of borrows can't be used as function + * inputs *) + sanity_check __FILE__ __LINE__ + (List.for_all + (fun arg -> + not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) + args) + meta; - (* Synthesize the symbolic AST *) - S.synthesize_regular_function_call fid call_id ctx sg regions_hierarchy - abs_ids generics trait_method_generics args args_places ret_spc dest_place - expr + (* Initialize the abstractions and push them in the context. + * First, we define the function which, given an initialized, empty + * abstraction, computes the avalues which should be inserted inside. + *) + let compute_abs_avalues (abs : abs) (ctx : eval_ctx) : + eval_ctx * typed_avalue list = + (* Project over the input values *) + let ctx, args_projs = + List.fold_left_map + (fun ctx (arg, arg_rty) -> + apply_proj_borrows_on_input_value config meta ctx abs.regions + abs.ancestors_regions arg arg_rty) + ctx args_with_rtypes + in + (* Group the input and output values *) + (ctx, List.append args_projs [ ret_av abs.regions ]) + in + (* Actually initialize and insert the abstractions *) + let call_id = fresh_fun_call_id () in + let region_can_end _ = true in + let ctx = + create_push_abstractions_from_abs_region_groups + (fun rg_id -> FunCall (call_id, rg_id)) + inst_sg.regions_hierarchy region_can_end compute_abs_avalues ctx + in + (* Synthesize the symbolic AST *) + let cc = + cc_comp cc + (S.synthesize_regular_function_call fid call_id ctx sg regions_hierarchy + abs_ids generics trait_method_generics args args_places ret_spc + dest_place) in - let cc = comp cc cf_call in (* Move the return value to its destination *) - let cc = comp cc (assign_to_place config meta ret_value dest) in + let ctx, cc = comp cc (assign_to_place config meta ret_value dest ctx) in (* End the abstractions which don't contain loans and don't have parent * abstractions. @@ -1499,8 +1499,7 @@ and eval_function_call_symbolic_from_inst_sig (config : config) * retry (because then we might end their children abstractions) *) let abs_ids = ref abs_ids in - let rec end_abs_with_no_loans cf : m_fun = - fun ctx -> + let rec end_abs_with_no_loans ctx = (* Find the abstractions which don't contain loans *) let no_loans_abs, with_loans_abs = List.partition @@ -1521,35 +1520,36 @@ and eval_function_call_symbolic_from_inst_sig (config : config) abs_ids := with_loans_abs; (* End the abstractions which can be ended *) let no_loans_abs = AbstractionId.Set.of_list no_loans_abs in - let cc = InterpreterBorrows.end_abstractions config meta no_loans_abs in + let ctx, cc = + InterpreterBorrows.end_abstractions config meta no_loans_abs ctx + in (* Recursive call *) - let cc = comp cc end_abs_with_no_loans in - (* Continue *) - cc cf ctx) + comp cc (end_abs_with_no_loans ctx)) else (* No abstractions to end: continue *) - cf ctx + (ctx, fun e -> e) in (* Try to end the abstractions with no loans if: * - the option is enabled * - the function returns unit * (see the documentation of {!config} for more information) *) - let cc = - if Config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output - then comp cc end_abs_with_no_loans - else cc + let ctx, cc = + comp cc + (if Config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output + then end_abs_with_no_loans ctx + else (ctx, fun e -> e)) in (* Continue - note that we do as if the function call has been successful, * by giving {!Unit} to the continuation, because we place us in the case * where we haven't panicked. Of course, the translation needs to take the * panic case into account... *) - cc (cf Unit) ctx + ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ meta cc) (** Evaluate a non-local function call in symbolic mode *) and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta) - (fid : assumed_fun_id) (call : call) (func : fn_ptr) : st_cm_fun = - fun cf ctx -> + (fid : assumed_fun_id) (call : call) (func : fn_ptr) : stl_cm_fun = + fun ctx -> let generics = func.generics in let args = call.args in let dest = call.dest in @@ -1570,7 +1570,8 @@ and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta) | BoxFree -> (* Degenerate case: box_free - note that this is not really a function * call: no need to call a "synthesize_..." function *) - eval_box_free config meta generics args dest (cf Unit) ctx + let ctx, cc = eval_box_free config meta generics args dest ctx in + ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ meta cc) | _ -> (* "Normal" case: not box_free *) (* In symbolic mode, the behaviour of a function call is completely defined @@ -1598,25 +1599,34 @@ and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta) (* Evaluate the function call *) eval_function_call_symbolic_from_inst_sig config meta (FunId (FAssumed fid)) sg regions_hierarchy inst_sig generics None args - dest cf ctx + dest ctx (** Evaluate a statement seen as a function body *) -and eval_function_body (config : config) (body : statement) : st_cm_fun = - fun cf ctx -> +and eval_function_body (config : config) (body : statement) : stl_cm_fun = + fun ctx -> log#ldebug (lazy "eval_function_body:"); - let cc = eval_statement config body in - let cf_finish cf res = - log#ldebug (lazy "eval_function_body: cf_finish"); - (* Note that we *don't* check the result ({!Panic}, {!Return}, etc.): we - * delegate the check to the caller. *) - (* Expand the symbolic values if necessary - we need to do that before - * checking the invariants *) - let cc = greedy_expand_symbolic_values config body.meta in - (* Sanity check *) - let cc = comp_check_ctx cc (Invariants.check_invariants body.meta) in - (* Check if right meta *) - (* Continue *) - cc (cf res) + let ctx_resl, cf_body = eval_statement config body ctx in + let ctx_res_cfl = + List.map + (fun (ctx, res) -> + log#ldebug (lazy "eval_function_body: cf_finish"); + (* Note that we *don't* check the result ({!Panic}, {!Return}, etc.): we + * delegate the check to the caller. *) + (* Expand the symbolic values if necessary - we need to do that before + * checking the invariants *) + let ctx, cf = greedy_expand_symbolic_values config body.meta ctx in + (* Sanity check *) + Invariants.check_invariants body.meta ctx; + (* Continue *) + ((ctx, res), cf)) + ctx_resl + in + let ctx_resl, cfl = List.split ctx_res_cfl in + let cf_end el = + match el with + | None -> None + | Some el -> + Some (List.map Option.get (List.map2 (fun cf e -> cf (Some e)) cfl el)) in (* Compose and continue *) - comp cc cf_finish cf ctx + (ctx_resl, cc_comp cf_body cf_end) diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli index 7a2783bb..79ce1f73 100644 --- a/compiler/InterpreterStatements.mli +++ b/compiler/InterpreterStatements.mli @@ -17,7 +17,11 @@ open Cps continuation with [None]. *) val pop_frame : - config -> Meta.meta -> bool -> (typed_value option -> m_fun) -> m_fun + config -> + Meta.meta -> + bool -> + eval_ctx -> + typed_value option * eval_ctx * (eval_result -> eval_result) (** Helper. @@ -46,7 +50,7 @@ val create_push_abstractions_from_abs_region_groups : eval_ctx (** Evaluate a statement *) -val eval_statement : config -> statement -> st_cm_fun +val eval_statement : config -> statement -> stl_cm_fun (** Evaluate a statement seen as a function body *) -val eval_function_body : config -> statement -> st_cm_fun +val eval_function_body : config -> statement -> stl_cm_fun diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index 4ee11cbd..a10ba89e 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -5,7 +5,6 @@ open Contexts open LlbcAst open Utils open TypesUtils -open Cps open Errors (* TODO: we should probably rename the file to ContextsUtils *) @@ -15,19 +14,6 @@ let log = Logging.interpreter_log (** Some utilities *) -(** Auxiliary function - call a function which requires a continuation, - and return the let context given to the continuation *) -let get_cf_ctx_no_synth (meta : Meta.meta) (f : cm_fun) (ctx : eval_ctx) : - eval_ctx = - let nctx = ref None in - let cf ctx = - sanity_check __FILE__ __LINE__ (!nctx = None) meta; - nctx := Some ctx; - None - in - let _ = f cf ctx in - Option.get !nctx - let eval_ctx_to_string_no_filter = Print.Contexts.eval_ctx_to_string_no_filter let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string let name_to_string = Print.EvalCtx.name_to_string diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index 689db0c4..bae48f24 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -4,7 +4,6 @@ open Types open Values open Contexts -open Cps open TypesUtils open InterpreterUtils open InterpreterBorrowsCore @@ -876,9 +875,3 @@ let check_invariants (meta : Meta.meta) (ctx : eval_ctx) : unit = check_typing_invariant meta ctx; check_symbolic_values meta ctx) else log#ldebug (lazy "Not checking invariants (check is not activated)") - -(** Same as {!check_invariants}, but written in CPS *) -let cf_check_invariants (meta : Meta.meta) : cm_fun = - fun cf ctx -> - check_invariants meta ctx; - cf ctx diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 576b2809..8e578a50 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -200,5 +200,3 @@ let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list) let save_snapshot (ctx : Contexts.eval_ctx) (e : expression option) : expression option = match e with None -> None | Some e -> Some (Meta (Snapshot ctx, e)) - -let cf_save_snapshot : Cps.cm_fun = fun cf ctx -> save_snapshot ctx (cf ctx) |