From b669f7c1228efb362cbb56b95090b24c0611ba7b Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 May 2024 12:01:31 +0200 Subject: tests: Add a README --- tests/README.md | 67 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 67 insertions(+) create mode 100644 tests/README.md (limited to 'tests') diff --git a/tests/README.md b/tests/README.md new file mode 100644 index 00000000..4f4f1ff5 --- /dev/null +++ b/tests/README.md @@ -0,0 +1,67 @@ +# Aeneas test suite + +This folder contains the test suite for Aeneas. It is organized as follows: +- `test_runner/`: ocaml script that orchestrates the test suite; +- `src/`: rust files and crates used as test inputs; +- `llbc/`: temporary directory (ignored by git) that stores intermediate files generated during tests; +- `coq/`, `fstar/`, `hol4/`, `lean/`: one folder per backend. Each folder contains: + - Files generated by Aeneas from our test inputs; + - Handwritten proof files. + +# Running the test suite + +Running the test suite has two parts: +- The generation of files from rust to each backend. This is done by running `make test` in the + project root. This will call the test runner on each file or crate in `tests/src`, which will call + `charon` and `aeneas` to generate the backend-specific outputs. +- The verification of proofs for each backend. This is done by running `make verify` in the project + root. It will run each verifier (`fstar`, `lean` etc) on the files in the corresponding folder to + verify the correctness of proofs. + +CI does both of these things; in particular it checks that we correctly committed the generated +files. + +Important note: at the moment we don't regenerate the `hol4` outputs. We do still check them with +hol4. This is tracked in https://github.com/AeneasVerif/aeneas/issues/62. + +# Adding a new test + +Adding a new test is easy: just add a `foo.rs` file or a `foo_crate` folder in `tests/src`. `make +test` will find the new file and call the test runner on it. + +To specify options for how your test should be run, see the next section. + +Ideally, any non-trivial change to Aeneas should have an accompanying test that exercises the new +code. The goal of this test suite is to cover a large portion of what Aeneas can do, so we can work +on it confidently. + +# Passing options to `Aeneas` and `Charon` + +The test runner supports setting several options for each test. +- For single files, it will read comments at the top of the file that start with `//@`; +- For crates, it will read the `crate_dir/aeneas-test-options` file. + +In both cases it supports the same options. Typical options are: +- `charon-args=--polonius --opaque=betree_utils`: pass these arguments to `charon`; +- `aeneas-args=-test-trans-units`: pass these arguments to `aeneas` for all backends; +- `[fstar] aeneas-args=-decreases-clauses -template-clauses`: pass these arguments to `aeneas` for + the `fstar` backend; +- `[coq,lean] skip`: skip the test for the `coq` and `lean` backends; +- `[fstar] known-failure`: see below; +- `[coq,fstar] subdir=misc`: store the output in the `misc` subdirectory for these two backends. + +For an up-to-date list of options, see comments in the test runner code. + +# `known-failure` tests + +There's a special kind of test that doesn't generate backend code: `//@ known-failure` tests. These +are meant to record: +- Cases that produce an error so we don't forget and can fix them later; +- Cases that _should_ error, to ensure we correctly raise an error and that the error output is nice. + +It is useful to add tests there whenever you find an interesting failure case. + +Note however that this is for failures of Aeneas. Tests that cause Charon errors should be submitted +to the Charon project. `known-failure` tests will not pass if the error occurs within Charon. Note +also that there is no option for tests that translate successfully but fail to be verified by the +backend. -- cgit v1.2.3 From 86d0789b5a303f43c0d9bfeff83f37d89750b5d6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 May 2024 12:14:08 +0200 Subject: runner: make the backend map a submodule of `Backend` --- tests/test_runner/run_test.ml | 84 ++++++++++++++++++++++++------------------- 1 file changed, 48 insertions(+), 36 deletions(-) (limited to 'tests') diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index c626b4d1..5314752c 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -36,27 +36,34 @@ module Backend = struct | Lean -> "lean" | FStar -> "fstar" | HOL4 -> "hol4" -end -module BackendMap = struct - include Map.Make (Backend) + module Map = struct + (* Hack to be able to include things from the parent module with the same names *) + type backend_t = t - (* 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 + let backend_compare = compare - (* 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 + include Map.Make (struct + type t = backend_t - (* 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 + 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 end let concat_path = List.fold_left Filename.concat "" @@ -109,12 +116,12 @@ module Input = struct name : string; path : string; kind : kind; - actions : action BackendMap.t; + actions : action Backend.Map.t; charon_options : string list; - aeneas_options : string list BackendMap.t; - subdirs : string BackendMap.t; + aeneas_options : string list Backend.Map.t; + subdirs : string Backend.Map.t; (* Whether to store the command output to a file. Only available for known-failure tests. *) - check_output : bool BackendMap.t; + check_output : bool Backend.Map.t; } (* The default subdirectory in which to store the outputs. *) @@ -152,16 +159,16 @@ module Input = struct let subdir = Core.String.chop_prefix comment ~prefix:"subdir=" in if comment = "skip" then - { input with actions = BackendMap.add_each backends Skip input.actions } + { input with actions = Backend.Map.add_each backends Skip input.actions } else if comment = "known-failure" then { input with - actions = BackendMap.add_each backends KnownFailure input.actions; + actions = Backend.Map.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; + check_output = Backend.Map.add_each backends false input.check_output; } else if Option.is_some charon_args then let args = Option.get charon_args in @@ -176,11 +183,14 @@ module Input = struct { input with aeneas_options = - BackendMap.update_each backends add_args input.aeneas_options; + Backend.Map.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 } + { + input with + subdirs = Backend.Map.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. *) @@ -192,12 +202,12 @@ module Input = struct 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 actions = Backend.Map.make (fun _ -> Normal) in let subdirs = - BackendMap.make (fun backend -> default_subdir backend name) + Backend.Map.make (fun backend -> default_subdir backend name) in - let aeneas_options = BackendMap.make (fun _ -> []) in - let check_output = BackendMap.make (fun _ -> true) in + let aeneas_options = Backend.Map.make (fun _ -> []) in + let check_output = Backend.Map.make (fun _ -> true) in let input = { path; @@ -240,11 +250,11 @@ 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 subdir = Backend.Map.find backend case.subdirs 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 + let aeneas_options = Backend.Map.find backend case.aeneas_options in + let action = Backend.Map.find backend case.actions in + let check_output = Backend.Map.find backend case.check_output in (* Build the command *) let args = @@ -332,13 +342,15 @@ let () = { test_case with aeneas_options = - BackendMap.map (List.append aeneas_options) test_case.aeneas_options; + Backend.Map.map + (List.append aeneas_options) + test_case.aeneas_options; } in let skip_all = List.for_all (fun backend -> - BackendMap.find backend test_case.actions = Input.Skip) + Backend.Map.find backend test_case.actions = Input.Skip) Backend.all in if skip_all then () -- cgit v1.2.3 From ec03335a473ffdf9371210e8558c691ea69d212d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 May 2024 12:18:52 +0200 Subject: runner: Split up into multiple files --- tests/README.md | 2 +- tests/test_runner/Backend.ml | 47 ++++++++++ tests/test_runner/Input.ml | 129 +++++++++++++++++++++++++++ tests/test_runner/Utils.ml | 12 +++ tests/test_runner/dune | 3 +- tests/test_runner/run_test.ml | 196 ------------------------------------------ 6 files changed, 191 insertions(+), 198 deletions(-) create mode 100644 tests/test_runner/Backend.ml create mode 100644 tests/test_runner/Input.ml create mode 100644 tests/test_runner/Utils.ml (limited to 'tests') diff --git a/tests/README.md b/tests/README.md index 4f4f1ff5..f68b509f 100644 --- a/tests/README.md +++ b/tests/README.md @@ -50,7 +50,7 @@ In both cases it supports the same options. Typical options are: - `[fstar] known-failure`: see below; - `[coq,fstar] subdir=misc`: store the output in the `misc` subdirectory for these two backends. -For an up-to-date list of options, see comments in the test runner code. +For an up-to-date list of options, see comments in `tests/test_runner/Input.ml`. # `known-failure` tests 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..dbb69a47 --- /dev/null +++ b/tests/test_runner/Input.ml @@ -0,0 +1,129 @@ +(*** The data for a specific test input *) + +type kind = SingleFile | Crate +type action = Normal | Skip | KnownFailure + +type t = { + name : string; + path : string; + kind : kind; + actions : action Backend.Map.t; + charon_options : string list; + aeneas_options : string list Backend.Map.t; + subdirs : string Backend.Map.t; + (* Whether to store the command output to a file. Only available for known-failure tests. *) + check_output : bool 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 + (* 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 = Backend.Map.add_each backends Skip input.actions } + else if comment = "known-failure" then + { + input with + actions = Backend.Map.add_each backends KnownFailure input.actions; + } + else if comment = "no-check-output" then + { + input with + check_output = Backend.Map.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 = + Backend.Map.update_each backends add_args input.aeneas_options; + } + else if Option.is_some subdir then + let subdir = Option.get subdir in + { input with subdirs = Backend.Map.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 = Backend.Map.make (fun _ -> Normal) in + let subdirs = Backend.Map.make (fun backend -> default_subdir backend name) in + let aeneas_options = Backend.Map.make (fun _ -> []) in + let check_output = Backend.Map.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 = + 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 5314752c..e8dd38bb 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,54 +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" - - 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 -end - let concat_path = List.fold_left Filename.concat "" module Command = struct @@ -107,142 +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 Backend.Map.t; - charon_options : string list; - aeneas_options : string list Backend.Map.t; - subdirs : string Backend.Map.t; - (* Whether to store the command output to a file. Only available for known-failure tests. *) - check_output : bool 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 - (* 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 = Backend.Map.add_each backends Skip input.actions } - else if comment = "known-failure" then - { - input with - actions = Backend.Map.add_each backends KnownFailure input.actions; - } - else if comment = "no-check-output" then - { - input with - check_output = Backend.Map.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 = - Backend.Map.update_each backends add_args input.aeneas_options; - } - else if Option.is_some subdir then - let subdir = Option.get subdir in - { - input with - subdirs = Backend.Map.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 = Backend.Map.make (fun _ -> Normal) in - let subdirs = - Backend.Map.make (fun backend -> default_subdir backend name) - in - let aeneas_options = Backend.Map.make (fun _ -> []) in - let check_output = Backend.Map.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 -- cgit v1.2.3 From 14d9ca2ddf5ccb350d3bd87ca14a7b7468398e9c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 May 2024 13:52:12 +0200 Subject: runner: Factor out backend-specific options --- tests/test_runner/Input.ml | 83 ++++++++++++++++++++++--------------------- tests/test_runner/run_test.ml | 22 +++++++----- 2 files changed, 56 insertions(+), 49 deletions(-) (limited to 'tests') diff --git a/tests/test_runner/Input.ml b/tests/test_runner/Input.ml index dbb69a47..960ffe8d 100644 --- a/tests/test_runner/Input.ml +++ b/tests/test_runner/Input.ml @@ -3,16 +3,22 @@ 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; - actions : action Backend.Map.t; charon_options : string list; - aeneas_options : string list Backend.Map.t; - subdirs : string Backend.Map.t; - (* Whether to store the command output to a file. Only available for known-failure tests. *) - check_output : bool Backend.Map.t; + per_backend : per_backend Backend.Map.t; } (* The default subdirectory in which to store the outputs. *) @@ -44,41 +50,42 @@ let apply_special_comment comment input = (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 - { input with actions = Backend.Map.add_each backends Skip input.actions } + if comment = "skip" then per_backend (fun x -> { x with action = Skip }) else if comment = "known-failure" then - { - input with - actions = Backend.Map.add_each backends KnownFailure input.actions; - } + per_backend (fun x -> { x with action = KnownFailure }) else if comment = "no-check-output" then - { - input with - check_output = Backend.Map.add_each backends false input.check_output; - } - else if Option.is_some charon_args 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 - if backends != Backend.all then - failwith "Cannot set per-backend charon-args" - else { input with charon_options = List.append input.charon_options args } + 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 - let add_args opts = List.append opts args in - { - input with - aeneas_options = - Backend.Map.update_each backends add_args input.aeneas_options; - } + 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 - { input with subdirs = Backend.Map.add_each backends subdir input.subdirs } + 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. *) @@ -90,22 +97,16 @@ let build (path : string) : t = else if Sys_unix.is_directory_exn path then Crate else failwith ("`" ^ path ^ "` is not a file or a directory.") in - let actions = Backend.Map.make (fun _ -> Normal) in - let subdirs = Backend.Map.make (fun backend -> default_subdir backend name) in - let aeneas_options = Backend.Map.make (fun _ -> []) in - let check_output = Backend.Map.make (fun _ -> true) in - let input = - { - path; - name; - kind; - actions; - charon_options = []; - subdirs; - aeneas_options; - check_output; - } + 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 diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index e8dd38bb..c17c17be 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -54,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 = Backend.Map.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 = Backend.Map.find backend case.aeneas_options in - let action = Backend.Map.find backend case.actions in - let check_output = Backend.Map.find backend case.check_output in (* Build the command *) let args = @@ -145,16 +146,21 @@ let () = let test_case = { test_case with - aeneas_options = + per_backend = Backend.Map.map - (List.append aeneas_options) - test_case.aeneas_options; + (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 -> - Backend.Map.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 () -- cgit v1.2.3 From 87d5a08f44b46657026a99c154bcec4a733f221d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 May 2024 10:37:17 +0200 Subject: Improve the tests README --- tests/Makefile | 6 +++--- tests/README.md | 30 +++++++++++++++++++----------- 2 files changed, 22 insertions(+), 14 deletions(-) (limited to 'tests') diff --git a/tests/Makefile b/tests/Makefile index ff4baaba..a911e037 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -1,6 +1,6 @@ .PHONY: all -all: test-fstar test-coq test-lean test-hol4 +all: verify-fstar verify-coq verify-lean verify-hol4 -.PHONY: test-% -test-%: +.PHONY: verify-% +verify-%: cd $* && $(MAKE) all diff --git a/tests/README.md b/tests/README.md index f68b509f..c9ca0047 100644 --- a/tests/README.md +++ b/tests/README.md @@ -8,23 +8,26 @@ This folder contains the test suite for Aeneas. It is organized as follows: - Files generated by Aeneas from our test inputs; - Handwritten proof files. -# Running the test suite +## Running the test suite Running the test suite has two parts: -- The generation of files from rust to each backend. This is done by running `make test` in the +- We generate files from rust to each backend. This is done by running `make test` in the project root. This will call the test runner on each file or crate in `tests/src`, which will call `charon` and `aeneas` to generate the backend-specific outputs. -- The verification of proofs for each backend. This is done by running `make verify` in the project - root. It will run each verifier (`fstar`, `lean` etc) on the files in the corresponding folder to - verify the correctness of proofs. +- We check that the generated output is valid code by parsing it and type-checking it with the + relevant verifier (Lean, Coq, F*, etc.), and replay the hand-written proofs which use it as + a dependency. This is done by running `make verify` in the project root. -CI does both of these things; in particular it checks that we correctly committed the generated -files. +To generate the output of a single test, run `make test-`, e.g. `make test-loops.rs` or +`make test-betree`. To verify the output for a single backend, run `make verify-` inside the +`tests/` folder, e.g. `make verify-coq`. -Important note: at the moment we don't regenerate the `hol4` outputs. We do still check them with +CI does both of these things; it also checks that we committed all the generated files. + +Important note: at the moment we don't regenerate the HOL4 outputs. We do still check them with hol4. This is tracked in https://github.com/AeneasVerif/aeneas/issues/62. -# Adding a new test +## Adding a new test Adding a new test is easy: just add a `foo.rs` file or a `foo_crate` folder in `tests/src`. `make test` will find the new file and call the test runner on it. @@ -35,7 +38,7 @@ Ideally, any non-trivial change to Aeneas should have an accompanying test that code. The goal of this test suite is to cover a large portion of what Aeneas can do, so we can work on it confidently. -# Passing options to `Aeneas` and `Charon` +## Passing options to `Aeneas` and `Charon` The test runner supports setting several options for each test. - For single files, it will read comments at the top of the file that start with `//@`; @@ -52,13 +55,18 @@ In both cases it supports the same options. Typical options are: For an up-to-date list of options, see comments in `tests/test_runner/Input.ml`. -# `known-failure` tests +## `known-failure` tests There's a special kind of test that doesn't generate backend code: `//@ known-failure` tests. These are meant to record: - Cases that produce an error so we don't forget and can fix them later; - Cases that _should_ error, to ensure we correctly raise an error and that the error output is nice. +We record the output of the `aeneas` call in `test-file.out` alongside the original `test-file.rs`. +This file must be committed like the rest of the test outputs. (Note: sometimes the output will be +different between your local machine and CI, e.g. because release build changed a stacktrace. In +that case we don't record the output, which is done with `//@ no-check-output`). + It is useful to add tests there whenever you find an interesting failure case. Note however that this is for failures of Aeneas. Tests that cause Charon errors should be submitted -- cgit v1.2.3