blob: 69e0933414ef6c067220f3f2eb32ef43bba3d905 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
module L = Logging
module T = Types
module A = CfimAst
module M = Modules
module SA = SymbolicAst
open Errors
open Cps
open InterpreterUtils
open InterpreterStatements
(** The local logger *)
let log = L.translate_log
(** 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_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
(* Return *)
(forward, backwards)
(*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 *)
let fun_defs = SymbolicToPure.translate_fun_signatures types_infos
raise Unimplemented*)
|
