summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/test_runner/run_test.ml223
1 files changed, 124 insertions, 99 deletions
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 949d5307..1ec2d1c8 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -1,110 +1,135 @@
-let concat_path = List.fold_left Filename.concat ""
+(* Paths to use for tests *)
+type test_env = { aeneas_path : string; llbc_dir : string }
-let () =
- match Array.to_list Sys.argv with
- (* Ad-hoc argument passing for now. *)
- | _exe_path :: aeneas_path :: tests_dir :: test_name :: backend :: options ->
- (* Reproduces the file layout that was set by the Makefile. FIXME: cleanup *)
- let subdir =
- match (backend, test_name) with
- | "lean", "demo" -> "Demo"
- | "lean", _ -> "."
- | _, ("arrays" | "demo" | "hashmap" | "traits") -> test_name
- | _, "betree_main" -> "betree"
- | _, "betree_main-special" -> "betree_back_stateful"
- | _, "hashmap_main" -> "hashmap_on_disk"
- | "hol4", _ -> "misc-" ^ test_name
- | ( _,
- ( "bitwise" | "constants" | "external" | "loops"
- | "no_nested_borrows" | "paper" | "polonius_list" ) ) ->
- "misc"
- | _ -> test_name
- in
+(* The data for a specific test to run *)
+type test_case = {
+ name : string;
+ backend : string;
+ subdir : string;
+ extra_aeneas_options : string list;
+}
- (* File-specific options *)
- (* 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" :: options else options in
+(* Run Aeneas on a specific input with the given options *)
+let run_test env case =
+ let concat_path = List.fold_left Filename.concat "" in
+ let input_file = concat_path [ env.llbc_dir; "llbc"; case.name ] ^ ".llbc" in
+ let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in
+ let args =
+ [|
+ env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; case.backend;
+ |]
+ in
+ let args = Array.append args (Array.of_list case.extra_aeneas_options) in
- let decrease_template_clauses =
- backend = "fstar"
- &&
- match test_name with
- | "arrays" | "betree_main" | "betree_main-special" | "hashmap"
- | "hashmap_main" | "loops" | "traits" ->
- true
- | _ -> false
- in
- let options =
- if decrease_template_clauses then
- "-decreases-clauses" :: "-template-clauses" :: options
- else options
- in
+ (* Debug arguments *)
+ print_string "[test_runner] Running: ";
+ Array.iter
+ (fun x ->
+ print_string x;
+ print_string " ")
+ args;
+ print_endline "";
- let extra_options =
- match (backend, test_name) with
- (* Additional, custom test on the betree: translate it without `-backward-no-state-update`. *)
- (* This generates very ugly code, but is good to test the translation. *)
- | _, "betree_main-special" ->
- [ "-test-trans-units"; "-state"; "-split-files" ]
- | _, "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
+ (* Run Aeneas *)
+ let pid =
+ Unix.create_process env.aeneas_path args Unix.stdin Unix.stdout Unix.stderr
+ in
+ let _ = Unix.waitpid [] pid in
+ ()
+
+(* File-specific options *)
+let test_options 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" | "betree_main-special" | "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
+ (* Additional, custom test on the betree: translate it without `-backward-no-state-update`. *)
+ (* This generates very ugly code, but is good to test the translation. *)
+ | _, "betree_main-special" ->
+ [ "-test-trans-units"; "-state"; "-split-files" ]
+ | _, "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
+
+(* 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"
+ | _, "betree_main-special" -> "betree_back_stateful"
+ | _, "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 :: aeneas_path :: llbc_dir :: test_name :: backend :: options ->
+ let subdir = test_subdir backend test_name in
+ let options = List.append (test_options backend test_name) options in
let test_file_name =
match test_name with
| "betree_main-special" -> "betree_main"
| _ -> test_name
in
- let input_file =
- concat_path [ tests_dir; "llbc"; test_file_name ] ^ ".llbc"
- in
- let dest_dir = concat_path [ "tests"; backend; subdir ] in
- let args =
- [| aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend |]
- in
- let args = Array.append args (Array.of_list options) in
-
- (* Debug arguments *)
- print_string "[test_runner] Running: ";
- Array.iter
- (fun x ->
- print_string x;
- print_string " ")
- args;
- print_endline "";
-
- (* Run Aeneas *)
- let pid =
- Unix.create_process aeneas_path args Unix.stdin Unix.stdout Unix.stderr
- in
- let _ = Unix.waitpid [] pid in
- ()
+ run_test { aeneas_path; llbc_dir }
+ {
+ name = test_file_name;
+ backend;
+ subdir;
+ extra_aeneas_options = options;
+ }
| _ -> ()
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 19:26:23 +0000