Require Import String.
Require Import Coqlib Maps Integers Floats Errors.
Require Import AST Linking.
Require Import Values Memory Globalenvs Builtins Events.
Require Import Ctypes Cop Csyntax Csem.

Local Open Scope error_monad_scope.

Definition strict := false.
Opaque strict.

Definition size_t : type :=
  if Archi.ptr64 then Tlong Unsigned noattr else Tint I32 Unsigned noattr.

Definition ptrdiff_t : type :=
  if Archi.ptr64 then Tlong Signed noattr else Tint I32 Signed noattr.

Operations over types

Definition attr_add_volatile (vol: bool) (a: attr) :=
  {| attr_volatile := a.(attr_volatile) || vol;
     attr_alignas := a.(attr_alignas) |}.

Definition type_of_member (a: attr) (f: ident) (m: members) : res type :=
  do ty <- field_type f m;
  OK (change_attributes (attr_add_volatile a.(attr_volatile)) ty).


Definition type_unop (op: unary_operation) (ty: type) : res type :=
  match op with
  | Onotbool =>
      match classify_bool ty with
      | bool_default => Error (msg "operator !")
      | _ => OK (Tint I32 Signed noattr)
      end
  | Onotint =>
      match classify_notint ty with
      | notint_case_i sg => OK (Tint I32 sg noattr)
      | notint_case_l sg => OK (Tlong sg noattr)
      | notint_default => Error (msg "operator ~")
      end
  | Oneg =>
      match classify_neg ty with
      | neg_case_i sg => OK (Tint I32 sg noattr)
      | neg_case_f => OK (Tfloat F64 noattr)
      | neg_case_s => OK (Tfloat F32 noattr)
      | neg_case_l sg => OK (Tlong sg noattr)
      | neg_default => Error (msg "operator prefix -")
      end
  | Oabsfloat =>
      match classify_neg ty with
      | neg_default => Error (msg "operator __builtin_fabs")
      | _ => OK (Tfloat F64 noattr)
      end
  end.

Definition binarith_type (ty1 ty2: type) (m: string): res type :=
  match classify_binarith ty1 ty2 with
  | bin_case_i sg => OK (Tint I32 sg noattr)
  | bin_case_l sg => OK (Tlong sg noattr)
  | bin_case_f => OK (Tfloat F64 noattr)
  | bin_case_s => OK (Tfloat F32 noattr)
  | bin_default => Error (msg m)
  end.

Definition binarith_int_type (ty1 ty2: type) (m: string): res type :=
  match classify_binarith ty1 ty2 with
  | bin_case_i sg => OK (Tint I32 sg noattr)
  | bin_case_l sg => OK (Tlong sg noattr)
  | _ => Error (msg m)
  end.

Definition shift_op_type (ty1 ty2: type) (m: string): res type :=
  match classify_shift ty1 ty2 with
  | shift_case_ii sg | shift_case_il sg => OK (Tint I32 sg noattr)
  | shift_case_li sg | shift_case_ll sg => OK (Tlong sg noattr)
  | shift_default => Error (msg m)
  end.

Definition comparison_type (ty1 ty2: type) (m: string): res type :=
  match classify_cmp ty1 ty2 with
  | cmp_default =>
      match classify_binarith ty1 ty2 with
      | bin_default => Error (msg m)
      | _ => OK (Tint I32 Signed noattr)
      end
  | _ => OK (Tint I32 Signed noattr)
  end.

Definition type_binop (op: binary_operation) (ty1 ty2: type) : res type :=
  match op with
  | Oexpect => binarith_type ty1 ty2 "__builtin_expect"
  | Oadd =>
      match classify_add ty1 ty2 with
      | add_case_pi ty _ | add_case_ip _ ty
      | add_case_pl ty | add_case_lp ty => OK (Tpointer ty noattr)
      | add_default => binarith_type ty1 ty2 "operator +"
      end
  | Osub =>
      match classify_sub ty1 ty2 with
      | sub_case_pi ty _ | sub_case_pl ty => OK (Tpointer ty noattr)
      | sub_case_pp ty => OK ptrdiff_t
      | sub_default => binarith_type ty1 ty2 "operator infix -"
      end
  | Omul => binarith_type ty1 ty2 "operator infix *"
  | Odiv => binarith_type ty1 ty2 "operator /"
  | Omod => binarith_int_type ty1 ty2 "operator %"
  | Oand => binarith_int_type ty1 ty2 "operator &"
  | Oor => binarith_int_type ty1 ty2 "operator |"
  | Oxor => binarith_int_type ty1 ty2 "operator ^"
  | Oshl => shift_op_type ty1 ty2 "operator <<"
  | Oshr => shift_op_type ty1 ty2 "operator >>"
  | Oeq => comparison_type ty1 ty2 "operator =="
  | One => comparison_type ty1 ty2 "operator !="
  | Olt => comparison_type ty1 ty2 "operator <"
  | Ogt => comparison_type ty1 ty2 "operator >"
  | Ole => comparison_type ty1 ty2 "operator <="
  | Oge => comparison_type ty1 ty2 "operator >="
  end.

Definition type_deref (ty: type) : res type :=
  match ty with
  | Tpointer tyelt _ => OK tyelt
  | Tarray tyelt _ _ => OK tyelt
  | Tfunction _ _ _ => OK ty
  | _ => Error (msg "operator prefix *")
  end.


Definition attr_combine (a1 a2: attr) : attr :=
  {| attr_volatile := a1.(attr_volatile) || a2.(attr_volatile);
     attr_alignas :=
       match a1.(attr_alignas), a2.(attr_alignas) with
       | None, al2 => al2
       | al1, None => al1
       | Some n1, Some n2 => Some (N.max n1 n2)
       end
  |}.

Definition intsize_eq: forall (x y: intsize), {x=y} + {x<>y}.

Definition signedness_eq: forall (x y: signedness), {x=y} + {x<>y}.

Definition floatsize_eq: forall (x y: floatsize), {x=y} + {x<>y}.

Definition callconv_combine (cc1 cc2: calling_convention) : res calling_convention :=
  if option_eq Z.eq_dec cc1.(cc_vararg) cc2.(cc_vararg) then
    OK {| cc_vararg := cc1.(cc_vararg);
          cc_unproto := cc1.(cc_unproto) && cc2.(cc_unproto);
          cc_structret := cc1.(cc_structret) |}
  else
    Error (msg "incompatible calling conventions").

Fixpoint type_combine (ty1 ty2: type) : res type :=
  match ty1, ty2 with
  | Tvoid, Tvoid => OK Tvoid
  | Tint sz1 sg1 a1, Tint sz2 sg2 a2 =>
      if intsize_eq sz1 sz2 && signedness_eq sg1 sg2
      then OK (Tint sz1 sg1 (attr_combine a1 a2))
      else Error (msg "incompatible int types")
  | Tlong sg1 a1, Tlong sg2 a2 =>
      if signedness_eq sg1 sg2
      then OK (Tlong sg1 (attr_combine a1 a2))
      else Error (msg "incompatible long types")
  | Tfloat sz1 a1, Tfloat sz2 a2 =>
      if floatsize_eq sz1 sz2
      then OK (Tfloat sz1 (attr_combine a1 a2))
      else Error (msg "incompatible float types")
  | Tpointer t1 a1, Tpointer t2 a2 =>
      do t <- type_combine t1 t2; OK (Tpointer t (attr_combine a1 a2))
  | Tarray t1 sz1 a1, Tarray t2 sz2 a2 =>
      do t <- type_combine t1 t2;
      if zeq sz1 sz2
      then OK (Tarray t sz1 (attr_combine a1 a2))
      else Error (msg "incompatible array types")
  | Tfunction args1 res1 cc1, Tfunction args2 res2 cc2 =>
      let fix typelist_combine (tl1 tl2: list type) : res (list type) :=
        match tl1, tl2 with
        | nil, nil => OK nil
        | t1 :: tl1, t2 :: tl2 =>
            do t <- type_combine t1 t2;
            do tl <- typelist_combine tl1 tl2;
            OK (t :: tl)
        | _, _ =>
            Error (msg "incompatible function types")
        end in
      do res <- type_combine res1 res2;
      do args <-
        (if cc1.(cc_unproto) then OK args2 else
         if cc2.(cc_unproto) then OK args1 else
         typelist_combine args1 args2);
      do cc <- callconv_combine cc1 cc2;
      OK (Tfunction args res cc)
  | Tstruct id1 a1, Tstruct id2 a2 =>
      if ident_eq id1 id2
      then OK (Tstruct id1 (attr_combine a1 a2))
      else Error (msg "incompatible struct types")
  | Tunion id1 a1, Tunion id2 a2 =>
      if ident_eq id1 id2
      then OK (Tunion id1 (attr_combine a1 a2))
      else Error (msg "incompatible union types")
  | _, _ =>
      Error (msg "incompatible types")
  end.

