diff options
| -rw-r--r-- | src/Interpreter.ml | 38 | ||||
| -rw-r--r-- | src/Translate.ml | 23 |
2 files changed, 29 insertions, 32 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 2641069b..53c2a091 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -28,10 +28,9 @@ let compute_type_fun_contexts (m : M.cfim_module) : let fun_context = { C.fun_defs } in (type_context, fun_context) -let initialize_eval_context (m : M.cfim_module) (type_vars : T.type_var list) : - C.eval_ctx = +let initialize_eval_context (type_context : C.type_context) + (fun_context : C.fun_context) (type_vars : T.type_var list) : C.eval_ctx = C.reset_global_counters (); - let type_context, fun_context = compute_type_fun_contexts m in { C.type_context; C.fun_context; @@ -48,7 +47,8 @@ let initialize_eval_context (m : M.cfim_module) (type_vars : T.type_var list) : Abstractions are introduced for the regions present in the function signature. *) -let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def) : +let initialize_symbolic_context_for_fun (type_context : C.type_context) + (fun_context : C.fun_context) (fdef : A.fun_def) : C.eval_ctx * A.inst_fun_sig = (* The abstractions are not initialized the same way as for function * calls: they contain *loan* projectors, because they "provide" us @@ -63,7 +63,7 @@ let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def) : * *) let sg = fdef.signature in (* Create the context *) - let ctx = initialize_eval_context m sg.type_params in + let ctx = initialize_eval_context type_context fun_context sg.type_params in (* Instantiate the signature *) let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in let inst_sg = instantiate_fun_sig type_params sg in @@ -174,11 +174,9 @@ 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) : SA.expression option = - (* Retrieve the function declaration *) - let fdef = A.FunDefId.nth m.functions fid in - + (type_context : C.type_context) (fun_context : C.fun_context) + (fdef : A.fun_def) (back_id : T.RegionGroupId.id option) : + SA.expression option = (* Debug *) let name_to_string () = Print.name_to_string fdef.A.name @@ -189,7 +187,9 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) log#ldebug (lazy ("evaluate_function_symbolic: " ^ name_to_string ())); (* Create the evaluation context *) - let ctx, inst_sg = initialize_symbolic_context_for_fun m fdef in + let ctx, inst_sg = + initialize_symbolic_context_for_fun type_context fun_context fdef + in (* Create the continuation to finish the evaluation *) let config = C.config_of_partial C.SymbolicMode config in @@ -249,7 +249,8 @@ module Test = struct assert (fdef.A.arg_count = 0); (* Create the evaluation context *) - let ctx = initialize_eval_context m [] in + let type_context, fun_context = compute_type_fun_contexts m in + let ctx = initialize_eval_context type_context fun_context [] in (* Insert the (uninitialized) local variables *) let ctx = C.ctx_push_uninitialized_vars ctx fdef.A.locals in @@ -288,16 +289,16 @@ module Test = struct (** Execute the symbolic interpreter on a function. *) let test_function_symbolic (config : C.partial_config) (synthesize : bool) - (m : M.cfim_module) (fid : A.FunDefId.id) : unit = - (* Retrieve the function declaration *) - let fdef = A.FunDefId.nth m.functions fid in - + (type_context : C.type_context) (fun_context : C.fun_context) + (fdef : A.fun_def) : unit = (* Debug *) log#ldebug (lazy ("test_function_symbolic: " ^ Print.name_to_string fdef.A.name)); (* Evaluate *) - let evaluate = evaluate_function_symbolic config synthesize m fid in + let evaluate = + evaluate_function_symbolic config synthesize type_context fun_context fdef + in (* Execute the forward function *) let _ = evaluate None in (* Execute the backward functions *) @@ -319,11 +320,12 @@ module Test = struct let no_loop_funs = List.filter (fun f -> not (CfimAstUtils.fun_def_has_loops f)) m.functions in + let type_context, fun_context = compute_type_fun_contexts m in let test_fun (def : A.fun_def) : unit = (* Execute the function - note that as the symbolic interpreter explores * all the path, some executions are expected to "panic": we thus don't * check the return value *) - test_function_symbolic config synthesize m def.A.def_id + test_function_symbolic config synthesize type_context fun_context def in List.iter test_fun no_loop_funs end diff --git a/src/Translate.ml b/src/Translate.ml index 79385ca3..756c28b4 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -18,11 +18,8 @@ type pure_fun_translation = Pure.fun_def * Pure.fun_def list 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 - + (type_context : C.type_context) (fun_context : C.fun_context) + (fdef : A.fun_def) : SA.expression * SA.expression list = (* Debug *) log#ldebug (lazy @@ -30,7 +27,9 @@ let translate_function_to_symbolics (config : C.partial_config) (* Evaluate *) let synthesize = true in - let evaluate = evaluate_function_symbolic config synthesize m fid in + let evaluate = + evaluate_function_symbolic config synthesize type_context fun_context fdef + in (* Execute the forward function *) let forward = Option.get (evaluate None) in (* Execute the backward functions *) @@ -43,12 +42,8 @@ let translate_function_to_symbolics (config : C.partial_config) (* Return *) (forward, backwards) -(** Translate a function, by generating its forward and backward translations. - - TODO: we shouldn't need to take m as parameter (we actually recompute the - type and function contexts in [translate_function_to_symbolics]...) - *) -let translate_function (config : C.partial_config) (m : M.cfim_module) +(** Translate a function, by generating its forward and backward translations. *) +let translate_function (config : C.partial_config) (type_context : C.type_context) (fun_context : C.fun_context) (fun_sigs : Pure.fun_sig SymbolicToPure.RegularFunIdMap.t) (fdef : A.fun_def) : pure_fun_translation = @@ -56,7 +51,7 @@ let translate_function (config : C.partial_config) (m : M.cfim_module) (* Compute the symbolic ASTs *) let symbolic_forward, symbolic_backwards = - translate_function_to_symbolics config m fdef.def_id + translate_function_to_symbolics config type_context fun_context fdef in (* Convert the symbolic ASTs to pure ASTs: *) @@ -176,7 +171,7 @@ let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) : List.map (fun (fdef : A.fun_def) -> ( fdef.def_id, - translate_function config m type_context fun_context fun_sigs fdef )) + translate_function config type_context fun_context fun_sigs fdef )) m.functions in |