From 1b446285bbbe356ead7c0e521799b35020f08147 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 24 Nov 2023 17:04:26 +0100 Subject: Make a minor update in ExtractName.pattern_to_extract_name --- compiler/ExtractName.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'compiler') diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml index 41c81207..c0a23080 100644 --- a/compiler/ExtractName.ml +++ b/compiler/ExtractName.ml @@ -61,7 +61,10 @@ let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) : | TArray -> "Array" | TSlice -> "Slice" else expr_to_string c ty - | ERef _ | EVar _ -> raise (Failure "")) + | ERef _ | EVar _ -> + (* We simply convert the pattern to a string. This is not very + satisfying but we should rarely get there. *) + expr_to_string c ty) in let rec pattern_to_string (n : pattern) : string list = match n with -- cgit v1.2.3 From 5b9f8de676829817d2b776166fda66bfb5128d6c Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 24 Nov 2023 17:10:05 +0100 Subject: Improve the error messages for some name collisions --- compiler/ExtractBase.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'compiler') diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index c6158847..dffe1ea3 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -634,11 +634,13 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = | TypeId id -> "type name: " ^ type_id_to_string ctx id | StructId id -> "struct constructor of: " ^ type_id_to_string ctx id | VariantId (id, variant_id) -> + let type_name = type_id_to_string ctx id in let variant_name = adt_variant_to_string ctx id (Some variant_id) in - "variant name: " ^ variant_name + "type name: " ^ type_name ^ ", variant name: " ^ variant_name | FieldId (id, field_id) -> + let type_name = type_id_to_string ctx id in let field_name = adt_field_to_string ctx id field_id in - "field name: " ^ field_name + "type name: " ^ type_name ^ ", field name: " ^ field_name | UnknownId -> "keyword" | TypeVarId id -> "type_var_id: " ^ TypeVarId.to_string id | ConstGenericVarId id -> -- cgit v1.2.3 From feb10e653131716698205f0b77b9623cdd1712b0 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 24 Nov 2023 17:22:33 +0100 Subject: Update some assumed type names/variants --- compiler/Extract.ml | 7 +---- compiler/ExtractBase.ml | 68 +++++++++++++++++++++++++++++-------------------- 2 files changed, 41 insertions(+), 34 deletions(-) (limited to 'compiler') diff --git a/compiler/Extract.ml b/compiler/Extract.ml index c8c16c08..a4319482 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -173,12 +173,7 @@ let extract_adt_g_value *) let cons = match variant_id with - | Some vid -> ( - (* In the case of Lean, we might have to add the type name as a prefix *) - match (!backend, adt_id) with - | Lean, TAssumed _ -> - ctx_get_type adt_id ctx ^ "." ^ ctx_get_variant adt_id vid ctx - | _ -> ctx_get_variant adt_id vid ctx) + | Some vid -> ctx_get_variant adt_id vid ctx | None -> ctx_get_struct adt_id ctx in let use_parentheses = inside && field_values <> [] in diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index dffe1ea3..b7fa7788 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -960,31 +960,40 @@ let keywords () = List.concat [ named_unops; named_binops; misc ] let assumed_adts () : (assumed_ty * string) list = - match !backend with - | Lean -> - [ - (TState, "State"); - (TResult, "Result"); - (TError, "Error"); - (TFuel, "Nat"); - (TArray, "Array"); - (TSlice, "Slice"); - (TStr, "Str"); - (TRawPtr Mut, "MutRawPtr"); - (TRawPtr Const, "ConstRawPtr"); - ] - | Coq | FStar | HOL4 -> - [ - (TState, "state"); - (TResult, "result"); - (TError, "error"); - (TFuel, if !backend = HOL4 then "num" else "nat"); - (TArray, "array"); - (TSlice, "slice"); - (TStr, "str"); - (TRawPtr Mut, "mut_raw_ptr"); - (TRawPtr Const, "const_raw_ptr"); - ] + let state = + if !use_state then + match !backend with + | Lean -> [ (TState, "State") ] + | Coq | FStar | HOL4 -> [ (TState, "state") ] + else [] + in + (* We voluntarily omit the type [Error]: it is never directly + referenced in the generated translation, and easily collides + with user-defined types *) + let adts = + match !backend with + | Lean -> + [ + (TResult, "Result"); + (TFuel, "Nat"); + (TArray, "Array"); + (TSlice, "Slice"); + (TStr, "Str"); + (TRawPtr Mut, "MutRawPtr"); + (TRawPtr Const, "ConstRawPtr"); + ] + | Coq | FStar | HOL4 -> + [ + (TResult, "result"); + (TFuel, if !backend = HOL4 then "num" else "nat"); + (TArray, "array"); + (TSlice, "slice"); + (TStr, "str"); + (TRawPtr Mut, "mut_raw_ptr"); + (TRawPtr Const, "const_raw_ptr"); + ] + in + state @ adts let assumed_struct_constructors () : (assumed_ty * string) list = match !backend with @@ -1015,9 +1024,12 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list = ] | Lean -> [ - (TResult, result_return_id, "ret"); - (TResult, result_fail_id, "fail"); - (TError, error_failure_id, "panic"); + (TResult, result_return_id, "Result.ret"); + (TResult, result_fail_id, "Result.fail"); + (* For panic: we omit the prefix "Error." because the type is always + clear from the context. Also, "Error" is often used by user-defined + types (when we omit the crate as a prefix). *) + (TError, error_failure_id, ".panic"); (* No Fuel::Zero on purpose *) (* No Fuel::Succ on purpose *) ] -- cgit v1.2.3 From 4d5d2a8628cfb002267be9a13982aa4ef24a2651 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 24 Nov 2023 17:29:08 +0100 Subject: Make a minor fix --- compiler/Extract.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'compiler') diff --git a/compiler/Extract.ml b/compiler/Extract.ml index a4319482..e48e6ae6 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -2718,7 +2718,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt "=="; F.pp_print_space fmt (); let success = ctx_get_variant (TAssumed TResult) result_return_id ctx in - F.pp_print_string fmt ("." ^ success ^ " ())") + F.pp_print_string fmt (success ^ " ())") | HOL4 -> F.pp_print_string fmt "val _ = assert_return ("; F.pp_print_string fmt "“"; -- cgit v1.2.3 From 3fb8105afe1d43beb326906f124d7e0e7cefe7bc Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 24 Nov 2023 17:30:56 +0100 Subject: Update a comment --- compiler/ExtractBase.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'compiler') diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index b7fa7788..43e7f158 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1419,9 +1419,10 @@ let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option) - we add "_fwd" - [rg] is [None]: this is a backward function: - this function has one extracted backward function: - - if the forward function has been filtered, we add "_fwd_back": + - if the forward function has been filtered, we add nothing: the forward function is useless, so the unique backward function - takes its place, in a way + takes its place, in a way (in effect, we "merge" the forward + and the backward functions). - otherwise we add "_back" - this function has several backward functions: we add "_back" and an additional suffix to identify the precise backward function -- cgit v1.2.3 From 1c8187d7f4129e09f23d3b5caf33938a0c91ea77 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 24 Nov 2023 17:38:44 +0100 Subject: Add the alloc::string::String type in the builtins --- compiler/ExtractBase.ml | 5 +++-- compiler/ExtractBuiltin.ml | 15 ++++++++++++--- compiler/ExtractName.ml | 1 + 3 files changed, 16 insertions(+), 5 deletions(-) (limited to 'compiler') diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 43e7f158..1ca68120 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1109,8 +1109,9 @@ let initialize_names_maps () : names_maps = let init = names_map_init () in let int_names = List.map int_name T.all_int_types in let keywords = - List.concat - [ [ bool_name (); char_name (); str_name () ]; int_names; init.keywords ] + (* Remark: we don't put "str_name()" below because it clashes with + "alloc::string::String", which we register elsewhere. *) + List.concat [ [ bool_name (); char_name () ]; int_names; init.keywords ] in let names_set = StringSet.empty in let name_to_id = StringMap.empty in diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 30ec7c19..24d16dca 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -127,9 +127,15 @@ let mk_struct_constructor (type_name : string) : string = a type parameter for the allocator to use, which we want to filter. *) let builtin_types () : builtin_type_info list = - let mk_type (rust_name : string) ?(keep_params : bool list option = None) + let mk_type (rust_name : string) ?(custom_name : string option = None) + ?(keep_params : bool list option = None) ?(kind : type_variant_kind = KOpaque) () : builtin_type_info = - let extract_name = flatten_name (split_on_separator rust_name) in + let rust_name = parse_pattern rust_name in + let extract_name = + match custom_name with + | None -> flatten_name (pattern_to_type_extract_name rust_name) + | Some name -> flatten_name (split_on_separator name) + in let body_info : builtin_type_body_info option = match kind with | KOpaque -> None @@ -147,13 +153,16 @@ let builtin_types () : builtin_type_info list = Some (Struct (constructor, fields)) | KEnum -> raise (Failure "TODO") in - let rust_name = parse_pattern rust_name in { rust_name; extract_name; keep_params; body_info } in [ (* Alloc *) mk_type "alloc::alloc::Global" (); + (* String *) + mk_type "alloc::string::String" + ~custom_name:(Some (backend_choice "string" "String")) + (); (* Vec *) mk_type "alloc::vec::Vec" ~keep_params:(Some [ true; false ]) (); (* Range *) diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml index c0a23080..a916bffb 100644 --- a/compiler/ExtractName.ml +++ b/compiler/ExtractName.ml @@ -76,6 +76,7 @@ let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) : in pattern_to_string name +let pattern_to_type_extract_name = pattern_to_extract_name false let pattern_to_fun_extract_name = pattern_to_extract_name false let pattern_to_trait_impl_extract_name = pattern_to_extract_name true -- cgit v1.2.3 From 959d6fce38c8d8ca6eaed3ad6f458b87f91a9abc Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 27 Nov 2023 09:37:31 +0100 Subject: Update the generation of files for external definitions and regenerate the tests --- compiler/Translate.ml | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) (limited to 'compiler') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 05e48af5..31cb4b32 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -977,7 +977,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) | FStar -> () | Lean -> if fi.in_namespace then Printf.fprintf out "end %s\n" fi.namespace | HOL4 -> Printf.fprintf out "val _ = export_theory ()\n" - | Coq -> Printf.fprintf out "End %s .\n" fi.module_name); + | Coq -> Printf.fprintf out "End %s.\n" fi.module_name); (* Some logging *) log#linfo (lazy ("Generated: " ^ fi.filename)); @@ -1320,13 +1320,20 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : (* 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 *) + (* For F*, we generate an .fsti, and let the user write the .fst. + For the other backends, we generate a template file as a model + for the file the user has to provide. *) let module_suffix, opaque_imported_suffix, custom_msg = match !Config.backend with - | FStar | Coq | HOL4 -> - ("Opaque", "Opaque", ": external function declarations") - | Lean -> - ( "FunsExternal_Template", + | FStar -> + ( "FunsExternal", + "FunsExternal", + ": external function declarations" ) + | HOL4 | Coq | Lean -> + ( (* The name of the file we generate *) + "FunsExternal_Template", + (* The name of the file that will be imported by the Funs + module, and that the user has to provide. *) "FunsExternal", ": external functions.\n\ -- This is a template file: rename it to \ @@ -1337,9 +1344,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : in let opaque_module = crate_name ^ module_delimiter ^ module_suffix in let opaque_imported_module = - if !Config.backend = Lean then - crate_name ^ module_delimiter ^ opaque_imported_suffix - else opaque_module + crate_name ^ module_delimiter ^ opaque_imported_suffix in let opaque_config = { -- cgit v1.2.3 From bef2bd34fcb0817f1b7d16b95122bcc3c6f05c72 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 27 Nov 2023 10:29:25 +0100 Subject: Generate a dedicated file for the external types --- compiler/Translate.ml | 114 ++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 102 insertions(+), 12 deletions(-) (limited to 'compiler') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 31cb4b32..cc84b9fb 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -481,9 +481,19 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) defs in + let dont_extract (d : Pure.type_decl) : bool = + match d.kind with + | Enum _ | Struct _ -> not config.extract_transparent + | Opaque -> not config.extract_opaque + in + if List.exists (fun b -> b) builtin then (* Sanity check *) assert (List.for_all (fun b -> b) builtin) + else if List.exists dont_extract defs then + (* Check if we have to ignore declarations *) + (* Sanity check *) + assert (List.for_all dont_extract defs) else ( (* Extract the type declarations. @@ -873,6 +883,7 @@ type extract_file_info = { filename : string; namespace : string; in_namespace : bool; + open_namespace : bool; crate_name : string; rust_module_name : string; module_name : string; @@ -931,8 +942,22 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) (* Add the custom includes *) List.iter (fun m -> - Printf.fprintf out "Require Export %s.\n" m; - Printf.fprintf out "Import %s.\n" m) + (* TODO: I don't really understand how the "Require Export", + "Require Import", "Include" work. + I used to have: + {[ + Require Export %s. + Import %s. + ]} + + I now have: + {[ + Require Import %s. + Include %s. + ]} + *) + Printf.fprintf out "Require Import %s.\n" m; + Printf.fprintf out "Include %s.\n" m) fi.custom_includes; Printf.fprintf out "Module %s.\n" fi.module_name | Lean -> @@ -943,9 +968,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) List.iter (fun m -> Printf.fprintf out "import %s\n" m) fi.custom_includes; (* Always open the Primitives namespace *) Printf.fprintf out "open Primitives\n"; - (* If we are inside the namespace: declare it, otherwise: open it *) - if fi.in_namespace then Printf.fprintf out "\nnamespace %s\n" fi.namespace - else Printf.fprintf out "open %s\n" fi.namespace + (* If we are inside the namespace: declare it *) + if fi.in_namespace then Printf.fprintf out "\nnamespace %s\n" fi.namespace; + (* We might need to open the namespace *) + if fi.open_namespace then Printf.fprintf out "open %s\n" fi.namespace | HOL4 -> Printf.fprintf out "open primitivesLib divDefLib\n"; (* Add the custom imports and includes *) @@ -1250,12 +1276,72 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : in let has_opaque_types = has_opaque_types || !Config.use_state in - (* Extract the types *) + (* + * Extract the types + *) (* If there are opaque types, we extract in an interface *) - (* TODO: for Lean and Coq: generate a template file *) + (* Extract the opaque type declarations, if needed *) + let opaque_types_module = + if has_opaque_types then ( + (* For F*, we generate an .fsti, and let the user write the .fst. + For the other backends, we generate a template file as a model + for the file the user has to provide. *) + let module_suffix, opaque_imported_suffix, custom_msg = + match !Config.backend with + | FStar -> + ("TypesExternal", "TypesExternal", ": external type declarations") + | HOL4 | Coq | Lean -> + ( (* The name of the file we generate *) + "TypesExternal_Template", + (* The name of the file that will be imported by the Types + module, and that the user has to provide. *) + "TypesExternal", + ": external types.\n\ + -- This is a template file: rename it to \ + \"TypesExternal.lean\" and fill the holes." ) + in + let opaque_filename = + extract_filebasename ^ file_delimiter ^ module_suffix ^ opaque_ext + in + let opaque_module = crate_name ^ module_delimiter ^ module_suffix in + let opaque_imported_module = + crate_name ^ module_delimiter ^ opaque_imported_suffix + in + let opaque_config = + { + base_gen_config with + extract_opaque = true; + extract_transparent = false; + extract_types = true; + extract_trait_decls = true; + extract_state_type = !Config.use_state; + interface = true; + } + in + let file_info = + { + filename = opaque_filename; + namespace; + in_namespace = false; + open_namespace = false; + crate_name; + rust_module_name = crate.name; + module_name = opaque_module; + custom_msg; + custom_imports = []; + custom_includes = []; + } + in + extract_file opaque_config ctx file_info; + (* Return the additional dependencies *) + [ opaque_imported_module ]) + else [] + in + + (* Extract the non opaque types *) let types_filename_ext = match !Config.backend with - | FStar -> if has_opaque_types then ".fsti" else ".fst" + | FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean" | HOL4 -> "Script.sml" @@ -1269,8 +1355,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : base_gen_config with extract_types = true; extract_trait_decls = true; - extract_opaque = true; - extract_state_type = !Config.use_state; + extract_opaque = false; interface = has_opaque_types; } in @@ -1279,12 +1364,13 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : filename = types_filename; namespace; in_namespace = true; + open_namespace = false; crate_name; rust_module_name = crate.name; module_name = types_module; custom_msg = ": type definitions"; custom_imports = []; - custom_includes = []; + custom_includes = opaque_types_module; } in extract_file types_config ctx file_info; @@ -1307,6 +1393,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : filename = template_clauses_filename; namespace; in_namespace = true; + open_namespace = false; crate_name; rust_module_name = crate.name; module_name = template_clauses_module; @@ -1317,7 +1404,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : in extract_file template_clauses_config ctx file_info); - (* Extract the opaque declarations, if needed *) + (* Extract the opaque fun declarations, if needed *) let opaque_funs_module = if has_opaque_funs then ( (* For F*, we generate an .fsti, and let the user write the .fst. @@ -1362,6 +1449,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : filename = opaque_filename; namespace; in_namespace = false; + open_namespace = true; crate_name; rust_module_name = crate.name; module_name = opaque_module; @@ -1401,6 +1489,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : filename = fun_filename; namespace; in_namespace = true; + open_namespace = false; crate_name; rust_module_name = crate.name; module_name = fun_module; @@ -1434,6 +1523,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : filename = extract_filebasename ^ ext; namespace; in_namespace = true; + open_namespace = false; crate_name; rust_module_name = crate.name; module_name = crate_name; -- cgit v1.2.3 From fdb8555cf6bc21ea230141373920196b078bdd28 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 27 Nov 2023 13:48:46 +0100 Subject: Do not activate the sanity (invariant) checks by default --- compiler/Config.ml | 8 ++++---- compiler/InterpreterBorrows.ml | 4 ++-- compiler/InterpreterLoopsJoinCtxs.ml | 2 +- compiler/InterpreterLoopsMatchCtxs.ml | 2 +- compiler/InterpreterPaths.ml | 2 +- compiler/Invariants.ml | 2 +- compiler/Main.ml | 8 ++++---- 7 files changed, 14 insertions(+), 14 deletions(-) (limited to 'compiler') diff --git a/compiler/Config.ml b/compiler/Config.ml index fe110ee4..48ee0a06 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -35,11 +35,11 @@ let backend = ref FStar (** {1 Interpreter} *) -(** Check that invariants are maintained whenever we execute a statement - - TODO: rename to sanity_checks. +(** Activate the sanity checks, and in particular the invariant checks + that are performed at every evaluation step. This is very expensive + (~100x slow down) but very efficient to catch mistakes early. *) -let check_invariants = ref true +let sanity_checks = ref false (** Expand all symbolic values containing borrows upon introduction - allows to use restrict ourselves to a simpler model for the projectors over diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index 8c9c0e72..2f793f4a 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -2155,7 +2155,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) ^ "\n\n- abs1:\n" ^ abs_to_string ctx abs1)); (* Check that the abstractions are destructured *) - if !Config.check_invariants then ( + if !Config.sanity_checks then ( let destructure_shared_values = true in assert (abs_is_destructured destructure_shared_values ctx abs0); assert (abs_is_destructured destructure_shared_values ctx abs1)); @@ -2487,7 +2487,7 @@ let merge_into_abstraction_aux (abs_kind : abs_kind) (can_end : bool) in (* Sanity check *) - if !Config.check_invariants then assert (abs_is_destructured true ctx abs); + if !Config.sanity_checks then assert (abs_is_destructured true ctx abs); (* Return *) abs diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml index 4cc74aae..8d485483 100644 --- a/compiler/InterpreterLoopsJoinCtxs.ml +++ b/compiler/InterpreterLoopsJoinCtxs.ml @@ -714,7 +714,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (loop_id : LoopId.id) ^ eval_ctx_to_string !joined_ctx)); (* Sanity check *) - if !Config.check_invariants then Invariants.check_invariants !joined_ctx; + if !Config.sanity_checks then Invariants.check_invariants !joined_ctx; (* Return *) ctx1 in diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 74f9ba2c..bf459e41 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -1580,7 +1580,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id) ^ eval_ctx_to_string tgt_ctx)); (* Sanity check *) - if !Config.check_invariants then + if !Config.sanity_checks then Invariants.check_borrowed_values_invariant tgt_ctx; (* End all the borrows which appear in the *new* abstractions *) diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml index 729a3577..999b8ab0 100644 --- a/compiler/InterpreterPaths.ml +++ b/compiler/InterpreterPaths.ml @@ -311,7 +311,7 @@ let try_read_place (access : access_kind) (p : place) (ctx : eval_ctx) : (* Note that we ignore the new environment: it should be the same as the original one. *) - if !Config.check_invariants then + if !Config.sanity_checks then if ctx1 <> ctx then ( let msg = "Unexpected environment update:\nNew environment:\n" diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index e0e3f354..fa0d7436 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -804,7 +804,7 @@ let check_symbolic_values (ctx : eval_ctx) : unit = M.iter check_info !infos let check_invariants (ctx : eval_ctx) : unit = - if !Config.check_invariants then ( + if !Config.sanity_checks then ( log#ldebug (lazy ("Checking invariants:\n" ^ eval_ctx_to_string ctx)); check_loans_borrows_relation_invariant ctx; check_borrowed_values_invariant ctx; diff --git a/compiler/Main.ml b/compiler/Main.ml index e350da8a..7f98f581 100644 --- a/compiler/Main.ml +++ b/compiler/Main.ml @@ -107,10 +107,10 @@ let () = Arg.Set split_files, " Split the definitions between different files for types, functions, \ etc." ); - ( "-no-check-inv", - Arg.Clear check_invariants, - " Deactivate the invariant sanity checks performed at every evaluation \ - step. Dramatically increases speed." ); + ( "-checks", + Arg.Set sanity_checks, + " Activate extensive sanity checks (warning: causes a ~100 times slow \ + down)." ); ( "-no-gen-lib-entry", Arg.Clear generate_lib_entry_point, " Do not generate the entry point file for the generated library (only \ -- cgit v1.2.3 From a17eef1053909117d75c9ea8eeaad786626cc05d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 27 Nov 2023 14:15:01 +0100 Subject: Update the way the Primitives file is copied --- compiler/Translate.ml | 33 ++++++++++++++++++++------------- 1 file changed, 20 insertions(+), 13 deletions(-) (limited to 'compiler') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index cc84b9fb..37f58140 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -1206,20 +1206,27 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : match primitives_src_dest with | None -> () | Some (primitives_src, primitives_destname) -> ( - let src = open_in (exe_dir ^ primitives_src) in - let tgt_filename = Filename.concat dest_dir primitives_destname in - let tgt = open_out tgt_filename in - (* Very annoying: I couldn't find a "cp" function in the OCaml libraries... *) try - while true do - (* We copy line by line *) - let line = input_line src in - Printf.fprintf tgt "%s\n" line - done - with End_of_file -> - close_in src; - close_out tgt; - log#linfo (lazy ("Copied: " ^ tgt_filename))) + (* TODO: stop copying the primitives file *) + let src = open_in (exe_dir ^ primitives_src) in + let tgt_filename = Filename.concat dest_dir primitives_destname in + let tgt = open_out tgt_filename in + (* Very annoying: I couldn't find a "cp" function in the OCaml libraries... *) + try + while true do + (* We copy line by line *) + let line = input_line src in + Printf.fprintf tgt "%s\n" line + done + with End_of_file -> + close_in src; + close_out tgt; + log#linfo (lazy ("Copied: " ^ tgt_filename)) + with Sys_error _ -> + log#error + "Could not copy the primitives file: %s.\n\ + You will have to copy it/set up the project by hand." + primitives_src) in (* Extract the file(s) *) -- cgit v1.2.3 From 8a6c26355ef82de725ed643f4a3c40ed54d1b4c7 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 27 Nov 2023 14:19:12 +0100 Subject: Update a comment --- compiler/Config.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'compiler') diff --git a/compiler/Config.ml b/compiler/Config.ml index 48ee0a06..1a00656d 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -52,7 +52,8 @@ let greedy_expand_symbolics_with_borrows = true (** Experimental. - TODO: remove (always true now) + TODO: remove (always true now), but check that when we panic/call a function + there is no bottom below a borrow. We sometimes want to temporarily break the invariant that there is no bottom value below a borrow. If this value is true, we don't check -- cgit v1.2.3 From 6f8f1213e056804eda4c521922cdf45f4e92a509 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 27 Nov 2023 15:57:55 +0100 Subject: Fix the issues with the cross-references for OCaml doc --- compiler/Config.ml | 2 +- compiler/Contexts.ml | 8 ++++---- compiler/ExtractBase.ml | 6 +++--- compiler/ExtractTypes.ml | 2 +- compiler/InterpreterBorrowsCore.ml | 12 ++++++------ compiler/InterpreterExpansion.mli | 2 +- compiler/InterpreterLoopsCore.ml | 8 ++++---- compiler/InterpreterLoopsMatchCtxs.mli | 6 +++--- compiler/InterpreterProjectors.mli | 2 +- compiler/InterpreterStatements.mli | 2 +- compiler/InterpreterUtils.ml | 4 ++-- compiler/Pure.ml | 4 ++-- compiler/PureUtils.ml | 2 +- compiler/Substitute.ml | 2 +- compiler/SymbolicAst.ml | 4 ++-- compiler/TypesUtils.ml | 4 ++-- 16 files changed, 35 insertions(+), 35 deletions(-) (limited to 'compiler') diff --git a/compiler/Config.ml b/compiler/Config.ml index 1a00656d..364ef748 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -289,7 +289,7 @@ let unfold_monadic_let_bindings = ref false we later filter the useless *forward* calls in the micro-passes, where it is more natural to do. - See the comments for {!val:PureMicroPasses.expression_contains_child_call_in_all_paths} + See the comments for {!PureMicroPasses.expression_contains_child_call_in_all_paths} for additional explanations. *) let filter_useless_monadic_calls = ref true diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml index a2ae4f16..c93bb213 100644 --- a/compiler/Contexts.ml +++ b/compiler/Contexts.ml @@ -112,7 +112,7 @@ let reset_global_counters () = fun_call_id_counter := FunCallId.generator_zero; dummy_var_id_counter := DummyVarId.generator_zero -(** Ancestor for {!env} iter visitor *) +(** Ancestor for {!type:env} iter visitor *) class ['self] iter_env_base = object (_self : 'self) inherit [_] iter_abs @@ -120,7 +120,7 @@ class ['self] iter_env_base = method visit_dummy_var_id : 'env -> dummy_var_id -> unit = fun _ _ -> () end -(** Ancestor for {!env} map visitor *) +(** Ancestor for {!type:env} map visitor *) class ['self] map_env_base = object (_self : 'self) inherit [_] map_abs @@ -423,11 +423,11 @@ let erase_regions (ty : ty) : ty = in v#visit_ty () ty -(** Push an uninitialized variable (which thus maps to {!constructor:Values.value.Bottom}) *) +(** Push an uninitialized variable (which thus maps to {!constructor:Values.value.VBottom}) *) let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx = ctx_push_var ctx var (mk_bottom (erase_regions var.var_ty)) -(** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.Bottom}) *) +(** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.VBottom}) *) let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx = let vars = List.map (fun v -> (v, mk_bottom (erase_regions v.var_ty))) vars in ctx_push_vars ctx vars diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 1ca68120..85ab1112 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -311,7 +311,7 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string) the same name because Lean uses the typing information to resolve the ambiguities. - This map complements the {!names_map}, which checks for collisions. + This map complements the {!type:names_map}, which checks for collisions. *) type unsafe_names_map = { id_to_name : string IdMap.t } @@ -1639,7 +1639,7 @@ let ctx_compute_trait_type_clause_name (ctx : extraction_ctx) function is an assumed function or a local function - function basename - the number of loops in the parent function. This is used for - the same purpose as in {!field:llbc_name}. + the same purpose as in [llbc_name]. - loop identifier, if this is for a loop *) let ctx_compute_termination_measure_name (ctx : extraction_ctx) @@ -1668,7 +1668,7 @@ let ctx_compute_termination_measure_name (ctx : extraction_ctx) function is an assumed function or a local function - function basename - the number of loops in the parent function. This is used for - the same purpose as in {!field:llbc_name}. + the same purpose as in [llbc_name]. - loop identifier, if this is for a loop *) let ctx_compute_decreases_proof_name (ctx : extraction_ctx) diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index c6212d31..ca9984be 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -213,7 +213,7 @@ let is_empty_record_type_decl_group (dg : Pure.type_decl list) : bool = - in Lean, groups of mutually recursive definitions must end with "end" - in HOL4 (in most situations) the whole group must be within a `Define` command - Calls to {!extract_fun_decl} should be inserted between calls to + Calls to {!Extract.extract_fun_decl} should be inserted between calls to {!start_fun_decl_group} and {!end_fun_decl_group}. TODO: maybe those [{start/end}_decl_group] functions are not that much a good diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml index b13d545c..44f85d0a 100644 --- a/compiler/InterpreterBorrowsCore.ml +++ b/compiler/InterpreterBorrowsCore.ml @@ -924,7 +924,7 @@ let remove_intersecting_aproj_borrows_shared (regions : RegionId.Set.t) [subst]: takes as parameters the abstraction in which we perform the substitution and the list of given back values at the projector of - loans where we perform the substitution (see the fields in {!AProjLoans}). + loans where we perform the substitution (see the fields in {!Values.AProjLoans}). Note that the symbolic value at this place is necessarily equal to [sv], which is why we don't give it as parameters. *) @@ -970,13 +970,13 @@ let update_intersecting_aproj_loans (proj_regions : RegionId.Set.t) (* Return *) ctx -(** Helper function: lookup an {!AProjLoans} by using an abstraction id and a +(** Helper function: lookup an {!constructor:Values.aproj.AProjLoans} by using an abstraction id and a symbolic value. - + We return the information from the looked up projector of loans. See the - fields in {!AProjLoans} (we don't return the symbolic value, because it + fields in {!constructor:Values.aproj.AProjLoans} (we don't return the symbolic value, because it is equal to [sv]). - + Sanity check: we check that there is exactly one projector which corresponds to the couple (abstraction id, symbolic value). *) @@ -1115,7 +1115,7 @@ let update_aproj_borrows (abs_id : AbstractionId.id) (sv : symbolic_value) (** Helper function: might break invariants. - Converts an {!AProjLoans} to an {!AEndedProjLoans}. The projector is identified + Converts an {!Values.aproj.AProjLoans} to an {!Values.aproj.AEndedProjLoans}. The projector is identified by a symbolic value and an abstraction id. *) let update_aproj_loans_to_ended (abs_id : AbstractionId.id) diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli index 4be1fd24..b545f979 100644 --- a/compiler/InterpreterExpansion.mli +++ b/compiler/InterpreterExpansion.mli @@ -79,6 +79,6 @@ val expand_symbolic_int : m_fun (** If this mode is activated through the [config], greedily expand the symbolic - values which need to be expanded. See {!type:config} for more information. + values which need to be expanded. See {!type:Contexts.config} for more information. *) val greedy_expand_symbolic_values : config -> cm_fun diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index d14230c6..ca1f8f31 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -41,10 +41,10 @@ type abs_borrows_loans_maps = { borrow_loan_to_abs : AbstractionId.Set.t BorrowId.Map.t; } -(** See {!InterpreterLoopsMatchCtxs.MakeMatcher} and {!InterpreterLoopsCore.Matcher}. +(** See {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} and [Matcher]. This module contains primitive match functions to instantiate the generic - {!InterpreterLoopsMatchCtxs.MakeMatcher} functor. + {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} functor. *) module type PrimMatcher = sig val match_etys : ety -> ety -> ety @@ -231,8 +231,8 @@ module type Matcher = sig eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue end -(** See {!InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and - {!InterpreterLoopsCore.CheckEquivMatcher}. +(** See {!module:InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and + {!module-type:InterpreterLoopsCore.CheckEquivMatcher}. Very annoying: functors only take modules as inputs... *) diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli index bf29af79..5f69b8d3 100644 --- a/compiler/InterpreterLoopsMatchCtxs.mli +++ b/compiler/InterpreterLoopsMatchCtxs.mli @@ -27,13 +27,13 @@ val compute_abs_borrows_loans_maps : We use it for joins, to check if two environments are convertible, etc. See for instance {!MakeJoinMatcher} and {!MakeCheckEquivMatcher}. - The functor is parameterized by a {!PrimMatcher}, which implements the - non-generic part of the match. More precisely, the role of {!PrimMatcher} is two + The functor is parameterized by a {!module-type:InterpreterLoopsCore.PrimMatcher}, which implements the + non-generic part of the match. More precisely, the role of {!module-type:InterpreterLoopsCore.PrimMatcher} is two provide generic functions which recursively match two values (by recursively matching the fields of ADT values for instance). When it does need to match values in a non-trivial manner (if two ADT values don't have the same variant for instance) it calls the corresponding specialized function from - {!PrimMatcher}. + {!module-type:InterpreterLoopsCore.PrimMatcher}. *) module MakeMatcher : functor (_ : PrimMatcher) -> Matcher diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli index 583c6907..9e4ebc20 100644 --- a/compiler/InterpreterProjectors.mli +++ b/compiler/InterpreterProjectors.mli @@ -6,7 +6,7 @@ open Contexts Apply a proj_borrows on a shared borrow. Note that when projecting over shared values, we generate - {!type:abstract_shared_borrows}, not {!type:avalue}s. + {!type:Aeneas.Values.abstract_shared_borrows}, not {!type:Aeneas.Values.avalue}s. Parameters: [regions] diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli index d84e8be6..3832d02f 100644 --- a/compiler/InterpreterStatements.mli +++ b/compiler/InterpreterStatements.mli @@ -10,7 +10,7 @@ open Cps dummy variables, after ending the proper borrows of course) but the return variable, move the return value out of the return variable, remove all the local variables (but preserve the abstractions!), remove the - {!constructor:env_elem.Frame} indicator delimiting the current frame and + {!constructor:Contexts.env_elem.EFrame} indicator delimiting the current frame and handle the return value to the continuation. If the boolean is false, we don't move the return value, and call the diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index ecd8f53f..bba88e9f 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -111,7 +111,7 @@ let mk_typed_value_from_symbolic_value (svalue : symbolic_value) : typed_value = (** Create a loans projector value from a symbolic value. Checks if the projector will actually project some regions. If not, - returns {!AIgnored} ([_]). + returns {!Values.AIgnored} ([_]). TODO: update to handle 'static *) @@ -238,7 +238,7 @@ let symbolic_value_has_ended_regions (ended_regions : RegionId.Set.t) let regions = ty_regions s.sv_ty in not (RegionId.Set.disjoint regions ended_regions) -(** Check if a {!type:value} contains [⊥]. +(** Check if a {!type:Values.value} contains [⊥]. Note that this function is very general: it also checks wether symbolic values contain already ended regions. diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 50849df9..0ae83007 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -273,7 +273,7 @@ class virtual ['self] mapreduce_ty_base = type ty = | TAdt of type_id * generic_args - (** {!Adt} encodes ADTs and tuples and assumed types. + (** {!TAdt} encodes ADTs and tuples and assumed types. TODO: what about the ended regions? (ADTs may be parameterized with several region variables. When giving back an ADT value, we may @@ -1064,7 +1064,7 @@ type trait_impl = { meta : meta; impl_trait : trait_decl_ref; llbc_impl_trait : Types.trait_decl_ref; - (** Same remark as for {llbc_generics}. *) + (** Same remark as for {!field:llbc_generics}. *) generics : generic_params; llbc_generics : Types.generic_params; (** We use the LLBC generics to generate "pretty" names, for instance diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 6b0deb73..a5143f3c 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -195,7 +195,7 @@ let fun_sig_substitute (subst : subst) (sg : fun_sig) : inst_fun_sig = We only look for outer monadic let-bindings. This is used when printing the branches of [if ... then ... else ...]. - Rem.: this function will *fail* if there are {!constructor:Aeneas.Pure.expression.Loop} + Rem.: this function will *fail* if there are {!Pure.Loop} nodes (you should call it on an expression where those nodes have been eliminated). *) let rec let_group_requires_parentheses (e : texpression) : bool = diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml index 73e7f71d..a05b2c5a 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -76,7 +76,7 @@ let erase_regions_subst : subst = tr_self = Self; } -(** Convert an {!rty} to an {!ety} by erasing the region variables *) +(** Erase the region variables in a type *) let erase_regions (ty : ty) : ty = ty_substitute erase_regions_subst ty let trait_ref_erase_regions (tr : trait_ref) : trait_ref = diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index a9f45926..53f99b7f 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -66,8 +66,8 @@ type 'a region_group_id_map = 'a RegionGroupId.Map.t [@@deriving show] (** Ancestor for {!expression} iter visitor. - We could make it inherit the visitor for {!eval_ctx}, but in all the uses - of this visitor we don't need to explore {!eval_ctx}, so we make it inherit + We could make it inherit the visitor for {!Contexts.eval_ctx}, but in all the uses + of this visitor we don't need to explore {!Contexts.eval_ctx}, so we make it inherit the abstraction visitors instead. *) class ['self] iter_expression_base = diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml index 52e12b9a..76cc710a 100644 --- a/compiler/TypesUtils.ml +++ b/compiler/TypesUtils.ml @@ -5,7 +5,7 @@ include Charon.TypesUtils (** Retuns true if the type contains borrows. Note that we can't simply explore the type and look for regions: sometimes - we erase the lists of regions (by replacing them with [[]] when using {!Types.ety}, + we erase the lists of regions (by replacing them with [[]] when using {!type:Types.ty}, and when a type uses 'static this region doesn't appear in the region parameters. *) let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool = @@ -15,7 +15,7 @@ let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool = (** Retuns true if the type contains nested borrows. Note that we can't simply explore the type and look for regions: sometimes - we erase the lists of regions (by replacing them with [[]] when using {!Types.ety}, + we erase the lists of regions (by replacing them with [[]] when using {!type:Types.ty}, and when a type uses 'static this region doesn't appear in the region parameters. *) let ty_has_nested_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool = -- cgit v1.2.3