Definition is_void (ty: type) : bool :=
  match ty with Tvoid => true | _ => false end.

Definition type_conditional (ty1 ty2: type) : res type :=
  match typeconv ty1, typeconv ty2 with
  | (Tint _ _ _ | Tlong _ _ | Tfloat _ _),
    (Tint _ _ _ | Tlong _ _ | Tfloat _ _) =>
      binarith_type ty1 ty2 "conditional expression"
  | Tpointer t1 a1, Tpointer t2 a2 =>
      let t :=
        if is_void t1 || is_void t2 then Tvoid else
          match type_combine t1 t2 with
          | OK t => t
          | Error _ => Tvoid
          end
       in OK (Tpointer t noattr)
  | Tpointer t1 a1, Tint _ _ _ =>
      OK (Tpointer t1 noattr)
  | Tint _ _ _, Tpointer t2 a2 =>
      OK (Tpointer t2 noattr)
  | t1, t2 =>
      type_combine t1 t2
  end.

Specification of the type system

Definition typenv := QITree.t type.

Definition wt_cast (from to: type) : Prop :=
  classify_cast from to <> cast_case_default.

Definition wt_bool (ty: type) : Prop :=
  classify_bool ty <> bool_default.

Definition wt_int (n: int) (sz: intsize) (sg: signedness) : Prop :=
  match sz, sg with
  | IBool, _ => n = Int.zero \/ n = Int.one
  | I8, Unsigned => Int.zero_ext 8 n = n
  | I8, Signed => Int.sign_ext 8 n = n
  | I16, Unsigned => Int.zero_ext 16 n = n
  | I16, Signed => Int.sign_ext 16 n = n
  | I32, _ => True
  end.

Inductive wt_val : val -> type -> Prop :=
  | wt_val_int: forall n sz sg a,
      wt_int n sz sg ->
      wt_val (Vint n) (Tint sz sg a)
  | wt_val_ptr_int: forall b ofs sg a,
      Archi.ptr64 = false ->
      wt_val (Vptr b ofs) (Tint I32 sg a)
  | wt_val_long: forall n sg a,
      wt_val (Vlong n) (Tlong sg a)
  | wt_val_ptr_long: forall b ofs sg a,
      Archi.ptr64 = true ->
      wt_val (Vptr b ofs) (Tlong sg a)
  | wt_val_float: forall f a,
      wt_val (Vfloat f) (Tfloat F64 a)
  | wt_val_single: forall f a,
      wt_val (Vsingle f) (Tfloat F32 a)
  | wt_val_pointer: forall b ofs ty a,
      wt_val (Vptr b ofs) (Tpointer ty a)
  | wt_val_int_pointer: forall n ty a,
      Archi.ptr64 = false ->
      wt_val (Vint n) (Tpointer ty a)
  | wt_val_long_pointer: forall n ty a,
      Archi.ptr64 = true ->
      wt_val (Vlong n) (Tpointer ty a)
  | wt_val_array: forall b ofs ty sz a,
      wt_val (Vptr b ofs) (Tarray ty sz a)
  | wt_val_function: forall b ofs tyargs tyres cc,
      wt_val (Vptr b ofs) (Tfunction tyargs tyres cc)
  | wt_val_struct: forall b ofs id a,
      wt_val (Vptr b ofs) (Tstruct id a)
  | wt_val_union: forall b ofs id a,
      wt_val (Vptr b ofs) (Tunion id a)
  | wt_val_undef: forall ty,
      wt_val Vundef ty
  | wt_val_void: forall v,
      wt_val v Tvoid.

Inductive wt_arguments: exprlist -> list type -> Prop :=
  | wt_arg_nil:
      wt_arguments Enil nil
  | wt_arg_cons: forall a al ty tyl,
      wt_cast (typeof a) ty ->
      wt_arguments al tyl ->
      wt_arguments (Econs a al) (ty :: tyl)
  | wt_arg_extra: forall a al, (* tolerance for varargs *)
      strict = false ->
      wt_arguments (Econs a al) nil.

Definition subtype (t1 t2: type) : Prop :=
  forall v, wt_val v t1 -> wt_val v t2.

Section WT_EXPR_STMT.

Variable ce: composite_env.
Variable e: typenv.

Inductive wt_rvalue : expr -> Prop :=
  | wt_Eval: forall v ty,
      wt_val v ty ->
      wt_rvalue (Eval v ty)
  | wt_Evalof: forall l,
      wt_lvalue l ->
      wt_rvalue (Evalof l (typeof l))
  | wt_Eaddrof: forall l,
      wt_lvalue l ->
      wt_rvalue (Eaddrof l (Tpointer (typeof l) noattr))
  | wt_Eunop: forall op r ty,
      wt_rvalue r ->
      type_unop op (typeof r) = OK ty ->
      wt_rvalue (Eunop op r ty)
  | wt_Ebinop: forall op r1 r2 ty,
      wt_rvalue r1 -> wt_rvalue r2 ->
      type_binop op (typeof r1) (typeof r2) = OK ty ->
      wt_rvalue (Ebinop op r1 r2 ty)
  | wt_Ecast: forall r ty,
      wt_rvalue r -> wt_cast (typeof r) ty ->
      wt_rvalue (Ecast r ty)
  | wt_Eseqand: forall r1 r2,
      wt_rvalue r1 -> wt_rvalue r2 ->
      wt_bool (typeof r1) -> wt_bool (typeof r2) ->
      wt_rvalue (Eseqand r1 r2 (Tint I32 Signed noattr))
  | wt_Eseqor: forall r1 r2,
      wt_rvalue r1 -> wt_rvalue r2 ->
      wt_bool (typeof r1) -> wt_bool (typeof r2) ->
      wt_rvalue (Eseqor r1 r2 (Tint I32 Signed noattr))
  | wt_Econdition: forall r1 r2 r3 ty,
      wt_rvalue r1 -> wt_rvalue r2 -> wt_rvalue r3 ->
      wt_bool (typeof r1) ->
      wt_cast (typeof r2) ty -> wt_cast (typeof r3) ty ->
      wt_rvalue (Econdition r1 r2 r3 ty)
  | wt_Esizeof: forall ty,
      wt_rvalue (Esizeof ty size_t)
  | wt_Ealignof: forall ty,
      wt_rvalue (Ealignof ty size_t)
  | wt_Eassign: forall l r,
      wt_lvalue l -> wt_rvalue r -> wt_cast (typeof r) (typeof l) ->
      wt_rvalue (Eassign l r (typeof l))
  | wt_Eassignop: forall op l r ty,
      wt_lvalue l -> wt_rvalue r ->
      type_binop op (typeof l) (typeof r) = OK ty ->
      wt_cast ty (typeof l) ->
      wt_rvalue (Eassignop op l r ty (typeof l))
  | wt_Epostincr: forall id l ty,
      wt_lvalue l ->
      type_binop (match id with Incr => Oadd | Decr => Osub end)
                 (typeof l) (Tint I32 Signed noattr) = OK ty ->
      wt_cast (incrdecr_type (typeof l)) (typeof l) ->
      wt_rvalue (Epostincr id l (typeof l))
  | wt_Ecomma: forall r1 r2,
      wt_rvalue r1 -> wt_rvalue r2 ->
      wt_rvalue (Ecomma r1 r2 (typeof r2))
  | wt_Ecall: forall r1 rargs tyargs tyres cconv,
      wt_rvalue r1 -> wt_exprlist rargs ->
      classify_fun (typeof r1) = fun_case_f tyargs tyres cconv ->
      wt_arguments rargs tyargs ->
      wt_rvalue (Ecall r1 rargs tyres)
  | wt_Ebuiltin: forall ef tyargs rargs ty,
      wt_exprlist rargs ->
      wt_arguments rargs tyargs ->
         (ty = Tvoid /\ sig_res (ef_sig ef) = Xvoid)
      \/ (tyargs = type_bool :: ty :: ty :: nil
          /\ let t := typ_of_type ty in
             let x := inj_type t in
             let sg := [Xint; x; x ---> x]%asttyp in
             ef = EF_builtin "__builtin_sel"%string sg) ->
      wt_rvalue (Ebuiltin ef tyargs rargs ty)
  | wt_Eparen: forall r tycast ty,
      wt_rvalue r ->
      wt_cast (typeof r) tycast -> subtype tycast ty ->
      wt_rvalue (Eparen r tycast ty)

