From 67b13ecb9cfd2511c1db62a6cc38cf796cfb2a14 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 31 Dec 2014 17:14:28 +0100 Subject: Add a type system for CompCert C and type-checking constructor functions. Use these constructor functions in C2C to rely less on the types produced by the unverified elaborator. --- cfrontend/Ctyping.v | 1999 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1999 insertions(+) create mode 100644 cfrontend/Ctyping.v (limited to 'cfrontend/Ctyping.v') diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v new file mode 100644 index 00000000..43d34007 --- /dev/null +++ b/cfrontend/Ctyping.v @@ -0,0 +1,1999 @@ +(* *********************************************************************) +(* *) +(* 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 GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Typing rules and type-checking for the Compcert C language *) + +Require Import Coqlib. +Require Import String. +Require Import Maps. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Events. +Require Import AST. +Require Import Ctypes. +Require Import Cop. +Require Import Csyntax. +Require Import Csem. +Require Import Errors. + +Local Open Scope error_monad_scope. + +Definition strict := false. +Opaque strict. + +(** * Operations over types *) + +(** The type of a member of a composite (struct or union). + The "volatile" attribute carried by the composite propagates + to the type of the member, but not the "alignas" attribute. *) + +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). + +(** Type-checking of arithmetic and logical operators *) + +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 + | 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 ty1 ty2 => + if type_eq (remove_attributes ty1) (remove_attributes ty2) + then OK (Tint I32 Signed noattr) + else Error (msg "operator - : incompatible pointer types") +*) + | sub_case_pp ty => OK (Tint I32 Signed noattr) + | 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 is_void (ty: type) : bool := + match ty with Tvoid => true | _ => false end. + +Definition type_join (ty1 ty2: type) : res type := + match typeconv ty1, typeconv ty2 with + | (Tint _ _ _ | Tfloat _ _), (Tint _ _ _ | Tfloat _ _) => + binarith_type ty1 ty2 "conditional expression" + | Tpointer t1 a1, Tpointer t2 a2 => + OK (Tpointer (if is_void t1 || is_void t2 then Tvoid else t1) noattr) + | Tpointer t1 a1, Tint _ _ _ => + OK (Tpointer t1 noattr) + | Tint _ _ _, Tpointer t2 a2 => + OK (Tpointer t2 noattr) + | Tvoid, Tvoid => + OK Tvoid + | Tstruct id1 a1, Tstruct id2 a2 => + if ident_eq id1 id2 + then OK (Tstruct id1 noattr) + else Error (msg "conditional expression") + | Tunion id1 a1, Tunion id2 a2 => + if ident_eq id1 id2 + then OK (Tunion id1 noattr) + else Error (msg "conditional expression") + | _, _ => + Error (msg "conditional expression") + end. + +(** * Specification of the type system *) + +(** Type environments map identifiers to their types. *) + +Definition typenv := PTree.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, _ => Int.zero_ext 8 n = n + | 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, + 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_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, + wt_val (Vint 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 -> typelist -> Prop := + | wt_arg_nil: + wt_arguments Enil Tnil + | wt_arg_cons: forall a al ty tyl, + wt_cast (typeof a) ty -> + wt_arguments al tyl -> + wt_arguments (Econs a al) (Tcons ty tyl) + | wt_arg_extra: forall a al, (**r tolerance for varargs *) + strict = false -> + wt_arguments (Econs a al) Tnil. + +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 (Tint I32 Unsigned noattr)) + | wt_Ealignof: forall ty, + wt_rvalue (Ealignof ty (Tint I32 Unsigned noattr)) + | 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, + wt_exprlist rargs -> + wt_arguments rargs tyargs -> + (* This is specialized to builtins returning void, the only + case generated by C2C. *) + sig_res (ef_sig ef) = None -> + wt_rvalue (Ebuiltin ef tyargs rargs Tvoid) + | 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 ty, + wt_lvalue (Eloc b ofs ty) + | wt_Evar: forall x ty, + e!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 (PTree.set 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 (ident * globdef fundef type)) : typenv := + match l with + | nil => e + | (id, Gfun fd) :: l => bind_globdef (PTree.set id (type_of_fundef fd) e) l + | (id, Gvar v) :: l => bind_globdef (PTree.set id v.(gvar_info) e) l + end. + +Inductive wt_program : program -> Prop := + | wt_program_intro: forall p, + let e := bind_globdef (PTree.empty _) p.(prog_defs) in + (forall id f, In (id, Gfun (Internal f)) p.(prog_defs) -> + wt_function p.(prog_comp_env) e f) -> + wt_program p. + +Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty. +Hint Extern 1 (wt_int _ _ _) => exact I: ty. +Hint Extern 1 (wt_int _ _ _) => reflexivity: ty. + +Ltac DestructCases := + match goal with + | [H: match match ?x with _ => _ end with _ => _ end = Some _ |- _ ] => destruct x; DestructCases + | [H: match match ?x with _ => _ end with _ => _ end = OK _ |- _ ] => destruct x; DestructCases + | [H: match ?x with _ => _ end = OK _ |- _ ] => destruct x; DestructCases + | [H: match ?x with _ => _ end = Some _ |- _ ] => destruct x; DestructCases + | [H: match ?x with _ => _ end = OK _ |- _ ] => destruct x; 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: typelist) : res unit := + match el, tyl with + | Enil, Tnil => OK tt + | Enil, _ => Error (msg "not enough arguments") + | _, Tnil => if strict then Error (msg "too many arguments") else OK tt + | Econs e1 el, Tcons 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. + +(** Type-checking of expressions is presented as smart constructors + that check type constraints and build the expression with the correct + type annotation. *) + +Definition evar (e: typenv) (x: ident) : res expr := + match e!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 (Vint n) (Tpointer ty noattr)). + +Definition econst_long (n: int64) (sg: signedness) : expr := + (Eval (Vlong n) (Tlong sg 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_join (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 (Tint I32 Unsigned noattr). + +Definition ealignof (ty: type) : expr := + Ealignof ty (Tint I32 Unsigned noattr). + +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: typelist) (args: exprlist) (tyres: type) : res expr := + do x1 <- check_rvals args; + do x2 <- check_arguments args tyargs; + if type_eq tyres Tvoid + && opt_typ_eq (sig_res (ef_sig ef)) None + then OK (Ebuiltin ef tyargs args tyres) + else Error (msg "builtin: wrong type decoration"). + +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. + +(** Using the smart constructors, we define a type checker that rebuilds + a correctly-type-annotated program. *) + +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). + +(** Soundness of the smart constructors. *) + +Lemma check_cast_sound: + forall t1 t2 x, check_cast t1 t2 = OK x -> wt_cast t1 t2. +Proof. + unfold check_cast, wt_cast; intros. + destruct (classify_cast t1 t2); congruence. +Qed. + +Lemma check_bool_sound: + forall t x, check_bool t = OK x -> wt_bool t. +Proof. + unfold check_bool, wt_bool; intros. + destruct (classify_bool t); congruence. +Qed. + +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. +Proof. + intros el tl; revert tl el. + induction tl; destruct el; simpl; intros; try discriminate. + constructor. + destruct strict eqn:S; try discriminate. constructor; auto. + monadInv H. constructor; eauto with ty. +Qed. + +Lemma check_rval_sound: + forall a x, check_rval a = OK x -> expr_kind a = RV. +Proof. + unfold check_rval; intros. destruct a; reflexivity || discriminate. +Qed. + +Lemma check_lval_sound: + forall a x, check_lval a = OK x -> expr_kind a = LV. +Proof. + unfold check_lval; intros. destruct a; reflexivity || discriminate. +Qed. + +Lemma binarith_type_cast: + forall t1 t2 m t, + binarith_type t1 t2 m = OK t -> wt_cast t1 t /\ wt_cast t2 t. +Proof. + unfold wt_cast, binarith_type, classify_binarith; intros; DestructCases; + simpl; split; try congruence. destruct f; congruence. +Qed. + +Lemma typeconv_cast: + forall t1 t2, wt_cast (typeconv t1) t2 -> wt_cast t1 t2. +Proof. + unfold typeconv, wt_cast; intros. destruct t1; auto. + assert (classify_cast (Tint I32 Signed a) t2 <> cast_case_default -> + classify_cast (Tint i s a) t2 <> cast_case_default). + { + unfold classify_cast. destruct t2; try congruence. destruct f; congruence. + } + destruct i; auto. +Qed. + +Lemma type_join_cast: + forall t1 t2 t, + type_join t1 t2 = OK t -> wt_cast t1 t /\ wt_cast t2 t. +Proof. + intros. unfold type_join in H. + destruct (typeconv t1) eqn:T1; try discriminate; + destruct (typeconv t2) eqn:T2; inv H. +- unfold wt_cast; simpl; split; congruence. +- eapply binarith_type_cast; eauto. +- eapply binarith_type_cast; eauto. +- split; apply typeconv_cast; unfold wt_cast. + rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. +- eapply binarith_type_cast; eauto. +- eapply binarith_type_cast; eauto. +- split; apply typeconv_cast; unfold wt_cast. + rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. +- split; apply typeconv_cast; unfold wt_cast. + rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. +- destruct (ident_eq i i0); inv H1. + split; apply typeconv_cast; unfold wt_cast. + rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. +- destruct (ident_eq i i0); inv H1. + split; apply typeconv_cast; unfold wt_cast. + rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. +Qed. + +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. +Proof. + unfold wt_expr; intros. erewrite check_rval_sound in H by eauto. auto. +Qed. + +Corollary check_lval_wt: + forall a x, wt_expr ce e a -> check_lval a = OK x -> wt_lvalue ce e a. +Proof. + unfold wt_expr; intros. erewrite check_lval_sound in H by eauto. auto. +Qed. + +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. +Proof. + unfold evar; intros. destruct (e!x) as [ty|] eqn:E; inv H. eauto with ty. +Qed. + +Lemma ederef_sound: + forall r a, ederef r = OK a -> wt_expr ce e r -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +Lemma efield_sound: + forall r f a, efield ce r f = OK a -> wt_expr ce e r -> wt_expr ce e a. +Proof. + intros. monadInv H. + destruct (typeof r) eqn:TR; try discriminate; + destruct (ce!i) as [co|] eqn:CE; monadInv EQ0; eauto with ty. +Qed. + +Lemma econst_int_sound: + forall n sg, wt_expr ce e (econst_int n sg). +Proof. + unfold econst_int; auto with ty. +Qed. + +Lemma econst_ptr_int_sound: + forall n ty, wt_expr ce e (econst_ptr_int n ty). +Proof. + unfold econst_ptr_int; auto with ty. +Qed. + +Lemma econst_long_sound: + forall n sg, wt_expr ce e (econst_long n sg). +Proof. + unfold econst_long; auto with ty. +Qed. + +Lemma econst_float_sound: + forall n, wt_expr ce e (econst_float n). +Proof. + unfold econst_float; auto with ty. +Qed. + +Lemma econst_single_sound: + forall n, wt_expr ce e (econst_single n). +Proof. + unfold econst_single; auto with ty. +Qed. + +Lemma evalof_sound: + forall l a, evalof l = OK a -> wt_expr ce e l -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +Lemma eaddrof_sound: + forall l a, eaddrof l = OK a -> wt_expr ce e l -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +Lemma eunop_sound: + forall op r a, eunop op r = OK a -> wt_expr ce e r -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +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. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +Lemma ecast_sound: + forall ty r a, ecast ty r = OK a -> wt_expr ce e r -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +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. +Proof. + intros. monadInv H. eauto 10 with ty. +Qed. + +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. +Proof. + intros. monadInv H. eauto 10 with ty. +Qed. + +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. +Proof. + intros. monadInv H. apply type_join_cast in EQ3. destruct EQ3. eauto 10 with ty. +Qed. + +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. +Proof. + intros. monadInv H. eauto 10 with ty. +Qed. + +Lemma esizeof_sound: + forall ty, wt_expr ce e (esizeof ty). +Proof. + unfold esizeof; auto with ty. +Qed. + +Lemma ealignof_sound: + forall ty, wt_expr ce e (ealignof ty). +Proof. + unfold ealignof; auto with ty. +Qed. + +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. +Proof. + intros. monadInv H. eauto 10 with ty. +Qed. + +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. +Proof. + intros. monadInv H. eauto 10 with ty. +Qed. + +Lemma epostincrdecr_sound: + forall id l a, epostincrdecr id l = OK a -> wt_expr ce e l -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto 10 with ty. +Qed. + +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. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +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. +Proof. + intros. monadInv H. + destruct (classify_fun (typeof fn)) eqn:CF; monadInv EQ2. + econstructor; eauto with ty. eapply check_arguments_sound; eauto. +Qed. + +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. +Proof. + intros. monadInv H. + destruct (type_eq tyres Tvoid); simpl in EQ2; try discriminate. + destruct (opt_typ_eq (sig_res (ef_sig ef)) None); inv EQ2. + econstructor; eauto. eapply check_arguments_sound; eauto. +Qed. + +Lemma sdo_sound: + forall a s, sdo a = OK s -> wt_expr ce e a -> wt_stmt ce e rt s. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +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. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +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. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +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. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +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. +Proof. + intros. monadInv H. eauto 10 with ty. +Qed. + +Lemma sreturn_sound: + forall a s, sreturn rt a = OK s -> wt_expr ce e a -> wt_stmt ce e rt s. +Proof. + intros. monadInv H; eauto with ty. +Qed. + +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. +Proof. + intros. monadInv H. destruct (typeof a) eqn:TA; inv EQ0. + eauto with ty. + eapply wt_Sswitch with (sz := I32); eauto with ty. +Qed. + +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'. +Proof. +- destruct a; simpl; intros a' RT; try (monadInv RT). ++ destruct v; try discriminate. + destruct ty; inv RT. apply econst_int_sound. apply econst_ptr_int_sound. + destruct ty; inv RT. apply econst_long_sound. + inv RT. apply econst_float_sound. + inv RT. apply econst_single_sound. ++ eapply evar_sound; eauto. ++ eapply efield_sound; eauto. ++ eapply evalof_sound; eauto. ++ eapply ederef_sound; eauto. ++ eapply eaddrof_sound; eauto. ++ eapply eunop_sound; eauto. ++ eapply ebinop_sound; eauto. ++ eapply ecast_sound; eauto. ++ eapply eseqand_sound; eauto. ++ eapply eseqor_sound; eauto. ++ eapply econdition_sound; eauto. ++ apply esizeof_sound. ++ apply ealignof_sound. ++ eapply eassign_sound; eauto. ++ eapply eassignop_sound; eauto. ++ eapply epostincrdecr_sound; eauto. ++ eapply ecomma_sound; eauto. ++ eapply ecall_sound; eauto. ++ eapply ebuiltin_sound; eauto. +- destruct al; simpl; intros al' RT; monadInv RT. ++ constructor. ++ constructor; eauto with ty. +Qed. + +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'. +Proof. +- destruct s; simpl; intros s' RT; try (monadInv RT). ++ constructor. ++ eapply sdo_sound; eauto using retype_expr_sound. ++ constructor; eauto. ++ eapply sifthenelse_sound; eauto using retype_expr_sound. ++ eapply swhile_sound; eauto using retype_expr_sound. ++ eapply sdowhile_sound; eauto using retype_expr_sound. ++ eapply sfor_sound; eauto using retype_expr_sound. ++ constructor. ++ constructor. ++ destruct o; monadInv RT. eapply sreturn_sound; eauto using retype_expr_sound. constructor. ++ eapply sswitch_sound; eauto using retype_expr_sound. ++ constructor; eauto. ++ constructor. +- destruct sl; simpl; intros sl' RT; monadInv RT. ++ constructor. ++ constructor; eauto. +Qed. + +End SOUNDNESS_CONSTRUCTORS. + +Lemma retype_function_sound: + forall ce e f f', retype_function ce e f = OK f' -> wt_function ce e f'. +Proof. + intros. monadInv H. constructor; simpl. eapply retype_stmt_sound; eauto. +Qed. + +(** * Subject reduction *) + +(** We show that reductions preserve well-typedness *) + +Lemma pres_cast_int_int: + forall sz sg n, wt_int (cast_int_int sz sg n) sz sg. +Proof. + intros. unfold cast_int_int. destruct sz; simpl. +- destruct sg. apply Int.sign_ext_idem; omega. apply Int.zero_ext_idem; omega. +- destruct sg. apply Int.sign_ext_idem; omega. apply Int.zero_ext_idem; omega. +- auto. +- destruct (Int.eq n Int.zero); auto. +Qed. + +Hint Resolve pres_cast_int_int: ty. + +Lemma pres_sem_cast: + forall v2 ty2 v1 ty1, wt_val v1 ty1 -> sem_cast v1 ty1 ty2 = Some v2 -> wt_val v2 ty2. +Proof. + unfold sem_cast, classify_cast; induction 1; simpl; intros; DestructCases; auto with ty. +- constructor. apply (pres_cast_int_int I8 s). +- constructor. apply (pres_cast_int_int I16 s). +- destruct (Int.eq n Int.zero); auto with ty. +- constructor. apply (pres_cast_int_int I8 s). +- constructor. apply (pres_cast_int_int I16 s). +- destruct (Int64.eq n Int64.zero); auto with ty. +- constructor. apply (pres_cast_int_int I8 s). +- constructor. apply (pres_cast_int_int I16 s). +- destruct (Float.cmp Ceq f Float.zero); auto with ty. +- constructor. apply (pres_cast_int_int I8 s). +- constructor. apply (pres_cast_int_int I16 s). +- destruct (Float32.cmp Ceq f Float32.zero); auto with ty. +- destruct (Int.eq n Int.zero); auto with ty. +Qed. + +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 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 = Some v -> + binarith_type ty1 ty2 msg = OK ty -> + wt_val v ty. +Proof with (try discriminate). + intros. unfold sem_binarith, binarith_type in *. + set (ty' := Cop.binarith_type (classify_binarith ty1 ty2)) in *. + destruct (sem_cast v1 ty1 ty') as [v1'|] eqn:CAST1... + destruct (sem_cast v2 ty2 ty') as [v2'|] eqn:CAST2... + DestructCases. +- specialize (H s i i0). rewrite H3 in H. + destruct v; auto with ty; contradiction. +- specialize (H0 s i i0). rewrite H3 in H0. + destruct v; auto with ty; contradiction. +- specialize (H1 f f0). rewrite H3 in H1. + destruct v; auto with ty; contradiction. +- specialize (H2 f f0). rewrite H3 in H2. + destruct v; auto with ty; contradiction. +Qed. + +Lemma pres_sem_binarith_int: + forall + (sem_int: signedness -> int -> int -> option val) + (sem_long: signedness -> int64 -> int64 -> option val) + v1 ty1 v2 ty2 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 = Some v -> + binarith_int_type ty1 ty2 msg = OK ty -> + wt_val v ty. +Proof. + intros. eapply pres_sem_binarith with (msg := msg); eauto. + simpl; auto. simpl; auto. + unfold binarith_int_type, binarith_type in *. + destruct (classify_binarith ty1 ty2); congruence. +Qed. + +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. +Proof. + intros. unfold shift_op_type, sem_shift in *. DestructCases; auto with ty. +Qed. + +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. +Proof with (try discriminate). + unfold comparison_type, sem_cmp; intros. + assert (X: forall b, wt_val (Val.of_bool b) (Tint I32 Signed noattr)). + { + intros b; destruct b; constructor; exact I. + } + assert (Y: forall ob, option_map Val.of_bool ob = Some v -> wt_val v (Tint I32 Signed noattr)). + { + intros ob EQ. destruct ob as [b|]; inv EQ. eauto. + } + destruct (classify_cmp ty1 ty2). +- inv H; eauto. +- DestructCases; eauto. +- DestructCases; eauto. +- unfold sem_binarith in H0. + set (ty' := Cop.binarith_type (classify_binarith ty1 ty2)) in *. + destruct (sem_cast v1 ty1 ty') as [v1'|]... + destruct (sem_cast v2 ty2 ty') as [v2'|]... + DestructCases; auto. +Qed. + +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. +Proof. + intros until m; intros TY SEM WT1 WT2. + destruct op; simpl in TY; simpl in SEM. +- (* add *) + unfold sem_add in SEM; DestructCases; auto with ty. + eapply pres_sem_binarith; eauto; intros; exact I. +- (* sub *) + unfold sem_sub in SEM; DestructCases; auto with ty. + eapply pres_sem_binarith; eauto; intros; exact I. +- (* mul *) + unfold sem_mul in SEM. eapply pres_sem_binarith; eauto; intros; exact I. +- (* div *) + unfold sem_div in SEM. eapply pres_sem_binarith; eauto; intros. + simpl; DestructMatch; auto. + simpl; DestructMatch; auto. + simpl; DestructMatch; auto. + simpl; DestructMatch; auto. +- (* mod *) + unfold sem_mod in SEM. eapply pres_sem_binarith_int; eauto; intros. + simpl; DestructMatch; auto. + simpl; DestructMatch; auto. +- (* and *) + unfold sem_and in SEM. eapply pres_sem_binarith_int; eauto; intros; exact I. +- (* or *) + unfold sem_or in SEM. eapply pres_sem_binarith_int; eauto; intros; exact I. +- (* xor *) + unfold sem_xor in SEM. eapply pres_sem_binarith_int; eauto; intros; exact I. +- (* shl *) + unfold sem_shl in SEM. eapply pres_sem_shift; eauto. +- (* shr *) + unfold sem_shr in SEM. eapply pres_sem_shift; eauto. +- (* comparisons *) + eapply pres_sem_cmp; eauto. +- eapply pres_sem_cmp; eauto. +- eapply pres_sem_cmp; eauto. +- eapply pres_sem_cmp; eauto. +- eapply pres_sem_cmp; eauto. +- eapply pres_sem_cmp; eauto. +Qed. + +Lemma pres_sem_unop: + forall op ty1 ty v1 v, + type_unop op ty1 = OK ty -> + sem_unary_operation op v1 ty1 = Some v -> + wt_val v1 ty1 -> + wt_val v ty. +Proof. + intros until v; intros TY SEM WT1. + destruct op; simpl in TY; simpl in SEM. +- (* notbool *) + unfold sem_notbool in SEM; DestructCases. + destruct (Int.eq i Int.zero); constructor; auto with ty. + destruct (Float.cmp Ceq f Float.zero); constructor; auto with ty. + destruct (Float32.cmp Ceq f Float32.zero); constructor; auto with ty. + destruct (Int.eq i Int.zero); constructor; auto with ty. + constructor; auto with ty. + destruct (Int64.eq i Int64.zero); constructor; auto with ty. +- (* notint *) + unfold sem_notint in SEM; DestructCases; auto with ty. +- (* neg *) + unfold sem_neg in SEM; DestructCases; auto with ty. +- (* absfloat *) + unfold sem_absfloat in SEM; DestructCases; auto with ty. +Qed. + +Lemma wt_load_result: + forall ty chunk v, + access_mode ty = By_value chunk -> + wt_val (Val.load_result chunk v) ty. +Proof. + intros until v; intros AC. destruct ty; simpl in AC; try discriminate. + destruct i; [destruct s|destruct s|idtac|idtac]; inv AC; simpl; destruct v; auto with ty. + constructor; red. apply Int.sign_ext_idem; omega. + constructor; red. apply Int.zero_ext_idem; omega. + constructor; red. apply Int.sign_ext_idem; omega. + constructor; red. apply Int.zero_ext_idem; omega. + constructor; red. apply Int.zero_ext_idem; omega. + inv AC; simpl; destruct v; auto with ty. + destruct f; inv AC; simpl; destruct v; auto with ty. + inv AC; simpl; destruct v; auto with ty. +Qed. + +Lemma wt_decode_val: + forall ty chunk vl, + access_mode ty = By_value chunk -> + wt_val (decode_val chunk vl) ty. +Proof. + intros until vl; intros ACC. + destruct ty; simpl in ACC; try discriminate. +- destruct i; [destruct s|destruct s|idtac|idtac]; inv ACC; unfold decode_val; + destruct (proj_bytes vl); auto with ty. + constructor; red. apply Int.sign_ext_idem; omega. + constructor; red. apply Int.zero_ext_idem; omega. + constructor; red. apply Int.sign_ext_idem; omega. + constructor; red. apply Int.zero_ext_idem; omega. + apply wt_load_result. auto. + constructor; red. apply Int.zero_ext_idem; omega. +- inv ACC. unfold decode_val. destruct (proj_bytes vl); auto with ty. +- destruct f; inv ACC; unfold decode_val; destruct (proj_bytes vl); auto with ty. +- inv ACC. unfold decode_val. destruct (proj_bytes vl); auto with ty. + apply wt_load_result. auto. +Qed. + +Lemma wt_deref_loc: + forall ge ty m b ofs t v, + deref_loc ge ty m b ofs t v -> + wt_val v ty. +Proof. + induction 1. +- (* by value, non volatile *) + simpl in H1. exploit Mem.load_result; eauto. intros EQ; rewrite EQ. + apply wt_decode_val; auto. +- (* by value, volatile *) + inv H1. + + (* truly volatile *) + eapply wt_load_result; eauto. + + (* not really volatile *) + exploit Mem.load_result; eauto. intros EQ; rewrite EQ. + apply wt_decode_val; auto. +- (* by reference *) + destruct ty; simpl in H; try discriminate; auto with ty. + destruct i; destruct s; discriminate. + destruct f; discriminate. +- (* by copy *) + destruct ty; simpl in H; try discriminate; auto with ty. + destruct i; destruct s; discriminate. + destruct f; discriminate. +Qed. + +Lemma wt_bool_cast: + forall ty, wt_bool ty -> wt_cast ty type_bool. +Proof. + unfold wt_bool, wt_cast; unfold classify_bool; intros. destruct ty; simpl in *; try congruence. destruct f; congruence. +Qed. + +Lemma wt_cast_self: + forall t1 t2, wt_cast t1 t2 -> wt_cast t2 t2. +Proof. + unfold wt_cast; intros. destruct t2; simpl in *; try congruence. + destruct i; congruence. + destruct f; congruence. +Qed. + +Lemma binarith_type_int32s: + forall ty1 msg ty2, + binarith_type ty1 type_int32s msg = OK ty2 -> + ty2 = incrdecr_type ty1. +Proof. + intros. unfold incrdecr_type. + unfold binarith_type, classify_binarith in H; simpl in H. + destruct ty1; simpl; try congruence. + destruct i; destruct s; try congruence. + destruct s; congruence. + destruct f; congruence. +Qed. + +Lemma type_add_int32s: + forall ty1 ty2, + type_binop Oadd ty1 type_int32s = OK ty2 -> + ty2 = incrdecr_type ty1. +Proof. + simpl; intros. unfold classify_add in H; destruct ty1; simpl in H; + try (eapply binarith_type_int32s; eauto; fail). + destruct i; eapply binarith_type_int32s; eauto. + inv H; auto. + inv H; auto. + inv H; auto. +Qed. + +Lemma type_sub_int32s: + forall ty1 ty2, + type_binop Osub ty1 type_int32s = OK ty2 -> + ty2 = incrdecr_type ty1. +Proof. + simpl; intros. unfold classify_sub in H; destruct ty1; simpl in H; + try (eapply binarith_type_int32s; eauto; fail). + destruct i; eapply binarith_type_int32s; eauto. + inv H; auto. + inv H; auto. + inv H; auto. +Qed. + +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'. +Proof. + induction 1; intros WT; inversion WT. +- (* valof *) simpl in *. constructor. eapply wt_deref_loc; eauto. +- (* addrof *) constructor; auto with ty. +- (* unop *) simpl in H4. inv H2. constructor. eapply pres_sem_unop; eauto. +- (* binop *) + simpl in H6. inv H3. inv H5. constructor. eapply pres_sem_binop; eauto. +- (* cast *) inv H2. constructor. eapply pres_sem_cast; eauto. +- (* sequand true *) subst. constructor. auto. apply wt_bool_cast; auto. + red; intros. inv H0; auto with ty. +- (* sequand false *) constructor. auto with ty. +- (* seqor true *) constructor. auto with ty. +- (* seqor false *) subst. constructor. auto. apply wt_bool_cast; auto. + red; intros. inv H0; auto with ty. +- (* condition *) constructor. destruct b; auto. destruct b; auto. red; auto. +- (* sizeof *) constructor; auto with ty. +- (* alignof *) constructor; auto with ty. +- (* assign *) inversion H5. constructor. eapply pres_sem_cast; eauto. +- (* assignop *) subst tyres l r. constructor. auto. + constructor. constructor. eapply wt_deref_loc; eauto. + auto. auto. auto. +- (* postincr *) simpl in *. subst id0 l. + exploit wt_deref_loc; eauto. intros WTV1. + constructor. + constructor. auto. rewrite <- H0 in H5. constructor. + constructor; auto. constructor. constructor. auto with ty. + subst op. destruct id. + erewrite <- type_add_int32s by eauto. auto. + erewrite <- type_sub_int32s by eauto. auto. + simpl; auto. + constructor; auto. +- (* comma *) auto. +- (* paren *) inv H3. constructor. apply H5. eapply pres_sem_cast; eauto. +- (* builtin *) subst. auto with ty. +Qed. + +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'. +Proof. + induction 1; intros WT; constructor. +Qed. + +Lemma rred_same_type: + forall ge a m t a' m', + rred ge a m t a' m' -> typeof a' = typeof a. +Proof. + induction 1; auto. +Qed. + +Lemma lred_same_type: + forall ge e a m a' m', + lred ge e a m a' m' -> typeof a' = typeof a. +Proof. + induction 1; auto. +Qed. + +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. +Proof. + destruct 1; intros WT; auto; inv WT; eauto. + destruct 1; intros WT; inv WT; eauto. +Qed. + +Lemma typeof_context: + forall from to C, context from to C -> typeof (C a') = typeof (C a). +Proof. + induction 1; simpl; auto. +Qed. + +Lemma wt_arguments_context: + forall k C, contextlist k C -> + forall tyl, wt_arguments (C a) tyl -> wt_arguments (C a') tyl. +Proof. + induction 1; intros. +- inv H0. constructor; auto. rewrite (typeof_context _ _ _ H); auto. + constructor; auto. +- inv H0. constructor; auto. constructor; auto. +Qed. + +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'). +Proof. +- induction 1; intros WT BASE; + auto; + inv WT; + try (pose (EQTY := typeof_context _ _ _ H); rewrite <- ? EQTY; econstructor; + try (apply IHcontext; assumption); rewrite ? EQTY; eauto). +* red. econstructor; eauto. eapply wt_arguments_context; eauto. +* red. econstructor; eauto. eapply wt_arguments_context; eauto. +- induction 1; intros WT BASE. +* inv WT. constructor. apply (wt_context _ _ _ H); auto. auto. +* inv WT. constructor; auto. +Qed. + +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). +Proof. + unfold select_switch; intros. + assert (A: wt_lblstmts ce e rt (select_switch_default sl)). + { + revert sl H. induction 1; simpl; intros. + constructor. + destruct case. auto. constructor; auto. + } + assert (B: forall sl', select_switch_case n sl = Some sl' -> wt_lblstmts ce e rt sl'). + { + revert H. generalize sl. induction 1; simpl; intros. + discriminate. + destruct case; eauto. destruct (zeq z n); eauto. inv H1. econstructor; eauto. + } + destruct (select_switch_case n sl); auto. +Qed. + +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). +Proof. + induction 1; simpl. + constructor. + constructor; auto. +Qed. + +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). + +Hypothesis WT_EXTERNAL: + forall id ef args res cc vargs m t vres m', + In (id, Gfun (External ef args res cc)) prog.(prog_defs) -> + external_call ef ge vargs m t vres m' -> + wt_val vres res. + +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). +Proof. + intros. inv H0; simpl in H; try contradiction. constructor. auto. +Qed. + +Lemma wt_call_cont_stmt_cont: + forall te f k, wt_call_cont k f.(fn_return) -> wt_stmt_cont te f k. +Proof. + intros. inversion H; subst. constructor. constructor; auto. +Qed. + +Lemma call_cont_wt: + forall e f k, wt_stmt_cont e f k -> wt_call_cont (call_cont k) f.(fn_return). +Proof. + induction 1; simpl; auto. + constructor. + congruence. +Qed. + +Lemma call_cont_wt': + forall e f k, wt_stmt_cont e f k -> wt_stmt_cont e f (call_cont k). +Proof. + induction 1; simpl; auto; econstructor; eauto. +Qed. + +Definition wt_fundef (fd: fundef) := + match fd with + | Internal f => wt_function ge gtenv f + | External ef targs tres cc => True + end. + +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 fd. +Proof. + intros. apply Genv.find_funct_prop with (p := prog) (v := v); auto. + intros. inv WTPROG. destruct f; simpl; auto. apply H1 with id; auto. +Qed. + +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 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'. +Proof. + intros lbl e f s0 WTS0. pattern s0. + apply (wt_stmt_ind2 ge e f.(fn_return)) with + (P0 := fun ls => wt_lblstmts ge e f.(fn_return) ls -> + forall k s' k', + find_label_ls lbl ls k = Some (s', k') -> + wt_stmt_cont e f k -> + wt_stmt ge e f.(fn_return) s' /\ wt_stmt_cont e f k'); + simpl; intros; try discriminate. + + destruct (find_label lbl s1 (Kseq s2 k)) as [[sx kx] | ] eqn:F. + inv H3. eauto with ty. + eauto with ty. + + destruct (find_label lbl s1 k) as [[sx kx] | ] eqn:F. + inv H5. eauto with ty. + eauto with ty. + + eauto with ty. + + eauto with ty. + + destruct (find_label lbl s1 (Kseq (Sfor Sskip r s2 s3) k)) as [[sx kx] | ] eqn:F. + inv H7. eauto with ty. + destruct (find_label lbl s3 (Kfor3 r s2 s3 k)) as [[sx kx] | ] eqn:F2. + inv H7. eauto with ty. + eauto with ty. + + eauto with ty. + + destruct (ident_eq lbl lbl0). + inv H1. auto. + eauto. + + destruct (find_label lbl s (Kseq (seq_of_labeled_statement ls) k)) as [[sx kx] | ] eqn:F. + inv H4. eapply H0; eauto. constructor. auto. apply wt_seq_of_ls; auto. + eauto. + + assumption. +Qed. + +End WT_FIND_LABEL. + + +Lemma preservation_estep: + forall S t S', estep ge S t S' -> wt_state S -> wt_state S'. +Proof. + induction 1; intros WT; inv WT. +- (* lred *) + econstructor; eauto. change (wt_expr_kind ge te RV (C a')). + eapply wt_context with (a := a); eauto. + eapply lred_same_type; eauto. + eapply wt_lred; eauto. change (wt_expr_kind ge te LV a). eapply wt_subexpr; eauto. +- (* rred *) + econstructor; eauto. change (wt_expr_kind ge te RV (C a')). + eapply wt_context with (a := a); eauto. + eapply rred_same_type; eauto. + eapply wt_rred; eauto. change (wt_expr_kind ge te RV a). eapply wt_subexpr; eauto. +- (* call *) + assert (A: wt_expr_kind ge te RV a) by (eapply wt_subexpr; eauto). + simpl in A. inv H. inv A. simpl in H9; rewrite H4 in H9; inv H9. + assert (fundef_return fd = ty). + { destruct fd; simpl in *. + unfold type_of_function in H3. congruence. + congruence. } + econstructor. + rewrite H. econstructor; eauto. + intros. change (wt_expr_kind ge te RV (C (Eval v ty))). + eapply wt_context with (a := Ecall (Eval vf tyf) el ty); eauto. + red; constructor; auto. + eapply wt_find_funct; eauto. + eauto. +- (* stuck *) + constructor. +Qed. + +Lemma preservation_sstep: + forall S t S', sstep ge S t S' -> wt_state S -> wt_state S'. +Proof. + induction 1; intros WT; inv WT. +- inv WTS; eauto with ty. +- inv WTK; eauto with ty. +- inv WTS; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTS; eauto with ty. +- inv WTK; destruct b; eauto with ty. +- inv WTS; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTS; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTS; eauto with ty. +- inv WTS; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- econstructor. eapply call_cont_wt; eauto. constructor. +- inv WTS. eauto with ty. +- inv WTK. econstructor. eapply call_cont_wt; eauto. + inv WTE. eapply pres_sem_cast; eauto. +- econstructor. eapply is_wt_call_cont; eauto. constructor. +- inv WTS; eauto with ty. +- inv WTK. econstructor; eauto with ty. + apply wt_seq_of_ls. apply wt_select_switch; auto. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTS; eauto with ty. +- exploit wt_find_label. eexact WTB. eauto. eapply call_cont_wt'; eauto. + intros [A B]. eauto with ty. +- simpl in WTFD; inv WTFD. econstructor; eauto. apply wt_call_cont_stmt_cont; auto. +- exploit (Genv.find_funct_inversion prog); eauto. intros (id & A). + econstructor; eauto. +- inv WTK. eauto with ty. +Qed. + +Theorem preservation: + forall S t S', step ge S t S' -> wt_state S -> wt_state S'. +Proof. + intros. destruct H. eapply preservation_estep; eauto. eapply preservation_sstep; eauto. +Qed. + +Theorem wt_initial_state: + forall S, initial_state prog S -> wt_state S. +Proof. + intros. inv H. econstructor. constructor. + apply Genv.find_funct_ptr_prop with (p := prog) (b := b); auto. + intros. inv WTPROG. destruct f0; simpl; auto. apply H4 with id; auto. + instantiate (1 := (Vptr b Int.zero)). rewrite Genv.find_funct_find_funct_ptr. auto. +Qed. + +End PRESERVATION. + + + + + + + + + + + + + + + + + + + + + + + + + -- cgit