diff options
Diffstat (limited to 'compiler/Translate.ml')
| -rw-r--r-- | compiler/Translate.ml | 151 |
1 files changed, 34 insertions, 117 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 72322c73..453e02db 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -11,63 +11,6 @@ open TranslateCore (** The local logger *) let log = TranslateCore.log -type config = { - eval_config : Contexts.partial_config; - mp_config : Micro.config; - use_state : bool; - (** Controls whether we need to use a state to model the external world - (I/O, for instance). - *) - backward_no_state_update : bool; - (** Controls whether backward functions update the state, in case we use - a state ({!use_state}). - - If they update the state, we generate code of the following style: - {[ - (st1, y) <-- f_fwd x st0; // st0 is the state upon calling f_fwd - ... - (st3, x') <-- f_back x st0 y' st2; // st2 is the state upon calling f_back - }] - - Otherwise, we generate code of the following shape: - {[ - (st1, y) <-- f_fwd x st0; - ... - x' <-- f_back x st0 y'; - }] - - The second format is easier to reason about, but the first one is - necessary to properly handle some Rust functions which use internal - mutability such as {{:https://doc.rust-lang.org/std/cell/struct.RefCell.html#method.try_borrow_mut} [RefCell::try_mut_borrow]}: - in order to model this behaviour we would need a state, and calling the backward - function would update the state by reinserting the updated value in it. - *) - split_files : bool; - (** Controls whether we split the generated definitions between different - files for the types, clauses and functions, or if we group them in - one file. - *) - 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 ()) - ]} - *) - extract_decreases_clauses : bool; - (** If [true], insert [decreases] clauses for all the recursive definitions. - - The body of such clauses must be defined by the user. - *) - extract_template_decreases_clauses : bool; - (** In order to help the user, we can generate "template" decrease clauses - (i.e., definitions with proper signatures but dummy bodies) in a - dedicated file. - *) -} - (** The result of running the symbolic interpreter on a function: - the list of symbolic values used for the input values - the generated symbolic AST @@ -77,9 +20,8 @@ type symbolic_fun_translation = V.symbolic_value list * SA.expression (** 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) - (trans_ctx : trans_ctx) (fdef : A.fun_decl) : - (symbolic_fun_translation * symbolic_fun_translation list) option = +let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : A.fun_decl) + : (symbolic_fun_translation * symbolic_fun_translation list) option = (* Debug *) log#ldebug (lazy @@ -96,7 +38,7 @@ let translate_function_to_symbolics (config : C.partial_config) let synthesize = true in let evaluate gid = let inputs, symb = - evaluate_function_symbolic config synthesize type_context fun_context + evaluate_function_symbolic synthesize type_context fun_context global_context fdef gid in (inputs, Option.get symb) @@ -119,9 +61,7 @@ let translate_function_to_symbolics (config : C.partial_config) of backward functions, we also provide names for the outputs. TODO: maybe we should introduce a record for this. *) -let translate_function_to_pure (config : C.partial_config) - (mp_config : Micro.config) (backward_no_state_update : bool) - (trans_ctx : trans_ctx) +let translate_function_to_pure (trans_ctx : trans_ctx) (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdMap.t) (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl) : pure_fun_translation = @@ -134,7 +74,7 @@ let translate_function_to_pure (config : C.partial_config) let def_id = fdef.def_id in (* Compute the symbolic ASTs, if the function is transparent *) - let symbolic_trans = translate_function_to_symbolics config trans_ctx fdef in + let symbolic_trans = translate_function_to_symbolics trans_ctx fdef in let symbolic_forward, symbolic_backwards = match symbolic_trans with | None -> (None, None) @@ -210,21 +150,12 @@ let translate_function_to_pure (config : C.partial_config) { ctx with forward_inputs } in - (* The symbolic to pure config *) - let sp_config = - { - SymbolicToPure.filter_useless_back_calls = - mp_config.filter_useless_monadic_calls; - backward_no_state_update; - } - in - (* Translate the forward function *) let pure_forward = match symbolic_forward with - | None -> SymbolicToPure.translate_fun_decl sp_config ctx None + | None -> SymbolicToPure.translate_fun_decl ctx None | Some (fwd_svs, fwd_ast) -> - SymbolicToPure.translate_fun_decl sp_config + SymbolicToPure.translate_fun_decl (add_forward_inputs fwd_svs ctx) (Some fwd_ast) in @@ -247,7 +178,7 @@ let translate_function_to_pure (config : C.partial_config) let ctx = { ctx with bid = Some back_id; sg = backward_sg.sg } in (* Translate *) - SymbolicToPure.translate_fun_decl sp_config ctx None + SymbolicToPure.translate_fun_decl ctx None | Some symbolic_backwards -> let input_svs, symbolic = T.RegionGroupId.nth symbolic_backwards back_id @@ -259,8 +190,8 @@ let translate_function_to_pure (config : C.partial_config) in (* We need to ignore the forward inputs, and the state input (if there is) *) let fun_info = - SymbolicToPure.get_fun_effect_info backward_no_state_update - fun_context.fun_infos (A.Regular def_id) (Some back_id) + SymbolicToPure.get_fun_effect_info fun_context.fun_infos + (A.Regular def_id) (Some back_id) in let backward_inputs = (* We need to ignore the forward state and the backward state *) @@ -313,7 +244,7 @@ let translate_function_to_pure (config : C.partial_config) in (* Translate *) - SymbolicToPure.translate_fun_decl sp_config ctx (Some symbolic) + SymbolicToPure.translate_fun_decl ctx (Some symbolic) in let pure_backwards = List.map translate_backward fdef.signature.regions_hierarchy @@ -322,9 +253,7 @@ let translate_function_to_pure (config : C.partial_config) (* Return *) (pure_forward, pure_backwards) -let translate_module_to_pure (config : C.partial_config) - (mp_config : Micro.config) (use_state : bool) - (backward_no_state_update : bool) (crate : A.crate) : +let translate_module_to_pure (crate : A.crate) : trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list = (* Debug *) log#ldebug (lazy "translate_module_to_pure"); @@ -335,7 +264,7 @@ let translate_module_to_pure (config : C.partial_config) in let fun_infos = FA.analyze_module crate fun_context.C.fun_decls - global_context.C.global_decls use_state + global_context.C.global_decls !Config.use_state in let fun_context = { fun_decls = fun_context.fun_decls; fun_infos } in let trans_ctx = { type_context; fun_context; global_context } in @@ -372,22 +301,21 @@ let translate_module_to_pure (config : C.partial_config) in let sigs = List.append assumed_sigs local_sigs in let fun_sigs = - SymbolicToPure.translate_fun_signatures backward_no_state_update - fun_context.fun_infos type_context.type_infos sigs + SymbolicToPure.translate_fun_signatures fun_context.fun_infos + type_context.type_infos sigs in (* Translate all the *transparent* functions *) let pure_translations = List.map - (translate_function_to_pure config mp_config backward_no_state_update - trans_ctx fun_sigs type_decls_map) + (translate_function_to_pure trans_ctx fun_sigs type_decls_map) crate.functions in (* Apply the micro-passes *) let pure_translations = List.map - (Micro.apply_passes_to_pure_fun_translation mp_config trans_ctx) + (Micro.apply_passes_to_pure_fun_translation trans_ctx) pure_translations in @@ -404,8 +332,6 @@ type gen_ctx = { } type gen_config = { - mp_config : Micro.config; - use_state : bool; extract_types : bool; extract_decreases_clauses : bool; extract_template_decreases_clauses : bool; @@ -423,7 +349,7 @@ type gen_config = { declarations in an interface file, together with an implementation file if needed. *) - test_unit_functions : bool; + test_trans_unit_functions : bool; } (** Returns the pair: (has opaque type decls, has opaque fun decls) *) @@ -538,7 +464,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) has_decr_clause def) fls); (* Insert unit tests if necessary *) - if config.test_unit_functions then + if config.test_trans_unit_functions then List.iter (fun (keep_fwd, (fwd, _)) -> if keep_fwd then @@ -665,13 +591,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) (** Translate a module and write the synthesized code to an output file. TODO: rename to translate_crate *) -let translate_module (filename : string) (dest_dir : string) (config : config) - (crate : A.crate) : unit = +let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : + unit = (* Translate the module to the pure AST *) - let trans_ctx, trans_types, trans_funs = - translate_module_to_pure config.eval_config config.mp_config - config.use_state config.backward_no_state_update crate - in + let trans_ctx, trans_types, trans_funs = translate_module_to_pure crate in (* Initialize the extraction context - for now we extract only to F*. * We initialize the names map by registering the keywords used in the @@ -796,30 +719,26 @@ let translate_module (filename : string) (dest_dir : string) (config : config) } in - let use_state = config.use_state in - (* Extract one or several files, depending on the configuration *) - if config.split_files then ( + if !Config.split_files then ( let base_gen_config = { - mp_config = config.mp_config; - use_state; extract_types = false; - extract_decreases_clauses = config.extract_decreases_clauses; + extract_decreases_clauses = !Config.extract_decreases_clauses; extract_template_decreases_clauses = false; extract_fun_decls = false; extract_transparent = true; extract_opaque = false; extract_state_type = false; interface = false; - test_unit_functions = false; + test_trans_unit_functions = false; } in (* Check if there are opaque types and functions - in which case we need * to split *) let has_opaque_types, has_opaque_funs = module_has_opaque_decls gen_ctx in - let has_opaque_types = has_opaque_types || use_state in + let has_opaque_types = has_opaque_types || !Config.use_state in (* Extract the types *) (* If there are opaque types, we extract in an interface *) @@ -831,7 +750,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) base_gen_config with extract_types = true; extract_opaque = true; - extract_state_type = use_state; + extract_state_type = !Config.use_state; interface = has_opaque_types; } in @@ -840,10 +759,10 @@ let translate_module (filename : string) (dest_dir : string) (config : config) (* Extract the template clauses *) let needs_clauses_module = - config.extract_decreases_clauses + !Config.extract_decreases_clauses && not (A.FunDeclId.Set.is_empty rec_functions) in - (if needs_clauses_module && config.extract_template_decreases_clauses then + (if needs_clauses_module && !Config.extract_template_decreases_clauses then let clauses_filename = extract_filebasename ^ ".Clauses.Template.fst" in let clauses_module = module_name ^ ".Clauses.Template" in let clauses_config = @@ -880,7 +799,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) { base_gen_config with extract_fun_decls = true; - test_unit_functions = config.test_unit_functions; + test_trans_unit_functions = !Config.test_trans_unit_functions; } in let clauses_module = @@ -892,18 +811,16 @@ let translate_module (filename : string) (dest_dir : string) (config : config) else let gen_config = { - mp_config = config.mp_config; - use_state; extract_types = true; - extract_decreases_clauses = config.extract_decreases_clauses; + extract_decreases_clauses = !Config.extract_decreases_clauses; extract_template_decreases_clauses = - config.extract_template_decreases_clauses; + !Config.extract_template_decreases_clauses; extract_fun_decls = true; extract_transparent = true; extract_opaque = true; - extract_state_type = use_state; + extract_state_type = !Config.use_state; interface = false; - test_unit_functions = config.test_unit_functions; + test_trans_unit_functions = !Config.test_trans_unit_functions; } in (* Add the extension for F* *) |