summaryrefslogtreecommitdiff
path: root/tests/test_runner
diff options
context:
space:
mode:
Diffstat (limited to 'tests/test_runner')
-rw-r--r--tests/test_runner/Backend.ml47
-rw-r--r--tests/test_runner/Input.ml130
-rw-r--r--tests/test_runner/Utils.ml12
-rw-r--r--tests/test_runner/dune3
-rw-r--r--tests/test_runner/run_test.ml208
5 files changed, 206 insertions, 194 deletions
diff --git a/tests/test_runner/Backend.ml b/tests/test_runner/Backend.ml
new file mode 100644
index 00000000..d21a46fc
--- /dev/null
+++ b/tests/test_runner/Backend.ml
@@ -0,0 +1,47 @@
+(*** Define the backends we support as an enum *)
+
+type t = Coq | Lean | FStar | HOL4 [@@deriving ord, sexp]
+
+(* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
+let all = [ Coq; Lean; FStar ]
+
+let of_string = function
+ | "coq" -> Coq
+ | "lean" -> Lean
+ | "fstar" -> FStar
+ | "hol4" -> HOL4
+ | backend -> failwith ("Unknown backend: `" ^ backend ^ "`")
+
+let to_string = function
+ | Coq -> "coq"
+ | Lean -> "lean"
+ | FStar -> "fstar"
+ | HOL4 -> "hol4"
+
+module Map = struct
+ (* Hack to be able to include things from the parent module with the same names *)
+ type backend_t = t
+
+ let backend_compare = compare
+
+ include Map.Make (struct
+ type t = backend_t
+
+ let compare = backend_compare
+ end)
+
+ (* 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 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
diff --git a/tests/test_runner/Input.ml b/tests/test_runner/Input.ml
new file mode 100644
index 00000000..960ffe8d
--- /dev/null
+++ b/tests/test_runner/Input.ml
@@ -0,0 +1,130 @@
+(*** The data for a specific test input *)
+
+type kind = SingleFile | Crate
+type action = Normal | Skip | KnownFailure
+
+(* Options that can be set for a specific backend *)
+type per_backend = {
+ action : action;
+ aeneas_options : string list;
+ subdir : string;
+ (* Whether to store the command output to a file. Only available for known-failure tests. *)
+ check_output : bool;
+}
+
+(* The data for a specific test input *)
+type t = {
+ name : string;
+ path : string;
+ kind : kind;
+ charon_options : string list;
+ per_backend : per_backend Backend.Map.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.
+*)
+let apply_special_comment comment input =
+ let comment = String.trim comment in
+ (* Parse the backends if any *)
+ let re = Re.compile (Re.Pcre.re "^\\[([a-zA-Z,]+)\\](.*)$") in
+ let comment, (backends : Backend.t list) =
+ match Re.exec_opt re comment with
+ | Some groups ->
+ let backends = Re.Group.get groups 1 in
+ let backends = String.split_on_char ',' backends in
+ let backends = List.map Backend.of_string backends in
+ let rest = Re.Group.get groups 2 in
+ (String.trim rest, backends)
+ | None -> (comment, Backend.all)
+ in
+ (* Apply `f` to the selected backends *)
+ let per_backend f =
+ {
+ input with
+ per_backend = Backend.Map.update_each backends f input.per_backend;
+ }
+ in
+ (* Assert that this option is not available to be set per-backend *)
+ let assert_no_backend option_name =
+ if backends != Backend.all then
+ failwith ("Cannot set the `" ^ option_name ^ "` option per-backend")
+ in
+
+ (* 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 per_backend (fun x -> { x with action = Skip })
+ else if comment = "known-failure" then
+ per_backend (fun x -> { x with action = KnownFailure })
+ else if comment = "no-check-output" then
+ per_backend (fun x -> { x with check_output = false })
+ else if Option.is_some charon_args then (
+ let args = Option.get charon_args in
+ let args = String.split_on_char ' ' args in
+ assert_no_backend "charon-args";
+ { 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
+ per_backend (fun x ->
+ { x with aeneas_options = List.append x.aeneas_options args })
+ else if Option.is_some subdir then
+ let subdir = Option.get subdir in
+ per_backend (fun x -> { x with subdir })
+ 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 per_backend =
+ Backend.Map.make (fun backend ->
+ {
+ action = Normal;
+ subdir = default_subdir backend name;
+ aeneas_options = [];
+ check_output = true;
+ })
+ in
+ let input = { path; name; kind; charon_options = []; per_backend } in
+ (* For crates, we store the special comments in a separate file. *)
+ let crate_config_file = Filename.concat path "aeneas-test-options" in
+ match kind with
+ | SingleFile ->
+ let file_lines = Core.In_channel.read_lines path in
+ (* Extract the special lines. Stop at the first non-special line. *)
+ let special_comments =
+ Utils.map_while
+ (fun line -> Core.String.chop_prefix line ~prefix:"//@")
+ file_lines
+ in
+ (* Apply the changes from the special lines to our input. *)
+ List.fold_left
+ (fun input comment -> apply_special_comment comment input)
+ input special_comments
+ | Crate when Sys.file_exists crate_config_file ->
+ let special_comments = Core.In_channel.read_lines crate_config_file in
+ List.fold_left
+ (fun input comment -> apply_special_comment comment input)
+ input special_comments
+ | Crate -> input
diff --git a/tests/test_runner/Utils.ml b/tests/test_runner/Utils.ml
new file mode 100644
index 00000000..79be617c
--- /dev/null
+++ b/tests/test_runner/Utils.ml
@@ -0,0 +1,12 @@
+(*** Convenience functions *)
+
+let map_while (f : 'a -> 'b option) (input : 'a list) : 'b list =
+ let _, result =
+ List.fold_left
+ (fun (continue, out) a ->
+ if continue then
+ match f a with None -> (false, out) | Some b -> (true, b :: out)
+ else (continue, out))
+ (true, []) input
+ in
+ List.rev result
diff --git a/tests/test_runner/dune b/tests/test_runner/dune
index 6bb3f7b2..52688d14 100644
--- a/tests/test_runner/dune
+++ b/tests/test_runner/dune
@@ -3,7 +3,8 @@
(libraries core_unix core_unix.filename_unix core_unix.sys_unix re str unix)
(preprocess
(pps ppx_deriving.show ppx_deriving.ord ppx_sexp_conv))
- (name run_test))
+ (name run_test)
+ (modules Backend Input Utils run_test))
(env
(dev
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index c626b4d1..c17c17be 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -1,15 +1,3 @@
-(* Convenience functions *)
-let map_while (f : 'a -> 'b option) (input : 'a list) : 'b list =
- let _, result =
- List.fold_left
- (fun (continue, out) a ->
- if continue then
- match f a with None -> (false, out) | Some b -> (true, b :: out)
- else (continue, out))
- (true, []) input
- in
- List.rev result
-
(* Paths to use for tests *)
type runner_env = {
charon_path : string;
@@ -18,47 +6,6 @@ type runner_env = {
dest_dir : string;
}
-module Backend = struct
- type t = Coq | Lean | FStar | HOL4 [@@deriving ord, sexp]
-
- (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
- let all = [ Coq; Lean; FStar ]
-
- let of_string = function
- | "coq" -> Coq
- | "lean" -> Lean
- | "fstar" -> FStar
- | "hol4" -> HOL4
- | backend -> failwith ("Unknown backend: `" ^ backend ^ "`")
-
- let to_string = function
- | Coq -> "coq"
- | Lean -> "lean"
- | FStar -> "fstar"
- | HOL4 -> "hol4"
-end
-
-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 ""
module Command = struct
@@ -100,139 +47,6 @@ module Command = struct
| Failure -> ()
end
-(* The data for a specific test input *)
-module Input = struct
- type kind = SingleFile | Crate
- type action = Normal | Skip | KnownFailure
-
- type t = {
- name : string;
- path : string;
- kind : kind;
- actions : action BackendMap.t;
- charon_options : string list;
- aeneas_options : string list BackendMap.t;
- subdirs : string BackendMap.t;
- (* Whether to store the command output to a file. Only available for known-failure tests. *)
- check_output : bool 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.
- *)
- let apply_special_comment comment input =
- let comment = String.trim comment in
- (* Parse the backends if any *)
- let re = Re.compile (Re.Pcre.re "^\\[([a-zA-Z,]+)\\](.*)$") in
- let comment, (backends : Backend.t list) =
- match Re.exec_opt re comment with
- | Some groups ->
- let backends = Re.Group.get groups 1 in
- let backends = String.split_on_char ',' backends in
- let backends = List.map Backend.of_string backends in
- let rest = Re.Group.get groups 2 in
- (String.trim rest, backends)
- | None -> (comment, Backend.all)
- in
- (* 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 }
- else if comment = "known-failure" then
- {
- input with
- actions = BackendMap.add_each backends KnownFailure input.actions;
- }
- else if comment = "no-check-output" then
- {
- input with
- check_output = BackendMap.add_each backends false input.check_output;
- }
- else if Option.is_some charon_args then
- let args = Option.get charon_args in
- let args = String.split_on_char ' ' args in
- 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
- let add_args opts = List.append opts args in
- {
- input with
- 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. *)
- 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 actions = BackendMap.make (fun _ -> Normal) in
- let subdirs =
- BackendMap.make (fun backend -> default_subdir backend name)
- in
- let aeneas_options = BackendMap.make (fun _ -> []) in
- let check_output = BackendMap.make (fun _ -> true) in
- let input =
- {
- path;
- name;
- kind;
- actions;
- charon_options = [];
- subdirs;
- aeneas_options;
- check_output;
- }
- in
- (* For crates, we store the special comments in a separate file. *)
- let crate_config_file = Filename.concat path "aeneas-test-options" in
- match kind with
- | SingleFile ->
- let file_lines = Core.In_channel.read_lines path in
- (* Extract the special lines. Stop at the first non-special line. *)
- let special_comments =
- map_while
- (fun line -> Core.String.chop_prefix line ~prefix:"//@")
- file_lines
- in
- (* Apply the changes from the special lines to our input. *)
- List.fold_left
- (fun input comment -> apply_special_comment comment input)
- input special_comments
- | Crate when Sys.file_exists crate_config_file ->
- let special_comments = Core.In_channel.read_lines crate_config_file in
- List.fold_left
- (fun input comment -> apply_special_comment comment input)
- input special_comments
- | Crate -> input
-end
-
(* Run Aeneas on a specific input with the given options *)
let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
let backend_str = Backend.to_string backend in
@@ -240,11 +54,12 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
let output_file =
Filename.remove_extension case.path ^ "." ^ backend_str ^ ".out"
in
- let subdir = BackendMap.find backend case.subdirs in
+ let per_backend = Backend.Map.find backend case.per_backend in
+ let subdir = per_backend.subdir in
+ let check_output = per_backend.check_output in
+ let aeneas_options = per_backend.aeneas_options in
+ let action = per_backend.action in
let dest_dir = concat_path [ env.dest_dir; backend_str; subdir ] in
- let aeneas_options = BackendMap.find backend case.aeneas_options in
- let action = BackendMap.find backend case.actions in
- let check_output = BackendMap.find backend case.check_output in
(* Build the command *)
let args =
@@ -331,14 +146,21 @@ let () =
let test_case =
{
test_case with
- aeneas_options =
- BackendMap.map (List.append aeneas_options) test_case.aeneas_options;
+ per_backend =
+ Backend.Map.map
+ (fun x ->
+ {
+ x with
+ Input.aeneas_options =
+ List.append aeneas_options x.Input.aeneas_options;
+ })
+ test_case.per_backend;
}
in
let skip_all =
List.for_all
(fun backend ->
- BackendMap.find backend test_case.actions = Input.Skip)
+ (Backend.Map.find backend test_case.per_backend).action = Input.Skip)
Backend.all
in
if skip_all then ()
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-20 07:45:13 +0000