summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorNadrieril2024-05-23 14:38:50 +0200
committerGuillaume Boisseau2024-05-24 14:24:38 +0200
commit3a380f990d0f202ee19bd163726ff5fc63181ae7 (patch)
treedeef31c2ff20dd9268380f3b5d563ab6eb32bf90 /Makefile
parent25973ee8ef28e2d5b8a9b9ec3de4d6ff340db18b (diff)
Use runner to generate llbc
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile53
1 files changed, 9 insertions, 44 deletions
diff --git a/Makefile b/Makefile
index b9aaf97c..fccca9b1 100644
--- a/Makefile
+++ b/Makefile
@@ -19,8 +19,7 @@ TEST_RUNNER_EXE ?= $(PWD)/bin/test_runner
CHARON_EXE ?= $(PWD)/charon/bin/charon
# The user can specify additional translation options for Aeneas.
-# In CI we activate the (expensive) sanity checks.
-OPTIONS ?=
+AENEAS_OPTIONS ?=
CHARON_OPTIONS ?=
# The directory thta contains the rust source files for tests.
@@ -28,7 +27,7 @@ INPUTS_DIR ?= tests/src
# The directory where to look for the .llbc files.
LLBC_DIR ?= $(PWD)/tests/llbc
-# In CI, we enforce formatting and we don't regenerate llbc files.
+# In CI, we enforce formatting and activate the (expensive) sanity checks.
IN_CI ?=
####################################
@@ -169,53 +168,19 @@ verify:
ifdef IN_CI
# In CI we do extra sanity checks.
-test-%: OPTIONS += -checks
+test-%: AENEAS_OPTIONS += -checks
+else
+test-%: check-charon
endif
-# Translate the given llbc file to available backends. The test runner decides
+# Translate the given rust file to available backends. The test runner decides
# which backends to use and sets test-specific options.
.PHONY: test-%
-test-%: TEST_NAME = $*
-test-%: $(LLBC_DIR)/%.llbc
- $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(LLBC_DIR) $(TEST_NAME) $(OPTIONS)
+test-%:
+ $(TEST_RUNNER_EXE) charon $(CHARON_EXE) $(INPUTS_DIR) $(LLBC_DIR) "$*" $(CHARON_OPTIONS)
+ $(TEST_RUNNER_EXE) aeneas $(AENEAS_EXE) $(LLBC_DIR) "$*" $(AENEAS_OPTIONS)
echo "# Test $* done"
-# 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:
- $(CHARON_EXE) --no-cargo --input $(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
# =============================================================================