From 479694819f7409cf92b4d0f2775853cda18c3ab4 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 4 Mar 2022 14:01:27 +0100 Subject: Fix minor issues for the translation of hashmap_on_disk --- Makefile | 40 ++++++++++++++++++++++------------------ src/ExtractToFStar.ml | 26 ++++++++++++++++++++++---- src/Translate.ml | 46 ++++++++++++++++++++++++++++++++++++++-------- 3 files changed, 82 insertions(+), 30 deletions(-) diff --git a/Makefile b/Makefile index c9839b45..0d99fa40 100644 --- a/Makefile +++ b/Makefile @@ -29,21 +29,26 @@ build: # Test the project .PHONY: test -test: build translate-no_nested_borrows translate-hashmap translate-paper \ - translate-external translate-nll-betree_nll +test: build trans-no_nested_borrows trans-paper \ + trans-hashmap trans-hashmap_main \ + trans-external trans-nll-betree_nll # Add specific options to some tests -translate-no_nested_borrows translate-paper: \ +trans-no_nested_borrows trans-paper: \ TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses -translate-no_nested_borrows translate-paper: SUBDIR:=misc -translate-hashmap: TRANS_OPTIONS += -template-clauses -no-state -translate-hashmap: SUBDIR:=hashmap +trans-no_nested_borrows trans-paper: SUBDIR:=misc -translate-nll-betree_nll: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses -translate-nll-betree_nll: SUBDIR:=misc +trans-hashmap: TRANS_OPTIONS += -template-clauses -no-state +trans-hashmap: SUBDIR:=hashmap -translate-external: TRANS_OPTIONS += -translate-external: SUBDIR:=misc +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-external: TRANS_OPTIONS += +trans-external: SUBDIR:=misc # 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 @@ -52,17 +57,16 @@ translate-external: SUBDIR:=misc gen-llbc-%: build cd $(CHARON_HOME) && make test-$* -# Generic rule to test the translation on an LLBC file. -# Note that the non-linear lifetime files are generated in the tests-nll -# subdirectory. -.PHONY: translate-% -translate-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc -translate-nll-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-nll/llbc +# Generic rule to test the translation of an LLBC file. +# Note that the non-linear lifetime files are generated in the tests-nll subdirectory. +.PHONY: trans-% +trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc +trans-nll-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-nll/llbc -translate-%: gen-llbc-% +trans-%: gen-llbc-% dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) -translate-nll-%: gen-llbc-nll-% +trans-nll-%: gen-llbc-nll-% dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) .PHONY: doc diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 1f59075a..9d96d058 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -1192,7 +1192,7 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) *) let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (qualif : fun_decl_qualif) (has_decreases_clause : bool) - (fwd_def : fun_decl) (def : fun_decl) : unit = + (has_state_param : bool) (fwd_def : fun_decl) (def : fun_decl) : unit = (* Retrieve the function name *) let def_name = ctx_get_local_function def.def_id def.back_id ctx in (* (* Add the type parameters - note that we need those bindings only for the @@ -1279,12 +1279,30 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) * backward functions have no influence on termination: we thus * share the decrease clauses between the forward and the backward * functions). + * Something annoying is that there may be a state parameter, for + * the state-error monad, in which case we need to forget the input + * parameter before last: + * ``` + * val f_fwd (x : u32) (st : state) : + * Tot (result (state & u32)) (decreases (f_decreases x st)) + * + * We ignore this parameter + * VVV + * val f_back (x : u32) (ret : u32) (st : state) : + * Tot (result (state & u32)) (decreases (f_decreases x st)) + * ``` * Rk.: if a function has a decreases clause, it is necessarily * a transparent function *) let inputs_lvs = - Collections.List.prefix - (List.length (Option.get fwd_def.body).inputs_lvs) - (Option.get def.body).inputs_lvs + let num_fwd_inputs = List.length (Option.get fwd_def.body).inputs_lvs in + let num_fwd_inputs = + if has_state_param then num_fwd_inputs - 1 else num_fwd_inputs + in + let all_inputs = (Option.get def.body).inputs_lvs in + let inputs = Collections.List.prefix num_fwd_inputs all_inputs in + if has_state_param then + inputs @ [ List.nth all_inputs (List.length all_inputs - 1) ] + else inputs in let _ = List.fold_left diff --git a/src/Translate.ml b/src/Translate.ml index 29f8f5ba..c29dd963 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -347,6 +347,7 @@ type gen_ctx = { (** Extraction context *) type gen_config = { + mp_config : Micro.config; extract_types : bool; extract_decreases_clauses : bool; extract_template_decreases_clauses : bool; @@ -470,13 +471,19 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) let has_decr_clause = has_decreases_clause def && config.extract_decreases_clauses in + (* Is there an input parameter "visible" for the state used in + * the state error monad (if we use a state error monad)? *) + let has_state_param = + config.mp_config.use_state_monad + && config.mp_config.unfold_monadic_let_bindings + in (* Check if the definition needs to be filtered or not *) if ((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque) then ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif - has_decr_clause fwd_def def) + has_decr_clause has_state_param fwd_def def) fls); (* Insert unit tests if necessary *) if config.test_unit_functions then @@ -579,7 +586,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) Format.pp_print_newline fmt (); (* Some logging *) - log#linfo (lazy ("Generated: " ^ filename)) + log#linfo (lazy ("Generated: " ^ filename)); + + (* Flush and close the file *) + close_out out (** Translate a module and write the synthesized code to an output file. TODO: rename to translate_crate @@ -665,6 +675,30 @@ let translate_module (filename : string) (dest_dir : string) (config : config) trans_funs) in + (* Create the directory, if necessary *) + if not (Sys.file_exists dest_dir) then ( + log#linfo (lazy ("Creating missing directory: " ^ dest_dir)); + (* Create a directory with *default* permissions *) + Core.Unix.mkdir_p dest_dir); + + (* Copy "Primitives.fst" - I couldn't find a "cp" function in the OCaml + * libraries... *) + let _ = + let src = open_in "fstar/Primitives.fst" in + let tgt_filename = Filename.concat dest_dir "Primitives.fst" in + let tgt = open_out tgt_filename in + 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)) + in + (* Extract the file(s) *) let gen_ctx = { @@ -676,18 +710,13 @@ let translate_module (filename : string) (dest_dir : string) (config : config) } in - (* Create the directory, if necessary *) - if not (Sys.file_exists dest_dir) then ( - log#linfo (lazy ("Creating missing directory: " ^ dest_dir)); - (* Create a directory with *default* permissions *) - Core.Unix.mkdir_p dest_dir); - let use_state = config.mp_config.use_state_monad in (* Extract one or several files, depending on the configuration *) if config.split_files then ( let base_gen_config = { + mp_config = config.mp_config; extract_types = false; extract_decreases_clauses = config.extract_decreases_clauses; extract_template_decreases_clauses = false; @@ -776,6 +805,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) else let gen_config = { + mp_config = config.mp_config; extract_types = true; extract_decreases_clauses = config.extract_decreases_clauses; extract_template_decreases_clauses = -- cgit v1.2.3