diff options
| -rw-r--r-- | compiler/Interpreter.ml | 19 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 5 |
2 files changed, 15 insertions, 9 deletions
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 85da809e..69109c4e 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -125,15 +125,16 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context) this continuation takes care of doing the proper manipulations to finish the synthesis (mostly by ending abstractions). - [entered_loop]: [true] if we reached the end of the function because we - (re-)entered a loop (results [EndEnterLoop] and [EndContinue]). + [is_regular_return]: [true] if we reached a [Return] instruction (i.e., the + result is {!Return} or {LoopReturn}). [inside_loop]: [true] if we are *inside* a loop (result [EndContinue]). *) let evaluate_function_symbolic_synthesize_backward_from_return (config : C.config) (fdef : A.fun_decl) (inst_sg : A.inst_fun_sig) (back_id : T.RegionGroupId.id) (loop_id : V.LoopId.id option) - (inside_loop : bool) (ctx : C.eval_ctx) : SA.expression option = + (is_regular_return : bool) (inside_loop : bool) (ctx : C.eval_ctx) : + SA.expression option = log#ldebug (lazy ("evaluate_function_symbolic_synthesize_backward_from_return:" @@ -145,7 +146,6 @@ let evaluate_function_symbolic_synthesize_backward_from_return ^ Print.bool_to_string inside_loop ^ "\n- ctx:\n" ^ Print.Contexts.eval_ctx_to_string_gen true true ctx)); - let entered_loop = Option.is_some loop_id in (* We need to instantiate the function signature - to retrieve * the return type. Note that it is important to re-generate * an instantiation of the signature, so that we use fresh @@ -155,7 +155,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return let ret_inst_sg = instantiate_fun_sig type_params sg in let ret_rty = ret_inst_sg.output in (* Move the return value out of the return variable *) - let pop_return_value = not entered_loop in + let pop_return_value = is_regular_return in let cf_pop_frame = pop_frame config pop_return_value in (* We need to find the parents regions/abstractions of the region we @@ -177,7 +177,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return * borrow projections) *) let cf_consume_ret (ret_value : V.typed_value option) ctx = let ctx = - if not entered_loop then ( + if is_regular_return then ( let ret_value = Option.get ret_value in let compute_abs_avalues (abs : V.abs) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_avalue list = @@ -366,11 +366,12 @@ let evaluate_function_symbolic (synthesize : bool) | LoopReturn loop_id -> Some loop_id | _ -> raise (Failure "Unreachable") in + let is_regular_return = true in let inside_loop = Option.is_some loop_id in let finish_back_eval back_id = Option.get (evaluate_function_symbolic_synthesize_backward_from_return config - fdef inst_sg back_id loop_id inside_loop ctx) + fdef inst_sg back_id loop_id is_regular_return inside_loop ctx) in let back_el = T.RegionGroupId.mapi @@ -409,10 +410,12 @@ let evaluate_function_symbolic (synthesize : bool) abstractions to consume the return value, then end all the abstractions up to the one in which we are interested. *) + let is_regular_return = false in let finish_back_eval back_id = Option.get (evaluate_function_symbolic_synthesize_backward_from_return config - fdef inst_sg back_id (Some loop_id) inside_loop ctx) + fdef inst_sg back_id (Some loop_id) is_regular_return + inside_loop ctx) in let back_el = T.RegionGroupId.mapi diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 335336be..937c9103 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1028,10 +1028,13 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list = let fuel = if !Config.use_fuel then 1 else 0 in let num_inputs = List.length loop.inputs in let num_fwd_inputs_with_fuel_no_state = fuel + num_inputs in - let num_fwd_inputs_with_fuel_with_state = + let fwd_state = fun_sig_info.num_fwd_inputs_with_fuel_with_state - fun_sig_info.num_fwd_inputs_with_fuel_no_state in + let num_fwd_inputs_with_fuel_with_state = + num_fwd_inputs_with_fuel_no_state + fwd_state + in { has_fuel = !Config.use_fuel; num_fwd_inputs_with_fuel_no_state; |