diff options
Diffstat (limited to '')
| -rw-r--r-- | Makefile | 152 |
1 files changed, 102 insertions, 50 deletions
@@ -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/<file>.llbc` for each `$(INPUTS_DIR)/<file>.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 |