summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-26 22:59:51 +0100
committerSon Ho2022-01-26 22:59:51 +0100
commit3e36b8c3b81a64d5f85dbff0f171741bb4c03423 (patch)
tree506b5340658adc02bcec96485ac8495c032d5a97
parent7729f9c571981e3ace548cbb780cb35662fba807 (diff)
Start actually generating symbolic ASTs for the backward functions
-rw-r--r--src/Identifiers.ml4
-rw-r--r--src/Interpreter.ml20
2 files changed, 18 insertions, 6 deletions
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 0a3e1c9d..3a900643 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -61,6 +61,8 @@ module type Id = sig
TODO: generalize to `map_from_i`
*)
+ val iteri : (id -> 'a -> unit) -> 'a list -> unit
+
module Ord : C.OrderedType with type t = id
module Set : C.Set with type elt = id
@@ -131,6 +133,8 @@ module IdGen () : Id = struct
in
aux 1 ls
+ let iteri = List.iteri
+
module Ord = struct
type t = id
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index bcfb9a78..a02b363e 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -99,9 +99,8 @@ let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def) :
*)
let evaluate_function_symbolic_synthesize_backward_from_return
- (config : C.config) (m : M.cfim_module) (fdef : A.fun_def)
- (inst_sg : A.inst_fun_sig) (back_id : T.RegionGroupId.id) (ctx : C.eval_ctx)
- : SA.expression option =
+ (config : C.config) (fdef : A.fun_def) (inst_sg : A.inst_fun_sig)
+ (back_id : T.RegionGroupId.id) (ctx : C.eval_ctx) : SA.expression option =
(* 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
@@ -212,7 +211,7 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
| Some back_id ->
(* Backward translation *)
evaluate_function_symbolic_synthesize_backward_from_return config
- m fdef inst_sg back_id ctx
+ fdef inst_sg back_id ctx
else None
| Panic ->
(* Note that as we explore all the execution branches, one of
@@ -292,8 +291,17 @@ module Test = struct
log#ldebug
(lazy ("test_function_symbolic: " ^ Print.name_to_string fdef.A.name));
- (* Execute *)
- let _ = evaluate_function_symbolic config synthesize m fid None in
+ (* Evaluate *)
+ let evaluate = evaluate_function_symbolic config synthesize m fid in
+ (* Execute the forward function *)
+ let _ = evaluate None in
+ (* Execute the backward functions *)
+ let _ =
+ T.RegionGroupId.iteri
+ (fun gid _ -> evaluate (Some gid))
+ fdef.signature.regions_hierarchy
+ in
+
()
(** Execute the symbolic interpreter on a list of functions.