with wt_lvalue : expr -> Prop :=
  | wt_Eloc: forall b ofs bf ty,
      wt_lvalue (Eloc b ofs bf ty)
  | wt_Evar: forall x ty,
      e!.(QualIdent.root x) = Some ty ->
      wt_lvalue (Evar x ty)
  | wt_Ederef: forall r ty,
      wt_rvalue r ->
      type_deref (typeof r) = OK ty ->
      wt_lvalue (Ederef r ty)
  | wt_Efield: forall r f id a co ty,
      wt_rvalue r ->
      typeof r = Tstruct id a \/ typeof r = Tunion id a ->
      ce!id = Some co ->
      type_of_member a f co.(co_members) = OK ty ->
      wt_lvalue (Efield r f ty)

with wt_exprlist : exprlist -> Prop :=
  | wt_Enil:
      wt_exprlist Enil
  | wt_Econs: forall r1 rl,
      wt_rvalue r1 -> wt_exprlist rl -> wt_exprlist (Econs r1 rl).

Definition wt_expr_kind (k: kind) (a: expr) :=
  match k with
  | RV => wt_rvalue a
  | LV => wt_lvalue a
  end.

Definition expr_kind (a: expr) : kind :=
  match a with
  | Eloc _ _ _ _ => LV
  | Evar _ _ => LV
  | Ederef _ _ => LV
  | Efield _ _ _ => LV
  | _ => RV
  end.

Definition wt_expr (a: expr) :=
  match expr_kind a with
  | RV => wt_rvalue a
  | LV => wt_lvalue a
  end.

Variable rt: type.

Inductive wt_stmt: statement -> Prop :=
  | wt_Sskip:
      wt_stmt Sskip
  | wt_Sdo: forall r,
      wt_rvalue r -> wt_stmt (Sdo r)
  | wt_Ssequence: forall s1 s2,
      wt_stmt s1 -> wt_stmt s2 -> wt_stmt (Ssequence s1 s2)
  | wt_Sifthenelse: forall r s1 s2,
      wt_rvalue r -> wt_stmt s1 -> wt_stmt s2 -> wt_bool (typeof r) ->
      wt_stmt (Sifthenelse r s1 s2)
  | wt_Swhile: forall r s,
      wt_rvalue r -> wt_stmt s -> wt_bool (typeof r) ->
      wt_stmt (Swhile r s)
  | wt_Sdowhile: forall r s,
      wt_rvalue r -> wt_stmt s -> wt_bool (typeof r) ->
      wt_stmt (Sdowhile r s)
  | wt_Sfor: forall s1 r s2 s3,
      wt_rvalue r -> wt_stmt s1 -> wt_stmt s2 -> wt_stmt s3 ->
      wt_bool (typeof r) ->
      wt_stmt (Sfor s1 r s2 s3)
  | wt_Sbreak:
      wt_stmt Sbreak
  | wt_Scontinue:
      wt_stmt Scontinue
  | wt_Sreturn_none:
      wt_stmt (Sreturn None)
  | wt_Sreturn_some: forall r,
      wt_rvalue r ->
      wt_cast (typeof r) rt ->
      wt_stmt (Sreturn (Some r))
  | wt_Sswitch: forall r ls sg sz a,
      wt_rvalue r ->
      typeof r = Tint sz sg a \/ typeof r = Tlong sg a ->
      wt_lblstmts ls ->
      wt_stmt (Sswitch r ls)
  | wt_Slabel: forall lbl s,
      wt_stmt s -> wt_stmt (Slabel lbl s)
  | wt_Sgoto: forall lbl,
      wt_stmt (Sgoto lbl)

with wt_lblstmts : labeled_statements -> Prop :=
  | wt_LSnil:
      wt_lblstmts LSnil
  | wt_LScons: forall case s ls,
      wt_stmt s -> wt_lblstmts ls ->
      wt_lblstmts (LScons case s ls).

End WT_EXPR_STMT.

Fixpoint bind_vars (e: typenv) (l: list (ident * type)) : typenv :=
  match l with
  | nil => e
  | (id, ty) :: l => bind_vars (QITree.set (QualIdent.root id) ty e) l
  end.

Inductive wt_function (ce: composite_env) (e: typenv) : function -> Prop :=
  | wt_function_intro: forall f,
      wt_stmt ce (bind_vars (bind_vars e f.(fn_params)) f.(fn_vars)) f.(fn_return) f.(fn_body) ->
      wt_function ce e f.

Fixpoint bind_globdef (e: typenv) (l: list (qualident * globdef fundef type)) : typenv :=
  match l with
  | nil => e
  | (id, Gfun fd) :: l => bind_globdef (QITree.set id (type_of_fundef fd) e) l
  | (id, Gvar v) :: l => bind_globdef (QITree.set id v.(gvar_info) e) l
  end.

Inductive wt_fundef (ce: composite_env) (e: typenv) : fundef -> Prop :=
  | wt_fundef_internal: forall f,
      wt_function ce e f ->
      wt_fundef ce e (Internal f)
  | wt_fundef_external: forall ef targs tres cc,
      (ef_sig ef).(sig_res) = rettype_of_type tres ->
      wt_fundef ce e (External ef targs tres cc).

Inductive wt_program : program -> Prop :=
  | wt_program_intro: forall p,
      let e := bind_globdef QITree.empty p.(prog_defs) in
      (forall id fd,
         In (id, Gfun fd) p.(prog_defs) ->
         wt_fundef p.(prog_comp_env) e fd) ->
      wt_program p.

Global Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty.
Global Hint Extern 1 (wt_int _ _ _) => exact I: ty.
Global Hint Extern 1 (wt_int _ _ _) => reflexivity: ty.

Ltac DestructCases :=
  match goal with
  | [H: match match ?x with _ => _ end with _ => _ end = Some _ |- _ ] => destruct x eqn:?; DestructCases
  | [H: match match ?x with _ => _ end with _ => _ end = OK _ |- _ ] => destruct x eqn:?; DestructCases
  | [H: match ?x with _ => _ end = OK _ |- _ ] => destruct x eqn:?; DestructCases
  | [H: match ?x with _ => _ end = Some _ |- _ ] => destruct x eqn:?; DestructCases
  | [H: Some _ = Some _ |- _ ] => inv H; DestructCases
  | [H: None = Some _ |- _ ] => discriminate
  | [H: OK _ = OK _ |- _ ] => inv H; DestructCases
  | [H: Error _ = OK _ |- _ ] => discriminate
  | _ => idtac
  end.

Ltac DestructMatch :=
  match goal with
  | [ |- match match ?x with _ => _ end with _ => _ end ] => destruct x; DestructMatch
  | [ |- match ?x with _ => _ end ] => destruct x; DestructMatch
  | _ => idtac
  end.

