From b66f7fee37bf2127e07b0865edb8fb1e039cab9e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 22 May 2024 15:10:50 +0200 Subject: make: deduplicate setting the backend --- Makefile | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 2058700a..32388a5e 100644 --- a/Makefile +++ b/Makefile @@ -34,8 +34,6 @@ OPTIONS ?= 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 := @@ -142,7 +140,7 @@ CHARON_CMD = cd $(CHARON_TEST_DIR) && $(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/$(BACKEND_SUBDIR)/$(SUBDIR) $(OPTIONS) +AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BACKEND)/$(SUBDIR) -backend $(BACKEND) $(OPTIONS) # Add specific options to some tests @@ -251,9 +249,9 @@ thol4-betree_main: OPTIONS += # 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 += -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: BACKEND := fstar ctest-test-betree_main: SUBDIR:=betree_back_stateful ctest-test-betree_main: FILE = betree_main ctest-test-betree_main: @@ -273,27 +271,23 @@ test-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-% echo "# Test $* done" .PHONY: tfstar-% -tfstar-%: OPTIONS += -backend fstar -tfstar-%: BACKEND_SUBDIR := fstar +tfstar-%: BACKEND := fstar tfstar-%: $(AENEAS_CMD) .PHONY: tcoq-% -tcoq-%: OPTIONS += -backend coq -tcoq-%: BACKEND_SUBDIR := coq +tcoq-%: BACKEND := coq tcoq-%: $(AENEAS_CMD) .PHONY: tlean-% -tlean-%: OPTIONS += -backend lean -tlean-%: BACKEND_SUBDIR := lean +tlean-%: BACKEND := 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-%: BACKEND := hol4 thol4-%: echo Ignoring the $* test for HOL4 -- cgit v1.2.3 From ad819ad9ccdf137ca87eb367810694246696b835 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 22 May 2024 15:41:30 +0200 Subject: Regroup and sort makefile test entries --- Makefile | 180 ++++++++++++++++++++++++++++++--------------------------------- 1 file changed, 85 insertions(+), 95 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 32388a5e..c2f42c75 100644 --- a/Makefile +++ b/Makefile @@ -108,13 +108,21 @@ clean: clean-generated test: build-dev test-all .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 \ +test-all: \ + test-arrays \ + test-betree_main \ ctest-test-betree_main \ + test-bitwise \ + test-constants \ + test-demo \ + test-external \ + test-hashmap \ + test-hashmap_main \ test-loops \ - test-arrays test-traits test-bitwise test-demo + test-no_nested_borrows \ + test-paper \ + test-polonius_list \ + test-traits .PHONY: clean-generated clean-generated: @@ -142,120 +150,95 @@ 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) -backend $(BACKEND) $(OPTIONS) +# Subdirs +test-arrays: SUBDIR := arrays +tlean-arrays: SUBDIR := -# 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: +test-betree_main: SUBDIR := betree +tlean-betree_main: SUBDIR := + +ctest-test-betree_main: SUBDIR := betree_back_stateful + +test-bitwise: SUBDIR := misc +tlean-bitwise: SUBDIR := +thol4-bitwise: SUBDIR := misc-bitwise + +test-constants: SUBDIR := misc +tlean-constants: SUBDIR := +thol4-constants: SUBDIR := misc-constants + +test-demo: SUBDIR := demo +tlean-demo: SUBDIR := Demo + +test-external: SUBDIR := misc +tlean-external: SUBDIR := +thol4-external: SUBDIR := misc-external + +test-hashmap: SUBDIR := hashmap +tlean-hashmap: SUBDIR := + +test-hashmap_main: SUBDIR := hashmap_on_disk +tlean-hashmap_main: SUBDIR := + +test-loops: SUBDIR := misc +tlean-loops: SUBDIR := +thol4-loops: SUBDIR := misc-loops + +test-no_nested_borrows: SUBDIR := misc tlean-no_nested_borrows: SUBDIR := -tlean-paper: SUBDIR := thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows + +test-paper: SUBDIR := misc +tlean-paper: SUBDIR := 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-polonius_list: SUBDIR := misc +tlean-polonius_list: SUBDIR := +thol4-polonius_list: SUBDIR := misc-polonius_list -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 +# Add specific options to some tests +# TODO: reactivate -test-trans-units for hashmap and hashmap_main +tfstar-arrays: OPTIONS += -decreases-clauses -template-clauses -split-files +tcoq-arrays: OPTIONS += -use-fuel + +test-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files +tfstar-betree_main: OPTIONS += -decreases-clauses -template-clauses +tcoq-betree_main: OPTIONS += -use-fuel + +ctest-test-betree_main: OPTIONS += -test-trans-units -state -split-files +ctest-test-betree_main: OPTIONS += -decreases-clauses -template-clauses + +test-bitwise: OPTIONS += -test-trans-units + +test-constants: OPTIONS += -test-trans-units -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-external: OPTIONS += -test-trans-units -state -split-files + 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 += +tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -split-files +tcoq-loops: OPTIONS += -use-fuel -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-no_nested_borrows: OPTIONS += -test-trans-units -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-paper: OPTIONS += -test-trans-units -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 += +test-polonius_list: OPTIONS += -test-trans-units -# 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 += -test-trans-units -state -split-files -ctest-test-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) -ctest-test-betree_main: BACKEND := fstar -ctest-test-betree_main: SUBDIR:=betree_back_stateful -ctest-test-betree_main: FILE = betree_main -ctest-test-betree_main: - $(AENEAS_CMD) +tfstar-traits: OPTIONS += -decreases-clauses -template-clauses # 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 @@ -290,10 +273,17 @@ tlean-%: thol4-%: BACKEND := hol4 thol4-%: echo Ignoring the $* test for HOL4 - -#thol4-%: # $(AENEAS_CMD) +# 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: FILE = betree_main +ctest-test-betree_main: BACKEND := fstar +ctest-test-betree_main: + $(AENEAS_CMD) + # Nix - TODO: add the lean tests .PHONY: nix nix: -- cgit v1.2.3 From 6f14e8c699169aa11ea9c106f8cae1ba593569d0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 22 May 2024 15:11:28 +0200 Subject: Add simple test runner --- Makefile | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index c2f42c75..2457bec2 100644 --- a/Makefile +++ b/Makefile @@ -24,6 +24,9 @@ CHARON_HOME ?= ./charon # change this path for the Nix package. AENEAS_EXE ?= bin/aeneas +# The path to our test runner. +TEST_RUNNER_EXE ?= bin/test_runner + # The user can specify additional translation options for Aeneas. # By default we activate the (expensive) sanity checks. OPTIONS ?= @@ -61,11 +64,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/ @@ -140,6 +148,7 @@ verify: 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)) @@ -148,7 +157,7 @@ CHARON_CMD = cd $(CHARON_TEST_DIR) && $(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/$(BACKEND)/$(SUBDIR) -backend $(BACKEND) $(OPTIONS) +AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) "$(SUBDIR)" $(BACKEND) $(OPTIONS) # Subdirs test-arrays: SUBDIR := arrays -- cgit v1.2.3 From 6ae8cde046530371345863f04d84be32b2a757bf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 22 May 2024 18:57:19 +0200 Subject: Move the subdirectory selection to the test runner --- Makefile | 55 ++----------------------------------------------------- 1 file changed, 2 insertions(+), 53 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 2457bec2..5e8fe7bb 100644 --- a/Makefile +++ b/Makefile @@ -37,8 +37,6 @@ OPTIONS ?= CHARON_TEST_DIR ?= $(CHARON_HOME)/tests # The options with which to call Charon CHARON_OPTIONS = -# The directory in which to extract the result of the translation -SUBDIR := #################################### # The rules @@ -157,56 +155,7 @@ CHARON_CMD = cd $(CHARON_TEST_DIR) && $(MAKE) test-$* endif # The command to run Aeneas on the proper llbc file -AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) "$(SUBDIR)" $(BACKEND) $(OPTIONS) - -# Subdirs -test-arrays: SUBDIR := arrays -tlean-arrays: SUBDIR := - -test-betree_main: SUBDIR := betree -tlean-betree_main: SUBDIR := - -ctest-test-betree_main: SUBDIR := betree_back_stateful - -test-bitwise: SUBDIR := misc -tlean-bitwise: SUBDIR := -thol4-bitwise: SUBDIR := misc-bitwise - -test-constants: SUBDIR := misc -tlean-constants: SUBDIR := -thol4-constants: SUBDIR := misc-constants - -test-demo: SUBDIR := demo -tlean-demo: SUBDIR := Demo - -test-external: SUBDIR := misc -tlean-external: SUBDIR := -thol4-external: SUBDIR := misc-external - -test-hashmap: SUBDIR := hashmap -tlean-hashmap: SUBDIR := - -test-hashmap_main: SUBDIR := hashmap_on_disk -tlean-hashmap_main: SUBDIR := - -test-loops: SUBDIR := misc -tlean-loops: SUBDIR := -thol4-loops: SUBDIR := misc-loops - -test-no_nested_borrows: SUBDIR := misc -tlean-no_nested_borrows: SUBDIR := -thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows - -test-paper: SUBDIR := misc -tlean-paper: SUBDIR := -thol4-paper: SUBDIR := misc-paper - -test-polonius_list: SUBDIR := misc -tlean-polonius_list: SUBDIR := -thol4-polonius_list: SUBDIR := misc-polonius_list - -test-traits: SUBDIR := traits -tlean-traits: SUBDIR := +AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(BACKEND) $(OPTIONS) # Add specific options to some tests # TODO: reactivate -test-trans-units for hashmap and hashmap_main @@ -288,7 +237,7 @@ thol4-%: # 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: FILE = betree_main +ctest-test-betree_main: FILE = betree_main-special ctest-test-betree_main: BACKEND := fstar ctest-test-betree_main: $(AENEAS_CMD) -- cgit v1.2.3 From a9471e615e03d6fa0bc1594176fe504c9a3c88ae Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 22 May 2024 19:23:03 +0200 Subject: Set all options in the test runner --- Makefile | 52 +--------------------------------------------------- 1 file changed, 1 insertion(+), 51 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 5e8fe7bb..0ceaa558 100644 --- a/Makefile +++ b/Makefile @@ -117,7 +117,7 @@ test: build-dev test-all test-all: \ test-arrays \ test-betree_main \ - ctest-test-betree_main \ + tfstar-betree_main-special \ test-bitwise \ test-constants \ test-demo \ @@ -157,47 +157,6 @@ endif # The command to run Aeneas on the proper llbc file AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(BACKEND) $(OPTIONS) -# Add specific options to some tests -# TODO: reactivate -test-trans-units for hashmap and hashmap_main -tfstar-arrays: OPTIONS += -decreases-clauses -template-clauses -split-files -tcoq-arrays: OPTIONS += -use-fuel - -test-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files -tfstar-betree_main: OPTIONS += -decreases-clauses -template-clauses -tcoq-betree_main: OPTIONS += -use-fuel - -ctest-test-betree_main: OPTIONS += -test-trans-units -state -split-files -ctest-test-betree_main: OPTIONS += -decreases-clauses -template-clauses - -test-bitwise: OPTIONS += -test-trans-units - -test-constants: OPTIONS += -test-trans-units - -tfstar-demo: OPTIONS += -use-fuel -tcoq-demo: OPTIONS += -use-fuel - -test-external: OPTIONS += -test-trans-units -state -split-files - -test-hashmap: OPTIONS += -split-files -tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses -tcoq-hashmap: OPTIONS += -use-fuel -tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hashmap.lean file: we do not want to overwrite it - -test-hashmap_main: OPTIONS += -state -split-files -tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses -tcoq-hashmap_main: OPTIONS += -use-fuel - -tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -split-files -tcoq-loops: OPTIONS += -use-fuel - -test-no_nested_borrows: OPTIONS += -test-trans-units - -test-paper: OPTIONS += -test-trans-units - -test-polonius_list: OPTIONS += -test-trans-units - -tfstar-traits: OPTIONS += -decreases-clauses -template-clauses - # 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. @@ -233,15 +192,6 @@ thol4-%: echo Ignoring the $* test for HOL4 # $(AENEAS_CMD) -# 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: FILE = betree_main-special -ctest-test-betree_main: BACKEND := fstar -ctest-test-betree_main: - $(AENEAS_CMD) - # Nix - TODO: add the lean tests .PHONY: nix nix: -- cgit v1.2.3 From b953b89f9739c6703c49667781f5509b1b2a3898 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 10:05:04 +0200 Subject: Let the runner choose which backends to use --- Makefile | 33 +++++---------------------------- 1 file changed, 5 insertions(+), 28 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 0ceaa558..506dec5e 100644 --- a/Makefile +++ b/Makefile @@ -117,7 +117,7 @@ test: build-dev test-all test-all: \ test-arrays \ test-betree_main \ - tfstar-betree_main-special \ + test-betree_main-special \ test-bitwise \ test-constants \ test-demo \ @@ -154,9 +154,6 @@ else CHARON_CMD = cd $(CHARON_TEST_DIR) && $(MAKE) test-$* endif -# The command to run Aeneas on the proper llbc file -AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(BACKEND) $(OPTIONS) - # 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. @@ -164,34 +161,14 @@ AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(BACKE gen-llbc-%: $(CHARON_CMD) -# Generic rules to test the translation of an LLBC file. +# 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-% tfstar-% tcoq-% tlean-% thol4-% +test-%: gen-llbc-% + $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(OPTIONS) echo "# Test $* done" -.PHONY: tfstar-% -tfstar-%: BACKEND := fstar -tfstar-%: - $(AENEAS_CMD) - -.PHONY: tcoq-% -tcoq-%: BACKEND := coq -tcoq-%: - $(AENEAS_CMD) - -.PHONY: tlean-% -tlean-%: BACKEND := lean -tlean-%: - $(AENEAS_CMD) - -# TODO: reactivate HOL4 once traits are parameterized by their associated types -.PHONY: thol4-% -thol4-%: BACKEND := hol4 -thol4-%: - echo Ignoring the $* test for HOL4 -# $(AENEAS_CMD) - # Nix - TODO: add the lean tests .PHONY: nix nix: -- cgit v1.2.3 From b8bdf14f3e4b25578d107160161f5bd2b548a113 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 14:06:51 +0200 Subject: Remove secondary betree test Opened https://github.com/AeneasVerif/aeneas/issues/196 to remember to add a more adequate replacement test. --- Makefile | 1 - 1 file changed, 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 506dec5e..dc38e56a 100644 --- a/Makefile +++ b/Makefile @@ -117,7 +117,6 @@ test: build-dev test-all test-all: \ test-arrays \ test-betree_main \ - test-betree_main-special \ test-bitwise \ test-constants \ test-demo \ -- cgit v1.2.3 From 4ce3e9c7c11744abae52d7a3ae1a3962395784be Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 10:41:10 +0200 Subject: Import test suite from charon --- Makefile | 152 ++++++++++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 102 insertions(+), 50 deletions(-) (limited to 'Makefile') 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/.llbc` for each `$(INPUTS_DIR)/.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 -- cgit v1.2.3 From 25973ee8ef28e2d5b8a9b9ec3de4d6ff340db18b Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 14:41:00 +0200 Subject: Tweak a path --- Makefile | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 73f711a7..b9aaf97c 100644 --- a/Makefile +++ b/Makefile @@ -205,8 +205,7 @@ 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) + $(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) -- cgit v1.2.3 From 3a380f990d0f202ee19bd163726ff5fc63181ae7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 14:38:50 +0200 Subject: Use runner to generate llbc --- Makefile | 53 +++++++++-------------------------------------------- 1 file changed, 9 insertions(+), 44 deletions(-) (limited to 'Makefile') 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/.llbc` for each `$(INPUTS_DIR)/.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 # ============================================================================= -- cgit v1.2.3 From ca045d57b6cc3fc700efe07bfc257231edf814e5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 15:37:01 +0200 Subject: Auto-detect test cases --- Makefile | 29 +++++++++++++---------------- 1 file changed, 13 insertions(+), 16 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index fccca9b1..8a7701cc 100644 --- a/Makefile +++ b/Makefile @@ -145,27 +145,24 @@ test: build-dev test-all betree-tests betree-tests: cd $(INPUTS_DIR)/betree && $(MAKE) test -.PHONY: test-all -test-all: \ - test-arrays \ - test-betree_main \ - test-bitwise \ - test-constants \ - test-demo \ - test-external \ - test-hashmap \ - test-hashmap_main \ - test-loops \ - test-no_nested_borrows \ - test-paper \ - test-polonius_list \ - test-traits - # Verify the F* files generated by the translation .PHONY: verify verify: cd tests && $(MAKE) all +# 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)) +# Remove some tests we don't want to run. +# FIXME: move this information to the file itself +INPUTS_LIST := $(filter-out test-hashmap_utils.rs,$(INPUTS_LIST)) +INPUTS_LIST := $(filter-out test-nested_borrows.rs,$(INPUTS_LIST)) + +# 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 -- cgit v1.2.3 From d37a302762fef4ea91b88f0ca8feb73612ff5382 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 15:46:45 +0200 Subject: runner: Do both steps of generation at once --- Makefile | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 8a7701cc..88e64646 100644 --- a/Makefile +++ b/Makefile @@ -174,8 +174,7 @@ endif # which backends to use and sets test-specific options. .PHONY: test-% test-%: - $(TEST_RUNNER_EXE) charon $(CHARON_EXE) $(INPUTS_DIR) $(LLBC_DIR) "$*" $(CHARON_OPTIONS) - $(TEST_RUNNER_EXE) aeneas $(AENEAS_EXE) $(LLBC_DIR) "$*" $(AENEAS_OPTIONS) + $(TEST_RUNNER_EXE) $(CHARON_EXE) $(AENEAS_EXE) $(INPUTS_DIR) $(LLBC_DIR) "$*" $(AENEAS_OPTIONS) echo "# Test $* done" # ============================================================================= -- cgit v1.2.3 From 41f78066da5cc10af6312ab1bef71e45ff460688 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 16:18:40 +0200 Subject: runner: Use full path and use an enum for crate vs file --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 88e64646..b3dc9f2b 100644 --- a/Makefile +++ b/Makefile @@ -174,7 +174,7 @@ endif # which backends to use and sets test-specific options. .PHONY: test-% test-%: - $(TEST_RUNNER_EXE) $(CHARON_EXE) $(AENEAS_EXE) $(INPUTS_DIR) $(LLBC_DIR) "$*" $(AENEAS_OPTIONS) + $(TEST_RUNNER_EXE) $(CHARON_EXE) $(AENEAS_EXE) $(LLBC_DIR) $(INPUTS_DIR)/"$*" $(AENEAS_OPTIONS) echo "# Test $* done" # ============================================================================= -- cgit v1.2.3 From c0a6916549b55fbae2226e4c34af45e500928645 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 May 2024 14:56:26 +0200 Subject: Fix running individual tests --- Makefile | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index b3dc9f2b..ca3bd66c 100644 --- a/Makefile +++ b/Makefile @@ -47,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 @@ -166,14 +171,13 @@ test-all: $(INPUTS_LIST) ifdef IN_CI # In CI we do extra sanity checks. test-%: AENEAS_OPTIONS += -checks -else -test-%: check-charon endif # 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-%: +test-%: build-dev $(TEST_RUNNER_EXE) $(CHARON_EXE) $(AENEAS_EXE) $(LLBC_DIR) $(INPUTS_DIR)/"$*" $(AENEAS_OPTIONS) echo "# Test $* done" -- cgit v1.2.3 From 4d3778bea3112168645efc03308056ec341abb5f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 May 2024 15:47:20 +0200 Subject: runner: Pass options in special comments --- Makefile | 4 ---- 1 file changed, 4 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index ca3bd66c..bda88c74 100644 --- a/Makefile +++ b/Makefile @@ -159,10 +159,6 @@ verify: INPUTS_LIST = $(wildcard $(INPUTS_DIR)/*) # Remove the directory prefix, replace with `test-` INPUTS_LIST := $(subst $(INPUTS_DIR)/,test-,$(INPUTS_LIST)) -# Remove some tests we don't want to run. -# FIXME: move this information to the file itself -INPUTS_LIST := $(filter-out test-hashmap_utils.rs,$(INPUTS_LIST)) -INPUTS_LIST := $(filter-out test-nested_borrows.rs,$(INPUTS_LIST)) # Run all the tests we found. .PHONY: test-all -- cgit v1.2.3