From 9bfbafc5f0773037c174da8d4dda036b8b13e4f2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 27 Jan 2022 09:27:59 +0100
Subject: Change the signatures of several functions in Interpreter.ml

---
 src/Interpreter.ml | 38 ++++++++++++++++++++------------------
 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
 
-- 
cgit v1.2.3