summaryrefslogtreecommitdiff
path: root/cfrontend/Initializersproof.v
blob: fde3c4ed671575121a2f805ea43c353e1dd4604d (plain)
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
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
(* *********************************************************************)
(*                                                                     *)
(*              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.     *)
(*                                                                     *)
(* *********************************************************************)

(** Compile-time evaluation of initializers for global C variables. *)

Require Import Coq.Program.Equality.
Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import AST.
Require Import Memory.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Csyntax.
Require Import Csem.
Require Import Initializers.

Open Scope error_monad_scope.

Section SOUNDNESS.

Variable ge: genv.

(** * Simple expressions and their big-step semantics *)

(** An expression is simple if it contains no assignments and no
  function calls. *)

Fixpoint simple (a: expr) : Prop :=
  match a with
  | Eloc _ _ _ => True
  | Evar _ _ => True
  | Ederef r _ => simple r
  | Efield l1 _ _ => simple l1
  | Eval _ _ => True
  | Evalof l _ => simple l
  | Eaddrof l _ => simple l
  | Eunop _ r1 _ => simple r1
  | Ebinop _ r1 r2 _ => simple r1 /\ simple r2
  | Ecast r1 _ => simple r1
  | Econdition r1 r2 r3 _ => simple r1 /\ simple r2 /\ simple r3
  | Esizeof _ _ => True
  | Eassign _ _ _ => False
  | Eassignop _ _ _ _ _ => False
  | Epostincr _ _ _ => False
  | Ecomma r1 r2 _ => simple r1 /\ simple r2
  | Ecall _ _ _ => False
  | Eparen r1 _ => simple r1
  end.

(** A big-step semantics for simple expressions.  Similar to the
  big-step semantics from [Cstrategy], with the addition of
  conditionals, comma and paren operators.  It is a pity we do not
  share definitions with [Cstrategy], but such sharing raises
  technical difficulties. *)

Section SIMPLE_EXPRS.

Variable e: env.
Variable m: mem.

Inductive eval_simple_lvalue: expr -> block -> int -> Prop :=
  | esl_loc: forall b ofs ty,
      eval_simple_lvalue (Eloc b ofs ty) b ofs
  | esl_var_local: forall x ty b,
      e!x = Some(b, ty) ->
      eval_simple_lvalue (Evar x ty) b Int.zero
  | esl_var_global: forall x ty b,
      e!x = None ->
      Genv.find_symbol ge x = Some b ->
      type_of_global ge b = Some ty ->
      eval_simple_lvalue (Evar x ty) b Int.zero
  | esl_deref: forall r ty b ofs,
      eval_simple_rvalue r (Vptr b ofs) ->
      eval_simple_lvalue (Ederef r ty) b ofs
  | esl_field_struct: forall l f ty b ofs id fList delta,
      eval_simple_lvalue l b ofs ->
      typeof l = Tstruct id fList -> field_offset f fList = OK delta ->
      eval_simple_lvalue (Efield l f ty) b (Int.add ofs (Int.repr delta))
  | esl_field_union: forall l f ty b ofs id fList,
      eval_simple_lvalue l b ofs ->
      typeof l = Tunion id fList ->
      eval_simple_lvalue (Efield l f ty) b ofs

with eval_simple_rvalue: expr -> val -> Prop :=
  | esr_val: forall v ty,
      eval_simple_rvalue (Eval v ty) v
  | esr_rvalof: forall b ofs l ty v,
      eval_simple_lvalue l b ofs ->
      ty = typeof l ->
      load_value_of_type ty m b ofs = Some v ->
      eval_simple_rvalue (Evalof l ty) v
  | esr_addrof: forall b ofs l ty,
      eval_simple_lvalue l b ofs ->
      eval_simple_rvalue (Eaddrof l ty) (Vptr b ofs)
  | esr_unop: forall op r1 ty v1 v,
      eval_simple_rvalue r1 v1 ->
      sem_unary_operation op v1 (typeof r1) = Some v ->
      eval_simple_rvalue (Eunop op r1 ty) v
  | esr_binop: forall op r1 r2 ty v1 v2 v,
      eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v2 ->
      sem_binary_operation op v1 (typeof r1) v2 (typeof r2) m = Some v ->
      eval_simple_rvalue (Ebinop op r1 r2 ty) v
  | esr_cast: forall ty r1 v1 v,
      eval_simple_rvalue r1 v1 ->
      cast v1 (typeof r1) ty v ->
      eval_simple_rvalue (Ecast r1 ty) v
  | esr_sizeof: forall ty1 ty,
      eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1)))
  | esr_condition_true: forall r1 r2 r3 ty v v1,
      eval_simple_rvalue r1 v1 -> is_true v1 (typeof r1) -> eval_simple_rvalue r2 v ->
      eval_simple_rvalue (Econdition r1 r2 r3 ty) v
  | esr_condition_false: forall r1 r2 r3 ty v v1,
      eval_simple_rvalue r1 v1 -> is_false v1 (typeof r1) -> eval_simple_rvalue r3 v ->
      eval_simple_rvalue (Econdition r1 r2 r3 ty) v
  | esr_comma: forall r1 r2 ty v1 v,
      eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v ->
      eval_simple_rvalue (Ecomma r1 r2 ty) v
  | esr_paren: forall r ty v,
      eval_simple_rvalue r v ->
      eval_simple_rvalue (Eparen r ty) v.

