Make a lot of small modifications

7 files changed, 70 insertions, 42 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index e7031d4c..f430c15d 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -11,6 +11,9 @@ open InterpreterUtils
 open InterpreterBorrowsCore
 open InterpreterProjectors
 
+(** The local logger *)
+let log = InterpreterBorrowsCore.log
+
 (** Auxiliary function to end borrows: lookup a borrow in the environment,
     update it (by returning an updated environment where the borrow has been
     replaced by [Bottom])) if we can end the borrow (for instance, it is not
diff --git a/src/Logging.ml b/src/Logging.ml
index ad600adc..5605772d 100644
--- a/src/Logging.ml
+++ b/src/Logging.ml
@@ -15,6 +15,9 @@ let translate_log = L.get_logger "MainLogger.Translate"
 (** Logger for SymbolicToPure *)
 let symbolic_to_pure_log = L.get_logger "MainLogger.SymbolicToPure"
 
+(** Logger for PureMicroPasses *)
+let pure_micro_passes_log = L.get_logger "MainLogger.PureMicroPasses"
+
 (** Logger for PureToExtract *)
 let pure_to_extract_log = L.get_logger "MainLogger.PureToExtract"
 
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index aab19c11..3e04912a 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -2,6 +2,10 @@
 
 open Errors
 open Pure
+open TranslateCore
+
+(** The local logger *)
+let log = L.pure_micro_passes_log
 
 type pn_ctx = string VarId.Map.t
 (** "pretty-name context": see [compute_pretty_names] *)
@@ -297,3 +301,19 @@ let remove_meta (def : fun_def) : fun_def =
   in
   let body = obj#visit_expression () def.body in
   { def with body }
+
+(** Apply all the micro-passes to a function.
+
+    [ctx]: used only for printing.
+ *)
+let apply_passes_to_def (ctx : trans_ctx) (def : fun_def) : fun_def =
+  (* 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));
+
+  (* The meta-information is now useless: remove it *)
+  let def = remove_meta def in
+  log#ldebug (lazy ("remove_meta:\n" ^ fun_def_to_string ctx def));
+
+  (* We are done *)
+  def
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 8b31bffa..d46d8386 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1298,13 +1298,8 @@ let translate_fun_def (ctx : bs_ctx) (body : S.expression) : fun_def =
   (* return *)
   def
 
-let translate_type_defs (type_defs : T.type_def list) : type_def TypeDefId.Map.t
-    =
-  List.fold_left
-    (fun tdefs def ->
-      let tdef = translate_type_def def in
-      TypeDefId.Map.add def.def_id tdef tdefs)
-    TypeDefId.Map.empty type_defs
+let translate_type_defs (type_defs : T.type_def list) : type_def list =
+  List.map translate_type_def type_defs
 
 (** Translates function signatures.
 
diff --git a/src/Translate.ml b/src/Translate.ml
index 1e8eb148..0971ba3d 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -6,31 +6,10 @@ module A = CfimAst
 module M = Modules
 module SA = SymbolicAst
 module Micro = PureMicroPasses
+open TranslateCore
 
 (** The local logger *)
-let log = L.translate_log
-
-type trans_ctx = { type_context : C.type_context; fun_context : C.fun_context }
-
-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
-  let fmt = PrintPure.mk_type_formatter type_defs type_params in
-  PrintPure.type_def_to_string fmt def
-
-let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string =
-  let type_params = sg.type_params in
-  let type_defs = ctx.type_context.type_defs in
-  let fun_defs = ctx.fun_context.fun_defs in
-  let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in
-  PrintPure.fun_sig_to_string fmt sg
-
-let fun_def_to_string (ctx : trans_ctx) (def : Pure.fun_def) : string =
-  let type_params = def.signature.type_params in
-  let type_defs = ctx.type_context.type_defs in
-  let fun_defs = ctx.fun_context.fun_defs in
-  let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in
-  PrintPure.fun_def_to_string fmt def
+let log = TranslateCore.log
 
 type symbolic_fun_translation = V.symbolic_value list * SA.expression
 (** The result of running the symbolic interpreter on a function:
@@ -208,7 +187,7 @@ let translate_function_to_pure (config : C.partial_config)
   (pure_forward, pure_backwards)
 
 let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) :
-    Pure.type_def T.TypeDefId.Map.t * pure_fun_translation A.FunDefId.Map.t =
+    Pure.type_def list * pure_fun_translation list =
   (* Debug *)
   log#ldebug (lazy "translate_module_to_pure");
 
@@ -243,19 +222,12 @@ let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) :
   (* Translate all the functions *)
   let pure_translations =
     List.map
-      (fun (fdef : A.fun_def) ->
-        ( fdef.def_id,
-          translate_function_to_pure config type_context fun_context fun_sigs
-            fdef ))
+      (translate_function_to_pure config type_context fun_context fun_sigs)
       m.functions
   in
 
-  (* Put the translated functions in a map *)
-  let fun_defs =
-    List.fold_left
-      (fun m (def_id, trans) -> A.FunDefId.Map.add def_id trans m)
-      A.FunDefId.Map.empty pure_translations
-  in
+  (* (* Apply the micro-passes *)
+     let pure_translations = List.map (Micro.apply_passes_to_def ctx)*)
 
   (* Return *)
-  (type_defs, fun_defs)
+  (type_defs, pure_translations)
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
new file mode 100644
index 00000000..9374d3b9
--- /dev/null
+++ b/src/TranslateCore.ml
@@ -0,0 +1,34 @@
+(** Some utilities for the translation *)
+
+open InterpreterStatements
+open Interpreter
+module L = Logging
+module T = Types
+module A = CfimAst
+module M = Modules
+module SA = SymbolicAst
+
+(** The local logger *)
+let log = L.translate_log
+
+type trans_ctx = { type_context : C.type_context; fun_context : C.fun_context }
+
+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
+  let fmt = PrintPure.mk_type_formatter type_defs type_params in
+  PrintPure.type_def_to_string fmt def
+
+let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string =
+  let type_params = sg.type_params in
+  let type_defs = ctx.type_context.type_defs in
+  let fun_defs = ctx.fun_context.fun_defs in
+  let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in
+  PrintPure.fun_sig_to_string fmt sg
+
+let fun_def_to_string (ctx : trans_ctx) (def : Pure.fun_def) : string =
+  let type_params = def.signature.type_params in
+  let type_defs = ctx.type_context.type_defs in
+  let fun_defs = ctx.fun_context.fun_defs in
+  let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in
+  PrintPure.fun_def_to_string fmt def
diff --git a/src/main.ml b/src/main.ml
index 1f996c2b..7381c648 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -55,6 +55,7 @@ let () =
   borrows_log#set_level EL.Debug;
   invariants_log#set_level EL.Warning;
   symbolic_to_pure_log#set_level EL.Debug;
+  pure_micro_passes_log#set_level EL.Debug;
   translate_log#set_level EL.Debug;
   (* Load the module *)
   let json = Yojson.Basic.from_file !filename in