diff options
Diffstat (limited to '')
| -rw-r--r-- | Makefile | 150 |
1 files changed, 86 insertions, 64 deletions
@@ -27,14 +27,11 @@ CHARON_TESTS_POLONIUS_DIR ?= $(CHARON_HOME)/tests-polonius # 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.exe +AENEAS_EXE ?= bin/aeneas # The user can specify additional translation options for Aeneas. -# By default we do: -# - unfold all the monadic let bindings to matches (required by F*) -# - insert calls to the normalizer in the translated code to test the -# generated unit functions -OPTIONS += +# By default we activate the (expensive) sanity checks. +OPTIONS ?= -checks # # The rules use (and update) the following variables @@ -58,22 +55,25 @@ build-tests-verify: build tests verify # Build the project .PHONY: build -build: build-driver build-lib build-bin-dir doc +build: build-bin build-lib build-bin-dir doc -.PHONY: build-driver -build-driver: - cd compiler && dune build $(AENEAS_DRIVER) +.PHONY: build-bin +build-bin: + cd compiler && dune build .PHONY: build-lib build-lib: cd compiler && dune build aeneas.cmxs .PHONY: build-bin-dir -build-bin-dir: build-driver build-lib +build-bin-dir: build-bin build-lib mkdir -p bin - cp -f compiler/_build/default/driver.exe bin/aeneas.exe - cp -f compiler/_build/default/driver.exe bin/aeneas.cmxs - cp -rf backends bin + cp -f compiler/_build/default/main.exe bin/aeneas + cp -f compiler/_build/default/main.exe bin/aeneas.cmxs + mkdir -p bin/backends/fstar + mkdir -p bin/backends/coq + cp -rf backends/fstar/*.fst* bin/backends/fstar/ + cp -rf backends/coq/*.v bin/backends/coq/ .PHONY: doc doc: @@ -85,13 +85,13 @@ clean: # Test the project by translating test files to F* .PHONY: tests -tests: trans-no_nested_borrows trans-paper \ - trans-hashmap trans-hashmap_main \ - trans-external trans-constants \ - transp-polonius_list transp-betree_main \ - test-transp-betree_main \ - trans-loops \ - trans-array # TODO: generalize to all backends +tests: test-no_nested_borrows test-paper \ + test-hashmap test-hashmap_main \ + test-external test-constants \ + testp-polonius_list testp-betree_main \ + ctest-testp-betree_main \ + test-loops \ + test-array test-traits # TODO: generalize to all backends # Verify the F* files generated by the translation .PHONY: verify @@ -114,51 +114,65 @@ AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BA # Add specific options to some tests -trans-no_nested_borrows trans-paper: \ - OPTIONS += -test-units -test-trans-units -no-split-files -no-state -trans-no_nested_borrows trans-paper: SUBDIR := misc +test-no_nested_borrows test-paper: \ + OPTIONS += -test-trans-units +test-no_nested_borrows test-paper: SUBDIR := misc tfstar-no_nested_borrows tfstar-paper: tlean-no_nested_borrows: SUBDIR := tlean-paper: SUBDIR := thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows thol4-paper: SUBDIR := misc-paper -trans-array: OPTIONS += -no-state -trans-array: SUBDIR := array -tfstar-array: OPTIONS += -decreases-clauses -template-clauses +test-array: OPTIONS += +test-array: SUBDIR := array +tfstar-array: OPTIONS += -decreases-clauses -template-clauses -split-files tcoq-array: OPTIONS += -use-fuel tlean-array: SUBDIR := tlean-array: OPTIONS += thol4-array: OPTIONS += +test-traits: OPTIONS += +test-traits: SUBDIR := traits +tfstar-traits: OPTIONS += -decreases-clauses -template-clauses +tcoq-traits: OPTIONS += +tlean-traits: SUBDIR := +tlean-traits: OPTIONS += +thol4-traits: OPTIONS += + # TODO: activate the arrays for all the backends thol4-array: echo "Ignoring the array test for HOL4" -trans-loops: OPTIONS += -no-state -trans-loops: SUBDIR := misc -tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -tcoq-loops: OPTIONS += -use-fuel -no-split-files +# TODO: activate the traits for all the backends +thol4-traits: + echo "Ignoring the traits test for HOL4" + +test-loops: OPTIONS += +test-loops: SUBDIR := misc +tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -split-files +tcoq-loops: OPTIONS += -use-fuel tlean-loops: SUBDIR := thol4-loops: SUBDIR := misc-loops -trans-hashmap: OPTIONS += -no-state -test-trans-units -trans-hashmap: SUBDIR := hashmap +# TODO: reactivate -test-trans-units +test-hashmap: OPTIONS += -split-files +test-hashmap: SUBDIR := hashmap tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap: OPTIONS += -use-fuel tlean-hashmap: SUBDIR := tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hashmap.lean file: we do not want to overwrite it thol4-hashmap: OPTIONS += -trans-hashmap_main: OPTIONS += -test-trans-units -trans-hashmap_main: SUBDIR := hashmap_on_disk +# TODO: reactivate -test-trans-units +test-hashmap_main: OPTIONS += -state -split-files +test-hashmap_main: SUBDIR := hashmap_on_disk tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap_main: OPTIONS += -use-fuel tlean-hashmap_main: SUBDIR := thol4-hashmap_main: OPTIONS += -transp-polonius_list: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -transp-polonius_list: SUBDIR := misc +testp-polonius_list: OPTIONS += -test-trans-units +testp-polonius_list: SUBDIR := misc tfstarp-polonius_list: OPTIONS += tcoqp-polonius_list: OPTIONS += tleanp-polonius_list: SUBDIR := @@ -166,8 +180,8 @@ tleanp-polonius_list: OPTIONS += thol4p-polonius_list: SUBDIR := misc-polonius_list thol4p-polonius_list: OPTIONS += -trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -trans-constants: SUBDIR := misc +test-constants: OPTIONS += -test-trans-units +test-constants: SUBDIR := misc tfstar-constants: OPTIONS += tcoq-constants: OPTIONS += tlean-constants: SUBDIR := @@ -175,8 +189,8 @@ tlean-constants: OPTIONS += thol4-constants: SUBDIR := misc-constants thol4-constants: OPTIONS += -trans-external: OPTIONS += -test-trans-units -trans-external: SUBDIR := misc +test-external: OPTIONS += -test-trans-units -state -split-files +test-external: SUBDIR := misc tfstar-external: OPTIONS += tcoq-external: OPTIONS += tlean-external: SUBDIR := @@ -185,25 +199,25 @@ thol4-external: SUBDIR := misc-external thol4-external: OPTIONS += BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses -transp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -transp-betree_main: SUBDIR:=betree +testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files +testp-betree_main: SUBDIR:=betree tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) tcoqp-betree_main: OPTIONS += -use-fuel tleanp-betree_main: SUBDIR := tleanp-betree_main: OPTIONS += thol4-betree_main: OPTIONS += -# Additional test on the betree: translate it without `-backward-no-state-update`. +# 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: test-transp-betree_main -test-transp-betree_main: transp-betree_main -test-transp-betree_main: OPTIONS += -backend fstar -test-trans-units -test-transp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) -test-transp-betree_main: BACKEND_SUBDIR := "fstar" -test-transp-betree_main: SUBDIR:=betree_back_stateful -test-transp-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) -test-transp-betree_main: FILE = betree_main -test-transp-betree_main: +.PHONY: ctest-testp-betree_main +ctest-testp-betree_main: testp-betree_main +ctest-testp-betree_main: OPTIONS += -backend fstar -test-trans-units -state -split-files +ctest-testp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) +ctest-testp-betree_main: BACKEND_SUBDIR := "fstar" +ctest-testp-betree_main: SUBDIR:=betree_back_stateful +ctest-testp-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) +ctest-testp-betree_main: FILE = betree_main +ctest-testp-betree_main: $(AENEAS_CMD) # Generic rules to extract the LLBC from a rust file @@ -220,20 +234,20 @@ gen-llbcp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) gen-llbcp-%: $(CHARON_CMD) -# Generic rules to test the translation of an LLBC file. +# Generic rules to test the testlation of an LLBC file. # Note that the files requiring the Polonius borrow-checker are generated # in the tests-polonius subdirectory. -.PHONY: trans-% -trans-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR) -trans-%: FILE = $* -trans-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-% +.PHONY: test-% +test-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR) +test-%: FILE = $* +test-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-% echo "# Test $* done" # "p" stands for "Polonius" -.PHONY: transp-% -transp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) -transp-%: FILE = $* -transp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-% +.PHONY: testp-% +testp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) +testp-%: FILE = $* +testp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-% echo "# Test $* done" .PHONY: tfstar-% @@ -276,17 +290,25 @@ tleanp-%: BACKEND_SUBDIR := lean tleanp-%: $(AENEAS_CMD) +# TODO: reactivate HOL4 once traits are parameterized by their associated types .PHONY: thol4-% thol4-%: OPTIONS += -backend hol4 thol4-%: BACKEND_SUBDIR := hol4 thol4-%: - $(AENEAS_CMD) + echo Ignoring the $* test for HOL4 +#thol4-%: +# $(AENEAS_CMD) + +# TODO: reactivate HOL4 once traits are parameterized by their associated types .PHONY: thol4p-% thol4p-%: OPTIONS += -backend hol4 thol4p-%: BACKEND_SUBDIR := hol4 thol4p-%: - $(AENEAS_CMD) + echo Ignoring the $* test for HOL4 + +#thol4p-%: +# $(AENEAS_CMD) # Nix - TODO: add the lean tests .PHONY: nix |