End SIMPLE_EXPRS.

(** * Correctness of the big-step semantics with respect to reduction sequences *)

(** In this section, we show that if a simple expression [a] reduces to
  some value (with the transition semantics from module [Csem]),
  then it evaluates to this value (with the big-step semantics above). *)

Definition compat_eval (k: kind) (e: env) (a a': expr) (m: mem) : Prop :=
  typeof a = typeof a' /\
  match k with
  | LV => forall b ofs, eval_simple_lvalue e m a' b ofs -> eval_simple_lvalue e m a b ofs
  | RV => forall v, eval_simple_rvalue e m a' v -> eval_simple_rvalue e m a v
  end.

Lemma lred_simple:
  forall e l m l' m', lred ge e l m l' m' -> simple l -> simple l'.
Proof.
  induction 1; simpl; tauto.
Qed.

Lemma lred_compat:
  forall e l m l' m', lred ge e l m l' m' ->
  m = m' /\ compat_eval LV e l l' m.
Proof.
  induction 1; simpl; split; auto; split; auto; intros bx ofsx EV; inv EV.
  apply esl_var_local; auto.
  apply esl_var_global; auto.
  constructor. constructor.
  eapply esl_field_struct; eauto. constructor. simpl; eauto.
  eapply esl_field_union; eauto. constructor. simpl; eauto.
Qed.

Lemma rred_simple:
  forall r m r' m', rred r m r' m' -> simple r -> simple r'.
Proof.
  induction 1; simpl; tauto.
Qed.

Lemma rred_compat:
  forall e r m r' m', rred r m r' m' ->
  simple r ->
  m = m' /\ compat_eval RV e r r' m.
Proof.
  induction 1; simpl; intro SIMP; try contradiction; split; auto; split; auto; intros vx EV.
  inv EV. econstructor. constructor. auto. auto. 
  inv EV. econstructor. constructor.
  inv EV. econstructor; eauto. constructor. 
  inv EV. econstructor; eauto. constructor. constructor.
  inv EV. econstructor; eauto. constructor.
  inv EV. eapply esr_condition_true; eauto. constructor. 
  inv EV. eapply esr_condition_false; eauto. constructor.
  inv EV. constructor.
  econstructor; eauto. constructor.
  constructor; auto.
Qed.

Lemma compat_eval_context:
  forall e a a' m from to C,
  context from to C ->
  compat_eval from e a a' m ->
  compat_eval to e (C a) (C a') m.
Proof.
  induction 1; intros CE; auto;
  try (generalize (IHcontext CE); intros [TY EV]; red; split; simpl; auto; intros).
  inv H0. constructor; auto.
  inv H0.
    eapply esl_field_struct; eauto. rewrite TY; eauto. 
    eapply esl_field_union; eauto. rewrite TY; eauto.
  inv H0. econstructor. eauto. auto. auto.
  inv H0. econstructor; eauto. 
  inv H0. econstructor; eauto. congruence.
  inv H0. econstructor; eauto. congruence.
  inv H0. econstructor; eauto. congruence.
  inv H0. econstructor; eauto. congruence.
  inv H0.
    eapply esr_condition_true; eauto. congruence.
    eapply esr_condition_false; eauto. congruence.
  inv H0.
  inv H0.
  inv H0.
  inv H0.
  inv H0.
  inv H0.
  red; split; intros. auto. inv H0.
  inv H0. econstructor; eauto.
  inv H0. constructor. auto. 
Qed.

Lemma simple_context_1:
  forall a from to C, context from to C -> simple (C a) -> simple a.
Proof.
  induction 1; simpl; tauto. 
Qed.

Lemma simple_context_2:
  forall a a', simple a' -> forall from to C, context from to C -> simple (C a) -> simple (C a').
Proof.
  induction 2; simpl; tauto. 
Qed.

Lemma compat_eval_steps:
  forall f r e m w r' m',
  star step ge (ExprState f r Kstop e m) w (ExprState f r' Kstop e m') ->
  simple r -> 
  m' = m /\ compat_eval RV e r r' m.
Proof.
  intros. dependent induction H.
  (* base case *) 
  split. auto. red; auto.
  (* inductive case *)
  destruct H.
  (* expression step *)
  assert (X: exists r1, s2 = ExprState f r1 Kstop e m /\ compat_eval RV e r r1 m /\ simple r1).
    inv H.
    (* lred *)
    assert (S: simple a) by (eapply simple_context_1; eauto).
    exploit lred_compat; eauto. intros [A B]. subst m'0.
    econstructor; split. eauto. split.
    eapply compat_eval_context; eauto.
    eapply simple_context_2; eauto. eapply lred_simple; eauto.
    (* rred *)
    assert (S: simple a) by (eapply simple_context_1; eauto).
    exploit rred_compat; eauto. intros [A B]. subst m'0.
    econstructor; split. eauto. split.
    eapply compat_eval_context; eauto.
    eapply simple_context_2; eauto. eapply rred_simple; eauto.
    (* callred *)
    assert (S: simple a) by (eapply simple_context_1; eauto).
    inv H9; simpl in S; contradiction.
  destruct X as [r1 [A [B C]]]. subst s2. 
  exploit IHstar; eauto. intros [D E]. 
  split. auto. destruct B; destruct E. split. congruence. auto. 
  (* statement steps *)
  inv H.
Qed.

Theorem eval_simple_steps:
  forall f r e m w v ty m',
  star step ge (ExprState f r Kstop e m) w (ExprState f (Eval v ty) Kstop e m') ->
  simple r ->
  m' = m /\ ty = typeof r /\ eval_simple_rvalue e m r v.
Proof.
  intros. exploit compat_eval_steps; eauto. intros [A [B C]]. 
  intuition. apply C. constructor.
Qed.

(** * Soundness of the compile-time evaluator *)

(** [match_val v v'] holds if the compile-time value [v]
  (with symbolic pointers) matches the run-time value [v']
  (with concrete pointers). *)

Inductive match_val: val -> val -> Prop :=
  | match_vint: forall n,
      match_val (Vint n) (Vint n)
  | match_vfloat: forall f,
      match_val (Vfloat f) (Vfloat f)
  | match_vptr: forall id b ofs,
      Genv.find_symbol ge id = Some b ->
      match_val (Vptr (Zpos id) ofs) (Vptr b ofs)
  | match_vundef:
      match_val Vundef Vundef.

Lemma match_val_of_bool:
  forall b, match_val (Val.of_bool b) (Val.of_bool b).
Proof.
  destruct b; constructor.
Qed.

Hint Constructors match_val: mval.
Hint Resolve match_val_of_bool: mval.

(** The [match_val] relation commutes with the evaluation functions
  from [Csem]. *)

Lemma sem_unary_match:
  forall op ty v1 v v1' v',
  sem_unary_operation op v1 ty = Some v ->
  sem_unary_operation op v1' ty = Some v' ->
  match_val v1 v1' ->
  match_val v v'.
Proof.
  intros. destruct op; simpl in *.
  unfold sem_notbool in *. destruct (classify_bool ty); inv H1; inv H; inv H0; auto with mval. constructor.
  unfold sem_notint in *. destruct (classify_notint ty); inv H1; inv H; inv H0; auto with mval.
  unfold sem_neg in *. destruct (classify_neg ty); inv H1; inv H; inv H0; auto with mval.
Qed.

Lemma mem_empty_not_valid_pointer:
  forall b ofs, Mem.valid_pointer Mem.empty b ofs = false.
Proof.
  intros. unfold Mem.valid_pointer. destruct (Mem.perm_dec Mem.empty b ofs Nonempty); auto.
  red in p. simpl in p. contradiction.
Qed.

Lemma sem_cmp_match:
  forall c v1 ty1 v2 ty2 m v v1' v2' v',
  sem_cmp c v1 ty1 v2 ty2 Mem.empty = Some v ->
  sem_cmp c v1' ty1 v2' ty2 m = Some v' ->
  match_val v1 v1' -> match_val v2 v2' ->
  match_val v v'.
Proof.
  intros. unfold sem_cmp in *.
  destruct (classify_cmp ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval.
  destruct (Int.eq n Int.zero); try discriminate. 
  unfold sem_cmp_mismatch in *. destruct c; inv H3; inv H2; constructor.
  destruct (Int.eq n Int.zero); try discriminate. 
  unfold sem_cmp_mismatch in *. destruct c; inv H2; inv H1; constructor.
  rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.signed ofs)) in H4. discriminate.
Qed.

Lemma sem_binary_match:
  forall op v1 ty1 v2 ty2 m v v1' v2' v',
  sem_binary_operation op v1 ty1 v2 ty2 Mem.empty = Some v ->
  sem_binary_operation op v1' ty1 v2' ty2 m = Some v' ->
  match_val v1 v1' -> match_val v2 v2' ->
  match_val v v'.
Proof.
  intros. unfold sem_binary_operation in *; destruct op.
(* add *)
  unfold sem_add in *. destruct (classify_add ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval.
(* sub *)
  unfold sem_sub in *. destruct (classify_sub ty1 ty2); inv H1; inv H2; try (inv H; inv H0; auto with mval; fail).
  destruct (zeq (Zpos id) (Zpos id0)); try discriminate.
  assert (b0 = b) by congruence. subst b0. rewrite zeq_true in H0. 
  destruct (Int.eq (Int.repr (sizeof ty)) Int.zero); inv H; inv H0; auto with mval.
(* mul *)
  unfold sem_mul in *. destruct (classify_mul ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval.
(* div *)
  unfold sem_div in H0. functional inversion H; rewrite H4 in H0; inv H1; inv H2; inv H0.
  rewrite H11 in H2. inv H2. inv H12. constructor.
  rewrite H11 in H2. inv H2. inv H12. constructor.
  inv H11. constructor.
  inv H11. constructor.
  inv H11. constructor.
(* mod *)
  unfold sem_mod in H0. functional inversion H; rewrite H4 in H0; inv H1; inv H2; inv H0.
  rewrite H11 in H2. inv H2. inv H12. constructor.
  rewrite H11 in H2. inv H2. inv H12. constructor.
(* and *)
  unfold sem_and in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval.
(* or *)
  unfold sem_or in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval.
(* xor *)
  unfold sem_xor in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval.
(* shl *)
  unfold sem_shl in *. destruct (classify_shift ty1 ty2); inv H1; inv H2; try discriminate.
  destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor.
(* shr *)
  unfold sem_shr in *. destruct (classify_shift ty1 ty2); try discriminate;
  destruct s; inv H1; inv H2; try discriminate.
  destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor.
  destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor.
(* comparisons *)
  eapply sem_cmp_match; eauto.
  eapply sem_cmp_match; eauto.
  eapply sem_cmp_match; eauto.
  eapply sem_cmp_match; eauto.
  eapply sem_cmp_match; eauto.
  eapply sem_cmp_match; eauto.
Qed.

Lemma is_neutral_for_cast_correct:
  forall t, neutral_for_cast t -> is_neutral_for_cast t = true.
Proof.
  induction 1; simpl; auto.
Qed.

Lemma cast_match:
  forall v1 ty1 ty2 v2, cast v1 ty1 ty2 v2 ->
  forall v1' v2',  match_val v1' v1 -> do_cast v1' ty1 ty2 = OK v2' ->
  match_val v2' v2.
Proof.
  induction 1; intros v1' v2' MV DC; inv MV; simpl in DC.
  inv DC; constructor.
  rewrite H in DC. inv DC. constructor.
  inv DC; constructor.
  inv DC; constructor.
  rewrite (is_neutral_for_cast_correct _ H) in DC. 
  rewrite (is_neutral_for_cast_correct _ H0) in DC.
  simpl in DC. inv DC. constructor; auto.
  rewrite (is_neutral_for_cast_correct _ H) in DC. 
  rewrite (is_neutral_for_cast_correct _ H0) in DC.
  simpl in DC. 
  assert (OK v2' = OK (Vint n)). 
    inv H; auto. inv H0; auto.
  inv H1. constructor.
Qed.

Lemma bool_val_true:
  forall v v' ty, is_true v' ty -> match_val v v' -> bool_val v ty = OK true.
Proof.
  induction 1; intros MV; inv MV; simpl; auto.
  predSpec Int.eq Int.eq_spec n Int.zero. congruence. auto.
  predSpec Int.eq Int.eq_spec n Int.zero. congruence. auto.
  rewrite H; auto.
Qed.

Lemma bool_val_false:
  forall v v' ty, is_false v' ty -> match_val v v' -> bool_val v ty = OK false.
Proof.
  induction 1; intros MV; inv MV; simpl; auto.
  rewrite H; auto.
Qed.

(** Soundness of [constval] with respect to the big-step semantics *)

Lemma constval_rvalue:
  forall m a v,
  eval_simple_rvalue empty_env m a v ->
  forall v',
  constval a = OK v' ->
  match_val v' v
with constval_lvalue:
  forall m a b ofs,
  eval_simple_lvalue empty_env m a b ofs ->
  forall v',
  constval a = OK v' ->
  match_val v' (Vptr b ofs).
Proof.
  (* rvalue *)
  induction 1; intros v' CV; simpl in CV; try (monadInv CV).
  (* val *)
  destruct v; monadInv CV; constructor.
  (* rval *)
  unfold load_value_of_type in H1. destruct (access_mode ty); try congruence. inv H1. 
  eauto.
  (* addrof *)
  eauto.
  (* unop *)
  revert EQ0. caseEq (sem_unary_operation op x (typeof r1)); intros; inv EQ0.
  eapply sem_unary_match; eauto. 
  (* binop *)
  revert EQ2. caseEq (sem_binary_operation op x (typeof r1) x0 (typeof r2) Mem.empty); intros; inv EQ2.
  eapply sem_binary_match; eauto.
  (* cast *)
  eapply cast_match; eauto. 
  (* sizeof *)
  constructor.
  (* conditional true *)
  assert (x0 = true). exploit bool_val_true; eauto. congruence. subst x0. auto.
  (* conditional false *)
  assert (x0 = false). exploit bool_val_false; eauto. congruence. subst x0. auto.
  (* comma *)
  auto.
  (* paren *)
  auto.

  (* lvalue *)
  induction 1; intros v' CV; simpl in CV; try (monadInv CV).
  (* var local *)
  unfold empty_env in H. rewrite PTree.gempty in H. congruence.
  (* var_global *)
  constructor; auto.
  (* deref *)
  eauto.
  (* field struct *)
  rewrite H0 in CV. monadInv CV. exploit IHeval_simple_lvalue; eauto. intro MV. inv MV.
  simpl. replace x with delta by congruence. constructor. auto.
  (* field union *)
  rewrite H0 in CV. auto.
Qed.

Lemma constval_simple:
  forall a v, constval a = OK v -> simple a.
Proof.
  induction a; simpl; intros vx CV; try (monadInv CV); eauto.
  destruct (typeof a); discriminate || eauto.
  monadInv CV. eauto.
  destruct (access_mode ty); discriminate || eauto.
  intuition eauto.
Qed.
  
(** Soundness of [constval] with respect to the reduction semantics. *)

Theorem constval_steps:
  forall f r m w v v' ty m',
  star step ge (ExprState f r Kstop empty_env m) w (ExprState f (Eval v' ty) Kstop empty_env m') ->
  constval r = OK v ->
  m' = m /\ ty = typeof r /\ match_val v v'.
Proof.
  intros. exploit eval_simple_steps; eauto. eapply constval_simple; eauto. 
  intros [A [B C]]. intuition. eapply constval_rvalue; eauto.
Qed.

(** * Soundness of the translation of initializers *)

Theorem transl_init_single_steps:
  forall ty a data f m w v1 ty1 m' v b ofs m'',
  transl_init_single ty a = OK data ->
  star step ge (ExprState f a Kstop empty_env m) w (ExprState f (Eval v1 ty1) Kstop empty_env m') ->
  cast v1 ty1 ty v ->
  store_value_of_type ty m' b ofs v = Some m'' ->
  Genv.store_init_data ge m b (Int.signed ofs) data = Some m''.
Proof.
  intros. monadInv H. 
  exploit constval_steps; eauto. intros [A [B C]]. subst m' ty1.
  exploit cast_match; eauto. intros D.
  unfold Genv.store_init_data. unfold store_value_of_type in H2. simpl in H2. 
  inv D. 
  (* int *)
  destruct ty; try discriminate. 
  destruct i; inv EQ2.
  destruct s; simpl in H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto. 
  destruct s; simpl in H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto.
  assumption.
  inv EQ2. assumption.
  (* float *)
  destruct ty; try discriminate. 
  destruct f1; inv EQ2; assumption.
  (* pointer *)
  assert (data = Init_addrof id ofs0 /\ access_mode ty = By_value Mint32).
    destruct ty; inv EQ2; auto. destruct i; inv H4; auto.
  destruct H3; subst. rewrite H4 in H2. rewrite H. assumption.
  (* undef *)
  discriminate.
Qed.

End SOUNDNESS.