From 0ebfa7a15f4d7218389488ff8a92206c0d6642ec Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 May 2024 16:20:26 +0200 Subject: runner: Allow filenames with dashes --- tests/test_runner/run_test.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'tests/test_runner/run_test.ml') diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 25efbcfd..3bda4e29 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -167,6 +167,7 @@ module Input = struct (* 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 -- cgit v1.2.3 From ff5c20b1ef1309f3752eaf0ffd2789514a30589d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 May 2024 16:09:05 +0200 Subject: runner: Allow per-backend skipping --- tests/test_runner/run_test.ml | 65 ++++++++++++++++++++++++++++++------------- 1 file changed, 46 insertions(+), 19 deletions(-) (limited to 'tests/test_runner/run_test.ml') diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 3bda4e29..71e2c32f 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -111,7 +111,7 @@ 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; @@ -124,7 +124,7 @@ module Input = struct - `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 @@ -144,12 +144,28 @@ module Input = struct let charon_args = Core.String.chop_prefix comment ~prefix:"charon-args=" in let aeneas_args = Core.String.chop_prefix comment ~prefix:"aeneas-args=" 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 = + List.fold_left + (fun map backend -> BackendMap.add backend Skip map) + input.actions backends; + } + else if comment = "known-failure" then + { + input with + actions = + List.fold_left + (fun map backend -> BackendMap.add backend KnownFailure map) + input.actions backends; + } 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 @@ -173,7 +189,11 @@ 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 action = Normal in + let actions = + List.fold_left + (fun map backend -> BackendMap.add backend Normal map) + BackendMap.empty Backend.all + in let charon_options = charon_options_for_test name in let subdir = List.fold_left @@ -190,7 +210,7 @@ module Input = struct BackendMap.empty Backend.all in let input = - { path; name; kind; action; charon_options; subdir; aeneas_options } + { path; name; kind; actions; charon_options; subdir; aeneas_options } in match kind with | SingleFile -> @@ -267,7 +287,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 = @@ -277,15 +297,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" -- cgit v1.2.3 From c1892d14fc9ec728422f05dbb9de13ee92984734 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 May 2024 16:45:45 +0200 Subject: runner: Factor out useful `BackendMap` operations --- tests/test_runner/run_test.ml | 59 +++++++++++++++++++------------------------ 1 file changed, 26 insertions(+), 33 deletions(-) (limited to 'tests/test_runner/run_test.ml') diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 71e2c32f..39330a77 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 "" @@ -145,20 +164,11 @@ module Input = struct let aeneas_args = Core.String.chop_prefix comment ~prefix:"aeneas-args=" in if comment = "skip" then - { - input with - actions = - List.fold_left - (fun map backend -> BackendMap.add backend Skip map) - input.actions backends; - } + { input with actions = BackendMap.add_each backends Skip input.actions } else if comment = "known-failure" then { input with - actions = - List.fold_left - (fun map backend -> BackendMap.add backend KnownFailure map) - input.actions backends; + actions = BackendMap.add_each backends KnownFailure input.actions; } else if Option.is_some charon_args then let args = Option.get charon_args in @@ -173,10 +183,7 @@ 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 failwith ("Unrecognized special comment: `" ^ comment ^ "`") @@ -189,25 +196,11 @@ 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 = - List.fold_left - (fun map backend -> BackendMap.add backend Normal map) - BackendMap.empty Backend.all - 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 - in + let subdir = BackendMap.make (fun backend -> test_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; actions; charon_options; subdir; aeneas_options } -- cgit v1.2.3 From 093ebced6d22f6b805147783c978af13a7a03caa Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 May 2024 16:51:54 +0200 Subject: runner: Specify subdirectory in magic comments --- tests/test_runner/run_test.ml | 31 ++++++++++++++++--------------- 1 file changed, 16 insertions(+), 15 deletions(-) (limited to 'tests/test_runner/run_test.ml') diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 39330a77..8f356365 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -104,21 +104,16 @@ let charon_options_for_test test_name = [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ] | _ -> [] -(* The subdirectory in which to store the outputs. *) +(* The default 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" + | Backend.Lean, _ -> "." | _, "hashmap_main" -> "hashmap_on_disk" - | "hol4", _ -> "misc-" ^ test_name - | ( _, - ( "bitwise" | "constants" | "external" | "loops" | "no_nested_borrows" - | "paper" | "polonius_list" ) ) -> - "misc" + | ( Backend.HOL4, + ( "constants" | "external" | "loops" | "no_nested_borrows" | "paper" + | "polonius_list" ) ) -> + "misc-" ^ test_name | _ -> test_name (* The data for a specific test input *) @@ -133,13 +128,15 @@ module Input = struct actions : action BackendMap.t; charon_options : string list; aeneas_options : string list BackendMap.t; - subdir : string BackendMap.t; + subdirs : string BackendMap.t; } (* 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 @@ -162,6 +159,7 @@ 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 actions = BackendMap.add_each backends Skip input.actions } @@ -185,6 +183,9 @@ module Input = struct 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. *) @@ -198,12 +199,12 @@ module Input = struct in let actions = BackendMap.make (fun _ -> Normal) in let charon_options = charon_options_for_test name in - let subdir = BackendMap.make (fun backend -> test_subdir backend name) in + let subdirs = BackendMap.make (fun backend -> test_subdir backend name) in let aeneas_options = BackendMap.make (fun backend -> aeneas_options_for_test backend name) in let input = - { path; name; kind; actions; charon_options; subdir; aeneas_options } + { path; name; kind; actions; charon_options; subdirs; aeneas_options } in match kind with | SingleFile -> @@ -226,7 +227,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 -- cgit v1.2.3 From 3adbe18d36df3767e98f30b760ccd9c6ace640ad Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 May 2024 17:01:16 +0200 Subject: Rename some subdirectories for consistency --- tests/test_runner/run_test.ml | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) (limited to 'tests/test_runner/run_test.ml') diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 8f356365..5d77bf9e 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -104,18 +104,6 @@ let charon_options_for_test test_name = [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ] | _ -> [] -(* The default 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 - | Backend.Lean, _ -> "." - | _, "hashmap_main" -> "hashmap_on_disk" - | ( Backend.HOL4, - ( "constants" | "external" | "loops" | "no_nested_borrows" | "paper" - | "polonius_list" ) ) -> - "misc-" ^ test_name - | _ -> test_name - (* The data for a specific test input *) module Input = struct type kind = SingleFile | Crate @@ -131,6 +119,10 @@ module Input = struct 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; @@ -199,7 +191,9 @@ module Input = struct in let actions = BackendMap.make (fun _ -> Normal) in let charon_options = charon_options_for_test name in - let subdirs = BackendMap.make (fun backend -> test_subdir backend name) in + let subdirs = + BackendMap.make (fun backend -> default_subdir backend name) + in let aeneas_options = BackendMap.make (fun backend -> aeneas_options_for_test backend name) in -- cgit v1.2.3