diff options
Diffstat (limited to 'compiler/Interpreter.ml')
| -rw-r--r-- | compiler/Interpreter.ml | 188 |
1 files changed, 88 insertions, 100 deletions
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 94158979..fb3701f3 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -277,7 +277,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) : let evaluate_function_symbolic_synthesize_backward_from_return (config : config) (fdef : fun_decl) (inst_sg : inst_fun_sig) (back_id : RegionGroupId.id) (loop_id : LoopId.id option) (is_regular_return : bool) (inside_loop : bool) - (ctx : eval_ctx) : SA.expression option = + (ctx : eval_ctx) : SA.expression = log#ldebug (lazy ("evaluate_function_symbolic_synthesize_backward_from_return:" @@ -477,8 +477,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) (* 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)) + | None -> SA.Return (ctx, None) + | Some loop_id -> SA.ReturnWithLoop (loop_id, inside_loop) in (* Apply *) cc return_expr @@ -486,12 +486,12 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) (** Evaluate a function with the symbolic interpreter. We return: - - the list of symbolic values introduced for the input values (this is useful - for the synthesis) + - the list of symbolic values introduced for the input values (this is + useful for the synthesis) - the symbolic AST generated by the symbolic execution *) -let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) - (fdef : fun_decl) : symbolic_value list * SA.expression option = +let evaluate_function_symbolic (ctx : decls_ctx) (fdef : fun_decl) : + symbolic_value list * SA.expression = (* Debug *) let name_to_string () = Print.Types.name_to_string @@ -518,101 +518,92 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) match res with | Return | LoopReturn _ -> - if synthesize then - (* We have to "play different endings": - * - one execution for the forward function - * - one execution per backward function - * We then group everything together. - *) - (* There are two cases: - * - if this is a forward translation, we retrieve the returned value. - * - if this is a backward translation, we introduce "return" - * abstractions to consume the return value, then end all the - * abstractions up to the one in which we are interested. - *) - (* Forward translation: retrieve the returned value *) - let fwd_e = - (* Pop the frame and retrieve the returned value at the same time *) - let pop_return_value = true in - let ret_value, ctx, cc_pop = - pop_frame config fdef.item_meta.span pop_return_value ctx - in - (* Generate the Return node *) - cc_pop (Some (SA.Return (ctx, ret_value))) - in - let fwd_e = Option.get fwd_e in - (* Backward translation: introduce "return" - abstractions to consume the return value, then end all the - abstractions up to the one in which we are interested. - *) - let loop_id = - match res with - | Return -> None - | LoopReturn loop_id -> Some loop_id - | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "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 is_regular_return inside_loop ctx) - in - let back_el = - RegionGroupId.mapi - (fun gid _ -> (gid, finish_back_eval gid)) - regions_hierarchy + (* We have to "play different endings": + * - one execution for the forward function + * - one execution per backward function + * We then group everything together. + *) + (* There are two cases: + * - if this is a forward translation, we retrieve the returned value. + * - if this is a backward translation, we introduce "return" + * abstractions to consume the return value, then end all the + * abstractions up to the one in which we are interested. + *) + (* Forward translation: retrieve the returned value *) + let fwd_e = + (* Pop the frame and retrieve the returned value at the same time *) + let pop_return_value = true in + let ret_value, ctx, cc_pop = + pop_frame config fdef.item_meta.span pop_return_value ctx in - let back_el = RegionGroupId.Map.of_list back_el in - (* Put everything together *) - synthesize_forward_end ctx0 None fwd_e back_el - else None + (* Generate the Return node *) + cc_pop (SA.Return (ctx, ret_value)) + in + (* Backward translation: introduce "return" + abstractions to consume the return value, then end all the + abstractions up to the one in which we are interested. + *) + let loop_id = + match res with + | Return -> None + | LoopReturn loop_id -> Some loop_id + | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable" + in + let is_regular_return = true in + let inside_loop = Option.is_some loop_id in + let finish_back_eval back_id = + evaluate_function_symbolic_synthesize_backward_from_return config fdef + inst_sg back_id loop_id is_regular_return inside_loop ctx + in + let back_el = + RegionGroupId.mapi + (fun gid _ -> (gid, finish_back_eval gid)) + regions_hierarchy + in + let back_el = RegionGroupId.Map.of_list back_el in + (* Put everything together *) + synthesize_forward_end ctx0 None fwd_e back_el | EndEnterLoop (loop_id, loop_input_values) | EndContinue (loop_id, loop_input_values) -> (* Similar to [Return]: we have to play different endings *) - if synthesize then - let inside_loop = - match res with - | EndEnterLoop _ -> false - | EndContinue _ -> true - | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable" - in - (* Forward translation *) - let fwd_e = - (* 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 _ret_value, _ctx, cc_pop = - pop_frame config fdef.item_meta.span pop_return_value ctx - in - (* Generate the Return node *) - cc_pop (Some (SA.ReturnWithLoop (loop_id, inside_loop))) - in - let fwd_e = Option.get fwd_e in - (* Backward translation: introduce "return" - 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) is_regular_return - inside_loop ctx) - in - let back_el = - RegionGroupId.mapi - (fun gid _ -> (gid, finish_back_eval gid)) - regions_hierarchy + let inside_loop = + match res with + | EndEnterLoop _ -> false + | EndContinue _ -> true + | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable" + in + (* Forward translation *) + let fwd_e = + (* 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 _ret_value, _ctx, cc_pop = + pop_frame config fdef.item_meta.span pop_return_value ctx in - let back_el = RegionGroupId.Map.of_list back_el in - (* Put everything together *) - synthesize_forward_end ctx0 (Some loop_input_values) fwd_e back_el - else None + (* Generate the Return node *) + cc_pop (SA.ReturnWithLoop (loop_id, inside_loop)) + in + (* Backward translation: introduce "return" + 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 = + evaluate_function_symbolic_synthesize_backward_from_return config fdef + inst_sg back_id (Some loop_id) is_regular_return inside_loop ctx + in + let back_el = + RegionGroupId.mapi + (fun gid _ -> (gid, finish_back_eval gid)) + regions_hierarchy + in + let back_el = RegionGroupId.Map.of_list back_el in + (* Put everything together *) + synthesize_forward_end ctx0 (Some loop_input_values) fwd_e back_el | Panic -> (* Note that as we explore all the execution branches, one of * the executions can lead to a panic *) - if synthesize then Some SA.Panic else None + SA.Panic | Unit | Break _ | Continue _ -> craise __FILE__ __LINE__ fdef.item_meta.span ("evaluate_function_symbolic failed on: " ^ name_to_string ()) @@ -624,12 +615,9 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) 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 (span, msg) -> Some (Error (span, msg)) + let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in + cc el + with CFailure (span, msg) -> Error (span, msg) in (* Return *) (input_svs, symbolic) |