Type checking

Definition check_cast (t1 t2: type) : res unit :=
  match classify_cast t1 t2 with
  | cast_case_default => Error (msg "illegal cast")
  | _ => OK tt
  end.

Definition check_bool (t: type) : res unit :=
  match classify_bool t with
  | bool_default => Error (msg "not a boolean")
  | _ => OK tt
  end.

Definition check_literal (v: val) (t: type) : res unit :=
  match v, t with
  | Vint n, Tint I32 sg a => OK tt
  | Vint n, Tpointer t' a => OK tt
  | Vlong n, Tlong sg a => OK tt
  | Vsingle f, Tfloat F32 a => OK tt
  | Vfloat f, Tfloat F64 a => OK tt
  | _, _ => Error (msg "wrong literal")
  end.

Fixpoint check_arguments (el: exprlist) (tyl: list type) : res unit :=
  match el, tyl with
  | Enil, nil => OK tt
  | Enil, _ => Error (msg "not enough arguments")
  | _, nil => if strict then Error (msg "too many arguments") else OK tt
  | Econs e1 el, ty1 :: tyl => do x <- check_cast (typeof e1) ty1; check_arguments el tyl
  end.

Definition check_rval (e: expr) : res unit :=
  match e with
  | Eloc _ _ _ _ | Evar _ _ | Ederef _ _ | Efield _ _ _ =>
      Error (msg "not a r-value")
  | _ =>
      OK tt
  end.

Definition check_lval (e: expr) : res unit :=
  match e with
  | Eloc _ _ _ _ | Evar _ _ | Ederef _ _ | Efield _ _ _ =>
      OK tt
  | _ =>
      Error (msg "not a l-value")
  end.

Fixpoint check_rvals (el: exprlist) : res unit :=
  match el with
  | Enil => OK tt
  | Econs e1 el => do x <- check_rval e1; check_rvals el
  end.


Definition evar (e: typenv) (x: ident) : res expr :=
  match e!.(QualIdent.root x) with
  | Some ty => OK (Evar x ty)
  | None => Error (MSG "unbound variable " :: CTX x :: nil)
  end.

Definition ederef (r: expr) : res expr :=
  do x1 <- check_rval r;
  do ty <- type_deref (typeof r);
  OK (Ederef r ty).

Definition efield (ce: composite_env) (r: expr) (f: ident) : res expr :=
  do x1 <- check_rval r;
  match typeof r with
  | Tstruct id a | Tunion id a =>
      match ce!id with
      | None => Error (MSG "unbound composite " :: CTX id :: nil)
      | Some co =>
          do ty <- type_of_member a f co.(co_members);
          OK (Efield r f ty)
      end
  | _ =>
      Error (MSG "argument of ." :: CTX f :: MSG " is not a struct or union" :: nil)
  end.

Definition econst_int (n: int) (sg: signedness) : expr :=
  (Eval (Vint n) (Tint I32 sg noattr)).

Definition econst_ptr_int (n: int) (ty: type) : expr :=
  (Eval (if Archi.ptr64 then Vlong (Int64.repr (Int.unsigned n)) else Vint n) (Tpointer ty noattr)).

Definition econst_long (n: int64) (sg: signedness) : expr :=
  (Eval (Vlong n) (Tlong sg noattr)).

Definition econst_ptr_long (n: int64) (ty: type) : expr :=
  (Eval (if Archi.ptr64 then Vlong n else Vint (Int64.loword n)) (Tpointer ty noattr)).

Definition econst_float (n: float) : expr :=
  (Eval (Vfloat n) (Tfloat F64 noattr)).

Definition econst_single (n: float32) : expr :=
  (Eval (Vsingle n) (Tfloat F32 noattr)).

Definition evalof (l: expr) : res expr :=
  do x <- check_lval l; OK (Evalof l (typeof l)).

Definition eaddrof (l: expr) : res expr :=
  do x <- check_lval l; OK (Eaddrof l (Tpointer (typeof l) noattr)).

Definition eunop (op: unary_operation) (r: expr) : res expr :=
  do x <- check_rval r;
  do ty <- type_unop op (typeof r);
  OK (Eunop op r ty).

Definition ebinop (op: binary_operation) (r1 r2: expr) : res expr :=
  do x1 <- check_rval r1; do x2 <- check_rval r2;
  do ty <- type_binop op (typeof r1) (typeof r2);
  OK (Ebinop op r1 r2 ty).

Definition ecast (ty: type) (r: expr) : res expr :=
  do x1 <- check_rval r;
  do x2 <- check_cast (typeof r) ty;
  OK (Ecast r ty).

Definition eseqand (r1 r2: expr) : res expr :=
  do x1 <- check_rval r1; do x2 <- check_rval r2;
  do y1 <- check_bool (typeof r1); do y2 <- check_bool (typeof r2);
  OK (Eseqand r1 r2 type_int32s).

Definition eseqor (r1 r2: expr) : res expr :=
  do x1 <- check_rval r1; do x2 <- check_rval r2;
  do y1 <- check_bool (typeof r1); do y2 <- check_bool (typeof r2);
  OK (Eseqor r1 r2 type_int32s).

Definition econdition (r1 r2 r3: expr) : res expr :=
  do x1 <- check_rval r1; do x2 <- check_rval r2; do x3 <- check_rval r3;
  do y1 <- check_bool (typeof r1);
  do ty <- type_conditional (typeof r2) (typeof r3);
  OK (Econdition r1 r2 r3 ty).

Definition econdition' (r1 r2 r3: expr) (ty: type) : res expr :=
  do x1 <- check_rval r1; do x2 <- check_rval r2; do x3 <- check_rval r3;
  do y1 <- check_bool (typeof r1);
  do y2 <- check_cast (typeof r2) ty;
  do y3 <- check_cast (typeof r3) ty;
  OK (Econdition r1 r2 r3 ty).

Definition esizeof (ty: type) : expr :=
  Esizeof ty size_t.

Definition ealignof (ty: type) : expr :=
  Ealignof ty size_t.

Definition eassign (l r: expr) : res expr :=
  do x1 <- check_lval l; do x2 <- check_rval r;
  do y1 <- check_cast (typeof r) (typeof l);
  OK (Eassign l r (typeof l)).

Definition eassignop (op: binary_operation) (l r: expr) : res expr :=
  do x1 <- check_lval l; do x2 <- check_rval r;
  do ty <- type_binop op (typeof l) (typeof r);
  do y1 <- check_cast ty (typeof l);
  OK (Eassignop op l r ty (typeof l)).

Definition epostincrdecr (id: incr_or_decr) (l: expr) : res expr :=
  do x1 <- check_lval l;
  do ty <- type_binop (match id with Incr => Oadd | Decr => Osub end)
                      (typeof l) type_int32s;
  do y1 <- check_cast (incrdecr_type (typeof l)) (typeof l);
  OK (Epostincr id l (typeof l)).

Definition epostincr (l: expr) := epostincrdecr Incr l.
Definition epostdecr (l: expr) := epostincrdecr Decr l.

Definition epreincr (l: expr) := eassignop Oadd l (Eval (Vint Int.one) type_int32s).
Definition epredecr (l: expr) := eassignop Osub l (Eval (Vint Int.one) type_int32s).

Definition ecomma (r1 r2: expr) : res expr :=
  do x1 <- check_rval r1; do x2 <- check_rval r2;
  OK (Ecomma r1 r2 (typeof r2)).

Definition ecall (fn: expr) (args: exprlist) : res expr :=
  do x1 <- check_rval fn; do x2 <- check_rvals args;
  match classify_fun (typeof fn) with
  | fun_case_f tyargs tyres cconv =>
      do y1 <- check_arguments args tyargs;
      OK (Ecall fn args tyres)
  | _ =>
      Error (msg "call: not a function")
  end.

