summaryrefslogtreecommitdiff
path: root/tests/test_runner
diff options
context:
space:
mode:
Diffstat (limited to '')
-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/dune11
-rw-r--r--tests/test_runner/run_test.ml289
5 files changed, 312 insertions, 177 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 7caf661f..52688d14 100644
--- a/tests/test_runner/dune
+++ b/tests/test_runner/dune
@@ -1,4 +1,11 @@
(executable
(public_name test_runner)
- (libraries core_unix.sys_unix unix)
- (name run_test))
+ (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)
+ (modules Backend Input Utils run_test))
+
+(env
+ (dev
+ (flags :standard -warn-error -5@8-11-14-32-33-20-21-26-27-39)))
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 8aa6347c..c17c17be 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -3,64 +3,104 @@ type runner_env = {
charon_path : string;
aeneas_path : 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;
-}
-
-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;
+ dest_dir : string;
}
let concat_path = List.fold_left Filename.concat ""
-let run_command args =
- (* Debug arguments *)
- print_string "[test_runner] Running: ";
- Array.iter
- (fun x ->
- print_string x;
- print_string " ")
- args;
- print_endline "";
-
- (* Run the command *)
- let pid =
- Unix.create_process args.(0) args Unix.stdin Unix.stdout Unix.stderr
- in
- let _ = Unix.waitpid [] pid in
- ()
+module Command = struct
+ type t = { args : string array; redirect_out : Unix.file_descr option }
+ type status = Success | Failure
+
+ let make (args : string list) : t =
+ { args = Array.of_list args; redirect_out = None }
+
+ let to_string (cmd : t) = Core.String.concat_array ~sep:" " cmd.args
+
+ (* Run the command and returns its exit status. *)
+ let run (cmd : t) : status =
+ let command_str = to_string cmd in
+ print_endline ("[test_runner] Running: " ^ command_str);
+
+ (* Run the command *)
+ let out = Option.value cmd.redirect_out ~default:Unix.stdout in
+ let pid = Unix.create_process cmd.args.(0) cmd.args Unix.stdin out out in
+ let status = Core_unix.waitpid (Core.Pid.of_int pid) in
+ match status with
+ | Ok () -> Success
+ | Error (`Exit_non_zero _) -> Failure
+ | Error (`Signal _) ->
+ failwith ("Command `" ^ command_str ^ "` exited incorrectly.")
+
+ (* Run the command and aborts the program if the command failed. *)
+ let run_command_expecting_success cmd =
+ match run cmd with
+ | Success -> ()
+ | Failure -> failwith ("Command `" ^ to_string cmd ^ "` failed.")
+
+ (* Run the command and aborts the program if the command succeeded. *)
+ let run_command_expecting_failure cmd =
+ match run cmd with
+ | Success ->
+ failwith
+ ("Command `" ^ to_string cmd ^ "` succeeded but was expected to fail.")
+ | Failure -> ()
+end
(* Run Aeneas on a specific input with the given options *)
-let run_aeneas (env : runner_env) (case : aeneas_test_case) =
+let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
+ let backend_str = Backend.to_string backend 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 output_file =
+ Filename.remove_extension case.path ^ "." ^ backend_str ^ ".out"
+ 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
+
+ (* Build the command *)
let args =
- [|
- env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; case.backend;
- |]
+ [ env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend_str ]
+ in
+ let abort_on_error =
+ match action with
+ | Skip | Normal -> []
+ | KnownFailure -> [ "-abort-on-error" ]
in
- let args = Array.append args (Array.of_list case.extra_aeneas_options) in
+ let args = List.concat [ args; aeneas_options; abort_on_error ] in
+ let cmd = Command.make args in
+ (* Remove leftover files if they're not needed anymore *)
+ if
+ Sys.file_exists output_file
+ &&
+ match action with
+ | Skip | Normal -> true
+ | KnownFailure when not check_output -> true
+ | _ -> false
+ then Sys.remove output_file;
(* Run Aeneas *)
- run_command args
+ match action with
+ | Skip -> ()
+ | Normal -> Command.run_command_expecting_success cmd
+ | KnownFailure ->
+ let out =
+ if check_output then
+ Core_unix.openfile ~mode:[ O_CREAT; O_TRUNC; O_WRONLY ] output_file
+ else Core_unix.openfile ~mode:[ O_WRONLY ] "/dev/null"
+ in
+ let cmd = { cmd with redirect_out = Some out } in
+ Command.run_command_expecting_failure cmd;
+ Unix.close out
(* Run Charon on a specific input with the given options *)
-let run_charon (env : runner_env) (case : charon_test_case) =
+let run_charon (env : runner_env) (case : Input.t) =
match case.kind with
| SingleFile ->
let args =
- [|
+ [
env.charon_path;
"--no-cargo";
"--input";
@@ -69,22 +109,22 @@ let run_charon (env : runner_env) (case : charon_test_case) =
case.name;
"--dest";
env.llbc_dir;
- |]
+ ]
in
- let args = Array.append args (Array.of_list case.extra_charon_options) in
+ let args = List.append args case.charon_options in
(* Run Charon on the rust file *)
- run_command args
+ Command.run_command_expecting_success (Command.make 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)
+ [ env.charon_path; "--dest"; Filename_unix.realpath env.llbc_dir ]
in
+ let args = List.append args case.charon_options in
(* Run Charon inside the crate *)
let old_pwd = Unix.getcwd () in
Unix.chdir case.path;
- run_command args;
+ Command.run_command_expecting_success (Command.make args);
Unix.chdir old_pwd
| Some _ ->
(* Crates with dependencies must be generated separately in CI. We skip
@@ -94,140 +134,39 @@ let run_charon (env : runner_env) (case : charon_test_case) =
"Warn: IN_CI is set; we skip generating llbc files for whole crates"
)
-(* File-specific options *)
-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
- | ( "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" | "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
- | _, "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
-
-(* 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 =
- match test_name with
- | "betree" ->
- [ "--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 =
- match (backend, test_name) with
- | "lean", "demo" -> "Demo"
- | "lean", _ -> "."
- | _, ("arrays" | "demo" | "hashmap" | "traits") -> test_name
- | _, "betree_main" -> "betree"
- | _, "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 :: 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.")
+ let runner_env =
+ { charon_path; aeneas_path; llbc_dir; dest_dir = "tests" }
in
- let extra_charon_options = charon_options_for_test test_name in
- let charon_case =
+ let test_case = Input.build test_path in
+ let test_case =
{
- path = test_path;
- name = test_name;
- kind = charon_kind;
- extra_charon_options;
+ test_case with
+ 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
- (* 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
+ let skip_all =
+ List.for_all
+ (fun backend ->
+ (Backend.Map.find backend test_case.per_backend).action = Input.Skip)
+ Backend.all
in
- (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
- let backends = [ "coq"; "lean"; "fstar" ] in
- List.iter
- (fun backend ->
- let subdir = test_subdir backend test_name in
- let extra_aeneas_options =
- List.append
- (aeneas_options_for_test backend test_name)
- aeneas_options
- in
- let aeneas_case =
- { name = test_name; backend; subdir; extra_aeneas_options }
- in
- (* Process the llbc file for the current backend *)
- run_aeneas runner_env aeneas_case)
- backends
+ 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 (run_aeneas runner_env test_case) Backend.all)
| _ -> failwith "Incorrect options passed to test runner"
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 15:51:55 +0000