diff options
| -rw-r--r-- | src/Translate.ml | 19 | ||||
| -rw-r--r-- | src/main.ml | 10 |
2 files changed, 17 insertions, 12 deletions
diff --git a/src/Translate.ml b/src/Translate.ml index e79a47c4..30d6d0f8 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -203,7 +203,8 @@ let translate_function_to_pure (config : C.partial_config) (* Return *) (pure_forward, pure_backwards) -let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) : +let translate_module_to_pure (config : C.partial_config) + (mp_config : Micro.config) (m : M.cfim_module) : trans_ctx * Pure.type_def list * pure_fun_translation list = (* Debug *) log#ldebug (lazy "translate_module_to_pure"); @@ -243,16 +244,9 @@ let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) : in (* Apply the micro-passes *) - (* TODO: move the configuration *) - let passes_config = - { - Micro.unfold_monadic_let_bindings = true; - filter_unused_monadic_calls = true; - } - in let pure_translations = List.map - (Micro.apply_passes_to_pure_fun_translation passes_config trans_ctx) + (Micro.apply_passes_to_pure_fun_translation mp_config trans_ctx) pure_translations in @@ -269,9 +263,12 @@ let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) : ``` *) let translate_module (filename : string) (config : C.partial_config) - (test_unit_functions : bool) (m : M.cfim_module) : unit = + (mp_config : Micro.config) (test_unit_functions : bool) (m : M.cfim_module) + : unit = (* Translate the module to the pure AST *) - let trans_ctx, trans_types, trans_funs = translate_module_to_pure config m in + let trans_ctx, trans_types, trans_funs = + translate_module_to_pure config mp_config m + in (* Initialize the extraction context - for now we extract only to F* *) let names_map = diff --git a/src/main.ml b/src/main.ml index bb7b0e06..7f7ed96c 100644 --- a/src/main.ml +++ b/src/main.ml @@ -6,6 +6,7 @@ module A = CfimAst module I = Interpreter module EL = Easy_logging.Logging module TA = TypesAnalysis +module Micro = PureMicroPasses (* This is necessary to have a backtrace when raising exceptions - for some * reason, the -g option doesn't work. @@ -85,4 +86,11 @@ let () = (* Translate the functions *) let test_unit_functions = true in - Translate.translate_module !filename config test_unit_functions m + let micro_passes_config = + { + Micro.unfold_monadic_let_bindings = true; + filter_unused_monadic_calls = true; + } + in + Translate.translate_module !filename config micro_passes_config + test_unit_functions m |