Definition ebuiltin (ef: external_function) (tyargs: list type) (args: exprlist) (tyres: type) : res expr :=
  do x1 <- check_rvals args;
  do x2 <- check_arguments args tyargs;
  if type_eq tyres Tvoid
  && xtype_eq (sig_res (ef_sig ef)) Xvoid
  then OK (Ebuiltin ef tyargs args tyres)
  else Error (msg "builtin: wrong type decoration").

Definition eselection (r1 r2 r3: expr) : res expr :=
  do x1 <- check_rval r1; do x2 <- check_rval r2; do x3 <- check_rval r3;
  do y1 <- check_bool (typeof r1);
  do ty <- type_conditional (typeof r2) (typeof r3);
  OK (Eselection r1 r2 r3 ty).

Definition sdo (a: expr) : res statement :=
  do x <- check_rval a; OK (Sdo a).

Definition sifthenelse (a: expr) (s1 s2: statement) : res statement :=
  do x <- check_rval a; do y <- check_bool (typeof a); OK (Sifthenelse a s1 s2).

Definition swhile (a: expr) (s: statement) : res statement :=
  do x <- check_rval a; do y <- check_bool (typeof a); OK (Swhile a s).

Definition sdowhile (a: expr) (s: statement) : res statement :=
  do x <- check_rval a; do y <- check_bool (typeof a); OK (Sdowhile a s).

Definition sfor (s1: statement) (a: expr) (s2 s3: statement) : res statement :=
  do x <- check_rval a; do y <- check_bool (typeof a); OK (Sfor s1 a s2 s3).

Definition sreturn (rt: type) (a: expr) : res statement :=
  do x <- check_rval a; do y <- check_cast (typeof a) rt;
  OK (Sreturn (Some a)).

Definition sswitch (a: expr) (sl: labeled_statements) : res statement :=
  do x <- check_rval a;
  match typeof a with
  | Tint _ _ _ | Tlong _ _ => OK (Sswitch a sl)
  | _ => Error (msg "wrong type for argument of switch")
  end.


Fixpoint retype_expr (ce: composite_env) (e: typenv) (a: expr) : res expr :=
  match a with
  | Eval (Vint n) (Tint _ sg _) =>
      OK (econst_int n sg)
  | Eval (Vint n) (Tpointer ty _) =>
      OK (econst_ptr_int n ty)
  | Eval (Vlong n) (Tlong sg _) =>
      OK (econst_long n sg)
  | Eval (Vfloat n) _ =>
      OK (econst_float n)
  | Eval (Vsingle n) _ =>
      OK (econst_single n)
  | Eval _ _ =>
      Error (msg "bad literal")
  | Evar x _ =>
      evar e x
  | Efield r f _ =>
      do r' <- retype_expr ce e r; efield ce r' f
  | Evalof l _ =>
      do l' <- retype_expr ce e l; evalof l'
  | Ederef r _ =>
      do r' <- retype_expr ce e r; ederef r'
  | Eaddrof l _ =>
      do l' <- retype_expr ce e l; eaddrof l'
  | Eunop op r _ =>
      do r' <- retype_expr ce e r; eunop op r'
  | Ebinop op r1 r2 _ =>
      do r1' <- retype_expr ce e r1; do r2' <- retype_expr ce e r2; ebinop op r1' r2'
  | Ecast r ty =>
      do r' <- retype_expr ce e r; ecast ty r'
  | Eseqand r1 r2 _ =>
      do r1' <- retype_expr ce e r1; do r2' <- retype_expr ce e r2; eseqand r1' r2'
  | Eseqor r1 r2 _ =>
      do r1' <- retype_expr ce e r1; do r2' <- retype_expr ce e r2; eseqor r1' r2'
  | Econdition r1 r2 r3 _ =>
      do r1' <- retype_expr ce e r1; do r2' <- retype_expr ce e r2; do r3' <- retype_expr ce e r3; econdition r1' r2' r3'
  | Esizeof ty _ =>
      OK (esizeof ty)
  | Ealignof ty _ =>
      OK (ealignof ty)
  | Eassign l r _ =>
      do l' <- retype_expr ce e l; do r' <- retype_expr ce e r; eassign l' r'
  | Eassignop op l r _ _ =>
      do l' <- retype_expr ce e l; do r' <- retype_expr ce e r; eassignop op l' r'
  | Epostincr id l _ =>
      do l' <- retype_expr ce e l; epostincrdecr id l'
  | Ecomma r1 r2 _ =>
      do r1' <- retype_expr ce e r1; do r2' <- retype_expr ce e r2; ecomma r1' r2'
  | Ecall r1 rl _ =>
      do r1' <- retype_expr ce e r1; do rl' <- retype_exprlist ce e rl; ecall r1' rl'
  | Ebuiltin ef tyargs rl tyres =>
      do rl' <- retype_exprlist ce e rl; ebuiltin ef tyargs rl' tyres
  | Eloc _ _ _ _ =>
      Error (msg "Eloc in source")
  | Eparen _ _ _ =>
      Error (msg "Eparen in source")
  end

with retype_exprlist (ce: composite_env) (e: typenv) (al: exprlist) : res exprlist :=
  match al with
  | Enil => OK Enil
  | Econs a1 al =>
      do a1' <- retype_expr ce e a1;
      do al' <- retype_exprlist ce e al;
      do x1 <- check_rval a1';
      OK (Econs a1' al')
  end.

Fixpoint retype_stmt (ce: composite_env) (e: typenv) (rt: type) (s: statement) : res statement :=
  match s with
  | Sskip =>
      OK Sskip
  | Sdo a =>
      do a' <- retype_expr ce e a; sdo a'
  | Ssequence s1 s2 =>
      do s1' <- retype_stmt ce e rt s1; do s2' <- retype_stmt ce e rt s2; OK (Ssequence s1' s2')
  | Sifthenelse a s1 s2 =>
      do a' <- retype_expr ce e a;
      do s1' <- retype_stmt ce e rt s1; do s2' <- retype_stmt ce e rt s2;
      sifthenelse a' s1' s2'
  | Swhile a s =>
      do a' <- retype_expr ce e a;
      do s' <- retype_stmt ce e rt s;
      swhile a' s'
  | Sdowhile a s =>
      do a' <- retype_expr ce e a;
      do s' <- retype_stmt ce e rt s;
      sdowhile a' s'
  | Sfor s1 a s2 s3 =>
      do a' <- retype_expr ce e a;
      do s1' <- retype_stmt ce e rt s1; do s2' <- retype_stmt ce e rt s2; do s3' <- retype_stmt ce e rt s3;
      sfor s1' a' s2' s3'
  | Sbreak =>
      OK Sbreak
  | Scontinue =>
      OK Scontinue
  | Sreturn None =>
      OK (Sreturn None)
  | Sreturn (Some a) =>
      do a' <- retype_expr ce e a;
      sreturn rt a'
  | Sswitch a sl =>
      do a' <- retype_expr ce e a;
      do sl' <- retype_lblstmts ce e rt sl;
      sswitch a' sl'
  | Slabel lbl s =>
      do s' <- retype_stmt ce e rt s; OK (Slabel lbl s')
  | Sgoto lbl =>
      OK (Sgoto lbl)
  end

with retype_lblstmts (ce: composite_env) (e: typenv) (rt: type) (sl: labeled_statements) : res labeled_statements :=
  match sl with
  | LSnil => OK LSnil
  | LScons case s sl =>
      do s' <- retype_stmt ce e rt s; do sl' <- retype_lblstmts ce e rt sl;
      OK (LScons case s' sl')
  end.

Definition retype_function (ce: composite_env) (e: typenv) (f: function) : res function :=
  let e := bind_vars (bind_vars e f.(fn_params)) f.(fn_vars) in
  do s <- retype_stmt ce e f.(fn_return) f.(fn_body);
  OK (mkfunction f.(fn_return)
                 f.(fn_callconv)
                 f.(fn_params)
                 f.(fn_vars)
                 s
                 f.(fn_attr)).

Definition retype_fundef (ce: composite_env) (e: typenv) (fd: fundef) : res fundef :=
  match fd with
  | Internal f => do f' <- retype_function ce e f; OK (Internal f')
  | External ef args res cc =>
      assertion (xtype_eq (ef_sig ef).(sig_res) (rettype_of_type res)); OK fd
  end.

