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
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
|
(** The compiler back-end and its proof of semantic preservation *)
(** Libraries. *)
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Values.
(** Languages (syntax and semantics). *)
Require Csharpminor.
Require Cminor.
Require RTL.
Require LTL.
Require Linear.
Require Mach.
Require PPC.
(** Translation passes. *)
Require Cminorgen.
Require RTLgen.
Require Constprop.
Require CSE.
Require Allocation.
Require Tunneling.
Require Linearize.
Require Stacking.
Require PPCgen.
(** Type systems. *)
Require RTLtyping.
Require LTLtyping.
Require Lineartyping.
Require Machtyping.
(** Proofs of semantic preservation and typing preservation. *)
Require Cminorgenproof.
Require RTLgenproof.
Require Constpropproof.
Require CSEproof.
Require Allocproof.
Require Alloctyping.
Require Tunnelingproof.
Require Tunnelingtyping.
Require Linearizeproof.
Require Linearizetyping.
Require Stackingproof.
Require Stackingtyping.
Require Machabstr2mach.
Require PPCgenproof.
(** * Composing the translation passes *)
(** We first define useful monadic composition operators,
along with funny (but convenient) notations. *)
Definition apply_total (A B: Set) (x: option A) (f: A -> B) : option B :=
match x with None => None | Some x1 => Some (f x1) end.
Definition apply_partial (A B: Set)
(x: option A) (f: A -> option B) : option B :=
match x with None => None | Some x1 => f x1 end.
Notation "a @@@ b" :=
(apply_partial _ _ a b) (at level 50, left associativity).
Notation "a @@ b" :=
(apply_total _ _ a b) (at level 50, left associativity).
(** We define two translation functions for whole programs: one starting with
a Csharpminor program, the other with a Cminor program. Both
translations produce PPC programs ready for pretty-printing and
assembling. Some front-ends will prefer to generate Csharpminor
(e.g. a C front-end) while some others (e.g. an ML compiler) might
find it more convenient to generate Cminor directly, bypassing
Csharpminor.
There are two ways to compose the compiler passes. The first translates
every function from the Cminor program from Cminor to RTL, then to LTL, etc,
all the way to PPC, and iterates this transformation for every function.
The second translates the whole Cminor program to a RTL program, then to
an LTL program, etc. We follow the first approach because it has lower
memory requirements.
The translation of a Cminor function to a PPC function is as follows. *)
Definition transf_cminor_fundef (f: Cminor.fundef) : option PPC.fundef :=
Some f
@@@ RTLgen.transl_fundef
@@ Constprop.transf_fundef
@@ CSE.transf_fundef
@@@ Allocation.transf_fundef
@@ Tunneling.tunnel_fundef
@@ Linearize.transf_fundef
@@@ Stacking.transf_fundef
@@@ PPCgen.transf_fundef.
(** And here is the translation for Csharpminor functions. *)
Definition transf_csharpminor_fundef
(gce: Cminorgen.compilenv) (f: Csharpminor.fundef) : option PPC.fundef :=
Some f
@@@ Cminorgen.transl_fundef gce
@@@ transf_cminor_fundef.
(** The corresponding translations for whole program follow. *)
Definition transf_cminor_program (p: Cminor.program) : option PPC.program :=
transform_partial_program transf_cminor_fundef p.
Definition transf_csharpminor_program (p: Csharpminor.program) : option PPC.program :=
let gce := Cminorgen.build_global_compilenv p in
transform_partial_program
(transf_csharpminor_fundef gce)
(Csharpminor.program_of_program p).
(** * Equivalence with whole program transformations *)
(** To prove semantic preservation for the whole compiler, it is easier to reason
over the second way to compose the compiler pass: the one that translate
whole programs through each compiler pass. We now define this second translation
and prove that it produces the same PPC programs as the first translation. *)
Definition transf_cminor_program2 (p: Cminor.program) : option PPC.program :=
Some p
@@@ RTLgen.transl_program
@@ Constprop.transf_program
@@ CSE.transf_program
@@@ Allocation.transf_program
@@ Tunneling.tunnel_program
@@ Linearize.transf_program
@@@ Stacking.transf_program
@@@ PPCgen.transf_program.
Definition transf_csharpminor_program2 (p: Csharpminor.program) : option PPC.program :=
Some p
@@@ Cminorgen.transl_program
@@@ transf_cminor_program2.
Lemma transf_partial_program_compose:
forall (A B C: Set)
(f1: A -> option B) (f2: B -> option C)
(p: list (ident * A)),
transf_partial_program f1 p @@@ transf_partial_program f2 =
transf_partial_program (fun f => f1 f @@@ f2) p.
Proof.
induction p. simpl. auto.
simpl. destruct a. destruct (f1 a).
simpl. simpl in IHp. destruct (transf_partial_program f1 p).
simpl. simpl in IHp. destruct (f2 b).
destruct (transf_partial_program f2 l).
rewrite <- IHp. auto.
rewrite <- IHp. auto.
auto.
simpl. rewrite <- IHp. simpl. destruct (f2 b); auto.
simpl. auto.
Qed.
Lemma transform_partial_program_compose:
forall (A B C: Set)
(f1: A -> option B) (f2: B -> option C)
(p: program A),
transform_partial_program f1 p @@@
(fun p' => transform_partial_program f2 p') =
transform_partial_program (fun f => f1 f @@@ f2) p.
Proof.
unfold transform_partial_program; intros.
rewrite <- transf_partial_program_compose. simpl.
destruct (transf_partial_program f1 (prog_funct p)); simpl.
auto. auto.
Qed.
Lemma transf_program_partial_total:
forall (A B: Set) (f: A -> B) (l: list (ident * A)),
Some (AST.transf_program f l) =
AST.transf_partial_program (fun x => Some (f x)) l.
Proof.
induction l. simpl. auto.
simpl. destruct a. rewrite <- IHl. auto.
Qed.
Lemma transform_program_partial_total:
forall (A B: Set) (f: A -> B) (p: program A),
Some (transform_program f p) =
transform_partial_program (fun x => Some (f x)) p.
Proof.
intros. unfold transform_program, transform_partial_program.
rewrite <- transf_program_partial_total. auto.
Qed.
Lemma apply_total_transf_program:
forall (A B: Set) (f: A -> B) (x: option (program A)),
x @@ (fun p => transform_program f p) =
x @@@ (fun p => transform_partial_program (fun x => Some (f x)) p).
Proof.
intros. unfold apply_total, apply_partial.
destruct x. apply transform_program_partial_total. auto.
Qed.
Lemma transf_cminor_program_equiv:
forall p, transf_cminor_program2 p = transf_cminor_program p.
Proof.
intro. unfold transf_cminor_program, transf_cminor_program2, transf_cminor_fundef.
simpl.
unfold RTLgen.transl_program,
Constprop.transf_program, RTL.program.
rewrite apply_total_transf_program.
rewrite transform_partial_program_compose.
unfold CSE.transf_program, RTL.program.
rewrite apply_total_transf_program.
rewrite transform_partial_program_compose.
unfold Allocation.transf_program,
LTL.program, RTL.program.
rewrite transform_partial_program_compose.
unfold Tunneling.tunnel_program, LTL.program.
rewrite apply_total_transf_program.
rewrite transform_partial_program_compose.
unfold Linearize.transf_program, LTL.program, Linear.program.
rewrite apply_total_transf_program.
rewrite transform_partial_program_compose.
unfold Stacking.transf_program, Linear.program, Mach.program.
rewrite transform_partial_program_compose.
unfold PPCgen.transf_program, Mach.program, PPC.program.
rewrite transform_partial_program_compose.
reflexivity.
Qed.
Lemma transf_csharpminor_program_equiv:
forall p, transf_csharpminor_program2 p = transf_csharpminor_program p.
Proof.
intros.
unfold transf_csharpminor_program2, transf_csharpminor_program, transf_csharpminor_fundef.
simpl.
replace transf_cminor_program2 with transf_cminor_program.
unfold transf_cminor_program, Cminorgen.transl_program, Cminor.program, PPC.program.
apply transform_partial_program_compose.
symmetry. apply extensionality. exact transf_cminor_program_equiv.
Qed.
(** * Semantic preservation *)
(** We prove that the [transf_program2] translations preserve semantics. The proof
composes the semantic preservation results for each pass. *)
Lemma transf_cminor_program2_correct:
forall p tp t n,
transf_cminor_program2 p = Some tp ->
Cminor.exec_program p t (Vint n) ->
PPC.exec_program tp t (Vint n).
Proof.
intros until n.
unfold transf_cminor_program2.
simpl. caseEq (RTLgen.transl_program p). intros p1 EQ1.
simpl. set (p2 := CSE.transf_program (Constprop.transf_program p1)).
caseEq (Allocation.transf_program p2). intros p3 EQ3.
simpl. set (p4 := Tunneling.tunnel_program p3).
set (p5 := Linearize.transf_program p4).
caseEq (Stacking.transf_program p5). intros p6 EQ6.
simpl. intros EQTP EXEC.
assert (WT3 : LTLtyping.wt_program p3).
apply Alloctyping.program_typing_preserved with p2. auto.
assert (WT4 : LTLtyping.wt_program p4).
unfold p4. apply Tunnelingtyping.program_typing_preserved. auto.
assert (WT5 : Lineartyping.wt_program p5).
unfold p5. apply Linearizetyping.program_typing_preserved. auto.
assert (WT6: Machtyping.wt_program p6).
apply Stackingtyping.program_typing_preserved with p5. auto. auto.
apply PPCgenproof.transf_program_correct with p6; auto.
apply Machabstr2mach.exec_program_equiv; auto.
apply Stackingproof.transl_program_correct with p5; auto.
unfold p5; apply Linearizeproof.transf_program_correct.
unfold p4; apply Tunnelingproof.transf_program_correct.
apply Allocproof.transl_program_correct with p2; auto.
unfold p2; apply CSEproof.transf_program_correct;
apply Constpropproof.transf_program_correct.
apply RTLgenproof.transl_program_correct with p; auto.
simpl; intros; discriminate.
simpl; intros; discriminate.
simpl; intros; discriminate.
Qed.
Lemma transf_csharpminor_program2_correct:
forall p tp t n,
transf_csharpminor_program2 p = Some tp ->
Csharpminor.exec_program p t (Vint n) ->
PPC.exec_program tp t (Vint n).
Proof.
intros until n; unfold transf_csharpminor_program2; simpl.
caseEq (Cminorgen.transl_program p).
simpl; intros p1 EQ1 EQ2 EXEC.
apply transf_cminor_program2_correct with p1. auto.
apply Cminorgenproof.transl_program_correct with p. auto.
assumption.
simpl; intros; discriminate.
Qed.
(** It follows that the whole compiler is semantic-preserving. *)
Theorem transf_cminor_program_correct:
forall p tp t n,
transf_cminor_program p = Some tp ->
Cminor.exec_program p t (Vint n) ->
PPC.exec_program tp t (Vint n).
Proof.
intros. apply transf_cminor_program2_correct with p.
rewrite transf_cminor_program_equiv. assumption. assumption.
Qed.
Theorem transf_csharpminor_program_correct:
forall p tp t n,
transf_csharpminor_program p = Some tp ->
Csharpminor.exec_program p t (Vint n) ->
PPC.exec_program tp t (Vint n).
Proof.
intros. apply transf_csharpminor_program2_correct with p.
rewrite transf_csharpminor_program_equiv. assumption. assumption.
Qed.
|
