diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Interpreter.ml | 7 | ||||
| -rw-r--r-- | src/Translate.ml | 57 |
2 files changed, 27 insertions, 37 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index a02b363e..79f39742 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -169,7 +169,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (** Evaluate a function with the symbolic interpreter *) let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) (m : M.cfim_module) (fid : A.FunDefId.id) - (back_id : T.RegionGroupId.id option) : unit = + (back_id : T.RegionGroupId.id option) : SA.expression option = (* Retrieve the function declaration *) let fdef = A.FunDefId.nth m.functions fid in @@ -222,8 +222,7 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) in (* Evaluate the function *) - let _ = eval_function_body config fdef.A.body cf_finish ctx in - () + eval_function_body config fdef.A.body cf_finish ctx module Test = struct (** Test a unit function (taking no arguments) by evaluating it in an empty @@ -297,7 +296,7 @@ module Test = struct let _ = evaluate None in (* Execute the backward functions *) let _ = - T.RegionGroupId.iteri + T.RegionGroupId.mapi (fun gid _ -> evaluate (Some gid)) fdef.signature.regions_hierarchy in diff --git a/src/Translate.ml b/src/Translate.ml index efdad619..69e09334 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -11,46 +11,37 @@ open InterpreterStatements (** The local logger *) let log = L.translate_log -(** Execute the symbolic interpreter on a function to generate a symbolic AST. *) -let translate_function_to_symbolic (config : C.partial_config) - (m : M.cfim_module) (fid : A.FunDefId.id) - (back_id : T.RegionGroupId.id option) : unit = +(** Execute the symbolic interpreter on a function to generate a list of symbolic ASTs, + for the forward function and the backward functions. *) +let translate_function_to_symbolics (config : C.partial_config) + (m : M.cfim_module) (fid : A.FunDefId.id) : + SA.expression * SA.expression list = (* Retrieve the function declaration *) let fdef = A.FunDefId.nth m.functions fid in (* Debug *) log#ldebug (lazy - ("translate_function_to_pure: " - ^ Print.name_to_string fdef.A.name - ^ " (" - ^ Print.option_to_string T.RegionGroupId.to_string back_id - ^ ")")); - - (* Create the evaluation context *) - let ctx = initialize_symbolic_context_for_fun m fdef in - - (* Create the continuation to check the function's result *) - let cf_check res _ = - match res with - | Return -> raise Errors.Unimplemented - | 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 - | _ -> - failwith - ("Unit test failed (symbolic execution) on: " - ^ Print.name_to_string fdef.A.name) + ("translate_function_to_symbolics: " ^ Print.name_to_string fdef.A.name)); + + (* Evaluate *) + let evaluate = evaluate_function_symbolic config synthesize m fid in + (* Execute the forward function *) + let forward = evaluate None in + (* Execute the backward functions *) + let backwards = + T.RegionGroupId.mapi + (fun gid _ -> evaluate (Some gid)) + fdef.signature.regions_hierarchy in - (* Evaluate the function *) - let config = C.config_of_partial C.SymbolicMode config in - let _ = eval_function_body config fdef.A.body cf_check ctx in - () + (* Return *) + (forward, backwards) -let translate (config : C.partial_config) (m : M.cfim_module) : unit = - (* Translate all the type definitions *) +(*let translate (config : C.partial_config) (m : M.cfim_module) : unit = + (* Translate all the type definitions *) + let type_defs = SymbolicToPure.translate_type_defs m.type_defs in - (* Translate all the function signatures *) - raise Unimplemented + (* Translate all the function signatures *) + let fun_defs = SymbolicToPure.translate_fun_signatures types_infos + raise Unimplemented*) |