1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
let concat_path = List.fold_left Filename.concat ""
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
(* 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
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
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
()
| _ -> ()
|
