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 ++-----------------------------------------
 tests/test_runner/run_test.ml | 29 ++++++++++++++++++++---
 2 files changed, 28 insertions(+), 56 deletions(-)

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)
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 379abe04..52ff7276 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -3,9 +3,32 @@ let concat_path = List.fold_left Filename.concat ""
 let () =
   match Array.to_list Sys.argv with
   (* Ad-hoc argument passing for now. *)
-  | _exe_path :: aeneas_path :: tests_dir :: test_name :: subdir :: backend
-    :: options ->
-      let input_file = concat_path [ tests_dir; "llbc"; test_name ] ^ ".llbc" in
+  | _exe_path :: aeneas_path :: tests_dir :: test_name :: backend :: options ->
+      (* Reproduces the file layout that was set by the Makefile. FIXME: cleanup *)
+      let subdir =
+        match (backend, test_name) with
+        | "lean", "demo" -> "Demo"
+        | "lean", _ -> "."
+        | _, ("arrays" | "demo" | "hashmap" | "traits") -> test_name
+        | _, "betree_main" -> "betree"
+        | _, "betree_main-special" -> "betree_back_stateful"
+        | _, "hashmap_main" -> "hashmap_on_disk"
+        | "hol4", _ -> "misc-" ^ test_name
+        | ( _,
+            ( "bitwise" | "constants" | "external" | "loops"
+            | "no_nested_borrows" | "paper" | "polonius_list" ) ) ->
+            "misc"
+        | _ -> test_name
+      in
+
+      let test_file_name =
+        match test_name with
+        | "betree_main-special" -> "betree_main"
+        | _ -> test_name
+      in
+      let input_file =
+        concat_path [ tests_dir; "llbc"; test_file_name ] ^ ".llbc"
+      in
       let dest_dir = concat_path [ "tests"; backend; subdir ] in
       let args =
         [| aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend |]
-- 
cgit v1.2.3