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

---
 tests/test_runner/.ocamlformat            |  0
 tests/test_runner/aeneas_test_runner.opam | 27 +++++++++++++++++++++++++++
 tests/test_runner/dune                    |  4 ++++
 tests/test_runner/dune-project            | 25 +++++++++++++++++++++++++
 tests/test_runner/run_test.ml             | 30 ++++++++++++++++++++++++++++++
 5 files changed, 86 insertions(+)
 create mode 100644 tests/test_runner/.ocamlformat
 create mode 100644 tests/test_runner/aeneas_test_runner.opam
 create mode 100644 tests/test_runner/dune
 create mode 100644 tests/test_runner/dune-project
 create mode 100644 tests/test_runner/run_test.ml

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/.ocamlformat b/tests/test_runner/.ocamlformat
new file mode 100644
index 00000000..e69de29b
diff --git a/tests/test_runner/aeneas_test_runner.opam b/tests/test_runner/aeneas_test_runner.opam
new file mode 100644
index 00000000..b57cc9f6
--- /dev/null
+++ b/tests/test_runner/aeneas_test_runner.opam
@@ -0,0 +1,27 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "0.1"
+authors: ["Son Ho" "Guillaume Boisseau"]
+license: "Apache-2.0"
+homepage: "https://github.com/AeneasVerif/aeneas"
+bug-reports: "https://github.com/AeneasVerif/aeneas/issues"
+depends: [
+  "ocaml"
+  "dune" {>= "3.12"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/AeneasVerif/aeneas.git"
diff --git a/tests/test_runner/dune b/tests/test_runner/dune
new file mode 100644
index 00000000..7da7a96d
--- /dev/null
+++ b/tests/test_runner/dune
@@ -0,0 +1,4 @@
+(executable
+ (public_name test_runner)
+ (libraries unix)
+ (name run_test))
diff --git a/tests/test_runner/dune-project b/tests/test_runner/dune-project
new file mode 100644
index 00000000..c614e923
--- /dev/null
+++ b/tests/test_runner/dune-project
@@ -0,0 +1,25 @@
+(lang dune 3.12)
+
+(name aeneas_test_runner)
+
+(version 0.1)
+
+(generate_opam_files true)
+
+(source
+ (uri git+https://github.com/AeneasVerif/aeneas.git))
+
+(homepage "https://github.com/AeneasVerif/aeneas")
+
+(bug_reports "https://github.com/AeneasVerif/aeneas/issues")
+
+(authors
+  "Son Ho"
+  "Guillaume Boisseau")
+
+(license Apache-2.0)
+
+(package
+ (name aeneas_test_runner)
+ (depends ocaml dune)
+)
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
new file mode 100644
index 00000000..379abe04
--- /dev/null
+++ b/tests/test_runner/run_test.ml
@@ -0,0 +1,30 @@
+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
+      let dest_dir = concat_path [ "tests"; backend; subdir ] in
+      let args =
+        [| aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend |]
+      in
+      let args = Array.append args (Array.of_list options) in
+
+      (* Debug arguments *)
+      print_string "[test_runner] Running: ";
+      Array.iter
+        (fun x ->
+          print_string x;
+          print_string " ")
+        args;
+      print_endline "";
+
+      (* Run Aeneas *)
+      let pid =
+        Unix.create_process aeneas_path args Unix.stdin Unix.stdout Unix.stderr
+      in
+      let _ = Unix.waitpid [] pid in
+      ()
+  | _ -> ()
-- 
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

---
 tests/test_runner/run_test.ml | 29 ++++++++++++++++++++++++++---
 1 file changed, 26 insertions(+), 3 deletions(-)

(limited to 'tests/test_runner')

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


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

---
 tests/test_runner/run_test.ml | 57 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 57 insertions(+)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 52ff7276..949d5307 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -21,6 +21,63 @@ let () =
         | _ -> test_name
       in
 
+      (* File-specific options *)
+      (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *)
+      let use_fuel =
+        match (backend, test_name) with
+        | ( "coq",
+            ( "arrays" | "betree_main" | "demo" | "hashmap" | "hashmap_main"
+            | "loops" ) ) ->
+            true
+        | "fstar", "demo" -> true
+        | _ -> false
+      in
+      let options = if use_fuel then "-use-fuel" :: options else options in
+
+      let decrease_template_clauses =
+        backend = "fstar"
+        &&
+        match test_name with
+        | "arrays" | "betree_main" | "betree_main-special" | "hashmap"
+        | "hashmap_main" | "loops" | "traits" ->
+            true
+        | _ -> false
+      in
+      let options =
+        if decrease_template_clauses then
+          "-decreases-clauses" :: "-template-clauses" :: options
+        else options
+      in
+
+      let extra_options =
+        match (backend, test_name) with
+        (* Additional, custom test on the betree: translate it without `-backward-no-state-update`. *)
+        (* This generates very ugly code, but is good to test the translation. *)
+        | _, "betree_main-special" ->
+            [ "-test-trans-units"; "-state"; "-split-files" ]
+        | _, "betree_main" ->
+            [
+              "-backward-no-state-update";
+              "-test-trans-units";
+              "-state";
+              "-split-files";
+            ]
+        | _, "bitwise" -> [ "-test-trans-units" ]
+        | _, "constants" -> [ "-test-trans-units" ]
+        | _, "external" -> [ "-test-trans-units"; "-state"; "-split-files" ]
+        | _, "hashmap_main" -> [ "-state"; "-split-files" ]
+        | _, "no_nested_borrows" -> [ "-test-trans-units" ]
+        | _, "paper" -> [ "-test-trans-units" ]
+        | _, "polonius_list" -> [ "-test-trans-units" ]
+        | "fstar", "arrays" -> [ "-split-files" ]
+        | "fstar", "loops" -> [ "-split-files" ]
+        (* We add a custom import in the Hashmap.lean file: we do not want to overwrite it *)
+        | "lean", "hashmap" -> [ "-split-files"; "-no-gen-lib-entry" ]
+        | _, "hashmap" -> [ "-split-files" ]
+        | _ -> []
+      in
+      let options = List.append extra_options options in
+
       let test_file_name =
         match test_name with
         | "betree_main-special" -> "betree_main"
-- 
cgit v1.2.3


From 9e834db4174a900845199ccb189b575a20f11eda Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 23 May 2024 09:58:36 +0200
Subject: Cleanup test runner

---
 tests/test_runner/run_test.ml | 223 +++++++++++++++++++++++-------------------
 1 file changed, 124 insertions(+), 99 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 949d5307..1ec2d1c8 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -1,110 +1,135 @@
-let concat_path = List.fold_left Filename.concat ""
+(* Paths to use for tests *)
+type test_env = { aeneas_path : string; llbc_dir : string }
 
-let () =
-  match Array.to_list Sys.argv with
-  (* Ad-hoc argument passing for now. *)
-  | _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
+(* The data for a specific test to run *)
+type test_case = {
+  name : string;
+  backend : string;
+  subdir : string;
+  extra_aeneas_options : string list;
+}
 
-      (* File-specific options *)
-      (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *)
-      let use_fuel =
-        match (backend, test_name) with
-        | ( "coq",
-            ( "arrays" | "betree_main" | "demo" | "hashmap" | "hashmap_main"
-            | "loops" ) ) ->
-            true
-        | "fstar", "demo" -> true
-        | _ -> false
-      in
-      let options = if use_fuel then "-use-fuel" :: options else options in
+(* Run Aeneas on a specific input with the given options *)
+let run_test env case =
+  let concat_path = List.fold_left Filename.concat "" in
+  let input_file = concat_path [ env.llbc_dir; "llbc"; case.name ] ^ ".llbc" in
+  let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in
+  let args =
+    [|
+      env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; case.backend;
+    |]
+  in
+  let args = Array.append args (Array.of_list case.extra_aeneas_options) in
 
-      let decrease_template_clauses =
-        backend = "fstar"
-        &&
-        match test_name with
-        | "arrays" | "betree_main" | "betree_main-special" | "hashmap"
-        | "hashmap_main" | "loops" | "traits" ->
-            true
-        | _ -> false
-      in
-      let options =
-        if decrease_template_clauses then
-          "-decreases-clauses" :: "-template-clauses" :: options
-        else options
-      in
+  (* Debug arguments *)
+  print_string "[test_runner] Running: ";
+  Array.iter
+    (fun x ->
+      print_string x;
+      print_string " ")
+    args;
+  print_endline "";
 
-      let extra_options =
-        match (backend, test_name) with
-        (* Additional, custom test on the betree: translate it without `-backward-no-state-update`. *)
-        (* This generates very ugly code, but is good to test the translation. *)
-        | _, "betree_main-special" ->
-            [ "-test-trans-units"; "-state"; "-split-files" ]
-        | _, "betree_main" ->
-            [
-              "-backward-no-state-update";
-              "-test-trans-units";
-              "-state";
-              "-split-files";
-            ]
-        | _, "bitwise" -> [ "-test-trans-units" ]
-        | _, "constants" -> [ "-test-trans-units" ]
-        | _, "external" -> [ "-test-trans-units"; "-state"; "-split-files" ]
-        | _, "hashmap_main" -> [ "-state"; "-split-files" ]
-        | _, "no_nested_borrows" -> [ "-test-trans-units" ]
-        | _, "paper" -> [ "-test-trans-units" ]
-        | _, "polonius_list" -> [ "-test-trans-units" ]
-        | "fstar", "arrays" -> [ "-split-files" ]
-        | "fstar", "loops" -> [ "-split-files" ]
-        (* We add a custom import in the Hashmap.lean file: we do not want to overwrite it *)
-        | "lean", "hashmap" -> [ "-split-files"; "-no-gen-lib-entry" ]
-        | _, "hashmap" -> [ "-split-files" ]
-        | _ -> []
-      in
-      let options = List.append extra_options options in
+  (* Run Aeneas *)
+  let pid =
+    Unix.create_process env.aeneas_path args Unix.stdin Unix.stdout Unix.stderr
+  in
+  let _ = Unix.waitpid [] pid in
+  ()
+
+(* File-specific options *)
+let test_options backend test_name =
+  (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *)
+  let use_fuel =
+    match (backend, test_name) with
+    | ( "coq",
+        ( "arrays" | "betree_main" | "demo" | "hashmap" | "hashmap_main"
+        | "loops" ) ) ->
+        true
+    | "fstar", "demo" -> true
+    | _ -> false
+  in
+  let options = if use_fuel then "-use-fuel" :: [] else [] in
+
+  let decrease_template_clauses =
+    backend = "fstar"
+    &&
+    match test_name with
+    | "arrays" | "betree_main" | "betree_main-special" | "hashmap"
+    | "hashmap_main" | "loops" | "traits" ->
+        true
+    | _ -> false
+  in
+  let options =
+    if decrease_template_clauses then
+      "-decreases-clauses" :: "-template-clauses" :: options
+    else options
+  in
+
+  let extra_options =
+    match (backend, test_name) with
+    (* Additional, custom test on the betree: translate it without `-backward-no-state-update`. *)
+    (* This generates very ugly code, but is good to test the translation. *)
+    | _, "betree_main-special" ->
+        [ "-test-trans-units"; "-state"; "-split-files" ]
+    | _, "betree_main" ->
+        [
+          "-backward-no-state-update";
+          "-test-trans-units";
+          "-state";
+          "-split-files";
+        ]
+    | _, "bitwise" -> [ "-test-trans-units" ]
+    | _, "constants" -> [ "-test-trans-units" ]
+    | _, "external" -> [ "-test-trans-units"; "-state"; "-split-files" ]
+    | _, "hashmap_main" -> [ "-state"; "-split-files" ]
+    | _, "no_nested_borrows" -> [ "-test-trans-units" ]
+    | _, "paper" -> [ "-test-trans-units" ]
+    | _, "polonius_list" -> [ "-test-trans-units" ]
+    | "fstar", "arrays" -> [ "-split-files" ]
+    | "fstar", "loops" -> [ "-split-files" ]
+    (* We add a custom import in the Hashmap.lean file: we do not want to overwrite it *)
+    | "lean", "hashmap" -> [ "-split-files"; "-no-gen-lib-entry" ]
+    | _, "hashmap" -> [ "-split-files" ]
+    | _ -> []
+  in
+  let options = List.append extra_options options in
+  options
+
+(* The subdirectory in which to store the outputs. *)
+(* This reproduces the file layout that was set by the old Makefile. FIXME: cleanup *)
+let test_subdir backend test_name =
+  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
+
+let () =
+  match Array.to_list Sys.argv with
+  (* Ad-hoc argument passing for now. *)
+  | _exe_path :: aeneas_path :: llbc_dir :: test_name :: backend :: options ->
+      let subdir = test_subdir backend test_name in
+      let options = List.append (test_options backend test_name) options 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 |]
-      in
-      let args = Array.append args (Array.of_list options) in
-
-      (* Debug arguments *)
-      print_string "[test_runner] Running: ";
-      Array.iter
-        (fun x ->
-          print_string x;
-          print_string " ")
-        args;
-      print_endline "";
-
-      (* Run Aeneas *)
-      let pid =
-        Unix.create_process aeneas_path args Unix.stdin Unix.stdout Unix.stderr
-      in
-      let _ = Unix.waitpid [] pid in
-      ()
+      run_test { aeneas_path; llbc_dir }
+        {
+          name = test_file_name;
+          backend;
+          subdir;
+          extra_aeneas_options = options;
+        }
   | _ -> ()
-- 
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

---
 tests/test_runner/run_test.ml | 38 +++++++++++++++++++++++---------------
 1 file changed, 23 insertions(+), 15 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 1ec2d1c8..52619c4a 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -116,20 +116,28 @@ let test_subdir backend test_name =
 let () =
   match Array.to_list Sys.argv with
   (* Ad-hoc argument passing for now. *)
-  | _exe_path :: aeneas_path :: llbc_dir :: test_name :: backend :: options ->
-      let subdir = test_subdir backend test_name in
-      let options = List.append (test_options backend test_name) options in
-
-      let test_file_name =
+  | _exe_path :: aeneas_path :: llbc_dir :: test_name :: options ->
+      let tests_env = { aeneas_path; llbc_dir } in
+      (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
+      let backends =
         match test_name with
-        | "betree_main-special" -> "betree_main"
-        | _ -> test_name
+        | "betree_main-special" -> [ "fstar" ]
+        | _ -> [ "coq"; "lean"; "fstar" ]
       in
-      run_test { aeneas_path; llbc_dir }
-        {
-          name = test_file_name;
-          backend;
-          subdir;
-          extra_aeneas_options = options;
-        }
-  | _ -> ()
+      List.iter
+        (fun backend ->
+          let subdir = test_subdir backend test_name in
+          let extra_aeneas_options =
+            List.append (test_options backend test_name) options
+          in
+          let test_file_name =
+            match test_name with
+            | "betree_main-special" -> "betree_main"
+            | _ -> test_name
+          in
+          let test_case =
+            { name = test_file_name; backend; subdir; extra_aeneas_options }
+          in
+          run_test tests_env test_case)
+        backends
+  | _ -> failwith "Incorrect options passed to test runner"
-- 
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.
---
 tests/test_runner/run_test.ml | 22 ++++------------------
 1 file changed, 4 insertions(+), 18 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 52619c4a..d3fe8836 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -55,8 +55,8 @@ let test_options backend test_name =
     backend = "fstar"
     &&
     match test_name with
-    | "arrays" | "betree_main" | "betree_main-special" | "hashmap"
-    | "hashmap_main" | "loops" | "traits" ->
+    | "arrays" | "betree_main" | "hashmap" | "hashmap_main" | "loops" | "traits"
+      ->
         true
     | _ -> false
   in
@@ -68,10 +68,6 @@ let test_options backend test_name =
 
   let extra_options =
     match (backend, test_name) with
-    (* Additional, custom test on the betree: translate it without `-backward-no-state-update`. *)
-    (* This generates very ugly code, but is good to test the translation. *)
-    | _, "betree_main-special" ->
-        [ "-test-trans-units"; "-state"; "-split-files" ]
     | _, "betree_main" ->
         [
           "-backward-no-state-update";
@@ -104,7 +100,6 @@ let test_subdir backend test_name =
   | "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
   | ( _,
@@ -119,24 +114,15 @@ let () =
   | _exe_path :: aeneas_path :: llbc_dir :: test_name :: options ->
       let tests_env = { aeneas_path; llbc_dir } in
       (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
-      let backends =
-        match test_name with
-        | "betree_main-special" -> [ "fstar" ]
-        | _ -> [ "coq"; "lean"; "fstar" ]
-      in
+      let backends = [ "coq"; "lean"; "fstar" ] in
       List.iter
         (fun backend ->
           let subdir = test_subdir backend test_name in
           let extra_aeneas_options =
             List.append (test_options backend test_name) options
           in
-          let test_file_name =
-            match test_name with
-            | "betree_main-special" -> "betree_main"
-            | _ -> test_name
-          in
           let test_case =
-            { name = test_file_name; backend; subdir; extra_aeneas_options }
+            { name = test_name; backend; subdir; extra_aeneas_options }
           in
           run_test tests_env test_case)
         backends
-- 
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

---
 tests/test_runner/run_test.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index d3fe8836..8b4a4208 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -12,7 +12,7 @@ type test_case = {
 (* Run Aeneas on a specific input with the given options *)
 let run_test env case =
   let concat_path = List.fold_left Filename.concat "" in
-  let input_file = concat_path [ env.llbc_dir; "llbc"; case.name ] ^ ".llbc" in
+  let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in
   let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in
   let args =
     [|
-- 
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

---
 tests/test_runner/run_test.ml | 124 +++++++++++++++++++++++++++++++++++-------
 1 file changed, 104 insertions(+), 20 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 8b4a4208..d80231d0 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -1,26 +1,26 @@
 (* Paths to use for tests *)
-type test_env = { aeneas_path : string; llbc_dir : string }
+type aeneas_env = { aeneas_path : string; llbc_dir : string }
 
-(* The data for a specific test to run *)
-type test_case = {
+type charon_env = {
+  charon_path : string;
+  inputs_dir : string;
+  llbc_dir : string;
+}
+
+(* The data for a specific test to run aeneas on *)
+type aeneas_test_case = {
   name : string;
   backend : string;
   subdir : string;
   extra_aeneas_options : string list;
 }
 
-(* Run Aeneas on a specific input with the given options *)
-let run_test env case =
-  let concat_path = List.fold_left Filename.concat "" in
-  let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in
-  let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in
-  let args =
-    [|
-      env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; case.backend;
-    |]
-  in
-  let args = Array.append args (Array.of_list case.extra_aeneas_options) in
+(* The data for a specific test to generate llbc for *)
+type charon_test_case = { name : string; extra_charon_options : string list }
 
+let concat_path = List.fold_left Filename.concat ""
+
+let run_command args =
   (* Debug arguments *)
   print_string "[test_runner] Running: ";
   Array.iter
@@ -30,15 +30,66 @@ let run_test env case =
     args;
   print_endline "";
 
-  (* Run Aeneas *)
+  (* Run the command *)
   let pid =
-    Unix.create_process env.aeneas_path args Unix.stdin Unix.stdout Unix.stderr
+    Unix.create_process args.(0) args Unix.stdin Unix.stdout Unix.stderr
   in
   let _ = Unix.waitpid [] pid in
   ()
 
+(* Run Aeneas on a specific input with the given options *)
+let run_aeneas (env : aeneas_env) (case : aeneas_test_case) =
+  let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in
+  let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in
+  let args =
+    [|
+      env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; case.backend;
+    |]
+  in
+  let args = Array.append args (Array.of_list case.extra_aeneas_options) in
+  (* Run Aeneas *)
+  run_command args
+
+(* Run Charon on a specific input with the given options *)
+let run_charon (env : charon_env) (case : charon_test_case) =
+  let input_crate = concat_path [ env.inputs_dir; case.name ] in
+  let input_file = input_crate ^ ".rs" in
+  if Sys.file_exists input_file then
+    let args =
+      [|
+        env.charon_path;
+        "--no-cargo";
+        "--input";
+        input_file;
+        "--crate";
+        case.name;
+        "--dest";
+        env.llbc_dir;
+      |]
+    in
+    let args = Array.append args (Array.of_list case.extra_charon_options) in
+    (* Run Charon on the rust file *)
+    run_command args
+  else if Sys.file_exists input_crate then
+    match Sys.getenv_opt "IN_CI" with
+    | None ->
+        let args = [| env.charon_path; "--dest"; env.llbc_dir |] in
+        let args =
+          Array.append args (Array.of_list case.extra_charon_options)
+        in
+        (* Run Charon inside the crate *)
+        Unix.chdir input_crate;
+        run_command args
+    | Some _ ->
+        (* Crates with dependencies must be generated separately in CI. We skip
+           here and trust that CI takes care to generate the necessary llbc
+           file. *)
+        print_endline
+          "Warn: IN_CI is set; we skip generating llbc files for whole crates"
+  else failwith ("Neither " ^ input_file ^ " nor " ^ input_crate ^ " exist.")
+
 (* File-specific options *)
-let test_options backend test_name =
+let aeneas_options_for_test backend test_name =
   (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *)
   let use_fuel =
     match (backend, test_name) with
@@ -92,6 +143,27 @@ let test_options backend test_name =
   let options = List.append extra_options options in
   options
 
+(* File-specific options *)
+let charon_options_for_test test_name =
+  (* Possible to add `--no-code-duplication` for `hashmap_main` if we use the optimized MIR *)
+  let no_code_dup =
+    match test_name with
+    | "constants" | "external" | "nested_borrows" | "no_nested_borrows"
+    | "paper" ->
+        [ "--no-code-duplication" ]
+    | _ -> []
+  in
+  let extra_options =
+    (* $(LLBC_DIR)/betree_main.llbc: CHARON_OPTIONS += --polonius --opaque=betree_utils --crate betree_main *)
+    match test_name with
+    | "betree_main" ->
+        [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ]
+    | "hashmap_main" -> [ "--opaque=hashmap_utils" ]
+    | "polonius_list" -> [ "--polonius" ]
+    | _ -> []
+  in
+  List.append no_code_dup extra_options
+
 (* The subdirectory in which to store the outputs. *)
 (* This reproduces the file layout that was set by the old Makefile. FIXME: cleanup *)
 let test_subdir backend test_name =
@@ -111,7 +183,7 @@ let test_subdir backend test_name =
 let () =
   match Array.to_list Sys.argv with
   (* Ad-hoc argument passing for now. *)
-  | _exe_path :: aeneas_path :: llbc_dir :: test_name :: options ->
+  | _exe_path :: "aeneas" :: aeneas_path :: llbc_dir :: test_name :: options ->
       let tests_env = { aeneas_path; llbc_dir } in
       (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
       let backends = [ "coq"; "lean"; "fstar" ] in
@@ -119,11 +191,23 @@ let () =
         (fun backend ->
           let subdir = test_subdir backend test_name in
           let extra_aeneas_options =
-            List.append (test_options backend test_name) options
+            List.append (aeneas_options_for_test backend test_name) options
           in
           let test_case =
             { name = test_name; backend; subdir; extra_aeneas_options }
           in
-          run_test tests_env test_case)
+          run_aeneas tests_env test_case)
         backends
+  | _exe_path :: "charon" :: charon_path :: inputs_dir :: llbc_dir :: test_name
+    :: options ->
+      let tests_env = { charon_path; inputs_dir; llbc_dir } in
+      let extra_charon_options =
+        List.append (charon_options_for_test test_name) options
+      in
+      (* FIXME: remove this special case *)
+      let test_name =
+        if test_name = "betree_main" then "betree" else test_name
+      in
+      let test_case = { name = test_name; extra_charon_options } in
+      run_charon tests_env test_case
   | _ -> failwith "Incorrect options passed to test runner"
-- 
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

---
 tests/test_runner/dune        |  2 +-
 tests/test_runner/run_test.ml | 38 ++++++++++++++++++++++----------------
 2 files changed, 23 insertions(+), 17 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/dune b/tests/test_runner/dune
index 7da7a96d..7caf661f 100644
--- a/tests/test_runner/dune
+++ b/tests/test_runner/dune
@@ -1,4 +1,4 @@
 (executable
  (public_name test_runner)
- (libraries unix)
+ (libraries core_unix.sys_unix unix)
  (name run_test))
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index d80231d0..688c81ae 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -16,7 +16,11 @@ type aeneas_test_case = {
 }
 
 (* The data for a specific test to generate llbc for *)
-type charon_test_case = { name : string; extra_charon_options : string list }
+type charon_test_case = {
+  name : string;
+  path : string;
+  extra_charon_options : string list;
+}
 
 let concat_path = List.fold_left Filename.concat ""
 
@@ -52,15 +56,14 @@ let run_aeneas (env : aeneas_env) (case : aeneas_test_case) =
 
 (* Run Charon on a specific input with the given options *)
 let run_charon (env : charon_env) (case : charon_test_case) =
-  let input_crate = concat_path [ env.inputs_dir; case.name ] in
-  let input_file = input_crate ^ ".rs" in
-  if Sys.file_exists input_file then
+  let input_path = concat_path [ env.inputs_dir; case.path ] in
+  if Sys_unix.is_file_exn input_path then
     let args =
       [|
         env.charon_path;
         "--no-cargo";
         "--input";
-        input_file;
+        input_path;
         "--crate";
         case.name;
         "--dest";
@@ -70,7 +73,7 @@ let run_charon (env : charon_env) (case : charon_test_case) =
     let args = Array.append args (Array.of_list case.extra_charon_options) in
     (* Run Charon on the rust file *)
     run_command args
-  else if Sys.file_exists input_crate then
+  else if Sys.is_directory input_path then
     match Sys.getenv_opt "IN_CI" with
     | None ->
         let args = [| env.charon_path; "--dest"; env.llbc_dir |] in
@@ -78,7 +81,7 @@ let run_charon (env : charon_env) (case : charon_test_case) =
           Array.append args (Array.of_list case.extra_charon_options)
         in
         (* Run Charon inside the crate *)
-        Unix.chdir input_crate;
+        Unix.chdir input_path;
         run_command args
     | Some _ ->
         (* Crates with dependencies must be generated separately in CI. We skip
@@ -86,7 +89,7 @@ let run_charon (env : charon_env) (case : charon_test_case) =
            file. *)
         print_endline
           "Warn: IN_CI is set; we skip generating llbc files for whole crates"
-  else failwith ("Neither " ^ input_file ^ " nor " ^ input_crate ^ " exist.")
+  else failwith ("`" ^ input_path ^ "` is not a file or a directory.")
 
 (* File-specific options *)
 let aeneas_options_for_test backend test_name =
@@ -154,9 +157,8 @@ let charon_options_for_test test_name =
     | _ -> []
   in
   let extra_options =
-    (* $(LLBC_DIR)/betree_main.llbc: CHARON_OPTIONS += --polonius --opaque=betree_utils --crate betree_main *)
     match test_name with
-    | "betree_main" ->
+    | "betree" ->
         [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ]
     | "hashmap_main" -> [ "--opaque=hashmap_utils" ]
     | "polonius_list" -> [ "--polonius" ]
@@ -183,8 +185,13 @@ let test_subdir backend test_name =
 let () =
   match Array.to_list Sys.argv with
   (* Ad-hoc argument passing for now. *)
-  | _exe_path :: "aeneas" :: aeneas_path :: llbc_dir :: test_name :: options ->
+  | _exe_path :: "aeneas" :: aeneas_path :: llbc_dir :: test_path :: options ->
       let tests_env = { aeneas_path; llbc_dir } in
+      let test_name = Filename.remove_extension test_path in
+      (* FIXME: remove this special case *)
+      let test_name =
+        if test_name = "betree" then "betree_main" else test_name
+      in
       (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
       let backends = [ "coq"; "lean"; "fstar" ] in
       List.iter
@@ -198,16 +205,15 @@ let () =
           in
           run_aeneas tests_env test_case)
         backends
-  | _exe_path :: "charon" :: charon_path :: inputs_dir :: llbc_dir :: test_name
+  | _exe_path :: "charon" :: charon_path :: inputs_dir :: llbc_dir :: test_path
     :: options ->
       let tests_env = { charon_path; inputs_dir; llbc_dir } in
+      let test_name = Filename.remove_extension test_path in
       let extra_charon_options =
         List.append (charon_options_for_test test_name) options
       in
-      (* FIXME: remove this special case *)
-      let test_name =
-        if test_name = "betree_main" then "betree" else test_name
+      let test_case =
+        { name = test_name; path = test_path; extra_charon_options }
       in
-      let test_case = { name = test_name; extra_charon_options } in
       run_charon tests_env test_case
   | _ -> failwith "Incorrect options passed to test runner"
-- 
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

---
 tests/test_runner/run_test.ml | 46 ++++++++++++++++++++++---------------------
 1 file changed, 24 insertions(+), 22 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 688c81ae..5eff95af 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -1,8 +1,7 @@
 (* Paths to use for tests *)
-type aeneas_env = { aeneas_path : string; llbc_dir : string }
-
-type charon_env = {
+type runner_env = {
   charon_path : string;
+  aeneas_path : string;
   inputs_dir : string;
   llbc_dir : string;
 }
@@ -42,7 +41,7 @@ let run_command args =
   ()
 
 (* Run Aeneas on a specific input with the given options *)
-let run_aeneas (env : aeneas_env) (case : aeneas_test_case) =
+let run_aeneas (env : runner_env) (case : aeneas_test_case) =
   let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in
   let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in
   let args =
@@ -55,7 +54,7 @@ let run_aeneas (env : aeneas_env) (case : aeneas_test_case) =
   run_command args
 
 (* Run Charon on a specific input with the given options *)
-let run_charon (env : charon_env) (case : charon_test_case) =
+let run_charon (env : runner_env) (case : charon_test_case) =
   let input_path = concat_path [ env.inputs_dir; case.path ] in
   if Sys_unix.is_file_exn input_path then
     let args =
@@ -81,8 +80,10 @@ let run_charon (env : charon_env) (case : charon_test_case) =
           Array.append args (Array.of_list case.extra_charon_options)
         in
         (* Run Charon inside the crate *)
+        let old_pwd = Unix.getcwd () in
         Unix.chdir input_path;
-        run_command args
+        run_command args;
+        Unix.chdir old_pwd
     | Some _ ->
         (* Crates with dependencies must be generated separately in CI. We skip
            here and trust that CI takes care to generate the necessary llbc
@@ -185,9 +186,18 @@ let test_subdir backend test_name =
 let () =
   match Array.to_list Sys.argv with
   (* Ad-hoc argument passing for now. *)
-  | _exe_path :: "aeneas" :: aeneas_path :: llbc_dir :: test_path :: options ->
-      let tests_env = { aeneas_path; llbc_dir } in
+  | _exe_path :: charon_path :: aeneas_path :: inputs_dir :: llbc_dir
+    :: test_path :: aeneas_options ->
+      let runner_env = { charon_path; aeneas_path; inputs_dir; llbc_dir } in
       let test_name = Filename.remove_extension test_path in
+
+      let extra_charon_options = charon_options_for_test test_name in
+      let charon_case =
+        { name = test_name; path = test_path; extra_charon_options }
+      in
+      (* Generate the llbc file *)
+      run_charon runner_env charon_case;
+
       (* FIXME: remove this special case *)
       let test_name =
         if test_name = "betree" then "betree_main" else test_name
@@ -198,22 +208,14 @@ let () =
         (fun backend ->
           let subdir = test_subdir backend test_name in
           let extra_aeneas_options =
-            List.append (aeneas_options_for_test backend test_name) options
+            List.append
+              (aeneas_options_for_test backend test_name)
+              aeneas_options
           in
-          let test_case =
+          let aeneas_case =
             { name = test_name; backend; subdir; extra_aeneas_options }
           in
-          run_aeneas tests_env test_case)
+          (* Process the llbc file for the current backend *)
+          run_aeneas runner_env aeneas_case)
         backends
-  | _exe_path :: "charon" :: charon_path :: inputs_dir :: llbc_dir :: test_path
-    :: options ->
-      let tests_env = { charon_path; inputs_dir; llbc_dir } in
-      let test_name = Filename.remove_extension test_path in
-      let extra_charon_options =
-        List.append (charon_options_for_test test_name) options
-      in
-      let test_case =
-        { name = test_name; path = test_path; extra_charon_options }
-      in
-      run_charon tests_env test_case
   | _ -> failwith "Incorrect options passed to test runner"
-- 
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

---
 tests/test_runner/run_test.ml | 96 ++++++++++++++++++++++++-------------------
 1 file changed, 54 insertions(+), 42 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 5eff95af..8aa6347c 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -2,7 +2,6 @@
 type runner_env = {
   charon_path : string;
   aeneas_path : string;
-  inputs_dir : string;
   llbc_dir : string;
 }
 
@@ -14,8 +13,11 @@ type aeneas_test_case = {
   extra_aeneas_options : string list;
 }
 
+type input_kind = SingleFile | Crate
+
 (* The data for a specific test to generate llbc for *)
 type charon_test_case = {
+  kind : input_kind;
   name : string;
   path : string;
   extra_charon_options : string list;
@@ -55,42 +57,42 @@ let run_aeneas (env : runner_env) (case : aeneas_test_case) =
 
 (* Run Charon on a specific input with the given options *)
 let run_charon (env : runner_env) (case : charon_test_case) =
-  let input_path = concat_path [ env.inputs_dir; case.path ] in
-  if Sys_unix.is_file_exn input_path then
-    let args =
-      [|
-        env.charon_path;
-        "--no-cargo";
-        "--input";
-        input_path;
-        "--crate";
-        case.name;
-        "--dest";
-        env.llbc_dir;
-      |]
-    in
-    let args = Array.append args (Array.of_list case.extra_charon_options) in
-    (* Run Charon on the rust file *)
-    run_command args
-  else if Sys.is_directory input_path then
-    match Sys.getenv_opt "IN_CI" with
-    | None ->
-        let args = [| env.charon_path; "--dest"; env.llbc_dir |] in
-        let args =
-          Array.append args (Array.of_list case.extra_charon_options)
-        in
-        (* Run Charon inside the crate *)
-        let old_pwd = Unix.getcwd () in
-        Unix.chdir input_path;
-        run_command args;
-        Unix.chdir old_pwd
-    | Some _ ->
-        (* Crates with dependencies must be generated separately in CI. We skip
-           here and trust that CI takes care to generate the necessary llbc
-           file. *)
-        print_endline
-          "Warn: IN_CI is set; we skip generating llbc files for whole crates"
-  else failwith ("`" ^ input_path ^ "` is not a file or a directory.")
+  match case.kind with
+  | SingleFile ->
+      let args =
+        [|
+          env.charon_path;
+          "--no-cargo";
+          "--input";
+          case.path;
+          "--crate";
+          case.name;
+          "--dest";
+          env.llbc_dir;
+        |]
+      in
+      let args = Array.append args (Array.of_list case.extra_charon_options) in
+      (* Run Charon on the rust file *)
+      run_command args
+  | Crate -> (
+      match Sys.getenv_opt "IN_CI" with
+      | None ->
+          let args = [| env.charon_path; "--dest"; env.llbc_dir |] in
+          let args =
+            Array.append args (Array.of_list case.extra_charon_options)
+          in
+          (* Run Charon inside the crate *)
+          let old_pwd = Unix.getcwd () in
+          Unix.chdir case.path;
+          run_command args;
+          Unix.chdir old_pwd
+      | Some _ ->
+          (* Crates with dependencies must be generated separately in CI. We skip
+             here and trust that CI takes care to generate the necessary llbc
+             file. *)
+          print_endline
+            "Warn: IN_CI is set; we skip generating llbc files for whole crates"
+      )
 
 (* File-specific options *)
 let aeneas_options_for_test backend test_name =
@@ -186,14 +188,24 @@ let test_subdir backend test_name =
 let () =
   match Array.to_list Sys.argv with
   (* Ad-hoc argument passing for now. *)
-  | _exe_path :: charon_path :: aeneas_path :: inputs_dir :: llbc_dir
-    :: test_path :: aeneas_options ->
-      let runner_env = { charon_path; aeneas_path; inputs_dir; llbc_dir } in
-      let test_name = Filename.remove_extension test_path in
+  | _exe_path :: charon_path :: aeneas_path :: llbc_dir :: test_path
+    :: aeneas_options ->
+      let runner_env = { charon_path; aeneas_path; llbc_dir } in
+      let test_name = Filename.remove_extension (Filename.basename test_path) in
 
+      let charon_kind =
+        if Sys_unix.is_file_exn test_path then SingleFile
+        else if Sys_unix.is_directory_exn test_path then Crate
+        else failwith ("`" ^ test_path ^ "` is not a file or a directory.")
+      in
       let extra_charon_options = charon_options_for_test test_name in
       let charon_case =
-        { name = test_name; path = test_path; extra_charon_options }
+        {
+          path = test_path;
+          name = test_name;
+          kind = charon_kind;
+          extra_charon_options;
+        }
       in
       (* Generate the llbc file *)
       run_charon runner_env charon_case;
-- 
cgit v1.2.3