diff options
Diffstat (limited to '')
| -rw-r--r-- | Makefile | 290 |
1 files changed, 85 insertions, 205 deletions
@@ -13,36 +13,30 @@ 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 ?= +# 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 path to Charon -CHARON_HOME ?= ./charon +# The user can specify additional translation options for Aeneas. +AENEAS_OPTIONS ?= +CHARON_OPTIONS ?= -# 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 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 user can specify additional translation options for Aeneas. -# By default we activate the (expensive) sanity checks. -OPTIONS ?= - -# 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 = -# The backend sub-directory in which to generate the files -BACKEND_SUBDIR := -# The directory in which to extract the result of the translation -SUBDIR := +# In CI, we enforce formatting and activate the (expensive) sanity checks. +IN_CI ?= #################################### # The rules #################################### +# Never remove intermediate files +.SECONDARY: + # Build the compiler, after formatting the code .PHONY: build build: format build-dev @@ -53,7 +47,12 @@ build-test-verify: build test verify # Build the project, without formatting the code .PHONY: build-dev +ifdef IN_CI +build-dev: + @true +else build-dev: build-bin build-lib build-bin-dir doc +endif .PHONY: build-bin build-bin: check-charon @@ -63,11 +62,16 @@ build-bin: check-charon build-lib: check-charon cd compiler && dune build aeneas.cmxs +.PHONY: build-runner +build-runner: check-charon + cd tests/test_runner && dune build + .PHONY: build-bin-dir -build-bin-dir: build-bin build-lib +build-bin-dir: build-bin build-lib build-runner mkdir -p bin cp -f compiler/_build/default/main.exe bin/aeneas cp -f compiler/_build/default/main.exe bin/aeneas.cmxs + cp -f tests/test_runner/_build/default/run_test.exe bin/test_runner mkdir -p bin/backends/fstar mkdir -p bin/backends/coq cp -rf backends/fstar/*.fst* bin/backends/fstar/ @@ -100,207 +104,83 @@ 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 -# Test the project by translating test files to F* -.PHONY: test -test: build-dev test-all +.PHONY: clean-generated +clean-generated: clean-generated-aeneas clean-generated-llbc -.PHONY: test-all -test-all: test-no_nested_borrows test-paper \ - test-hashmap test-hashmap_main \ - test-external test-constants \ - test-polonius_list test-betree_main \ - ctest-test-betree_main \ - test-loops \ - test-arrays test-traits test-bitwise test-demo +.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 -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 +.PHONY: clean-generated-llbc +clean-generated-llbc: + rm -rf $(LLBC_DIR) + +# ============================================================================= +# The tests. +# ============================================================================= + +# Test the project by translating test files to various backends. +.PHONY: test +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 # 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 +# 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)) -# The commands to run Charon to generate the .llbc files -ifeq (, $(REGEN_LLBC)) -else -CHARON_CMD = cd $(CHARON_TEST_DIR) && $(MAKE) test-$* +# 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 endif -# The command to run Aeneas on the proper llbc file -AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BACKEND_SUBDIR)/$(SUBDIR) $(OPTIONS) - - -# Add specific options to some tests -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 - -test-arrays: OPTIONS += -test-arrays: SUBDIR := arrays -tfstar-arrays: OPTIONS += -decreases-clauses -template-clauses -split-files -tcoq-arrays: OPTIONS += -use-fuel -tlean-arrays: SUBDIR := -tlean-arrays: OPTIONS += -thol4-arrays: 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 += - -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 - -test-demo: OPTIONS += -test-demo: SUBDIR := demo -tfstar-demo: OPTIONS += -use-fuel -tcoq-demo: OPTIONS += -use-fuel -tlean-demo: SUBDIR := Demo -thol4-demo: OPTIONS += - -# 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 += - -# 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 += - -test-polonius_list: OPTIONS += -test-trans-units -test-polonius_list: SUBDIR := misc -tfstar-polonius_list: OPTIONS += -tcoq-polonius_list: OPTIONS += -tlean-polonius_list: SUBDIR := -tlean-polonius_list: OPTIONS += -thol4-polonius_list: SUBDIR := misc-polonius_list -thol4-polonius_list: OPTIONS += - -test-constants: OPTIONS += -test-trans-units -test-constants: SUBDIR := misc -tfstar-constants: OPTIONS += -tcoq-constants: OPTIONS += -tlean-constants: SUBDIR := -tlean-constants: OPTIONS += -thol4-constants: SUBDIR := misc-constants -thol4-constants: OPTIONS += - -test-external: OPTIONS += -test-trans-units -state -split-files -test-external: SUBDIR := misc -tfstar-external: OPTIONS += -tcoq-external: OPTIONS += -tlean-external: SUBDIR := -tlean-external: OPTIONS += -thol4-external: SUBDIR := misc-external -thol4-external: OPTIONS += - -test-bitwise: OPTIONS += -test-trans-units -test-bitwise: SUBDIR := misc -tfstar-bitwise: OPTIONS += -tcoq-bitwise: OPTIONS += -tlean-bitwise: SUBDIR := -tlean-bitwise: OPTIONS += -thol4-bitwise: SUBDIR := misc-bitwise -thol4-bitwise: OPTIONS += - -BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses -test-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files -test-betree_main: SUBDIR:=betree -tfstar-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) -tcoq-betree_main: OPTIONS += -use-fuel -tlean-betree_main: SUBDIR := -tlean-betree_main: OPTIONS += -thol4-betree_main: OPTIONS += - -# 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: OPTIONS += -backend fstar -test-trans-units -state -split-files -ctest-test-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) -ctest-test-betree_main: BACKEND_SUBDIR := "fstar" -ctest-test-betree_main: SUBDIR:=betree_back_stateful -ctest-test-betree_main: FILE = betree_main -ctest-test-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-% -gen-llbc-%: - $(CHARON_CMD) - -# Generic rules to test the translation of an LLBC file. +# Translate the given rust file to available backends. The test runner decides +# which backends to use and sets test-specific options. +# Note: the tests have the fulle file name: `test-arrays.rs`, `test-loops.rs`, `test-betree`. .PHONY: test-% -test-%: FILE = $* -test-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-% +test-%: build-dev + $(TEST_RUNNER_EXE) $(CHARON_EXE) $(AENEAS_EXE) $(LLBC_DIR) $(INPUTS_DIR)/"$*" $(AENEAS_OPTIONS) echo "# Test $* done" -.PHONY: tfstar-% -tfstar-%: OPTIONS += -backend fstar -tfstar-%: BACKEND_SUBDIR := fstar -tfstar-%: - $(AENEAS_CMD) - -.PHONY: tcoq-% -tcoq-%: OPTIONS += -backend coq -tcoq-%: BACKEND_SUBDIR := coq -tcoq-%: - $(AENEAS_CMD) - -.PHONY: tlean-% -tlean-%: OPTIONS += -backend lean -tlean-%: BACKEND_SUBDIR := lean -tlean-%: - $(AENEAS_CMD) - -# TODO: reactivate HOL4 once traits are parameterized by their associated types -.PHONY: thol4-% -thol4-%: OPTIONS += -backend hol4 -thol4-%: BACKEND_SUBDIR := hol4 -thol4-%: - echo Ignoring the $* test for HOL4 - -#thol4-%: -# $(AENEAS_CMD) - -# Nix - TODO: add the lean tests +# ============================================================================= +# Nix +# ============================================================================= +# TODO: add the lean tests .PHONY: nix nix: nix build && nix flake check |