summaryrefslogtreecommitdiff
path: root/tests/test_runner
diff options
context:
space:
mode:
authorGuillaume Boisseau2024-05-24 17:10:02 +0200
committerGitHub2024-05-24 17:10:02 +0200
commit4971b7edf4538144df735f9fa5327fe4d0e2e003 (patch)
tree979ed531f66c3b0040fa5714fa70db606ca786c0 /tests/test_runner
parentfbfa0e13ab56ee847e891fa7d798d2eb226b6794 (diff)
parent3adbe18d36df3767e98f30b760ccd9c6ace640ad (diff)
Merge pull request #206 from AeneasVerif/subdir
Diffstat (limited to 'tests/test_runner')
-rw-r--r--tests/test_runner/dune2
-rw-r--r--tests/test_runner/run_test.ml124
2 files changed, 71 insertions, 55 deletions
diff --git a/tests/test_runner/dune b/tests/test_runner/dune
index e8b29d66..1c719532 100644
--- a/tests/test_runner/dune
+++ b/tests/test_runner/dune
@@ -1,6 +1,6 @@
(executable
(public_name test_runner)
- (libraries core_unix.sys_unix re unix)
+ (libraries core_unix.sys_unix re str unix)
(preprocess
(pps ppx_deriving.show ppx_deriving.ord ppx_sexp_conv))
(name run_test))
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 25efbcfd..5d77bf9e 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -37,7 +37,26 @@ module Backend = struct
| HOL4 -> "hol4"
end
-module BackendMap = Map.Make (Backend)
+module BackendMap = struct
+ include Map.Make (Backend)
+
+ (* Make a new map with one entry per backend, given by `f` *)
+ let make (f : Backend.t -> 'a) : 'a t =
+ List.fold_left
+ (fun map backend -> add backend (f backend) map)
+ empty Backend.all
+
+ (* Set this value for all the backends in `backends` *)
+ let add_each (backends : Backend.t list) (v : 'a) (map : 'a t) : 'a t =
+ List.fold_left (fun map backend -> add backend v map) map backends
+
+ (* Updates all the backends in `backends` with `f` *)
+ let update_each (backends : Backend.t list) (f : 'a -> 'a) (map : 'a t) : 'a t
+ =
+ List.fold_left
+ (fun map backend -> update backend (Option.map f) map)
+ map backends
+end
let concat_path = List.fold_left Filename.concat ""
@@ -85,23 +104,6 @@ let charon_options_for_test test_name =
[ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ]
| _ -> []
-(* 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 =
- let backend = Backend.to_string backend in
- match (backend, test_name) with
- | "lean", "demo" -> "Demo"
- | "lean", _ -> "."
- | _, ("arrays" | "demo" | "hashmap" | "traits") -> test_name
- | _, "betree" -> "betree"
- | _, "hashmap_main" -> "hashmap_on_disk"
- | "hol4", _ -> "misc-" ^ test_name
- | ( _,
- ( "bitwise" | "constants" | "external" | "loops" | "no_nested_borrows"
- | "paper" | "polonius_list" ) ) ->
- "misc"
- | _ -> test_name
-
(* The data for a specific test input *)
module Input = struct
type kind = SingleFile | Crate
@@ -111,20 +113,26 @@ module Input = struct
name : string;
path : string;
kind : kind;
- action : action;
+ actions : action BackendMap.t;
charon_options : string list;
aeneas_options : string list BackendMap.t;
- subdir : string BackendMap.t;
+ subdirs : string BackendMap.t;
}
+ (* The default subdirectory in which to store the outputs. *)
+ let default_subdir backend test_name =
+ match backend with Backend.Lean -> "." | _ -> test_name
+
(* 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
- aeneas; this sets options for these backends only. Only supported for `aeneas-args`.
+ aeneas; this sets options for these backends only.
*)
let apply_special_comment comment input =
let comment = String.trim comment in
@@ -143,13 +151,21 @@ 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 action = Skip }
- else if comment = "known-failure" then { input with action = KnownFailure }
+ if comment = "skip" then
+ { input with actions = BackendMap.add_each backends Skip input.actions }
+ else if comment = "known-failure" then
+ {
+ input with
+ actions = BackendMap.add_each backends KnownFailure input.actions;
+ }
else if Option.is_some charon_args then
let args = Option.get charon_args in
let args = String.split_on_char ' ' args in
- { input with charon_options = List.append input.charon_options args }
+ if backends != Backend.all then
+ failwith "Cannot set per-backend charon-args"
+ else { input with charon_options = List.append input.charon_options args }
else if Option.is_some aeneas_args then
let args = Option.get aeneas_args in
let args = String.split_on_char ' ' args in
@@ -157,39 +173,32 @@ module Input = struct
{
input with
aeneas_options =
- List.fold_left
- (fun map backend ->
- BackendMap.update backend (Option.map add_args) map)
- input.aeneas_options backends;
+ 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. *)
let build (path : string) : t =
let name = Filename.remove_extension (Filename.basename path) in
+ let name = Str.global_replace (Str.regexp "-") "_" name in
let kind =
if Sys_unix.is_file_exn path then SingleFile
else if Sys_unix.is_directory_exn path then Crate
else failwith ("`" ^ path ^ "` is not a file or a directory.")
in
- let action = Normal in
+ let actions = BackendMap.make (fun _ -> Normal) in
let charon_options = charon_options_for_test name in
- let subdir =
- List.fold_left
- (fun map backend ->
- let subdir = test_subdir backend name in
- BackendMap.add backend subdir map)
- BackendMap.empty Backend.all
+ let subdirs =
+ BackendMap.make (fun backend -> default_subdir backend name)
in
let aeneas_options =
- List.fold_left
- (fun map backend ->
- let opts = aeneas_options_for_test backend name in
- BackendMap.add backend opts map)
- BackendMap.empty Backend.all
+ BackendMap.make (fun backend -> aeneas_options_for_test backend name)
in
let input =
- { path; name; kind; action; charon_options; subdir; aeneas_options }
+ { path; name; kind; actions; charon_options; subdirs; aeneas_options }
in
match kind with
| SingleFile ->
@@ -212,7 +221,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
@@ -266,7 +275,7 @@ let () =
match Array.to_list Sys.argv with
(* Ad-hoc argument passing for now. *)
| _exe_path :: charon_path :: aeneas_path :: llbc_dir :: test_path
- :: aeneas_options -> (
+ :: aeneas_options ->
let runner_env = { charon_path; aeneas_path; llbc_dir } in
let test_case = Input.build test_path in
let test_case =
@@ -276,15 +285,22 @@ let () =
BackendMap.map (List.append aeneas_options) test_case.aeneas_options;
}
in
-
- match test_case.action with
- | Skip -> ()
- | Normal ->
- (* Generate the llbc file *)
- run_charon runner_env test_case;
- (* Process the llbc file for the each backend *)
- List.iter
- (fun backend -> run_aeneas runner_env test_case backend)
- Backend.all
- | KnownFailure -> failwith "KnownFailure is unimplemented")
+ let skip_all =
+ List.for_all
+ (fun backend ->
+ BackendMap.find backend test_case.actions = Input.Skip)
+ Backend.all
+ in
+ if skip_all then ()
+ else (
+ (* Generate the llbc file *)
+ run_charon runner_env test_case;
+ (* Process the llbc file for the each backend *)
+ List.iter
+ (fun backend ->
+ match BackendMap.find backend test_case.actions with
+ | Skip -> ()
+ | Normal -> run_aeneas runner_env test_case backend
+ | KnownFailure -> failwith "KnownFailure is unimplemented")
+ Backend.all)
| _ -> failwith "Incorrect options passed to test runner"