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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
|
(*
The Compcert verified compiler
Compiler.vexpand -> Compiler.v
Expand the list of RTL compiler passes into Compiler.v
David Monniaux, CNRS, VERIMAG
*)
type is_partial = TOTAL | PARTIAL;;
type print_result = Noprint | Print of string;;
type when_triggered = Always | Option of string;;
type needs_require = Require | NoRequire;;
let rtl_tunneling = PARTIAL, Always, Require, (Some "RTL Branch Tunneling"), "RTLTunneling"
(* FIXME - The gestion of NoRequire is a bit ugly right now. *)
let rtl_passes =
[|
TOTAL, (Option "optim_tailcalls"), Require, (Some "Tail calls"), "Tailcall";
PARTIAL, Always, Require, (Some "Inlining"), "Inlining";
TOTAL, (Option "profile_arcs"), Require, (Some "Profiling insertion"), "Profiling";
TOTAL, (Option "branch_probabilities"), Require, (Some "Profiling use"), "ProfilingExploit";
TOTAL, (Option "optim_move_loop_invariants"), Require, (Some "Inserting initial nop"), "FirstNop";
TOTAL, Always, Require, (Some "Renumbering"), "Renumber";
PARTIAL, (Option "optim_CSE"), Require, (Some "CSE"), "CSE";
PARTIAL, Always, NoRequire, (Some "Static Prediction + inverting conditions"), "Staticpredict";
PARTIAL, Always, NoRequire, (Some "Unrolling one iteration out of innermost loops"), "Unrollsingle";
TOTAL, Always, NoRequire, (Some "Renumbering pre tail duplication"), "Renumber";
PARTIAL, Always, NoRequire, (Some "Performing tail duplication"), "Tailduplicate";
TOTAL, Always, NoRequire, (Some "Renumbering pre unrolling"), "Renumber";
PARTIAL, Always, NoRequire, (Some "Unrolling the body of innermost loops"), "Unrollbody";
TOTAL, Always, NoRequire, (Some "Renumbering pre constprop"), "Renumber";
TOTAL, (Option "optim_constprop"), Require, (Some "Constant propagation"), "Constprop";
TOTAL, Always, NoRequire, (Some "Renumbering pre CSE"), "Renumber";
PARTIAL, (Option "optim_CSE"), Require, (Some "CSE"), "CSE";
TOTAL, (Option "optim_CSE2"), Require, (Some "CSE2"), "CSE2";
PARTIAL, (Option "optim_CSE3"), Require, (Some "CSE3"), "CSE3";
TOTAL, (Option "optim_CSE3"), Require, (Some "Kill useless moves after CSE3"), "KillUselessMoves";
TOTAL, (Option "optim_forward_moves"), Require, (Some "Forwarding moves"), "ForwardMoves";
PARTIAL, (Option "optim_redundancy"), Require, (Some "Redundancy elimination"), "Deadcode";
rtl_tunneling;
TOTAL, Always, Require, (Some "Renumbering pre rotate"), "Renumber";
PARTIAL, Always, NoRequire, (Some "Loop Rotate"), "Looprotate";
TOTAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "Renumbering for LICM"), "Renumber";
PARTIAL, (Option "optim_move_loop_invariants"), Require, (Some "LICM"), "LICM";
TOTAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "Renumbering for LICM"), "Renumber";
PARTIAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "CSE3 for LICM"), "CSE3";
PARTIAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "Redundancy elimination for LICM"), "Deadcode";
TOTAL, (Option "all_loads_nontrap"), Require, None, "Allnontrap";
PARTIAL, Always, Require, (Some "Unused globals"), "Unusedglob";
|];;
let post_rtl_passes =
[|
PARTIAL, Always, Require, (Some "BTL generation"), "RTLtoBTL", Noprint;
PARTIAL, Always, Require, (Some "Prepass scheduling"), "BTL_Scheduler", Noprint;
PARTIAL, Always, Require, (Some "Projection to RTL"), "BTLtoRTL", (Print (Printf.sprintf "RTL %d" ((Array.length rtl_passes) + 1)));
PARTIAL, Always, Require, (Some "Register allocation"), "Allocation", (Print "LTL 1");
PARTIAL, Always, Require, (Some "LTL Branch tunneling"), "LTLTunneling", (Print "LTL 2");
PARTIAL, Always, Require, (Some "CFG linearization"), "Linearize", Noprint;
TOTAL, Always, Require, (Some "Label cleanup"), "CleanupLabels", Noprint;
PARTIAL, (Option "debug"), Require, (Some "Debugging info for local variables"), "Debugvar", Noprint;
PARTIAL, Always, Require, (Some "Mach generation"), "Stacking", (Print "Mach")
|];;
let all_passes =
Array.concat
[Array.mapi
(fun i (a,b,r,c,d) -> (a,b,r,c,d, Print (Printf.sprintf "RTL %d" (i+1))))
rtl_passes;
post_rtl_passes];;
let totality = function TOTAL -> "total" | PARTIAL -> "partial";;
let print_rtl_require oc =
Array.iter (fun (partial, trigger, require, time_label, pass_name, printing) ->
match require with Require ->
Printf.fprintf oc "Require %s.\n" pass_name
| _ -> ()
) all_passes;;
let print_rtl_require_proof oc =
Array.iter (fun (partial, trigger, require, time_label, pass_name, printing) ->
match require with Require ->
Printf.fprintf oc "Require %sproof.\n" pass_name
| _ -> ()
) all_passes;;
let print_rtl_transf oc =
Array.iteri
(fun i (partial, trigger, require, time_label, pass_name, printing) ->
output_string oc (match partial with
| TOTAL -> " @@ "
| PARTIAL -> " @@@ ");
(match trigger with
| Always -> ()
| Option s ->
Printf.fprintf oc "%s_if Compopts.%s " (totality partial) s);
output_char oc '(';
(match time_label with
| None -> ()
| Some s ->
Printf.fprintf oc "time \"%s\" " s);
Printf.fprintf oc "%s.transf_program)\n" pass_name;
(match printing with
| Noprint -> ()
| Print s ->
Printf.fprintf oc " @@ print (print_%s)\n" s)
) all_passes;;
let print_rtl_mkpass oc =
Array.iter (fun (partial, trigger, require, time_label, pass_name, printing) ->
output_string oc " ::: mkpass (";
(match trigger with
| Always -> ()
| Option s ->
Printf.fprintf oc "match_if Compopts.%s " s);
Printf.fprintf oc "%sproof.match_prog)\n" pass_name)
all_passes;;
let print_if kind oc = function
| Always -> ()
| Option s -> Printf.fprintf oc "%s_if %s " kind s;;
let numbering_base = 7
let print_rtl_proof oc =
Array.iteri (fun i (partial, trigger, require, time_label, pass_name, printing) ->
let j = i+numbering_base in
match partial with
| TOTAL ->
Printf.fprintf oc "set (p%d := %a%s.transf_program p%d) in *.\n"
j (print_if "total") trigger pass_name (pred j)
| PARTIAL ->
Printf.fprintf oc "destruct (%a%s.transf_program p%d) as [p%d|e] eqn:P%d; cbn in T; try discriminate.\n"
(print_if "partial") trigger pass_name (pred j) j j)
all_passes;;
let print_rtl_proof2 oc =
Array.iteri (fun i (partial, trigger, require, time_label, pass_name, printing) ->
let j = i+numbering_base in
Printf.fprintf oc " exists p%d; split. " j;
(match trigger with
| Always -> ()
| Option _ ->
(match partial with
| TOTAL -> output_string oc "apply total_if_match. "
| PARTIAL -> output_string oc "eapply partial_if_match; eauto. "));
Printf.fprintf oc "apply %sproof.transf_program_match; auto.\n" pass_name)
all_passes;;
let print_rtl_forward_simulations oc =
Array.iter (fun (partial, trigger, require, time_label, pass_name) ->
output_string oc " eapply compose_forward_simulations.\n ";
(match trigger with
| Always -> ()
| Option s -> output_string oc "eapply match_if_simulation. eassumption. ");
Printf.fprintf oc "eapply %sproof.transf_program_correct; eassumption." pass_name
)
rtl_passes;;
if (Array.length Sys.argv)<>3
then exit 1;;
let filename_in = Sys.argv.(1) and filename_out = Sys.argv.(2) in
let ic = open_in filename_in and oc = open_out filename_out in
try
while true
do
match input_line ic with
| "EXPAND_RTL_TRANSF_PROGRAM" ->
print_rtl_transf oc
| "EXPAND_RTL_REQUIRE" ->
print_rtl_require oc
| "EXPAND_RTL_REQUIRE_PROOF" ->
print_rtl_require_proof oc
| "EXPAND_RTL_MKPASS" ->
print_rtl_mkpass oc
| "EXPAND_RTL_PROOF" ->
print_rtl_proof oc
| "EXPAND_RTL_PROOF2" ->
print_rtl_proof2 oc
| "EXPAND_ASM_SEMANTICS" ->
Printf.fprintf oc " (Asm.semantics p%d)\n"
((Array.length all_passes) + 7)
| "EXPAND_RTL_FORWARD_SIMULATIONS" ->
print_rtl_forward_simulations oc
| line -> (output_string oc line;
output_char oc '\n')
done
with End_of_file ->
(close_in ic; close_out oc);;
|
