From 6f14e8c699169aa11ea9c106f8cae1ba593569d0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 22 May 2024 15:11:28 +0200 Subject: Add simple test runner --- tests/test_runner/.ocamlformat | 0 tests/test_runner/aeneas_test_runner.opam | 27 +++++++++++++++++++++++++++ tests/test_runner/dune | 4 ++++ tests/test_runner/dune-project | 25 +++++++++++++++++++++++++ tests/test_runner/run_test.ml | 30 ++++++++++++++++++++++++++++++ 5 files changed, 86 insertions(+) create mode 100644 tests/test_runner/.ocamlformat create mode 100644 tests/test_runner/aeneas_test_runner.opam create mode 100644 tests/test_runner/dune create mode 100644 tests/test_runner/dune-project create mode 100644 tests/test_runner/run_test.ml (limited to 'tests/test_runner') diff --git a/tests/test_runner/.ocamlformat b/tests/test_runner/.ocamlformat new file mode 100644 index 00000000..e69de29b diff --git a/tests/test_runner/aeneas_test_runner.opam b/tests/test_runner/aeneas_test_runner.opam new file mode 100644 index 00000000..b57cc9f6 --- /dev/null +++ b/tests/test_runner/aeneas_test_runner.opam @@ -0,0 +1,27 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "0.1" +authors: ["Son Ho" "Guillaume Boisseau"] +license: "Apache-2.0" +homepage: "https://github.com/AeneasVerif/aeneas" +bug-reports: "https://github.com/AeneasVerif/aeneas/issues" +depends: [ + "ocaml" + "dune" {>= "3.12"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/AeneasVerif/aeneas.git" diff --git a/tests/test_runner/dune b/tests/test_runner/dune new file mode 100644 index 00000000..7da7a96d --- /dev/null +++ b/tests/test_runner/dune @@ -0,0 +1,4 @@ +(executable + (public_name test_runner) + (libraries unix) + (name run_test)) diff --git a/tests/test_runner/dune-project b/tests/test_runner/dune-project new file mode 100644 index 00000000..c614e923 --- /dev/null +++ b/tests/test_runner/dune-project @@ -0,0 +1,25 @@ +(lang dune 3.12) + +(name aeneas_test_runner) + +(version 0.1) + +(generate_opam_files true) + +(source + (uri git+https://github.com/AeneasVerif/aeneas.git)) + +(homepage "https://github.com/AeneasVerif/aeneas") + +(bug_reports "https://github.com/AeneasVerif/aeneas/issues") + +(authors + "Son Ho" + "Guillaume Boisseau") + +(license Apache-2.0) + +(package + (name aeneas_test_runner) + (depends ocaml dune) +) diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml new file mode 100644 index 00000000..379abe04 --- /dev/null +++ b/tests/test_runner/run_test.ml @@ -0,0 +1,30 @@ +let concat_path = List.fold_left Filename.concat "" + +let () = + match Array.to_list Sys.argv with + (* Ad-hoc argument passing for now. *) + | _exe_path :: aeneas_path :: tests_dir :: test_name :: subdir :: backend + :: options -> + let input_file = concat_path [ tests_dir; "llbc"; test_name ] ^ ".llbc" in + let dest_dir = concat_path [ "tests"; backend; subdir ] in + let args = + [| aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend |] + in + let args = Array.append args (Array.of_list options) in + + (* Debug arguments *) + print_string "[test_runner] Running: "; + Array.iter + (fun x -> + print_string x; + print_string " ") + args; + print_endline ""; + + (* Run Aeneas *) + let pid = + Unix.create_process aeneas_path args Unix.stdin Unix.stdout Unix.stderr + in + let _ = Unix.waitpid [] pid in + () + | _ -> () -- cgit v1.3.1 From 6ae8cde046530371345863f04d84be32b2a757bf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 22 May 2024 18:57:19 +0200 Subject: Move the subdirectory selection to the test runner --- Makefile | 55 ++----------------------------------------- tests/test_runner/run_test.ml | 29 ++++++++++++++++++++--- 2 files changed, 28 insertions(+), 56 deletions(-) (limited to 'tests/test_runner') diff --git a/Makefile b/Makefile index 2457bec2..5e8fe7bb 100644 --- a/Makefile +++ b/Makefile @@ -37,8 +37,6 @@ OPTIONS ?= CHARON_TEST_DIR ?= $(CHARON_HOME)/tests # The options with which to call Charon CHARON_OPTIONS = -# The directory in which to extract the result of the translation -SUBDIR := #################################### # The rules @@ -157,56 +155,7 @@ CHARON_CMD = cd $(CHARON_TEST_DIR) && $(MAKE) test-$* endif # The command to run Aeneas on the proper llbc file -AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) "$(SUBDIR)" $(BACKEND) $(OPTIONS) - -# Subdirs -test-arrays: SUBDIR := arrays -tlean-arrays: SUBDIR := - -test-betree_main: SUBDIR := betree -tlean-betree_main: SUBDIR := - -ctest-test-betree_main: SUBDIR := betree_back_stateful - -test-bitwise: SUBDIR := misc -tlean-bitwise: SUBDIR := -thol4-bitwise: SUBDIR := misc-bitwise - -test-constants: SUBDIR := misc -tlean-constants: SUBDIR := -thol4-constants: SUBDIR := misc-constants - -test-demo: SUBDIR := demo -tlean-demo: SUBDIR := Demo - -test-external: SUBDIR := misc -tlean-external: SUBDIR := -thol4-external: SUBDIR := misc-external - -test-hashmap: SUBDIR := hashmap -tlean-hashmap: SUBDIR := - -test-hashmap_main: SUBDIR := hashmap_on_disk -tlean-hashmap_main: SUBDIR := - -test-loops: SUBDIR := misc -tlean-loops: SUBDIR := -thol4-loops: SUBDIR := misc-loops - -test-no_nested_borrows: SUBDIR := misc -tlean-no_nested_borrows: SUBDIR := -thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows - -test-paper: SUBDIR := misc -tlean-paper: SUBDIR := -thol4-paper: SUBDIR := misc-paper - -test-polonius_list: SUBDIR := misc -tlean-polonius_list: SUBDIR := -thol4-polonius_list: SUBDIR := misc-polonius_list - -test-traits: SUBDIR := traits -tlean-traits: SUBDIR := +AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(BACKEND) $(OPTIONS) # Add specific options to some tests # TODO: reactivate -test-trans-units for hashmap and hashmap_main @@ -288,7 +237,7 @@ thol4-%: # This generates very ugly code, but is good to test the translation. .PHONY: ctest-test-betree_main ctest-test-betree_main: test-betree_main -ctest-test-betree_main: FILE = betree_main +ctest-test-betree_main: FILE = betree_main-special ctest-test-betree_main: BACKEND := fstar ctest-test-betree_main: $(AENEAS_CMD) diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 379abe04..52ff7276 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -3,9 +3,32 @@ let concat_path = List.fold_left Filename.concat "" let () = match Array.to_list Sys.argv with (* Ad-hoc argument passing for now. *) - | _exe_path :: aeneas_path :: tests_dir :: test_name :: subdir :: backend - :: options -> - let input_file = concat_path [ tests_dir; "llbc"; test_name ] ^ ".llbc" in + | _exe_path :: aeneas_path :: tests_dir :: test_name :: backend :: options -> + (* Reproduces the file layout that was set by the Makefile. FIXME: cleanup *) + let subdir = + match (backend, test_name) with + | "lean", "demo" -> "Demo" + | "lean", _ -> "." + | _, ("arrays" | "demo" | "hashmap" | "traits") -> test_name + | _, "betree_main" -> "betree" + | _, "betree_main-special" -> "betree_back_stateful" + | _, "hashmap_main" -> "hashmap_on_disk" + | "hol4", _ -> "misc-" ^ test_name + | ( _, + ( "bitwise" | "constants" | "external" | "loops" + | "no_nested_borrows" | "paper" | "polonius_list" ) ) -> + "misc" + | _ -> test_name + in + + let test_file_name = + match test_name with + | "betree_main-special" -> "betree_main" + | _ -> test_name + in + let input_file = + concat_path [ tests_dir; "llbc"; test_file_name ] ^ ".llbc" + in let dest_dir = concat_path [ "tests"; backend; subdir ] in let args = [| aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend |] -- cgit v1.3.1 From a9471e615e03d6fa0bc1594176fe504c9a3c88ae Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 22 May 2024 19:23:03 +0200 Subject: Set all options in the test runner --- Makefile | 52 +-------------------------------------- tests/test_runner/run_test.ml | 57 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 58 insertions(+), 51 deletions(-) (limited to 'tests/test_runner') diff --git a/Makefile b/Makefile index 5e8fe7bb..0ceaa558 100644 --- a/Makefile +++ b/Makefile @@ -117,7 +117,7 @@ test: build-dev test-all test-all: \ test-arrays \ test-betree_main \ - ctest-test-betree_main \ + tfstar-betree_main-special \ test-bitwise \ test-constants \ test-demo \ @@ -157,47 +157,6 @@ endif # The command to run Aeneas on the proper llbc file AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(BACKEND) $(OPTIONS) -# Add specific options to some tests -# TODO: reactivate -test-trans-units for hashmap and hashmap_main -tfstar-arrays: OPTIONS += -decreases-clauses -template-clauses -split-files -tcoq-arrays: OPTIONS += -use-fuel - -test-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files -tfstar-betree_main: OPTIONS += -decreases-clauses -template-clauses -tcoq-betree_main: OPTIONS += -use-fuel - -ctest-test-betree_main: OPTIONS += -test-trans-units -state -split-files -ctest-test-betree_main: OPTIONS += -decreases-clauses -template-clauses - -test-bitwise: OPTIONS += -test-trans-units - -test-constants: OPTIONS += -test-trans-units - -tfstar-demo: OPTIONS += -use-fuel -tcoq-demo: OPTIONS += -use-fuel - -test-external: OPTIONS += -test-trans-units -state -split-files - -test-hashmap: OPTIONS += -split-files -tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses -tcoq-hashmap: OPTIONS += -use-fuel -tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hashmap.lean file: we do not want to overwrite it - -test-hashmap_main: OPTIONS += -state -split-files -tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses -tcoq-hashmap_main: OPTIONS += -use-fuel - -tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -split-files -tcoq-loops: OPTIONS += -use-fuel - -test-no_nested_borrows: OPTIONS += -test-trans-units - -test-paper: OPTIONS += -test-trans-units - -test-polonius_list: OPTIONS += -test-trans-units - -tfstar-traits: OPTIONS += -decreases-clauses -template-clauses - # 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. @@ -233,15 +192,6 @@ thol4-%: echo Ignoring the $* test for HOL4 # $(AENEAS_CMD) -# Additional, *c*ustom test on the betree: translate it without `-backward-no-state-update`. -# This generates very ugly code, but is good to test the translation. -.PHONY: ctest-test-betree_main -ctest-test-betree_main: test-betree_main -ctest-test-betree_main: FILE = betree_main-special -ctest-test-betree_main: BACKEND := fstar -ctest-test-betree_main: - $(AENEAS_CMD) - # Nix - TODO: add the lean tests .PHONY: nix nix: diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 52ff7276..949d5307 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -21,6 +21,63 @@ let () = | _ -> test_name in + (* File-specific options *) + (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *) + let use_fuel = + match (backend, test_name) with + | ( "coq", + ( "arrays" | "betree_main" | "demo" | "hashmap" | "hashmap_main" + | "loops" ) ) -> + true + | "fstar", "demo" -> true + | _ -> false + in + let options = if use_fuel then "-use-fuel" :: options else options in + + let decrease_template_clauses = + backend = "fstar" + && + match test_name with + | "arrays" | "betree_main" | "betree_main-special" | "hashmap" + | "hashmap_main" | "loops" | "traits" -> + true + | _ -> false + in + let options = + if decrease_template_clauses then + "-decreases-clauses" :: "-template-clauses" :: options + else options + in + + let extra_options = + match (backend, test_name) with + (* Additional, custom test on the betree: translate it without `-backward-no-state-update`. *) + (* This generates very ugly code, but is good to test the translation. *) + | _, "betree_main-special" -> + [ "-test-trans-units"; "-state"; "-split-files" ] + | _, "betree_main" -> + [ + "-backward-no-state-update"; + "-test-trans-units"; + "-state"; + "-split-files"; + ] + | _, "bitwise" -> [ "-test-trans-units" ] + | _, "constants" -> [ "-test-trans-units" ] + | _, "external" -> [ "-test-trans-units"; "-state"; "-split-files" ] + | _, "hashmap_main" -> [ "-state"; "-split-files" ] + | _, "no_nested_borrows" -> [ "-test-trans-units" ] + | _, "paper" -> [ "-test-trans-units" ] + | _, "polonius_list" -> [ "-test-trans-units" ] + | "fstar", "arrays" -> [ "-split-files" ] + | "fstar", "loops" -> [ "-split-files" ] + (* We add a custom import in the Hashmap.lean file: we do not want to overwrite it *) + | "lean", "hashmap" -> [ "-split-files"; "-no-gen-lib-entry" ] + | _, "hashmap" -> [ "-split-files" ] + | _ -> [] + in + let options = List.append extra_options options in + let test_file_name = match test_name with | "betree_main-special" -> "betree_main" -- cgit v1.3.1 From 9e834db4174a900845199ccb189b575a20f11eda Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 09:58:36 +0200 Subject: Cleanup test runner --- tests/test_runner/run_test.ml | 223 +++++++++++++++++++++++------------------- 1 file changed, 124 insertions(+), 99 deletions(-) (limited to 'tests/test_runner') diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 949d5307..1ec2d1c8 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -1,110 +1,135 @@ -let concat_path = List.fold_left Filename.concat "" +(* Paths to use for tests *) +type test_env = { aeneas_path : string; llbc_dir : string } -let () = - match Array.to_list Sys.argv with - (* Ad-hoc argument passing for now. *) - | _exe_path :: aeneas_path :: tests_dir :: test_name :: backend :: options -> - (* Reproduces the file layout that was set by the Makefile. FIXME: cleanup *) - let subdir = - match (backend, test_name) with - | "lean", "demo" -> "Demo" - | "lean", _ -> "." - | _, ("arrays" | "demo" | "hashmap" | "traits") -> test_name - | _, "betree_main" -> "betree" - | _, "betree_main-special" -> "betree_back_stateful" - | _, "hashmap_main" -> "hashmap_on_disk" - | "hol4", _ -> "misc-" ^ test_name - | ( _, - ( "bitwise" | "constants" | "external" | "loops" - | "no_nested_borrows" | "paper" | "polonius_list" ) ) -> - "misc" - | _ -> test_name - in +(* The data for a specific test to run *) +type test_case = { + name : string; + backend : string; + subdir : string; + extra_aeneas_options : string list; +} - (* File-specific options *) - (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *) - let use_fuel = - match (backend, test_name) with - | ( "coq", - ( "arrays" | "betree_main" | "demo" | "hashmap" | "hashmap_main" - | "loops" ) ) -> - true - | "fstar", "demo" -> true - | _ -> false - in - let options = if use_fuel then "-use-fuel" :: options else options in +(* Run Aeneas on a specific input with the given options *) +let run_test env case = + let concat_path = List.fold_left Filename.concat "" in + let input_file = concat_path [ env.llbc_dir; "llbc"; case.name ] ^ ".llbc" in + let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in + let args = + [| + env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; case.backend; + |] + in + let args = Array.append args (Array.of_list case.extra_aeneas_options) in - let decrease_template_clauses = - backend = "fstar" - && - match test_name with - | "arrays" | "betree_main" | "betree_main-special" | "hashmap" - | "hashmap_main" | "loops" | "traits" -> - true - | _ -> false - in - let options = - if decrease_template_clauses then - "-decreases-clauses" :: "-template-clauses" :: options - else options - in + (* Debug arguments *) + print_string "[test_runner] Running: "; + Array.iter + (fun x -> + print_string x; + print_string " ") + args; + print_endline ""; - let extra_options = - match (backend, test_name) with - (* Additional, custom test on the betree: translate it without `-backward-no-state-update`. *) - (* This generates very ugly code, but is good to test the translation. *) - | _, "betree_main-special" -> - [ "-test-trans-units"; "-state"; "-split-files" ] - | _, "betree_main" -> - [ - "-backward-no-state-update"; - "-test-trans-units"; - "-state"; - "-split-files"; - ] - | _, "bitwise" -> [ "-test-trans-units" ] - | _, "constants" -> [ "-test-trans-units" ] - | _, "external" -> [ "-test-trans-units"; "-state"; "-split-files" ] - | _, "hashmap_main" -> [ "-state"; "-split-files" ] - | _, "no_nested_borrows" -> [ "-test-trans-units" ] - | _, "paper" -> [ "-test-trans-units" ] - | _, "polonius_list" -> [ "-test-trans-units" ] - | "fstar", "arrays" -> [ "-split-files" ] - | "fstar", "loops" -> [ "-split-files" ] - (* We add a custom import in the Hashmap.lean file: we do not want to overwrite it *) - | "lean", "hashmap" -> [ "-split-files"; "-no-gen-lib-entry" ] - | _, "hashmap" -> [ "-split-files" ] - | _ -> [] - in - let options = List.append extra_options options in + (* Run Aeneas *) + let pid = + Unix.create_process env.aeneas_path args Unix.stdin Unix.stdout Unix.stderr + in + let _ = Unix.waitpid [] pid in + () + +(* File-specific options *) +let test_options backend test_name = + (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *) + let use_fuel = + match (backend, test_name) with + | ( "coq", + ( "arrays" | "betree_main" | "demo" | "hashmap" | "hashmap_main" + | "loops" ) ) -> + true + | "fstar", "demo" -> true + | _ -> false + in + let options = if use_fuel then "-use-fuel" :: [] else [] in + + let decrease_template_clauses = + backend = "fstar" + && + match test_name with + | "arrays" | "betree_main" | "betree_main-special" | "hashmap" + | "hashmap_main" | "loops" | "traits" -> + true + | _ -> false + in + let options = + if decrease_template_clauses then + "-decreases-clauses" :: "-template-clauses" :: options + else options + in + + let extra_options = + match (backend, test_name) with + (* Additional, custom test on the betree: translate it without `-backward-no-state-update`. *) + (* This generates very ugly code, but is good to test the translation. *) + | _, "betree_main-special" -> + [ "-test-trans-units"; "-state"; "-split-files" ] + | _, "betree_main" -> + [ + "-backward-no-state-update"; + "-test-trans-units"; + "-state"; + "-split-files"; + ] + | _, "bitwise" -> [ "-test-trans-units" ] + | _, "constants" -> [ "-test-trans-units" ] + | _, "external" -> [ "-test-trans-units"; "-state"; "-split-files" ] + | _, "hashmap_main" -> [ "-state"; "-split-files" ] + | _, "no_nested_borrows" -> [ "-test-trans-units" ] + | _, "paper" -> [ "-test-trans-units" ] + | _, "polonius_list" -> [ "-test-trans-units" ] + | "fstar", "arrays" -> [ "-split-files" ] + | "fstar", "loops" -> [ "-split-files" ] + (* We add a custom import in the Hashmap.lean file: we do not want to overwrite it *) + | "lean", "hashmap" -> [ "-split-files"; "-no-gen-lib-entry" ] + | _, "hashmap" -> [ "-split-files" ] + | _ -> [] + in + let options = List.append extra_options options in + options + +(* The subdirectory in which to store the outputs. *) +(* This reproduces the file layout that was set by the old Makefile. FIXME: cleanup *) +let test_subdir backend test_name = + match (backend, test_name) with + | "lean", "demo" -> "Demo" + | "lean", _ -> "." + | _, ("arrays" | "demo" | "hashmap" | "traits") -> test_name + | _, "betree_main" -> "betree" + | _, "betree_main-special" -> "betree_back_stateful" + | _, "hashmap_main" -> "hashmap_on_disk" + | "hol4", _ -> "misc-" ^ test_name + | ( _, + ( "bitwise" | "constants" | "external" | "loops" | "no_nested_borrows" + | "paper" | "polonius_list" ) ) -> + "misc" + | _ -> test_name + +let () = + match Array.to_list Sys.argv with + (* Ad-hoc argument passing for now. *) + | _exe_path :: aeneas_path :: llbc_dir :: test_name :: backend :: options -> + let subdir = test_subdir backend test_name in + let options = List.append (test_options backend test_name) options in let test_file_name = match test_name with | "betree_main-special" -> "betree_main" | _ -> test_name in - let input_file = - concat_path [ tests_dir; "llbc"; test_file_name ] ^ ".llbc" - in - let dest_dir = concat_path [ "tests"; backend; subdir ] in - let args = - [| aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend |] - in - let args = Array.append args (Array.of_list options) in - - (* Debug arguments *) - print_string "[test_runner] Running: "; - Array.iter - (fun x -> - print_string x; - print_string " ") - args; - print_endline ""; - - (* Run Aeneas *) - let pid = - Unix.create_process aeneas_path args Unix.stdin Unix.stdout Unix.stderr - in - let _ = Unix.waitpid [] pid in - () + run_test { aeneas_path; llbc_dir } + { + name = test_file_name; + backend; + subdir; + extra_aeneas_options = options; + } | _ -> () -- cgit v1.3.1 From b953b89f9739c6703c49667781f5509b1b2a3898 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 10:05:04 +0200 Subject: Let the runner choose which backends to use --- Makefile | 33 +++++---------------------------- tests/test_runner/run_test.ml | 38 +++++++++++++++++++++++--------------- 2 files changed, 28 insertions(+), 43 deletions(-) (limited to 'tests/test_runner') diff --git a/Makefile b/Makefile index 0ceaa558..506dec5e 100644 --- a/Makefile +++ b/Makefile @@ -117,7 +117,7 @@ test: build-dev test-all test-all: \ test-arrays \ test-betree_main \ - tfstar-betree_main-special \ + test-betree_main-special \ test-bitwise \ test-constants \ test-demo \ @@ -154,9 +154,6 @@ else CHARON_CMD = cd $(CHARON_TEST_DIR) && $(MAKE) test-$* endif -# The command to run Aeneas on the proper llbc file -AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(BACKEND) $(OPTIONS) - # 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. @@ -164,34 +161,14 @@ AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(BACKE gen-llbc-%: $(CHARON_CMD) -# Generic rules to test the translation of an LLBC file. +# Translate the given llbc file to available backends. The test runner decides +# which backends to use and sets test-specific options. .PHONY: test-% test-%: FILE = $* -test-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-% +test-%: gen-llbc-% + $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(OPTIONS) echo "# Test $* done" -.PHONY: tfstar-% -tfstar-%: BACKEND := fstar -tfstar-%: - $(AENEAS_CMD) - -.PHONY: tcoq-% -tcoq-%: BACKEND := coq -tcoq-%: - $(AENEAS_CMD) - -.PHONY: tlean-% -tlean-%: BACKEND := lean -tlean-%: - $(AENEAS_CMD) - -# TODO: reactivate HOL4 once traits are parameterized by their associated types -.PHONY: thol4-% -thol4-%: BACKEND := hol4 -thol4-%: - echo Ignoring the $* test for HOL4 -# $(AENEAS_CMD) - # Nix - TODO: add the lean tests .PHONY: nix nix: diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 1ec2d1c8..52619c4a 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -116,20 +116,28 @@ let test_subdir backend test_name = let () = match Array.to_list Sys.argv with (* Ad-hoc argument passing for now. *) - | _exe_path :: aeneas_path :: llbc_dir :: test_name :: backend :: options -> - let subdir = test_subdir backend test_name in - let options = List.append (test_options backend test_name) options in - - let test_file_name = + | _exe_path :: aeneas_path :: llbc_dir :: test_name :: options -> + let tests_env = { aeneas_path; llbc_dir } in + (* TODO: reactivate HOL4 once traits are parameterized by their associated types *) + let backends = match test_name with - | "betree_main-special" -> "betree_main" - | _ -> test_name + | "betree_main-special" -> [ "fstar" ] + | _ -> [ "coq"; "lean"; "fstar" ] in - run_test { aeneas_path; llbc_dir } - { - name = test_file_name; - backend; - subdir; - extra_aeneas_options = options; - } - | _ -> () + List.iter + (fun backend -> + let subdir = test_subdir backend test_name in + let extra_aeneas_options = + List.append (test_options backend test_name) options + in + let test_file_name = + match test_name with + | "betree_main-special" -> "betree_main" + | _ -> test_name + in + let test_case = + { name = test_file_name; backend; subdir; extra_aeneas_options } + in + run_test tests_env test_case) + backends + | _ -> failwith "Incorrect options passed to test runner" -- cgit v1.3.1 From b8bdf14f3e4b25578d107160161f5bd2b548a113 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 14:06:51 +0200 Subject: Remove secondary betree test Opened https://github.com/AeneasVerif/aeneas/issues/196 to remember to add a more adequate replacement test. --- Makefile | 1 - .../BetreeMain.Clauses.Template.fst | 117 --- .../betree_back_stateful/BetreeMain.Clauses.fst | 210 ----- .../fstar/betree_back_stateful/BetreeMain.Funs.fst | 676 --------------- .../BetreeMain.FunsExternal.fsti | 30 - .../betree_back_stateful/BetreeMain.Types.fst | 61 -- .../BetreeMain.TypesExternal.fsti | 10 - tests/fstar/betree_back_stateful/Makefile | 49 -- tests/fstar/betree_back_stateful/Primitives.fst | 929 --------------------- tests/test_runner/run_test.ml | 22 +- 10 files changed, 4 insertions(+), 2101 deletions(-) delete mode 100644 tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst delete mode 100644 tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst delete mode 100644 tests/fstar/betree_back_stateful/BetreeMain.Funs.fst delete mode 100644 tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti delete mode 100644 tests/fstar/betree_back_stateful/BetreeMain.Types.fst delete mode 100644 tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti delete mode 100644 tests/fstar/betree_back_stateful/Makefile delete mode 100644 tests/fstar/betree_back_stateful/Primitives.fst (limited to 'tests/test_runner') diff --git a/Makefile b/Makefile index 506dec5e..dc38e56a 100644 --- a/Makefile +++ b/Makefile @@ -117,7 +117,6 @@ test: build-dev test-all test-all: \ test-arrays \ test-betree_main \ - test-betree_main-special \ test-bitwise \ test-constants \ test-demo \ diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst deleted file mode 100644 index b317dca4..00000000 --- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst +++ /dev/null @@ -1,117 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: templates for the decreases clauses *) -module BetreeMain.Clauses.Template -open Primitives -open BetreeMain.Types - -#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" - -(** [betree_main::betree::{betree_main::betree::List#1}::len]: decreases clause - Source: 'src/betree.rs', lines 276:4-276:24 *) -unfold -let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : nat = - admit () - -(** [betree_main::betree::{betree_main::betree::List#1}::split_at]: decreases clause - Source: 'src/betree.rs', lines 284:4-284:51 *) -unfold -let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t) - (n : u64) : nat = - admit () - -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause - Source: 'src/betree.rs', lines 339:4-339:73 *) -unfold -let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0) - (self : betree_List_t (u64 & t)) (pivot : u64) : nat = - admit () - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: decreases clause - Source: 'src/betree.rs', lines 789:4-792:34 *) -unfold -let betree_Node_lookup_first_message_for_key_decreases (key : u64) - (msgs : betree_List_t (u64 & betree_Message_t)) : nat = - admit () - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: decreases clause - Source: 'src/betree.rs', lines 636:4-636:80 *) -unfold -let betree_Node_lookup_in_bindings_decreases (key : u64) - (bindings : betree_List_t (u64 & u64)) : nat = - admit () - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: decreases clause - Source: 'src/betree.rs', lines 819:4-819:90 *) -unfold -let betree_Node_apply_upserts_decreases - (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) - (key : u64) : nat = - admit () - -(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause - Source: 'src/betree.rs', lines 395:4-395:63 *) -unfold -let betree_Internal_lookup_in_children_decreases (self : betree_Internal_t) - (key : u64) (st : state) : nat = - admit () - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: decreases clause - Source: 'src/betree.rs', lines 709:4-709:58 *) -unfold -let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64) - (st : state) : nat = - admit () - -(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: decreases clause - Source: 'src/betree.rs', lines 674:4-674:77 *) -unfold -let betree_Node_filter_messages_for_key_decreases (key : u64) - (msgs : betree_List_t (u64 & betree_Message_t)) : nat = - admit () - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: decreases clause - Source: 'src/betree.rs', lines 689:4-692:34 *) -unfold -let betree_Node_lookup_first_message_after_key_decreases (key : u64) - (msgs : betree_List_t (u64 & betree_Message_t)) : nat = - admit () - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: decreases clause - Source: 'src/betree.rs', lines 502:4-505:5 *) -unfold -let betree_Node_apply_messages_to_internal_decreases - (msgs : betree_List_t (u64 & betree_Message_t)) - (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat = - admit () - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: decreases clause - Source: 'src/betree.rs', lines 653:4-656:32 *) -unfold -let betree_Node_lookup_mut_in_bindings_decreases (key : u64) - (bindings : betree_List_t (u64 & u64)) : nat = - admit () - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: decreases clause - Source: 'src/betree.rs', lines 444:4-447:5 *) -unfold -let betree_Node_apply_messages_to_leaf_decreases - (bindings : betree_List_t (u64 & u64)) - (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat = - admit () - -(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: decreases clause - Source: 'src/betree.rs', lines 410:4-415:26 *) -unfold -let betree_Internal_flush_decreases (self : betree_Internal_t) - (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) - (content : betree_List_t (u64 & betree_Message_t)) (st : state) : nat = - admit () - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: decreases clause - Source: 'src/betree.rs', lines 588:4-593:5 *) -unfold -let betree_Node_apply_messages_decreases (self : betree_Node_t) - (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) - (msgs : betree_List_t (u64 & betree_Message_t)) (st : state) : nat = - admit () - diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst deleted file mode 100644 index b95d4c7e..00000000 --- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst +++ /dev/null @@ -1,210 +0,0 @@ -(** [betree_main]: templates for the decreases clauses *) -module BetreeMain.Clauses -open Primitives -open BetreeMain.Types - -#set-options "--z3rlimit 50 --fuel 0 --ifuel 1" - -(*** Well-founded relations *) - -(* We had a few issues when proving termination of the mutually recursive functions: - * - betree_Internal_flush - * - betree_Node_apply_messages - * - * The quantity which effectively decreases is: - * (betree_size, messages_length) - * where messages_length is 0 when there are no messages - * (and where we use the lexicographic ordering, of course) - * - * However, the `%[...]` and `{:well-founded ...} notations are not available outside - * of `decrease` clauses. - * - * We thus resorted to writing and proving correct a well-founded relation over - * pairs of natural numbers. The trick is that `<<` can be used outside of decrease - * clauses, and can be used to trigger SMT patterns. - * - * What follows is adapted from: - * https://www.fstar-lang.org/tutorial/book/part2/part2_well_founded.html - * - * Also, the following PR might make things easier: - * https://github.com/FStarLang/FStar/pull/2561 - *) - -module P = FStar.Preorder -module W = FStar.WellFounded -module L = FStar.LexicographicOrdering - -let lt_nat (x y:nat) : Type = x < y == true -let rec wf_lt_nat (x:nat) - : W.acc lt_nat x - = W.AccIntro (fun y _ -> wf_lt_nat y) - -// A type abbreviation for a pair of nats -let nat_pair = (x:nat & nat) - -// Making a lexicographic ordering from a pair of nat ordering -let lex_order_nat_pair : P.relation nat_pair = - L.lex_t lt_nat (fun _ -> lt_nat) - -// The lex order on nat pairs is well-founded, using our general proof -// of lexicographic composition of well-founded orders -let lex_order_nat_pair_wf : W.well_founded lex_order_nat_pair = - L.lex_t_wf wf_lt_nat (fun _ -> wf_lt_nat) - -// A utility to introduce lt_nat -let mk_lt_nat (x:nat) (y:nat { x < y }) : lt_nat x y = - let _ : equals (x < y) true = Refl in - () - -// A utility to make a lex ordering of nat pairs -let mk_lex_order_nat_pair (xy0:nat_pair) - (xy1:nat_pair { - let (|x0, y0|) = xy0 in - let (|x1, y1|) = xy1 in - x0 < x1 \/ (x0 == x1 /\ y0 < y1) - }) : lex_order_nat_pair xy0 xy1 = - let (|x0, y0|) = xy0 in - let (|x1, y1|) = xy1 in - if x0 < x1 then L.Left_lex x0 x1 y0 y1 (mk_lt_nat x0 x1) - else L.Right_lex x0 y0 y1 (mk_lt_nat y0 y1) - -let rec coerce #a #r #x (p:W.acc #a r x) : Tot (W.acc r x) (decreases p) = - W.AccIntro (fun y r -> coerce (p.access_smaller y r)) - -let coerce_wf #a #r (p: (x:a -> W.acc r x)) : x:a -> W.acc r x = - fun x -> coerce (p x) - -(* We need this axiom, which comes from the following discussion: - * https://github.com/FStarLang/FStar/issues/1916 - * An issue here is that the `{well-founded ... }` notation - *) -assume -val axiom_well_founded (a : Type) (rel : a -> a -> Type0) - (rwf : W.well_founded #a rel) (x y : a) : - Lemma (requires (rel x y)) (ensures (x << y)) - -(* This lemma has a pattern (which makes it work) *) -let wf_nat_pair_lem (p0 p1 : nat_pair) : - Lemma - (requires ( - let (|x0, y0|) = p0 in - let (|x1, y1|) = p1 in - x0 < x1 || (x0 = x1 && y0 < y1))) - (ensures (p0 << p1)) - [SMTPat (p0 << p1)] = - let rel = lex_order_nat_pair in - let rel_wf = lex_order_nat_pair_wf in - let _ = mk_lex_order_nat_pair p0 p1 in - assert(rel p0 p1); - axiom_well_founded nat_pair rel rel_wf p0 p1 - -(*** Decrease clauses *) -/// "Standard" decrease clauses - -(** [betree_main::betree::List::{1}::len]: decreases clause *) -unfold -let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : betree_List_t t = - self - -(** [betree_main::betree::List::{1}::split_at]: decreases clause *) -unfold -let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t) - (n : u64) : nat = - n - -(** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *) -unfold -let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0) - (self : betree_List_t (u64 & t)) (pivot : u64) : betree_List_t (u64 & t) = - self - -(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *) -unfold -let betree_Node_lookup_in_bindings_decreases (key : u64) - (bindings : betree_List_t (u64 & u64)) : betree_List_t (u64 & u64) = - bindings - -(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *) -unfold -let betree_Node_lookup_first_message_for_key_decreases (key : u64) - (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) = - msgs - -(** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *) -unfold -let betree_Node_apply_upserts_decreases - (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) - (key : u64) : betree_List_t (u64 & betree_Message_t) = - msgs - -(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *) -unfold -let betree_Internal_lookup_in_children_decreases (self : betree_Internal_t) - (key : u64) (st : state) : betree_Internal_t = - self - -(** [betree_main::betree::Node::{5}::lookup]: decreases clause *) -unfold -let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64) - (st : state) : betree_Node_t = - self - -(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *) -unfold -let betree_Node_lookup_mut_in_bindings_decreases (key : u64) - (bindings : betree_List_t (u64 & u64)) : betree_List_t (u64 & u64) = - bindings - -unfold -let betree_Node_apply_messages_to_leaf_decreases - (bindings : betree_List_t (u64 & u64)) - (new_msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) = - new_msgs - -(** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *) -unfold -let betree_Node_filter_messages_for_key_decreases (key : u64) - (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) = - msgs - -(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *) -unfold -let betree_Node_lookup_first_message_after_key_decreases (key : u64) - (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) = - msgs - -let betree_Node_apply_messages_to_internal_decreases - (msgs : betree_List_t (u64 & betree_Message_t)) - (new_msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) = - new_msgs - -(*** Decrease clauses - nat_pair *) -/// The following decrease clauses use the [nat_pair] definition and the well-founded -/// relation proven above. - -let rec betree_size (bt : betree_Node_t) : nat = - match bt with - | Betree_Node_Internal node -> 1 + betree_Internal_size node - | Betree_Node_Leaf _ -> 1 - -and betree_Internal_size (node : betree_Internal_t) : nat = - 1 + betree_size node.left + betree_size node.right - -let rec betree_List_len (#a : Type0) (ls : betree_List_t a) : nat = - match ls with - | Betree_List_Cons _ tl -> 1 + betree_List_len tl - | Betree_List_Nil -> 0 - -(** [betree_main::betree::Internal::{4}::flush]: decreases clause *) -unfold -let betree_Internal_flush_decreases (self : betree_Internal_t) - (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) - (content : betree_List_t (u64 & betree_Message_t)) (st : state) : nat_pair = - (|betree_Internal_size self, 0|) - -(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *) -unfold -let betree_Node_apply_messages_decreases (self : betree_Node_t) - (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) - (msgs : betree_List_t (u64 & betree_Message_t)) (st : state) : nat_pair = - (|betree_size self, betree_List_len msgs|) diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst deleted file mode 100644 index 9942ef68..00000000 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ /dev/null @@ -1,676 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: function definitions *) -module BetreeMain.Funs -open Primitives -include BetreeMain.Types -include BetreeMain.FunsExternal -include BetreeMain.Clauses - -#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" - -(** [betree_main::betree::load_internal_node]: - Source: 'src/betree.rs', lines 36:0-36:52 *) -let betree_load_internal_node - (id : u64) (st : state) : - result (state & (betree_List_t (u64 & betree_Message_t))) - = - betree_utils_load_internal_node id st - -(** [betree_main::betree::store_internal_node]: - Source: 'src/betree.rs', lines 41:0-41:60 *) -let betree_store_internal_node - (id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) : - result (state & unit) - = - betree_utils_store_internal_node id content st - -(** [betree_main::betree::load_leaf_node]: - Source: 'src/betree.rs', lines 46:0-46:44 *) -let betree_load_leaf_node - (id : u64) (st : state) : result (state & (betree_List_t (u64 & u64))) = - betree_utils_load_leaf_node id st - -(** [betree_main::betree::store_leaf_node]: - Source: 'src/betree.rs', lines 51:0-51:52 *) -let betree_store_leaf_node - (id : u64) (content : betree_List_t (u64 & u64)) (st : state) : - result (state & unit) - = - betree_utils_store_leaf_node id content st - -(** [betree_main::betree::fresh_node_id]: - Source: 'src/betree.rs', lines 55:0-55:48 *) -let betree_fresh_node_id (counter : u64) : result (u64 & u64) = - let* counter1 = u64_add counter 1 in Ok (counter, counter1) - -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: - Source: 'src/betree.rs', lines 206:4-206:20 *) -let betree_NodeIdCounter_new : result betree_NodeIdCounter_t = - Ok { next_node_id = 0 } - -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: - Source: 'src/betree.rs', lines 210:4-210:36 *) -let betree_NodeIdCounter_fresh_id - (self : betree_NodeIdCounter_t) : result (u64 & betree_NodeIdCounter_t) = - let* i = u64_add self.next_node_id 1 in - Ok (self.next_node_id, { next_node_id = i }) - -(** [betree_main::betree::upsert_update]: - Source: 'src/betree.rs', lines 234:0-234:70 *) -let betree_upsert_update - (prev : option u64) (st : betree_UpsertFunState_t) : result u64 = - begin match prev with - | None -> - begin match st with - | Betree_UpsertFunState_Add v -> Ok v - | Betree_UpsertFunState_Sub _ -> Ok 0 - end - | Some prev1 -> - begin match st with - | Betree_UpsertFunState_Add v -> - let* margin = u64_sub core_u64_max prev1 in - if margin >= v then u64_add prev1 v else Ok core_u64_max - | Betree_UpsertFunState_Sub v -> - if prev1 >= v then u64_sub prev1 v else Ok 0 - end - end - -(** [betree_main::betree::{betree_main::betree::List#1}::len]: - Source: 'src/betree.rs', lines 276:4-276:24 *) -let rec betree_List_len - (t : Type0) (self : betree_List_t t) : - Tot (result u64) (decreases (betree_List_len_decreases t self)) - = - begin match self with - | Betree_List_Cons _ tl -> let* i = betree_List_len t tl in u64_add 1 i - | Betree_List_Nil -> Ok 0 - end - -(** [betree_main::betree::{betree_main::betree::List#1}::split_at]: - Source: 'src/betree.rs', lines 284:4-284:51 *) -let rec betree_List_split_at - (t : Type0) (self : betree_List_t t) (n : u64) : - Tot (result ((betree_List_t t) & (betree_List_t t))) - (decreases (betree_List_split_at_decreases t self n)) - = - if n = 0 - then Ok (Betree_List_Nil, self) - else - begin match self with - | Betree_List_Cons hd tl -> - let* i = u64_sub n 1 in - let* p = betree_List_split_at t tl i in - let (ls0, ls1) = p in - Ok (Betree_List_Cons hd ls0, ls1) - | Betree_List_Nil -> Fail Failure - end - -(** [betree_main::betree::{betree_main::betree::List#1}::push_front]: - Source: 'src/betree.rs', lines 299:4-299:34 *) -let betree_List_push_front - (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) = - let (tl, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in - Ok (Betree_List_Cons x tl) - -(** [betree_main::betree::{betree_main::betree::List#1}::pop_front]: - Source: 'src/betree.rs', lines 306:4-306:32 *) -let betree_List_pop_front - (t : Type0) (self : betree_List_t t) : result (t & (betree_List_t t)) = - let (ls, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in - begin match ls with - | Betree_List_Cons x tl -> Ok (x, tl) - | Betree_List_Nil -> Fail Failure - end - -(** [betree_main::betree::{betree_main::betree::List#1}::hd]: - Source: 'src/betree.rs', lines 318:4-318:22 *) -let betree_List_hd (t : Type0) (self : betree_List_t t) : result t = - begin match self with - | Betree_List_Cons hd _ -> Ok hd - | Betree_List_Nil -> Fail Failure - end - -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: - Source: 'src/betree.rs', lines 327:4-327:44 *) -let betree_ListPairU64T_head_has_key - (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool = - begin match self with - | Betree_List_Cons hd _ -> let (i, _) = hd in Ok (i = key) - | Betree_List_Nil -> Ok false - end - -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: - Source: 'src/betree.rs', lines 339:4-339:73 *) -let rec betree_ListPairU64T_partition_at_pivot - (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : - Tot (result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t)))) - (decreases (betree_ListPairU64T_partition_at_pivot_decreases t self pivot)) - = - begin match self with - | Betree_List_Cons hd tl -> - let (i, x) = hd in - if i >= pivot - then Ok (Betree_List_Nil, Betree_List_Cons (i, x) tl) - else - let* p = betree_ListPairU64T_partition_at_pivot t tl pivot in - let (ls0, ls1) = p in - Ok (Betree_List_Cons (i, x) ls0, ls1) - | Betree_List_Nil -> Ok (Betree_List_Nil, Betree_List_Nil) - end - -(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: - Source: 'src/betree.rs', lines 359:4-364:17 *) -let betree_Leaf_split - (self : betree_Leaf_t) (content : betree_List_t (u64 & u64)) - (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) - (st : state) : - result (state & (betree_Internal_t & betree_NodeIdCounter_t)) - = - let* p = betree_List_split_at (u64 & u64) content params.split_size in - let (content0, content1) = p in - let* p1 = betree_List_hd (u64 & u64) content1 in - let (pivot, _) = p1 in - let* (id0, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in - let* (id1, node_id_cnt2) = betree_NodeIdCounter_fresh_id node_id_cnt1 in - let* (st1, _) = betree_store_leaf_node id0 content0 st in - let* (st2, _) = betree_store_leaf_node id1 content1 st1 in - let n = Betree_Node_Leaf { id = id0; size = params.split_size } in - let n1 = Betree_Node_Leaf { id = id1; size = params.split_size } in - Ok (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, - node_id_cnt2)) - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: - Source: 'src/betree.rs', lines 789:4-792:34 *) -let rec betree_Node_lookup_first_message_for_key - (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : - Tot (result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 & - betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t))))) - (decreases (betree_Node_lookup_first_message_for_key_decreases key msgs)) - = - begin match msgs with - | Betree_List_Cons x next_msgs -> - let (i, m) = x in - if i >= key - then Ok (Betree_List_Cons (i, m) next_msgs, Ok) - else - let* (l, lookup_first_message_for_key_back) = - betree_Node_lookup_first_message_for_key key next_msgs in - let back = - fun ret -> - let* next_msgs1 = lookup_first_message_for_key_back ret in - Ok (Betree_List_Cons (i, m) next_msgs1) in - Ok (l, back) - | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: - Source: 'src/betree.rs', lines 636:4-636:80 *) -let rec betree_Node_lookup_in_bindings - (key : u64) (bindings : betree_List_t (u64 & u64)) : - Tot (result (option u64)) - (decreases (betree_Node_lookup_in_bindings_decreases key bindings)) - = - begin match bindings with - | Betree_List_Cons hd tl -> - let (i, i1) = hd in - if i = key - then Ok (Some i1) - else if i > key then Ok None else betree_Node_lookup_in_bindings key tl - | Betree_List_Nil -> Ok None - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: - Source: 'src/betree.rs', lines 819:4-819:90 *) -let rec betree_Node_apply_upserts - (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64) - (key : u64) : - Tot (result (u64 & (betree_List_t (u64 & betree_Message_t)))) - (decreases (betree_Node_apply_upserts_decreases msgs prev key)) - = - let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in - if b - then - let* (msg, msgs1) = betree_List_pop_front (u64 & betree_Message_t) msgs in - let (_, m) = msg in - begin match m with - | Betree_Message_Insert _ -> Fail Failure - | Betree_Message_Delete -> Fail Failure - | Betree_Message_Upsert s -> - let* v = betree_upsert_update prev s in - betree_Node_apply_upserts msgs1 (Some v) key - end - else - let* v = core_option_Option_unwrap u64 prev in - let* msgs1 = - betree_List_push_front (u64 & betree_Message_t) msgs (key, - Betree_Message_Insert v) in - Ok (v, msgs1) - -(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: - Source: 'src/betree.rs', lines 395:4-395:63 *) -let rec betree_Internal_lookup_in_children - (self : betree_Internal_t) (key : u64) (st : state) : - Tot (result (state & ((option u64) & betree_Internal_t))) - (decreases (betree_Internal_lookup_in_children_decreases self key st)) - = - if key < self.pivot - then - let* (st1, (o, n)) = betree_Node_lookup self.left key st in - Ok (st1, (o, { self with left = n })) - else - let* (st1, (o, n)) = betree_Node_lookup self.right key st in - Ok (st1, (o, { self with right = n })) - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: - Source: 'src/betree.rs', lines 709:4-709:58 *) -and betree_Node_lookup - (self : betree_Node_t) (key : u64) (st : state) : - Tot (result (state & ((option u64) & betree_Node_t))) - (decreases (betree_Node_lookup_decreases self key st)) - = - begin match self with - | Betree_Node_Internal node -> - let* (st1, msgs) = betree_load_internal_node node.id st in - let* (pending, lookup_first_message_for_key_back) = - betree_Node_lookup_first_message_for_key key msgs in - begin match pending with - | Betree_List_Cons p l -> - let (k, msg) = p in - if k <> key - then - let* (st2, (o, node1)) = - betree_Internal_lookup_in_children node key st1 in - let* _ = - lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l) in - Ok (st2, (o, Betree_Node_Internal node1)) - else - begin match msg with - | Betree_Message_Insert v -> - let* _ = - lookup_first_message_for_key_back (Betree_List_Cons (k, - Betree_Message_Insert v) l) in - Ok (st1, (Some v, Betree_Node_Internal node)) - | Betree_Message_Delete -> - let* _ = - lookup_first_message_for_key_back (Betree_List_Cons (k, - Betree_Message_Delete) l) in - Ok (st1, (None, Betree_Node_Internal node)) - | Betree_Message_Upsert ufs -> - let* (st2, (v, node1)) = - betree_Internal_lookup_in_children node key st1 in - let* (v1, pending1) = - betree_Node_apply_upserts (Betree_List_Cons (k, - Betree_Message_Upsert ufs) l) v key in - let* msgs1 = lookup_first_message_for_key_back pending1 in - let* (st3, _) = betree_store_internal_node node1.id msgs1 st2 in - Ok (st3, (Some v1, Betree_Node_Internal node1)) - end - | Betree_List_Nil -> - let* (st2, (o, node1)) = betree_Internal_lookup_in_children node key st1 - in - let* _ = lookup_first_message_for_key_back Betree_List_Nil in - Ok (st2, (o, Betree_Node_Internal node1)) - end - | Betree_Node_Leaf node -> - let* (st1, bindings) = betree_load_leaf_node node.id st in - let* o = betree_Node_lookup_in_bindings key bindings in - Ok (st1, (o, Betree_Node_Leaf node)) - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: - Source: 'src/betree.rs', lines 674:4-674:77 *) -let rec betree_Node_filter_messages_for_key - (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : - Tot (result (betree_List_t (u64 & betree_Message_t))) - (decreases (betree_Node_filter_messages_for_key_decreases key msgs)) - = - begin match msgs with - | Betree_List_Cons p l -> - let (k, m) = p in - if k = key - then - let* (_, msgs1) = - betree_List_pop_front (u64 & betree_Message_t) (Betree_List_Cons (k, m) - l) in - betree_Node_filter_messages_for_key key msgs1 - else Ok (Betree_List_Cons (k, m) l) - | Betree_List_Nil -> Ok Betree_List_Nil - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: - Source: 'src/betree.rs', lines 689:4-692:34 *) -let rec betree_Node_lookup_first_message_after_key - (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : - Tot (result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 & - betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t))))) - (decreases (betree_Node_lookup_first_message_after_key_decreases key msgs)) - = - begin match msgs with - | Betree_List_Cons p next_msgs -> - let (k, m) = p in - if k = key - then - let* (l, lookup_first_message_after_key_back) = - betree_Node_lookup_first_message_after_key key next_msgs in - let back = - fun ret -> - let* next_msgs1 = lookup_first_message_after_key_back ret in - Ok (Betree_List_Cons (k, m) next_msgs1) in - Ok (l, back) - else Ok (Betree_List_Cons (k, m) next_msgs, Ok) - | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: - Source: 'src/betree.rs', lines 521:4-521:89 *) -let betree_Node_apply_to_internal - (msgs : betree_List_t (u64 & betree_Message_t)) (key : u64) - (new_msg : betree_Message_t) : - result (betree_List_t (u64 & betree_Message_t)) - = - let* (msgs1, lookup_first_message_for_key_back) = - betree_Node_lookup_first_message_for_key key msgs in - let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs1 key in - if b - then - begin match new_msg with - | Betree_Message_Insert i -> - let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in - let* msgs3 = - betree_List_push_front (u64 & betree_Message_t) msgs2 (key, - Betree_Message_Insert i) in - lookup_first_message_for_key_back msgs3 - | Betree_Message_Delete -> - let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in - let* msgs3 = - betree_List_push_front (u64 & betree_Message_t) msgs2 (key, - Betree_Message_Delete) in - lookup_first_message_for_key_back msgs3 - | Betree_Message_Upsert s -> - let* p = betree_List_hd (u64 & betree_Message_t) msgs1 in - let (_, m) = p in - begin match m with - | Betree_Message_Insert prev -> - let* v = betree_upsert_update (Some prev) s in - let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1 - in - let* msgs3 = - betree_List_push_front (u64 & betree_Message_t) msgs2 (key, - Betree_Message_Insert v) in - lookup_first_message_for_key_back msgs3 - | Betree_Message_Delete -> - let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1 - in - let* v = betree_upsert_update None s in - let* msgs3 = - betree_List_push_front (u64 & betree_Message_t) msgs2 (key, - Betree_Message_Insert v) in - lookup_first_message_for_key_back msgs3 - | Betree_Message_Upsert _ -> - let* (msgs2, lookup_first_message_after_key_back) = - betree_Node_lookup_first_message_after_key key msgs1 in - let* msgs3 = - betree_List_push_front (u64 & betree_Message_t) msgs2 (key, - Betree_Message_Upsert s) in - let* msgs4 = lookup_first_message_after_key_back msgs3 in - lookup_first_message_for_key_back msgs4 - end - end - else - let* msgs2 = - betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in - lookup_first_message_for_key_back msgs2 - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: - Source: 'src/betree.rs', lines 502:4-505:5 *) -let rec betree_Node_apply_messages_to_internal - (msgs : betree_List_t (u64 & betree_Message_t)) - (new_msgs : betree_List_t (u64 & betree_Message_t)) : - Tot (result (betree_List_t (u64 & betree_Message_t))) - (decreases (betree_Node_apply_messages_to_internal_decreases msgs new_msgs)) - = - begin match new_msgs with - | Betree_List_Cons new_msg new_msgs_tl -> - let (i, m) = new_msg in - let* msgs1 = betree_Node_apply_to_internal msgs i m in - betree_Node_apply_messages_to_internal msgs1 new_msgs_tl - | Betree_List_Nil -> Ok msgs - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: - Source: 'src/betree.rs', lines 653:4-656:32 *) -let rec betree_Node_lookup_mut_in_bindings - (key : u64) (bindings : betree_List_t (u64 & u64)) : - Tot (result ((betree_List_t (u64 & u64)) & (betree_List_t (u64 & u64) -> - result (betree_List_t (u64 & u64))))) - (decreases (betree_Node_lookup_mut_in_bindings_decreases key bindings)) - = - begin match bindings with - | Betree_List_Cons hd tl -> - let (i, i1) = hd in - if i >= key - then Ok (Betree_List_Cons (i, i1) tl, Ok) - else - let* (l, lookup_mut_in_bindings_back) = - betree_Node_lookup_mut_in_bindings key tl in - let back = - fun ret -> - let* tl1 = lookup_mut_in_bindings_back ret in - Ok (Betree_List_Cons (i, i1) tl1) in - Ok (l, back) - | Betree_List_Nil -> Ok (Betree_List_Nil, Ok) - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: - Source: 'src/betree.rs', lines 460:4-460:87 *) -let betree_Node_apply_to_leaf - (bindings : betree_List_t (u64 & u64)) (key : u64) - (new_msg : betree_Message_t) : - result (betree_List_t (u64 & u64)) - = - let* (bindings1, lookup_mut_in_bindings_back) = - betree_Node_lookup_mut_in_bindings key bindings in - let* b = betree_ListPairU64T_head_has_key u64 bindings1 key in - if b - then - let* (hd, bindings2) = betree_List_pop_front (u64 & u64) bindings1 in - begin match new_msg with - | Betree_Message_Insert v -> - let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in - lookup_mut_in_bindings_back bindings3 - | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings2 - | Betree_Message_Upsert s -> - let (_, i) = hd in - let* v = betree_upsert_update (Some i) s in - let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in - lookup_mut_in_bindings_back bindings3 - end - else - begin match new_msg with - | Betree_Message_Insert v -> - let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in - lookup_mut_in_bindings_back bindings2 - | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings1 - | Betree_Message_Upsert s -> - let* v = betree_upsert_update None s in - let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in - lookup_mut_in_bindings_back bindings2 - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: - Source: 'src/betree.rs', lines 444:4-447:5 *) -let rec betree_Node_apply_messages_to_leaf - (bindings : betree_List_t (u64 & u64)) - (new_msgs : betree_List_t (u64 & betree_Message_t)) : - Tot (result (betree_List_t (u64 & u64))) - (decreases (betree_Node_apply_messages_to_leaf_decreases bindings new_msgs)) - = - begin match new_msgs with - | Betree_List_Cons new_msg new_msgs_tl -> - let (i, m) = new_msg in - let* bindings1 = betree_Node_apply_to_leaf bindings i m in - betree_Node_apply_messages_to_leaf bindings1 new_msgs_tl - | Betree_List_Nil -> Ok bindings - end - -(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: - Source: 'src/betree.rs', lines 410:4-415:26 *) -let rec betree_Internal_flush - (self : betree_Internal_t) (params : betree_Params_t) - (node_id_cnt : betree_NodeIdCounter_t) - (content : betree_List_t (u64 & betree_Message_t)) (st : state) : - Tot (result (state & ((betree_List_t (u64 & betree_Message_t)) & - (betree_Internal_t & betree_NodeIdCounter_t)))) - (decreases ( - betree_Internal_flush_decreases self params node_id_cnt content st)) - = - let* p = - betree_ListPairU64T_partition_at_pivot betree_Message_t content self.pivot - in - let (msgs_left, msgs_right) = p in - let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in - if len_left >= params.min_flush_size - then - let* (st1, p1) = - betree_Node_apply_messages self.left params node_id_cnt msgs_left st in - let (n, node_id_cnt1) = p1 in - let* len_right = betree_List_len (u64 & betree_Message_t) msgs_right in - if len_right >= params.min_flush_size - then - let* (st2, p2) = - betree_Node_apply_messages self.right params node_id_cnt1 msgs_right - st1 in - let (n1, node_id_cnt2) = p2 in - Ok (st2, (Betree_List_Nil, ({ self with left = n; right = n1 }, - node_id_cnt2))) - else Ok (st1, (msgs_right, ({ self with left = n }, node_id_cnt1))) - else - let* (st1, p1) = - betree_Node_apply_messages self.right params node_id_cnt msgs_right st in - let (n, node_id_cnt1) = p1 in - Ok (st1, (msgs_left, ({ self with right = n }, node_id_cnt1))) - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: - Source: 'src/betree.rs', lines 588:4-593:5 *) -and betree_Node_apply_messages - (self : betree_Node_t) (params : betree_Params_t) - (node_id_cnt : betree_NodeIdCounter_t) - (msgs : betree_List_t (u64 & betree_Message_t)) (st : state) : - Tot (result (state & (betree_Node_t & betree_NodeIdCounter_t))) - (decreases ( - betree_Node_apply_messages_decreases self params node_id_cnt msgs st)) - = - begin match self with - | Betree_Node_Internal node -> - let* (st1, content) = betree_load_internal_node node.id st in - let* content1 = betree_Node_apply_messages_to_internal content msgs in - let* num_msgs = betree_List_len (u64 & betree_Message_t) content1 in - if num_msgs >= params.min_flush_size - then - let* (st2, (content2, p)) = - betree_Internal_flush node params node_id_cnt content1 st1 in - let (node1, node_id_cnt1) = p in - let* (st3, _) = betree_store_internal_node node1.id content2 st2 in - Ok (st3, (Betree_Node_Internal node1, node_id_cnt1)) - else - let* (st2, _) = betree_store_internal_node node.id content1 st1 in - Ok (st2, (Betree_Node_Internal node, node_id_cnt)) - | Betree_Node_Leaf node -> - let* (st1, content) = betree_load_leaf_node node.id st in - let* content1 = betree_Node_apply_messages_to_leaf content msgs in - let* len = betree_List_len (u64 & u64) content1 in - let* i = u64_mul 2 params.split_size in - if len >= i - then - let* (st2, (new_node, node_id_cnt1)) = - betree_Leaf_split node content1 params node_id_cnt st1 in - let* (st3, _) = betree_store_leaf_node node.id Betree_List_Nil st2 in - Ok (st3, (Betree_Node_Internal new_node, node_id_cnt1)) - else - let* (st2, _) = betree_store_leaf_node node.id content1 st1 in - Ok (st2, (Betree_Node_Leaf { node with size = len }, node_id_cnt)) - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: - Source: 'src/betree.rs', lines 576:4-582:5 *) -let betree_Node_apply - (self : betree_Node_t) (params : betree_Params_t) - (node_id_cnt : betree_NodeIdCounter_t) (key : u64) - (new_msg : betree_Message_t) (st : state) : - result (state & (betree_Node_t & betree_NodeIdCounter_t)) - = - let* (st1, p) = - betree_Node_apply_messages self params node_id_cnt (Betree_List_Cons (key, - new_msg) Betree_List_Nil) st in - let (self1, node_id_cnt1) = p in - Ok (st1, (self1, node_id_cnt1)) - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: - Source: 'src/betree.rs', lines 849:4-849:60 *) -let betree_BeTree_new - (min_flush_size : u64) (split_size : u64) (st : state) : - result (state & betree_BeTree_t) - = - let* node_id_cnt = betree_NodeIdCounter_new in - let* (id, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in - let* (st1, _) = betree_store_leaf_node id Betree_List_Nil st in - Ok (st1, - { - params = { min_flush_size = min_flush_size; split_size = split_size }; - node_id_cnt = node_id_cnt1; - root = (Betree_Node_Leaf { id = id; size = 0 }) - }) - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: - Source: 'src/betree.rs', lines 868:4-868:47 *) -let betree_BeTree_apply - (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) : - result (state & betree_BeTree_t) - = - let* (st1, p) = - betree_Node_apply self.root self.params self.node_id_cnt key msg st in - let (n, nic) = p in - Ok (st1, { self with node_id_cnt = nic; root = n }) - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: - Source: 'src/betree.rs', lines 874:4-874:52 *) -let betree_BeTree_insert - (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : - result (state & betree_BeTree_t) - = - betree_BeTree_apply self key (Betree_Message_Insert value) st - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: - Source: 'src/betree.rs', lines 880:4-880:38 *) -let betree_BeTree_delete - (self : betree_BeTree_t) (key : u64) (st : state) : - result (state & betree_BeTree_t) - = - betree_BeTree_apply self key Betree_Message_Delete st - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: - Source: 'src/betree.rs', lines 886:4-886:59 *) -let betree_BeTree_upsert - (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t) - (st : state) : - result (state & betree_BeTree_t) - = - betree_BeTree_apply self key (Betree_Message_Upsert upd) st - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: - Source: 'src/betree.rs', lines 895:4-895:62 *) -let betree_BeTree_lookup - (self : betree_BeTree_t) (key : u64) (st : state) : - result (state & ((option u64) & betree_BeTree_t)) - = - let* (st1, (o, n)) = betree_Node_lookup self.root key st in - Ok (st1, (o, { self with root = n })) - -(** [betree_main::main]: - Source: 'src/main.rs', lines 4:0-4:9 *) -let main : result unit = - Ok () - -(** Unit test for [betree_main::main] *) -let _ = assert_norm (main = Ok ()) - diff --git a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti deleted file mode 100644 index 8be98acf..00000000 --- a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti +++ /dev/null @@ -1,30 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: external function declarations *) -module BetreeMain.FunsExternal -open Primitives -include BetreeMain.Types - -#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" - -(** [betree_main::betree_utils::load_internal_node]: - Source: 'src/betree_utils.rs', lines 98:0-98:63 *) -val betree_utils_load_internal_node - : u64 -> state -> result (state & (betree_List_t (u64 & betree_Message_t))) - -(** [betree_main::betree_utils::store_internal_node]: - Source: 'src/betree_utils.rs', lines 115:0-115:71 *) -val betree_utils_store_internal_node - : - u64 -> betree_List_t (u64 & betree_Message_t) -> state -> result (state & - unit) - -(** [betree_main::betree_utils::load_leaf_node]: - Source: 'src/betree_utils.rs', lines 132:0-132:55 *) -val betree_utils_load_leaf_node - : u64 -> state -> result (state & (betree_List_t (u64 & u64))) - -(** [betree_main::betree_utils::store_leaf_node]: - Source: 'src/betree_utils.rs', lines 145:0-145:63 *) -val betree_utils_store_leaf_node - : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit) - diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Types.fst b/tests/fstar/betree_back_stateful/BetreeMain.Types.fst deleted file mode 100644 index b87219b2..00000000 --- a/tests/fstar/betree_back_stateful/BetreeMain.Types.fst +++ /dev/null @@ -1,61 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: type definitions *) -module BetreeMain.Types -open Primitives -include BetreeMain.TypesExternal - -#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" - -(** [betree_main::betree::List] - Source: 'src/betree.rs', lines 17:0-17:23 *) -type betree_List_t (t : Type0) = -| Betree_List_Cons : t -> betree_List_t t -> betree_List_t t -| Betree_List_Nil : betree_List_t t - -(** [betree_main::betree::UpsertFunState] - Source: 'src/betree.rs', lines 63:0-63:23 *) -type betree_UpsertFunState_t = -| Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t -| Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t - -(** [betree_main::betree::Message] - Source: 'src/betree.rs', lines 69:0-69:23 *) -type betree_Message_t = -| Betree_Message_Insert : u64 -> betree_Message_t -| Betree_Message_Delete : betree_Message_t -| Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t - -(** [betree_main::betree::Leaf] - Source: 'src/betree.rs', lines 167:0-167:11 *) -type betree_Leaf_t = { id : u64; size : u64; } - -(** [betree_main::betree::Internal] - Source: 'src/betree.rs', lines 156:0-156:15 *) -type betree_Internal_t = -{ - id : u64; pivot : u64; left : betree_Node_t; right : betree_Node_t; -} - -(** [betree_main::betree::Node] - Source: 'src/betree.rs', lines 179:0-179:9 *) -and betree_Node_t = -| Betree_Node_Internal : betree_Internal_t -> betree_Node_t -| Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t - -(** [betree_main::betree::Params] - Source: 'src/betree.rs', lines 187:0-187:13 *) -type betree_Params_t = { min_flush_size : u64; split_size : u64; } - -(** [betree_main::betree::NodeIdCounter] - Source: 'src/betree.rs', lines 201:0-201:20 *) -type betree_NodeIdCounter_t = { next_node_id : u64; } - -(** [betree_main::betree::BeTree] - Source: 'src/betree.rs', lines 218:0-218:17 *) -type betree_BeTree_t = -{ - params : betree_Params_t; - node_id_cnt : betree_NodeIdCounter_t; - root : betree_Node_t; -} - diff --git a/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti b/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti deleted file mode 100644 index 1b2c53a6..00000000 --- a/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti +++ /dev/null @@ -1,10 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: external type declarations *) -module BetreeMain.TypesExternal -open Primitives - -#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" - -(** The state type used in the state-error monad *) -val state : Type0 - diff --git a/tests/fstar/betree_back_stateful/Makefile b/tests/fstar/betree_back_stateful/Makefile deleted file mode 100644 index fa7d1f36..00000000 --- a/tests/fstar/betree_back_stateful/Makefile +++ /dev/null @@ -1,49 +0,0 @@ -# This file was automatically generated - modify ../Makefile.template instead -INCLUDE_DIRS = . - -FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) - -FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints - -FSTAR_OPTIONS = $(FSTAR_HINTS) \ - --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ - --warn_error '+241@247+285-274' \ - -FSTAR_EXE ?= fstar.exe -FSTAR_NO_FLAGS = $(FSTAR_EXE) --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj - -FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS) - -# The F* roots are used to compute the dependency graph, and generate the .depend file -FSTAR_ROOTS ?= $(wildcard *.fst *.fsti) - -# Build all the files -all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS))) - -# This is the right way to ensure the .depend file always gets re-built. -ifeq (,$(filter %-in,$(MAKECMDGOALS))) -ifndef NODEPEND -ifndef MAKE_RESTARTS -.depend: .FORCE - $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@ - -.PHONY: .FORCE -.FORCE: -endif -endif - -include .depend -endif - -# For the interactive mode -%.fst-in %.fsti-in: - @echo $(FSTAR_OPTIONS) - -# Generete the .checked files in batch mode -%.checked: - $(FSTAR) $(FSTAR_OPTIONS) $< && \ - touch -c $@ - -.PHONY: clean -clean: - rm -f obj/* diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst deleted file mode 100644 index 9951ccc3..00000000 --- a/tests/fstar/betree_back_stateful/Primitives.fst +++ /dev/null @@ -1,929 +0,0 @@ -/// This file lists primitive and assumed functions and types -module Primitives -open FStar.Mul -open FStar.List.Tot - -#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" - -(*** Utilities *) -val list_update (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a) : - ls':list a{ - length ls' = length ls /\ - index ls' i == x - } -#push-options "--fuel 1" -let rec list_update #a ls i x = - match ls with - | x' :: ls -> if i = 0 then x :: ls else x' :: list_update ls (i-1) x -#pop-options - -(*** Result *) -type error : Type0 = -| Failure -| OutOfFuel - -type result (a : Type0) : Type0 = -| Ok : v:a -> result a -| Fail : e:error -> result a - -// Monadic return operator -unfold let return (#a : Type0) (x : a) : result a = Ok x - -// Monadic bind operator. -// Allows to use the notation: -// ``` -// let* x = y in -// ... -// ``` -unfold let (let*) (#a #b : Type0) (m: result a) - (f: (x:a) -> Pure (result b) (requires (m == Ok x)) (ensures fun _ -> True)) : - result b = - match m with - | Ok x -> f x - | Fail e -> Fail e - -// Monadic assert(...) -let massert (b:bool) : result unit = if b then Ok () else Fail Failure - -// Normalize and unwrap a successful result (used for globals). -let eval_global (#a : Type0) (x : result a{Ok? (normalize_term x)}) : a = Ok?.v x - -(*** Misc *) -type char = FStar.Char.char -type string = string - -let is_zero (n: nat) : bool = n = 0 -let decrease (n: nat{n > 0}) : nat = n - 1 - -let core_mem_replace (a : Type0) (x : a) (y : a) : a & a = (x, x) - -// We don't really use raw pointers for now -type mut_raw_ptr (t : Type0) = { v : t } -type const_raw_ptr (t : Type0) = { v : t } - -(*** Scalars *) -/// Rem.: most of the following code was partially generated - -assume val size_numbits : pos - -// TODO: we could use FStar.Int.int_t and FStar.UInt.int_t - -let isize_min : int = -9223372036854775808 // TODO: should be opaque -let isize_max : int = 9223372036854775807 // TODO: should be opaque -let i8_min : int = -128 -let i8_max : int = 127 -let i16_min : int = -32768 -let i16_max : int = 32767 -let i32_min : int = -2147483648 -let i32_max : int = 2147483647 -let i64_min : int = -9223372036854775808 -let i64_max : int = 9223372036854775807 -let i128_min : int = -170141183460469231731687303715884105728 -let i128_max : int = 170141183460469231731687303715884105727 -let usize_min : int = 0 -let usize_max : int = 4294967295 // TODO: should be opaque -let u8_min : int = 0 -let u8_max : int = 255 -let u16_min : int = 0 -let u16_max : int = 65535 -let u32_min : int = 0 -let u32_max : int = 4294967295 -let u64_min : int = 0 -let u64_max : int = 18446744073709551615 -let u128_min : int = 0 -let u128_max : int = 340282366920938463463374607431768211455 - -type scalar_ty = -| Isize -| I8 -| I16 -| I32 -| I64 -| I128 -| Usize -| U8 -| U16 -| U32 -| U64 -| U128 - -let is_unsigned = function - | Isize | I8 | I16 | I32 | I64 | I128 -> false - | Usize | U8 | U16 | U32 | U64 | U128 -> true - -let scalar_min (ty : scalar_ty) : int = - match ty with - | Isize -> isize_min - | I8 -> i8_min - | I16 -> i16_min - | I32 -> i32_min - | I64 -> i64_min - | I128 -> i128_min - | Usize -> usize_min - | U8 -> u8_min - | U16 -> u16_min - | U32 -> u32_min - | U64 -> u64_min - | U128 -> u128_min - -let scalar_max (ty : scalar_ty) : int = - match ty with - | Isize -> isize_max - | I8 -> i8_max - | I16 -> i16_max - | I32 -> i32_max - | I64 -> i64_max - | I128 -> i128_max - | Usize -> usize_max - | U8 -> u8_max - | U16 -> u16_max - | U32 -> u32_max - | U64 -> u64_max - | U128 -> u128_max - -type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty} - -let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) = - if scalar_min ty <= x && scalar_max ty >= x then Ok x else Fail Failure - -let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x) - -let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - if y <> 0 then mk_scalar ty (x / y) else Fail Failure - -/// The remainder operation -let int_rem (x : int) (y : int{y <> 0}) : int = - if x >= 0 then (x % y) else -(x % y) - -(* Checking consistency with Rust *) -let _ = assert_norm(int_rem 1 2 = 1) -let _ = assert_norm(int_rem (-1) 2 = -1) -let _ = assert_norm(int_rem 1 (-2) = 1) -let _ = assert_norm(int_rem (-1) (-2) = -1) - -let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure - -let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - mk_scalar ty (x + y) - -let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - mk_scalar ty (x - y) - -let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - mk_scalar ty (x * y) - -let scalar_xor (#ty : scalar_ty) - (x : scalar ty) (y : scalar ty) : scalar ty = - match ty with - | U8 -> FStar.UInt.logxor #8 x y - | U16 -> FStar.UInt.logxor #16 x y - | U32 -> FStar.UInt.logxor #32 x y - | U64 -> FStar.UInt.logxor #64 x y - | U128 -> FStar.UInt.logxor #128 x y - | Usize -> admit() // TODO - | I8 -> - // Encoding issues... - normalize_spec (FStar.Int.int_t 8); - normalize_spec (scalar I8); - FStar.Int.logxor #8 x y - | I16 -> - // Encoding issues... - normalize_spec (FStar.Int.int_t 16); - normalize_spec (scalar I16); - FStar.Int.logxor #16 x y - | I32 -> FStar.Int.logxor #32 x y - | I64 -> FStar.Int.logxor #64 x y - | I128 -> - // Encoding issues... - normalize_spec (FStar.Int.int_t 128); - normalize_spec (scalar I128); - FStar.Int.logxor #128 x y - | Isize -> admit() // TODO - -let scalar_or (#ty : scalar_ty) - (x : scalar ty) (y : scalar ty) : scalar ty = - match ty with - | U8 -> FStar.UInt.logor #8 x y - | U16 -> FStar.UInt.logor #16 x y - | U32 -> FStar.UInt.logor #32 x y - | U64 -> FStar.UInt.logor #64 x y - | U128 -> FStar.UInt.logor #128 x y - | Usize -> admit() // TODO - | I8 -> - // Encoding issues... - normalize_spec (FStar.Int.int_t 8); - normalize_spec (scalar I8); - FStar.Int.logor #8 x y - | I16 -> - // Encoding issues... - normalize_spec (FStar.Int.int_t 16); - normalize_spec (scalar I16); - FStar.Int.logor #16 x y - | I32 -> FStar.Int.logor #32 x y - | I64 -> FStar.Int.logor #64 x y - | I128 -> - // Encoding issues... - normalize_spec (FStar.Int.int_t 128); - normalize_spec (scalar I128); - FStar.Int.logor #128 x y - | Isize -> admit() // TODO - -let scalar_and (#ty : scalar_ty) - (x : scalar ty) (y : scalar ty) : scalar ty = - match ty with - | U8 -> FStar.UInt.logand #8 x y - | U16 -> FStar.UInt.logand #16 x y - | U32 -> FStar.UInt.logand #32 x y - | U64 -> FStar.UInt.logand #64 x y - | U128 -> FStar.UInt.logand #128 x y - | Usize -> admit() // TODO - | I8 -> - // Encoding issues... - normalize_spec (FStar.Int.int_t 8); - normalize_spec (scalar I8); - FStar.Int.logand #8 x y - | I16 -> - // Encoding issues... - normalize_spec (FStar.Int.int_t 16); - normalize_spec (scalar I16); - FStar.Int.logand #16 x y - | I32 -> FStar.Int.logand #32 x y - | I64 -> FStar.Int.logand #64 x y - | I128 -> - // Encoding issues... - normalize_spec (FStar.Int.int_t 128); - normalize_spec (scalar I128); - FStar.Int.logand #128 x y - | Isize -> admit() // TODO - -// Shift left -let scalar_shl (#ty0 #ty1 : scalar_ty) - (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) = - admit() - -// Shift right -let scalar_shr (#ty0 #ty1 : scalar_ty) - (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) = - admit() - -(** Cast an integer from a [src_ty] to a [tgt_ty] *) -// TODO: check the semantics of casts in Rust -let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = - mk_scalar tgt_ty x - -// This can't fail, but for now we make all casts faillible (easier for the translation) -let scalar_cast_bool (tgt_ty : scalar_ty) (x : bool) : result (scalar tgt_ty) = - mk_scalar tgt_ty (if x then 1 else 0) - -/// The scalar types -type isize : eqtype = scalar Isize -type i8 : eqtype = scalar I8 -type i16 : eqtype = scalar I16 -type i32 : eqtype = scalar I32 -type i64 : eqtype = scalar I64 -type i128 : eqtype = scalar I128 -type usize : eqtype = scalar Usize -type u8 : eqtype = scalar U8 -type u16 : eqtype = scalar U16 -type u32 : eqtype = scalar U32 -type u64 : eqtype = scalar U64 -type u128 : eqtype = scalar U128 - - -let core_isize_min : isize = isize_min -let core_isize_max : isize = isize_max -let core_i8_min : i8 = i8_min -let core_i8_max : i8 = i8_max -let core_i16_min : i16 = i16_min -let core_i16_max : i16 = i16_max -let core_i32_min : i32 = i32_min -let core_i32_max : i32 = i32_max -let core_i64_min : i64 = i64_min -let core_i64_max : i64 = i64_max -let core_i128_min : i128 = i128_min -let core_i128_max : i128 = i128_max - -let core_usize_min : usize = usize_min -let core_usize_max : usize = usize_max -let core_u8_min : u8 = u8_min -let core_u8_max : u8 = u8_max -let core_u16_min : u16 = u16_min -let core_u16_max : u16 = u16_max -let core_u32_min : u32 = u32_min -let core_u32_max : u32 = u32_max -let core_u64_min : u64 = u64_min -let core_u64_max : u64 = u64_max -let core_u128_min : u128 = u128_min -let core_u128_max : u128 = u128_max - -/// Negation -let isize_neg = scalar_neg #Isize -let i8_neg = scalar_neg #I8 -let i16_neg = scalar_neg #I16 -let i32_neg = scalar_neg #I32 -let i64_neg = scalar_neg #I64 -let i128_neg = scalar_neg #I128 - -/// Division -let isize_div = scalar_div #Isize -let i8_div = scalar_div #I8 -let i16_div = scalar_div #I16 -let i32_div = scalar_div #I32 -let i64_div = scalar_div #I64 -let i128_div = scalar_div #I128 -let usize_div = scalar_div #Usize -let u8_div = scalar_div #U8 -let u16_div = scalar_div #U16 -let u32_div = scalar_div #U32 -let u64_div = scalar_div #U64 -let u128_div = scalar_div #U128 - -/// Remainder -let isize_rem = scalar_rem #Isize -let i8_rem = scalar_rem #I8 -let i16_rem = scalar_rem #I16 -let i32_rem = scalar_rem #I32 -let i64_rem = scalar_rem #I64 -let i128_rem = scalar_rem #I128 -let usize_rem = scalar_rem #Usize -let u8_rem = scalar_rem #U8 -let u16_rem = scalar_rem #U16 -let u32_rem = scalar_rem #U32 -let u64_rem = scalar_rem #U64 -let u128_rem = scalar_rem #U128 - -/// Addition -let isize_add = scalar_add #Isize -let i8_add = scalar_add #I8 -let i16_add = scalar_add #I16 -let i32_add = scalar_add #I32 -let i64_add = scalar_add #I64 -let i128_add = scalar_add #I128 -let usize_add = scalar_add #Usize -let u8_add = scalar_add #U8 -let u16_add = scalar_add #U16 -let u32_add = scalar_add #U32 -let u64_add = scalar_add #U64 -let u128_add = scalar_add #U128 - -/// Subtraction -let isize_sub = scalar_sub #Isize -let i8_sub = scalar_sub #I8 -let i16_sub = scalar_sub #I16 -let i32_sub = scalar_sub #I32 -let i64_sub = scalar_sub #I64 -let i128_sub = scalar_sub #I128 -let usize_sub = scalar_sub #Usize -let u8_sub = scalar_sub #U8 -let u16_sub = scalar_sub #U16 -let u32_sub = scalar_sub #U32 -let u64_sub = scalar_sub #U64 -let u128_sub = scalar_sub #U128 - -/// Multiplication -let isize_mul = scalar_mul #Isize -let i8_mul = scalar_mul #I8 -let i16_mul = scalar_mul #I16 -let i32_mul = scalar_mul #I32 -let i64_mul = scalar_mul #I64 -let i128_mul = scalar_mul #I128 -let usize_mul = scalar_mul #Usize -let u8_mul = scalar_mul #U8 -let u16_mul = scalar_mul #U16 -let u32_mul = scalar_mul #U32 -let u64_mul = scalar_mul #U64 -let u128_mul = scalar_mul #U128 - -/// Xor -let u8_xor = scalar_xor #U8 -let u16_xor = scalar_xor #U16 -let u32_xor = scalar_xor #U32 -let u64_xor = scalar_xor #U64 -let u128_xor = scalar_xor #U128 -let usize_xor = scalar_xor #Usize -let i8_xor = scalar_xor #I8 -let i16_xor = scalar_xor #I16 -let i32_xor = scalar_xor #I32 -let i64_xor = scalar_xor #I64 -let i128_xor = scalar_xor #I128 -let isize_xor = scalar_xor #Isize - -/// Or -let u8_or = scalar_or #U8 -let u16_or = scalar_or #U16 -let u32_or = scalar_or #U32 -let u64_or = scalar_or #U64 -let u128_or = scalar_or #U128 -let usize_or = scalar_or #Usize -let i8_or = scalar_or #I8 -let i16_or = scalar_or #I16 -let i32_or = scalar_or #I32 -let i64_or = scalar_or #I64 -let i128_or = scalar_or #I128 -let isize_or = scalar_or #Isize - -/// And -let u8_and = scalar_and #U8 -let u16_and = scalar_and #U16 -let u32_and = scalar_and #U32 -let u64_and = scalar_and #U64 -let u128_and = scalar_and #U128 -let usize_and = scalar_and #Usize -let i8_and = scalar_and #I8 -let i16_and = scalar_and #I16 -let i32_and = scalar_and #I32 -let i64_and = scalar_and #I64 -let i128_and = scalar_and #I128 -let isize_and = scalar_and #Isize - -/// Shift left -let u8_shl #ty = scalar_shl #U8 #ty -let u16_shl #ty = scalar_shl #U16 #ty -let u32_shl #ty = scalar_shl #U32 #ty -let u64_shl #ty = scalar_shl #U64 #ty -let u128_shl #ty = scalar_shl #U128 #ty -let usize_shl #ty = scalar_shl #Usize #ty -let i8_shl #ty = scalar_shl #I8 #ty -let i16_shl #ty = scalar_shl #I16 #ty -let i32_shl #ty = scalar_shl #I32 #ty -let i64_shl #ty = scalar_shl #I64 #ty -let i128_shl #ty = scalar_shl #I128 #ty -let isize_shl #ty = scalar_shl #Isize #ty - -/// Shift right -let u8_shr #ty = scalar_shr #U8 #ty -let u16_shr #ty = scalar_shr #U16 #ty -let u32_shr #ty = scalar_shr #U32 #ty -let u64_shr #ty = scalar_shr #U64 #ty -let u128_shr #ty = scalar_shr #U128 #ty -let usize_shr #ty = scalar_shr #Usize #ty -let i8_shr #ty = scalar_shr #I8 #ty -let i16_shr #ty = scalar_shr #I16 #ty -let i32_shr #ty = scalar_shr #I32 #ty -let i64_shr #ty = scalar_shr #I64 #ty -let i128_shr #ty = scalar_shr #I128 #ty -let isize_shr #ty = scalar_shr #Isize #ty - -(*** core *) - -/// Trait declaration: [core::clone::Clone] -noeq type core_clone_Clone (self : Type0) = { - clone : self → result self -} - -let core_clone_impls_CloneBool_clone (b : bool) : bool = b - -let core_clone_CloneBool : core_clone_Clone bool = { - clone = fun b -> Ok (core_clone_impls_CloneBool_clone b) -} - -let core_clone_impls_CloneUsize_clone (x : usize) : usize = x -let core_clone_impls_CloneU8_clone (x : u8) : u8 = x -let core_clone_impls_CloneU16_clone (x : u16) : u16 = x -let core_clone_impls_CloneU32_clone (x : u32) : u32 = x -let core_clone_impls_CloneU64_clone (x : u64) : u64 = x -let core_clone_impls_CloneU128_clone (x : u128) : u128 = x - -let core_clone_impls_CloneIsize_clone (x : isize) : isize = x -let core_clone_impls_CloneI8_clone (x : i8) : i8 = x -let core_clone_impls_CloneI16_clone (x : i16) : i16 = x -let core_clone_impls_CloneI32_clone (x : i32) : i32 = x -let core_clone_impls_CloneI64_clone (x : i64) : i64 = x -let core_clone_impls_CloneI128_clone (x : i128) : i128 = x - -let core_clone_CloneUsize : core_clone_Clone usize = { - clone = fun x -> Ok (core_clone_impls_CloneUsize_clone x) -} - -let core_clone_CloneU8 : core_clone_Clone u8 = { - clone = fun x -> Ok (core_clone_impls_CloneU8_clone x) -} - -let core_clone_CloneU16 : core_clone_Clone u16 = { - clone = fun x -> Ok (core_clone_impls_CloneU16_clone x) -} - -let core_clone_CloneU32 : core_clone_Clone u32 = { - clone = fun x -> Ok (core_clone_impls_CloneU32_clone x) -} - -let core_clone_CloneU64 : core_clone_Clone u64 = { - clone = fun x -> Ok (core_clone_impls_CloneU64_clone x) -} - -let core_clone_CloneU128 : core_clone_Clone u128 = { - clone = fun x -> Ok (core_clone_impls_CloneU128_clone x) -} - -let core_clone_CloneIsize : core_clone_Clone isize = { - clone = fun x -> Ok (core_clone_impls_CloneIsize_clone x) -} - -let core_clone_CloneI8 : core_clone_Clone i8 = { - clone = fun x -> Ok (core_clone_impls_CloneI8_clone x) -} - -let core_clone_CloneI16 : core_clone_Clone i16 = { - clone = fun x -> Ok (core_clone_impls_CloneI16_clone x) -} - -let core_clone_CloneI32 : core_clone_Clone i32 = { - clone = fun x -> Ok (core_clone_impls_CloneI32_clone x) -} - -let core_clone_CloneI64 : core_clone_Clone i64 = { - clone = fun x -> Ok (core_clone_impls_CloneI64_clone x) -} - -let core_clone_CloneI128 : core_clone_Clone i128 = { - clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) -} - -(** [core::option::{core::option::Option}::unwrap] *) -let core_option_Option_unwrap (t : Type0) (x : option t) : result t = - match x with - | None -> Fail Failure - | Some x -> Ok x - -(*** core::ops *) - -// Trait declaration: [core::ops::index::Index] -noeq type core_ops_index_Index (self idx : Type0) = { - output : Type0; - index : self → idx → result output -} - -// Trait declaration: [core::ops::index::IndexMut] -noeq type core_ops_index_IndexMut (self idx : Type0) = { - indexInst : core_ops_index_Index self idx; - index_mut : self → idx → result (indexInst.output & (indexInst.output → result self)); -} - -// Trait declaration [core::ops::deref::Deref] -noeq type core_ops_deref_Deref (self : Type0) = { - target : Type0; - deref : self → result target; -} - -// Trait declaration [core::ops::deref::DerefMut] -noeq type core_ops_deref_DerefMut (self : Type0) = { - derefInst : core_ops_deref_Deref self; - deref_mut : self → result (derefInst.target & (derefInst.target → result self)); -} - -type core_ops_range_Range (a : Type0) = { - start : a; - end_ : a; -} - -(*** [alloc] *) - -let alloc_boxed_Box_deref (t : Type0) (x : t) : result t = Ok x -let alloc_boxed_Box_deref_mut (t : Type0) (x : t) : result (t & (t -> result t)) = - Ok (x, (fun x -> Ok x)) - -// Trait instance -let alloc_boxed_Box_coreopsDerefInst (self : Type0) : core_ops_deref_Deref self = { - target = self; - deref = alloc_boxed_Box_deref self; -} - -// Trait instance -let alloc_boxed_Box_coreopsDerefMutInst (self : Type0) : core_ops_deref_DerefMut self = { - derefInst = alloc_boxed_Box_coreopsDerefInst self; - deref_mut = alloc_boxed_Box_deref_mut self; -} - -(*** Array *) -type array (a : Type0) (n : usize) = s:list a{length s = n} - -// We tried putting the normalize_term condition as a refinement on the list -// but it didn't work. It works with the requires clause. -let mk_array (a : Type0) (n : usize) - (l : list a) : - Pure (array a n) - (requires (normalize_term(FStar.List.Tot.length l) = n)) - (ensures (fun _ -> True)) = - normalize_term_spec (FStar.List.Tot.length l); - l - -let array_index_usize (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = - if i < length x then Ok (index x i) - else Fail Failure - -let array_update_usize (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : - result (array a n) = - if i < length x then Ok (list_update x i nx) - else Fail Failure - -let array_index_mut_usize (a : Type0) (n : usize) (x : array a n) (i : usize) : - result (a & (a -> result (array a n))) = - match array_index_usize a n x i with - | Fail e -> Fail e - | Ok v -> - Ok (v, array_update_usize a n x i) - -(*** Slice *) -type slice (a : Type0) = s:list a{length s <= usize_max} - -let slice_len (a : Type0) (s : slice a) : usize = length s - -let slice_index_usize (a : Type0) (x : slice a) (i : usize) : result a = - if i < length x then Ok (index x i) - else Fail Failure - -let slice_update_usize (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) = - if i < length x then Ok (list_update x i nx) - else Fail Failure - -let slice_index_mut_usize (a : Type0) (s : slice a) (i : usize) : - result (a & (a -> result (slice a))) = - match slice_index_usize a s i with - | Fail e -> Fail e - | Ok x -> - Ok (x, slice_update_usize a s i) - -(*** Subslices *) - -let array_to_slice (a : Type0) (n : usize) (x : array a n) : result (slice a) = Ok x -let array_from_slice (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) = - if length s = n then Ok s - else Fail Failure - -let array_to_slice_mut (a : Type0) (n : usize) (x : array a n) : - result (slice a & (slice a -> result (array a n))) = - Ok (x, array_from_slice a n x) - -// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *) -let array_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) : result (slice a) = - admit() - -let array_update_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) (ns : slice a) : result (array a n) = - admit() - -let array_repeat (a : Type0) (n : usize) (x : a) : array a n = - admit() - -let slice_subslice (a : Type0) (x : slice a) (r : core_ops_range_Range usize) : result (slice a) = - admit() - -let slice_update_subslice (a : Type0) (x : slice a) (r : core_ops_range_Range usize) (ns : slice a) : result (slice a) = - admit() - -(*** Vector *) -type alloc_vec_Vec (a : Type0) = v:list a{length v <= usize_max} - -let alloc_vec_Vec_new (a : Type0) : alloc_vec_Vec a = assert_norm(length #a [] == 0); [] -let alloc_vec_Vec_len (a : Type0) (v : alloc_vec_Vec a) : usize = length v - -// Helper -let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : result a = - if i < length v then Ok (index v i) else Fail Failure -// Helper -let alloc_vec_Vec_update_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) = - if i < length v then Ok (list_update v i x) else Fail Failure - -let alloc_vec_Vec_index_mut_usize (#a : Type0) (v: alloc_vec_Vec a) (i: usize) : - result (a & (a → result (alloc_vec_Vec a))) = - match alloc_vec_Vec_index_usize v i with - | Ok x -> - Ok (x, alloc_vec_Vec_update_usize v i) - | Fail e -> Fail e - -let alloc_vec_Vec_push (a : Type0) (v : alloc_vec_Vec a) (x : a) : - Pure (result (alloc_vec_Vec a)) - (requires True) - (ensures (fun res -> - match res with - | Fail e -> e == Failure - | Ok v' -> length v' = length v + 1)) = - if length v < usize_max then begin - (**) assert_norm(length [x] == 1); - (**) append_length v [x]; - (**) assert(length (append v [x]) = length v + 1); - Ok (append v [x]) - end - else Fail Failure - -let alloc_vec_Vec_insert (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) = - if i < length v then Ok (list_update v i x) else Fail Failure - -// Trait declaration: [core::slice::index::private_slice_index::Sealed] -type core_slice_index_private_slice_index_Sealed (self : Type0) = unit - -// Trait declaration: [core::slice::index::SliceIndex] -noeq type core_slice_index_SliceIndex (self t : Type0) = { - sealedInst : core_slice_index_private_slice_index_Sealed self; - output : Type0; - get : self → t → result (option output); - get_mut : self → t → result (option output & (option output -> result t)); - get_unchecked : self → const_raw_ptr t → result (const_raw_ptr output); - get_unchecked_mut : self → mut_raw_ptr t → result (mut_raw_ptr output); - index : self → t → result output; - index_mut : self → t → result (output & (output -> result t)); -} - -// [core::slice::index::[T]::index]: forward function -let core_slice_index_Slice_index - (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) - (s : slice t) (i : idx) : result inst.output = - let* x = inst.get i s in - match x with - | None -> Fail Failure - | Some x -> Ok x - -// [core::slice::index::Range:::get]: forward function -let core_slice_index_RangeUsize_get (t : Type0) (i : core_ops_range_Range usize) (s : slice t) : - result (option (slice t)) = - admit () // TODO - -// [core::slice::index::Range::get_mut]: forward function -let core_slice_index_RangeUsize_get_mut (t : Type0) : - core_ops_range_Range usize → slice t → result (option (slice t) & (option (slice t) -> result (slice t))) = - admit () // TODO - -// [core::slice::index::Range::get_unchecked]: forward function -let core_slice_index_RangeUsize_get_unchecked - (t : Type0) : - core_ops_range_Range usize → const_raw_ptr (slice t) → result (const_raw_ptr (slice t)) = - // Don't know what the model should be - for now we always fail to make - // sure code which uses it fails - fun _ _ -> Fail Failure - -// [core::slice::index::Range::get_unchecked_mut]: forward function -let core_slice_index_RangeUsize_get_unchecked_mut - (t : Type0) : - core_ops_range_Range usize → mut_raw_ptr (slice t) → result (mut_raw_ptr (slice t)) = - // Don't know what the model should be - for now we always fail to make - // sure code which uses it fails - fun _ _ -> Fail Failure - -// [core::slice::index::Range::index]: forward function -let core_slice_index_RangeUsize_index - (t : Type0) : core_ops_range_Range usize → slice t → result (slice t) = - admit () // TODO - -// [core::slice::index::Range::index_mut]: forward function -let core_slice_index_RangeUsize_index_mut (t : Type0) : - core_ops_range_Range usize → slice t → result (slice t & (slice t -> result (slice t))) = - admit () // TODO - -// [core::slice::index::[T]::index_mut]: forward function -let core_slice_index_Slice_index_mut - (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) : - slice t → idx → result (inst.output & (inst.output -> result (slice t))) = - admit () // - -// [core::array::[T; N]::index]: forward function -let core_array_Array_index - (t idx : Type0) (n : usize) (inst : core_ops_index_Index (slice t) idx) - (a : array t n) (i : idx) : result inst.output = - admit () // TODO - -// [core::array::[T; N]::index_mut]: forward function -let core_array_Array_index_mut - (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx) - (a : array t n) (i : idx) : - result (inst.indexInst.output & (inst.indexInst.output -> result (array t n))) = - admit () // TODO - -// Trait implementation: [core::slice::index::private_slice_index::Range] -let core_slice_index_private_slice_index_SealedRangeUsizeInst - : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) = () - -// Trait implementation: [core::slice::index::Range] -let core_slice_index_SliceIndexRangeUsizeSliceTInst (t : Type0) : - core_slice_index_SliceIndex (core_ops_range_Range usize) (slice t) = { - sealedInst = core_slice_index_private_slice_index_SealedRangeUsizeInst; - output = slice t; - get = core_slice_index_RangeUsize_get t; - get_mut = core_slice_index_RangeUsize_get_mut t; - get_unchecked = core_slice_index_RangeUsize_get_unchecked t; - get_unchecked_mut = core_slice_index_RangeUsize_get_unchecked_mut t; - index = core_slice_index_RangeUsize_index t; - index_mut = core_slice_index_RangeUsize_index_mut t; -} - -// Trait implementation: [core::slice::index::[T]] -let core_ops_index_IndexSliceTIInst (t idx : Type0) - (inst : core_slice_index_SliceIndex idx (slice t)) : - core_ops_index_Index (slice t) idx = { - output = inst.output; - index = core_slice_index_Slice_index t idx inst; -} - -// Trait implementation: [core::slice::index::[T]] -let core_ops_index_IndexMutSliceTIInst (t idx : Type0) - (inst : core_slice_index_SliceIndex idx (slice t)) : - core_ops_index_IndexMut (slice t) idx = { - indexInst = core_ops_index_IndexSliceTIInst t idx inst; - index_mut = core_slice_index_Slice_index_mut t idx inst; -} - -// Trait implementation: [core::array::[T; N]] -let core_ops_index_IndexArrayInst (t idx : Type0) (n : usize) - (inst : core_ops_index_Index (slice t) idx) : - core_ops_index_Index (array t n) idx = { - output = inst.output; - index = core_array_Array_index t idx n inst; -} - -// Trait implementation: [core::array::[T; N]] -let core_ops_index_IndexMutArrayIInst (t idx : Type0) (n : usize) - (inst : core_ops_index_IndexMut (slice t) idx) : - core_ops_index_IndexMut (array t n) idx = { - indexInst = core_ops_index_IndexArrayInst t idx n inst.indexInst; - index_mut = core_array_Array_index_mut t idx n inst; -} - -// [core::slice::index::usize::get]: forward function -let core_slice_index_usize_get - (t : Type0) : usize → slice t → result (option t) = - admit () // TODO - -// [core::slice::index::usize::get_mut]: forward function -let core_slice_index_usize_get_mut (t : Type0) : - usize → slice t → result (option t & (option t -> result (slice t))) = - admit () // TODO - -// [core::slice::index::usize::get_unchecked]: forward function -let core_slice_index_usize_get_unchecked - (t : Type0) : usize → const_raw_ptr (slice t) → result (const_raw_ptr t) = - admit () // TODO - -// [core::slice::index::usize::get_unchecked_mut]: forward function -let core_slice_index_usize_get_unchecked_mut - (t : Type0) : usize → mut_raw_ptr (slice t) → result (mut_raw_ptr t) = - admit () // TODO - -// [core::slice::index::usize::index]: forward function -let core_slice_index_usize_index (t : Type0) : usize → slice t → result t = - admit () // TODO - -// [core::slice::index::usize::index_mut]: forward function -let core_slice_index_usize_index_mut (t : Type0) : - usize → slice t → result (t & (t -> result (slice t))) = - admit () // TODO - -// Trait implementation: [core::slice::index::private_slice_index::usize] -let core_slice_index_private_slice_index_SealedUsizeInst - : core_slice_index_private_slice_index_Sealed usize = () - -// Trait implementation: [core::slice::index::usize] -let core_slice_index_SliceIndexUsizeSliceTInst (t : Type0) : - core_slice_index_SliceIndex usize (slice t) = { - sealedInst = core_slice_index_private_slice_index_SealedUsizeInst; - output = t; - get = core_slice_index_usize_get t; - get_mut = core_slice_index_usize_get_mut t; - get_unchecked = core_slice_index_usize_get_unchecked t; - get_unchecked_mut = core_slice_index_usize_get_unchecked_mut t; - index = core_slice_index_usize_index t; - index_mut = core_slice_index_usize_index_mut t; -} - -// [alloc::vec::Vec::index]: forward function -let alloc_vec_Vec_index (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) - (self : alloc_vec_Vec t) (i : idx) : result inst.output = - admit () // TODO - -// [alloc::vec::Vec::index_mut]: forward function -let alloc_vec_Vec_index_mut (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) - (self : alloc_vec_Vec t) (i : idx) : - result (inst.output & (inst.output -> result (alloc_vec_Vec t))) = - admit () // TODO - -// Trait implementation: [alloc::vec::Vec] -let alloc_vec_Vec_coreopsindexIndexInst (t idx : Type0) - (inst : core_slice_index_SliceIndex idx (slice t)) : - core_ops_index_Index (alloc_vec_Vec t) idx = { - output = inst.output; - index = alloc_vec_Vec_index t idx inst; -} - -// Trait implementation: [alloc::vec::Vec] -let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0) - (inst : core_slice_index_SliceIndex idx (slice t)) : - core_ops_index_IndexMut (alloc_vec_Vec t) idx = { - indexInst = alloc_vec_Vec_coreopsindexIndexInst t idx inst; - index_mut = alloc_vec_Vec_index_mut t idx inst; -} - -(*** Theorems *) - -let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : - Lemma ( - alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i == - alloc_vec_Vec_index_usize v i) - [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)] - = - admit() - -let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : - Lemma ( - alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i == - alloc_vec_Vec_index_mut_usize v i) - [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)] - = - admit() diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 52619c4a..d3fe8836 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -55,8 +55,8 @@ let test_options backend test_name = backend = "fstar" && match test_name with - | "arrays" | "betree_main" | "betree_main-special" | "hashmap" - | "hashmap_main" | "loops" | "traits" -> + | "arrays" | "betree_main" | "hashmap" | "hashmap_main" | "loops" | "traits" + -> true | _ -> false in @@ -68,10 +68,6 @@ let test_options backend test_name = let extra_options = match (backend, test_name) with - (* Additional, custom test on the betree: translate it without `-backward-no-state-update`. *) - (* This generates very ugly code, but is good to test the translation. *) - | _, "betree_main-special" -> - [ "-test-trans-units"; "-state"; "-split-files" ] | _, "betree_main" -> [ "-backward-no-state-update"; @@ -104,7 +100,6 @@ let test_subdir backend test_name = | "lean", _ -> "." | _, ("arrays" | "demo" | "hashmap" | "traits") -> test_name | _, "betree_main" -> "betree" - | _, "betree_main-special" -> "betree_back_stateful" | _, "hashmap_main" -> "hashmap_on_disk" | "hol4", _ -> "misc-" ^ test_name | ( _, @@ -119,24 +114,15 @@ let () = | _exe_path :: aeneas_path :: llbc_dir :: test_name :: options -> let tests_env = { aeneas_path; llbc_dir } in (* TODO: reactivate HOL4 once traits are parameterized by their associated types *) - let backends = - match test_name with - | "betree_main-special" -> [ "fstar" ] - | _ -> [ "coq"; "lean"; "fstar" ] - in + let backends = [ "coq"; "lean"; "fstar" ] in List.iter (fun backend -> let subdir = test_subdir backend test_name in let extra_aeneas_options = List.append (test_options backend test_name) options in - let test_file_name = - match test_name with - | "betree_main-special" -> "betree_main" - | _ -> test_name - in let test_case = - { name = test_file_name; backend; subdir; extra_aeneas_options } + { name = test_name; backend; subdir; extra_aeneas_options } in run_test tests_env test_case) backends -- cgit v1.3.1 From 4ce3e9c7c11744abae52d7a3ae1a3962395784be Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 10:41:10 +0200 Subject: Import test suite from charon --- Makefile | 152 +++-- flake.nix | 35 +- tests/.gitignore | 2 + tests/Makefile | 2 + tests/src/arrays.rs | 328 ++++++++++ tests/src/betree/Cargo.lock | 299 ++++++++++ tests/src/betree/Cargo.toml | 13 + tests/src/betree/Makefile | 11 + tests/src/betree/README.md | 1 + tests/src/betree/rust-toolchain | 3 + tests/src/betree/src/betree.rs | 1084 ++++++++++++++++++++++++++++++++++ tests/src/betree/src/betree_utils.rs | 155 +++++ tests/src/betree/src/main.rs | 4 + tests/src/bitwise.rs | 27 + tests/src/constants.rs | 96 +++ tests/src/demo.rs | 111 ++++ tests/src/external.rs | 11 + tests/src/hashmap.rs | 352 +++++++++++ tests/src/hashmap_main.rs | 16 + tests/src/hashmap_utils.rs | 12 + tests/src/loops.rs | 366 ++++++++++++ tests/src/nested_borrows.rs | 181 ++++++ tests/src/no_nested_borrows.rs | 491 +++++++++++++++ tests/src/paper.rs | 82 +++ tests/src/polonius_list.rs | 27 + tests/src/traits.rs | 341 +++++++++++ tests/test_runner/run_test.ml | 2 +- 27 files changed, 4148 insertions(+), 56 deletions(-) create mode 100644 tests/.gitignore create mode 100644 tests/src/arrays.rs create mode 100644 tests/src/betree/Cargo.lock create mode 100644 tests/src/betree/Cargo.toml create mode 100644 tests/src/betree/Makefile create mode 100644 tests/src/betree/README.md create mode 100644 tests/src/betree/rust-toolchain create mode 100644 tests/src/betree/src/betree.rs create mode 100644 tests/src/betree/src/betree_utils.rs create mode 100644 tests/src/betree/src/main.rs create mode 100644 tests/src/bitwise.rs create mode 100644 tests/src/constants.rs create mode 100644 tests/src/demo.rs create mode 100644 tests/src/external.rs create mode 100644 tests/src/hashmap.rs create mode 100644 tests/src/hashmap_main.rs create mode 100644 tests/src/hashmap_utils.rs create mode 100644 tests/src/loops.rs create mode 100644 tests/src/nested_borrows.rs create mode 100644 tests/src/no_nested_borrows.rs create mode 100644 tests/src/paper.rs create mode 100644 tests/src/polonius_list.rs create mode 100644 tests/src/traits.rs (limited to 'tests/test_runner') diff --git a/Makefile b/Makefile index dc38e56a..73f711a7 100644 --- a/Makefile +++ b/Makefile @@ -13,35 +13,31 @@ all: build-tests-verify nix # Variables customizable by the user #################################### -# Set this variable to any value to call Charon to regenerate the .llbc source -# files before running the tests -REGEN_LLBC ?= - -# The path to Charon -CHARON_HOME ?= ./charon - -# The path to the Aeneas executable to run the tests - we need the ability to -# change this path for the Nix package. -AENEAS_EXE ?= bin/aeneas - -# The path to our test runner. -TEST_RUNNER_EXE ?= bin/test_runner +# Paths to the executables we need for tests. They are overriden in CI. +AENEAS_EXE ?= $(PWD)/bin/aeneas +TEST_RUNNER_EXE ?= $(PWD)/bin/test_runner +CHARON_EXE ?= $(PWD)/charon/bin/charon # The user can specify additional translation options for Aeneas. -# By default we activate the (expensive) sanity checks. +# In CI we activate the (expensive) sanity checks. OPTIONS ?= +CHARON_OPTIONS ?= + +# The directory thta contains the rust source files for tests. +INPUTS_DIR ?= tests/src +# The directory where to look for the .llbc files. +LLBC_DIR ?= $(PWD)/tests/llbc -# The rules use (and update) the following variables -# -# The Charon test directory where to look for the .llbc files -CHARON_TEST_DIR ?= $(CHARON_HOME)/tests -# The options with which to call Charon -CHARON_OPTIONS = +# In CI, we enforce formatting and we don't regenerate llbc files. +IN_CI ?= #################################### # The rules #################################### +# Never remove intermediate files +.SECONDARY: + # Build the compiler, after formatting the code .PHONY: build build: format build-dev @@ -104,14 +100,51 @@ check-charon: setup-charon: @./scripts/check-charon-install.sh --force +ifdef IN_CI +# In CI, error if formatting is not done. +format: RUSTFMT_FLAGS := --check +endif + +# Reformat the project files +.PHONY: format +format: + @# `|| `true` because the command returns an error if it changed anything, which we don't care about. + cd compiler && dune fmt || true + cd tests/test_runner && dune fmt || true + rustfmt $(RUSTFMT_FLAGS) $(INPUTS_DIR)/*.rs + cd $(INPUTS_DIR)/betree && cargo fmt $(RUSTFMT_FLAGS) .PHONY: clean clean: clean-generated cd compiler && dune clean + cd $(INPUTS_DIR)/betree && $(MAKE) clean + +.PHONY: clean-generated +clean-generated: clean-generated-aeneas clean-generated-llbc + +.PHONY: clean-generated-aeneas +clean-generated-aeneas: + @# We can't put this line in `tests/Makefile` otherwise it will detect itself. + @# FIXME: generation of hol4 files is deactivated so we don't delete those. + @# `|| true` to avoid failing if there are no generated files present. + grep -lR 'THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS' tests | grep -v '^tests/hol4' | xargs rm || true + +.PHONY: clean-generated-llbc +clean-generated-llbc: + rm -rf $(LLBC_DIR) -# Test the project by translating test files to F* +# ============================================================================= +# The tests. +# ============================================================================= + +# Test the project by translating test files to various backends. .PHONY: test -test: build-dev test-all +test: build-dev test-all betree-tests + +# This runs the rust tests of the betree crate. +.PHONY: betree-tests +betree-tests: + cd $(INPUTS_DIR)/betree && $(MAKE) test .PHONY: test-all test-all: \ @@ -129,46 +162,65 @@ test-all: \ test-polonius_list \ test-traits -.PHONY: clean-generated -clean-generated: - # We can't put this line in `tests/Makefile` otherwise it will detect itself. - # FIXME: generation of hol4 files is deactivated so we don't delete those. - grep -lR 'THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS' tests | grep -v '^tests/hol4' | xargs rm - # Verify the F* files generated by the translation .PHONY: verify verify: cd tests && $(MAKE) all -# Reformat the project -.PHONY: format -format: - @# `|| `true` because the command returns an error if it changed anything, which we don't care about. - cd compiler && dune fmt || true - cd tests/test_runner && dune fmt || true - -# The commands to run Charon to generate the .llbc files -ifeq (, $(REGEN_LLBC)) -else -CHARON_CMD = cd $(CHARON_TEST_DIR) && $(MAKE) test-$* +ifdef IN_CI +# In CI we do extra sanity checks. +test-%: OPTIONS += -checks endif -# 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-% -gen-llbc-%: - $(CHARON_CMD) - # Translate the given llbc file to available backends. The test runner decides # which backends to use and sets test-specific options. .PHONY: test-% -test-%: FILE = $* -test-%: gen-llbc-% - $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(OPTIONS) +test-%: TEST_NAME = $* +test-%: $(LLBC_DIR)/%.llbc + $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(LLBC_DIR) $(TEST_NAME) $(OPTIONS) echo "# Test $* done" -# Nix - TODO: add the lean tests +# List the `.rs` files in `$(INPUTS_DIR)/` +INDIVIDUAL_RUST_SRCS = $(wildcard $(INPUTS_DIR)/*.rs) +# We test all rust files except this one. +INDIVIDUAL_RUST_SRCS := $(filter-out $(INPUTS_DIR)/hashmap_utils.rs, $(INDIVIDUAL_RUST_SRCS)) +# List the corresponding llbc files. +INDIVIDUAL_LLBCS := $(subst $(INPUTS_DIR)/,$(LLBC_DIR)/,$(patsubst %.rs,%.llbc,$(INDIVIDUAL_RUST_SRCS))) + +.PHONY: generate-llbc +# This depends on `llbc/.llbc` for each `$(INPUTS_DIR)/.rs` we care about, plus the whole-crate test. +generate-llbc: $(INDIVIDUAL_LLBCS) $(LLBC_DIR)/betree_main.llbc + +$(LLBC_DIR)/hashmap_main.llbc: CHARON_OPTIONS += --opaque=hashmap_utils +$(LLBC_DIR)/nested_borrows.llbc: CHARON_OPTIONS += --no-code-duplication +$(LLBC_DIR)/no_nested_borrows.llbc: CHARON_OPTIONS += --no-code-duplication +$(LLBC_DIR)/paper.llbc: CHARON_OPTIONS += --no-code-duplication +$(LLBC_DIR)/constants.llbc: CHARON_OPTIONS += --no-code-duplication +$(LLBC_DIR)/external.llbc: CHARON_OPTIONS += --no-code-duplication +$(LLBC_DIR)/polonius_list.llbc: CHARON_OPTIONS += --polonius +# Possible to add `--no-code-duplication` if we use the optimized MIR +$(LLBC_DIR)/betree_main.llbc: CHARON_OPTIONS += --polonius --opaque=betree_utils --crate betree_main + +ifndef IN_CI +$(LLBC_DIR)/%.llbc: check-charon + +$(LLBC_DIR)/%.llbc: + @# We do a `cd` dance to keep the exact same paths as before since that appears in the test outputs. + cd tests && $(CHARON_EXE) --no-cargo --input $(subst tests/,,$(INPUTS_DIR))/$*.rs --crate $* $(CHARON_OPTIONS) --dest $(LLBC_DIR) +# Special rule for the whole-crate test. +$(LLBC_DIR)/betree_main.llbc: + cd $(INPUTS_DIR)/betree && $(CHARON_EXE) $(CHARON_OPTIONS) --dest $(LLBC_DIR) +else +$(LLBC_DIR)/%.llbc: + @echo 'ERROR: llbc files should be built separately in CI' + @false +endif + + +# ============================================================================= +# Nix +# ============================================================================= +# TODO: add the lean tests .PHONY: nix nix: nix build && nix flake check diff --git a/flake.nix b/flake.nix index 7dd2b7c0..26689af0 100644 --- a/flake.nix +++ b/flake.nix @@ -80,6 +80,32 @@ OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors. }; + betree-llbc = charon.extractCrateWithCharon.${system} { + name = "betree"; + src = ./tests/src/betree; + charonFlags = "--polonius --opaque=betree_utils --crate betree_main"; + craneExtraArgs.checkPhaseCargoCommand = '' + cargo rustc -- --test -Zpolonius + ./target/debug/betree + ''; + }; + input-llbcs = pkgs.runCommand "input-llbcs" + { + src = ./tests/src; + makefile = ./Makefile; + buildInputs = [ charon.packages.${system}.rustToolchain charon.packages.${system}.charon ]; + } '' + # Copy the betree output file + mkdir -p $out + cp ${betree-llbc}/llbc/betree_main.llbc $out + + mkdir tests + cp -r $src tests/src + cp $makefile Makefile + # Generate the llbc files + CHARON_EXE="charon" INPUTS_DIR="tests/src" LLBC_DIR="$out" make generate-llbc + ''; + # Run the translation on various files. # Make sure we don't need to recompile the package whenever we make # unnecessary changes - we list the exact files and folders the package @@ -95,9 +121,7 @@ || pkgs.lib.hasPrefix (toString ./tests) path; }; buildPhase = '' - # We need to provide the paths to the Charon tests derivations - export CHARON_TEST_DIR=${charon.checks.${system}.tests} - + export LLBC_DIR=${input-llbcs} export AENEAS_EXE=${aeneas}/bin/aeneas export TEST_RUNNER_EXE=${test_runner}/bin/test_runner @@ -106,8 +130,8 @@ # Run the tests with extra sanity checks enabled # Remark: we could remove the file - make clean-generated - OPTIONS=-checks make test-all -j $NIX_BUILD_CORES + make clean-generated-aeneas + IN_CI=1 make test-all -j $NIX_BUILD_CORES # Check that there are no differences between the generated tests # and the original tests @@ -124,6 +148,7 @@ # something, otherwise Nix will consider the build has failed. installPhase = "touch $out"; }; + # Replay the F* proofs. aeneas-verify-fstar = pkgs.stdenv.mkDerivation { name = "aeneas_verify_fstar"; diff --git a/tests/.gitignore b/tests/.gitignore new file mode 100644 index 00000000..7eab4f57 --- /dev/null +++ b/tests/.gitignore @@ -0,0 +1,2 @@ +*.llbc +target/ diff --git a/tests/Makefile b/tests/Makefile index 8d40e8da..ff4baaba 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -1,4 +1,6 @@ +.PHONY: all all: test-fstar test-coq test-lean test-hol4 +.PHONY: test-% test-%: cd $* && $(MAKE) all diff --git a/tests/src/arrays.rs b/tests/src/arrays.rs new file mode 100644 index 00000000..1f094541 --- /dev/null +++ b/tests/src/arrays.rs @@ -0,0 +1,328 @@ +//! Exercise the translation of arrays, with features supported by Eurydice + +pub enum AB { + A, + B, +} + +pub fn incr(x: &mut u32) { + *x += 1; +} + +// Nano-tests +// ---------- + +// The suffix `_` prevents name collisions in some backends +pub fn array_to_shared_slice_(s: &[T; 32]) -> &[T] { + s +} + +// The suffix `_` prevents name collisions in some backends +pub fn array_to_mut_slice_(s: &mut [T; 32]) -> &mut [T] { + s +} + +pub fn array_len(s: [T; 32]) -> usize { + s.len() +} + +pub fn shared_array_len(s: &[T; 32]) -> usize { + s.len() +} + +pub fn shared_slice_len(s: &[T]) -> usize { + s.len() +} + +pub fn index_array_shared(s: &[T; 32], i: usize) -> &T { + &s[i] +} + +// Remark: can't move out of an array +// Also: can't move out of a slice. + +pub fn index_array_u32(s: [u32; 32], i: usize) -> u32 { + s[i] +} + +pub fn index_array_copy(x: &[u32; 32]) -> u32 { + x[0] +} + +pub fn index_mut_array(s: &mut [T; 32], i: usize) -> &mut T { + &mut s[i] +} + +pub fn index_slice(s: &[T], i: usize) -> &T { + &s[i] +} + +pub fn index_mut_slice(s: &mut [T], i: usize) -> &mut T { + &mut s[i] +} + +pub fn slice_subslice_shared_(x: &[u32], y: usize, z: usize) -> &[u32] { + &x[y..z] +} + +pub fn slice_subslice_mut_(x: &mut [u32], y: usize, z: usize) -> &mut [u32] { + &mut x[y..z] +} + +pub fn array_to_slice_shared_(x: &[u32; 32]) -> &[u32] { + x +} + +pub fn array_to_slice_mut_(x: &mut [u32; 32]) -> &mut [u32] { + x +} + +pub fn array_subslice_shared_(x: &[u32; 32], y: usize, z: usize) -> &[u32] { + &x[y..z] +} + +pub fn array_subslice_mut_(x: &mut [u32; 32], y: usize, z: usize) -> &mut [u32] { + &mut x[y..z] +} + +pub fn index_slice_0(s: &[T]) -> &T { + &s[0] +} + +pub fn index_array_0(s: &[T; 32]) -> &T { + &s[0] +} + +/* +// Unsupported by Aeneas for now +pub fn index_index_slice<'a, T>(s: &'a [&[T]], i: usize, j: usize) -> &'a T { + &s[i][j] +} +*/ + +pub fn index_index_array(s: [[u32; 32]; 32], i: usize, j: usize) -> u32 { + s[i][j] +} + +/* +// Unsupported by Aeneas for now +pub fn update_update_slice(s: &mut [&mut [u32]], i: usize, j: usize) { + s[i][j] = 0; +} +*/ + +pub fn update_update_array(mut s: [[u32; 32]; 32], i: usize, j: usize) { + s[i][j] = 0; +} + +pub fn array_local_deep_copy(x: &[u32; 32]) { + let _y = *x; +} + +pub fn take_array(_: [u32; 2]) {} +pub fn take_array_borrow(_: &[u32; 2]) {} +pub fn take_slice(_: &[u32]) {} +pub fn take_mut_slice(_: &mut [u32]) {} + +pub fn const_array() -> [u32; 2] { + [0, 0] +} + +pub fn const_slice() { + let _: &[u32] = &[0, 0]; +} + +/* +// This triggers a special case in the constant expressions +pub fn const_string() { + let _ = "hello"; +}*/ + +pub fn take_all() { + let mut x: [u32; 2] = [0, 0]; + // x is deep copied (copy node appears in Charon, followed by a move) + take_array(x); + take_array(x); + // x passed by address, there is a reborrow here + take_array_borrow(&x); + // automatic cast from array to slice (spanning entire array) + take_slice(&x); + // note that both appear as SliceNew expressions, meaning the SliceNew UnOp is overloaded for + // mut and non-mut cases + take_mut_slice(&mut x); +} + +pub fn index_array(x: [u32; 2]) -> u32 { + x[0] +} +pub fn index_array_borrow(x: &[u32; 2]) -> u32 { + x[0] +} + +pub fn index_slice_u32_0(x: &[u32]) -> u32 { + x[0] +} + +pub fn index_mut_slice_u32_0(x: &mut [u32]) -> u32 { + x[0] +} + +pub fn index_all() -> u32 { + let mut x: [u32; 2] = [0, 0]; + if true { + let _y: [u32; 2] = [0, 0]; + } else { + let _z: [u32; 1] = [0]; + } + index_array(x) + + index_array(x) + + index_array_borrow(&x) + + index_slice_u32_0(&x) + + index_mut_slice_u32_0(&mut x) +} + +pub fn update_array(mut x: [u32; 2]) { + x[0] = 1 +} +pub fn update_array_mut_borrow(x: &mut [u32; 2]) { + x[0] = 1 +} +pub fn update_mut_slice(x: &mut [u32]) { + x[0] = 1 +} + +pub fn update_all() { + let mut x: [u32; 2] = [0, 0]; + update_array(x); + update_array(x); + update_array_mut_borrow(&mut x); + update_mut_slice(&mut x); +} + +// Nano-tests, with ranges +// ----------------------- + +pub fn range_all() { + let mut x: [u32; 4] = [0, 0, 0, 0]; + // CONFIRM: there is no way to shrink [T;N] into [T;M] with M u32 { + let x: [u32; 2] = *x; + x[0] +} + +pub fn deref_array_mut_borrow(x: &mut [u32; 2]) -> u32 { + let x: [u32; 2] = *x; + x[0] +} + +// Non-copiable arrays +// ------------------- + +pub fn take_array_t(_: [AB; 2]) {} + +pub fn non_copyable_array() { + let x: [AB; 2] = [AB::A, AB::B]; + // x is moved (not deep copied!) + // TODO: determine whether the translation needs to be aware of that and pass by ref instead of by copy + take_array_t(x); + + // this fails, naturally: + // take_array_t(x); +} + +// Larger, random tests +// -------------------- + +pub fn sum(s: &[u32]) -> u32 { + let mut sum = 0; + let mut i = 0; + while i < s.len() { + sum += s[i]; + i += 1; + } + sum +} + +pub fn sum2(s: &[u32], s2: &[u32]) -> u32 { + let mut sum = 0; + assert!(s.len() == s2.len()); + let mut i = 0; + while i < s.len() { + sum += s[i] + s2[i]; + i += 1; + } + sum +} + +pub fn f0() { + let s: &mut [u32] = &mut [1, 2]; + s[0] = 1; +} + +pub fn f1() { + let mut s: [u32; 2] = [1, 2]; + s[0] = 1; +} + +pub fn f2(_: u32) {} + +pub fn f3() -> u32 { + let a: [u32; 2] = [1, 2]; + f2(a[0]); + let b = [0; 32]; + sum2(&a, f4(&b, 16, 18)) +} + +pub fn f4(x: &[u32; 32], y: usize, z: usize) -> &[u32] { + &x[y..z] +} + +pub const SZ: usize = 32; + +// There is something slightly annoying here: the SZ constant gets inlined +pub fn f5(x: &[u32; SZ]) -> u32 { + x[0] +} + +// To avoid lifetime shortening +pub fn ite() { + let mut x: [u32; 2] = [0, 0]; + if true { + let mut y: [u32; 2] = [0, 0]; + index_mut_slice_u32_0(&mut x); + index_mut_slice_u32_0(&mut y); + } +} + +pub fn zero_slice(a: &mut [u8]) { + let mut i: usize = 0; + let len = a.len(); + while i < len { + a[i] = 0; + i += 1; + } +} + +pub fn iter_mut_slice(a: &mut [u8]) { + let len = a.len(); + let mut i = 0; + while i < len { + i += 1; + } +} + +pub fn sum_mut_slice(a: &mut [u32]) -> u32 { + let mut i = 0; + let mut s = 0; + while i < a.len() { + s += a[i]; + i += 1; + } + s +} diff --git a/tests/src/betree/Cargo.lock b/tests/src/betree/Cargo.lock new file mode 100644 index 00000000..1bd274ad --- /dev/null +++ b/tests/src/betree/Cargo.lock @@ -0,0 +1,299 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "aho-corasick" +version = "1.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8e60d3430d3a69478ad0993f19238d2df97c507009a52b3c10addcd7f6bcb916" +dependencies = [ + "memchr", +] + +[[package]] +name = "atty" +version = "0.2.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8" +dependencies = [ + "hermit-abi", + "libc", + "winapi", +] + +[[package]] +name = "betree" +version = "0.1.0" +dependencies = [ + "env_logger", + "log", + "serde", + "serde_json", +] + +[[package]] +name = "env_logger" +version = "0.8.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a19187fea3ac7e84da7dacf48de0c45d63c6a76f9490dae389aead16c243fce3" +dependencies = [ + "atty", + "humantime", + "log", + "regex", + "termcolor", +] + +[[package]] +name = "hermit-abi" +version = "0.1.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33" +dependencies = [ + "libc", +] + +[[package]] +name = "humantime" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" + +[[package]] +name = "itoa" +version = "1.0.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" + +[[package]] +name = "libc" +version = "0.2.155" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "97b3888a4aecf77e811145cadf6eef5901f4782c53886191b2f693f24761847c" + +[[package]] +name = "log" +version = "0.4.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "90ed8c1e510134f979dbc4f070f87d4313098b704861a105fe34231c70a3901c" + +[[package]] +name = "memchr" +version = "2.7.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6c8640c5d730cb13ebd907d8d04b52f55ac9a2eec55b440c8892f40d56c76c1d" + +[[package]] +name = "proc-macro2" +version = "1.0.83" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b33eb56c327dec362a9e55b3ad14f9d2f0904fb5a5b03b513ab5465399e9f43" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.36" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fa76aaf39101c457836aec0ce2316dbdc3ab723cdda1c6bd4e6ad4208acaca7" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "regex" +version = "1.10.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c117dbdfde9c8308975b6a18d71f3f385c89461f7b3fb054288ecf2a2058ba4c" +dependencies = [ + "aho-corasick", + "memchr", + "regex-automata", + "regex-syntax", +] + +[[package]] +name = "regex-automata" +version = "0.4.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "86b83b8b9847f9bf95ef68afb0b8e6cdb80f498442f5179a29fad448fcc1eaea" +dependencies = [ + "aho-corasick", + "memchr", + "regex-syntax", +] + +[[package]] +name = "regex-syntax" +version = "0.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "adad44e29e4c806119491a7f06f03de4d1af22c3a680dd47f1e6e179439d1f56" + +[[package]] +name = "ryu" +version = "1.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f3cb5ba0dc43242ce17de99c180e96db90b235b8a9fdc9543c96d2209116bd9f" + +[[package]] +name = "serde" +version = "1.0.202" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "226b61a0d411b2ba5ff6d7f73a476ac4f8bb900373459cd00fab8512828ba395" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.202" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6048858004bcff69094cd972ed40a32500f153bd3be9f716b2eed2e8217c4838" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "serde_json" +version = "1.0.117" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "455182ea6142b14f93f4bc5320a2b31c1f266b66a4a5c858b013302a5d8cbfc3" +dependencies = [ + "itoa", + "ryu", + "serde", +] + +[[package]] +name = "syn" +version = "2.0.65" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d2863d96a84c6439701d7a38f9de935ec562c8832cc55d1dde0f513b52fad106" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "termcolor" +version = "1.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "06794f8f6c5c898b3275aebefa6b8a1cb24cd2c6c79397ab15774837a0bc5755" +dependencies = [ + "winapi-util", +] + +[[package]] +name = "unicode-ident" +version = "1.0.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b" + +[[package]] +name = "winapi" +version = "0.3.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419" +dependencies = [ + "winapi-i686-pc-windows-gnu", + "winapi-x86_64-pc-windows-gnu", +] + +[[package]] +name = "winapi-i686-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" + +[[package]] +name = "winapi-util" +version = "0.1.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4d4cc384e1e73b93bafa6fb4f1df8c41695c8a91cf9c4c64358067d15a7b6c6b" +dependencies = [ + "windows-sys", +] + +[[package]] +name = "winapi-x86_64-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" + +[[package]] +name = "windows-sys" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" +dependencies = [ + "windows-targets", +] + +[[package]] +name = "windows-targets" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6f0713a46559409d202e70e28227288446bf7841d3211583a4b53e3f6d96e7eb" +dependencies = [ + "windows_aarch64_gnullvm", + "windows_aarch64_msvc", + "windows_i686_gnu", + "windows_i686_gnullvm", + "windows_i686_msvc", + "windows_x86_64_gnu", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc", +] + +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7088eed71e8b8dda258ecc8bac5fb1153c5cffaf2578fc8ff5d61e23578d3263" + +[[package]] +name = "windows_aarch64_msvc" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9985fd1504e250c615ca5f281c3f7a6da76213ebd5ccc9561496568a2752afb6" + +[[package]] +name = "windows_i686_gnu" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "88ba073cf16d5372720ec942a8ccbf61626074c6d4dd2e745299726ce8b89670" + +[[package]] +name = "windows_i686_gnullvm" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "87f4261229030a858f36b459e748ae97545d6f1ec60e5e0d6a3d32e0dc232ee9" + +[[package]] +name = "windows_i686_msvc" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "db3c2bf3d13d5b658be73463284eaf12830ac9a26a90c717b7f771dfe97487bf" + +[[package]] +name = "windows_x86_64_gnu" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4e4246f76bdeff09eb48875a0fd3e2af6aada79d409d33011886d3e1581517d9" + +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "852298e482cd67c356ddd9570386e2862b5673c85bd5f88df9ab6802b334c596" + +[[package]] +name = "windows_x86_64_msvc" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bec47e5bfd1bff0eeaf6d8b485cc1074891a197ab4225d504cb7a1ab88b02bf0" diff --git a/tests/src/betree/Cargo.toml b/tests/src/betree/Cargo.toml new file mode 100644 index 00000000..c05c7d93 --- /dev/null +++ b/tests/src/betree/Cargo.toml @@ -0,0 +1,13 @@ +[package] +name = "betree" +version = "0.1.0" +authors = ["Son Ho "] +edition = "2018" + +[dependencies] +serde_json = "1.0.91" +serde = { version = "1.0.152", features = ["derive"] } +log = "0.4.17" +env_logger = "0.8.4" + +# TODO: If we turn this package into a library, building the tests fails. diff --git a/tests/src/betree/Makefile b/tests/src/betree/Makefile new file mode 100644 index 00000000..7b41e56d --- /dev/null +++ b/tests/src/betree/Makefile @@ -0,0 +1,11 @@ +.PHONY: all +all: tests + +.PHONY: test +test: + cargo rustc -- --test -Zpolonius + cd target/debug/ && ./betree + +.PHONY: clean +clean: + cargo clean diff --git a/tests/src/betree/README.md b/tests/src/betree/README.md new file mode 100644 index 00000000..a71fe884 --- /dev/null +++ b/tests/src/betree/README.md @@ -0,0 +1 @@ +This project contains tests which require the Polonius borrow checker. diff --git a/tests/src/betree/rust-toolchain b/tests/src/betree/rust-toolchain new file mode 100644 index 00000000..9460b1a8 --- /dev/null +++ b/tests/src/betree/rust-toolchain @@ -0,0 +1,3 @@ +[toolchain] +channel = "nightly-2023-06-02" +components = [ "rustc-dev", "llvm-tools-preview" ] diff --git a/tests/src/betree/src/betree.rs b/tests/src/betree/src/betree.rs new file mode 100644 index 00000000..12f2847d --- /dev/null +++ b/tests/src/betree/src/betree.rs @@ -0,0 +1,1084 @@ +//! The following module implements a minimal betree. +//! We don't have loops for now, so we will need to update the code to remove +//! the recursive functions at some point. +//! We drew a lot of inspiration from the C++ [Be-Tree](https://github.com/oscarlab/Be-Tree). +//! implementation. +#![allow(dead_code)] + +use crate::betree_utils as utils; + +pub type NodeId = u64; +pub type Key = u64; +pub type Value = u64; + +type Map = List<(K, V)>; + +/// We use linked lists for the maps from keys to messages/bindings +pub(crate) enum List { + Cons(T, Box>), + Nil, +} + +/// Every node has a unique identifier (the betree has a counter). +/// Whenever we need to read/update the content of a node, we read/update +/// the whole content from disk at once. +/// +/// In order to make things simple, the content of each node is saved in +/// a single file, identified by the node index. Also, we use json. +/// +/// We don't reason about the content of the load/store node functions +/// (which are assumed), while the purpose of this example is to illustrate the +/// proof experience we have with Aeneas: we are not looking for performance here. +/// +/// Rk.: in the future, we will directly use the functions from betree_utils +/// and setup the translation to consider this module as assumed (i.e., no +/// wrappers) +fn load_internal_node(id: NodeId) -> InternalContent { + utils::load_internal_node(id) +} + +/// See [load_internal_node]. +fn store_internal_node(id: NodeId, content: InternalContent) { + utils::store_internal_node(id, content) +} + +/// See [load_internal_node]. +fn load_leaf_node(id: NodeId) -> LeafContent { + utils::load_leaf_node(id) +} + +/// See [load_internal_node]. +fn store_leaf_node(id: NodeId, content: LeafContent) { + utils::store_leaf_node(id, content) +} + +fn fresh_node_id(counter: &mut NodeId) -> NodeId { + let id = *counter; + *counter += 1; + id +} + +/// We use this type to encode closures. +/// See [Message::Upsert] and [upsert_update] +pub enum UpsertFunState { + Add(u64), + Sub(u64), +} + +/// A message - note that all those messages have to be linked to a key +pub(crate) enum Message { + /// Insert a binding from value to key + Insert(Value), + /// Delete a binding from value to key + Delete, + /// [Upsert] is "query then update" (query a value, then update the binding + /// by using the result of the query). This is pretty expensive if we + /// actually *do* query, *then* update: queries are expensive, because + /// we potentially have to explore the tree in depth (and every time we + /// lookup a node, we have an expensive I/O operation). + /// Instead, we insert this [Upsert] message in the tree, which progressively + /// gets propagated to the children untils it gets applied (when we find an + /// [Insert], or when we reach a leaf). + /// + /// In practice, [Upsert] should store a closure. For now we don't have + /// support for function pointers and closures, so [Upsert] doesn't store + /// a closure and always applies the same update function. Note that the + /// [Value] stored in [Upsert] acts as a closure's state. + /// + /// The interest of this example is to split the proof in two: + /// 1. a very simple refinement proof (which is made simple by the fact that + /// Aeneas takes care of the memory management proof obligations through + /// the translation) + /// 2. a more complex functional proof. + /// We write a very general model of the b-epsilon tree, prove that it is + /// refined by the translated code in 1., then prove the general functional + /// correctness case once and for all in 2. + /// The idea is that once we add support for closures, we should be able to + /// update the Rust code, and all we would need to do on the proof side is + /// to update the refinement proof in 1., which should hopefully be + /// straightforward. + /// + /// Also note that if we don't have [Upsert], there is no point in using + /// b-epsilon trees, which have the particularity of storing messages: + /// b-trees and their variants work very well (and don't use messages). + /// + /// Note there is something interesting about the proofs we do for [Upsert]. + /// When we use [Insert] or [Delete], we remove the upserts which are pending + /// for the key, because there is no point in applying them (there would be + /// if we wanted to leverage the fact that the update functions we apply may + /// be stateful). + /// The consequence is that we don't observe potentially failing executions of + /// the update functions. At the opposite, the specification of [Upsert] is + /// "greedy": we see [Upsert] as query then update. This means that the + /// implementation refines the specification only if we make sure that the + /// update function used for the upsert doesn't fail on the input we give it + /// (all this can be seen in the specification we prove about the be-tree). + Upsert(UpsertFunState), +} + +/// Internal node content. +/// +/// An internal node contains a map from keys to pending messages +/// +/// Invariants: +/// - the pairs (key, message) are sorted so that the keys are in increasing order +/// - for a given key, there can be: +/// - no message +/// - one insert or delete message +/// - a list of upsert messages. In that case, the upsert message are sorted +/// from the *first* to the *last* added in the betree. +pub(crate) type InternalContent = Map; + +/// Leaf node content. +/// +/// A leaf node contains a map from keys to values. +/// We store the bindings in order of increasing key. +pub(crate) type LeafContent = Map; + +/// Internal node. See [Node]. +/// +/// An internal node contains a stack of messages (stored on disk and thus +/// absent from the node itself), and two children. +/// +/// When transmitting messages to the children: the messages/bindings for the +/// keys < pivot are given to the left child, and those for the keys >= pivot +/// are given to the right child. +/// +/// Note that in Be-Tree the internal nodes have lists of children, which +/// allows to do even smarter things: if an internal node has too many +/// messages, then: +/// - either it can transmit big batches of those messages to some of its +/// children, in which case it does +/// - or it can't, in which case it splits, because otherwise we have too +/// many unefficient updates to perform (the aim really is to amortize +/// the cost of I/O, which is achieved by minimizing the number of +/// accesses to node contents) +struct Internal { + id: NodeId, + pivot: Key, + left: Box, + right: Box, +} + +/// Leaf node. See [Node] +/// +/// A leaf node contains bindings (stored on disk, and thus absent from the +/// node itself). +struct Leaf { + id: NodeId, + /// The number of bindings in the node + size: u64, +} + +/// A node in the BeTree. +/// +/// The node's content is stored on disk (and hence absent from the node itself). +/// +/// Note that we don't have clean/dirty nodes: all node contents are immediately +/// written on disk upon being updated. +enum Node { + /// An internal node (with children). + Internal(Internal), + /// A leaf node. + Leaf(Leaf), +} + +/// The parameters of a BeTree, which control when to flush or split. +struct Params { + /// The minimum number of messages we flush to the children. + /// We wait to reach 2 * min_flush_size before flushing to children. + /// If one of the children doesn't receive a number of + /// messages >= min_flush_size, we keep those messages in the parent + /// node. Of course, at least one of the two children will receive + /// flushed messages: this gives us that an internal node has at most + /// 2 * min_flush_size pending messages - 1. + min_flush_size: u64, + /// The maximum number of bindings we can store in a leaf node (if we + /// reach this number, we split). + split_size: u64, +} + +struct NodeIdCounter { + next_node_id: NodeId, +} + +impl NodeIdCounter { + fn new() -> Self { + NodeIdCounter { next_node_id: 0 } + } + + fn fresh_id(&mut self) -> NodeId { + let id = self.next_node_id; + self.next_node_id += 1; + id + } +} + +/// The BeTree itself +pub struct BeTree { + /// The parameters of the BeTree + params: Params, + /// Every node has a unique id: we keep a counter to generate fresh ids + node_id_cnt: NodeIdCounter, + /// The root of the tree + root: Node, +} + +/// The update function used for [Upsert]. +/// Will be removed once we have closures (or at least function pointers). +/// This function just computes a saturated sum. +/// Also note that it takes an option as input, for the previous value: +/// we draw inspiration from the C++ Be-Tree implemenation, where +/// in case the binding is not present, the closure stored in upsert is +/// given a default value. +pub fn upsert_update(prev: Option, st: UpsertFunState) -> Value { + // We just compute the sum, until it saturates + match prev { + Option::None => { + match st { + UpsertFunState::Add(v) => { + // We consider the default value is 0, so we return 0 + v + // (or we could fail - it doesn't really matter) + v + } + UpsertFunState::Sub(_) => { + // Same logic as for [sub], but this time we saturate at 0 + 0 + } + } + } + Option::Some(prev) => { + match st { + UpsertFunState::Add(v) => { + // Note that Aeneas is a bit conservative about the max_usize + let margin = u64::MAX - prev; + // Check if we saturate + if margin >= v { + prev + v + } else { + u64::MAX + } + } + UpsertFunState::Sub(v) => { + // Check if we saturate + if prev >= v { + prev - v + } else { + 0 + } + } + } + } + } +} + +impl List { + fn len(&self) -> u64 { + match self { + List::Nil => 0, + List::Cons(_, tl) => 1 + tl.len(), + } + } + + /// Split a list at a given length + fn split_at(self, n: u64) -> (List, List) { + if n == 0 { + (List::Nil, self) + } else { + match self { + List::Nil => unreachable!(), + List::Cons(hd, tl) => { + let (ls0, ls1) = tl.split_at(n - 1); + (List::Cons(hd, Box::new(ls0)), ls1) + } + } + } + } + + /// Push an element at the front of the list. + fn push_front(&mut self, x: T) { + // Move under borrows: annoying... + let tl = std::mem::replace(self, List::Nil); + *self = List::Cons(x, Box::new(tl)); + } + + /// Pop the element at the front of the list + fn pop_front(&mut self) -> T { + // Move under borrows: annoying... + let ls = std::mem::replace(self, List::Nil); + match ls { + List::Nil => panic!(), + List::Cons(x, tl) => { + *self = *tl; + x + } + } + } + + fn hd(&self) -> &T { + match self { + List::Nil => panic!(), + List::Cons(hd, _) => hd, + } + } +} + +impl Map { + fn head_has_key(&self, key: Key) -> bool { + match self { + List::Nil => false, + List::Cons(hd, _) => hd.0 == key, + } + } + + /// Partition the map between two maps: + /// - a first map where the keys < pivot + /// - a second map where the keys >= pivot + /// Note that the bindings in the map are supposed to be sorted in + /// order of increasing keys. + fn partition_at_pivot(self, pivot: Key) -> (Map, Map) { + match self { + List::Nil => (List::Nil, List::Nil), + List::Cons(hd, tl) => { + if hd.0 >= pivot { + (List::Nil, List::Cons(hd, tl)) + } else { + let (ls0, ls1) = tl.partition_at_pivot(pivot); + (List::Cons(hd, Box::new(ls0)), ls1) + } + } + } + } +} + +impl Leaf { + /// Split a leaf into an internal node with two children. + /// + /// The leaf should have exactly 2 * split_size elements. + /// Also, we use the fact that the keys are sorted in increasing order. + fn split( + &self, + content: Map, + params: &Params, + node_id_cnt: &mut NodeIdCounter, + ) -> Internal { + // Split the content + let (content0, content1) = content.split_at(params.split_size); + // Get the pivot + let pivot = content1.hd().0; + // Create the two nodes + let id0 = node_id_cnt.fresh_id(); + let id1 = node_id_cnt.fresh_id(); + let left = Leaf { + id: id0, + size: params.split_size, + }; + let right = Leaf { + id: id1, + size: params.split_size, + }; + // Store the content + store_leaf_node(id0, content0); + store_leaf_node(id1, content1); + // Return + Internal { + id: self.id, + pivot, + left: Box::new(Node::Leaf(left)), + right: Box::new(Node::Leaf(right)), + } + } +} + +impl Internal { + /// Small utility: lookup a value in the children nodes. + fn lookup_in_children(&mut self, key: Key) -> Option { + if key < self.pivot { + self.left.lookup(key) + } else { + self.right.lookup(key) + } + } + + /// Flush the messages in an internal node to its children. + /// Note that when flushing, we send messages to a child only if there + /// are more than min_flush_size messages to send. Also, we flush only + /// if the number of messages in the current node is >= 2* num_flush_size. + /// + /// The function returns the messages we couldn't flush to the children + /// nodes. + fn flush<'a>( + &'a mut self, + params: &Params, + node_id_cnt: &'a mut NodeIdCounter, + content: Map, + ) -> Map { + // Partition the messages + let (msgs_left, msgs_right) = content.partition_at_pivot(self.pivot); + // Check if we need to flush to the left child + let len_left = msgs_left.len(); + if len_left >= params.min_flush_size { + // Flush to the left + self.left.apply_messages(params, node_id_cnt, msgs_left); + // Check if we need to flush to the right + let len_right = msgs_right.len(); + if len_right >= params.min_flush_size { + self.right.apply_messages(params, node_id_cnt, msgs_right); + // No messages remain in the current node + List::Nil + } else { + // We keep the messages which belong to the right node + msgs_right + } + } else { + // Don't flush to the left: we necessarily flush to the right + self.right.apply_messages(params, node_id_cnt, msgs_right); + // We keep the messages which belong to the left node + msgs_left + } + } +} + +impl Node { + /// Apply a list of message to ourselves: leaf node case + fn apply_messages_to_leaf<'a>( + bindings: &'a mut Map, + new_msgs: List<(Key, Message)>, + ) { + match new_msgs { + List::Nil => (), + List::Cons(new_msg, new_msgs_tl) => { + Node::apply_to_leaf(bindings, new_msg.0, new_msg.1); + Node::apply_messages_to_leaf(bindings, *new_msgs_tl); + } + } + } + + /// Apply a message to ourselves: leaf node case + /// + /// This simply updates the bindings. + fn apply_to_leaf<'a>(bindings: &'a mut Map, key: Key, new_msg: Message) { + // Retrieve a mutable borrow to the position of the binding, if there is + // one, or to the end of the list + let bindings = Node::lookup_mut_in_bindings(key, bindings); + // Check if we point to a binding which has the key we are looking for + if bindings.head_has_key(key) { + // We need to pop the binding, and may need to reuse the + // previous value (for an upsert) + let hd = bindings.pop_front(); + // Match over the message + match new_msg { + Message::Insert(v) => { + bindings.push_front((key, v)); + } + Message::Delete => { + // Nothing to do: we popped the binding + () + } + Message::Upsert(s) => { + let v = upsert_update(Option::Some(hd.1), s); + bindings.push_front((key, v)); + } + } + } else { + // Key not found: simply insert + match new_msg { + Message::Insert(v) => { + bindings.push_front((key, v)); + } + Message::Delete => { + // Nothing to do + () + } + Message::Upsert(s) => { + let v = upsert_update(Option::None, s); + bindings.push_front((key, v)); + } + } + } + } + + /// Apply a list of message to ourselves: internal node case + fn apply_messages_to_internal<'a>( + msgs: &'a mut Map, + new_msgs: List<(Key, Message)>, + ) { + match new_msgs { + List::Nil => (), + List::Cons(new_msg, new_msgs_tl) => { + Node::apply_to_internal(msgs, new_msg.0, new_msg.1); + Node::apply_messages_to_internal(msgs, *new_msgs_tl); + } + } + } + + /// Apply a message to ourselves: internal node case + /// + /// This basically inserts a message in a messages stack. However, + /// we may need to filter previous messages: for insert, if we insert an + /// [Insert] in a stack which contains an [Insert] or a [Delete] for the + /// same key, we replace this old message with the new one. + fn apply_to_internal<'a>(msgs: &'a mut Map, key: Key, new_msg: Message) { + // Lookup the first message for [key] (if there is no message for [key], + // we get a mutable borrow to the position in the list where we need + // to insert the new message). + let msgs = Node::lookup_first_message_for_key(key, msgs); + // What we do is not the same, depending on whether there is already + // a message or not. + if msgs.head_has_key(key) { + // We need to check the current message + match new_msg { + Message::Insert(_) | Message::Delete => { + // If [Insert] or [Delete]: filter the current + // messages, and insert the new one + Node::filter_messages_for_key(key, msgs); + msgs.push_front((key, new_msg)); + } + Message::Upsert(s) => { + // If [Update]: we need to take into account the + // previous messages. + match msgs.hd().1 { + Message::Insert(prev) => { + // There should be exactly one [Insert]: + // pop it, compute the result of the [Upsert] + // and insert this result + let v = upsert_update(Option::Some(prev), s); + let _ = msgs.pop_front(); + msgs.push_front((key, Message::Insert(v))); + } + Message::Delete => { + // There should be exactly one [Delete] + // message : pop it, compute the result of + // the [Upsert], and insert this result + let _ = msgs.pop_front(); + let v = upsert_update(Option::None, s); + msgs.push_front((key, Message::Insert(v))); + } + Message::Upsert(_) => { + // There may be several msgs upserts: + // we need to insert the new message at + // the end of the list of upserts (so + // that later we can apply them all in + // proper order). + let msgs = Node::lookup_first_message_after_key(key, msgs); + msgs.push_front((key, Message::Upsert(s))); + } + } + } + } + } else { + // No pending message for [key]: simply add the new message + msgs.push_front((key, new_msg)) + } + } + + /// Apply a message to ourselves + fn apply<'a>( + &'a mut self, + params: &Params, + node_id_cnt: &'a mut NodeIdCounter, + key: Key, + new_msg: Message, + ) { + let msgs = List::Cons((key, new_msg), Box::new(List::Nil)); + self.apply_messages(params, node_id_cnt, msgs); + } + + /// Apply a list of messages to ourselves + fn apply_messages<'a>( + &'a mut self, + params: &Params, + node_id_cnt: &'a mut NodeIdCounter, + msgs: List<(Key, Message)>, + ) { + match self { + Node::Leaf(node) => { + // Load the content from disk + let mut content = load_leaf_node(node.id); + // Insert + Node::apply_messages_to_leaf(&mut content, msgs); + // Check if we need to split - in the future, we might want to + // do something smarter to compute the number of messages + let len = content.len(); + if len >= 2 * params.split_size { + // Split + let new_node = node.split(content, params, node_id_cnt); + // Store the content to disk + store_leaf_node(node.id, List::Nil); + // Update the node + *self = Node::Internal(new_node); + } else { + // Update the size if necessary + node.size = len; + // Store the content to disk + store_leaf_node(node.id, content); + } + } + Node::Internal(node) => { + // Load the content from disk + let mut content = load_internal_node(node.id); + // Insert + Node::apply_messages_to_internal(&mut content, msgs); + // Check if we need to flush - in the future, we might want to + // do something smarter to compute the number of messages + let num_msgs = content.len(); + if num_msgs >= params.min_flush_size { + content = node.flush(params, node_id_cnt, content); + } + // Store the content to disk + store_internal_node(node.id, content) + } + } + } + + /// Lookup a value in a list of bindings. + /// Note that the values should be stored in order of increasing key. + fn lookup_in_bindings(key: Key, bindings: &Map) -> Option { + match bindings { + List::Nil => Option::None, + List::Cons(hd, tl) => { + if hd.0 == key { + Option::Some(hd.1) + } else if hd.0 > key { + Option::None + } else { + Node::lookup_in_bindings(key, tl) + } + } + } + } + + /// Lookup a value in a list of bindings, and return a borrow to the position + /// where the value is (or should be inserted, if the key is not in the bindings). + fn lookup_mut_in_bindings<'a>( + key: Key, + bindings: &'a mut Map, + ) -> &'a mut Map { + match bindings { + List::Nil => bindings, + List::Cons(hd, tl) => { + // This requires Polonius + if hd.0 >= key { + bindings + } else { + Node::lookup_mut_in_bindings(key, tl) + } + } + } + } + + /// Filter all the messages which concern [key]. + /// + /// Note that the stack of messages must start with a message for [key]: + /// we stop filtering at the first message which is not about [key]. + fn filter_messages_for_key<'a>(key: Key, msgs: &'a mut Map) { + match msgs { + List::Nil => (), + List::Cons((k, _), _) => { + if *k == key { + msgs.pop_front(); + Node::filter_messages_for_key(key, msgs); + } else { + // Stop + () + } + } + } + } + + fn lookup_first_message_after_key<'a>( + key: Key, + msgs: &'a mut Map, + ) -> &'a mut Map { + match msgs { + List::Nil => msgs, + List::Cons((k, _), next_msgs) => { + if *k == key { + Node::lookup_first_message_after_key(key, next_msgs) + } else { + msgs + } + } + } + } + + /// Returns the value bound to a key. + /// Note that while looking for the binding, we might reorganize the + /// internals of the betree to apply or flush messages: hence the mutable + /// borrow. + fn lookup<'a>(&'a mut self, key: Key) -> Option { + match self { + Node::Leaf(node) => { + // Load the node content + let bindings = load_leaf_node(node.id); + // Just lookup the binding in the map + Node::lookup_in_bindings(key, &bindings) + } + Node::Internal(node) => { + // Load the node content + let mut msgs = load_internal_node(node.id); + // Look for the first message pending for the key. + // Note that we maintain the following invariants: + // - if there are > 1 messages, they must be upsert messages only + // - the upsert messages are sorted from the *first* added to the + // *last* added to the betree. + // Also note that if there are upsert messages, we have to apply + // them immediately. + // + // Rk.: [lookup_first_message_for_key] below returns a borrow to + // the portion of the list we will update (if we have upserts, + // we will apply the messages, filter them while doing so, + // insert an [Insert] message, etc.). Should be interesting + // to see how the proof experience with the backward functions + // is at this for this piece of code. Note that this was inpired + // by Be-Tree. + // Also, can't wait to see how all this will work with loops. + let pending = Node::lookup_first_message_for_key(key, &mut msgs); + match pending { + List::Nil => { + // Nothing: dive into the children + node.lookup_in_children(key) + } + List::Cons((k, msg), _) => { + // Check if the borrow which points inside the messages + // stack points to a message for [key] + if *k != key { + // Note the same key: dive into the children + node.lookup_in_children(key) + } else { + // Same key: match over the message for this key + match msg { + Message::Insert(v) => Some(*v), + Message::Delete => None, + Message::Upsert(_) => { + // There are pending upserts: we have no choice but to + // apply them. + // + // Rk.: rather than calling [lookup], we could actually + // go down the tree accumulating upserts. On the other + // hand, the key is now "hotter", so it is not a bad + // idea to keep it as close to the root as possible. + // Note that what we do is what Be-Tree does. + // + // First, lookup the value from the children. + let v = node.lookup_in_children(key); + // Apply the pending updates, and replace them with + // an [Insert] containing the updated value. + // + // Rk.: Be-Tree doesn't seem to store the newly computed + // value, which I don't understand. + let v = Node::apply_upserts(pending, v, key); + // Update the node content + store_internal_node(node.id, msgs); + // Return the value + Option::Some(v) + } + } + } + } + } + } + } + } + + /// Return a mutable borrow to the first message whose key is <= than [key]. + /// If the key is [key], then it is the first message about [key]. + /// Otherwise, it gives us a mutable borrow to the place where we need + /// to insert new messages (note that the borrow may point to the end + /// of the list). + fn lookup_first_message_for_key<'a>( + key: Key, + msgs: &'a mut Map, + ) -> &'a mut Map { + match msgs { + List::Nil => msgs, + List::Cons(x, next_msgs) => { + // Rk.: we need Polonius here + // We wouldn't need Polonius if directly called the proper + // function to make the modifications here (because we wouldn't + // need to return anything). However, it would not be very + // idiomatic, especially with regards to the fact that we will + // rewrite everything with loops at some point. + if x.0 >= key { + msgs + } else { + Node::lookup_first_message_for_key(key, next_msgs) + } + } + } + } + + /// Apply the upserts from the current messages stack to a looked up value. + /// + /// The input mutable borrow must point to the first upsert message in the + /// messages stack of the current node. We remove the messages from the stack + /// while applying them. + /// Note that if there are no more upserts to apply, then the value must be + /// `Some`. Also note that we use the invariant that in the message stack, + /// upsert messages are sorted from the first to the last to apply. + fn apply_upserts(msgs: &mut Map, prev: Option, key: Key) -> Value { + if msgs.head_has_key(key) { + // Pop the front message. + // Note that it *must* be an upsert. + let msg = msgs.pop_front(); + match msg.1 { + Message::Upsert(s) => { + // Apply the update + let v = upsert_update(prev, s); + let prev = Option::Some(v); + // Continue + Node::apply_upserts(msgs, prev, key) + } + _ => { + // Unreachable: we can only have [Upsert] messages + // for the key + unreachable!(); + } + } + } else { + // We applied all the upsert messages: simply put an [Insert] + // message and return the value. + let v = prev.unwrap(); + msgs.push_front((key, Message::Insert(v))); + return v; + } + } +} + +impl BeTree { + pub fn new(min_flush_size: u64, split_size: u64) -> Self { + let mut node_id_cnt = NodeIdCounter::new(); + let id = node_id_cnt.fresh_id(); + let root = Node::Leaf(Leaf { id, size: 0 }); + store_leaf_node(id, List::Nil); + let params = Params { + min_flush_size, + split_size, + }; + BeTree { + params, + node_id_cnt, + root, + } + } + + /// Apply a message to the tree. + /// + /// This is an auxiliary function. + fn apply(&mut self, key: Key, msg: Message) { + self.root + .apply(&self.params, &mut self.node_id_cnt, key, msg) + } + + /// Insert a binding from [key] to [value] + pub fn insert(&mut self, key: Key, value: Value) { + let msg = Message::Insert(value); + self.apply(key, msg); + } + + /// Delete the bindings for [key] + pub fn delete(&mut self, key: Key) { + let msg = Message::Delete; + self.apply(key, msg); + } + + /// Apply a query-update + pub fn upsert(&mut self, key: Key, upd: UpsertFunState) { + let msg = Message::Upsert(upd); + self.apply(key, msg); + } + + /// Returns the value bound to a key. + /// Note that while looking for the binding, we might reorganize the + /// internals of the betree to apply or flush messages: hence the mutable + /// borrow. + pub fn lookup<'a>(&'a mut self, key: Key) -> Option { + self.root.lookup(key) + } +} + +#[cfg(test)] +mod tests { + use crate::betree::*; + use std::collections::HashMap; + use std::fmt::{Display, Error, Formatter}; + use std::vec::Vec; + + struct Maps { + betree: BeTree, + refmap: HashMap, + } + + impl Maps { + fn insert(&mut self, k: Key, v: Value) { + log::trace!("insert: {} -> {}", k, v); + self.betree.insert(k, v); + self.refmap.insert(k, v); + } + + fn delete(&mut self, k: Key) { + log::trace!("delete: {}", k); + self.betree.delete(k); + self.refmap.remove(&k); + } + + /// This function doesn't return a value: it simply checks that the + /// b-epsilon tree and the reference map have the same bindings. + fn lookup(&mut self, k: Key) { + let v0 = self.betree.lookup(k); + let v1 = self.refmap.get(&k).map(|x| *x); + log::trace!("lookup {k}: betree: {:?}, ref: {:?}", v0, v1); + assert!(v0 == v1); + } + + /// Only testing the addition (the choice of the update function doesn't + /// make much difference) + fn upsert(&mut self, k: Key, v: Value) { + log::trace!("upsert: {} -> add({})", k, v); + self.betree.upsert(k, UpsertFunState::Add(v)); + let prev = self.refmap.get(&k).map(|x| *x); + let nv = upsert_update(prev, UpsertFunState::Add(v)); + self.refmap.insert(k, nv); + } + + /// Check that all the bindings in the betree give the same result as the + /// reference. + /// + /// Rk.: looking up actually updates the b-epsilon tree. + fn check_equal(&mut self) { + let keys: Vec = self.refmap.keys().map(|k| *k).collect(); + for k in keys { + self.lookup(k); + } + } + } + + impl Display for Map { + fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> { + match self { + List::Nil => write!(f, ""), + List::Cons(hd, tl) => { + write!(f, "{} -> {}, ", hd.0, hd.1).unwrap(); + tl.fmt(f) + } + } + } + } + + impl Display for UpsertFunState { + fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> { + match self { + UpsertFunState::Add(v) => write!(f, "add({})", v), + UpsertFunState::Sub(v) => write!(f, "sub({})", v), + } + } + } + + impl Display for Message { + fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> { + match self { + Message::Insert(v) => write!(f, "insert({})", v), + Message::Delete => write!(f, "delete"), + Message::Upsert(v) => write!(f, "upsert({})", v), + } + } + } + + impl Display for Map { + fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> { + match self { + List::Nil => write!(f, ""), + List::Cons(hd, tl) => { + write!(f, "{} -> {}, ", hd.0, hd.1).unwrap(); + tl.fmt(f) + } + } + } + } + + impl Node { + fn fmt(&self, indent: &String, f: &mut Formatter<'_>) -> Result<(), Error> { + match self { + Node::Leaf(node) => { + let content = load_leaf_node(node.id); + write!(f, "{}{}: [{}]", indent, node.id, content) + } + Node::Internal(node) => { + let content = load_internal_node(node.id); + let indent1 = format!("{} ", indent).to_string(); + write!( + f, + "{}{{\n{}{},\n{}[{}],", + indent, indent, node.id, indent, &content + ) + .unwrap(); + write!(f, "\n{}", indent1).unwrap(); + node.left.fmt(&indent1, f).unwrap(); + write!(f, "\n{}", indent1).unwrap(); + node.right.fmt(&indent1, f).unwrap(); + write!(f, "\n{}}}", indent) + } + } + } + } + + impl Display for BeTree { + fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> { + self.root.fmt(&"".to_string(), f) + } + } + + #[test] + fn test1() { + // Initialize the logger + env_logger::init(); + + let mut m = Maps { + betree: BeTree::new(5, 5), + refmap: HashMap::new(), + }; + let num_keys = 100; + + // Insert bindings + for k in 0..num_keys { + let v = 2 * k + 1; + m.insert(k, v); + log::trace!("\n{}", &m.betree); + } + + // Make various queries + for kb in 0..(10 * num_keys) { + let k = kb % num_keys; + match k % 4 { + 0 => { + let v = 3 * k + 2; + m.insert(k, v); + } + 1 => { + m.delete(k); + } + 2 => { + let v = kb % 7; + m.upsert(k, v); + } + 3 => { + m.lookup(k); + } + _ => { + unreachable!(); + } + } + log::trace!("\n{}", &m.betree); + } + + // Check that the b-epsilon tree didn't diverge (we check twice, + // because looking up performs updates that we also want to test) + m.check_equal(); + m.check_equal(); + } + fn range_insert(tree: &mut BeTree, start: Key, end: Key) { + for k in start..end { + tree.insert(k, 2 * k + 1); + } + } +} diff --git a/tests/src/betree/src/betree_utils.rs b/tests/src/betree/src/betree_utils.rs new file mode 100644 index 00000000..fd269f4d --- /dev/null +++ b/tests/src/betree/src/betree_utils.rs @@ -0,0 +1,155 @@ +//! The following module implements utilities for [betree.rs]. +//! Those utilities are only used for serialization/deserialization (we don't +//! reason about them). +//! +//! The issue is that we can't derive serialization/deserialization +//! implementations directly in betree.rs, otherwise we can't translate. +//! We could have hacked in Aeneas to skip those implementations, but I'd +//! rather put a little bit of engineering time into this file, while thinking +//! about a cleaner way of doing this in general. The following file is not +//! difficult to write and maintain anyway. +#![allow(dead_code)] + +use crate::betree::{ + InternalContent, Key, LeafContent, List, Message, NodeId, UpsertFunState, Value, +}; +use serde::{Deserialize, Serialize}; +use std::fs::File; +use std::vec::Vec; + +/// Note that I tried using Serde's facilities to define serialization/ +/// deserialization functions for external types, but it proved cumbersome +/// for the betree case. +#[derive(Serialize, Deserialize)] +pub enum UpsertFunStateSerde { + Add(u64), + Sub(u64), +} + +impl UpsertFunStateSerde { + fn to_state(self) -> UpsertFunState { + match self { + UpsertFunStateSerde::Add(v) => UpsertFunState::Add(v), + UpsertFunStateSerde::Sub(v) => UpsertFunState::Sub(v), + } + } + + fn from_state(msg: UpsertFunState) -> Self { + match msg { + UpsertFunState::Add(v) => UpsertFunStateSerde::Add(v), + UpsertFunState::Sub(v) => UpsertFunStateSerde::Sub(v), + } + } +} + +/// Same remark as for [UpsertFunStateSerde] +#[derive(Serialize, Deserialize)] +enum MessageSerde { + Insert(Value), + Delete, + Upsert(UpsertFunStateSerde), +} + +impl MessageSerde { + fn to_msg(self) -> Message { + match self { + MessageSerde::Insert(v) => Message::Insert(v), + MessageSerde::Delete => Message::Delete, + MessageSerde::Upsert(v) => Message::Upsert(v.to_state()), + } + } + + fn from_msg(msg: Message) -> Self { + match msg { + Message::Insert(v) => MessageSerde::Insert(v), + Message::Delete => MessageSerde::Delete, + Message::Upsert(v) => MessageSerde::Upsert(UpsertFunStateSerde::from_state(v)), + } + } +} + +// For some reason, I don't manage to make that in an impl... +pub(crate) fn list_from_vec(mut v: Vec) -> List { + // We need to reverse + v.reverse(); + let mut l = List::Nil; + for x in v.into_iter() { + l = List::Cons(x, Box::new(l)); + } + l +} + +// For some reason, I don't manage to make that in an impl... +pub(crate) fn list_to_vec(mut l: List) -> Vec { + let mut v = Vec::new(); + loop { + match l { + List::Nil => break, + List::Cons(hd, tl) => { + v.push(hd); + l = *tl; + } + } + } + v +} + +/// See the equivalent function in betree.rs +pub(crate) fn load_internal_node(id: NodeId) -> InternalContent { + // Open the file + std::fs::create_dir_all("tmp").unwrap(); + let filename = format!("tmp/node{}", id).to_string(); + // Read + let f = File::open(filename).unwrap(); + // Serde makes things easy + let c: Vec<(Key, MessageSerde)> = serde_json::from_reader(&f).unwrap(); + let c: Vec<(Key, Message)> = c + .into_iter() + .map(|(key, msg)| (key, msg.to_msg())) + .collect(); + // Convert + list_from_vec(c) +} + +/// See the equivalent function in betree.rs +pub(crate) fn store_internal_node(id: NodeId, content: InternalContent) { + // Open the file + std::fs::create_dir_all("tmp").unwrap(); + let filename = format!("tmp/node{}", id).to_string(); + // Write + let f = File::create(filename).unwrap(); + // Convert + let v: Vec<(Key, Message)> = list_to_vec(content); + let v: Vec<(Key, MessageSerde)> = v + .into_iter() + .map(|(k, msg)| (k, MessageSerde::from_msg(msg))) + .collect(); + // Serde makes things easy + serde_json::to_writer(&f, &v).unwrap(); +} + +/// See the equivalent function in betree.rs +pub(crate) fn load_leaf_node(id: NodeId) -> LeafContent { + // Open the file + std::fs::create_dir_all("tmp").unwrap(); + let filename = format!("tmp/node{}", id).to_string(); + // Read + let f = File::open(filename).unwrap(); + // Serde makes things easy + let c: Vec<(Key, Value)> = serde_json::from_reader(&f).unwrap(); + // Convert + list_from_vec(c) +} + +/// See the equivalent function in betree.rs +pub(crate) fn store_leaf_node(id: NodeId, content: LeafContent) { + // Open the file + std::fs::create_dir_all("tmp").unwrap(); + let filename = format!("tmp/node{}", id).to_string(); + // Write + let f = File::create(filename).unwrap(); + // Convert + let v: Vec<(Key, Value)> = list_to_vec(content); + // Serde makes things easy + serde_json::to_writer(&f, &v).unwrap(); +} diff --git a/tests/src/betree/src/main.rs b/tests/src/betree/src/main.rs new file mode 100644 index 00000000..64e9f7db --- /dev/null +++ b/tests/src/betree/src/main.rs @@ -0,0 +1,4 @@ +mod betree; +mod betree_utils; + +fn main() {} diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs new file mode 100644 index 00000000..9f48cb04 --- /dev/null +++ b/tests/src/bitwise.rs @@ -0,0 +1,27 @@ +//! Exercise the bitwise operations + +pub fn shift_u32(a: u32) -> u32 { + let i: usize = 16; + let mut t = a >> i; + t <<= i; + t +} + +pub fn shift_i32(a: i32) -> i32 { + let i: isize = 16; + let mut t = a >> i; + t <<= i; + t +} + +pub fn xor_u32(a: u32, b: u32) -> u32 { + a ^ b +} + +pub fn or_u32(a: u32, b: u32) -> u32 { + a | b +} + +pub fn and_u32(a: u32, b: u32) -> u32 { + a & b +} diff --git a/tests/src/constants.rs b/tests/src/constants.rs new file mode 100644 index 00000000..83904eed --- /dev/null +++ b/tests/src/constants.rs @@ -0,0 +1,96 @@ +//! Tests with constants + +// Integers + +pub const X0: u32 = 0; + +pub const X1: u32 = u32::MAX; + +#[allow(clippy::let_and_return)] +pub const X2: u32 = { + let x = 3; + x +}; + +pub const X3: u32 = incr(32); + +pub const fn incr(n: u32) -> u32 { + n + 1 +} + +// Pairs + +pub const fn mk_pair0(x: u32, y: u32) -> (u32, u32) { + (x, y) +} + +pub const fn mk_pair1(x: u32, y: u32) -> Pair { + Pair { x, y } +} + +pub const P0: (u32, u32) = mk_pair0(0, 1); +pub const P1: Pair = mk_pair1(0, 1); +pub const P2: (u32, u32) = (0, 1); +pub const P3: Pair = Pair { x: 0, y: 1 }; + +pub struct Pair { + pub x: T1, + pub y: T2, +} + +pub const Y: Wrap = Wrap::new(2); + +pub const fn unwrap_y() -> i32 { + Y.value +} + +pub const YVAL: i32 = unwrap_y(); + +pub struct Wrap { + value: T, +} + +impl Wrap { + pub const fn new(value: T) -> Wrap { + Wrap { value } + } +} + +// Additions + +pub const fn get_z1() -> i32 { + const Z1: i32 = 3; + Z1 +} + +pub const fn add(a: i32, b: i32) -> i32 { + a + b +} + +pub const fn get_z2() -> i32 { + add(Q1, add(get_z1(), Q3)) +} + +pub const Q1: i32 = 5; +pub const Q2: i32 = Q1; +pub const Q3: i32 = add(Q2, 3); + +// Static + +pub static S1: u32 = 6; +pub static S2: u32 = incr(S1); +pub static S3: Pair = P3; +pub static S4: Pair = mk_pair1(7, 8); + +// Constants with generics +pub struct V { + pub x: [T; N], +} + +impl V { + pub const LEN: usize = N; +} + +pub fn use_v() -> usize { + V::::LEN +} diff --git a/tests/src/demo.rs b/tests/src/demo.rs new file mode 100644 index 00000000..bc74cc8b --- /dev/null +++ b/tests/src/demo.rs @@ -0,0 +1,111 @@ +#![allow(clippy::needless_lifetimes)] + +/* Simple functions */ + +pub fn choose<'a, T>(b: bool, x: &'a mut T, y: &'a mut T) -> &'a mut T { + if b { + x + } else { + y + } +} + +pub fn mul2_add1(x: u32) -> u32 { + (x + x) + 1 +} + +pub fn use_mul2_add1(x: u32, y: u32) -> u32 { + mul2_add1(x) + y +} + +pub fn incr<'a>(x: &'a mut u32) { + *x += 1; +} + +pub fn use_incr() { + let mut x = 0; + incr(&mut x); + incr(&mut x); + incr(&mut x); +} + +/* Recursion, loops */ + +pub enum CList { + CCons(T, Box>), + CNil, +} + +pub fn list_nth<'a, T>(l: &'a CList, i: u32) -> &'a T { + match l { + CList::CCons(x, tl) => { + if i == 0 { + x + } else { + list_nth(tl, i - 1) + } + } + CList::CNil => { + panic!() + } + } +} + +pub fn list_nth_mut<'a, T>(l: &'a mut CList, i: u32) -> &'a mut T { + match l { + CList::CCons(x, tl) => { + if i == 0 { + x + } else { + list_nth_mut(tl, i - 1) + } + } + CList::CNil => { + panic!() + } + } +} + +pub fn list_nth_mut1<'a, T>(mut l: &'a mut CList, mut i: u32) -> &'a mut T { + while let CList::CCons(x, tl) = l { + if i == 0 { + return x; + } + i -= 1; + l = tl; + } + panic!() +} + +pub fn i32_id(i: i32) -> i32 { + if i == 0 { + 0 + } else { + i32_id(i - 1) + 1 + } +} + +pub fn list_tail<'a, T>(l: &'a mut CList) -> &'a mut CList { + match l { + CList::CCons(_, tl) => list_tail(tl), + CList::CNil => l, + } +} + +/* Traits */ + +pub trait Counter { + fn incr(&mut self) -> usize; +} + +impl Counter for usize { + fn incr(&mut self) -> usize { + let x = *self; + *self += 1; + x + } +} + +pub fn use_counter<'a, T: Counter>(cnt: &'a mut T) -> usize { + cnt.incr() +} diff --git a/tests/src/external.rs b/tests/src/external.rs new file mode 100644 index 00000000..521749d6 --- /dev/null +++ b/tests/src/external.rs @@ -0,0 +1,11 @@ +//! This module uses external types and functions + +use std::cell::Cell; + +pub fn use_get(rc: &Cell) -> u32 { + rc.get() +} + +pub fn incr(rc: &mut Cell) { + *rc.get_mut() += 1; +} diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs new file mode 100644 index 00000000..58d22acd --- /dev/null +++ b/tests/src/hashmap.rs @@ -0,0 +1,352 @@ +//! A hashmap implementation. +//! +//! Current limitations: +//! - all the recursive functions should be rewritten with loops, once +//! we have support for this. +//! - we will need function pointers/closures if we want to make the map +//! generic in the key type (having function pointers allows to mimic traits) +//! - for the "get" functions: we don't support borrows inside of enumerations +//! for now, so we can't return a type like `Option<&T>`. The real restriction +//! we currently have on borrows is that we forbid *nested* borrows in function +//! signatures, like in `&'a mut &'b mut T` (and the real problem comes from +//! nested *lifetimes*, not nested borrows). Getting the borrows inside of +//! enumerations mostly requires to pour some implementation time in it. + +use std::vec::Vec; +pub type Key = usize; // TODO: make this generic +pub type Hash = usize; + +pub enum List { + Cons(Key, T, Box>), + Nil, +} + +/// A hash function for the keys. +/// Rk.: we use shared references because we anticipate on the generic +/// hash map version. +pub fn hash_key(k: &Key) -> Hash { + // Do nothing for now, we might want to implement something smarter + // in the future, or to call an external function (which will be + // abstract): we don't need to reason about the hash function. + *k +} + +/// A hash map from [u64] to values +pub struct HashMap { + /// The current number of entries in the table + num_entries: usize, + /// The max load factor, expressed as a fraction + max_load_factor: (usize, usize), + /// The max load factor applied to the current table length: + /// gives the threshold at which to resize the table. + max_load: usize, + /// The table itself + slots: Vec>, +} + +impl HashMap { + /// Allocate a vector of slots of a given size. + /// We would need a loop, but can't use loops for now... + fn allocate_slots(mut slots: Vec>, mut n: usize) -> Vec> { + while n > 0 { + slots.push(List::Nil); + n -= 1; + } + slots + } + + /// Create a new table, with a given capacity + fn new_with_capacity( + capacity: usize, + max_load_dividend: usize, + max_load_divisor: usize, + ) -> Self { + // TODO: better to use `Vec::with_capacity(capacity)` instead + // of `Vec::new()` + let slots = HashMap::allocate_slots(Vec::new(), capacity); + HashMap { + num_entries: 0, + max_load_factor: (max_load_dividend, max_load_divisor), + max_load: (capacity * max_load_dividend) / max_load_divisor, + slots, + } + } + + pub fn new() -> Self { + // For now we create a table with 32 slots and a max load factor of 4/5 + HashMap::new_with_capacity(32, 4, 5) + } + + pub fn clear(&mut self) { + self.num_entries = 0; + let slots = &mut self.slots; + let mut i = 0; + while i < slots.len() { + slots[i] = List::Nil; + i += 1; + } + } + + pub fn len(&self) -> usize { + self.num_entries + } + + /// Insert in a list. + /// Return `true` if we inserted an element, `false` if we simply updated + /// a value. + fn insert_in_list(key: Key, value: T, mut ls: &mut List) -> bool { + loop { + match ls { + List::Nil => { + *ls = List::Cons(key, value, Box::new(List::Nil)); + return true; + } + List::Cons(ckey, cvalue, tl) => { + if *ckey == key { + *cvalue = value; + return false; + } else { + ls = tl; + } + } + } + } + } + + /// Auxiliary function to insert in the hashmap without triggering a resize + fn insert_no_resize(&mut self, key: Key, value: T) { + let hash = hash_key(&key); + let hash_mod = hash % self.slots.len(); + // We may want to use slots[...] instead of get_mut... + let inserted = HashMap::insert_in_list(key, value, &mut self.slots[hash_mod]); + if inserted { + self.num_entries += 1; + } + } + + /// Insertion function. + /// May trigger a resize of the hash table. + pub fn insert(&mut self, key: Key, value: T) { + // Insert + self.insert_no_resize(key, value); + // Resize if necessary + if self.len() > self.max_load { + self.try_resize() + } + } + + /// The resize function, called if we need to resize the table after + /// an insertion. + fn try_resize(&mut self) { + // Check that we can resize: we need to check that there are no overflows. + // Note that we are conservative about the usize::MAX. + // Also note that `as usize` is a trait, but we apply it to a constant + // here, which gets compiled by the MIR interpreter (so we don't see + // the conversion, actually). + // Rk.: this is a hit heavy... + let max_usize = u32::MAX as usize; + let capacity = self.slots.len(); + // Checking that there won't be overflows by using the fact that, if m > 0: + // n * m <= p <==> n <= p / m + let n1 = max_usize / 2; + if capacity <= n1 / self.max_load_factor.0 { + // Create a new table with a higher capacity + let mut ntable = HashMap::new_with_capacity( + capacity * 2, + self.max_load_factor.0, + self.max_load_factor.1, + ); + + // Move the elements to the new table + HashMap::move_elements(&mut ntable, &mut self.slots, 0); + + // Replace the current table with the new table + self.slots = ntable.slots; + self.max_load = ntable.max_load; + } + } + + /// Auxiliary function called by [try_resize] to move all the elements + /// from the table to a new table + fn move_elements<'a>(ntable: &'a mut HashMap, slots: &'a mut Vec>, mut i: usize) { + while i < slots.len() { + // Move the elements out of the slot i + let ls = std::mem::replace(&mut slots[i], List::Nil); + // Move all those elements to the new table + HashMap::move_elements_from_list(ntable, ls); + // Do the same for slot i+1 + i += 1; + } + } + + /// Auxiliary function. + fn move_elements_from_list(ntable: &mut HashMap, mut ls: List) { + // As long as there are elements in the list, move them + loop { + match ls { + List::Nil => return, // We're done + List::Cons(k, v, tl) => { + // Insert the element in the new table + ntable.insert_no_resize(k, v); + // Move the elements out of the tail + ls = *tl; + } + } + } + } + + /// Returns `true` if the map contains a value for the specified key. + pub fn contains_key(&self, key: &Key) -> bool { + let hash = hash_key(key); + let hash_mod = hash % self.slots.len(); + HashMap::contains_key_in_list(key, &self.slots[hash_mod]) + } + + /// Returns `true` if the list contains a value for the specified key. + pub fn contains_key_in_list(key: &Key, mut ls: &List) -> bool { + loop { + match ls { + List::Nil => return false, + List::Cons(ckey, _, tl) => { + if *ckey == *key { + return true; + } else { + ls = tl; + } + } + } + } + } + + /// We don't support borrows inside of enumerations for now, so we + /// can't return an option... + /// TODO: add support for that + fn get_in_list<'a, 'k>(key: &'k Key, mut ls: &'a List) -> &'a T { + loop { + match ls { + List::Nil => panic!(), + List::Cons(ckey, cvalue, tl) => { + if *ckey == *key { + return cvalue; + } else { + ls = tl; + } + } + } + } + } + + pub fn get<'a, 'k>(&'a self, key: &'k Key) -> &'a T { + let hash = hash_key(key); + let hash_mod = hash % self.slots.len(); + HashMap::get_in_list(key, &self.slots[hash_mod]) + } + + pub fn get_mut_in_list<'a, 'k>(mut ls: &'a mut List, key: &'k Key) -> &'a mut T { + while let List::Cons(ckey, cvalue, tl) = ls { + if *ckey == *key { + return cvalue; + } else { + ls = tl; + } + } + panic!() + } + + /// Same remark as for [get]. + pub fn get_mut<'a, 'k>(&'a mut self, key: &'k Key) -> &'a mut T { + let hash = hash_key(key); + let hash_mod = hash % self.slots.len(); + HashMap::get_mut_in_list(&mut self.slots[hash_mod], key) + } + + /// Remove an element from the list. + /// Return the removed element. + fn remove_from_list(key: &Key, mut ls: &mut List) -> Option { + loop { + match ls { + List::Nil => return None, + // We have to use a guard and split the Cons case into two + // branches, otherwise the borrow checker is not happy. + List::Cons(ckey, _, _) if *ckey == *key => { + // We have to move under borrows, so we need to use + // [std::mem::replace] in several steps. + // Retrieve the tail + let mv_ls = std::mem::replace(ls, List::Nil); + match mv_ls { + List::Nil => unreachable!(), + List::Cons(_, cvalue, tl) => { + // Make the list equal to its tail + *ls = *tl; + // Return the dropped value + return Some(cvalue); + } + } + } + List::Cons(_, _, tl) => { + ls = tl; + } + } + } + } + + /// Same remark as for [get]. + pub fn remove(&mut self, key: &Key) -> Option { + let hash = hash_key(key); + let hash_mod = hash % self.slots.len(); + + let x = HashMap::remove_from_list(key, &mut self.slots[hash_mod]); + match x { + Option::None => Option::None, + Option::Some(x) => { + self.num_entries -= 1; + Option::Some(x) + } + } + } +} + +/// I currently can't retrieve functions marked with the attribute #[test], +/// while I want to extract the unit tests and use the normalize on them, +/// so I have to define the test functions somewhere and call them from +/// a test function. +/// TODO: find a way to do that. +#[allow(dead_code)] +fn test1() { + let mut hm: HashMap = HashMap::new(); + hm.insert(0, 42); + hm.insert(128, 18); + hm.insert(1024, 138); + hm.insert(1056, 256); + // Rk.: `&128` introduces a ref constant value + // TODO: add support for this + // Rk.: this only happens if we query the MIR too late (for instance, + // the optimized MIR). It is not a problem if we query, say, the + // "built" MIR. + let k = 128; + assert!(*hm.get(&k) == 18); + let k = 1024; + let x = hm.get_mut(&k); + *x = 56; + assert!(*hm.get(&k) == 56); + let x = hm.remove(&k); + // If we write `x == Option::Some(56)` rust introduces + // a call to `core::cmp::PartialEq::eq`, which is a trait + // I don't support for now. + // Also, I haven't implemented support for `unwrap` yet... + match x { + Option::None => panic!(), + Option::Some(x) => assert!(x == 56), + }; + let k = 0; + assert!(*hm.get(&k) == 42); + let k = 128; + assert!(*hm.get(&k) == 18); + let k = 1056; + assert!(*hm.get(&k) == 256); +} + +#[test] +fn tests() { + test1(); +} diff --git a/tests/src/hashmap_main.rs b/tests/src/hashmap_main.rs new file mode 100644 index 00000000..45dfa6e2 --- /dev/null +++ b/tests/src/hashmap_main.rs @@ -0,0 +1,16 @@ +mod hashmap; +mod hashmap_utils; + +use crate::hashmap::*; +use crate::hashmap_utils::*; + +pub fn insert_on_disk(key: Key, value: u64) { + // Deserialize + let mut hm = deserialize(); + // Update + hm.insert(key, value); + // Serialize + serialize(hm); +} + +pub fn main() {} diff --git a/tests/src/hashmap_utils.rs b/tests/src/hashmap_utils.rs new file mode 100644 index 00000000..cd7b481f --- /dev/null +++ b/tests/src/hashmap_utils.rs @@ -0,0 +1,12 @@ +use crate::hashmap::*; + +/// Serialize a hash map - we don't have traits, so we fix the type of the +/// values (this is not the interesting part anyway) +pub(crate) fn serialize(_hm: HashMap) { + unimplemented!(); +} +/// Deserialize a hash map - we don't have traits, so we fix the type of the +/// values (this is not the interesting part anyway) +pub(crate) fn deserialize() -> HashMap { + unimplemented!(); +} diff --git a/tests/src/loops.rs b/tests/src/loops.rs new file mode 100644 index 00000000..2f71d75b --- /dev/null +++ b/tests/src/loops.rs @@ -0,0 +1,366 @@ +use std::vec::Vec; + +/// No borrows +pub fn sum(max: u32) -> u32 { + let mut i = 0; + let mut s = 0; + while i < max { + s += i; + i += 1; + } + + s *= 2; + s +} + +/// Same as [sum], but we use borrows in order tocreate loans inside a loop +/// iteration, and those borrows will have to be ended by the end of the +/// iteration. +pub fn sum_with_mut_borrows(max: u32) -> u32 { + let mut i = 0; + let mut s = 0; + while i < max { + let ms = &mut s; + *ms += i; + let mi = &mut i; + *mi += 1; + } + + s *= 2; + s +} + +/// Similar to [sum_with_mut_borrows]. +pub fn sum_with_shared_borrows(max: u32) -> u32 { + let mut i = 0; + let mut s = 0; + while i < max { + i += 1; + // We changed the order compared to [sum_with_mut_borrows]: + // we want to have a shared borrow surviving until the end + // of the iteration. + let mi = &i; + s += *mi; + } + + s *= 2; + s +} + +pub fn sum_array(a: [u32; N]) -> u32 { + let mut i = 0; + let mut s = 0; + while i < N { + s += a[i]; + i += 1; + } + s +} + +/// This case is interesting, because the fixed point for the loop doesn't +/// introduce new abstractions. +pub fn clear(v: &mut Vec) { + let mut i = 0; + while i < v.len() { + v[i] = 0; + i += 1; + } +} + +pub enum List { + Cons(T, Box>), + Nil, +} + +/// The parameter `x` is a borrow on purpose +pub fn list_mem(x: &u32, mut ls: &List) -> bool { + while let List::Cons(y, tl) = ls { + if *y == *x { + return true; + } else { + ls = tl; + } + } + false +} + +/// Same as [list_nth_mut] but with a loop +pub fn list_nth_mut_loop(mut ls: &mut List, mut i: u32) -> &mut T { + while let List::Cons(x, tl) = ls { + if i == 0 { + return x; + } else { + ls = tl; + i -= 1; + } + } + panic!() +} + +/// Same as [list_nth_mut_loop] but with shared borrows +pub fn list_nth_shared_loop(mut ls: &List, mut i: u32) -> &T { + while let List::Cons(x, tl) = ls { + if i == 0 { + return x; + } else { + ls = tl; + i -= 1; + } + } + panic!() +} + +pub fn get_elem_mut(slots: &mut Vec>, x: usize) -> &mut usize { + let mut ls = &mut slots[0]; + loop { + match ls { + List::Nil => panic!(), + List::Cons(y, tl) => { + if *y == x { + return y; + } else { + ls = tl; + } + } + } + } +} + +pub fn get_elem_shared(slots: &Vec>, x: usize) -> &usize { + let mut ls = &slots[0]; + loop { + match ls { + List::Nil => panic!(), + List::Cons(y, tl) => { + if *y == x { + return y; + } else { + ls = tl; + } + } + } + } +} + +pub fn id_mut(ls: &mut List) -> &mut List { + ls +} + +pub fn id_shared(ls: &List) -> &List { + ls +} + +/// Small variation of [list_nth_mut_loop] +pub fn list_nth_mut_loop_with_id(ls: &mut List, mut i: u32) -> &mut T { + let mut ls = id_mut(ls); + while let List::Cons(x, tl) = ls { + if i == 0 { + return x; + } else { + ls = tl; + i -= 1; + } + } + panic!() +} + +/// Small variation of [list_nth_shared_loop] +pub fn list_nth_shared_loop_with_id(ls: &List, mut i: u32) -> &T { + let mut ls = id_shared(ls); + while let List::Cons(x, tl) = ls { + if i == 0 { + return x; + } else { + ls = tl; + i -= 1; + } + } + panic!() +} + +/// Same as [list_nth_mut] but on a pair of lists. +/// +/// This test checks that we manage to decompose a loop into disjoint regions. +pub fn list_nth_mut_loop_pair<'a, 'b, T>( + mut ls0: &'a mut List, + mut ls1: &'b mut List, + mut i: u32, +) -> (&'a mut T, &'b mut T) { + loop { + match (ls0, ls1) { + (List::Nil, _) | (_, List::Nil) => { + panic!() + } + (List::Cons(x0, tl0), List::Cons(x1, tl1)) => { + if i == 0 { + return (x0, x1); + } else { + ls0 = tl0; + ls1 = tl1; + i -= 1; + } + } + } + } +} + +/// Same as [list_nth_mut_loop_pair] but with shared borrows. +pub fn list_nth_shared_loop_pair<'a, 'b, T>( + mut ls0: &'a List, + mut ls1: &'b List, + mut i: u32, +) -> (&'a T, &'b T) { + loop { + match (ls0, ls1) { + (List::Nil, _) | (_, List::Nil) => { + panic!() + } + (List::Cons(x0, tl0), List::Cons(x1, tl1)) => { + if i == 0 { + return (x0, x1); + } else { + ls0 = tl0; + ls1 = tl1; + i -= 1; + } + } + } + } +} + +/// Same as [list_nth_mut_loop_pair] but this time we force the two loop +/// regions to be merged. +pub fn list_nth_mut_loop_pair_merge<'a, T>( + mut ls0: &'a mut List, + mut ls1: &'a mut List, + mut i: u32, +) -> (&'a mut T, &'a mut T) { + while let (List::Cons(x0, tl0), List::Cons(x1, tl1)) = (ls0, ls1) { + if i == 0 { + return (x0, x1); + } else { + ls0 = tl0; + ls1 = tl1; + i -= 1; + } + } + panic!() +} + +/// Same as [list_nth_mut_loop_pair_merge] but with shared borrows. +pub fn list_nth_shared_loop_pair_merge<'a, T>( + mut ls0: &'a List, + mut ls1: &'a List, + mut i: u32, +) -> (&'a T, &'a T) { + while let (List::Cons(x0, tl0), List::Cons(x1, tl1)) = (ls0, ls1) { + if i == 0 { + return (x0, x1); + } else { + ls0 = tl0; + ls1 = tl1; + i -= 1; + } + } + panic!() +} + +/// Mixing mutable and shared borrows. +pub fn list_nth_mut_shared_loop_pair<'a, 'b, T>( + mut ls0: &'a mut List, + mut ls1: &'b List, + mut i: u32, +) -> (&'a mut T, &'b T) { + while let (List::Cons(x0, tl0), List::Cons(x1, tl1)) = (ls0, ls1) { + if i == 0 { + return (x0, x1); + } else { + ls0 = tl0; + ls1 = tl1; + i -= 1; + } + } + panic!() +} + +/// Same as [list_nth_mut_shared_loop_pair] but this time we force the two loop +/// regions to be merged. +pub fn list_nth_mut_shared_loop_pair_merge<'a, T>( + mut ls0: &'a mut List, + mut ls1: &'a List, + mut i: u32, +) -> (&'a mut T, &'a T) { + while let (List::Cons(x0, tl0), List::Cons(x1, tl1)) = (ls0, ls1) { + if i == 0 { + return (x0, x1); + } else { + ls0 = tl0; + ls1 = tl1; + i -= 1; + } + } + panic!() +} + +/// Same as [list_nth_mut_shared_loop_pair], but we switched the positions of +/// the mutable and shared borrows. +pub fn list_nth_shared_mut_loop_pair<'a, 'b, T>( + mut ls0: &'a List, + mut ls1: &'b mut List, + mut i: u32, +) -> (&'a T, &'b mut T) { + while let (List::Cons(x0, tl0), List::Cons(x1, tl1)) = (ls0, ls1) { + if i == 0 { + return (x0, x1); + } else { + ls0 = tl0; + ls1 = tl1; + i -= 1; + } + } + panic!() +} + +/// Same as [list_nth_mut_shared_loop_pair_merge], but we switch the positions of +/// the mutable and shared borrows. +pub fn list_nth_shared_mut_loop_pair_merge<'a, T>( + mut ls0: &'a List, + mut ls1: &'a mut List, + mut i: u32, +) -> (&'a T, &'a mut T) { + while let (List::Cons(x0, tl0), List::Cons(x1, tl1)) = (ls0, ls1) { + if i == 0 { + return (x0, x1); + } else { + ls0 = tl0; + ls1 = tl1; + i -= 1; + } + } + panic!() +} + +// We do not use the input borrow inside the loop +#[allow(clippy::empty_loop)] +pub fn ignore_input_mut_borrow(_a: &mut u32, mut i: u32) { + while i > 0 { + i -= 1; + } +} + +// We do not use the input borrow inside the loop +#[allow(clippy::empty_loop)] +pub fn incr_ignore_input_mut_borrow(a: &mut u32, mut i: u32) { + *a += 1; + while i > 0 { + i -= 1; + } +} + +// We do not use the input borrow inside the loop +#[allow(clippy::empty_loop)] +pub fn ignore_input_shared_borrow(_a: &mut u32, mut i: u32) { + while i > 0 { + i -= 1; + } +} diff --git a/tests/src/nested_borrows.rs b/tests/src/nested_borrows.rs new file mode 100644 index 00000000..94db0cec --- /dev/null +++ b/tests/src/nested_borrows.rs @@ -0,0 +1,181 @@ +//! This module contains functions with nested borrows in their signatures. + +pub fn id_mut_mut<'a, 'b, T>(x: &'a mut &'b mut T) -> &'a mut &'b mut T { + x +} + +pub fn id_mut_pair<'a, T>(x: &'a mut (&'a mut T, u32)) -> &'a mut (&'a mut T, u32) { + x +} + +pub fn id_mut_pair_test1() { + let mut x: u32 = 0; + let px = &mut x; + let mut p = (px, 1); + let pp0 = &mut p; + let pp1 = id_mut_pair(pp0); + let mut y = 2; + *pp1 = (&mut y, 3); +} + +pub fn id_mut_mut_pair<'a, T>( + x: &'a mut &'a mut (&'a mut T, u32), +) -> &'a mut &'a mut (&'a mut T, u32) { + x +} + +pub fn id_mut_mut_mut_same<'a, T>(x: &'a mut &'a mut &'a mut u32) -> &'a mut &'a mut &'a mut u32 { + x +} + +pub fn id_borrow1<'a, 'b, 'c>(_x: &'a mut &'b u32, _y: &'a &'a mut u32) { + () +} + +/// For symbolic execution: testing what happens with several abstractions. +pub fn id_mut_mut_test1() { + let mut x = 0; + let mut px = &mut x; + let ppx = &mut px; + let ppy = id_mut_mut(ppx); + **ppy = 1; + // Ending one abstraction + assert!(*px == 1); + // Ending the other abstraction + assert!(x == 1); +} + +/* +/// For symbolic execution: testing what happens with several abstractions. +/// This case is a bit trickier, because we modify the borrow graph through +/// a value returned by a function call. +/// TODO: not supported! We overwrite a borrow in a returned value. +pub fn id_mut_mut_test2() { + let mut x = 0; + let mut px = &mut x; + let ppx = &mut px; + let ppy = id_mut_mut(ppx); + **ppy = 1; + // This time, we replace one of the borrows + let mut y = 2; + let py = &mut y; + *ppy = py; + // Ending one abstraction + assert!(*px == 2); + *px = 3; + // Ending the other abstraction + assert!(x == 1); + assert!(y == 3); +} +*/ + +/* +/// For symbolic execution: testing what happens with several abstractions. +/// See what happens when chaining function calls. +/// TODO: not supported! We overwrite a borrow in a returned value. +pub fn id_mut_mut_test3() { + let mut x = 0; + let mut px = &mut x; + let ppx = &mut px; + let ppy = id_mut_mut(ppx); // &'a mut &'b mut i32 + **ppy = 1; + let ppz = id_mut_mut(ppy); // &'c mut &'b mut i32 + **ppz = 2; + // End 'a and 'c + assert!(*px == 2); + // End 'b (2 abstractions at once) + assert!(x == 2); +}*/ + +/* +/// For symbolic execution: testing what happens with several abstractions. +/// See what happens when chaining function calls. +/// This one is slightly more complex than the previous one. +pub fn id_mut_mut_test4() { + let mut x = 0; + let mut px = &mut x; + let ppx = &mut px; + let ppy = id_mut_mut(ppx); // &'a mut &'b mut i32 + **ppy = 1; + let ppz = id_mut_mut(ppy); // &'c mut &'b mut i32 + **ppz = 2; + // End 'c + assert!(**ppy == 2); + // End 'a + assert!(*px == 2); + // End 'b (2 abstractions at once) + assert!(x == 2); +} +*/ + +fn id<'a, T>(x: &'a mut T) -> &'a mut T { + x +} + +/// Checking projectors over symbolic values +pub fn test_borrows1() { + let mut x = 3; + let y = id(&mut x); + let z = id(y); + // We do not write a statement which would expand `z` on purpose: + // we want to test that the handling of non-expanded symbolic values + // is correct + assert!(x == 3); +} + +fn id_pair<'a, 'b, T>(x: &'a mut T, y: &'b mut T) -> (&'a mut T, &'b mut T) { + (x, y) +} + +/// Similar to the previous one +pub fn test_borrows2() { + let mut x = 3; + let mut y = 4; + let z = id_pair(&mut x, &mut y); + // We do not write a statement which would expand `z` on purpose: + // we want to test that the handling of non-expanded symbolic values + // is correct + assert!(x == 3); + assert!(y == 4); +} + +/// input type: 'b must last longer than 'a +/// output type: 'a must last longer than 'b +/// So: 'a = 'b, and the function is legal. +pub fn nested_mut_borrows1<'a, 'b>(x: &'a mut &'b mut u32) -> &'b mut &'a mut u32 { + x +} + +pub fn nested_shared_borrows1<'a, 'b>(x: &'a &'b u32) -> &'a &'b u32 { + x +} + +pub fn nested_borrows1<'a, 'b>(x: &'a mut &'b u32) -> &'a mut &'b u32 { + x +} + +pub fn nested_borrows2<'a, 'b>(x: &'a &'b mut u32) -> &'a &'b mut u32 { + x +} + +fn nested_borrows1_test1() { + let x = 0; + let mut px = &x; + let ppx = &mut px; + let ppy = nested_borrows1(ppx); + assert!(**ppy == 0); + assert!(x == 0); +} + +fn nested_borrows1_test2<'a, 'b>(x: &'a mut &'b u32) -> &'a mut &'b u32 { + nested_borrows1(x) +} + +fn nested_borrows2_test1() { + let mut x = 0; + let px = &mut x; + let ppx = &px; + let ppy = nested_borrows2(ppx); + assert!(**ppy == 0); + assert!(x == 0); +} diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs new file mode 100644 index 00000000..9a7604e6 --- /dev/null +++ b/tests/src/no_nested_borrows.rs @@ -0,0 +1,491 @@ +//! This module doesn't contain **functions which use nested borrows in their +//! signatures**, and doesn't contain functions with loops. + +pub struct Pair { + pub x: T1, + pub y: T2, +} + +pub enum List { + Cons(T, Box>), + Nil, +} + +/// Sometimes, enumerations with one variant are not treated +/// the same way as the other variants (for example, downcasts +/// are not always introduced). +/// A downcast is the cast of an enum to a specific variant, like +/// in the left value of: +/// `((_0 as Right).0: T2) = move _1;` +pub enum One { + One(T1), +} + +/// Truely degenerate case +/// Instantiations of this are encoded as constant values by rust. +pub enum EmptyEnum { + Empty, +} + +/// Enumeration (several variants with no parameters) +/// Those are not encoded as constant values. +pub enum Enum { + Variant1, + Variant2, +} + +/// Degenerate struct +/// Instanciations of this are encoded as constant values by rust. +pub struct EmptyStruct {} + +pub enum Sum { + Left(T1), + Right(T2), +} + +pub fn cast_u32_to_i32(x: u32) -> i32 { + x as i32 +} + +pub fn cast_bool_to_i32(x: bool) -> i32 { + x as i32 +} + +#[allow(clippy::unnecessary_cast)] +pub fn cast_bool_to_bool(x: bool) -> bool { + x as bool +} + +#[allow(unused_variables)] +pub fn test2() { + let x: u32 = 23; + let y: u32 = 44; + let z = x + y; + let p: Pair = Pair { x, y: z }; + let s: Sum = Sum::Right(true); + let o: One = One::One(3); + let e0 = EmptyEnum::Empty; + let e1 = e0; + let enum0 = Enum::Variant1; +} + +pub fn get_max(x: u32, y: u32) -> u32 { + if x >= y { + x + } else { + y + } +} + +pub fn test3() { + let x = get_max(4, 3); + let y = get_max(10, 11); + let z = x + y; + assert!(z == 15); +} + +pub fn test_neg1() { + let x: i32 = 3; + let y = -x; + assert!(y == -3); +} + +/// Testing nested references. +pub fn refs_test1() { + let mut x = 0; + let mut px = &mut x; + let ppx = &mut px; + **ppx = 1; + // The interesting thing happening here is that the borrow of x is inside + // the borrow of px: ending the borrow of x requires ending the borrow of + // px first. + assert!(x == 1); +} + +pub fn refs_test2() { + let mut x = 0; + let mut y = 1; + let mut px = &mut x; + let py = &mut y; + let ppx = &mut px; + *ppx = py; + **ppx = 2; + assert!(*px == 2); + assert!(x == 0); + assert!(*py == 2); + assert!(y == 2); +} + +/// Box creation +#[allow(unused_variables)] +pub fn test_list1() { + let l: List = List::Cons(0, Box::new(List::Nil)); +} + +/// Box deref +pub fn test_box1() { + use std::ops::Deref; + use std::ops::DerefMut; + let mut b: Box = Box::new(0); + let x = b.deref_mut(); + *x = 1; + let x = b.deref(); + assert!(*x == 1); +} + +pub fn copy_int(x: i32) -> i32 { + x +} + +/// Just checking the parameters given to unreachable +/// Rk.: the input parameter prevents using the function as a unit test. +pub fn test_unreachable(b: bool) { + if b { + unreachable!(); + } +} + +/// Just checking the parameters given to panic +/// Rk.: the input parameter prevents using the function as a unit test. +pub fn test_panic(b: bool) { + if b { + panic!("Panicked!"); + } +} + +// Just testing that shared loans are correctly handled +pub fn test_copy_int() { + let x = 0; + let px = &x; + let y = copy_int(x); + assert!(*px == y); +} + +pub fn is_cons(l: &List) -> bool { + match l { + List::Cons(_, _) => true, + List::Nil => false, + } +} + +pub fn test_is_cons() { + let l: List = List::Cons(0, Box::new(List::Nil)); + + assert!(is_cons(&l)); +} + +pub fn split_list(l: List) -> (T, List) { + match l { + List::Cons(hd, tl) => (hd, *tl), + _ => panic!(), + } +} + +#[allow(unused_variables)] +pub fn test_split_list() { + let l: List = List::Cons(0, Box::new(List::Nil)); + + let (hd, tl) = split_list(l); + assert!(hd == 0); +} + +pub fn choose<'a, T>(b: bool, x: &'a mut T, y: &'a mut T) -> &'a mut T { + if b { + x + } else { + y + } +} + +pub fn choose_test() { + let mut x = 0; + let mut y = 0; + let z = choose(true, &mut x, &mut y); + *z += 1; + assert!(*z == 1); + // drop(z) + assert!(x == 1); + assert!(y == 0); +} + +/// Test with a char literal - testing serialization +pub fn test_char() -> char { + 'a' +} + +/// Mutually recursive types +pub enum Tree { + Leaf(T), + Node(T, NodeElem, Box>), +} + +pub enum NodeElem { + Cons(Box>, Box>), + Nil, +} + +/* +// TODO: those definitions requires semantic termination (breaks the Coq backend +// because we don't use fuel in this case). + +/// Mutually recursive functions +pub fn even(x: u32) -> bool { + if x == 0 { + true + } else { + odd(x - 1) + } +} + +pub fn odd(x: u32) -> bool { + if x == 0 { + false + } else { + even(x - 1) + } +} + +pub fn test_even_odd() { + assert!(even(0)); + assert!(even(4)); + assert!(odd(1)); + assert!(odd(5)); +} +*/ + +#[allow(clippy::needless_lifetimes)] +pub fn list_length<'a, T>(l: &'a List) -> u32 { + match l { + List::Nil => 0, + List::Cons(_, l1) => 1 + list_length(l1), + } +} + +#[allow(clippy::needless_lifetimes)] +pub fn list_nth_shared<'a, T>(l: &'a List, i: u32) -> &'a T { + match l { + List::Nil => { + panic!() + } + List::Cons(x, tl) => { + if i == 0 { + x + } else { + list_nth_shared(tl, i - 1) + } + } + } +} + +#[allow(clippy::needless_lifetimes)] +pub fn list_nth_mut<'a, T>(l: &'a mut List, i: u32) -> &'a mut T { + match l { + List::Nil => { + panic!() + } + List::Cons(x, tl) => { + if i == 0 { + x + } else { + list_nth_mut(tl, i - 1) + } + } + } +} + +/// In-place list reversal - auxiliary function +pub fn list_rev_aux(li: List, mut lo: List) -> List { + match li { + List::Nil => lo, + List::Cons(hd, mut tl) => { + let next = *tl; + *tl = lo; + lo = List::Cons(hd, tl); + list_rev_aux(next, lo) + } + } +} + +/// In-place list reversal +#[allow(clippy::needless_lifetimes)] +pub fn list_rev<'a, T>(l: &'a mut List) { + let li = std::mem::replace(l, List::Nil); + *l = list_rev_aux(li, List::Nil); +} + +pub fn test_list_functions() { + let mut ls = List::Cons( + 0, + Box::new(List::Cons(1, Box::new(List::Cons(2, Box::new(List::Nil))))), + ); + assert!(list_length(&ls) == 3); + assert!(*list_nth_shared(&ls, 0) == 0); + assert!(*list_nth_shared(&ls, 1) == 1); + assert!(*list_nth_shared(&ls, 2) == 2); + let x = list_nth_mut(&mut ls, 1); + *x = 3; + assert!(*list_nth_shared(&ls, 0) == 0); + assert!(*list_nth_shared(&ls, 1) == 3); // Updated + assert!(*list_nth_shared(&ls, 2) == 2); +} + +pub fn id_mut_pair1<'a, T1, T2>(x: &'a mut T1, y: &'a mut T2) -> (&'a mut T1, &'a mut T2) { + (x, y) +} + +pub fn id_mut_pair2<'a, T1, T2>(p: (&'a mut T1, &'a mut T2)) -> (&'a mut T1, &'a mut T2) { + p +} + +pub fn id_mut_pair3<'a, 'b, T1, T2>(x: &'a mut T1, y: &'b mut T2) -> (&'a mut T1, &'b mut T2) { + (x, y) +} + +pub fn id_mut_pair4<'a, 'b, T1, T2>(p: (&'a mut T1, &'b mut T2)) -> (&'a mut T1, &'b mut T2) { + p +} + +/// Testing constants (some constants are hard to retrieve from MIR, because +/// they are compiled to very low values). +/// We resort to the following structure to make rustc generate constants... +pub struct StructWithTuple { + p: (T1, T2), +} + +pub fn new_tuple1() -> StructWithTuple { + StructWithTuple { p: (1, 2) } +} + +pub fn new_tuple2() -> StructWithTuple { + StructWithTuple { p: (1, 2) } +} + +pub fn new_tuple3() -> StructWithTuple { + StructWithTuple { p: (1, 2) } +} + +/// Similar to [StructWithTuple] +pub struct StructWithPair { + p: Pair, +} + +pub fn new_pair1() -> StructWithPair { + // This actually doesn't make rustc generate a constant... + // I guess it only happens for tuples. + StructWithPair { + p: Pair { x: 1, y: 2 }, + } +} + +pub fn test_constants() { + assert!(new_tuple1().p.0 == 1); + assert!(new_tuple2().p.0 == 1); + assert!(new_tuple3().p.0 == 1); + assert!(new_pair1().p.x == 1); +} + +/// This assignment is trickier than it seems +#[allow(unused_assignments)] +pub fn test_weird_borrows1() { + let mut x = 0; + let mut px = &mut x; + // Context: + // x -> [l0] + // px -> &mut l0 (0:i32) + + px = &mut (*px); +} + +pub fn test_mem_replace(px: &mut u32) { + let y = std::mem::replace(px, 1); + assert!(y == 0); + *px = 2; +} + +/// Check that matching on borrowed values works well. +pub fn test_shared_borrow_bool1(b: bool) -> u32 { + // Create a shared borrow of b + let _pb = &b; + // Match on b + if b { + 0 + } else { + 1 + } +} + +/// Check that matching on borrowed values works well. +/// Testing the concrete execution here. +pub fn test_shared_borrow_bool2() -> u32 { + let b = true; + // Create a shared borrow of b + let _pb = &b; + // Match on b + if b { + 0 + } else { + 1 + } +} + +/// Check that matching on borrowed values works well. +/// In case of enumerations, we need to strip the outer loans before evaluating +/// the discriminant. +pub fn test_shared_borrow_enum1(l: List) -> u32 { + // Create a shared borrow of l + let _pl = &l; + // Match on l - must ignore the shared loan + match l { + List::Nil => 0, + List::Cons(_, _) => 1, + } +} + +/// Check that matching on borrowed values works well. +/// Testing the concrete execution here. +pub fn test_shared_borrow_enum2() -> u32 { + let l: List = List::Nil; + // Create a shared borrow of l + let _pl = &l; + // Match on l - must ignore the shared loan + match l { + List::Nil => 0, + List::Cons(_, _) => 1, + } +} + +pub fn incr(x: &mut u32) { + *x += 1; +} + +pub fn call_incr(mut x: u32) -> u32 { + incr(&mut x); + x +} + +pub fn read_then_incr(x: &mut u32) -> u32 { + let r = *x; + *x += 1; + r +} + +pub struct Tuple(T1, T2); + +pub fn use_tuple_struct(x: &mut Tuple) { + x.0 = 1; +} + +pub fn create_tuple_struct(x: u32, y: u64) -> Tuple { + Tuple(x, y) +} + +/// Structure with one field +pub struct IdType(T); + +pub fn use_id_type(x: IdType) -> T { + x.0 +} + +pub fn create_id_type(x: T) -> IdType { + IdType(x) +} diff --git a/tests/src/paper.rs b/tests/src/paper.rs new file mode 100644 index 00000000..156f13ab --- /dev/null +++ b/tests/src/paper.rs @@ -0,0 +1,82 @@ +//! The examples from the ICFP submission, all in one place. + +// 2.1 +pub fn ref_incr(x: &mut i32) { + *x = *x + 1; +} + +pub fn test_incr() { + let mut x = 0i32; + ref_incr(&mut x); + assert!(x == 1); +} + +// 2.2 +pub fn choose<'a, T>(b: bool, x: &'a mut T, y: &'a mut T) -> &'a mut T { + if b { + return x; + } else { + return y; + } +} + +pub fn test_choose() { + let mut x = 0; + let mut y = 0; + let z = choose(true, &mut x, &mut y); + *z = *z + 1; + assert!(*z == 1); + assert!(x == 1); + assert!(y == 0); +} + +// 2.3 + +pub enum List { + Cons(T, Box>), + Nil, +} +use List::Cons; +use List::Nil; + +pub fn list_nth_mut<'a, T>(l: &'a mut List, i: u32) -> &'a mut T { + match l { + Nil => { + panic!() + } + Cons(x, tl) => { + if i == 0 { + return x; + } else { + return list_nth_mut(tl, i - 1); + } + } + } +} + +pub fn sum(l: &List) -> i32 { + match l { + Nil => { + return 0; + } + Cons(x, tl) => { + return *x + sum(tl); + } + } +} + +pub fn test_nth() { + let mut l = Cons(1, Box::new(Cons(2, Box::new(Cons(3, Box::new(Nil)))))); + let x = list_nth_mut(&mut l, 2); + *x = *x + 1; + assert!(sum(&l) == 7); +} + +// 4.3 +pub fn call_choose(mut p: (u32, u32)) -> u32 { + let px = &mut p.0; + let py = &mut p.1; + let pz = choose(true, px, py); + *pz = *pz + 1; + return p.0; +} diff --git a/tests/src/polonius_list.rs b/tests/src/polonius_list.rs new file mode 100644 index 00000000..8c64110d --- /dev/null +++ b/tests/src/polonius_list.rs @@ -0,0 +1,27 @@ +#![allow(dead_code)] + +pub enum List { + Cons(T, Box>), + Nil, +} + +/// An example which comes from the b-epsilon tree. +/// +/// Returns a mutable borrow to the first portion of the list where we +/// can find [x]. This allows to do in-place modifications (insertion, filtering) +/// in a natural manner (this piece of code was inspired by the C++ BeTree). +pub fn get_list_at_x<'a>(ls: &'a mut List, x: u32) -> &'a mut List { + match ls { + List::Nil => { + // We reached the end: just return it + ls + } + List::Cons(hd, tl) => { + if *hd == x { + ls // Doing this requires NLL + } else { + get_list_at_x(tl, x) + } + } + } +} diff --git a/tests/src/traits.rs b/tests/src/traits.rs new file mode 100644 index 00000000..27c90586 --- /dev/null +++ b/tests/src/traits.rs @@ -0,0 +1,341 @@ +pub trait BoolTrait { + // Required method + fn get_bool(&self) -> bool; + + // Provided method + fn ret_true(&self) -> bool { + true + } +} + +impl BoolTrait for bool { + fn get_bool(&self) -> bool { + *self + } +} + +pub fn test_bool_trait_bool(x: bool) -> bool { + x.get_bool() && x.ret_true() +} + +#[allow(clippy::redundant_pattern_matching)] +impl BoolTrait for Option { + fn get_bool(&self) -> bool { + match self { + Option::Some(_) => true, + Option::None => false, + } + } +} + +pub fn test_bool_trait_option(x: Option) -> bool { + x.get_bool() && x.ret_true() +} + +pub fn test_bool_trait(x: T) -> bool { + x.get_bool() +} + +pub trait ToU64 { + fn to_u64(self) -> u64; +} + +impl ToU64 for u64 { + fn to_u64(self) -> u64 { + self + } +} + +impl ToU64 for (A, A) { + fn to_u64(self) -> u64 { + self.0.to_u64() + self.1.to_u64() + } +} + +pub fn f(x: (T, T)) -> u64 { + x.to_u64() +} + +pub fn g(x: (T, T)) -> u64 +where + (T, T): ToU64, +{ + x.to_u64() +} + +pub fn h0(x: u64) -> u64 { + x.to_u64() +} + +pub struct Wrapper { + x: T, +} + +impl ToU64 for Wrapper { + fn to_u64(self) -> u64 { + self.x.to_u64() + } +} + +pub fn h1(x: Wrapper) -> u64 { + x.to_u64() +} + +pub fn h2(x: Wrapper) -> u64 { + x.to_u64() +} + +pub trait ToType { + fn to_type(self) -> T; +} + +impl ToType for u64 { + fn to_type(self) -> bool { + self > 0 + } +} + +pub trait OfType { + fn of_type>(x: T) -> Self + where + Self: std::marker::Sized; +} + +pub fn h3>(y: T2) -> T1 { + T1::of_type(y) +} + +// Checking what happens if we move trait clauses from a method to its enclosing block +pub trait OfTypeBis> +where + Self: std::marker::Sized, +{ + fn of_type(x: T) -> Self + where + Self: std::marker::Sized; +} + +pub fn h4, T2: ToType>(y: T2) -> T1 { + T1::of_type(y) +} + +pub struct TestType(T); + +// Checking what happens with nested blocks +impl TestType { + pub fn test(&self, x: T) -> bool { + struct TestType1(u64); + trait TestTrait { + fn test(&self) -> bool; + } + + // Remark: we can't write: impl TestTrait for TestType, + // we have to use a *local* parameter (can't use the outer T). + // In other words: the parameters used in the items inside + // an impl must be bound by the impl block (can't come from outer + // blocks). + + impl TestTrait for TestType1 { + fn test(&self) -> bool { + self.0 > 1 + } + } + + let x = x.to_u64(); + let y = TestType1(0); + x > 0 && y.test() + } +} + +pub struct BoolWrapper(pub bool); + +impl ToType for BoolWrapper +where + bool: ToType, +{ + fn to_type(self) -> T { + self.0.to_type() + } +} + +pub trait WithConstTy { + const LEN1: usize; + // Testing default values + const LEN2: usize = 32; + + type V; + type W: ToU64; + + // Below: we can't use [Self::Len1] in the type of the array. + // Probably because of dyn traits... + fn f(x: &mut Self::W, y: &[u8; LEN]); +} + +impl WithConstTy<32> for bool { + const LEN1: usize = 12; + + type V = u8; + type W = u64; + + fn f(_: &mut Self::W, _: &[u8; 32]) {} +} + +pub fn use_with_const_ty1>() -> usize { + H::LEN1 +} + +pub fn use_with_const_ty2>(_: H::W) {} + +pub fn use_with_const_ty3>(x: H::W) -> u64 { + x.to_u64() +} + +pub fn test_where1<'a, T: 'a>(_x: &'a T) {} +pub fn test_where2>(_x: T::V) {} + +// Below: testing super traits. +// +// Actually, this comes for free: ChildTrait : ParentTrait just adds a trait +// clause for Self: `Self : ParentTrait`. +pub trait ParentTrait0 { + type W; + fn get_name(&self) -> String; + fn get_w(&self) -> Self::W; +} +pub trait ParentTrait1 {} +pub trait ChildTrait: ParentTrait0 + ParentTrait1 {} + +// But we still need to correctly reference the traits +pub fn test_child_trait1(x: &T) -> String { + x.get_name() +} + +pub fn test_child_trait2(x: &T) -> T::W { + x.get_w() +} + +// Checking if the order has an importance (we use U::W before we declare that +// U:ParentTrait0) +pub fn order1, U: ParentTrait0>() {} + +/* */ +pub trait ChildTrait1: ParentTrait1 {} + +impl ParentTrait1 for usize {} +impl ChildTrait1 for usize {} + +/* [IntoIterator] is interesting because of the condition [Item = Self::Item] +for the [IntoIter] associated type. */ +pub trait Iterator { + type Item; +} + +pub trait IntoIterator { + type Item; + type IntoIter: Iterator; + + // Required method + fn into_iter(self) -> Self::IntoIter; +} + +/* The traits below are inspired by [Try] and [FromResidual]. + + The reference to `Self as Try` in the `FromResidual` clause used to + cause a bug. +*/ +trait Try: FromResidual<::Residual> { + type Residual; +} + +trait FromResidual {} + +pub trait WithTarget { + type Target; +} + +pub trait ParentTrait2 { + type U: WithTarget; +} + +pub trait ChildTrait2: ParentTrait2 { + fn convert(x: Self::U) -> ::Target; +} + +impl WithTarget for u32 { + type Target = u32; +} + +impl ParentTrait2 for u32 { + type U = u32; +} + +impl ChildTrait2 for u32 { + fn convert(x: u32) -> u32 { + x + } +} + +/* +// This one requires a lot of traits +pub fn test_enumerate(x: usize) { + for _ in 0..x {} +} +*/ + +/* Custom function pointers */ +pub trait CFnOnce { + type Output; + + fn call_once(self, args: Args) -> Self::Output; +} + +pub trait CFnMut: CFnOnce { + fn call_mut(&mut self, args: Args) -> Self::Output; +} + +pub trait CFn: CFnMut { + fn call(&self, args: Args) -> Self::Output; +} + +pub trait GetTrait { + type W; + fn get_w(&self) -> Self::W; +} + +pub fn test_get_trait(x: &T) -> T::W { + x.get_w() +} + +// Constants with generics +pub trait Trait { + const LEN: usize; +} + +impl Trait for [T; N] { + const LEN: usize = N; +} + +impl Trait for Wrapper { + const LEN: usize = 0; +} + +pub fn use_wrapper_len() -> usize { + Wrapper::::LEN +} + +pub struct Foo { + pub x: T, + pub y: U, +} + +impl Foo { + pub const FOO: Result = Err(0); +} + +pub fn use_foo1() -> Result { + Foo::::FOO +} + +pub fn use_foo2() -> Result { + Foo::::FOO +} diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index d3fe8836..8b4a4208 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -12,7 +12,7 @@ type test_case = { (* Run Aeneas on a specific input with the given options *) let run_test env case = let concat_path = List.fold_left Filename.concat "" in - let input_file = concat_path [ env.llbc_dir; "llbc"; case.name ] ^ ".llbc" in + let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in let args = [| -- cgit v1.3.1 From 3a380f990d0f202ee19bd163726ff5fc63181ae7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 14:38:50 +0200 Subject: Use runner to generate llbc --- Makefile | 53 +++--------------- flake.nix | 33 +++++------ tests/test_runner/run_test.ml | 124 +++++++++++++++++++++++++++++++++++------- 3 files changed, 126 insertions(+), 84 deletions(-) (limited to 'tests/test_runner') diff --git a/Makefile b/Makefile index b9aaf97c..fccca9b1 100644 --- a/Makefile +++ b/Makefile @@ -19,8 +19,7 @@ TEST_RUNNER_EXE ?= $(PWD)/bin/test_runner CHARON_EXE ?= $(PWD)/charon/bin/charon # The user can specify additional translation options for Aeneas. -# In CI we activate the (expensive) sanity checks. -OPTIONS ?= +AENEAS_OPTIONS ?= CHARON_OPTIONS ?= # The directory thta contains the rust source files for tests. @@ -28,7 +27,7 @@ INPUTS_DIR ?= tests/src # The directory where to look for the .llbc files. LLBC_DIR ?= $(PWD)/tests/llbc -# In CI, we enforce formatting and we don't regenerate llbc files. +# In CI, we enforce formatting and activate the (expensive) sanity checks. IN_CI ?= #################################### @@ -169,53 +168,19 @@ verify: ifdef IN_CI # In CI we do extra sanity checks. -test-%: OPTIONS += -checks +test-%: AENEAS_OPTIONS += -checks +else +test-%: check-charon endif -# Translate the given llbc file to available backends. The test runner decides +# Translate the given rust file to available backends. The test runner decides # which backends to use and sets test-specific options. .PHONY: test-% -test-%: TEST_NAME = $* -test-%: $(LLBC_DIR)/%.llbc - $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(LLBC_DIR) $(TEST_NAME) $(OPTIONS) +test-%: + $(TEST_RUNNER_EXE) charon $(CHARON_EXE) $(INPUTS_DIR) $(LLBC_DIR) "$*" $(CHARON_OPTIONS) + $(TEST_RUNNER_EXE) aeneas $(AENEAS_EXE) $(LLBC_DIR) "$*" $(AENEAS_OPTIONS) echo "# Test $* done" -# List the `.rs` files in `$(INPUTS_DIR)/` -INDIVIDUAL_RUST_SRCS = $(wildcard $(INPUTS_DIR)/*.rs) -# We test all rust files except this one. -INDIVIDUAL_RUST_SRCS := $(filter-out $(INPUTS_DIR)/hashmap_utils.rs, $(INDIVIDUAL_RUST_SRCS)) -# List the corresponding llbc files. -INDIVIDUAL_LLBCS := $(subst $(INPUTS_DIR)/,$(LLBC_DIR)/,$(patsubst %.rs,%.llbc,$(INDIVIDUAL_RUST_SRCS))) - -.PHONY: generate-llbc -# This depends on `llbc/.llbc` for each `$(INPUTS_DIR)/.rs` we care about, plus the whole-crate test. -generate-llbc: $(INDIVIDUAL_LLBCS) $(LLBC_DIR)/betree_main.llbc - -$(LLBC_DIR)/hashmap_main.llbc: CHARON_OPTIONS += --opaque=hashmap_utils -$(LLBC_DIR)/nested_borrows.llbc: CHARON_OPTIONS += --no-code-duplication -$(LLBC_DIR)/no_nested_borrows.llbc: CHARON_OPTIONS += --no-code-duplication -$(LLBC_DIR)/paper.llbc: CHARON_OPTIONS += --no-code-duplication -$(LLBC_DIR)/constants.llbc: CHARON_OPTIONS += --no-code-duplication -$(LLBC_DIR)/external.llbc: CHARON_OPTIONS += --no-code-duplication -$(LLBC_DIR)/polonius_list.llbc: CHARON_OPTIONS += --polonius -# Possible to add `--no-code-duplication` if we use the optimized MIR -$(LLBC_DIR)/betree_main.llbc: CHARON_OPTIONS += --polonius --opaque=betree_utils --crate betree_main - -ifndef IN_CI -$(LLBC_DIR)/%.llbc: check-charon - -$(LLBC_DIR)/%.llbc: - $(CHARON_EXE) --no-cargo --input $(INPUTS_DIR)/$*.rs --crate $* $(CHARON_OPTIONS) --dest $(LLBC_DIR) -# Special rule for the whole-crate test. -$(LLBC_DIR)/betree_main.llbc: - cd $(INPUTS_DIR)/betree && $(CHARON_EXE) $(CHARON_OPTIONS) --dest $(LLBC_DIR) -else -$(LLBC_DIR)/%.llbc: - @echo 'ERROR: llbc files should be built separately in CI' - @false -endif - - # ============================================================================= # Nix # ============================================================================= diff --git a/flake.nix b/flake.nix index 26689af0..9c918ff9 100644 --- a/flake.nix +++ b/flake.nix @@ -80,6 +80,9 @@ OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors. }; + # This test is a full crate with dependencies. We generate the + # corresponding llbc file here; this function takes care of cargo + # dependencies for us. betree-llbc = charon.extractCrateWithCharon.${system} { name = "betree"; src = ./tests/src/betree; @@ -89,22 +92,6 @@ ./target/debug/betree ''; }; - input-llbcs = pkgs.runCommand "input-llbcs" - { - src = ./tests/src; - makefile = ./Makefile; - buildInputs = [ charon.packages.${system}.rustToolchain charon.packages.${system}.charon ]; - } '' - # Copy the betree output file - mkdir -p $out - cp ${betree-llbc}/llbc/betree_main.llbc $out - - mkdir tests - cp -r $src tests/src - cp $makefile Makefile - # Generate the llbc files - CHARON_EXE="charon" INPUTS_DIR="tests/src" LLBC_DIR="$out" make generate-llbc - ''; # Run the translation on various files. # Make sure we don't need to recompile the package whenever we make @@ -118,19 +105,25 @@ path == toString ./Makefile || pkgs.lib.hasPrefix (toString ./compiler) path || pkgs.lib.hasPrefix (toString ./backends) path - || pkgs.lib.hasPrefix (toString ./tests) path; + || (pkgs.lib.hasPrefix (toString ./tests) path + && !pkgs.lib.hasSuffix ".llbc" path); }; + buildInputs = [ charon.packages.${system}.rustToolchain ]; buildPhase = '' - export LLBC_DIR=${input-llbcs} export AENEAS_EXE=${aeneas}/bin/aeneas + export CHARON_EXE=${charon.packages.${system}.charon}/bin/charon export TEST_RUNNER_EXE=${test_runner}/bin/test_runner + mkdir llbc + export LLBC_DIR=llbc + # Copy over the llbc file we can't generate ourselves. + cp ${betree-llbc}/llbc/betree_main.llbc $LLBC_DIR + # Copy the tests cp -r tests tests-copy + make clean-generated-aeneas # Run the tests with extra sanity checks enabled - # Remark: we could remove the file - make clean-generated-aeneas IN_CI=1 make test-all -j $NIX_BUILD_CORES # Check that there are no differences between the generated tests diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 8b4a4208..d80231d0 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -1,26 +1,26 @@ (* Paths to use for tests *) -type test_env = { aeneas_path : string; llbc_dir : string } +type aeneas_env = { aeneas_path : string; llbc_dir : string } -(* The data for a specific test to run *) -type test_case = { +type charon_env = { + charon_path : string; + inputs_dir : string; + llbc_dir : string; +} + +(* The data for a specific test to run aeneas on *) +type aeneas_test_case = { name : string; backend : string; subdir : string; extra_aeneas_options : string list; } -(* Run Aeneas on a specific input with the given options *) -let run_test env case = - let concat_path = List.fold_left Filename.concat "" in - let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in - let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in - let args = - [| - env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; case.backend; - |] - in - let args = Array.append args (Array.of_list case.extra_aeneas_options) in +(* The data for a specific test to generate llbc for *) +type charon_test_case = { name : string; extra_charon_options : string list } +let concat_path = List.fold_left Filename.concat "" + +let run_command args = (* Debug arguments *) print_string "[test_runner] Running: "; Array.iter @@ -30,15 +30,66 @@ let run_test env case = args; print_endline ""; - (* Run Aeneas *) + (* Run the command *) let pid = - Unix.create_process env.aeneas_path args Unix.stdin Unix.stdout Unix.stderr + Unix.create_process args.(0) args Unix.stdin Unix.stdout Unix.stderr in let _ = Unix.waitpid [] pid in () +(* Run Aeneas on a specific input with the given options *) +let run_aeneas (env : aeneas_env) (case : aeneas_test_case) = + let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in + let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in + let args = + [| + env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; case.backend; + |] + in + let args = Array.append args (Array.of_list case.extra_aeneas_options) in + (* Run Aeneas *) + run_command args + +(* Run Charon on a specific input with the given options *) +let run_charon (env : charon_env) (case : charon_test_case) = + let input_crate = concat_path [ env.inputs_dir; case.name ] in + let input_file = input_crate ^ ".rs" in + if Sys.file_exists input_file then + let args = + [| + env.charon_path; + "--no-cargo"; + "--input"; + input_file; + "--crate"; + case.name; + "--dest"; + env.llbc_dir; + |] + in + let args = Array.append args (Array.of_list case.extra_charon_options) in + (* Run Charon on the rust file *) + run_command args + else if Sys.file_exists input_crate then + match Sys.getenv_opt "IN_CI" with + | None -> + let args = [| env.charon_path; "--dest"; env.llbc_dir |] in + let args = + Array.append args (Array.of_list case.extra_charon_options) + in + (* Run Charon inside the crate *) + Unix.chdir input_crate; + run_command args + | Some _ -> + (* Crates with dependencies must be generated separately in CI. We skip + here and trust that CI takes care to generate the necessary llbc + file. *) + print_endline + "Warn: IN_CI is set; we skip generating llbc files for whole crates" + else failwith ("Neither " ^ input_file ^ " nor " ^ input_crate ^ " exist.") + (* File-specific options *) -let test_options backend test_name = +let aeneas_options_for_test backend test_name = (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *) let use_fuel = match (backend, test_name) with @@ -92,6 +143,27 @@ let test_options backend test_name = let options = List.append extra_options options in options +(* File-specific options *) +let charon_options_for_test test_name = + (* Possible to add `--no-code-duplication` for `hashmap_main` if we use the optimized MIR *) + let no_code_dup = + match test_name with + | "constants" | "external" | "nested_borrows" | "no_nested_borrows" + | "paper" -> + [ "--no-code-duplication" ] + | _ -> [] + in + let extra_options = + (* $(LLBC_DIR)/betree_main.llbc: CHARON_OPTIONS += --polonius --opaque=betree_utils --crate betree_main *) + match test_name with + | "betree_main" -> + [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ] + | "hashmap_main" -> [ "--opaque=hashmap_utils" ] + | "polonius_list" -> [ "--polonius" ] + | _ -> [] + in + List.append no_code_dup extra_options + (* The subdirectory in which to store the outputs. *) (* This reproduces the file layout that was set by the old Makefile. FIXME: cleanup *) let test_subdir backend test_name = @@ -111,7 +183,7 @@ let test_subdir backend test_name = let () = match Array.to_list Sys.argv with (* Ad-hoc argument passing for now. *) - | _exe_path :: aeneas_path :: llbc_dir :: test_name :: options -> + | _exe_path :: "aeneas" :: aeneas_path :: llbc_dir :: test_name :: options -> let tests_env = { aeneas_path; llbc_dir } in (* TODO: reactivate HOL4 once traits are parameterized by their associated types *) let backends = [ "coq"; "lean"; "fstar" ] in @@ -119,11 +191,23 @@ let () = (fun backend -> let subdir = test_subdir backend test_name in let extra_aeneas_options = - List.append (test_options backend test_name) options + List.append (aeneas_options_for_test backend test_name) options in let test_case = { name = test_name; backend; subdir; extra_aeneas_options } in - run_test tests_env test_case) + run_aeneas tests_env test_case) backends + | _exe_path :: "charon" :: charon_path :: inputs_dir :: llbc_dir :: test_name + :: options -> + let tests_env = { charon_path; inputs_dir; llbc_dir } in + let extra_charon_options = + List.append (charon_options_for_test test_name) options + in + (* FIXME: remove this special case *) + let test_name = + if test_name = "betree_main" then "betree" else test_name + in + let test_case = { name = test_name; extra_charon_options } in + run_charon tests_env test_case | _ -> failwith "Incorrect options passed to test runner" -- cgit v1.3.1 From ca045d57b6cc3fc700efe07bfc257231edf814e5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 15:37:01 +0200 Subject: Auto-detect test cases --- Makefile | 29 +++++++++++++---------------- flake.nix | 3 +++ tests/test_runner/dune | 2 +- tests/test_runner/run_test.ml | 38 ++++++++++++++++++++++---------------- 4 files changed, 39 insertions(+), 33 deletions(-) (limited to 'tests/test_runner') diff --git a/Makefile b/Makefile index fccca9b1..8a7701cc 100644 --- a/Makefile +++ b/Makefile @@ -145,27 +145,24 @@ test: build-dev test-all betree-tests betree-tests: cd $(INPUTS_DIR)/betree && $(MAKE) test -.PHONY: test-all -test-all: \ - test-arrays \ - test-betree_main \ - test-bitwise \ - test-constants \ - test-demo \ - test-external \ - test-hashmap \ - test-hashmap_main \ - test-loops \ - test-no_nested_borrows \ - test-paper \ - test-polonius_list \ - test-traits - # Verify the F* files generated by the translation .PHONY: verify verify: cd tests && $(MAKE) all +# List the files and directories in `INPUTS_DIR` +INPUTS_LIST = $(wildcard $(INPUTS_DIR)/*) +# Remove the directory prefix, replace with `test-` +INPUTS_LIST := $(subst $(INPUTS_DIR)/,test-,$(INPUTS_LIST)) +# Remove some tests we don't want to run. +# FIXME: move this information to the file itself +INPUTS_LIST := $(filter-out test-hashmap_utils.rs,$(INPUTS_LIST)) +INPUTS_LIST := $(filter-out test-nested_borrows.rs,$(INPUTS_LIST)) + +# Run all the tests we found. +.PHONY: test-all +test-all: $(INPUTS_LIST) + ifdef IN_CI # In CI we do extra sanity checks. test-%: AENEAS_OPTIONS += -checks diff --git a/flake.nix b/flake.nix index 9c918ff9..caa29fae 100644 --- a/flake.nix +++ b/flake.nix @@ -78,6 +78,9 @@ duneVersion = "3"; src = ./tests/test_runner; OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors. + propagatedBuildInputs = (with ocamlPackages; [ + core_unix + ]); }; # This test is a full crate with dependencies. We generate the diff --git a/tests/test_runner/dune b/tests/test_runner/dune index 7da7a96d..7caf661f 100644 --- a/tests/test_runner/dune +++ b/tests/test_runner/dune @@ -1,4 +1,4 @@ (executable (public_name test_runner) - (libraries unix) + (libraries core_unix.sys_unix unix) (name run_test)) diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index d80231d0..688c81ae 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -16,7 +16,11 @@ type aeneas_test_case = { } (* The data for a specific test to generate llbc for *) -type charon_test_case = { name : string; extra_charon_options : string list } +type charon_test_case = { + name : string; + path : string; + extra_charon_options : string list; +} let concat_path = List.fold_left Filename.concat "" @@ -52,15 +56,14 @@ let run_aeneas (env : aeneas_env) (case : aeneas_test_case) = (* Run Charon on a specific input with the given options *) let run_charon (env : charon_env) (case : charon_test_case) = - let input_crate = concat_path [ env.inputs_dir; case.name ] in - let input_file = input_crate ^ ".rs" in - if Sys.file_exists input_file then + let input_path = concat_path [ env.inputs_dir; case.path ] in + if Sys_unix.is_file_exn input_path then let args = [| env.charon_path; "--no-cargo"; "--input"; - input_file; + input_path; "--crate"; case.name; "--dest"; @@ -70,7 +73,7 @@ let run_charon (env : charon_env) (case : charon_test_case) = let args = Array.append args (Array.of_list case.extra_charon_options) in (* Run Charon on the rust file *) run_command args - else if Sys.file_exists input_crate then + else if Sys.is_directory input_path then match Sys.getenv_opt "IN_CI" with | None -> let args = [| env.charon_path; "--dest"; env.llbc_dir |] in @@ -78,7 +81,7 @@ let run_charon (env : charon_env) (case : charon_test_case) = Array.append args (Array.of_list case.extra_charon_options) in (* Run Charon inside the crate *) - Unix.chdir input_crate; + Unix.chdir input_path; run_command args | Some _ -> (* Crates with dependencies must be generated separately in CI. We skip @@ -86,7 +89,7 @@ let run_charon (env : charon_env) (case : charon_test_case) = file. *) print_endline "Warn: IN_CI is set; we skip generating llbc files for whole crates" - else failwith ("Neither " ^ input_file ^ " nor " ^ input_crate ^ " exist.") + else failwith ("`" ^ input_path ^ "` is not a file or a directory.") (* File-specific options *) let aeneas_options_for_test backend test_name = @@ -154,9 +157,8 @@ let charon_options_for_test test_name = | _ -> [] in let extra_options = - (* $(LLBC_DIR)/betree_main.llbc: CHARON_OPTIONS += --polonius --opaque=betree_utils --crate betree_main *) match test_name with - | "betree_main" -> + | "betree" -> [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ] | "hashmap_main" -> [ "--opaque=hashmap_utils" ] | "polonius_list" -> [ "--polonius" ] @@ -183,8 +185,13 @@ let test_subdir backend test_name = let () = match Array.to_list Sys.argv with (* Ad-hoc argument passing for now. *) - | _exe_path :: "aeneas" :: aeneas_path :: llbc_dir :: test_name :: options -> + | _exe_path :: "aeneas" :: aeneas_path :: llbc_dir :: test_path :: options -> let tests_env = { aeneas_path; llbc_dir } in + let test_name = Filename.remove_extension test_path in + (* FIXME: remove this special case *) + let test_name = + if test_name = "betree" then "betree_main" else test_name + in (* TODO: reactivate HOL4 once traits are parameterized by their associated types *) let backends = [ "coq"; "lean"; "fstar" ] in List.iter @@ -198,16 +205,15 @@ let () = in run_aeneas tests_env test_case) backends - | _exe_path :: "charon" :: charon_path :: inputs_dir :: llbc_dir :: test_name + | _exe_path :: "charon" :: charon_path :: inputs_dir :: llbc_dir :: test_path :: options -> let tests_env = { charon_path; inputs_dir; llbc_dir } in + let test_name = Filename.remove_extension test_path in let extra_charon_options = List.append (charon_options_for_test test_name) options in - (* FIXME: remove this special case *) - let test_name = - if test_name = "betree_main" then "betree" else test_name + let test_case = + { name = test_name; path = test_path; extra_charon_options } in - let test_case = { name = test_name; extra_charon_options } in run_charon tests_env test_case | _ -> failwith "Incorrect options passed to test runner" -- cgit v1.3.1 From d37a302762fef4ea91b88f0ca8feb73612ff5382 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 15:46:45 +0200 Subject: runner: Do both steps of generation at once --- Makefile | 3 +-- tests/test_runner/run_test.ml | 46 ++++++++++++++++++++++--------------------- 2 files changed, 25 insertions(+), 24 deletions(-) (limited to 'tests/test_runner') diff --git a/Makefile b/Makefile index 8a7701cc..88e64646 100644 --- a/Makefile +++ b/Makefile @@ -174,8 +174,7 @@ endif # which backends to use and sets test-specific options. .PHONY: test-% test-%: - $(TEST_RUNNER_EXE) charon $(CHARON_EXE) $(INPUTS_DIR) $(LLBC_DIR) "$*" $(CHARON_OPTIONS) - $(TEST_RUNNER_EXE) aeneas $(AENEAS_EXE) $(LLBC_DIR) "$*" $(AENEAS_OPTIONS) + $(TEST_RUNNER_EXE) $(CHARON_EXE) $(AENEAS_EXE) $(INPUTS_DIR) $(LLBC_DIR) "$*" $(AENEAS_OPTIONS) echo "# Test $* done" # ============================================================================= diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 688c81ae..5eff95af 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -1,8 +1,7 @@ (* Paths to use for tests *) -type aeneas_env = { aeneas_path : string; llbc_dir : string } - -type charon_env = { +type runner_env = { charon_path : string; + aeneas_path : string; inputs_dir : string; llbc_dir : string; } @@ -42,7 +41,7 @@ let run_command args = () (* Run Aeneas on a specific input with the given options *) -let run_aeneas (env : aeneas_env) (case : aeneas_test_case) = +let run_aeneas (env : runner_env) (case : aeneas_test_case) = let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in let args = @@ -55,7 +54,7 @@ let run_aeneas (env : aeneas_env) (case : aeneas_test_case) = run_command args (* Run Charon on a specific input with the given options *) -let run_charon (env : charon_env) (case : charon_test_case) = +let run_charon (env : runner_env) (case : charon_test_case) = let input_path = concat_path [ env.inputs_dir; case.path ] in if Sys_unix.is_file_exn input_path then let args = @@ -81,8 +80,10 @@ let run_charon (env : charon_env) (case : charon_test_case) = Array.append args (Array.of_list case.extra_charon_options) in (* Run Charon inside the crate *) + let old_pwd = Unix.getcwd () in Unix.chdir input_path; - run_command args + run_command args; + Unix.chdir old_pwd | Some _ -> (* Crates with dependencies must be generated separately in CI. We skip here and trust that CI takes care to generate the necessary llbc @@ -185,9 +186,18 @@ let test_subdir backend test_name = let () = match Array.to_list Sys.argv with (* Ad-hoc argument passing for now. *) - | _exe_path :: "aeneas" :: aeneas_path :: llbc_dir :: test_path :: options -> - let tests_env = { aeneas_path; llbc_dir } in + | _exe_path :: charon_path :: aeneas_path :: inputs_dir :: llbc_dir + :: test_path :: aeneas_options -> + let runner_env = { charon_path; aeneas_path; inputs_dir; llbc_dir } in let test_name = Filename.remove_extension test_path in + + let extra_charon_options = charon_options_for_test test_name in + let charon_case = + { name = test_name; path = test_path; extra_charon_options } + in + (* Generate the llbc file *) + run_charon runner_env charon_case; + (* FIXME: remove this special case *) let test_name = if test_name = "betree" then "betree_main" else test_name @@ -198,22 +208,14 @@ let () = (fun backend -> let subdir = test_subdir backend test_name in let extra_aeneas_options = - List.append (aeneas_options_for_test backend test_name) options + List.append + (aeneas_options_for_test backend test_name) + aeneas_options in - let test_case = + let aeneas_case = { name = test_name; backend; subdir; extra_aeneas_options } in - run_aeneas tests_env test_case) + (* Process the llbc file for the current backend *) + run_aeneas runner_env aeneas_case) backends - | _exe_path :: "charon" :: charon_path :: inputs_dir :: llbc_dir :: test_path - :: options -> - let tests_env = { charon_path; inputs_dir; llbc_dir } in - let test_name = Filename.remove_extension test_path in - let extra_charon_options = - List.append (charon_options_for_test test_name) options - in - let test_case = - { name = test_name; path = test_path; extra_charon_options } - in - run_charon tests_env test_case | _ -> failwith "Incorrect options passed to test runner" -- cgit v1.3.1 From 41f78066da5cc10af6312ab1bef71e45ff460688 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 16:18:40 +0200 Subject: runner: Use full path and use an enum for crate vs file --- Makefile | 2 +- tests/test_runner/run_test.ml | 96 ++++++++++++++++++++++++------------------- 2 files changed, 55 insertions(+), 43 deletions(-) (limited to 'tests/test_runner') diff --git a/Makefile b/Makefile index 88e64646..b3dc9f2b 100644 --- a/Makefile +++ b/Makefile @@ -174,7 +174,7 @@ endif # which backends to use and sets test-specific options. .PHONY: test-% test-%: - $(TEST_RUNNER_EXE) $(CHARON_EXE) $(AENEAS_EXE) $(INPUTS_DIR) $(LLBC_DIR) "$*" $(AENEAS_OPTIONS) + $(TEST_RUNNER_EXE) $(CHARON_EXE) $(AENEAS_EXE) $(LLBC_DIR) $(INPUTS_DIR)/"$*" $(AENEAS_OPTIONS) echo "# Test $* done" # ============================================================================= diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 5eff95af..8aa6347c 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -2,7 +2,6 @@ type runner_env = { charon_path : string; aeneas_path : string; - inputs_dir : string; llbc_dir : string; } @@ -14,8 +13,11 @@ type aeneas_test_case = { extra_aeneas_options : string list; } +type input_kind = SingleFile | Crate + (* The data for a specific test to generate llbc for *) type charon_test_case = { + kind : input_kind; name : string; path : string; extra_charon_options : string list; @@ -55,42 +57,42 @@ let run_aeneas (env : runner_env) (case : aeneas_test_case) = (* Run Charon on a specific input with the given options *) let run_charon (env : runner_env) (case : charon_test_case) = - let input_path = concat_path [ env.inputs_dir; case.path ] in - if Sys_unix.is_file_exn input_path then - let args = - [| - env.charon_path; - "--no-cargo"; - "--input"; - input_path; - "--crate"; - case.name; - "--dest"; - env.llbc_dir; - |] - in - let args = Array.append args (Array.of_list case.extra_charon_options) in - (* Run Charon on the rust file *) - run_command args - else if Sys.is_directory input_path then - match Sys.getenv_opt "IN_CI" with - | None -> - let args = [| env.charon_path; "--dest"; env.llbc_dir |] in - let args = - Array.append args (Array.of_list case.extra_charon_options) - in - (* Run Charon inside the crate *) - let old_pwd = Unix.getcwd () in - Unix.chdir input_path; - run_command args; - Unix.chdir old_pwd - | Some _ -> - (* Crates with dependencies must be generated separately in CI. We skip - here and trust that CI takes care to generate the necessary llbc - file. *) - print_endline - "Warn: IN_CI is set; we skip generating llbc files for whole crates" - else failwith ("`" ^ input_path ^ "` is not a file or a directory.") + match case.kind with + | SingleFile -> + let args = + [| + env.charon_path; + "--no-cargo"; + "--input"; + case.path; + "--crate"; + case.name; + "--dest"; + env.llbc_dir; + |] + in + let args = Array.append args (Array.of_list case.extra_charon_options) in + (* Run Charon on the rust file *) + run_command args + | Crate -> ( + match Sys.getenv_opt "IN_CI" with + | None -> + let args = [| env.charon_path; "--dest"; env.llbc_dir |] in + let args = + Array.append args (Array.of_list case.extra_charon_options) + in + (* Run Charon inside the crate *) + let old_pwd = Unix.getcwd () in + Unix.chdir case.path; + run_command args; + Unix.chdir old_pwd + | Some _ -> + (* Crates with dependencies must be generated separately in CI. We skip + here and trust that CI takes care to generate the necessary llbc + file. *) + print_endline + "Warn: IN_CI is set; we skip generating llbc files for whole crates" + ) (* File-specific options *) let aeneas_options_for_test backend test_name = @@ -186,14 +188,24 @@ let test_subdir backend test_name = let () = match Array.to_list Sys.argv with (* Ad-hoc argument passing for now. *) - | _exe_path :: charon_path :: aeneas_path :: inputs_dir :: llbc_dir - :: test_path :: aeneas_options -> - let runner_env = { charon_path; aeneas_path; inputs_dir; llbc_dir } in - let test_name = Filename.remove_extension test_path in + | _exe_path :: charon_path :: aeneas_path :: llbc_dir :: test_path + :: aeneas_options -> + let runner_env = { charon_path; aeneas_path; llbc_dir } in + let test_name = Filename.remove_extension (Filename.basename test_path) in + let charon_kind = + if Sys_unix.is_file_exn test_path then SingleFile + else if Sys_unix.is_directory_exn test_path then Crate + else failwith ("`" ^ test_path ^ "` is not a file or a directory.") + in let extra_charon_options = charon_options_for_test test_name in let charon_case = - { name = test_name; path = test_path; extra_charon_options } + { + path = test_path; + name = test_name; + kind = charon_kind; + extra_charon_options; + } in (* Generate the llbc file *) run_charon runner_env charon_case; -- cgit v1.3.1