diff options
| -rw-r--r-- | src/Identifiers.ml | 4 | ||||
| -rw-r--r-- | src/Interpreter.ml | 20 |
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. |