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
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** Type preservation for the [Stacking] pass. *)
Require Import Coqlib.
Require Import Maps.
Require Import Errors.
Require Import Integers.
Require Import AST.
Require Import Op.
Require Import Locations.
Require Import Conventions.
Require Import Linear.
Require Import Lineartyping.
Require Import Mach.
Require Import Machtyping.
Require Import Bounds.
Require Import Stacklayout.
Require Import Stacking.
Require Import Stackingproof.
(** We show that the Mach code generated by the [Stacking] pass
is well-typed if the original LTLin code is. *)
Definition wt_instrs (k: Mach.code) : Prop :=
forall i, In i k -> wt_instr i.
Lemma wt_instrs_cons:
forall i k,
wt_instr i -> wt_instrs k -> wt_instrs (i :: k).
Proof.
unfold wt_instrs; intros. elim H1; intro.
subst i0; auto. auto.
Qed.
Section TRANSL_FUNCTION.
Variable f: Linear.function.
Let fe := make_env (function_bounds f).
Variable tf: Mach.function.
Hypothesis TRANSF_F: transf_function f = OK tf.
Lemma wt_fold_right:
forall (A: Set) (f: A -> code -> code) (k: code) (l: list A),
(forall x k', In x l -> wt_instrs k' -> wt_instrs (f x k')) ->
wt_instrs k ->
wt_instrs (List.fold_right f k l).
Proof.
induction l; intros; simpl.
auto.
apply H. apply in_eq. apply IHl.
intros. apply H. auto with coqlib. auto.
auto.
Qed.
Lemma wt_save_callee_save_int:
forall k,
wt_instrs k ->
wt_instrs (save_callee_save_int fe k).
Proof.
intros. unfold save_callee_save_int, save_callee_save_regs.
apply wt_fold_right; auto.
intros. unfold save_callee_save_reg.
case (zlt (index_int_callee_save x) (fe_num_int_callee_save fe)); intro.
apply wt_instrs_cons; auto.
apply wt_Msetstack. apply int_callee_save_type; auto.
auto.
Qed.
Lemma wt_save_callee_save_float:
forall k,
wt_instrs k ->
wt_instrs (save_callee_save_float fe k).
Proof.
intros. unfold save_callee_save_float, save_callee_save_regs.
apply wt_fold_right; auto.
intros. unfold save_callee_save_reg.
case (zlt (index_float_callee_save x) (fe_num_float_callee_save fe)); intro.
apply wt_instrs_cons; auto.
apply wt_Msetstack. apply float_callee_save_type; auto.
auto.
Qed.
Lemma wt_restore_callee_save_int:
forall k,
wt_instrs k ->
wt_instrs (restore_callee_save_int fe k).
Proof.
intros. unfold restore_callee_save_int, restore_callee_save_regs.
apply wt_fold_right; auto.
intros. unfold restore_callee_save_reg.
case (zlt (index_int_callee_save x) (fe_num_int_callee_save fe)); intro.
apply wt_instrs_cons; auto.
constructor. apply int_callee_save_type; auto.
auto.
Qed.
Lemma wt_restore_callee_save_float:
forall k,
wt_instrs k ->
wt_instrs (restore_callee_save_float fe k).
Proof.
intros. unfold restore_callee_save_float, restore_callee_save_regs.
apply wt_fold_right; auto.
intros. unfold restore_callee_save_reg.
case (zlt (index_float_callee_save x) (fe_num_float_callee_save fe)); intro.
apply wt_instrs_cons; auto.
constructor. apply float_callee_save_type; auto.
auto.
Qed.
Lemma wt_save_callee_save:
forall k,
wt_instrs k -> wt_instrs (save_callee_save fe k).
Proof.
intros. unfold save_callee_save.
apply wt_save_callee_save_int. apply wt_save_callee_save_float. auto.
Qed.
Lemma wt_restore_callee_save:
forall k,
wt_instrs k -> wt_instrs (restore_callee_save fe k).
Proof.
intros. unfold restore_callee_save.
apply wt_restore_callee_save_int. apply wt_restore_callee_save_float. auto.
Qed.
Lemma wt_transl_instr:
forall instr k,
In instr f.(Linear.fn_code) ->
Lineartyping.wt_instr f instr ->
wt_instrs k ->
wt_instrs (transl_instr fe instr k).
Proof.
intros.
generalize (instr_is_within_bounds f instr H H0); intro BND.
destruct instr; unfold transl_instr; inv H0; simpl in BND.
(* getstack *)
destruct BND.
destruct s; simpl in *; apply wt_instrs_cons; auto;
constructor; auto.
(* setstack *)
destruct s.
apply wt_instrs_cons; auto. apply wt_Msetstack. auto.
auto.
apply wt_instrs_cons; auto. apply wt_Msetstack. auto.
(* op, move *)
simpl. apply wt_instrs_cons. constructor; auto. auto.
(* op, others *)
apply wt_instrs_cons; auto.
constructor.
destruct o; simpl; congruence.
rewrite H6. destruct o; reflexivity || congruence.
(* load *)
apply wt_instrs_cons; auto.
constructor; auto.
rewrite H4. destruct a; reflexivity.
(* store *)
apply wt_instrs_cons; auto.
constructor; auto.
rewrite H4. destruct a; reflexivity.
(* call *)
apply wt_instrs_cons; auto.
constructor; auto.
(* tailcall *)
apply wt_restore_callee_save. apply wt_instrs_cons; auto.
constructor; auto.
destruct s0; auto. rewrite H5; auto.
(* alloc *)
apply wt_instrs_cons; auto. constructor.
(* label *)
apply wt_instrs_cons; auto.
constructor.
(* goto *)
apply wt_instrs_cons; auto.
constructor; auto.
(* cond *)
apply wt_instrs_cons; auto.
constructor; auto.
(* return *)
apply wt_restore_callee_save. apply wt_instrs_cons. constructor. auto.
Qed.
End TRANSL_FUNCTION.
Lemma wt_transf_function:
forall f tf,
transf_function f = OK tf ->
Lineartyping.wt_function f ->
wt_function tf.
Proof.
intros.
generalize H; unfold transf_function.
case (zlt (Linear.fn_stacksize f) 0); intro.
intros; discriminate.
case (zlt (- Int.min_signed) (fe_size (make_env (function_bounds f)))); intro.
intros; discriminate. intro EQ.
generalize (unfold_transf_function f tf H); intro.
set (b := function_bounds f) in *.
set (fe := make_env b) in *.
assert (fn_framesize tf = fe_size fe).
subst tf; reflexivity.
assert (Int.signed tf.(fn_link_ofs) = offset_of_index fe FI_link).
rewrite H1; unfold fn_link_ofs.
change (fe_ofs_link fe) with (offset_of_index fe FI_link).
unfold fe, b; eapply offset_of_index_no_overflow. eauto. red; auto.
assert (Int.signed tf.(fn_retaddr_ofs) = offset_of_index fe FI_retaddr).
rewrite H1; unfold fn_retaddr_ofs.
change (fe_ofs_retaddr fe) with (offset_of_index fe FI_retaddr).
unfold fe, b; eapply offset_of_index_no_overflow. eauto. red; auto.
constructor.
change (wt_instrs (fn_code tf)).
rewrite H1; simpl; unfold transl_body.
unfold fe, b; apply wt_save_callee_save; auto.
unfold transl_code. apply wt_fold_right.
intros. eapply wt_transl_instr; eauto.
red; intros. elim H5.
subst tf; simpl; auto.
rewrite H2. generalize (size_pos f). fold b; fold fe; omega.
rewrite H3; rewrite H2. change 4 with (4 * typesize (type_of_index FI_link)).
unfold fe, b; apply offset_of_index_valid. red; auto.
rewrite H4; rewrite H2. change 4 with (4 * typesize (type_of_index FI_retaddr)).
unfold fe, b; apply offset_of_index_valid. red; auto.
rewrite H3; rewrite H4.
apply (offset_of_index_disj f FI_retaddr FI_link); red; auto.
Qed.
Lemma wt_transf_fundef:
forall f tf,
Lineartyping.wt_fundef f ->
transf_fundef f = OK tf ->
wt_fundef tf.
Proof.
intros f tf WT. inversion WT; subst.
simpl; intros; inversion H. constructor.
unfold transf_fundef, transf_partial_fundef.
caseEq (transf_function f0); simpl; try congruence.
intros tfn TRANSF EQ. inversion EQ; subst tf.
constructor; eapply wt_transf_function; eauto.
Qed.
Lemma program_typing_preserved:
forall (p: Linear.program) (tp: Mach.program),
transf_program p = OK tp ->
Lineartyping.wt_program p ->
Machtyping.wt_program tp.
Proof.
intros; red; intros.
generalize (transform_partial_program_function transf_fundef p i f H H1).
intros [f0 [IN TRANSF]].
apply wt_transf_fundef with f0; auto.
eapply H0; eauto.
Qed.
|
