summaryrefslogtreecommitdiff
path: root/compiler/Interpreter.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/Interpreter.ml')
-rw-r--r--compiler/Interpreter.ml188
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)