diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Driver.ml | 14 | ||||
| -rw-r--r-- | compiler/Extract.ml | 8 | ||||
| -rw-r--r-- | compiler/ExtractAssumed.ml | 49 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 22 | ||||
| -rw-r--r-- | compiler/LlbcAstUtils.ml | 20 | ||||
| -rw-r--r-- | compiler/Translate.ml | 36 | ||||
| -rw-r--r-- | compiler/dune | 1 |
7 files changed, 112 insertions, 38 deletions
diff --git a/compiler/Driver.ml b/compiler/Driver.ml index d88962db..0fde1d74 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -222,20 +222,6 @@ let () = in if has_loops then log#lwarning (lazy "Support for loops is experimental"); - (* If we target Lean, we request the crates to be split into several files - whenever there are opaque functions *) - if - !backend = Lean - && A.FunDeclId.Map.exists - (fun _ (d : A.fun_decl) -> d.body = None) - m.functions - && not !split_files - then ( - log#error - "For Lean, we request the -split-file option whenever using opaque \ - functions"; - fail ()); - (* We don't support mutually recursive definitions with decreases clauses in Lean *) if !backend = Lean && !extract_decreases_clauses diff --git a/compiler/Extract.ml b/compiler/Extract.ml index de6c2fc8..74540787 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -8,6 +8,7 @@ open Pure open PureUtils open TranslateCore open ExtractBase +open ExtractAssumed open StringUtils open Config module F = Format @@ -3852,8 +3853,13 @@ let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) (* Print the type *) F.pp_open_hovbox fmt 0; extract_ty ctx fmt TypeDeclId.Set.empty false ty; + (* Close the definition *) + F.pp_print_string fmt ")"; + F.pp_close_box fmt (); + (* Close the definition box *) F.pp_close_box fmt (); - (* Close the definition boxe *) F.pp_close_box fmt () + (* Add a line *) + F.pp_print_space fmt () (** Extract a global declaration. diff --git a/compiler/ExtractAssumed.ml b/compiler/ExtractAssumed.ml new file mode 100644 index 00000000..bbcedb2b --- /dev/null +++ b/compiler/ExtractAssumed.ml @@ -0,0 +1,49 @@ +(** This file declares external identifiers that we catch to map them to + definitions coming from the standard libraries in our backends. *) + +open Utils +open StringUtils +open Names + +type simple_name = string list [@@deriving show, ord] + +let name_to_simple_name (s : name) : simple_name = + (* We simply ignore the disambiguators *) + List.filter_map (function Ident id -> Some id | Disambiguator _ -> None) s + +(** Small helper which cuts a string at the occurrences of "::" *) +let string_to_simple_name (s : string) : simple_name = + (* No function to split by using string separator?? *) + let name = String.split_on_char ':' s in + List.filter (fun s -> s <> "") name + +module SimpleNameOrd = struct + type t = simple_name + + let compare = compare_simple_name + let to_string = show_simple_name + let pp_t = pp_simple_name + let show_t = show_simple_name +end + +module SimpleNameMap = Collections.MakeMap (SimpleNameOrd) + +let assumed_globals : (string * string) list = + [ + ("core::num::usize::MAX", "usize_max"); + ("core::num::u8::MAX", "u8_max"); + ("core::num::u16::MAX", "u16_max"); + ("core::num::u32::MAX", "u32_max"); + ("core::num::u64::MAX", "u64_max"); + ("core::num::u128::MAX", "u128_max"); + ("core::num::isize::MAX", "isize_max"); + ("core::num::i8::MAX", "i8_max"); + ("core::num::i16::MAX", "i16_max"); + ("core::num::i32::MAX", "i32_max"); + ("core::num::i64::MAX", "i64_max"); + ("core::num::i128::MAX", "i128_max"); + ] + +let assumed_globals_map : string SimpleNameMap.t = + SimpleNameMap.of_list + (List.map (fun (x, y) -> (string_to_simple_name x, y)) assumed_globals) diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 435aa10c..9c9e08a5 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -5,6 +5,7 @@ open TranslateCore module C = Contexts module RegionVarId = T.RegionVarId module F = Format +open ExtractAssumed (** The local logger *) let log = L.pure_to_extract_log @@ -1198,12 +1199,23 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : extraction_ctx = (* TODO: update once the body id can be an option *) let is_opaque = false in - let name = ctx.fmt.global_name def.name in let decl = GlobalId def.def_id in - let body = FunId (FromLlbc (Regular def.body_id, None, None)) in - let ctx = ctx_add is_opaque decl (name ^ "_c") ctx in - let ctx = ctx_add is_opaque body (name ^ "_body") ctx in - ctx + + (* Check if the global corresponds to an assumed global that we should map + to a custom definition in our standard library (for instance, happens + with "core::num::usize::MAX") *) + let sname = name_to_simple_name def.name in + match SimpleNameMap.find_opt sname assumed_globals_map with + | Some name -> + (* Yes: register the custom binding *) + ctx_add is_opaque decl name ctx + | None -> + (* Not the case: "standard" registration *) + let name = ctx.fmt.global_name def.name in + let body = FunId (FromLlbc (Regular def.body_id, None, None)) in + let ctx = ctx_add is_opaque decl (name ^ "_c") ctx in + let ctx = ctx_add is_opaque body (name ^ "_body") ctx in + ctx let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl) (ctx : extraction_ctx) : string = diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 1111c297..8c8bbabe 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -12,3 +12,23 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : match fun_id with | Regular id -> (FunDeclId.Map.find id fun_decls).name | Assumed aid -> Assumed.get_assumed_name aid + +(** Return the opaque declarations found in the crate. + + Remark: the list of functions also contains the list of opaque global bodies. + *) +let crate_get_opaque_decls (k : crate) : T.type_decl list * fun_decl list = + let open ExtractAssumed in + let is_opaque_fun (d : fun_decl) : bool = + let sname = name_to_simple_name d.name in + d.body = None && not (SimpleNameMap.mem sname assumed_globals_map) + in + let is_opaque_type (d : T.type_decl) : bool = d.kind = T.Opaque in + (* Note that by checking the function bodies we also the globals *) + ( List.filter is_opaque_type (T.TypeDeclId.Map.values k.types), + List.filter is_opaque_fun (FunDeclId.Map.values k.functions) ) + +(** Return true if the crate contains opaque declarations, ignoring the assumed + definitions. *) +let crate_has_opaque_decls (k : crate) : bool = + crate_get_opaque_decls k <> ([], []) diff --git a/compiler/Translate.ml b/compiler/Translate.ml index a4041751..90066163 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -430,19 +430,9 @@ type gen_config = { } (** Returns the pair: (has opaque type decls, has opaque fun decls) *) -let module_has_opaque_decls (ctx : gen_ctx) : bool * bool = - let has_opaque_types = - Pure.TypeDeclId.Map.exists - (fun _ (d : Pure.type_decl) -> - match d.kind with Opaque -> true | _ -> false) - ctx.trans_types - in - let has_opaque_funs = - A.FunDeclId.Map.exists - (fun _ (trans : pure_fun_translation) -> Option.is_none trans.fwd.f.body) - ctx.trans_funs - in - (has_opaque_types, has_opaque_funs) +let crate_has_opaque_decls (ctx : gen_ctx) : bool * bool = + let types, funs = LlbcAstUtils.crate_get_opaque_decls ctx.crate in + (types <> [], funs <> []) (** Export a type declaration. @@ -557,11 +547,20 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) let body = trans.fwd.f in let is_opaque = Option.is_none body.Pure.body in - if + (* Check if we extract the global *) + let extract = config.extract_globals && (((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque)) - then + in + (* Check if it is an assumed global - if yes, we ignore it because we + map the definition to one in the standard library *) + let open ExtractAssumed in + let sname = name_to_simple_name global.name in + let extract = + extract && SimpleNameMap.find_opt sname assumed_globals_map = None + in + if extract then (* We don't wrap global declaration groups between calls to functions [{start, end}_global_decl_group] (which don't exist): global declaration groups are always singletons, so the [extract_global_decl] function @@ -828,7 +827,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) config.extract_opaque && config.extract_fun_decls && !Config.wrap_opaque_in_sig && - let _, opaque_funs = module_has_opaque_decls ctx in + let _, opaque_funs = crate_has_opaque_decls ctx in opaque_funs in if wrap_in_sig then ( @@ -1233,7 +1232,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : (* 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 ctx in + let has_opaque_types, has_opaque_funs = crate_has_opaque_decls ctx in let has_opaque_types = has_opaque_types || !Config.use_state in (* Extract the types *) @@ -1302,7 +1301,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : in extract_file template_clauses_config ctx file_info); - (* Extract the opaque functions, if needed *) + (* Extract the opaque declarations, if needed *) let opaque_funs_module = if has_opaque_funs then ( (* In the case of Lean we generate a template file *) @@ -1330,6 +1329,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : { base_gen_config with extract_fun_decls = true; + extract_globals = true; extract_transparent = false; extract_opaque = true; interface = true; diff --git a/compiler/dune b/compiler/dune index db099c3c..2f5a0a44 100644 --- a/compiler/dune +++ b/compiler/dune @@ -22,6 +22,7 @@ Expressions ExpressionsUtils Extract + ExtractAssumed ExtractBase FunsAnalysis Identifiers |