Merge pull request #167 from AeneasVerif/bump-charon

3 files changed, 23 insertions, 78 deletions

diff --git a/Makefile b/Makefile
index f4bb8f9e..414f562d 100644
--- a/Makefile
+++ b/Makefile
@@ -20,11 +20,6 @@ REGEN_LLBC ?=
 # The path to Charon
 CHARON_HOME ?= ../charon
 
-# The paths to the test directories in Charon (Aeneas will look for the .llbc
-# files in there).
-CHARON_TESTS_REGULAR_DIR ?= $(CHARON_HOME)/tests
-CHARON_TESTS_POLONIUS_DIR ?= $(CHARON_HOME)/tests-polonius
-
 # 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
@@ -36,7 +31,7 @@ OPTIONS ?=
 # The rules use (and update) the following variables
 #
 # The Charon test directory where to look for the .llbc files
-CHARON_TEST_DIR =
+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
@@ -94,8 +89,8 @@ test: build-dev test-all
 test-all: test-no_nested_borrows test-paper \
 	test-hashmap test-hashmap_main \
 	test-external test-constants \
-	test-polonius_list testp-betree_main \
-	ctest-testp-betree_main \
+	test-polonius_list test-betree_main \
+	ctest-test-betree_main \
 	test-loops \
 	test-arrays test-traits test-bitwise test-demo
 
@@ -220,97 +215,57 @@ thol4-bitwise: SUBDIR := misc-bitwise
 thol4-bitwise: OPTIONS +=
 
 BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses
-testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files
-testp-betree_main: SUBDIR:=betree
-tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
-tcoqp-betree_main: OPTIONS += -use-fuel
-tleanp-betree_main: SUBDIR :=
-tleanp-betree_main: OPTIONS +=
+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 +=
 
 # 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-testp-betree_main
-ctest-testp-betree_main: testp-betree_main
-ctest-testp-betree_main: OPTIONS += -backend fstar -test-trans-units -state -split-files
-ctest-testp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
-ctest-testp-betree_main: BACKEND_SUBDIR := "fstar"
-ctest-testp-betree_main: SUBDIR:=betree_back_stateful
-ctest-testp-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
-ctest-testp-betree_main: FILE = betree_main
-ctest-testp-betree_main:
+.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 += $(BETREE_FSTAR_OPTIONS)
+ctest-test-betree_main: BACKEND_SUBDIR := "fstar"
+ctest-test-betree_main: SUBDIR:=betree_back_stateful
+ctest-test-betree_main: FILE = betree_main
+ctest-test-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-%
-gen-llbc-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
 gen-llbc-%:
 	$(CHARON_CMD)
 
-# "p" stands for "Polonius"
-.PHONY: gen-llbcp-%
-gen-llbcp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
-gen-llbcp-%:
-	$(CHARON_CMD)
-
-# Generic rules to test the testlation of an LLBC file.
-# Note that the files requiring the Polonius borrow-checker are generated
-# in the tests-polonius subdirectory.
+# Generic rules to test the translation of an LLBC file.
 .PHONY: test-%
-test-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
 test-%: FILE = $*
 test-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-%
 	echo "# Test $* done"
 
-# "p" stands for "Polonius"
-.PHONY: testp-%
-testp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
-testp-%: FILE = $*
-testp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-%
-	echo "# Test $* done"
-
 .PHONY: tfstar-%
 tfstar-%: OPTIONS += -backend fstar
 tfstar-%: BACKEND_SUBDIR := fstar
 tfstar-%:
 	$(AENEAS_CMD)
 
-# "p" stands for "Polonius"
-.PHONY: tfstarp-%
-tfstarp-%: OPTIONS += -backend fstar
-tfstarp-%: BACKEND_SUBDIR := fstar
-tfstarp-%:
-	$(AENEAS_CMD)
-
 .PHONY: tcoq-%
 tcoq-%: OPTIONS += -backend coq
 tcoq-%: BACKEND_SUBDIR := coq
 tcoq-%:
 	$(AENEAS_CMD)
 
-# "p" stands for "Polonius"
-.PHONY: tcoqp-%
-tcoqp-%: OPTIONS += -backend coq
-tcoqp-%: BACKEND_SUBDIR := coq
-tcoqp-%:
-	$(AENEAS_CMD)
-
 .PHONY: tlean-%
 tlean-%: OPTIONS += -backend lean
 tlean-%: BACKEND_SUBDIR := lean
 tlean-%:
 	$(AENEAS_CMD)
 
-# "p" stands for "Polonius"
-.PHONY: tleanp-%
-
-tleanp-%: OPTIONS += -backend lean
-tleanp-%: BACKEND_SUBDIR := lean
-tleanp-%:
-	$(AENEAS_CMD)
-
 # TODO: reactivate HOL4 once traits are parameterized by their associated types
 .PHONY: thol4-%
 thol4-%: OPTIONS += -backend hol4
@@ -321,16 +276,6 @@ thol4-%:
 #thol4-%:
 #	$(AENEAS_CMD)
 
-# TODO: reactivate HOL4 once traits are parameterized by their associated types
-.PHONY: thol4p-%
-thol4p-%: OPTIONS += -backend hol4
-thol4p-%: BACKEND_SUBDIR := hol4
-thol4p-%:
-	echo Ignoring the $* test for HOL4
-
-#thol4p-%:
-#	$(AENEAS_CMD)
-
 # Nix - TODO: add the lean tests
 .PHONY: nix
 nix:
diff --git a/flake.lock b/flake.lock
index 014b0af1..e901898b 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,15 +9,16 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1714483898,
-        "narHash": "sha256-R9c3HgcKZQq6VF7ZBjidiJTtxB2mYNJYxctD1JI7As0=",
+        "lastModified": 1714656338,
+        "narHash": "sha256-+ksk7i8Kzm1V1rR/auH2EGlzGefPYgiuWMfAEH1Efjk=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "eb48f4a62ce7c330d44c1e3c870b2a7271bba73b",
+        "rev": "c54e6dc374fd77b0da8328f34f17a5b44e8d6ed0",
         "type": "github"
       },
       "original": {
         "owner": "aeneasverif",
+        "ref": "main",
         "repo": "charon",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index 6f868e3b..fd94d1d0 100644
--- a/flake.nix
+++ b/flake.nix
@@ -85,8 +85,7 @@
           };
           buildPhase = ''
             # We need to provide the paths to the Charon tests derivations
-            export CHARON_TESTS_REGULAR_DIR=${charon.checks.${system}.tests}
-            export CHARON_TESTS_POLONIUS_DIR=${charon.checks.${system}.tests-polonius}
+            export CHARON_TEST_DIR=${charon.checks.${system}.tests}
 
             # Copy the Aeneas executable, and update the path to it
             cp ${aeneas}/bin/aeneas aeneas