Implement the generation of stateful backward functions (controlled by an option)

1 files changed, 28 insertions, 6 deletions

diff --git a/Makefile b/Makefile
index c9b0b566..a0ce6d21 100644
--- a/Makefile
+++ b/Makefile
@@ -54,7 +54,8 @@ clean:
 tests: build trans-no_nested_borrows trans-paper \
 	trans-hashmap trans-hashmap_main \
 	trans-external trans-constants \
-	trans-polonius-betree_polonius trans-polonius-betree_main
+	trans-polonius-betree_polonius trans-polonius-betree_main \
+	test-trans-polonius-betree_main
 
 # Verify the F* files generated by the translation
 .PHONY: verify
@@ -66,6 +67,12 @@ verify: build tests
 format:
 	cd compiler && dune promote
 
+# The commands to run Charon to generate the .llbc files
+CHARON_CMD = cd $(CHARON_HOME)/$(CHARON_TEST_SUBFOLDER) && NOT_ALL_TESTS=1 $(MAKE) test-$*
+
+# The command to run Aeneas on the proper llbc file
+AENEAS_CMD = cd compiler && dune exec -- ./$(AENEAS_DRIVER) ../$(CHARON_TESTS_DIR)/$(FILE).llbc -dest ../$(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
+
 # Add specific options to some tests
 trans-no_nested_borrows trans-paper: \
 	TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
@@ -86,19 +93,32 @@ trans-constants: SUBDIR:=misc
 trans-external: TRANS_OPTIONS +=
 trans-external: SUBDIR:=misc
 
-trans-polonius-betree_main: TRANS_OPTIONS += -template-clauses
+BETREE_OPTIONS = -template-clauses
+trans-polonius-betree_main: TRANS_OPTIONS += $(BETREE_OPTIONS) -backward-no-state-update
 trans-polonius-betree_main: SUBDIR:=betree
 
+# Additional test on the betree: translate it without `-backward-no-state-update`.
+# This generates very ugly code, but is good to test the translation.
+test-trans-polonius-betree_main: trans-polonius-betree_main
+test-trans-polonius-betree_main: TRANS_OPTIONS += $(BETREE_OPTIONS)
+test-trans-polonius-betree_main: SUBDIR:=betree_back_stateful
+test-trans-polonius-betree_main: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc
+test-trans-polonius-betree_main: FILE = betree_main
+test-trans-polonius-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-polonius-%
+gen-llbc-polonius-%: CHARON_TEST_SUBFOLDER = tests-polonius
 gen-llbc-polonius-%: build
-	cd $(CHARON_HOME)/tests-polonius && NOT_ALL_TESTS=1 $(MAKE) test-$*
+	$(CHARON_CMD)
 
 .PHONY: gen-llbc-%
+gen-llbc-%: CHARON_TEST_SUBFOLDER = tests
 gen-llbc-%: build
-	cd $(CHARON_HOME)/tests && NOT_ALL_TESTS=1 $(MAKE) test-$*
+	$(CHARON_CMD)
 
 # Generic rule to test the translation of an LLBC file.
 # Note that the files requiring the Polonius borrow-checker are generated
@@ -107,8 +127,10 @@ gen-llbc-%: build
 trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc
 trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc
 
+trans-polonius-%: FILE = $*
 trans-polonius-%: gen-llbc-polonius-%
-	cd compiler && dune exec -- ./$(AENEAS_DRIVER) ../$(CHARON_TESTS_DIR)/$*.llbc -dest ../$(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
+	$(AENEAS_CMD)
 
+trans-%: FILE = $*
 trans-%: gen-llbc-%
-	cd compiler && dune exec -- ./$(AENEAS_DRIVER) ../$(CHARON_TESTS_DIR)/$*.llbc -dest ../$(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
+	$(AENEAS_CMD)