(* *********************************************************************)
(*                                                                     *)
(*              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 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 Events.
Require Import Smallstep.
Require Import Ctypes.
Require Import Cop.
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
  | Eseqand r1 r2 _ => simple r1 /\ simple r2
  | Eseqor r1 r2 _ => simple r1 /\ simple r2
  | Econdition r1 r2 r3 _ => simple r1 /\ simple r2 /\ simple r3
  | Esizeof _ _ => True
  | Ealignof _ _ => True
  | Eassign _ _ _ => False
  | Eassignop _ _ _ _ _ => False
  | Epostincr _ _ _ => False
  | Ecomma r1 r2 _ => simple r1 /\ simple r2
  | Ecall _ _ _ => False
  | Ebuiltin _ _ _ _ => 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 ->
      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 r f ty b ofs id co a delta,
      eval_simple_rvalue r (Vptr b ofs) ->
      typeof r = Tstruct id a -> ge.(genv_cenv)!id = Some co -> field_offset ge f (co_members co) = OK delta ->
      eval_simple_lvalue (Efield r f ty) b (Int.add ofs (Int.repr delta))
  | esl_field_union: forall r f ty b ofs id a,
      eval_simple_rvalue r (Vptr b ofs) ->
      typeof r = Tunion id a ->
      eval_simple_lvalue (Efield r 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 ->
      deref_loc ge ty m b ofs E0 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) m = 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 ge 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 ->
      sem_cast v1 (typeof r1) ty = Some v ->
      eval_simple_rvalue (Ecast r1 ty) v
  | esr_sizeof: forall ty1 ty,
      eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1)))
  | esr_alignof: forall ty1 ty,
      eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1)))
  | esr_seqand_true: forall r1 r2 ty v1 v2 v3,
      eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true ->
      eval_simple_rvalue r2 v2 ->
      sem_cast v2 (typeof r2) type_bool = Some v3 ->
      eval_simple_rvalue (Eseqand r1 r2 ty) v3
  | esr_seqand_false: forall r1 r2 ty v1,
      eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some false ->
      eval_simple_rvalue (Eseqand r1 r2 ty) (Vint Int.zero)
  | esr_seqor_false: forall r1 r2 ty v1 v2 v3,
      eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some false ->
      eval_simple_rvalue r2 v2 ->
      sem_cast v2 (typeof r2) type_bool = Some v3 ->
      eval_simple_rvalue (Eseqor r1 r2 ty) v3
  | esr_seqor_true: forall r1 r2 ty v1,
      eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true ->
      eval_simple_rvalue (Eseqor r1 r2 ty) (Vint Int.one)
  | esr_condition: forall r1 r2 r3 ty v v1 b v',
      eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some b ->
      eval_simple_rvalue (if b then r2 else r3) v' ->
      sem_cast v' (typeof (if b then r2 else r3)) ty = Some 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 tycast ty v v',
      eval_simple_rvalue r v -> sem_cast v (typeof r) tycast = Some v' ->
      eval_simple_rvalue (Eparen r tycast 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 t r' m', rred ge r m t r' m' -> simple r -> simple r'.
Proof.
  induction 1; simpl; intuition. destruct b; auto.
Qed.

Lemma rred_compat:
  forall e r m r' m', rred ge r m E0 r' m' ->
  simple r ->
  m = m' /\ compat_eval RV e r r' m.
Proof.
  intros until m'; intros RED SIMP. inv RED; simpl in 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_seqand_true; eauto. constructor.
  inv EV. eapply esr_seqand_false; eauto. constructor.
  inv EV. eapply esr_seqor_true; eauto. constructor.
  inv EV. eapply esr_seqor_false; eauto. constructor.
  inv EV. eapply esr_condition; eauto. constructor.
  inv EV. constructor.
  inv EV. constructor.
  econstructor; eauto. constructor.
  inv EV. econstructor. 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_seqand_true; eauto. rewrite TY; auto.
    eapply esr_seqand_false; eauto. rewrite TY; auto.
  inv H0.
    eapply esr_seqor_false; eauto. rewrite TY; auto.
    eapply esr_seqor_true; eauto. rewrite TY; auto.
  inv H0. eapply esr_condition; eauto. congruence.
  inv H0.
  inv H0.
  inv H0.
  inv H0.
  inv H0.
  inv H0.
  red; split; intros. auto. inv H0.
  red; split; intros. auto. inv H0.
  inv H0. econstructor; eauto.
  inv H0. econstructor; eauto. congruence.
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; try tauto.
Qed.

Lemma compat_eval_steps_aux f r e m r' m' s2 :
  simple r ->
  star step ge s2 nil (ExprState f r' Kstop e m') ->
  estep ge (ExprState f r Kstop e m) nil s2 ->
  exists r1,
    s2 = ExprState f r1 Kstop e m /\
    compat_eval RV e r r1 m /\ simple r1.
Proof.
  intros.
  inv H1.
  (* 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 H8; simpl in S; contradiction.
  (* stuckred *)
  inv H0. destruct H1; inv H0.
Qed.

Lemma compat_eval_steps:
  forall f r e m  r' m',
  star step ge (ExprState f r Kstop e m) E0 (ExprState f r' Kstop e m') ->
  simple r ->
  m' = m /\ compat_eval RV e r r' m.
Proof.
  intros.
  remember (ExprState f r Kstop e m) as S1.
  remember E0 as t.
  remember (ExprState f r' Kstop e m') as S2.
  revert S1 t S2 H r m r' m' HeqS1 Heqt HeqS2 H0.
  induction 1; intros; subst.
  (* base case *)
  inv HeqS2. split. auto. red; auto.
  (* inductive case *)
  destruct (app_eq_nil t1 t2); auto. subst. inv H.
  (* expression step *)
  exploit compat_eval_steps_aux; eauto.
  intros [r1 [A [B C]]]. subst s2.
  exploit IHstar; eauto. intros [D E].
  split. auto. destruct B; destruct E. split. congruence. auto.
  (* statement steps *)
  inv H1.
Qed.

Theorem eval_simple_steps:
  forall f r e m v ty m',
  star step ge (ExprState f r Kstop e m) E0 (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 *)

(** A global environment [ge] induces a memory injection mapping
  our symbolic pointers [Vptr id ofs] to run-time pointers
  [Vptr b ofs] where [Genv.find_symbol ge id = Some b]. *)

Definition inj (b: block) :=
  match Genv.find_symbol ge b with
  | Some b' => Some (b', 0)
  | None => None
  end.

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 Cur Nonempty); auto.
  eelim Mem.perm_empty; eauto.
