diff options
30 files changed, 145 insertions, 112 deletions
@@ -34,6 +34,10 @@ rust-tests/target/ # F* .depend *.hints +tests/betree/obj/ +tests/hashmap/obj/ +tests/hashmap_on_disk/obj/ +tests/misc/obj/ # Misc /fstar-tests @@ -3,7 +3,7 @@ ifeq (3.81,$(MAKE_VERSION)) install make, then invoke gmake instead of make) endif -all: build-test-verify +all: build-tests-verify CHARON_HOME = ../charon CHARON_EXEC = $(CHARON_HOME)/charon @@ -25,7 +25,7 @@ SUBDIR := # Build the project, test it and verify the generated files .PHONY: build-test-verify -build-test-verify: build test verify +build-tests-verify: build tests verify # Build the project .PHONY: build @@ -33,15 +33,15 @@ build: dune build src/main.exe # Test the project by translating test files to F* -.PHONY: test -test: build trans-no_nested_borrows trans-paper \ +.PHONY: tests +tests: build trans-no_nested_borrows trans-paper \ trans-hashmap trans-hashmap_main \ trans-external trans-constants \ - trans-nll-betree_nll trans-nll-betree_main + trans-polonius-betree_polonius trans-polonius-betree_main # Verify the F* files generated by the translation .PHONY: verify -verify: build test +verify: build tests cd tests && $(MAKE) all # Reformat the project @@ -60,8 +60,8 @@ trans-hashmap: SUBDIR:=hashmap trans-hashmap_main: TRANS_OPTIONS += -template-clauses trans-hashmap_main: SUBDIR:=hashmap_on_disk -trans-nll-betree_nll: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses -trans-nll-betree_nll: SUBDIR:=misc +trans-polonius-betree_polonius: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses +trans-polonius-betree_polonius: SUBDIR:=misc trans-constants: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses trans-constants: SUBDIR:=misc @@ -69,26 +69,31 @@ trans-constants: SUBDIR:=misc trans-external: TRANS_OPTIONS += trans-external: SUBDIR:=misc -trans-nll-betree_main: TRANS_OPTIONS += -template-clauses -trans-nll-betree_main: SUBDIR:=betree +trans-polonius-betree_main: TRANS_OPTIONS += -template-clauses +trans-polonius-betree_main: SUBDIR:=betree # Generic rules to extract the LLBC from a rust file # We use the rules in Charon's Makefile to generate the .llbc files: the options # vary with the test files. +.PHONY: gen-llbc-polonius-% +gen-llbc-polonius-%: build + cd $(CHARON_HOME)/tests-polonius && $(MAKE) test-$* + .PHONY: gen-llbc-% gen-llbc-%: build - cd $(CHARON_HOME) && $(MAKE) test-$* + cd $(CHARON_HOME)/tests && $(MAKE) test-$* # Generic rule to test the translation of an LLBC file. -# Note that the non-linear lifetime files are generated in the tests-nll subdirectory. +# Note that the files requiring the Polonius borrow-checker are generated +# in the tests-polonius subdirectory. .PHONY: trans-% trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc -trans-nll-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-nll/llbc +trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc -trans-%: gen-llbc-% +trans-polonius-%: gen-llbc-polonius-% dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) -trans-nll-%: gen-llbc-nll-% +trans-%: gen-llbc-% dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) .PHONY: doc @@ -78,7 +78,7 @@ 6. add `mvalue` (meta values) stored in abstractions when ending loans -8. The following doesn't work: +8. The following doesn't work (if we don't expand the symbolic values): ``` fn f1<'c, T>(p : (&'c mut T, &'c mut T)) -> (&'c mut T, &'c mut T) diff --git a/src/Collections.ml b/src/Collections.ml index 2cb298a7..351b6523 100644 --- a/src/Collections.ml +++ b/src/Collections.ml @@ -184,6 +184,7 @@ module type Set = sig val pp : Format.formatter -> t -> unit val show : t -> string + val pairwise_distinct : elt list -> bool end module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct @@ -218,6 +219,19 @@ module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct pp_string "}" let show s = to_string None s + + let pairwise_distinct ls = + let s = ref empty in + let rec check ls = + match ls with + | [] -> true + | x :: ls' -> + if mem x !s then false + else ( + s := add x !s; + check ls') + in + check ls end (** A map where the bindings are injective (i.e., if two keys are distinct, diff --git a/src/Contexts.ml b/src/Contexts.ml index 716326cf..07535e06 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -3,7 +3,6 @@ open Values open LlbcAst module V = Values open ValuesUtils -module M = Modules (** Some global counters. * @@ -210,7 +209,7 @@ let config_of_partial (mode : interpreter_mode) (config : partial_config) : } type type_context = { - type_decls_groups : M.type_declaration_group TypeDeclId.Map.t; + type_decls_groups : Crates.type_declaration_group TypeDeclId.Map.t; type_decls : type_decl TypeDeclId.Map.t; type_infos : TypesAnalysis.type_infos; } @@ -391,7 +390,7 @@ let ctx_lookup_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) : V.abs = let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool = let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in - match decl_group with M.Rec _ -> true | M.NonRec _ -> false + match decl_group with Crates.Rec _ -> true | Crates.NonRec _ -> false (** Visitor to iterate over the values in the *current* frame *) class ['self] iter_frame = diff --git a/src/Modules.ml b/src/Crates.ml index 7f372d09..844afb94 100644 --- a/src/Modules.ml +++ b/src/Crates.ml @@ -16,33 +16,33 @@ type declaration_group = | Global of GlobalDeclId.id [@@deriving show] -type llbc_module = { +type llbc_crate = { name : string; declarations : declaration_group list; types : type_decl list; functions : fun_decl list; globals : global_decl list; } -(** LLBC module - TODO: rename to crate *) +(** LLBC crate *) -let compute_defs_maps (m : llbc_module) : +let compute_defs_maps (c : llbc_crate) : type_decl TypeDeclId.Map.t * fun_decl FunDeclId.Map.t * global_decl GlobalDeclId.Map.t = let types_map = List.fold_left (fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m) - TypeDeclId.Map.empty m.types + TypeDeclId.Map.empty c.types in let funs_map = List.fold_left (fun m (def : fun_decl) -> FunDeclId.Map.add def.def_id def m) - FunDeclId.Map.empty m.functions + FunDeclId.Map.empty c.functions in let globals_map = List.fold_left (fun m (def : global_decl) -> GlobalDeclId.Map.add def.def_id def m) - GlobalDeclId.Map.empty m.globals + GlobalDeclId.Map.empty c.globals in (types_map, funs_map, globals_map) diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml index 615f45b3..248ad8b3 100644 --- a/src/FunsAnalysis.ml +++ b/src/FunsAnalysis.ml @@ -8,7 +8,7 @@ *) open LlbcAst -open Modules +open Crates module EU = ExpressionsUtils type fun_info = { @@ -26,7 +26,7 @@ type fun_info = { type modules_funs_info = fun_info FunDeclId.Map.t (** Various information about a module's functions *) -let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) +let analyze_module (m : llbc_crate) (funs_map : fun_decl FunDeclId.Map.t) (globals_map : global_decl GlobalDeclId.Map.t) (use_state : bool) : modules_funs_info = let infos = ref FunDeclId.Map.empty in diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 3a2939ef..9308fa16 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -7,18 +7,17 @@ open LlbcAstUtils module L = Logging module T = Types module A = LlbcAst -module M = Modules module SA = SymbolicAst (** The local logger *) let log = L.interpreter_log -let compute_type_fun_global_contexts (m : M.llbc_module) : +let compute_type_fun_global_contexts (m : Crates.llbc_crate) : C.type_context * C.fun_context * C.global_context = - let type_decls_list, _, _ = M.split_declarations m.declarations in - let type_decls, fun_decls, global_decls = M.compute_defs_maps m in + let type_decls_list, _, _ = Crates.split_declarations m.declarations in + let type_decls, fun_decls, global_decls = Crates.compute_defs_maps m in let type_decls_groups, _funs_defs_groups, _globals_defs_groups = - M.split_declarations_to_group_maps m.declarations + Crates.split_declarations_to_group_maps m.declarations in let type_infos = TypesAnalysis.analyze_type_declarations type_decls type_decls_list @@ -277,10 +276,10 @@ module Test = struct (** Test a unit function (taking no arguments) by evaluating it in an empty environment. *) - let test_unit_function (config : C.partial_config) (m : M.llbc_module) + let test_unit_function (config : C.partial_config) (crate : Crates.llbc_crate) (fid : A.FunDeclId.id) : unit = (* Retrieve the function declaration *) - let fdef = A.FunDeclId.nth m.functions fid in + let fdef = A.FunDeclId.nth crate.functions fid in let body = Option.get fdef.body in (* Debug *) @@ -294,7 +293,7 @@ module Test = struct (* Create the evaluation context *) let type_context, fun_context, global_context = - compute_type_fun_global_contexts m + compute_type_fun_global_contexts crate in let ctx = initialize_eval_context type_context fun_context global_context [] @@ -332,11 +331,11 @@ module Test = struct && List.length def.A.signature.inputs = 0 (** Test all the unit functions in a list of function definitions *) - let test_unit_functions (config : C.partial_config) (m : M.llbc_module) : unit - = - let unit_funs = List.filter fun_decl_is_transparent_unit m.functions in + let test_unit_functions (config : C.partial_config) + (crate : Crates.llbc_crate) : unit = + let unit_funs = List.filter fun_decl_is_transparent_unit crate.functions in let test_unit_fun (def : A.fun_decl) : unit = - test_unit_function config m def.A.def_id + test_unit_function config crate def.A.def_id in List.iter test_unit_fun unit_funs @@ -374,15 +373,17 @@ module Test = struct they are not supported by the symbolic interpreter. *) let test_functions_symbolic (config : C.partial_config) (synthesize : bool) - (m : M.llbc_module) : unit = + (crate : Crates.llbc_crate) : unit = (* Filter the functions which contain loops *) let no_loop_funs = - List.filter (fun f -> not (LlbcAstUtils.fun_decl_has_loops f)) m.functions + List.filter + (fun f -> not (LlbcAstUtils.fun_decl_has_loops f)) + crate.functions in (* Filter the opaque functions *) let no_loop_funs = List.filter fun_decl_is_transparent no_loop_funs in let type_context, fun_context, global_context = - compute_type_fun_global_contexts m + compute_type_fun_global_contexts crate in let test_fun (def : A.fun_decl) : unit = (* Execute the function - note that as the symbolic interpreter explores diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index edd27138..16ab9aad 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -771,6 +771,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) [end_borrows]: if false, we only end the outer loans we find. If true, we end all the loans and the borrows we find. + TODO: end_borrows is not necessary anymore. *) let prepare_lplace (config : C.config) (end_borrows : bool) (p : E.place) (cf : V.typed_value -> m_fun) : m_fun = diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 34310ea1..ae9e59fe 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -20,20 +20,32 @@ open InterpreterExpressions (** The local logger *) let log = L.statements_log -(** Drop a value at a given place *) +(** Drop a value at a given place - TODO: factorize this with [assign_to_place] *) let drop_value (config : C.config) (p : E.place) : cm_fun = fun cf ctx -> - log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p)); - (* Prepare the place (by ending the outer loans and the borrows). + log#ldebug + (lazy + ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Initial context:\n" + ^ eval_ctx_to_string ctx)); + (* Prepare the place (by ending the outer loans). * Note that [prepare_lplace] will use the `Write` access kind: * it is ok, because when updating the value with [Bottom] below, * we will use the `Move` access *) - let end_borrows = true in + let end_borrows = false in let prepare = prepare_lplace config end_borrows p in (* Replace the value with [Bottom] *) let replace cf (v : V.typed_value) ctx = + (* Move the value at destination (that we will overwrite) to a dummy variable + * to preserve the borrows *) + let mv = read_place_unwrap config Write p ctx in + let ctx = C.ctx_push_dummy_var ctx mv in + (* Update the destination to ⊥ *) let nv = { v with value = V.Bottom } in let ctx = write_place_unwrap config Move p nv ctx in + log#ldebug + (lazy + ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n" + ^ eval_ctx_to_string ctx)); cf ctx in (* Compose and apply *) diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml index 4e10c642..44abedf2 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -14,7 +14,6 @@ open OfJsonBasic module T = Types module V = Values module S = Scalars -module M = Modules module E = Expressions module A = LlbcAst module TU = TypesUtils @@ -680,24 +679,24 @@ let global_decl_of_json (js : json) (gid_conv : global_id_converter) : | _ -> Error "") let g_declaration_group_of_json (id_of_json : json -> ('id, string) result) - (js : json) : ('id M.g_declaration_group, string) result = + (js : json) : ('id Crates.g_declaration_group, string) result = combine_error_msgs js "g_declaration_group_of_json" (match js with | `Assoc [ ("NonRec", `List [ id ]) ] -> let* id = id_of_json id in - Ok (M.NonRec id) + Ok (Crates.NonRec id) | `Assoc [ ("Rec", `List [ ids ]) ] -> let* ids = list_of_json id_of_json ids in - Ok (M.Rec ids) + Ok (Crates.Rec ids) | _ -> Error "") let type_declaration_group_of_json (js : json) : - (M.type_declaration_group, string) result = + (Crates.type_declaration_group, string) result = combine_error_msgs js "type_declaration_group_of_json" (g_declaration_group_of_json T.TypeDeclId.id_of_json js) let fun_declaration_group_of_json (js : json) : - (M.fun_declaration_group, string) result = + (Crates.fun_declaration_group, string) result = combine_error_msgs js "fun_declaration_group_of_json" (g_declaration_group_of_json A.FunDeclId.id_of_json js) @@ -711,19 +710,19 @@ let global_declaration_group_of_json (js : json) : | `Assoc [ ("Rec", `List [ _ ]) ] -> Error "got mutually dependent globals" | _ -> Error "") -let declaration_group_of_json (js : json) : (M.declaration_group, string) result - = +let declaration_group_of_json (js : json) : + (Crates.declaration_group, string) result = combine_error_msgs js "declaration_of_json" (match js with | `Assoc [ ("Type", `List [ decl ]) ] -> let* decl = type_declaration_group_of_json decl in - Ok (M.Type decl) + Ok (Crates.Type decl) | `Assoc [ ("Fun", `List [ decl ]) ] -> let* decl = fun_declaration_group_of_json decl in - Ok (M.Fun decl) + Ok (Crates.Fun decl) | `Assoc [ ("Global", `List [ decl ]) ] -> let* id = global_declaration_group_of_json decl in - Ok (M.Global id) + Ok (Crates.Global id) | _ -> Error "") let length_of_json_list (js : json) : (int, string) result = @@ -732,8 +731,8 @@ let length_of_json_list (js : json) : (int, string) result = | `List jsl -> Ok (List.length jsl) | _ -> Error ("not a list: " ^ show js)) -let llbc_module_of_json (js : json) : (M.llbc_module, string) result = - combine_error_msgs js "llbc_module_of_json" +let llbc_crate_of_json (js : json) : (Crates.llbc_crate, string) result = + combine_error_msgs js "llbc_crate_of_json" (match js with | `Assoc [ @@ -763,7 +762,7 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result = let globals, global_bodies = List.split globals in Ok { - M.name; + Crates.name; declarations; types; functions = functions @ global_bodies; diff --git a/src/PrePasses.ml b/src/PrePasses.ml index c9d496ea..3159907e 100644 --- a/src/PrePasses.ml +++ b/src/PrePasses.ml @@ -7,7 +7,6 @@ module V = Values module E = Expressions module C = Contexts module A = LlbcAst -module M = Modules module L = Logging let log = L.pre_passes_log @@ -50,6 +49,6 @@ let filter_drop_assigns (f : A.fun_decl) : A.fun_decl = in { f with body } -let apply_passes (m : M.llbc_module) : M.llbc_module = +let apply_passes (m : Crates.llbc_crate) : Crates.llbc_crate = let functions = List.map filter_drop_assigns m.functions in { m with functions } diff --git a/src/Print.ml b/src/Print.ml index c10c5989..1439a74d 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -6,7 +6,6 @@ module VU = ValuesUtils module E = Expressions module A = LlbcAst module C = Contexts -module M = Modules let option_to_string (to_string : 'a -> string) (x : 'a option) : string = match x with Some x -> "Some (" ^ to_string x ^ ")" | None -> "None" @@ -1194,19 +1193,21 @@ module Module = struct in PA.fun_decl_to_string fmt "" " " def - let module_to_string (m : M.llbc_module) : string = + let module_to_string (m : Crates.llbc_crate) : string = let types_defs_map, funs_defs_map, globals_defs_map = - M.compute_defs_maps m + Crates.compute_defs_maps m in (* The types *) - let type_decls = List.map (type_decl_to_string types_defs_map) m.M.types in + let type_decls = + List.map (type_decl_to_string types_defs_map) m.Crates.types + in (* The functions *) let fun_decls = List.map (fun_decl_to_string types_defs_map funs_defs_map globals_defs_map) - m.M.functions + m.Crates.functions in (* Put everything together *) diff --git a/src/PrintSymbolicAst.ml b/src/PrintSymbolicAst.ml index e44b422a..37b7555e 100644 --- a/src/PrintSymbolicAst.ml +++ b/src/PrintSymbolicAst.ml @@ -14,7 +14,6 @@ module V = Values module E = Expressions module A = LlbcAst module C = Contexts -module M = Modules open SymbolicAst module P = Print module PT = Print.Types diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index f321ce8c..77c5e0e8 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -3,7 +3,6 @@ open LlbcAstUtils open Pure open PureUtils module Id = Identifiers -module M = Modules module S = SymbolicAst module TA = TypesAnalysis module L = Logging diff --git a/src/Translate.ml b/src/Translate.ml index 61300ed8..8024d910 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -3,7 +3,6 @@ open Interpreter module L = Logging module T = Types module A = LlbcAst -module M = Modules module SA = SymbolicAst module Micro = PureMicroPasses open PureUtils @@ -286,24 +285,24 @@ let translate_function_to_pure (config : C.partial_config) (pure_forward, pure_backwards) let translate_module_to_pure (config : C.partial_config) - (mp_config : Micro.config) (use_state : bool) (m : M.llbc_module) : + (mp_config : Micro.config) (use_state : bool) (crate : Crates.llbc_crate) : trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list = (* Debug *) log#ldebug (lazy "translate_module_to_pure"); (* Compute the type and function contexts *) let type_context, fun_context, global_context = - compute_type_fun_global_contexts m + compute_type_fun_global_contexts crate in let fun_infos = - FA.analyze_module m fun_context.C.fun_decls global_context.C.global_decls - use_state + FA.analyze_module crate fun_context.C.fun_decls + global_context.C.global_decls 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 (* Translate all the type definitions *) - let type_decls = SymbolicToPure.translate_type_decls m.types in + let type_decls = SymbolicToPure.translate_type_decls crate.types in (* Compute the type definition map *) let type_decls_map = @@ -330,7 +329,7 @@ let translate_module_to_pure (config : C.partial_config) (LlbcAstUtils.fun_body_get_input_vars body) in (A.Regular fdef.def_id, input_names, fdef.signature)) - m.functions + crate.functions in let sigs = List.append assumed_sigs local_sigs in let fun_sigs = @@ -343,7 +342,7 @@ let translate_module_to_pure (config : C.partial_config) List.map (translate_function_to_pure config mp_config trans_ctx fun_sigs type_decls_map) - m.functions + crate.functions in (* Apply the micro-passes *) @@ -357,7 +356,7 @@ let translate_module_to_pure (config : C.partial_config) (trans_ctx, type_decls, pure_translations) type gen_ctx = { - m : M.llbc_module; + crate : Crates.llbc_crate; extract_ctx : PureToExtract.extraction_ctx; trans_types : Pure.type_decl Pure.TypeDeclId.Map.t; trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t; @@ -534,7 +533,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) ExtractToFStar.extract_state_type fmt ctx.extract_ctx qualif in - let export_decl (decl : M.declaration_group) : unit = + let export_decl (decl : Crates.declaration_group) : unit = match decl with | Type (NonRec id) -> if config.extract_types then export_type ExtractToFStar.Type id @@ -574,7 +573,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) *) if config.extract_state_type && config.extract_fun_decls then export_state_type (); - List.iter export_decl ctx.m.declarations; + List.iter export_decl ctx.crate.declarations; if config.extract_state_type && not config.extract_fun_decls then export_state_type () @@ -628,11 +627,11 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) TODO: rename to translate_crate *) let translate_module (filename : string) (dest_dir : string) (config : config) - (m : M.llbc_module) : unit = + (crate : Crates.llbc_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 m + config.use_state crate in (* Initialize the extraction context - for now we extract only to F* *) @@ -641,7 +640,8 @@ let translate_module (filename : string) (dest_dir : string) (config : config) in let variant_concatenate_type_name = true in let fstar_fmt = - ExtractToFStar.mk_formatter trans_ctx m.name variant_concatenate_type_name + ExtractToFStar.mk_formatter trans_ctx crate.name + variant_concatenate_type_name in let ctx = { PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 } @@ -653,8 +653,9 @@ let translate_module (filename : string) (dest_dir : string) (config : config) A.FunDeclId.Set.of_list (List.concat (List.map - (fun decl -> match decl with M.Fun (Rec ids) -> ids | _ -> []) - m.declarations)) + (fun decl -> + match decl with Crates.Fun (Rec ids) -> ids | _ -> []) + crate.declarations)) in (* Register unique names for all the top-level types, globals and functions. @@ -686,7 +687,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) let ctx = List.fold_left ExtractToFStar.extract_global_decl_register_names ctx - m.globals + crate.globals in (* Open the output file *) @@ -746,7 +747,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) (* Extract the file(s) *) let gen_ctx = { - m; + crate; extract_ctx = ctx; trans_types; trans_funs; @@ -793,8 +794,8 @@ let translate_module (filename : string) (dest_dir : string) (config : config) interface = has_opaque_types; } in - extract_file types_config gen_ctx types_filename m.M.name types_module - ": type definitions" [] []; + extract_file types_config gen_ctx types_filename crate.Crates.name + types_module ": type definitions" [] []; (* Extract the template clauses *) let needs_clauses_module = @@ -807,7 +808,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) let clauses_config = { base_gen_config with extract_template_decreases_clauses = true } in - extract_file clauses_config gen_ctx clauses_filename m.M.name + extract_file clauses_config gen_ctx clauses_filename crate.Crates.name clauses_module ": templates for the decreases clauses" [ types_module ] []); @@ -825,7 +826,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) interface = true; } in - extract_file opaque_config gen_ctx opaque_filename m.M.name + extract_file opaque_config gen_ctx opaque_filename crate.Crates.name opaque_module ": opaque function definitions" [] [ types_module ]; [ opaque_module ]) else [] @@ -844,7 +845,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) let clauses_module = if needs_clauses_module then [ module_name ^ ".Clauses" ] else [] in - extract_file fun_config gen_ctx fun_filename m.M.name fun_module + extract_file fun_config gen_ctx fun_filename crate.Crates.name fun_module ": function definitions" [] ([ types_module ] @ opaque_funs_module @ clauses_module)) else @@ -866,5 +867,5 @@ let translate_module (filename : string) (dest_dir : string) (config : config) in (* Add the extension for F* *) let extract_filename = extract_filebasename ^ ".fst" in - extract_file gen_config gen_ctx extract_filename m.M.name module_name "" [] - [] + extract_file gen_config gen_ctx extract_filename crate.Crates.name + module_name "" [] [] diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml index 326bb05f..a658147d 100644 --- a/src/TranslateCore.ml +++ b/src/TranslateCore.ml @@ -4,7 +4,6 @@ open InterpreterStatements module L = Logging module T = Types module A = LlbcAst -module M = Modules module SA = SymbolicAst module FA = FunsAnalysis diff --git a/src/TypesAnalysis.ml b/src/TypesAnalysis.ml index e84b4f58..0d23e92b 100644 --- a/src/TypesAnalysis.ml +++ b/src/TypesAnalysis.ml @@ -1,5 +1,5 @@ open Types -open Modules +open Crates type subtype_info = { under_borrow : bool; (** Are we inside a borrow? *) diff --git a/src/main.ml b/src/main.ml index 6b1083f5..b7868722 100644 --- a/src/main.ml +++ b/src/main.ml @@ -141,7 +141,7 @@ let () = translate_log#set_level EL.Info; (* Load the module *) let json = Yojson.Basic.from_file filename in - match llbc_module_of_json json with + match llbc_crate_of_json json with | Error s -> main_log#error "error: %s\n" s; exit 1 diff --git a/tests/betree/BetreeMain.Clauses.Template.fst b/tests/betree/BetreeMain.Clauses.Template.fst index c2412775..d48213d3 100644 --- a/tests/betree/BetreeMain.Clauses.Template.fst +++ b/tests/betree/BetreeMain.Clauses.Template.fst @@ -6,7 +6,7 @@ open BetreeMain.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [core::num::u64::{9}::MAX] *) +(** [core::num::u64::{10}::MAX] *) let core_num_u64_max_body : result u64 = Return 18446744073709551615 let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body diff --git a/tests/betree/BetreeMain.Funs.fst b/tests/betree/BetreeMain.Funs.fst index e80e96a6..9ba5d3e7 100644 --- a/tests/betree/BetreeMain.Funs.fst +++ b/tests/betree/BetreeMain.Funs.fst @@ -80,7 +80,7 @@ let betree_node_id_counter_fresh_id_back | Return i -> Return (Mkbetree_node_id_counter_t i) end -(** [core::num::u64::{9}::MAX] *) +(** [core::num::u64::{10}::MAX] *) let core_num_u64_max_body : result u64 = Return 18446744073709551615 let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body diff --git a/tests/betree/BetreeMain.Types.fsti b/tests/betree/BetreeMain.Types.fsti index f0ca1d9e..c81e3302 100644 --- a/tests/betree/BetreeMain.Types.fsti +++ b/tests/betree/BetreeMain.Types.fsti @@ -55,7 +55,7 @@ type betree_be_tree_t = betree_be_tree_root : betree_node_t; } -(** [core::num::u64::{9}::MAX] *) +(** [core::num::u64::{10}::MAX] *) let core_num_u64_max_body : result u64 = Return 18446744073709551615 let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body diff --git a/tests/hashmap/Hashmap.Clauses.Template.fst b/tests/hashmap/Hashmap.Clauses.Template.fst index 2a3d9cb9..3e51c6f1 100644 --- a/tests/hashmap/Hashmap.Clauses.Template.fst +++ b/tests/hashmap/Hashmap.Clauses.Template.fst @@ -24,7 +24,7 @@ let hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t) (ls : list_t t) : nat = admit () -(** [core::num::u32::{8}::MAX] *) +(** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst index 397ee720..6e67fca4 100644 --- a/tests/hashmap/Hashmap.Funs.fst +++ b/tests/hashmap/Hashmap.Funs.fst @@ -188,7 +188,7 @@ let hash_map_insert_no_resize_fwd_back end end -(** [core::num::u32::{8}::MAX] *) +(** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body diff --git a/tests/hashmap/Hashmap.Types.fst b/tests/hashmap/Hashmap.Types.fst index f81f4185..d53b8a42 100644 --- a/tests/hashmap/Hashmap.Types.fst +++ b/tests/hashmap/Hashmap.Types.fst @@ -19,7 +19,7 @@ type hash_map_t (t : Type0) = hash_map_slots : vec (list_t t); } -(** [core::num::u32::{8}::MAX] *) +(** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body diff --git a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst index 0cf876d9..55685114 100644 --- a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst +++ b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst @@ -24,7 +24,7 @@ let hashmap_hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) : nat = admit () -(** [core::num::u32::{8}::MAX] *) +(** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst index 83bf80d1..82b44dbd 100644 --- a/tests/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst @@ -198,7 +198,7 @@ let hashmap_hash_map_insert_no_resize_fwd_back end end -(** [core::num::u32::{8}::MAX] *) +(** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body diff --git a/tests/hashmap_on_disk/HashmapMain.Types.fsti b/tests/hashmap_on_disk/HashmapMain.Types.fsti index 370844db..ce4d6485 100644 --- a/tests/hashmap_on_disk/HashmapMain.Types.fsti +++ b/tests/hashmap_on_disk/HashmapMain.Types.fsti @@ -19,7 +19,7 @@ type hashmap_hash_map_t (t : Type0) = hashmap_hash_map_slots : vec (hashmap_list_t t); } -(** [core::num::u32::{8}::MAX] *) +(** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body diff --git a/tests/misc/BetreeNll.fst b/tests/misc/BetreePolonius.fst index b548a18b..2bac07b6 100644 --- a/tests/misc/BetreeNll.fst +++ b/tests/misc/BetreePolonius.fst @@ -1,16 +1,16 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_nll] *) -module BetreeNll +(** [betree_polonius] *) +module BetreePolonius open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_nll::List] *) +(** [betree_polonius::List] *) type list_t (t : Type0) = | ListCons : t -> list_t t -> list_t t | ListNil : list_t t -(** [betree_nll::get_list_at_x] *) +(** [betree_polonius::get_list_at_x] *) let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) = begin match ls with | ListCons hd tl -> @@ -24,7 +24,7 @@ let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) = | ListNil -> Return ListNil end -(** [betree_nll::get_list_at_x] *) +(** [betree_polonius::get_list_at_x] *) let rec get_list_at_x_back (ls : list_t u32) (x : u32) (ret : list_t u32) : result (list_t u32) = begin match ls with diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst index 4a9a0e48..884d1778 100644 --- a/tests/misc/Constants.fst +++ b/tests/misc/Constants.fst @@ -9,7 +9,7 @@ open Primitives let x0_body : result u32 = Return 0 let x0_c : u32 = eval_global x0_body -(** [core::num::u32::{8}::MAX] *) +(** [core::num::u32::{9}::MAX] *) let core_num_u32_max_body : result u32 = Return 4294967295 let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body |