summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/PrintPure.ml2
-rw-r--r--src/PureMicroPasses.ml16
-rw-r--r--src/Translate.ml25
-rw-r--r--src/TranslateCore.ml2
4 files changed, 33 insertions, 12 deletions
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