diff options
| -rw-r--r-- | src/PrintPure.ml | 2 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 16 | ||||
| -rw-r--r-- | src/Translate.ml | 25 | ||||
| -rw-r--r-- | src/TranslateCore.ml | 2 |
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 |