diff options
Diffstat (limited to 'compiler/InterpreterLoops.ml')
| -rw-r--r-- | compiler/InterpreterLoops.ml | 239 |
1 files changed, 141 insertions, 98 deletions
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) |