From 239435fc667fa0d18979e603ce3fd4caa128cd54 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 23 May 2024 23:21:12 +0200 Subject: Update the interpreter so that it is not written in CPS style (#120) * Start turning the compiler in a style which is less CPS * Update a function in InterpreterExpressions.ml * WIP work on cps * WIP * WIP, currently on InterpreterStatements.ml * WIP * Finished CPS-related modification * Fixed some warning related to documentation comments * Finished loop support, fixed a loop * fixed a typed value * Fixed check_disappeared related error * cleaned check_disappeared related error * Start cleaning up * Do more cleanup * Make some cleanup and fix an issue * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Do more cleanup * Rename a function * Do more cleanup * Cleanup the loops code and fix some bugs * Cleanup assign_to_place * Make a minor cleanup --------- Co-authored-by: Son Ho --- compiler/InterpreterLoops.ml | 239 +++++++++++++++++++++++++------------------ 1 file changed, 141 insertions(+), 98 deletions(-) (limited to 'compiler/InterpreterLoops.ml') 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) -- cgit v1.2.3 From b294639a5cbd2a51fc5bb5e55e0c386ee568ca8c Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Fri, 24 May 2024 13:28:12 +0200 Subject: Rename meta into span --- compiler/InterpreterLoops.ml | 72 ++++++++++++++++++++++---------------------- 1 file changed, 36 insertions(+), 36 deletions(-) (limited to 'compiler/InterpreterLoops.ml') diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 3264bd18..776cb6fa 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -15,7 +15,7 @@ open Errors let log = Logging.loops_log (** Evaluate a loop in concrete mode *) -let eval_loop_concrete (meta : Meta.meta) (eval_loop_body : stl_cm_fun) : +let eval_loop_concrete (span : Meta.span) (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 @@ -54,10 +54,10 @@ let eval_loop_concrete (meta : Meta.meta) (eval_loop_body : stl_cm_fun) : * {!Unit} would account for the first iteration of the loop. * We prefer to write it this way for consistency and sanity, * though. *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> (* We can't get there: this is only used in symbolic mode *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ span "Unreachable" in (* Apply - for the first iteration, we use the result `Continue 0` to evaluate @@ -65,20 +65,20 @@ let eval_loop_concrete (meta : Meta.meta) (eval_loop_body : stl_cm_fun) : 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; + sanity_check __FILE__ __LINE__ (el = None) span; None in (ctx_resl, cf) (** Evaluate a loop in symbolic mode *) -let eval_loop_symbolic (config : config) (meta : meta) +let eval_loop_symbolic (config : config) (span : span) (eval_loop_body : stl_cm_fun) : stl_cm_fun = fun ctx -> (* Debug *) log#ldebug (lazy ("eval_loop_symbolic:\nContext:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx + ^ eval_ctx_to_string ~span:(Some span) ctx ^ "\n\n")); (* Generate a fresh loop id *) @@ -86,20 +86,20 @@ let eval_loop_symbolic (config : config) (meta : meta) (* Compute the fixed point at the loop entrance *) let fp_ctx, fixed_ids, rg_to_abs = - compute_loop_entry_fixed_point config meta loop_id eval_loop_body ctx + compute_loop_entry_fixed_point config span loop_id eval_loop_body ctx in (* Debug *) log#ldebug (lazy ("eval_loop_symbolic:\nInitial context:\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx + ^ eval_ctx_to_string ~span:(Some span) ctx ^ "\n\nFixed point:\n" - ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx)); + ^ eval_ctx_to_string ~span:(Some span) fp_ctx)); (* Compute the loop input parameters *) let fresh_sids, input_svalues = - compute_fp_ctx_symbolic_values meta ctx fp_ctx + compute_fp_ctx_symbolic_values span ctx fp_ctx in let fp_input_svalues = List.map (fun sv -> sv.sv_id) input_svalues in @@ -119,7 +119,7 @@ let eval_loop_symbolic (config : config) (meta : meta) - 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 ctx + prepare_match_ctx_with_target config span loop_id fixed_ids fp_ctx ctx in (* Actually match *) @@ -132,23 +132,23 @@ let eval_loop_symbolic (config : config) (meta : meta) (* Compute the id correspondance between the contexts *) let fp_bl_corresp = - compute_fixed_point_id_correspondance meta fixed_ids ctx fp_ctx + compute_fixed_point_id_correspondance span fixed_ids ctx fp_ctx in log#ldebug (lazy ("eval_loop_symbolic: about to match the fixed-point context with the \ original context:\n\ - src ctx (fixed-point ctx)" - ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx + ^ eval_ctx_to_string ~span:(Some span) fp_ctx ^ "\n\n-tgt ctx (original context):\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + ^ eval_ctx_to_string ~span:(Some span) 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 + (match_ctx_with_target config span loop_id true fp_bl_corresp fp_input_svalues fixed_ids fp_ctx ctx) in (res_fun_end, fp_bl_corresp) @@ -177,26 +177,26 @@ let eval_loop_symbolic (config : config) (meta : meta) | Panic -> ((ctx, res), fun e -> e) | Break _ -> (* Breaks should have been eliminated in the prepasses *) - craise __FILE__ __LINE__ meta "Unexpected break" + craise __FILE__ __LINE__ span "Unexpected break" | Continue i -> (* We don't support nested loops for now *) - cassert __FILE__ __LINE__ (i = 0) meta + cassert __FILE__ __LINE__ (i = 0) span "Nested loops are not supported yet"; log#ldebug (lazy ("eval_loop_symbolic: about to match the fixed-point context \ with the context at a continue:\n\ - src ctx (fixed-point ctx)" - ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx + ^ eval_ctx_to_string ~span:(Some span) fp_ctx ^ "\n\n-tgt ctx (ctx at continue):\n" - ^ eval_ctx_to_string ~meta:(Some meta) ctx)); - match_ctx_with_target config meta loop_id false fp_bl_corresp + ^ eval_ctx_to_string ~span:(Some span) ctx)); + match_ctx_with_target config span 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" + craise __FILE__ __LINE__ span "Unreachable" in (* Apply and compose *) @@ -219,9 +219,9 @@ let eval_loop_symbolic (config : config) (meta : meta) log#ldebug (lazy ("eval_loop_symbolic: result:" ^ "\n- src context:\n" - ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx + ^ eval_ctx_to_string_no_filter ~span:(Some span) ctx ^ "\n- fixed point:\n" - ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp_ctx + ^ eval_ctx_to_string_no_filter ~span:(Some span) fp_ctx ^ "\n- fixed_sids: " ^ SymbolicValueId.Set.show fixed_ids.sids ^ "\n- fresh_sids: " @@ -247,7 +247,7 @@ let eval_loop_symbolic (config : config) (meta : meta) match av.value with | ABorrow _ -> true | ALoan _ -> false - | _ -> craise __FILE__ __LINE__ meta "Unreachable" + | _ -> craise __FILE__ __LINE__ span "Unreachable" in let borrows, loans = List.partition is_borrow abs.avalues in @@ -256,10 +256,10 @@ let eval_loop_symbolic (config : config) (meta : meta) (fun (av : typed_avalue) -> match av.value with | ABorrow (AMutBorrow (bid, child_av)) -> - sanity_check __FILE__ __LINE__ (is_aignored child_av.value) meta; + sanity_check __FILE__ __LINE__ (is_aignored child_av.value) span; Some (bid, child_av.ty) | ABorrow (ASharedBorrow _) -> None - | _ -> craise __FILE__ __LINE__ meta "Unreachable") + | _ -> craise __FILE__ __LINE__ span "Unreachable") borrows in let borrows = ref (BorrowId.Map.of_list borrows) in @@ -269,10 +269,10 @@ let eval_loop_symbolic (config : config) (meta : meta) (fun (av : typed_avalue) -> match av.value with | ALoan (AMutLoan (bid, child_av)) -> - sanity_check __FILE__ __LINE__ (is_aignored child_av.value) meta; + sanity_check __FILE__ __LINE__ (is_aignored child_av.value) span; Some bid | ALoan (ASharedLoan _) -> None - | _ -> craise __FILE__ __LINE__ meta "Unreachable") + | _ -> craise __FILE__ __LINE__ span "Unreachable") loans in @@ -288,7 +288,7 @@ let eval_loop_symbolic (config : config) (meta : meta) ty) loan_ids in - sanity_check __FILE__ __LINE__ (BorrowId.Map.is_empty !borrows) meta; + sanity_check __FILE__ __LINE__ (BorrowId.Map.is_empty !borrows) span; given_back_tys in @@ -301,25 +301,25 @@ let eval_loop_symbolic (config : config) (meta : meta) | None -> None | Some el -> ( match el with - | [] -> internal_error __FILE__ __LINE__ meta + | [] -> internal_error __FILE__ __LINE__ span | 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) + fun_end_expr loop_expr span) in (res_fun_end :: resl_loop_body, cc) -let eval_loop (config : config) (meta : meta) (eval_loop_body : stl_cm_fun) : +let eval_loop (config : config) (span : span) (eval_loop_body : stl_cm_fun) : stl_cm_fun = fun ctx -> match config.mode with - | ConcreteMode -> (eval_loop_concrete meta eval_loop_body) ctx + | ConcreteMode -> (eval_loop_concrete span 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 ctx, cc = - cleanup_fresh_values_and_abs config meta empty_ids_set ctx + cleanup_fresh_values_and_abs config span empty_ids_set ctx in (* We want to make sure the loop will *not* manipulate shared avalues @@ -340,5 +340,5 @@ let eval_loop (config : config) (meta : meta) (eval_loop_body : stl_cm_fun) : introduce *fixed* abstractions, and again later to introduce *non-fixed* abstractions. *) - let ctx, cc = comp cc (prepare_ashared_loans meta None ctx) in - comp cc (eval_loop_symbolic config meta eval_loop_body ctx) + let ctx, cc = comp cc (prepare_ashared_loans span None ctx) in + comp cc (eval_loop_symbolic config span eval_loop_body ctx) -- cgit v1.2.3