Definition typecheck_program (p: program) : res program :=
  let e := bind_globdef (PTree.empty _) p.(prog_defs) in
  let ce := p.(prog_comp_env) in
  do tp <- transform_partial_program (retype_fundef ce e) p;
  OK {| prog_defs := tp.(AST.prog_defs);
        prog_public := p.(prog_public);
        prog_main := p.(prog_main);
        prog_types := p.(prog_types);
        prog_comp_env := ce;
        prog_comp_env_eq := p.(prog_comp_env_eq) |}.


Lemma check_cast_sound:
  forall t1 t2 x, check_cast t1 t2 = OK x -> wt_cast t1 t2.

Lemma check_bool_sound:
  forall t x, check_bool t = OK x -> wt_bool t.

Global Hint Resolve check_cast_sound check_bool_sound: ty.

Lemma check_arguments_sound:
  forall el tl x, check_arguments el tl = OK x -> wt_arguments el tl.

Lemma check_rval_sound:
  forall a x, check_rval a = OK x -> expr_kind a = RV.

Lemma check_lval_sound:
  forall a x, check_lval a = OK x -> expr_kind a = LV.

Lemma binarith_type_cast:
  forall t1 t2 m t,
  binarith_type t1 t2 m = OK t -> wt_cast t1 t /\ wt_cast t2 t.

Lemma typeconv_cast:
  forall t1 t2, wt_cast (typeconv t1) t2 -> wt_cast t1 t2.

Lemma wt_bool_cast:
  forall ty, wt_bool ty -> wt_cast ty type_bool.

Lemma wt_cast_int:
  forall i1 s1 a1 i2 s2 a2, wt_cast (Tint i1 s1 a1) (Tint i2 s2 a2).
 
Lemma type_combine_cast:
  forall t1 t2 t,
  type_combine t1 t2 = OK t ->
  match t1 with Tarray _ _ _ => False | Tfunction _ _ _ => False | _ => True end ->
  match t2 with Tarray _ _ _ => False | Tfunction _ _ _ => False | _ => True end ->
  wt_cast t1 t /\ wt_cast t2 t.

Lemma type_conditional_cast:
  forall t1 t2 t,
  type_conditional t1 t2 = OK t -> wt_cast t1 t /\ wt_cast t2 t.

Section SOUNDNESS_CONSTRUCTORS.

Variable ce: composite_env.
Variable e: typenv.
Variable rt: type.

Corollary check_rval_wt:
  forall a x, wt_expr ce e a -> check_rval a = OK x -> wt_rvalue ce e a.

Corollary check_lval_wt:
  forall a x, wt_expr ce e a -> check_lval a = OK x -> wt_lvalue ce e a.

Hint Resolve check_rval_wt check_lval_wt: ty.
Hint Extern 1 (wt_expr _ _ _) => (unfold wt_expr; simpl): ty.

Lemma evar_sound:
  forall x a, evar e x = OK a -> wt_expr ce e a.

Lemma ederef_sound:
  forall r a, ederef r = OK a -> wt_expr ce e r -> wt_expr ce e a.

Lemma efield_sound:
  forall r f a, efield ce r f = OK a -> wt_expr ce e r -> wt_expr ce e a.

Lemma econst_int_sound:
  forall n sg, wt_expr ce e (econst_int n sg).

Lemma econst_ptr_int_sound:
  forall n ty, wt_expr ce e (econst_ptr_int n ty).

Lemma econst_long_sound:
  forall n sg, wt_expr ce e (econst_long n sg).

Lemma econst_ptr_long_sound:
  forall n ty, wt_expr ce e (econst_ptr_long n ty).

Lemma econst_float_sound:
  forall n, wt_expr ce e (econst_float n).

Lemma econst_single_sound:
  forall n, wt_expr ce e (econst_single n).

Lemma evalof_sound:
  forall l a, evalof l = OK a -> wt_expr ce e l -> wt_expr ce e a.

Lemma eaddrof_sound:
  forall l a, eaddrof l = OK a -> wt_expr ce e l -> wt_expr ce e a.

Lemma eunop_sound:
  forall op r a, eunop op r = OK a -> wt_expr ce e r -> wt_expr ce e a.

Lemma ebinop_sound:
  forall op r1 r2 a, ebinop op r1 r2 = OK a -> wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e a.

Lemma ecast_sound:
  forall ty r a, ecast ty r = OK a -> wt_expr ce e r -> wt_expr ce e a.

Lemma eseqand_sound:
  forall r1 r2 a, eseqand r1 r2 = OK a -> wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e a.

Lemma eseqor_sound:
  forall r1 r2 a, eseqor r1 r2 = OK a -> wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e a.

Lemma econdition_sound:
  forall r1 r2 r3 a, econdition r1 r2 r3 = OK a ->
  wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e r3 -> wt_expr ce e a.

Lemma econdition'_sound:
  forall r1 r2 r3 ty a, econdition' r1 r2 r3 ty = OK a ->
  wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e r3 -> wt_expr ce e a.

Lemma esizeof_sound:
  forall ty, wt_expr ce e (esizeof ty).

Lemma ealignof_sound:
  forall ty, wt_expr ce e (ealignof ty).

Lemma eassign_sound:
  forall l r a, eassign l r = OK a -> wt_expr ce e l -> wt_expr ce e r -> wt_expr ce e a.

Lemma eassignop_sound:
  forall op l r a, eassignop op l r = OK a -> wt_expr ce e l -> wt_expr ce e r -> wt_expr ce e a.

Lemma epostincrdecr_sound:
  forall id l a, epostincrdecr id l = OK a -> wt_expr ce e l -> wt_expr ce e a.

Lemma ecomma_sound:
  forall r1 r2 a, ecomma r1 r2 = OK a -> wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e a.

Lemma ecall_sound:
  forall fn args a, ecall fn args = OK a -> wt_expr ce e fn -> wt_exprlist ce e args -> wt_expr ce e a.

Lemma ebuiltin_sound:
  forall ef tyargs args tyres a,
  ebuiltin ef tyargs args tyres = OK a -> wt_exprlist ce e args -> wt_expr ce e a.

Lemma eselection_sound:
  forall r1 r2 r3 a, eselection r1 r2 r3 = OK a ->
  wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e r3 -> wt_expr ce e a.

Lemma sdo_sound:
  forall a s, sdo a = OK s -> wt_expr ce e a -> wt_stmt ce e rt s.

Lemma sifthenelse_sound:
  forall a s1 s2 s, sifthenelse a s1 s2 = OK s ->
  wt_expr ce e a -> wt_stmt ce e rt s1 -> wt_stmt ce e rt s2 -> wt_stmt ce e rt s.

Lemma swhile_sound:
  forall a s1 s, swhile a s1 = OK s ->
  wt_expr ce e a -> wt_stmt ce e rt s1 -> wt_stmt ce e rt s.

Lemma sdowhile_sound:
  forall a s1 s, sdowhile a s1 = OK s ->
  wt_expr ce e a -> wt_stmt ce e rt s1 -> wt_stmt ce e rt s.

Lemma sfor_sound:
  forall s1 a s2 s3 s, sfor s1 a s2 s3 = OK s ->
  wt_stmt ce e rt s1 -> wt_expr ce e a -> wt_stmt ce e rt s2 -> wt_stmt ce e rt s3 ->
  wt_stmt ce e rt s.

Lemma sreturn_sound:
  forall a s, sreturn rt a = OK s -> wt_expr ce e a -> wt_stmt ce e rt s.

Lemma sswitch_sound:
  forall a sl s, sswitch a sl = OK s ->
  wt_expr ce e a -> wt_lblstmts ce e rt sl -> wt_stmt ce e rt s.

Lemma retype_expr_sound:
  forall a a', retype_expr ce e a = OK a' -> wt_expr ce e a'
with retype_exprlist_sound:
  forall al al', retype_exprlist ce e al = OK al' -> wt_exprlist ce e al'.

