Import test suite from charon

1 files changed, 102 insertions, 50 deletions

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/<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