summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2024-05-24 16:51:54 +0200
committerNadrieril2024-05-24 17:03:28 +0200
commit093ebced6d22f6b805147783c978af13a7a03caa (patch)
tree5b50ecfd2b2c3d1ded494285249c0670df4d60f9
parentc1892d14fc9ec728422f05dbb9de13ee92984734 (diff)
runner: Specify subdirectory in magic comments
-rw-r--r--tests/src/bitwise.rs1
-rw-r--r--tests/src/constants.rs1
-rw-r--r--tests/src/demo.rs1
-rw-r--r--tests/src/external.rs1
-rw-r--r--tests/src/loops.rs1
-rw-r--r--tests/src/no_nested_borrows.rs1
-rw-r--r--tests/src/paper.rs1
-rw-r--r--tests/src/polonius_list.rs1
-rw-r--r--tests/test_runner/run_test.ml31
9 files changed, 24 insertions, 15 deletions
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