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
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
(** * Correctness of the C front end, part 2: Csharpminor construction functions *)
Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import Integers.
Require Import Floats.
Require Import AST.
Require Import Values.
Require Import Events.
Require Import Memory.
Require Import Globalenvs.
Require Import Csyntax.
Require Import Csem.
Require Import Ctyping.
Require Import Cminor.
Require Import Csharpminor.
Require Import Cshmgen.
Require Import Cshmgenproof1.
Section CONSTRUCTORS.
Variable globenv : genv * gvarenv.
Let ge := fst globenv.
(** * Correctness of Csharpminor construction functions *)
Lemma make_intconst_correct:
forall n e m,
eval_expr globenv e m (make_intconst n) (Vint n).
Proof.
intros. unfold make_intconst. econstructor. reflexivity.
Qed.
Lemma make_floatconst_correct:
forall n e m,
eval_expr globenv e m (make_floatconst n) (Vfloat n).
Proof.
intros. unfold make_floatconst. econstructor. reflexivity.
Qed.
Hint Resolve make_intconst_correct make_floatconst_correct
eval_Eunop eval_Ebinop: cshm.
Hint Extern 2 (@eq trace _ _) => traceEq: cshm.
Remark Vtrue_is_true: Val.is_true Vtrue.
Proof.
simpl. apply Int.one_not_zero.
Qed.
Remark Vfalse_is_false: Val.is_false Vfalse.
Proof.
simpl. auto.
Qed.
Lemma make_boolean_correct_true:
forall e m a v ty,
eval_expr globenv e m a v ->
is_true v ty ->
exists vb,
eval_expr globenv e m (make_boolean a ty) vb
/\ Val.is_true vb.
Proof.
intros until ty; intros EXEC VTRUE.
destruct ty; simpl;
try (exists v; intuition; inversion VTRUE; simpl; auto; fail).
exists Vtrue; split.
eapply eval_Ebinop; eauto with cshm.
inversion VTRUE; simpl.
replace (Float.cmp Cne f0 Float.zero) with (negb (Float.cmp Ceq f0 Float.zero)).
rewrite Float.eq_zero_false. reflexivity. auto.
rewrite Float.cmp_ne_eq. auto.
apply Vtrue_is_true.
Qed.
Lemma make_boolean_correct_false:
forall e m a v ty,
eval_expr globenv e m a v ->
is_false v ty ->
exists vb,
eval_expr globenv e m (make_boolean a ty) vb
/\ Val.is_false vb.
Proof.
intros until ty; intros EXEC VFALSE.
destruct ty; simpl;
try (exists v; intuition; inversion VFALSE; simpl; auto; fail).
exists Vfalse; split.
eapply eval_Ebinop; eauto with cshm.
inversion VFALSE; simpl.
replace (Float.cmp Cne Float.zero Float.zero) with (negb (Float.cmp Ceq Float.zero Float.zero)).
rewrite Float.eq_zero_true. reflexivity.
rewrite Float.cmp_ne_eq. auto.
apply Vfalse_is_false.
Qed.
Lemma make_neg_correct:
forall a tya c va v e m,
sem_neg va tya = Some v ->
make_neg a tya = OK c ->
eval_expr globenv e m a va ->
eval_expr globenv e m c v.
Proof.
intros until m; intro SEM. unfold make_neg.
functional inversion SEM; intros.
inversion H4. eapply eval_Eunop; eauto with cshm.
inversion H4. eauto with cshm.
Qed.
Lemma make_notbool_correct:
forall a tya c va v e m,
sem_notbool va tya = Some v ->
make_notbool a tya = c ->
eval_expr globenv e m a va ->
eval_expr globenv e m c v.
Proof.
intros until m; intro SEM. unfold make_notbool.
functional inversion SEM; intros; rewrite H0 in H4; inversion H4; simpl;
eauto with cshm.
Qed.
Lemma make_notint_correct:
forall a tya c va v e m,
sem_notint va = Some v ->
make_notint a tya = c ->
eval_expr globenv e m a va ->
eval_expr globenv e m c v.
Proof.
intros until m; intro SEM. unfold make_notint.
functional inversion SEM; intros.
inversion H2; eauto with cshm.
Qed.
Definition binary_constructor_correct
(make: expr -> type -> expr -> type -> res expr)
(sem: val -> type -> val -> type -> option val): Prop :=
forall a tya b tyb c va vb v e m,
sem va tya vb tyb = Some v ->
make a tya b tyb = OK c ->
eval_expr globenv e m a va ->
eval_expr globenv e m b vb ->
eval_expr globenv e m c v.
Definition binary_constructor_correct'
(make: expr -> type -> expr -> type -> res expr)
(sem: val -> val -> option val): Prop :=
forall a tya b tyb c va vb v e m,
sem va vb = Some v ->
make a tya b tyb = OK c ->
eval_expr globenv e m a va ->
eval_expr globenv e m b vb ->
eval_expr globenv e m c v.
Lemma make_add_correct: binary_constructor_correct make_add sem_add.
Proof.
red; intros until m. intro SEM. unfold make_add.
functional inversion SEM; rewrite H0; intros.
inversion H7. eauto with cshm.
inversion H7. eauto with cshm.
inversion H7.
eapply eval_Ebinop. eauto.
eapply eval_Ebinop. eauto with cshm. eauto.
simpl. reflexivity. reflexivity.
inversion H7.
eapply eval_Ebinop. eauto.
eapply eval_Ebinop. eauto with cshm. eauto.
simpl. reflexivity. simpl. reflexivity.
Qed.
Lemma make_sub_correct: binary_constructor_correct make_sub sem_sub.
Proof.
red; intros until m. intro SEM. unfold make_sub.
functional inversion SEM; rewrite H0; intros;
inversion H7; eauto with cshm.
eapply eval_Ebinop. eauto.
eapply eval_Ebinop. eauto with cshm. eauto.
simpl. reflexivity. reflexivity.
inversion H9. eapply eval_Ebinop.
eapply eval_Ebinop; eauto.
simpl. unfold eq_block; rewrite H3. reflexivity.
eauto with cshm. simpl. rewrite H8. reflexivity.
Qed.
Lemma make_mul_correct: binary_constructor_correct make_mul sem_mul.
Proof.
red; intros until m. intro SEM. unfold make_mul.
functional inversion SEM; rewrite H0; intros;
inversion H7; eauto with cshm.
Qed.
Lemma make_div_correct: binary_constructor_correct make_div sem_div.
Proof.
red; intros until m. intro SEM. unfold make_div.
functional inversion SEM; rewrite H0; intros.
inversion H8. eapply eval_Ebinop; eauto with cshm.
simpl. rewrite H7; auto.
inversion H8. eapply eval_Ebinop; eauto with cshm.
simpl. rewrite H7; auto.
inversion H7; eauto with cshm.
Qed.
Lemma make_mod_correct: binary_constructor_correct make_mod sem_mod.
red; intros until m. intro SEM. unfold make_mod.
functional inversion SEM; rewrite H0; intros.
inversion H8. eapply eval_Ebinop; eauto with cshm.
simpl. rewrite H7; auto.
inversion H8. eapply eval_Ebinop; eauto with cshm.
simpl. rewrite H7; auto.
Qed.
Lemma make_and_correct: binary_constructor_correct' make_and sem_and.
Proof.
red; intros until m. intro SEM. unfold make_and.
functional inversion SEM. intros. inversion H4.
eauto with cshm.
Qed.
Lemma make_or_correct: binary_constructor_correct' make_or sem_or.
Proof.
red; intros until m. intro SEM. unfold make_or.
functional inversion SEM. intros. inversion H4.
eauto with cshm.
Qed.
Lemma make_xor_correct: binary_constructor_correct' make_xor sem_xor.
Proof.
red; intros until m. intro SEM. unfold make_xor.
functional inversion SEM. intros. inversion H4.
eauto with cshm.
Qed.
Lemma make_shl_correct: binary_constructor_correct' make_shl sem_shl.
Proof.
red; intros until m. intro SEM. unfold make_shl.
functional inversion SEM. intros. inversion H5.
eapply eval_Ebinop; eauto with cshm.
simpl. rewrite H4. auto.
Qed.
Lemma make_shr_correct: binary_constructor_correct make_shr sem_shr.
Proof.
red; intros until m. intro SEM. unfold make_shr.
functional inversion SEM; intros; rewrite H0 in H8; inversion H8.
eapply eval_Ebinop; eauto with cshm.
simpl; rewrite H7; auto.
eapply eval_Ebinop; eauto with cshm.
simpl; rewrite H7; auto.
Qed.
Lemma make_cmp_correct:
forall cmp a tya b tyb c va vb v e m,
sem_cmp cmp va tya vb tyb m = Some v ->
make_cmp cmp a tya b tyb = OK c ->
eval_expr globenv e m a va ->
eval_expr globenv e m b vb ->
eval_expr globenv e m c v.
Proof.
intros until m. intro SEM. unfold make_cmp.
functional inversion SEM; rewrite H0; intros.
(* I32unsi *)
inversion H8. eauto with cshm.
(* ipip int int *)
inversion H8. eauto with cshm.
(* ipip ptr ptr *)
inversion H10. eapply eval_Ebinop; eauto with cshm.
simpl. rewrite H3. unfold eq_block. rewrite H9. auto.
inversion H10. eapply eval_Ebinop; eauto with cshm.
simpl. rewrite H3. unfold eq_block. rewrite H9. auto.
(* ipip ptr int *)
inversion H9. eapply eval_Ebinop; eauto with cshm.
simpl. unfold eval_compare_null. rewrite H8. auto.
(* ipip int ptr *)
inversion H9. eapply eval_Ebinop; eauto with cshm.
simpl. unfold eval_compare_null. rewrite H8. auto.
(* ff *)
inversion H8. eauto with cshm.
Qed.
Lemma transl_unop_correct:
forall op a tya c va v e m,
transl_unop op a tya = OK c ->
sem_unary_operation op va tya = Some v ->
eval_expr globenv e m a va ->
eval_expr globenv e m c v.
Proof.
intros. destruct op; simpl in *.
eapply make_notbool_correct; eauto. congruence.
eapply make_notint_correct with (tya := tya); eauto. congruence.
eapply make_neg_correct; eauto.
Qed.
Lemma transl_binop_correct:
forall op a tya b tyb c va vb v e m,
transl_binop op a tya b tyb = OK c ->
sem_binary_operation op va tya vb tyb m = Some v ->
eval_expr globenv e m a va ->
eval_expr globenv e m b vb ->
eval_expr globenv e m c v.
Proof.
intros. destruct op; simpl in *.
eapply make_add_correct; eauto.
eapply make_sub_correct; eauto.
eapply make_mul_correct; eauto.
eapply make_div_correct; eauto.
eapply make_mod_correct; eauto.
eapply make_and_correct; eauto.
eapply make_or_correct; eauto.
eapply make_xor_correct; eauto.
eapply make_shl_correct; eauto.
eapply make_shr_correct; eauto.
eapply make_cmp_correct; eauto.
eapply make_cmp_correct; eauto.
eapply make_cmp_correct; eauto.
eapply make_cmp_correct; eauto.
eapply make_cmp_correct; eauto.
eapply make_cmp_correct; eauto.
Qed.
Lemma make_cast_correct:
forall e m a v ty1 ty2 v',
eval_expr globenv e m a v ->
cast v ty1 ty2 v' ->
eval_expr globenv e m (make_cast ty1 ty2 a) v'.
Proof.
unfold make_cast, make_cast1, make_cast2.
intros until v'; intros EVAL CAST.
inversion CAST; clear CAST; subst.
(* cast_int_int *)
destruct sz2; destruct si2; repeat econstructor; eauto with cshm.
(* cast_float_int *)
destruct sz2; destruct si2; unfold make_intoffloat; repeat econstructor; eauto with cshm; simpl; auto.
(* cast_int_float *)
destruct sz2; destruct si1; unfold make_floatofint; repeat econstructor; eauto with cshm; simpl; auto.
(* cast_float_float *)
destruct sz2; repeat econstructor; eauto with cshm.
(* neutral, ptr *)
inversion H0; auto; inversion H; auto.
(* neutral, int *)
inversion H0; auto; inversion H; auto.
Qed.
Lemma make_load_correct:
forall addr ty code b ofs v e m,
make_load addr ty = OK code ->
eval_expr globenv e m addr (Vptr b ofs) ->
load_value_of_type ty m b ofs = Some v ->
eval_expr globenv e m code v.
Proof.
unfold make_load, load_value_of_type.
intros until m; intros MKLOAD EVEXP LDVAL.
destruct (access_mode ty); inversion MKLOAD.
(* access_mode ty = By_value m *)
apply eval_Eload with (Vptr b ofs); auto.
(* access_mode ty = By_reference *)
subst code. inversion LDVAL. auto.
Qed.
Lemma make_store_correct:
forall addr ty rhs code e m b ofs v m' f k,
make_store addr ty rhs = OK code ->
eval_expr globenv e m addr (Vptr b ofs) ->
eval_expr globenv e m rhs v ->
store_value_of_type ty m b ofs v = Some m' ->
step globenv (State f code k e m) E0 (State f Sskip k e m').
Proof.
unfold make_store, store_value_of_type.
intros until k; intros MKSTORE EV1 EV2 STVAL.
destruct (access_mode ty); inversion MKSTORE.
(* access_mode ty = By_value m *)
eapply step_store; eauto.
Qed.
End CONSTRUCTORS.
|