Qed.

Lemma mem_empty_not_weak_valid_pointer:
  forall b ofs, Mem.weak_valid_pointer Mem.empty b ofs = false.
Proof.
  intros. unfold Mem.weak_valid_pointer.
  now rewrite !mem_empty_not_valid_pointer.
Qed.

Lemma sem_cast_match:
  forall v1 ty1 ty2 v2 v1' v2',
  sem_cast v1 ty1 ty2 = Some v2 ->
  do_cast v1' ty1 ty2 = OK v2' ->
  Val.inject inj v1' v1 ->
  Val.inject inj v2' v2.
Proof.
  intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:E; inv H0.
  exploit sem_cast_inject. eexact E. eauto.
  intros [v' [A B]]. congruence.
Qed.

Lemma bool_val_match:
  forall v ty b v' m,
  bool_val v ty Mem.empty = Some b ->
  Val.inject inj v v' ->
  bool_val v' ty m = Some b.
Proof.
  intros. eapply bool_val_inj; eauto. intros. rewrite mem_empty_not_weak_valid_pointer in H2; discriminate.
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 ge a = OK v' ->
  Val.inject inj v' v
with constval_lvalue:
  forall m a b ofs,
  eval_simple_lvalue empty_env m a b ofs ->
  forall v',
  constval ge a = OK v' ->
  Val.inject inj v' (Vptr b ofs).
Proof.
  (* rvalue *)
  induction 1; intros vres CV; simpl in CV; try (monadInv CV).
  (* val *)
  destruct v; monadInv CV; constructor.
  (* rval *)
  inv H1; rewrite H2 in CV; try congruence. eauto. eauto.
  (* addrof *)
  eauto.
  (* unop *)
  destruct (sem_unary_operation op x (typeof r1) Mem.empty) as [v1'|] eqn:E; inv EQ0.
  exploit (sem_unary_operation_inj inj Mem.empty m).
  intros. rewrite mem_empty_not_weak_valid_pointer in H2; discriminate.
  eexact E. eauto.
  intros [v' [A B]]. congruence.
  (* binop *)
  destruct (sem_binary_operation ge op x (typeof r1) x0 (typeof r2) Mem.empty) as [v1'|] eqn:E; inv EQ2.
  exploit (sem_binary_operation_inj inj Mem.empty m).
  intros. rewrite mem_empty_not_valid_pointer in H3; discriminate.
  intros. rewrite mem_empty_not_weak_valid_pointer in H3; discriminate.
  intros. rewrite mem_empty_not_weak_valid_pointer in H3; discriminate.
  intros. rewrite mem_empty_not_valid_pointer in H3; discriminate.
  eauto. eauto. eauto.
  intros [v' [A B]]. congruence.
  (* cast *)
  eapply sem_cast_match; eauto.
  (* sizeof *)
  constructor.
  (* alignof *)
  constructor.
  (* seqand *)
  destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2.
  exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'.
  assert (b = true) by congruence. subst b.
  eapply sem_cast_match; eauto.
  destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2.
  exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'.
  assert (b = false) by congruence. subst b. inv H2. auto.
  (* seqor *)
  destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2.
  exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'.
  assert (b = false) by congruence. subst b.
  eapply sem_cast_match; eauto.
  destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2.
  exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'.
  assert (b = true) by congruence. subst b. inv H2. auto.
  (* conditional *)
  destruct (bool_val x (typeof r1) Mem.empty) as [b'|] eqn:E; inv EQ3.
  exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'.
  assert (b' = b) by congruence. subst b'.
  destruct b; eapply sem_cast_match; eauto.
  (* comma *)
  auto.
  (* paren *)
  eapply sem_cast_match; eauto.

  (* 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 *)
  econstructor. unfold inj. rewrite H0. eauto. auto.
  (* deref *)
  eauto.
  (* field struct *)
  rewrite H0 in CV. monadInv CV. unfold lookup_composite in EQ; rewrite H1 in EQ; monadInv EQ.
  exploit constval_rvalue; eauto. intro MV. inv MV.
  simpl. replace x0 with delta by congruence. econstructor; eauto.
  rewrite ! Int.add_assoc. f_equal. apply Int.add_commut.
  simpl. auto.
  (* field union *)
  rewrite H0 in CV. eauto.
Qed.

Lemma constval_simple:
  forall a v, constval ge 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 v v' ty m',
  star step ge (ExprState f r Kstop empty_env m) E0 (ExprState f (Eval v' ty) Kstop empty_env m') ->
  constval ge r = OK v ->
  m' = m /\ ty = typeof r /\ Val.inject inj v v'.
Proof.
  intros. exploit eval_simple_steps; eauto. eapply constval_simple; eauto.
  intros [A [B C]]. intuition. eapply constval_rvalue; eauto.
Qed.

(** * Relational specification of the translation of initializers *)

Definition tr_padding (frm to: Z) : list init_data :=
  if zlt frm to then Init_space (to - frm) :: nil else nil.

Inductive tr_init: type -> initializer -> list init_data -> Prop :=
  | tr_init_sgl: forall ty a d,
      transl_init_single ge ty a = OK d ->
      tr_init ty (Init_single a) (d :: nil)
  | tr_init_arr: forall tyelt nelt attr il d,
      tr_init_array tyelt il (Zmax 0 nelt) d ->
      tr_init (Tarray tyelt nelt attr) (Init_array il) d
  | tr_init_str: forall id attr il co d,
      lookup_composite ge id = OK co -> co_su co = Struct ->
      tr_init_struct (Tstruct id attr) (co_members co) il 0 d ->
      tr_init (Tstruct id attr) (Init_struct il) d
  | tr_init_uni: forall id attr f i1 co ty1 d,
      lookup_composite ge id = OK co -> co_su co = Union -> field_type f (co_members co) = OK ty1 ->
      tr_init ty1 i1 d ->
      tr_init (Tunion id attr) (Init_union f i1)
              (d ++ tr_padding (sizeof ge ty1) (sizeof ge (Tunion id attr)))

with tr_init_array: type -> initializer_list -> Z -> list init_data -> Prop :=
  | tr_init_array_nil_0: forall ty,
      tr_init_array ty Init_nil 0 nil
  | tr_init_array_nil_pos: forall ty sz,
      0 < sz ->
      tr_init_array ty Init_nil sz (Init_space (sz * sizeof ge ty) :: nil)
  | tr_init_array_cons: forall ty i il sz d1 d2,
      tr_init ty i d1 -> tr_init_array ty il (sz - 1) d2 ->
      tr_init_array ty (Init_cons i il) sz (d1 ++ d2)

with tr_init_struct: type -> members -> initializer_list -> Z -> list init_data -> Prop :=
  | tr_init_struct_nil: forall ty pos,
      tr_init_struct ty nil Init_nil pos (tr_padding pos (sizeof ge ty))
  | tr_init_struct_cons: forall ty f1 ty1 fl i1 il pos d1 d2,
      let pos1 := align pos (alignof ge ty1) in
      tr_init ty1 i1 d1 ->
      tr_init_struct ty fl il (pos1 + sizeof ge ty1) d2 ->
      tr_init_struct ty ((f1, ty1) :: fl) (Init_cons i1 il)
                     pos (tr_padding pos pos1 ++ d1 ++ d2).

Lemma transl_padding_spec:
  forall frm to k, padding frm to k = rev (tr_padding frm to) ++ k.
Proof.
  unfold padding, tr_padding; intros. 
  destruct (zlt frm to); auto.
Qed.

Lemma transl_init_rec_spec:
  forall i ty k res,
  transl_init_rec ge ty i k = OK res ->
  exists d, tr_init ty i d /\ res = rev d ++ k

with transl_init_array_spec:
  forall il ty sz k res,
  transl_init_array ge ty il sz k = OK res ->
  exists d, tr_init_array ty il sz d /\ res = rev d ++ k

with transl_init_struct_spec:
  forall il ty fl pos k res,
  transl_init_struct ge ty fl il pos k = OK res ->
  exists d, tr_init_struct ty fl il pos d /\ res = rev d ++ k.

Proof.
Local Opaque sizeof.
- destruct i; intros until res; intros TR; simpl in TR.
+ monadInv TR. exists (x :: nil); split; auto. constructor; auto.
+ destruct ty; try discriminate.
  destruct (transl_init_array_spec _ _ _ _ _ TR) as (d & A & B).
  exists d; split; auto. constructor; auto.
+ destruct ty; try discriminate. monadInv TR. destruct (co_su x) eqn:SU; try discriminate.
  destruct (transl_init_struct_spec _ _ _ _ _ _ EQ0) as (d & A & B).
  exists d; split; auto. econstructor; eauto.
+ destruct ty; try discriminate.
  monadInv TR. destruct (co_su x) eqn:SU; monadInv EQ0.
  destruct (transl_init_rec_spec _ _ _ _ EQ0) as (d & A & B).
  exists (d ++ tr_padding (sizeof ge x0) (sizeof ge (Tunion i0 a))); split.
  econstructor; eauto.
  rewrite rev_app_distr, app_ass, B. apply transl_padding_spec. 

- destruct il; intros until res; intros TR; simpl in TR.
+ destruct (zeq sz 0). 
  inv TR. exists (@nil init_data); split; auto. constructor.
  destruct (zle 0 sz).
  inv TR. econstructor; split. constructor. omega. auto.
  discriminate.
+ monadInv TR. 
  destruct (transl_init_rec_spec _ _ _ _ EQ) as (d1 & A1 & B1).
  destruct (transl_init_array_spec _ _ _ _ _ EQ0) as (d2 & A2 & B2).
  exists (d1 ++ d2); split. econstructor; eauto. 
  subst res x. rewrite rev_app_distr, app_ass. auto.

- destruct il; intros until res; intros TR; simpl in TR.
+ destruct fl; inv TR. econstructor; split. constructor. apply transl_padding_spec.
+ destruct fl as [ | [f1 ty1] fl ]; monadInv TR.
  destruct (transl_init_rec_spec _ _ _ _ EQ) as (d1 & A1 & B1).
  destruct (transl_init_struct_spec _ _ _ _ _ _ EQ0) as (d2 & A2 & B2).
  exists (tr_padding pos (align pos (alignof ge ty1)) ++ d1 ++ d2); split.
  econstructor; eauto.
  rewrite ! rev_app_distr. subst res x. rewrite ! app_ass. rewrite transl_padding_spec. auto.
Qed.

Theorem transl_init_spec:
  forall ty i d, transl_init ge ty i = OK d -> tr_init ty i d.
Proof.
  unfold transl_init; intros. monadInv H. 
  exploit transl_init_rec_spec; eauto. intros (d & A & B). 
  subst x. unfold rev'; rewrite <- rev_alt. 
  rewrite rev_app_distr; simpl. rewrite rev_involutive. auto.
Qed.

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

(** Soundness for single initializers. *)

Theorem transl_init_single_steps:
  forall ty a data f m v1 ty1 m' v chunk b ofs m'',
  transl_init_single ge ty a = OK data ->
  star step ge (ExprState f a Kstop empty_env m) E0 (ExprState f (Eval v1 ty1) Kstop empty_env m') ->
  sem_cast v1 ty1 ty = Some v ->
  access_mode ty = By_value chunk ->
  Mem.store chunk m' b ofs v = Some m'' ->
  Genv.store_init_data ge m b ofs data = Some m''.
Proof.
  intros. monadInv H.
  exploit constval_steps; eauto. intros [A [B C]]. subst m' ty1.
  exploit sem_cast_match; eauto. intros D.
  unfold Genv.store_init_data.
  inv D.
  (* int *)
  destruct ty; try discriminate.
  destruct i0; inv EQ2.
  destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto.
  destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto.
  simpl in H2; inv H2. assumption.
  simpl in H2; inv H2. assumption.
  inv EQ2. simpl in H2; inv H2. assumption.
  (* long *)
  destruct ty; inv EQ2. simpl in H2; inv H2. assumption.
  (* float *)
  destruct ty; try discriminate.
  destruct f1; inv EQ2; simpl in H2; inv H2; assumption.
  (* single *)
  destruct ty; try discriminate.
  destruct f1; inv EQ2; simpl in H2; inv H2; assumption.
  (* pointer *)
  unfold inj in H.
  assert (data = Init_addrof b1 ofs1 /\ chunk = Mint32).
    destruct ty; inv EQ2; inv H2.
    destruct i; inv H5. intuition congruence. auto.
  destruct H4; subst. destruct (Genv.find_symbol ge b1); inv H.
  rewrite Int.add_zero in H3. auto.
  (* undef *)
  discriminate.
Qed.

(** Size properties for initializers. *)

Lemma transl_init_single_size:
  forall ty a data,
  transl_init_single ge ty a = OK data ->
  Genv.init_data_size data = sizeof ge ty.
Proof.
  intros. monadInv H. destruct x0.
- monadInv EQ2.
- destruct ty; try discriminate.
  destruct i0; inv EQ2; auto.
  inv EQ2; auto.
- destruct ty; inv EQ2; auto.
- destruct ty; try discriminate.
  destruct f0; inv EQ2; auto.
- destruct ty; try discriminate.
  destruct f0; inv EQ2; auto.
- destruct ty; try discriminate.
  destruct i0; inv EQ2; auto.
  inv EQ2; auto.
Qed.

Notation idlsize := Genv.init_data_list_size.

Remark padding_size:
  forall frm to, frm <= to -> idlsize (tr_padding frm to) = to - frm.
Proof.
  unfold tr_padding; intros. destruct (zlt frm to).
  simpl. xomega.
  simpl. omega.
Qed.

Remark idlsize_app:
  forall d1 d2, idlsize (d1 ++ d2) = idlsize d1 + idlsize d2.
Proof.
  induction d1; simpl; intros.
  auto.
  rewrite IHd1. omega.
Qed.

Remark union_field_size:
  forall f ty fl, field_type f fl = OK ty -> sizeof ge ty <= sizeof_union ge fl.
Proof.
  induction fl as [|[i t]]; simpl; intros.
- inv H.
- destruct (ident_eq f i).
  + inv H. xomega.
  + specialize (IHfl H). xomega.
Qed.

Hypothesis ce_consistent: composite_env_consistent ge.

Lemma tr_init_size:
  forall i ty data,
  tr_init ty i data ->
  idlsize data = sizeof ge ty
with tr_init_array_size:
  forall ty il sz data,
  tr_init_array ty il sz data ->
  idlsize data = sizeof ge ty * sz
with tr_init_struct_size:
  forall ty fl il pos data,
  tr_init_struct ty fl il pos data ->
  sizeof_struct ge pos fl <= sizeof ge ty ->
  idlsize data + pos = sizeof ge ty.
Proof.
- destruct 1; simpl.
+ erewrite transl_init_single_size by eauto. omega.
+ Local Transparent sizeof. simpl. eapply tr_init_array_size; eauto. 
+ replace (idlsize d) with (idlsize d + 0) by omega.
  eapply tr_init_struct_size; eauto. simpl.
  unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H.
  erewrite co_consistent_sizeof by (eapply ce_consistent; eauto).
  unfold sizeof_composite. rewrite H0. apply align_le.
  destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
+ rewrite idlsize_app, padding_size. 
  exploit tr_init_size; eauto. intros EQ; rewrite EQ. omega.
  simpl. unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H.
  apply Zle_trans with (sizeof_union ge (co_members co)).
  eapply union_field_size; eauto.
  erewrite co_consistent_sizeof by (eapply ce_consistent; eauto).
  unfold sizeof_composite. rewrite H0. apply align_le.
  destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos.

- destruct 1; simpl.
+ omega.
+ rewrite Z.mul_comm.
  assert (0 <= sizeof ge ty * sz).
  { apply Zmult_gt_0_le_0_compat. omega. generalize (sizeof_pos ge ty); omega. }
  xomega.
+ rewrite idlsize_app. 
  erewrite tr_init_size by eauto. 
  erewrite tr_init_array_size by eauto.
  ring.

- destruct 1; simpl; intros.
+ rewrite padding_size by auto. omega.
+ rewrite ! idlsize_app, padding_size. 
  erewrite tr_init_size by eauto. 
  rewrite <- (tr_init_struct_size _ _ _ _ _ H0 H1). omega.
  unfold pos1. apply align_le. apply alignof_pos. 
Qed.

(** A semantics for general initializers *)

Definition dummy_function := mkfunction Tvoid cc_default nil nil Sskip.

Fixpoint fields_of_struct (fl: members) (pos: Z) : list (Z * type) :=
  match fl with
  | nil => nil
  | (id1, ty1) :: fl' =>
      (align pos (alignof ge ty1), ty1) :: fields_of_struct fl' (align pos (alignof ge ty1) + sizeof ge ty1)
  end.

Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop :=
  | exec_init_single: forall m b ofs ty a v1 ty1 chunk m' v m'',
      star step ge (ExprState dummy_function a Kstop empty_env m)
                E0 (ExprState dummy_function (Eval v1 ty1) Kstop empty_env m') ->
      sem_cast v1 ty1 ty = Some v ->
      access_mode ty = By_value chunk ->
      Mem.store chunk m' b ofs v = Some m'' ->
      exec_init m b ofs ty (Init_single a) m''
  | exec_init_array_: forall m b ofs ty sz a il m',
      exec_init_array m b ofs ty sz il m' ->
      exec_init m b ofs (Tarray ty sz a) (Init_array il) m'
  | exec_init_struct: forall m b ofs id a il co m',
      ge.(genv_cenv)!id = Some co -> co_su co = Struct ->
      exec_init_list m b ofs (fields_of_struct (co_members co) 0) il m' ->
      exec_init m b ofs (Tstruct id a) (Init_struct il) m'
  | exec_init_union: forall m b ofs id a f i ty co m',
      ge.(genv_cenv)!id = Some co -> co_su co = Union ->
      field_type f (co_members co) = OK ty ->
      exec_init m b ofs ty i m' ->
      exec_init m b ofs (Tunion id a) (Init_union f i) m'

with exec_init_array: mem -> block -> Z -> type -> Z -> initializer_list -> mem -> Prop :=
  | exec_init_array_nil: forall m b ofs ty sz,
      sz >= 0 ->
      exec_init_array m b ofs ty sz Init_nil m
  | exec_init_array_cons: forall m b ofs ty sz i1 il m' m'',
      exec_init m b ofs ty i1 m' ->
      exec_init_array m' b (ofs + sizeof ge ty) ty (sz - 1) il m'' ->
      exec_init_array m b ofs ty sz (Init_cons i1 il) m''

with exec_init_list: mem -> block -> Z -> list (Z * type) -> initializer_list -> mem -> Prop :=
  | exec_init_list_nil: forall m b ofs,
      exec_init_list m b ofs nil Init_nil m
  | exec_init_list_cons: forall m b ofs pos ty l i1 il m' m'',
      exec_init m b (ofs + pos) ty i1 m' ->
      exec_init_list m' b ofs l il m'' ->
      exec_init_list m b ofs ((pos, ty) :: l) (Init_cons i1 il) m''.

Scheme exec_init_ind3 := Minimality for exec_init Sort Prop
  with exec_init_array_ind3 := Minimality for exec_init_array Sort Prop
  with exec_init_list_ind3 := Minimality for exec_init_list Sort Prop.
Combined Scheme exec_init_scheme from exec_init_ind3, exec_init_array_ind3, exec_init_list_ind3.

Remark exec_init_array_length:
  forall m b ofs ty sz il m',
  exec_init_array m b ofs ty sz il m' -> sz >= 0.
Proof.
  induction 1; omega.
Qed.

Lemma store_init_data_list_app:
  forall data1 m b ofs m' data2 m'',
  Genv.store_init_data_list ge m b ofs data1 = Some m' ->
  Genv.store_init_data_list ge m' b (ofs + idlsize data1) data2 = Some m'' ->
  Genv.store_init_data_list ge m b ofs (data1 ++ data2) = Some m''.
Proof.
  induction data1; simpl; intros.
  inv H. rewrite Zplus_0_r in H0. auto.
  destruct (Genv.store_init_data ge m b ofs a); try discriminate.
  rewrite Zplus_assoc in H0. eauto.
Qed.

Remark store_init_data_list_padding:
  forall frm to b ofs m,
  Genv.store_init_data_list ge m b ofs (tr_padding frm to) = Some m.
Proof.
  intros. unfold tr_padding. destruct (zlt frm to); auto.
Qed.

Lemma tr_init_sound:
  (forall m b ofs ty i m', exec_init m b ofs ty i m' ->
   forall data, tr_init ty i data ->
   Genv.store_init_data_list ge m b ofs data = Some m')
/\(forall m b ofs ty sz il m', exec_init_array m b ofs ty sz il m' ->
   forall data, tr_init_array ty il sz data ->
   Genv.store_init_data_list ge m b ofs data = Some m')
/\(forall m b ofs l il m', exec_init_list m b ofs l il m' ->
   forall ty fl data pos,
   l = fields_of_struct fl pos ->
   tr_init_struct ty fl il pos data ->
   Genv.store_init_data_list ge m b (ofs + pos) data = Some m').
Proof.
Local Opaque sizeof.
  apply exec_init_scheme; simpl; intros.
- (* single *)
  inv H3. simpl. erewrite transl_init_single_steps by eauto. auto.
- (* array *)
  inv H1. replace (Z.max 0 sz) with sz in H7. eauto.
  assert (sz >= 0) by (eapply exec_init_array_length; eauto). xomega.
- (* struct *)
  inv H3. unfold lookup_composite in H7. rewrite H in H7. inv H7. 
  replace ofs with (ofs + 0) by omega. eauto.
- (* union *)
  inv H4. unfold lookup_composite in H9. rewrite H in H9. inv H9. rewrite H1 in H12; inv H12. 
  eapply store_init_data_list_app. eauto.
  apply store_init_data_list_padding.

- (* array, empty *)
  inv H0; auto.
- (* array, nonempty *)
  inv H3.
  eapply store_init_data_list_app.
  eauto.
  rewrite (tr_init_size _ _ _ H7). eauto.

- (* struct, empty *)
  inv H0. apply store_init_data_list_padding.
- (* struct, nonempty *)
  inv H4. simpl in H3; inv H3. 
  eapply store_init_data_list_app. apply store_init_data_list_padding.
  rewrite padding_size.
  replace (ofs + pos0 + (pos2 - pos0)) with (ofs + pos2) by omega.
  eapply store_init_data_list_app.
  eauto.
  rewrite (tr_init_size _ _ _ H9).
  rewrite <- Zplus_assoc. eapply H2. eauto. eauto.
  apply align_le. apply alignof_pos.
Qed.

End SOUNDNESS.

Theorem transl_init_sound:
  forall p m b ty i m' data,
  exec_init (globalenv p) m b 0 ty i m' ->
  transl_init (prog_comp_env p) ty i = OK data ->
  Genv.store_init_data_list (globalenv p) m b 0 data = Some m'.
Proof.
  intros.
  set (ge := globalenv p) in *.
  change (prog_comp_env p) with (genv_cenv ge) in H0.
  destruct (tr_init_sound ge) as (A & B & C).
  eapply build_composite_env_consistent. apply prog_comp_env_eq.
  eapply A; eauto. apply transl_init_spec; auto.
Qed.