Lemma retype_stmt_sound:
  forall s s', retype_stmt ce e rt s = OK s' -> wt_stmt ce e rt s'
with retype_lblstmts_sound:
  forall sl sl', retype_lblstmts ce e rt sl = OK sl' -> wt_lblstmts ce e rt sl'.

End SOUNDNESS_CONSTRUCTORS.

Lemma retype_function_sound:
  forall ce e f f', retype_function ce e f = OK f' -> wt_function ce e f'.

Lemma retype_fundef_sound:
  forall ce e fd fd', retype_fundef ce e fd = OK fd' -> wt_fundef ce e fd'.

Theorem typecheck_program_sound:
  forall p p', typecheck_program p = OK p' -> wt_program p'.

Subject reduction

Lemma pres_cast_int_int:
  forall sz sg n, wt_int (cast_int_int sz sg n) sz sg.

Lemma wt_val_casted:
  forall v ty, val_casted v ty -> wt_val v ty.

Lemma pres_sem_cast:
  forall m v2 ty2 v1 ty1, wt_val v1 ty1 -> sem_cast v1 ty1 ty2 m = Some v2 -> wt_val v2 ty2.

Lemma pres_sem_binarith:
  forall
    (sem_int: signedness -> int -> int -> option val)
    (sem_long: signedness -> int64 -> int64 -> option val)
    (sem_float: float -> float -> option val)
    (sem_single: float32 -> float32 -> option val)
    v1 ty1 v2 ty2 m v ty msg,
    (forall sg n1 n2,
     match sem_int sg n1 n2 with None | Some (Vint _) | Some Vundef => True | _ => False end) ->
    (forall sg n1 n2,
     match sem_long sg n1 n2 with None | Some (Vlong _) | Some Vundef => True | _ => False end) ->
    (forall n1 n2,
     match sem_float n1 n2 with None | Some (Vfloat _) | Some Vundef => True | _ => False end) ->
    (forall n1 n2,
     match sem_single n1 n2 with None | Some (Vsingle _) | Some Vundef => True | _ => False end) ->
    sem_binarith sem_int sem_long sem_float sem_single v1 ty1 v2 ty2 m = Some v ->
    binarith_type ty1 ty2 msg = OK ty ->
    wt_val v ty.

Lemma pres_sem_binarith_int:
  forall
    (sem_int: signedness -> int -> int -> option val)
    (sem_long: signedness -> int64 -> int64 -> option val)
    v1 ty1 v2 ty2 m v ty msg,
    (forall sg n1 n2,
     match sem_int sg n1 n2 with None | Some (Vint _) | Some Vundef => True | _ => False end) ->
    (forall sg n1 n2,
     match sem_long sg n1 n2 with None | Some (Vlong _) | Some Vundef => True | _ => False end) ->
    sem_binarith sem_int sem_long (fun n1 n2 => None) (fun n1 n2 => None) v1 ty1 v2 ty2 m = Some v ->
    binarith_int_type ty1 ty2 msg = OK ty ->
    wt_val v ty.

Lemma pres_sem_shift:
  forall sem_int sem_long ty1 ty2 m ty v1 v2 v,
  shift_op_type ty1 ty2 m = OK ty ->
  sem_shift sem_int sem_long v1 ty1 v2 ty2 = Some v ->
  wt_val v ty.

Lemma pres_sem_cmp:
  forall ty1 ty2 msg ty c v1 v2 m v,
  comparison_type ty1 ty2 msg = OK ty ->
  sem_cmp c v1 ty1 v2 ty2 m = Some v ->
  wt_val v ty.

Lemma pres_sem_binop:
  forall ce op ty1 ty2 ty v1 v2 v m,
  type_binop op ty1 ty2 = OK ty ->
  sem_binary_operation ce op v1 ty1 v2 ty2 m = Some v ->
  wt_val v1 ty1 -> wt_val v2 ty2 ->
  wt_val v ty.

Lemma pres_sem_unop:
  forall op ty1 ty v1 m v,
  type_unop op ty1 = OK ty ->
  sem_unary_operation op v1 ty1 m = Some v ->
  wt_val v1 ty1 ->
  wt_val v ty.

Lemma wt_load_result:
  forall ty chunk v,
  access_mode ty = By_value chunk ->
  wt_val (Val.load_result chunk v) ty.

Lemma wt_decode_val:
  forall ty chunk vl,
  access_mode ty = By_value chunk ->
  wt_val (decode_val chunk vl) ty.

Remark wt_bitfield_normalize: forall sz sg width sg1 n,
  0 < width <= bitsize_intsize sz ->
  sg1 = (if zlt width (bitsize_intsize sz) then Signed else sg) ->
  wt_int (bitfield_normalize sz sg width n) sz sg1.

Lemma wt_deref_loc:
  forall ge ty m b ofs bf t v,
  deref_loc ge ty m b ofs bf t v ->
  wt_val v ty.

Lemma wt_assign_loc:
  forall ge ty m b ofs bf v t m' v',
  assign_loc ge ty m b ofs bf v t m' v' ->
  wt_val v ty -> wt_val v' ty.

Lemma wt_cast_self:
  forall t1 t2, wt_cast t1 t2 -> wt_cast t2 t2.

Lemma binarith_type_int32s:
  forall ty1 msg ty2,
  binarith_type ty1 type_int32s msg = OK ty2 ->
  ty2 = incrdecr_type ty1.

Lemma type_add_int32s:
  forall ty1 ty2,
  type_binop Oadd ty1 type_int32s = OK ty2 ->
  ty2 = incrdecr_type ty1.

Lemma type_sub_int32s:
  forall ty1 ty2,
  type_binop Osub ty1 type_int32s = OK ty2 ->
  ty2 = incrdecr_type ty1.

Lemma has_rettype_wt_val:
  forall v ty,
  Val.has_rettype v (rettype_of_type ty) -> wt_val v ty.

Lemma wt_rred:
  forall ge tenv a m t a' m',
  rred ge a m t a' m' -> wt_rvalue ge tenv a -> wt_rvalue ge tenv a'.

Lemma wt_lred:
  forall tenv ge e a m a' m',
  lred ge e a m a' m' -> wt_lvalue ge tenv a -> wt_lvalue ge tenv a'.

Lemma rred_same_type:
  forall ge a m t a' m',
  rred ge a m t a' m' -> typeof a' = typeof a.

Lemma lred_same_type:
  forall ge e a m a' m',
  lred ge e a m a' m' -> typeof a' = typeof a.

Section WT_CONTEXT.

Variable cenv: composite_env.
Variable tenv: typenv.
Variable a a': expr.
Hypothesis SAMETY: typeof a' = typeof a.

Lemma wt_subexpr:
  forall from to C,
  context from to C ->
  wt_expr_kind cenv tenv to (C a) ->
  wt_expr_kind cenv tenv from a
with wt_subexprlist:
  forall from C,
  contextlist from C ->
  wt_exprlist cenv tenv (C a) ->
  wt_expr_kind cenv tenv from a.

