Require Import Coqlib Maps.
Require Import Errors Integers Floats Values AST Memory Globalenvs Events Smallstep.
Require Import Ctypes Cop Csyntax Csem.
Require Import Initializers.

Open Scope error_monad_scope.

Section WITHEXTERNALCALLS.
Context `{external_calls_prf: ExternalCalls}.

Variable fn_stack_requirements: ident -> Z.

Section SOUNDNESS.

Variable ge: genv.

Simple expressions and their big-step semantics

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.


Section SIMPLE_EXPRS.

Variable e: env.
Variable m: mem.

Inductive eval_simple_lvalue: expr -> block -> ptrofs -> 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 Ptrofs.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 Ptrofs.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 (Ptrofs.add ofs (Ptrofs.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 m = Some v ->
      eval_simple_rvalue (Ecast r1 ty) v
  | esr_sizeof: forall ty1 ty,
      eval_simple_rvalue (Esizeof ty1 ty) (Vptrofs (Ptrofs.repr (sizeof ge ty1)))
  | esr_alignof: forall ty1 ty,
      eval_simple_rvalue (Ealignof ty1 ty) (Vptrofs (Ptrofs.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 m = 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 m = 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 m = 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 m = Some v' ->
      eval_simple_rvalue (Eparen r tycast ty) v'.

End SIMPLE_EXPRS.

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

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'.

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.

Lemma rred_simple:
  forall r m t r' m', rred ge r m t r' m' -> simple r -> simple r'.

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.

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.

Lemma simple_context_1:
  forall a from to C, context from to C -> simple (C a) -> simple a.

Lemma simple_context_2:
  forall a a', simple a' -> forall from to C, context from to C -> simple (C a) -> simple (C a').

Lemma compat_eval_steps_aux f r e m r' m' s2 :
  simple r ->
  star (step fn_stack_requirements) ge s2 nil (ExprState f r' Kstop e m') ->
  estep fn_stack_requirements 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.

Lemma compat_eval_steps:
  forall f r e m r' m',
  star (step fn_stack_requirements) 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.

Theorem eval_simple_steps:
  forall f r e m v ty m',
  star (step fn_stack_requirements) 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.

Soundness of the compile-time evaluator

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.

Lemma mem_empty_not_weak_valid_pointer:
  forall b ofs, Mem.weak_valid_pointer Mem.empty b ofs = false.

Lemma sem_cast_match:
  forall v1 ty1 ty2 m v2 v1' v2',
  sem_cast v1 ty1 ty2 m = Some v2 ->
  do_cast v1' ty1 ty2 = OK v2' ->
  Val.inject inj v1' v1 ->
  Val.inject inj v2' v2.

Lemma bool_val_match:
  forall v ty b v' m,
  bool_val v ty tt = Some b ->
  Val.inject inj v v' ->
  bool_val v' ty m = Some b.


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).

Lemma constval_simple:
  forall a v, constval ge a = OK v -> simple a.


Theorem constval_steps:
  forall f r m v v' ty m',
  star (step fn_stack_requirements) 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'.

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.

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.


Theorem transl_init_spec:
  forall ty i d, transl_init ge ty i = OK d -> tr_init ty i d.

Soundness of the translation of 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 fn_stack_requirements) ge (ExprState f a Kstop empty_env m) E0 (ExprState f (Eval v1 ty1) Kstop empty_env m') ->
  sem_cast v1 ty1 ty m' = 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''.


Lemma transl_init_single_size:
  forall ty a data,
  transl_init_single ge ty a = OK data ->
  init_data_size data = sizeof ge ty.

Notation idlsize := init_data_list_size.

Remark padding_size:
  forall frm to, frm <= to -> idlsize (tr_padding frm to) = to - frm.

Remark idlsize_app:
  forall d1 d2, idlsize (d1 ++ d2) = idlsize d1 + idlsize d2.

Remark union_field_size:
  forall f ty fl, field_type f fl = OK ty -> sizeof ge ty <= sizeof_union ge fl.

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.


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 fn_stack_requirements) 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 m' = 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.

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''.

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.

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').

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'.

End WITHEXTERNALCALLS.