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
|
(** Type preservation for the [Stacking] pass. *)
Require Import Coqlib.
Require Import Maps.
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 Stacking.
Require Import Stackingproof.
(** We show that the Mach code generated by the [Stacking] pass
is well-typed if the original Linear 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 = Some tf.
Lemma wt_Msetstack':
forall idx ty r,
mreg_type r = ty -> index_valid f idx ->
wt_instr (Msetstack r (Int.repr (offset_of_index fe idx)) ty).
Proof.
intros. constructor. auto.
unfold fe. rewrite (offset_of_index_no_overflow f tf TRANSF_F); auto.
generalize (offset_of_index_valid f idx H0). tauto.
Qed.
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_int_callee_save:
forall cs k,
In cs int_callee_save_regs -> wt_instrs k ->
wt_instrs (save_int_callee_save fe cs k).
Proof.
intros. unfold save_int_callee_save.
case (zlt (index_int_callee_save cs) (fe_num_int_callee_save fe)); intro.
apply wt_instrs_cons; auto.
apply wt_Msetstack'. apply int_callee_save_type; auto.
apply index_saved_int_valid. auto. exact z.
auto.
Qed.
Lemma wt_save_float_callee_save:
forall cs k,
In cs float_callee_save_regs -> wt_instrs k ->
wt_instrs (save_float_callee_save fe cs k).
Proof.
intros. unfold save_float_callee_save.
case (zlt (index_float_callee_save cs) (fe_num_float_callee_save fe)); intro.
apply wt_instrs_cons; auto.
apply wt_Msetstack'. apply float_callee_save_type; auto.
apply index_saved_float_valid. auto. exact z.
auto.
Qed.
Lemma wt_restore_int_callee_save:
forall cs k,
In cs int_callee_save_regs -> wt_instrs k ->
wt_instrs (restore_int_callee_save fe cs k).
Proof.
intros. unfold restore_int_callee_save.
case (zlt (index_int_callee_save cs) (fe_num_int_callee_save fe)); intro.
apply wt_instrs_cons; auto.
constructor. apply int_callee_save_type; auto.
auto.
Qed.
Lemma wt_restore_float_callee_save:
forall cs k,
In cs float_callee_save_regs -> wt_instrs k ->
wt_instrs (restore_float_callee_save fe cs k).
Proof.
intros. unfold restore_float_callee_save.
case (zlt (index_float_callee_save cs) (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_fold_right. exact wt_save_int_callee_save.
apply wt_fold_right. exact wt_save_float_callee_save.
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_fold_right. exact wt_restore_int_callee_save.
apply wt_fold_right. exact wt_restore_float_callee_save.
auto.
Qed.
Lemma wt_transl_instr:
forall instr k,
Lineartyping.wt_instr f instr ->
wt_instrs k ->
wt_instrs (transl_instr fe instr k).
Proof.
intros. destruct instr; unfold transl_instr; inversion H.
(* getstack *)
destruct s; simpl in H3; apply wt_instrs_cons; auto;
constructor; auto.
(* setstack *)
destruct s; simpl in H3; simpl in H4.
apply wt_instrs_cons; auto. apply wt_Msetstack'. auto.
apply index_local_valid. auto.
auto.
apply wt_instrs_cons; auto. apply wt_Msetstack'. auto.
apply index_arg_valid. auto.
(* op, move *)
simpl. apply wt_instrs_cons. constructor; auto. auto.
(* op, undef *)
simpl. apply wt_instrs_cons. constructor. auto.
(* op, others *)
apply wt_instrs_cons; auto.
constructor.
destruct o; simpl; congruence.
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 H3. destruct a; reflexivity.
(* call *)
apply wt_instrs_cons; auto.
constructor; 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 = Some 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.
assert (fn_framesize tf = fe_size (make_env (function_bounds f))).
subst tf; reflexivity.
constructor.
change (wt_instrs (fn_code tf)).
rewrite H1; simpl; unfold transl_body.
apply wt_save_callee_save with tf; auto.
unfold transl_code. apply wt_fold_right.
intros. eapply wt_transl_instr; eauto.
red; intros. elim H3.
subst tf; simpl; auto.
rewrite H2. eapply size_pos; eauto.
rewrite H2. eapply size_no_overflow; eauto.
Qed.
Lemma wt_transf_fundef:
forall f tf,
Lineartyping.wt_fundef f ->
transf_fundef f = Some 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); 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 = Some 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.
|
