From 85629935e24c7ae068314d3eaeffad04b0e8349f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 28 Jan 2022 02:02:25 +0100
Subject: Apply the micro-passes to the pure ASTs

---
 src/PrintPure.ml       |  2 +-
 src/PureMicroPasses.ml | 16 ++++++++++++++++
 src/Translate.ml       | 25 ++++++++++++++-----------
 src/TranslateCore.ml   |  2 ++
 4 files changed, 33 insertions(+), 12 deletions(-)

(limited to 'src')

diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index f78e4a97..064d8b9d 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -189,7 +189,7 @@ let var_to_string (fmt : type_formatter) (v : var) : string =
   let varname =
     match v.basename with
     | Some name -> name ^ "^" ^ VarId.to_string v.id
-    | None -> "@" ^ VarId.to_string v.id
+    | None -> "^" ^ VarId.to_string v.id
   in
   "(" ^ varname ^ " : " ^ ty_to_string fmt v.ty ^ ")"
 
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 3e04912a..043e8ca9 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -307,6 +307,15 @@ let remove_meta (def : fun_def) : fun_def =
     [ctx]: used only for printing.
  *)
 let apply_passes_to_def (ctx : trans_ctx) (def : fun_def) : fun_def =
+  (* Debug *)
+  log#ldebug
+    (lazy
+      ("PureMicroPasses.apply_passes_to_def: "
+      ^ Print.name_to_string def.basename
+      ^ " ("
+      ^ Print.option_to_string T.RegionGroupId.to_string def.back_id
+      ^ ")"));
+
   (* First, find names for the variables which are unnamed *)
   let def = compute_pretty_names def in
   log#ldebug (lazy ("compute_pretty_name:\n" ^ fun_def_to_string ctx def));
@@ -317,3 +326,10 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_def) : fun_def =
 
   (* We are done *)
   def
+
+let apply_passes_to_pure_fun_translation (ctx : trans_ctx)
+    (trans : pure_fun_translation) : pure_fun_translation =
+  let forward, backwards = trans in
+  let forward = apply_passes_to_def ctx forward in
+  let backwards = List.map (apply_passes_to_def ctx) backwards in
+  (forward, backwards)
diff --git a/src/Translate.ml b/src/Translate.ml
index 0971ba3d..d70c1486 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -17,20 +17,19 @@ type symbolic_fun_translation = V.symbolic_value list * SA.expression
     - the generated symbolic AST
  *)
 
-type pure_fun_translation = Pure.fun_def * Pure.fun_def list
-
 (** 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)
-    (type_context : C.type_context) (fun_context : C.fun_context)
-    (fdef : A.fun_def) :
+    (trans_ctx : trans_ctx) (fdef : A.fun_def) :
     symbolic_fun_translation * symbolic_fun_translation list =
   (* Debug *)
   log#ldebug
     (lazy
       ("translate_function_to_symbolics: " ^ Print.name_to_string fdef.A.name));
 
+  let { type_context; fun_context } = trans_ctx in
+
   (* Evaluate *)
   let synthesize = true in
   let evaluate gid =
@@ -59,7 +58,7 @@ let translate_function_to_symbolics (config : C.partial_config)
     TODO: maybe we should introduce a record for this.
  *)
 let translate_function_to_pure (config : C.partial_config)
-    (type_context : C.type_context) (fun_context : C.fun_context)
+    (trans_ctx : trans_ctx)
     (fun_sigs :
       SymbolicToPure.fun_sig_named_outputs SymbolicToPure.RegularFunIdMap.t)
     (fdef : A.fun_def) : pure_fun_translation =
@@ -67,11 +66,12 @@ let translate_function_to_pure (config : C.partial_config)
   log#ldebug
     (lazy ("translate_function_to_pure: " ^ Print.name_to_string fdef.A.name));
 
+  let { type_context; fun_context } = trans_ctx in
   let def_id = fdef.def_id in
 
   (* Compute the symbolic ASTs *)
   let symbolic_forward, symbolic_backwards =
-    translate_function_to_symbolics config type_context fun_context fdef
+    translate_function_to_symbolics config trans_ctx fdef
   in
 
   (* Convert the symbolic ASTs to pure ASTs: *)
@@ -193,6 +193,7 @@ let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) :
 
   (* Compute the type and function contexts *)
   let type_context, fun_context = compute_type_fun_contexts m in
+  let trans_ctx = { type_context; fun_context } in
 
   (* Translate all the type definitions *)
   let type_defs = SymbolicToPure.translate_type_defs m.types in
@@ -221,13 +222,15 @@ let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) :
 
   (* Translate all the functions *)
   let pure_translations =
-    List.map
-      (translate_function_to_pure config type_context fun_context fun_sigs)
-      m.functions
+    List.map (translate_function_to_pure config trans_ctx fun_sigs) m.functions
   in
 
-  (* (* Apply the micro-passes *)
-     let pure_translations = List.map (Micro.apply_passes_to_def ctx)*)
+  (* Apply the micro-passes *)
+  let pure_translations =
+    List.map
+      (Micro.apply_passes_to_pure_fun_translation trans_ctx)
+      pure_translations
+  in
 
   (* Return *)
   (type_defs, pure_translations)
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
index 9374d3b9..02528f9a 100644
--- a/src/TranslateCore.ml
+++ b/src/TranslateCore.ml
@@ -13,6 +13,8 @@ let log = L.translate_log
 
 type trans_ctx = { type_context : C.type_context; fun_context : C.fun_context }
 
+type pure_fun_translation = Pure.fun_def * Pure.fun_def list
+
 let type_def_to_string (ctx : trans_ctx) (def : Pure.type_def) : string =
   let type_params = def.type_params in
   let type_defs = ctx.type_context.type_defs in
-- 
cgit v1.2.3