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

---
 tests/src/arrays.rs            | 3 +++
 tests/src/bitwise.rs           | 1 +
 tests/src/constants.rs         | 2 ++
 tests/src/demo.rs              | 1 +
 tests/src/external.rs          | 3 +++
 tests/src/hashmap.rs           | 8 ++++++++
 tests/src/hashmap_main.rs      | 6 ++++++
 tests/src/hashmap_utils.rs     | 1 +
 tests/src/loops.rs             | 3 +++
 tests/src/nested_borrows.rs    | 2 ++
 tests/src/no_nested_borrows.rs | 2 ++
 tests/src/paper.rs             | 2 ++
 tests/src/polonius_list.rs     | 2 ++
 tests/src/traits.rs            | 1 +
 14 files changed, 37 insertions(+)

(limited to 'tests/src')

diff --git a/tests/src/arrays.rs b/tests/src/arrays.rs
index 1f094541..ddad2ad3 100644
--- a/tests/src/arrays.rs
+++ b/tests/src/arrays.rs
@@ -1,3 +1,6 @@
+//@ [coq] aeneas-args=-use-fuel
+//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
+//@ [fstar] aeneas-args=-split-files
 //! Exercise the translation of arrays, with features supported by Eurydice
 
 pub enum AB {
diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs
index 9f48cb04..15962047 100644
--- a/tests/src/bitwise.rs
+++ b/tests/src/bitwise.rs
@@ -1,3 +1,4 @@
+//@ aeneas-args=-test-trans-units
 //! Exercise the bitwise operations
 
 pub fn shift_u32(a: u32) -> u32 {
diff --git a/tests/src/constants.rs b/tests/src/constants.rs
index 83904eed..925c62b1 100644
--- a/tests/src/constants.rs
+++ b/tests/src/constants.rs
@@ -1,3 +1,5 @@
+//@ charon-args=--no-code-duplication
+//@ aeneas-args=-test-trans-units
 //! Tests with constants
 
 // Integers
diff --git a/tests/src/demo.rs b/tests/src/demo.rs
index bc74cc8b..b9bb7ca2 100644
--- a/tests/src/demo.rs
+++ b/tests/src/demo.rs
@@ -1,3 +1,4 @@
+//@ [coq,fstar] aeneas-args=-use-fuel
 #![allow(clippy::needless_lifetimes)]
 
 /* Simple functions */
diff --git a/tests/src/external.rs b/tests/src/external.rs
index 521749d6..ddd5539f 100644
--- a/tests/src/external.rs
+++ b/tests/src/external.rs
@@ -1,3 +1,6 @@
+//@ charon-args=--no-code-duplication
+//@ aeneas-args=-state -split-files
+//@ aeneas-args=-test-trans-units
 //! This module uses external types and functions
 
 use std::cell::Cell;
diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs
index 58d22acd..4552e4f2 100644
--- a/tests/src/hashmap.rs
+++ b/tests/src/hashmap.rs
@@ -1,3 +1,11 @@
+//@ [coq] aeneas-args=-use-fuel
+//@ aeneas-args=-split-files
+//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
+//@ [lean] aeneas-args=-no-gen-lib-entry
+// ^ the `-no-gen-lib-entry` is because we add a custom import in the Hashmap.lean file: we do not
+// want to overwrite it.
+// TODO: reactivate -test-trans-units
+
 //! A hashmap implementation.
 //!
 //! Current limitations:
diff --git a/tests/src/hashmap_main.rs b/tests/src/hashmap_main.rs
index 45dfa6e2..0c827844 100644
--- a/tests/src/hashmap_main.rs
+++ b/tests/src/hashmap_main.rs
@@ -1,3 +1,9 @@
+//@ charon-args=--opaque=hashmap_utils
+//@ aeneas-args=-state -split-files
+//@ [coq] aeneas-args=-use-fuel
+//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
+// Possible to add `--no-code-duplication` if we use the optimized MIR
+// TODO: reactivate -test-trans-units
 mod hashmap;
 mod hashmap_utils;
 
diff --git a/tests/src/hashmap_utils.rs b/tests/src/hashmap_utils.rs
index cd7b481f..33de49e1 100644
--- a/tests/src/hashmap_utils.rs
+++ b/tests/src/hashmap_utils.rs
@@ -1,3 +1,4 @@
+//@ skip
 use crate::hashmap::*;
 
 /// Serialize a hash map - we don't have traits, so we fix the type of the
diff --git a/tests/src/loops.rs b/tests/src/loops.rs
index 2f71d75b..8692c60e 100644
--- a/tests/src/loops.rs
+++ b/tests/src/loops.rs
@@ -1,3 +1,6 @@
+//@ [coq] aeneas-args=-use-fuel
+//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
+//@ [fstar] aeneas-args=-split-files
 use std::vec::Vec;
 
 /// No borrows
diff --git a/tests/src/nested_borrows.rs b/tests/src/nested_borrows.rs
index 94db0cec..d4d8cf73 100644
--- a/tests/src/nested_borrows.rs
+++ b/tests/src/nested_borrows.rs
@@ -1,3 +1,5 @@
+//@ skip
+//@ charon-args=--no-code-duplication
 //! This module contains functions with nested borrows in their signatures.
 
 pub fn id_mut_mut<'a, 'b, T>(x: &'a mut &'b mut T) -> &'a mut &'b mut T {
diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs
index 9a7604e6..78163371 100644
--- a/tests/src/no_nested_borrows.rs
+++ b/tests/src/no_nested_borrows.rs
@@ -1,3 +1,5 @@
+//@ charon-args=--no-code-duplication
+//@ aeneas-args=-test-trans-units
 //! This module doesn't contain **functions which use nested borrows in their
 //! signatures**, and doesn't contain functions with loops.
 
diff --git a/tests/src/paper.rs b/tests/src/paper.rs
index 156f13ab..07453098 100644
--- a/tests/src/paper.rs
+++ b/tests/src/paper.rs
@@ -1,3 +1,5 @@
+//@ charon-args=--no-code-duplication
+//@ aeneas-args=-test-trans-units
 //! The examples from the ICFP submission, all in one place.
 
 // 2.1
diff --git a/tests/src/polonius_list.rs b/tests/src/polonius_list.rs
index 8c64110d..a8d51e40 100644
--- a/tests/src/polonius_list.rs
+++ b/tests/src/polonius_list.rs
@@ -1,3 +1,5 @@
+//@ charon-args=--polonius
+//@ aeneas-args=-test-trans-units
 #![allow(dead_code)]
 
 pub enum List<T> {
diff --git a/tests/src/traits.rs b/tests/src/traits.rs
index 27c90586..fd50db8c 100644
--- a/tests/src/traits.rs
+++ b/tests/src/traits.rs
@@ -1,3 +1,4 @@
+//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
 pub trait BoolTrait {
     // Required method
     fn get_bool(&self) -> bool;
-- 
cgit v1.3.1


From 093ebced6d22f6b805147783c978af13a7a03caa Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 16:51:54 +0200
Subject: runner: Specify subdirectory in magic comments

---
 tests/src/bitwise.rs           |  1 +
 tests/src/constants.rs         |  1 +
 tests/src/demo.rs              |  1 +
 tests/src/external.rs          |  1 +
 tests/src/loops.rs             |  1 +
 tests/src/no_nested_borrows.rs |  1 +
 tests/src/paper.rs             |  1 +
 tests/src/polonius_list.rs     |  1 +
 tests/test_runner/run_test.ml  | 31 ++++++++++++++++---------------
 9 files changed, 24 insertions(+), 15 deletions(-)

(limited to 'tests/src')

diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs
index 15962047..fda8eff3 100644
--- a/tests/src/bitwise.rs
+++ b/tests/src/bitwise.rs
@@ -1,4 +1,5 @@
 //@ aeneas-args=-test-trans-units
+//@ [coq,fstar] subdir=misc
 //! Exercise the bitwise operations
 
 pub fn shift_u32(a: u32) -> u32 {
diff --git a/tests/src/constants.rs b/tests/src/constants.rs
index 925c62b1..ac24dcd4 100644
--- a/tests/src/constants.rs
+++ b/tests/src/constants.rs
@@ -1,5 +1,6 @@
 //@ charon-args=--no-code-duplication
 //@ aeneas-args=-test-trans-units
+//@ [coq,fstar] subdir=misc
 //! Tests with constants
 
 // Integers
diff --git a/tests/src/demo.rs b/tests/src/demo.rs
index b9bb7ca2..0a589338 100644
--- a/tests/src/demo.rs
+++ b/tests/src/demo.rs
@@ -1,4 +1,5 @@
 //@ [coq,fstar] aeneas-args=-use-fuel
+//@ [lean] subdir=Demo
 #![allow(clippy::needless_lifetimes)]
 
 /* Simple functions */
diff --git a/tests/src/external.rs b/tests/src/external.rs
index ddd5539f..baea76e4 100644
--- a/tests/src/external.rs
+++ b/tests/src/external.rs
@@ -1,6 +1,7 @@
 //@ charon-args=--no-code-duplication
 //@ aeneas-args=-state -split-files
 //@ aeneas-args=-test-trans-units
+//@ [coq,fstar] subdir=misc
 //! This module uses external types and functions
 
 use std::cell::Cell;
diff --git a/tests/src/loops.rs b/tests/src/loops.rs
index 8692c60e..afc52ace 100644
--- a/tests/src/loops.rs
+++ b/tests/src/loops.rs
@@ -1,6 +1,7 @@
 //@ [coq] aeneas-args=-use-fuel
 //@ [fstar] aeneas-args=-decreases-clauses -template-clauses
 //@ [fstar] aeneas-args=-split-files
+//@ [coq,fstar] subdir=misc
 use std::vec::Vec;
 
 /// No borrows
diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs
index 78163371..a250748c 100644
--- a/tests/src/no_nested_borrows.rs
+++ b/tests/src/no_nested_borrows.rs
@@ -1,5 +1,6 @@
 //@ charon-args=--no-code-duplication
 //@ aeneas-args=-test-trans-units
+//@ [coq,fstar] subdir=misc
 //! This module doesn't contain **functions which use nested borrows in their
 //! signatures**, and doesn't contain functions with loops.
 
diff --git a/tests/src/paper.rs b/tests/src/paper.rs
index 07453098..6a4a7c31 100644
--- a/tests/src/paper.rs
+++ b/tests/src/paper.rs
@@ -1,5 +1,6 @@
 //@ charon-args=--no-code-duplication
 //@ aeneas-args=-test-trans-units
+//@ [coq,fstar] subdir=misc
 //! The examples from the ICFP submission, all in one place.
 
 // 2.1
diff --git a/tests/src/polonius_list.rs b/tests/src/polonius_list.rs
index a8d51e40..b029ad02 100644
--- a/tests/src/polonius_list.rs
+++ b/tests/src/polonius_list.rs
@@ -1,5 +1,6 @@
 //@ charon-args=--polonius
 //@ aeneas-args=-test-trans-units
+//@ [coq,fstar] subdir=misc
 #![allow(dead_code)]
 
 pub enum List<T> {
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 39330a77..8f356365 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -104,21 +104,16 @@ let charon_options_for_test test_name =
       [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ]
   | _ -> []
 
-(* The subdirectory in which to store the outputs. *)
+(* The default 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 =
-  let backend = Backend.to_string backend in
   match (backend, test_name) with
-  | "lean", "demo" -> "Demo"
-  | "lean", _ -> "."
-  | _, ("arrays" | "demo" | "hashmap" | "traits") -> test_name
-  | _, "betree" -> "betree"
+  | Backend.Lean, _ -> "."
   | _, "hashmap_main" -> "hashmap_on_disk"
-  | "hol4", _ -> "misc-" ^ test_name
-  | ( _,
-      ( "bitwise" | "constants" | "external" | "loops" | "no_nested_borrows"
-      | "paper" | "polonius_list" ) ) ->
-      "misc"
+  | ( Backend.HOL4,
+      ( "constants" | "external" | "loops" | "no_nested_borrows" | "paper"
+      | "polonius_list" ) ) ->
+      "misc-" ^ test_name
   | _ -> test_name
 
 (* The data for a specific test input *)
@@ -133,13 +128,15 @@ module Input = struct
     actions : action BackendMap.t;
     charon_options : string list;
     aeneas_options : string list BackendMap.t;
-    subdir : string BackendMap.t;
+    subdirs : string BackendMap.t;
   }
 
   (* Parse lines that start `//@`. Each of them modifies the options we use for the test.
      Supported comments:
        - `skip`: don't process the file;
        - `known-failure`: TODO;
+       - `subdir=...: set the subdirectory in which to store the outputs.
+            Defaults to nothing for lean and to the test name for other backends;
        - `charon-args=...`: extra arguments to pass to charon;
        - `aeneas-args=...`: extra arguments to pass to aeneas;
        - `[backend,..]...`: where each `backend` is the name of a backend supported by
@@ -162,6 +159,7 @@ module Input = struct
     (* Parse the other options *)
     let charon_args = Core.String.chop_prefix comment ~prefix:"charon-args=" in
     let aeneas_args = Core.String.chop_prefix comment ~prefix:"aeneas-args=" in
+    let subdir = Core.String.chop_prefix comment ~prefix:"subdir=" in
 
     if comment = "skip" then
       { input with actions = BackendMap.add_each backends Skip input.actions }
@@ -185,6 +183,9 @@ module Input = struct
         aeneas_options =
           BackendMap.update_each backends add_args input.aeneas_options;
       }
+    else if Option.is_some subdir then
+      let subdir = Option.get subdir in
+      { input with subdirs = BackendMap.add_each backends subdir input.subdirs }
     else failwith ("Unrecognized special comment: `" ^ comment ^ "`")
 
   (* Given a path to a rust file or crate, gather the details and options about how to build the test. *)
@@ -198,12 +199,12 @@ module Input = struct
     in
     let actions = BackendMap.make (fun _ -> Normal) in
     let charon_options = charon_options_for_test name in
-    let subdir = BackendMap.make (fun backend -> test_subdir backend name) in
+    let subdirs = BackendMap.make (fun backend -> test_subdir backend name) in
     let aeneas_options =
       BackendMap.make (fun backend -> aeneas_options_for_test backend name)
     in
     let input =
-      { path; name; kind; actions; charon_options; subdir; aeneas_options }
+      { path; name; kind; actions; charon_options; subdirs; aeneas_options }
     in
     match kind with
     | SingleFile ->
@@ -226,7 +227,7 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
   (* FIXME: remove this special case *)
   let test_name = if case.name = "betree" then "betree_main" else case.name in
   let input_file = concat_path [ env.llbc_dir; test_name ] ^ ".llbc" in
-  let subdir = BackendMap.find backend case.subdir in
+  let subdir = BackendMap.find backend case.subdirs in
   let aeneas_options = BackendMap.find backend case.aeneas_options in
   let backend_str = Backend.to_string backend in
   let dest_dir = concat_path [ "tests"; backend_str; subdir ] in
-- 
cgit v1.3.1