Lemma typeof_context:
  forall from to C, context from to C -> typeof (C a') = typeof (C a).

Lemma wt_arguments_context:
  forall k C, contextlist k C ->
  forall tyl, wt_arguments (C a) tyl -> wt_arguments (C a') tyl.

Lemma wt_context:
  forall from to C,
  context from to C ->
  wt_expr_kind cenv tenv to (C a) ->
  wt_expr_kind cenv tenv from a' ->
  wt_expr_kind cenv tenv to (C a')
with wt_contextlist:
  forall from C,
  contextlist from C ->
  wt_exprlist cenv tenv (C a) ->
  wt_expr_kind cenv tenv from a' ->
  wt_exprlist cenv tenv (C a').

End WT_CONTEXT.

Section WT_SWITCH.

Lemma wt_select_switch:
  forall n ce e rt sl,
  wt_lblstmts ce e rt sl -> wt_lblstmts ce e rt (select_switch n sl).

Lemma wt_seq_of_ls:
  forall ce e rt sl,
  wt_lblstmts ce e rt sl -> wt_stmt ce e rt (seq_of_labeled_statement sl).

End WT_SWITCH.

Section PRESERVATION.

Variable prog: program.
Hypothesis WTPROG: wt_program prog.
Let ge := globalenv prog.
Let gtenv := bind_globdef (PTree.empty _) prog.(prog_defs).

Inductive wt_expr_cont: typenv -> function -> cont -> Prop :=
  | wt_Kdo: forall te f k,
      wt_stmt_cont te f k ->
      wt_expr_cont te f (Kdo k)
  | wt_Kifthenelse: forall te f s1 s2 k,
      wt_stmt_cont te f k ->
      wt_stmt ge te f.(fn_return) s1 -> wt_stmt ge te f.(fn_return) s2 ->
      wt_expr_cont te f (Kifthenelse s1 s2 k)
  | wt_Kwhile1: forall te f r s k,
      wt_stmt_cont te f k ->
      wt_rvalue ge te r -> wt_stmt ge te f.(fn_return) s -> wt_bool (typeof r) ->
      wt_expr_cont te f (Kwhile1 r s k)
  | wt_Kdowhile2: forall te f r s k,
      wt_stmt_cont te f k ->
      wt_rvalue ge te r -> wt_stmt ge te f.(fn_return) s -> wt_bool (typeof r) ->
      wt_expr_cont te f (Kdowhile2 r s k)
  | wt_Kfor2: forall te f r s2 s3 k,
      wt_stmt_cont te f k ->
      wt_rvalue ge te r -> wt_stmt ge te f.(fn_return) s2 -> wt_stmt ge te f.(fn_return) s3 ->
      classify_bool (typeof r) <> bool_default ->
      wt_expr_cont te f (Kfor2 r s2 s3 k)
  | wt_Kswitch1: forall te f ls k,
      wt_stmt_cont te f k ->
      wt_lblstmts ge te f.(fn_return) ls ->
      wt_expr_cont te f (Kswitch1 ls k)
  | wt_Kreturn: forall te f k,
      wt_stmt_cont te f k ->
      wt_expr_cont te f (Kreturn k)

with wt_stmt_cont: typenv -> function -> cont -> Prop :=
  | wt_Kseq: forall te f s k,
      wt_stmt_cont te f k ->
      wt_stmt ge te f.(fn_return) s ->
      wt_stmt_cont te f (Kseq s k)
  | wt_Kwhile2: forall te f r s k,
      wt_stmt_cont te f k ->
      wt_rvalue ge te r -> wt_stmt ge te f.(fn_return) s -> wt_bool (typeof r) ->
      wt_stmt_cont te f (Kwhile2 r s k)
  | wt_Kdowhile1: forall te f r s k,
      wt_stmt_cont te f k ->
      wt_rvalue ge te r -> wt_stmt ge te f.(fn_return) s -> wt_bool (typeof r) ->
      wt_stmt_cont te f (Kdowhile1 r s k)
  | wt_Kfor3: forall te f r s2 s3 k,
      wt_stmt_cont te f k ->
      wt_rvalue ge te r -> wt_stmt ge te f.(fn_return) s2 -> wt_stmt ge te f.(fn_return) s3 ->
      wt_bool (typeof r) ->
      wt_stmt_cont te f (Kfor3 r s2 s3 k)
  | wt_Kfor4: forall te f r s2 s3 k,
      wt_stmt_cont te f k ->
      wt_rvalue ge te r -> wt_stmt ge te f.(fn_return) s2 -> wt_stmt ge te f.(fn_return) s3 ->
      wt_bool (typeof r) ->
      wt_stmt_cont te f (Kfor4 r s2 s3 k)
  | wt_Kswitch2: forall te f k,
      wt_stmt_cont te f k ->
      wt_stmt_cont te f (Kswitch2 k)
  | wt_Kstop': forall te f,
      wt_stmt_cont te f Kstop
  | wt_Kcall': forall te f f' e C ty k,
      wt_call_cont (Kcall f' e C ty k) ty ->
      ty = f.(fn_return) ->
      wt_stmt_cont te f (Kcall f' e C ty k)

with wt_call_cont: cont -> type -> Prop :=
  | wt_Kstop: forall ty,
      wt_call_cont Kstop ty
  | wt_Kcall: forall te f e C ty k,
      wt_expr_cont te f k ->
      wt_stmt ge te f.(fn_return) f.(fn_body) ->
      (forall v, wt_val v ty -> wt_rvalue ge te (C (Eval v ty))) ->
      wt_call_cont (Kcall f e C ty k) ty.

Lemma is_wt_call_cont:
  forall te f k,
  is_call_cont k -> wt_stmt_cont te f k -> wt_call_cont k f.(fn_return).

Lemma wt_call_cont_stmt_cont:
  forall te f k, wt_call_cont k f.(fn_return) -> wt_stmt_cont te f k.

Lemma call_cont_wt:
  forall e f k, wt_stmt_cont e f k -> wt_call_cont (call_cont k) f.(fn_return).

Lemma call_cont_wt':
  forall e f k, wt_stmt_cont e f k -> wt_stmt_cont e f (call_cont k).

Definition fundef_return (fd: fundef) : type :=
  match fd with
  | Internal f => f.(fn_return)
  | External ef targs tres cc => tres
  end.

Lemma wt_find_funct:
  forall v fd, Genv.find_funct ge v = Some fd -> wt_fundef ge gtenv fd.

Inductive wt_state: state -> Prop :=
  | wt_stmt_state: forall f s k e m te
        (WTK: wt_stmt_cont te f k)
        (WTB: wt_stmt ge te f.(fn_return) f.(fn_body))
        (WTS: wt_stmt ge te f.(fn_return) s),
      wt_state (State f s k e m)
  | wt_expr_state: forall f r k e m te
        (WTK: wt_expr_cont te f k)
        (WTB: wt_stmt ge te f.(fn_return) f.(fn_body))
        (WTE: wt_rvalue ge te r),
      wt_state (ExprState f r k e m)
  | wt_call_state: forall b fd vargs k m
        (WTK: wt_call_cont k (fundef_return fd))
        (WTFD: wt_fundef ge gtenv fd)
        (FIND: Genv.find_funct ge b = Some fd),
      wt_state (Callstate fd vargs k m)
  | wt_return_state: forall v k m ty
        (WTK: wt_call_cont k ty)
        (VAL: wt_val v ty),
      wt_state (Returnstate v k m)
  | wt_stuck_state:
      wt_state Stuckstate.

Hint Constructors wt_expr_cont wt_stmt_cont wt_stmt wt_state: ty.

Section WT_FIND_LABEL.

Scheme wt_stmt_ind2 := Minimality for wt_stmt Sort Prop
  with wt_lblstmts2_ind2 := Minimality for wt_lblstmts Sort Prop.

Lemma wt_find_label:
  forall lbl e f s, wt_stmt ge e f.(fn_return) s ->
  forall k s' k',
  find_label lbl s k = Some (s', k') ->
  wt_stmt_cont e f k ->
  wt_stmt ge e f.(fn_return) s' /\ wt_stmt_cont e f k'.

End WT_FIND_LABEL.

Lemma preservation_estep:
  forall S t S', estep ge S t S' -> wt_state S -> wt_state S'.

Lemma preservation_sstep:
  forall S t S', sstep ge S t S' -> wt_state S -> wt_state S'.

Theorem preservation:
  forall S t S', step ge S t S' -> wt_state S -> wt_state S'.

Theorem wt_initial_state:
  forall S, initial_state prog S -> wt_state S.

End PRESERVATION.

Additional type-related results

Lemma sem_cast_already_typed: forall v t1 t2 m,
  wt_val v t2 ->
  sem_cast v t1 t2 m = Some v \/ sem_cast v t1 t2 m = None.

Corollary sem_cast_already_typed_idem: forall v t1 t2 m v',
  sem_cast v t1 t2 m = Some v' -> wt_val v t2 -> v' = v.