diff options
Diffstat (limited to 'compiler/Translate.ml')
| -rw-r--r-- | compiler/Translate.ml | 82 |
1 files changed, 42 insertions, 40 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 9af3c71b..04aadafe 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -3,6 +3,7 @@ open Types open Values open LlbcAst open Contexts +open Errors module SA = SymbolicAst module Micro = PureMicroPasses open TranslateCore @@ -40,7 +41,7 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) : of backward functions, we also provide names for the outputs. TODO: maybe we should introduce a record for this. *) -let translate_function_to_pure (trans_ctx : trans_ctx) +let translate_function_to_pure (meta : Meta.meta) (trans_ctx : trans_ctx) (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) : pure_fun_translation_no_loops = @@ -175,7 +176,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) SymbolicToPure.fresh_named_vars_for_symbolic_values input_svs ctx in { ctx with forward_inputs } - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in (* Add the backward inputs *) @@ -194,7 +195,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx) | Some (_, ast) -> SymbolicToPure.translate_fun_decl ctx (Some ast) (* TODO: factor out the return type *) -let translate_crate_to_pure (crate : crate) : +let translate_crate_to_pure (meta : Meta.meta) (crate : crate) : trans_ctx * Pure.type_decl list * pure_fun_translation list @@ -207,7 +208,7 @@ let translate_crate_to_pure (crate : crate) : let trans_ctx = compute_contexts crate in (* Translate all the type definitions *) - let type_decls = SymbolicToPure.translate_type_decls trans_ctx in + let type_decls = SymbolicToPure.translate_type_decls meta trans_ctx in (* Compute the type definition map *) let type_decls_map = @@ -221,7 +222,7 @@ let translate_crate_to_pure (crate : crate) : (List.map (fun (fdef : LlbcAst.fun_decl) -> ( fdef.def_id, - SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx + SymbolicToPure.translate_fun_sig_from_decl_to_decomposed meta trans_ctx fdef )) (FunDeclId.Map.values crate.fun_decls)) in @@ -229,21 +230,21 @@ let translate_crate_to_pure (crate : crate) : (* Translate all the *transparent* functions *) let pure_translations = List.map - (translate_function_to_pure trans_ctx type_decls_map fun_dsigs) + (translate_function_to_pure meta trans_ctx type_decls_map fun_dsigs) (FunDeclId.Map.values crate.fun_decls) in (* Translate the trait declarations *) let trait_decls = List.map - (SymbolicToPure.translate_trait_decl trans_ctx) + (SymbolicToPure.translate_trait_decl meta trans_ctx) (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls) in (* Translate the trait implementations *) let trait_impls = List.map - (SymbolicToPure.translate_trait_impl trans_ctx) + (SymbolicToPure.translate_trait_impl meta trans_ctx) (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls) in @@ -351,9 +352,9 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) [is_rec]: [true] if the types are recursive. Necessarily [true] if there is > 1 type to extract. *) -let export_types_group (fmt : Format.formatter) (config : gen_config) +let export_types_group (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (is_rec : bool) (ids : Pure.TypeDeclId.id list) : unit = - assert (ids <> []); + cassert (ids <> []) meta "TODO: Error message"; let export_type = export_type fmt config ctx in let ids_set = Pure.TypeDeclId.Set.of_list ids in let export_type_decl kind id = export_type ids_set kind id true false in @@ -395,11 +396,11 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) if List.exists (fun b -> b) builtin then (* Sanity check *) - assert (List.for_all (fun b -> b) builtin) + cassert (List.for_all (fun b -> b) builtin) meta "TODO: Error message" else if List.exists dont_extract defs then (* Check if we have to ignore declarations *) (* Sanity check *) - assert (List.for_all dont_extract defs) + cassert (List.for_all dont_extract defs) meta "TODO: Error message" else ( (* Extract the type declarations. @@ -441,13 +442,14 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) TODO: check correct behavior with opaque globals. *) -let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) +let export_global (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (id : GlobalDeclId.id) : unit = let global_decls = ctx.trans_ctx.global_ctx.global_decls in let global = GlobalDeclId.Map.find id global_decls in let trans = FunDeclId.Map.find global.body ctx.trans_funs in - assert (trans.loops = []); - let body = trans.f in + assert (trans.fwd.loops = []); + assert (trans.backs = []); + let body = trans.fwd.f in let is_opaque = Option.is_none body.Pure.body in (* Check if we extract the global *) @@ -491,7 +493,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) Rem.: this function doesn't check [config.extract_fun_decls]: it should have been checked by the caller. *) -let export_functions_group_scc (fmt : Format.formatter) (config : gen_config) +let export_functions_group_scc (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (is_rec : bool) (decls : Pure.fun_decl list) : unit = (* Utility to check a function has a decrease clause *) let has_decreases_clause (def : Pure.fun_decl) : bool = @@ -502,7 +504,7 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config) (* Extract the function declarations *) (* Check if the functions are mutually recursive *) let is_mut_rec = List.length decls > 1 in - assert ((not is_mut_rec) || is_rec); + cassert ((not is_mut_rec) || is_rec) meta "TODO: Error message"; let decls_length = List.length decls in (* We open and close the declaration group with [{start, end}_fun_decl_group]. @@ -566,7 +568,7 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config) In case of (non-mutually) recursive functions, we use a simple procedure to check if the forward and backward functions are mutually recursive. *) -let export_functions_group (fmt : Format.formatter) (config : gen_config) +let export_functions_group (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) (pure_ls : pure_fun_translation list) : unit = (* Check if the definition are builtin - if yes they must be ignored. Note that if one definition in the group is builtin, then all the @@ -582,7 +584,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) if List.exists (fun b -> b) builtin then (* Sanity check *) - assert (List.for_all (fun b -> b) builtin) + cassert (List.for_all (fun b -> b) builtin) meta "TODO: Error message" else (* Utility to check a function has a decrease clause *) let has_decreases_clause (def : Pure.fun_decl) : bool = @@ -614,11 +616,11 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) | FStar -> Extract.extract_template_fstar_decreases_clause ctx fmt decl | Coq -> - raise - (Failure "Coq doesn't have decreases/termination clauses") + craise + meta "Coq doesn't have decreases/termination clauses" | HOL4 -> - raise - (Failure "HOL4 doesn't have decreases/termination clauses") + craise + meta "HOL4 doesn't have decreases/termination clauses" in extract_decrease f.f; List.iter extract_decrease f.loops) @@ -637,7 +639,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) (* Extract the subgroups *) let export_subgroup (is_rec : bool) (decls : Pure.fun_decl list) : unit = - export_functions_group_scc fmt config ctx is_rec decls + export_functions_group_scc meta fmt config ctx is_rec decls in List.iter (fun (is_rec, decls) -> export_subgroup is_rec decls) subgroups); @@ -692,16 +694,16 @@ let export_trait_impl (fmt : Format.formatter) (_config : gen_config) split the definitions between different files (or not), we can control what is precisely extracted. *) -let extract_definitions (fmt : Format.formatter) (config : gen_config) +let extract_definitions (meta : Meta.meta) (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) : unit = (* Export the definition groups to the file, in the proper order. - [extract_decl]: extract the type declaration (if not filtered) - [extract_extra_info]: extra the extra type information (e.g., the [Arguments] information in Coq). *) - let export_functions_group = export_functions_group fmt config ctx in - let export_global = export_global fmt config ctx in - let export_types_group = export_types_group fmt config ctx in + let export_functions_group = export_functions_group meta fmt config ctx in + let export_global = export_global meta fmt config ctx in + let export_types_group = export_types_group meta fmt config ctx in let export_trait_decl_group id = export_trait_decl fmt config ctx id true false in @@ -783,7 +785,7 @@ type extract_file_info = { custom_includes : string list; } -let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) +let extract_file (meta : Meta.meta) (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) : unit = (* Open the file and create the formatter *) let out = open_out fi.filename in @@ -883,7 +885,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) Format.pp_open_vbox fmt 0; (* Extract the definitions *) - extract_definitions fmt config ctx; + extract_definitions meta fmt config ctx; (* Close the box and end the formatting *) Format.pp_close_box fmt (); @@ -903,11 +905,11 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) close_out out (** Translate a crate and write the synthesized code to an output file. *) -let translate_crate (filename : string) (dest_dir : string) (crate : crate) : +let translate_crate (meta : Meta.meta) (filename : string) (dest_dir : string) (crate : crate) : unit = (* Translate the module to the pure AST *) let trans_ctx, trans_types, trans_funs, trans_trait_decls, trans_trait_impls = - translate_crate_to_pure crate + translate_crate_to_pure meta crate in (* Initialize the names map by registering the keywords used in the @@ -1036,7 +1038,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : match Filename.chop_suffix_opt ~suffix:".llbc" filename with | None -> (* Note that we already checked the suffix upon opening the file *) - raise (Failure "Unreachable") + craise meta "Unreachable" | Some filename -> (* Retrieve the file basename *) let basename = Filename.basename filename in @@ -1078,7 +1080,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : let ( ^^ ) = Filename.concat in if !Config.split_files then mkdir_if (dest_dir ^^ crate_name); if needs_clauses_module then ( - assert !Config.split_files; + cassert !Config.split_files meta "TODO: Error message"; mkdir_if (dest_dir ^^ crate_name ^^ "Clauses"))); (* Copy the "Primitives" file, if necessary *) @@ -1228,7 +1230,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : custom_includes = []; } in - extract_file opaque_config ctx file_info; + extract_file meta opaque_config ctx file_info; (* Return the additional dependencies *) [ opaque_imported_module ]) else [] @@ -1269,7 +1271,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : custom_includes = opaque_types_module; } in - extract_file types_config ctx file_info; + extract_file meta types_config ctx file_info; (* Extract the template clauses *) (if needs_clauses_module && !Config.extract_template_decreases_clauses then @@ -1298,7 +1300,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : custom_includes = []; } in - extract_file template_clauses_config ctx file_info); + extract_file meta template_clauses_config ctx file_info); (* Extract the opaque fun declarations, if needed *) let opaque_funs_module = @@ -1354,7 +1356,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : custom_includes = [ types_module ]; } in - extract_file opaque_config ctx file_info; + extract_file meta opaque_config ctx file_info; (* Return the additional dependencies *) [ opaque_imported_module ]) else [] @@ -1395,7 +1397,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : [ types_module ] @ opaque_funs_module @ clauses_module; } in - extract_file fun_config ctx file_info) + extract_file meta fun_config ctx file_info) else let gen_config = { @@ -1428,7 +1430,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : custom_includes = []; } in - extract_file gen_config ctx file_info); + extract_file meta gen_config ctx file_info); (* Generate the build file *) match !Config.backend with |