diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 96 |
1 files changed, 65 insertions, 31 deletions
@@ -34,7 +34,7 @@ AENEAS_EXE ?= bin/aeneas.exe # - 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 += -unfold-monads -test-trans-units +OPTIONS += # # The rules use (and update) the following variables @@ -43,6 +43,8 @@ OPTIONS += -unfold-monads -test-trans-units CHARON_TEST_DIR = # The options with which to call Charon CHARON_OPTIONS = +# The backend sub-directory in which to generate the files +BACKEND_SUBDIR := # The directory in which to extract the result of the translation SUBDIR := @@ -86,8 +88,8 @@ clean: tests: trans-no_nested_borrows trans-paper \ trans-hashmap trans-hashmap_main \ trans-external trans-constants \ - trans-polonius-polonius_list trans-polonius-betree_main \ - test-trans-polonius-betree_main + transp-polonius_list transp-betree_main \ + test-transp-betree_main # Verify the F* files generated by the translation .PHONY: verify @@ -106,70 +108,102 @@ CHARON_CMD = cd $(CHARON_TEST_DIR) && NOT_ALL_TESTS=1 $(MAKE) test-$* endif # The command to run Aeneas on the proper llbc file -AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/fstar/$(SUBDIR) $(OPTIONS) +AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BACKEND_SUBDIR)/$(SUBDIR) $(OPTIONS) # Add specific options to some tests trans-no_nested_borrows trans-paper: \ - OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses + OPTIONS += -test-units -test-trans-units -no-split-files -no-state trans-no_nested_borrows trans-paper: SUBDIR:=misc +tfstar-no_nested_borrows tfstar-paper: -trans-hashmap: OPTIONS += -template-clauses -no-state +trans-hashmap: OPTIONS += -no-state trans-hashmap: SUBDIR:=hashmap +tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses -trans-hashmap_main: OPTIONS += -template-clauses +trans-hashmap_main: OPTIONS += trans-hashmap_main: SUBDIR:=hashmap_on_disk +tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses -trans-polonius-polonius_list: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses -trans-polonius-polonius_list: SUBDIR:=misc +transp-polonius_list: OPTIONS += -test-units -test-trans-units -no-split-files -no-state +transp-polonius_list: SUBDIR:=misc +tfstarp-polonius_list: OPTIONS += -trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses +trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state trans-constants: SUBDIR:=misc +tfstar-constants: OPTIONS += trans-external: OPTIONS += trans-external: SUBDIR:=misc +tfstar-external: OPTIONS += -BETREE_OPTIONS = -template-clauses -trans-polonius-betree_main: OPTIONS += $(BETREE_OPTIONS) -backward-no-state-update -trans-polonius-betree_main: SUBDIR:=betree +BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses +transp-betree_main: OPTIONS += -backward-no-state-update +transp-betree_main: SUBDIR:=betree +tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) # Additional test on the betree: translate it without `-backward-no-state-update`. # This generates very ugly code, but is good to test the translation. -test-trans-polonius-betree_main: trans-polonius-betree_main -test-trans-polonius-betree_main: OPTIONS += $(BETREE_OPTIONS) -test-trans-polonius-betree_main: SUBDIR:=betree_back_stateful -test-trans-polonius-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) -test-trans-polonius-betree_main: FILE = betree_main -test-trans-polonius-betree_main: +.PHONY: test-transp-betree_main +test-transp-betree_main: transp-betree_main +test-transp-betree_main: OPTIONS += -backend fstar -unfold-monads -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: $(AENEAS_CMD) # Generic rules to extract the LLBC from a rust file # We use the rules in Charon's Makefile to generate the .llbc files: the options # vary with the test files. -.PHONY: gen-llbc-polonius-% -gen-llbc-polonius-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) -gen-llbc-polonius-%: - $(CHARON_CMD) - .PHONY: gen-llbc-% gen-llbc-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR) gen-llbc-%: $(CHARON_CMD) -# Generic rule to test the translation of an LLBC file. +# "p" stands for "Polonius" +.PHONY: gen-llbcp-% +gen-llbcp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) +gen-llbcp-%: + $(CHARON_CMD) + +# Generic rules to test the translation of an LLBC file. # Note that the files requiring the Polonius borrow-checker are generated # in the tests-polonius subdirectory. .PHONY: trans-% -trans-%: -trans-polonius-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) trans-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR) +trans-%: FILE = $* +trans-%: gen-llbc-% tfstar-% tcoq-% + echo "# Test $* done" + +# "p" stands for "Polonius" +.PHONY: transp-% +transp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) +transp-%: FILE = $* +transp-%: gen-llbcp-% tfstarp-% + echo "# Test $* done" + +.PHONY: tfstar-% +tfstar-%: OPTIONS += -backend fstar -unfold-monads -test-trans-units +tfstar-%: BACKEND_SUBDIR := fstar +tfstar-%: + $(AENEAS_CMD) -trans-polonius-%: FILE = $* -trans-polonius-%: gen-llbc-polonius-% +# "p" stands for "Polonius" +.PHONY: tfstarp-% +tfstarp-%: OPTIONS += -backend fstar -unfold-monads -test-trans-units +tfstarp-%: BACKEND_SUBDIR := fstar +tfstarp-%: $(AENEAS_CMD) -trans-%: FILE = $* -trans-%: gen-llbc-% +# TODO: -test-trans-units +# It doesn't work on vec_push_fwd, I don't understand why. +.PHONY: tcoq-% +tcoq-%: OPTIONS += -backend coq -decompose-monads +tcoq-%: BACKEND_SUBDIR := coq +tcoq-%: $(AENEAS_CMD) # Nix |