diff options
| -rw-r--r-- | src/Translate.ml | 33 | ||||
| -rw-r--r-- | src/main.ml | 16 |
2 files changed, 30 insertions, 19 deletions
diff --git a/src/Translate.ml b/src/Translate.ml index c6db9f19..ba3effc5 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -12,6 +12,20 @@ open TranslateCore (** The local logger *) let log = TranslateCore.log +type config = { + eval_config : Contexts.partial_config; + mp_config : Micro.config; + test_unit_functions : bool; + (** If true, insert tests in the generated files to check that the + unit functions normalize to `Success _`. + + For instance, in F* it generates code like this: + ``` + let _ = assert_norm (FUNCTION () = Success ()) + ``` + *) +} + type symbolic_fun_translation = V.symbolic_value list * SA.expression (** The result of running the symbolic interpreter on a function: - the list of symbolic values used for the input values @@ -272,21 +286,12 @@ let translate_module_to_pure (config : C.partial_config) (* Return *) (trans_ctx, type_defs, pure_translations) -(** Translate a module and write the synthesized code to an output file. - - [test_unit_functions]: if true, insert tests in the generated files to - check that the unit functions normalize to `Success _`. For instance, - in F* it generates code like this: - ``` - let _ = assert_norm (FUNCTION () = Success ()) - ``` - *) -let translate_module (filename : string) (dest_dir : string) - (config : C.partial_config) (mp_config : Micro.config) - (test_unit_functions : bool) (m : M.cfim_module) : unit = +(** Translate a module and write the synthesized code to an output file. *) +let translate_module (filename : string) (dest_dir : string) (config : config) + (m : M.cfim_module) : unit = (* Translate the module to the pure AST *) let trans_ctx, trans_types, trans_funs = - translate_module_to_pure config mp_config m + translate_module_to_pure config.eval_config config.mp_config m in (* Initialize the extraction context - for now we extract only to F* *) @@ -413,7 +418,7 @@ let translate_module (filename : string) (dest_dir : string) ExtractToFStar.extract_fun_def extract_ctx fmt qualif def) fls; (* Insert unit tests if necessary *) - if test_unit_functions then + if config.test_unit_functions then List.iter (fun (keep_fwd, (fwd, _)) -> if keep_fwd then diff --git a/src/main.ml b/src/main.ml index ba677361..38cb339a 100644 --- a/src/main.ml +++ b/src/main.ml @@ -123,7 +123,7 @@ let () = let m = PrePasses.apply_passes m in (* Some options for the execution *) - let config = + let eval_config = { C.check_invariants = true; greedy_expand_symbolics_with_borrows = true; @@ -132,12 +132,12 @@ let () = in (* Test the unit functions with the concrete interpreter *) - if !test_units then I.Test.test_unit_functions config m; + if !test_units then I.Test.test_unit_functions eval_config m; (* Evaluate the symbolic interpreter on the functions, ignoring the * functions which contain loops - TODO: remove *) let synthesize = true in - I.Test.test_functions_symbolic config synthesize m; + I.Test.test_functions_symbolic eval_config synthesize m; (* Translate the functions *) let test_unit_functions = !test_trans_units in @@ -150,5 +150,11 @@ let () = add_unit_args = false; } in - Translate.translate_module filename dest_dir config micro_passes_config - test_unit_functions m + let trans_config = + { + Translate.eval_config; + mp_config = micro_passes_config; + test_unit_functions; + } + in + Translate.translate_module filename dest_dir trans_config m |