diff options
author | Son Ho | 2024-06-05 15:03:01 +0200 |
---|---|---|
committer | Son Ho | 2024-06-05 15:03:01 +0200 |
commit | bb1caf9a8efdadd599560b3ff7a12d275a12f696 (patch) | |
tree | e13444dcd87192e62ca3e17362b37a2e92d2825a /tests | |
parent | 49c8e42ec3bcfc323e61c5ba0345abeb41372ac4 (diff) |
Update the test runner to allow the syntax [!lean] and [borrow-check]
Diffstat (limited to '')
-rw-r--r-- | tests/src/betree/aeneas-test-options | 2 | ||||
-rw-r--r-- | tests/src/bitwise.rs | 2 | ||||
-rw-r--r-- | tests/src/constants.rs | 2 | ||||
-rw-r--r-- | tests/src/external.rs | 4 | ||||
-rw-r--r-- | tests/src/hashmap.rs | 2 | ||||
-rw-r--r-- | tests/src/mutually-recursive-traits.lean.out | 14 | ||||
-rw-r--r-- | tests/src/mutually-recursive-traits.rs | 4 | ||||
-rw-r--r-- | tests/src/no_nested_borrows.rs | 2 | ||||
-rw-r--r-- | tests/src/paper.rs | 2 | ||||
-rw-r--r-- | tests/src/polonius_list.rs | 2 | ||||
-rw-r--r-- | tests/src/string-chars.rs | 2 | ||||
-rw-r--r-- | tests/test_runner/Backend.ml | 18 | ||||
-rw-r--r-- | tests/test_runner/Input.ml | 28 | ||||
-rw-r--r-- | tests/test_runner/run_test.ml | 15 |
14 files changed, 65 insertions, 34 deletions
diff --git a/tests/src/betree/aeneas-test-options b/tests/src/betree/aeneas-test-options index c71e01df..5a1e4180 100644 --- a/tests/src/betree/aeneas-test-options +++ b/tests/src/betree/aeneas-test-options @@ -1,4 +1,4 @@ charon-args=--polonius --opaque=betree_utils -aeneas-args=-backward-no-state-update -test-trans-units -state -split-files +[!borrow-check] aeneas-args=-backward-no-state-update -test-trans-units -state -split-files [coq] aeneas-args=-use-fuel [fstar] aeneas-args=-decreases-clauses -template-clauses diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs index fda8eff3..be12cea0 100644 --- a/tests/src/bitwise.rs +++ b/tests/src/bitwise.rs @@ -1,4 +1,4 @@ -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc //! Exercise the bitwise operations diff --git a/tests/src/constants.rs b/tests/src/constants.rs index ac24dcd4..71d7c557 100644 --- a/tests/src/constants.rs +++ b/tests/src/constants.rs @@ -1,5 +1,5 @@ //@ charon-args=--no-code-duplication -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc //! Tests with constants diff --git a/tests/src/external.rs b/tests/src/external.rs index baea76e4..00acdb0b 100644 --- a/tests/src/external.rs +++ b/tests/src/external.rs @@ -1,6 +1,6 @@ //@ charon-args=--no-code-duplication -//@ aeneas-args=-state -split-files -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-state -split-files +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc //! This module uses external types and functions diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs index 19832a84..7dda2404 100644 --- a/tests/src/hashmap.rs +++ b/tests/src/hashmap.rs @@ -1,5 +1,5 @@ //@ charon-args=--opaque=utils -//@ aeneas-args=-state -split-files +//@ [!borrow-check] aeneas-args=-state -split-files //@ [coq] aeneas-args=-use-fuel //@ [fstar] aeneas-args=-decreases-clauses -template-clauses //@ [lean] aeneas-args=-no-gen-lib-entry diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out index 6d638644..e2ed3abc 100644 --- a/tests/src/mutually-recursive-traits.lean.out +++ b/tests/src/mutually-recursive-traits.lean.out @@ -1,17 +1,17 @@ [[92mInfo[39m ] Imported: tests/llbc/mutually_recursive_traits.llbc -[[91mError[39m] In file Translate.ml, line 812: +[[91mError[39m] In file Translate.ml, line 813: Mutually recursive trait declarations are not supported Uncaught exception: (Failure - "In file Translate.ml, line 812:\ - \nIn file Translate.ml, line 812:\ + "In file Translate.ml, line 813:\ + \nIn file Translate.ml, line 813:\ \nMutually recursive trait declarations are not supported") Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 -Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 835, characters 2-52 -Called from Aeneas__Translate.extract_file in file "Translate.ml", line 953, characters 2-36 -Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1501, characters 5-42 -Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61 +Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 836, characters 2-52 +Called from Aeneas__Translate.extract_file in file "Translate.ml", line 954, characters 2-36 +Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1503, characters 5-42 +Called from Dune__exe__Main in file "Main.ml", line 314, characters 14-66 diff --git a/tests/src/mutually-recursive-traits.rs b/tests/src/mutually-recursive-traits.rs index 351763b2..9bc4ca63 100644 --- a/tests/src/mutually-recursive-traits.rs +++ b/tests/src/mutually-recursive-traits.rs @@ -1,6 +1,6 @@ //@ [lean] known-failure -//@ [coq,fstar] skip -//@ subdir=misc +//@ [!lean] skip +//@ [lean] subdir=misc pub trait Trait1 { type T: Trait2; } diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs index 6d3074ef..11c4a695 100644 --- a/tests/src/no_nested_borrows.rs +++ b/tests/src/no_nested_borrows.rs @@ -1,5 +1,5 @@ //@ charon-args=--no-code-duplication -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] 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 6a4a7c31..d9fb1032 100644 --- a/tests/src/paper.rs +++ b/tests/src/paper.rs @@ -1,5 +1,5 @@ //@ charon-args=--no-code-duplication -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc //! The examples from the ICFP submission, all in one place. diff --git a/tests/src/polonius_list.rs b/tests/src/polonius_list.rs index b029ad02..084441aa 100644 --- a/tests/src/polonius_list.rs +++ b/tests/src/polonius_list.rs @@ -1,5 +1,5 @@ //@ charon-args=--polonius -//@ aeneas-args=-test-trans-units +//@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc #![allow(dead_code)] diff --git a/tests/src/string-chars.rs b/tests/src/string-chars.rs index f8490e76..9fd91752 100644 --- a/tests/src/string-chars.rs +++ b/tests/src/string-chars.rs @@ -1,5 +1,5 @@ //@ [lean] known-failure -//@ [coq,fstar] skip +//@ [!lean] skip //@ no-check-output fn main() { let s = "hello"; diff --git a/tests/test_runner/Backend.ml b/tests/test_runner/Backend.ml index d21a46fc..819081a2 100644 --- a/tests/test_runner/Backend.ml +++ b/tests/test_runner/Backend.ml @@ -1,15 +1,24 @@ (*** Define the backends we support as an enum *) -type t = Coq | Lean | FStar | HOL4 [@@deriving ord, sexp] +type t = + | Coq + | Lean + | FStar + | HOL4 + | BorrowCheck + (** Borrow check: no backend. + We use this when we only want to borrow-check the program *) +[@@deriving ord, sexp] (* TODO: reactivate HOL4 once traits are parameterized by their associated types *) -let all = [ Coq; Lean; FStar ] +let all = [ Coq; Lean; FStar; BorrowCheck ] let of_string = function | "coq" -> Coq | "lean" -> Lean | "fstar" -> FStar | "hol4" -> HOL4 + | "borrow-check" -> BorrowCheck | backend -> failwith ("Unknown backend: `" ^ backend ^ "`") let to_string = function @@ -17,6 +26,11 @@ let to_string = function | Lean -> "lean" | FStar -> "fstar" | HOL4 -> "hol4" + | BorrowCheck -> "borrow-check" + +let to_command = function + | BorrowCheck -> [ "-borrow-check" ] + | x -> [ "-backend"; to_string x ] module Map = struct (* Hack to be able to include things from the parent module with the same names *) diff --git a/tests/test_runner/Input.ml b/tests/test_runner/Input.ml index 960ffe8d..e35be96f 100644 --- a/tests/test_runner/Input.ml +++ b/tests/test_runner/Input.ml @@ -7,7 +7,7 @@ type action = Normal | Skip | KnownFailure type per_backend = { action : action; aeneas_options : string list; - subdir : string; + subdir : string option; (* Whether to store the command output to a file. Only available for known-failure tests. *) check_output : bool; } @@ -22,8 +22,11 @@ type t = { } (* The default subdirectory in which to store the outputs. *) -let default_subdir backend test_name = - match backend with Backend.Lean -> "." | _ -> test_name +let default_subdir backend test_name : string option = + match backend with + | Backend.Lean -> Some "." + | Backend.BorrowCheck -> None + | _ -> Some test_name (* Parse lines that start `//@`. Each of them modifies the options we use for the test. Supported comments: @@ -39,14 +42,21 @@ let default_subdir backend test_name = 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 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 exclude = Re.Group.get_opt groups 1 <> None in + let backends = Re.Group.get groups 2 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 + let rest = Re.Group.get groups 3 in + (* If [exclude]: we take all the backends *but* the list provided. *) + let backends = + if exclude then + List.filter (fun x -> not (List.mem x backends)) Backend.all + else backends + in (String.trim rest, backends) | None -> (comment, Backend.all) in @@ -83,9 +93,9 @@ let apply_special_comment comment input = 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 if Option.is_some subdir then ( + assert (not (List.mem Backend.BorrowCheck backends)); + 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. *) diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index c17c17be..9bdfe81d 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -50,21 +50,28 @@ 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 + let backend_command = Backend.to_command backend in let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" 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 + (* No destination directory if we borrow-check *) + let dest_command = + match backend with + | Backend.BorrowCheck -> [] + | _ -> + let subdir = match subdir with None -> [] | Some x -> [ x ] in + [ "-dest"; concat_path ([ env.dest_dir; backend_str ] @ subdir) ] + in (* Build the command *) - let args = - [ env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend_str ] - in + let args = [ env.aeneas_path; input_file ] @ dest_command @ backend_command in let abort_on_error = match action with | Skip | Normal -> [] |