(* *********************************************************************) (* *) (* 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. *) (* *) (* *********************************************************************) (* * Dynamic semantics for the Clight language *) (*include "Coqlib.ma".*) (*include "Errors.ma".*) (*include "Integers.ma".*) (*include "Floats.ma".*) (*include "Values.ma".*) (*include "AST.ma".*) (*include "Mem.ma".*) include "common/Globalenvs.ma". include "Clight/Csyntax.ma". include "common/Maps.ma". (*include "Events.ma".*) include "common/Smallstep.ma". (* * * Semantics of type-dependent operations *) (* * Interpretation of values as truth values. Non-zero integers, non-zero floats and non-null pointers are considered as true. The integer zero (which also represents the null pointer) and the float 0.0 are false. *) inductive is_false: val → type → Prop ≝ | is_false_int: ∀sz,sg. is_false (Vint zero) (Tint sz sg) | is_false_pointer: ∀r,r',t. is_false (Vnull r) (Tpointer r' t) | is_false_float: ∀sz. is_false (Vfloat Fzero) (Tfloat sz). inductive is_true: val → type → Prop ≝ | is_true_int_int: ∀n,sz,sg. n ≠ zero → is_true (Vint n) (Tint sz sg) | is_true_pointer_pointer: ∀r,b,pc,ofs,s,t. is_true (Vptr r b pc ofs) (Tpointer s t) | is_true_float: ∀f,sz. f ≠ Fzero → is_true (Vfloat f) (Tfloat sz). inductive bool_of_val : val → type → val → Prop ≝ | bool_of_val_true: ∀v,ty. is_true v ty → bool_of_val v ty Vtrue | bool_of_val_false: ∀v,ty. is_false v ty → bool_of_val v ty Vfalse. (* * The following [sem_] functions compute the result of an operator application. Since operators are overloaded, the result depends both on the static types of the arguments and on their run-time values. Unlike in C, automatic conversions between integers and floats are not performed. For instance, [e1 + e2] is undefined if [e1] is a float and [e2] an integer. The Clight producer must have explicitly promoted [e2] to a float. *) let rec sem_neg (v: val) (ty: type) : option val ≝ match ty with [ Tint _ _ ⇒ match v with [ Vint n ⇒ Some ? (Vint (two_complement_negation wordsize n)) | _ ⇒ None ? ] | Tfloat _ ⇒ match v with [ Vfloat f ⇒ Some ? (Vfloat (Fneg f)) | _ ⇒ None ? ] | _ ⇒ None ? ]. let rec sem_notint (v: val) : option val ≝ match v with [ Vint n ⇒ Some ? (Vint (xor n mone)) (* XXX *) | _ ⇒ None ? ]. let rec sem_notbool (v: val) (ty: type) : option val ≝ match ty with [ Tint _ _ ⇒ match v with [ Vint n ⇒ Some ? (of_bool (eq n zero)) | _ ⇒ None ? ] | Tpointer _ _ ⇒ match v with [ Vptr _ _ _ _ ⇒ Some ? Vfalse | Vnull _ ⇒ Some ? Vtrue | _ ⇒ None ? ] | Tfloat _ ⇒ match v with [ Vfloat f ⇒ Some ? (of_bool (Fcmp Ceq f Fzero)) | _ ⇒ None ? ] | _ ⇒ None ? ]. let rec sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ match classify_add t1 t2 with [ add_case_ii ⇒ (**r integer addition *) match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ Some ? (Vint (addition_n wordsize n1 n2)) | _ ⇒ None ? ] | _ ⇒ None ? ] | add_case_ff ⇒ (**r float addition *) match v1 with [ Vfloat n1 ⇒ match v2 with [ Vfloat n2 ⇒ Some ? (Vfloat (Fadd n1 n2)) | _ ⇒ None ? ] | _ ⇒ None ? ] | add_case_pi ty ⇒ (**r pointer plus integer *) match v1 with [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (shift_offset ofs1 (mul (repr (sizeof ty)) n2))) | _ ⇒ None ? ] | Vnull r ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ] | _ ⇒ None ? ] | add_case_ip ty ⇒ (**r integer plus pointer *) match v1 with [ Vint n1 ⇒ match v2 with [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (shift_offset ofs2 (mul (repr (sizeof ty)) n1))) | Vnull r ⇒ if eq n1 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ] | _ ⇒ None ? ] | add_default ⇒ None ? ]. let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ match classify_sub t1 t2 with [ sub_case_ii ⇒ (**r integer subtraction *) match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ Some ? (Vint (subtraction wordsize n1 n2)) | _ ⇒ None ? ] | _ ⇒ None ? ] | sub_case_ff ⇒ (**r float subtraction *) match v1 with [ Vfloat f1 ⇒ match v2 with [ Vfloat f2 ⇒ Some ? (Vfloat (Fsub f1 f2)) | _ ⇒ None ? ] | _ ⇒ None ? ] | sub_case_pi ty ⇒ (**r pointer minus integer *) match v1 with [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 (mul (repr (sizeof ty)) n2))) | _ ⇒ None ? ] | Vnull r ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ] | _ ⇒ None ? ] | sub_case_pp ty ⇒ (**r pointer minus pointer *) match v1 with [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with [ Vptr r2 b2 p2 ofs2 ⇒ if eq_block b1 b2 then if eq (repr (sizeof ty)) zero then None ? else match division_u ? (sub_offset ofs1 ofs2) (repr (sizeof ty)) with [ None ⇒ None ? | Some v ⇒ Some ? (Vint v) ] else None ? | _ ⇒ None ? ] | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero) | _ ⇒ None ? ] | _ ⇒ None ? ] | sub_default ⇒ None ? ]. let rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ match classify_mul t1 t2 with [ mul_case_ii ⇒ match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ Some ? (Vint (mul n1 n2)) (* [ Vint n2 ⇒ Some ? (Vint (\snd (split ? wordsize wordsize (multiplication ? n1 n2))))*) | _ ⇒ None ? ] | _ ⇒ None ? ] | mul_case_ff ⇒ match v1 with [ Vfloat f1 ⇒ match v2 with [ Vfloat f2 ⇒ Some ? (Vfloat (Fmul f1 f2)) | _ ⇒ None ? ] | _ ⇒ None ? ] | mul_default ⇒ None ? ]. let rec sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ match classify_div t1 t2 with [ div_case_I32unsi ⇒ match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2) | _ ⇒ None ? ] | _ ⇒ None ? ] | div_case_ii ⇒ match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2) | _ ⇒ None ? ] | _ ⇒ None ? ] | div_case_ff ⇒ match v1 with [ Vfloat f1 ⇒ match v2 with [ Vfloat f2 ⇒ Some ? (Vfloat(Fdiv f1 f2)) | _ ⇒ None ? ] | _ ⇒ None ? ] | div_default ⇒ None ? ]. let rec sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ match classify_mod t1 t2 with [ mod_case_I32unsi ⇒ match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2) | _ ⇒ None ? ] | _ ⇒ None ? ] | mod_case_ii ⇒ match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2) | _ ⇒ None ? ] | _ ⇒ None ? ] | mod_default ⇒ None ? ]. let rec sem_and (v1,v2: val) : option val ≝ match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ Some ? (Vint (conjunction_bv ? n1 n2)) | _ ⇒ None ? ] | _ ⇒ None ? ]. let rec sem_or (v1,v2: val) : option val ≝ match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ Some ? (Vint (inclusive_disjunction_bv ? n1 n2)) | _ ⇒ None ? ] | _ ⇒ None ? ]. let rec sem_xor (v1,v2: val) : option val ≝ match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ Some ? (Vint (exclusive_disjunction_bv ? n1 n2)) | _ ⇒ None ? ] | _ ⇒ None ? ]. let rec sem_shl (v1,v2: val): option val ≝ match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ if ltu n2 iwordsize then Some ? (Vint(shl n1 n2)) else None ? | _ ⇒ None ? ] | _ ⇒ None ? ]. let rec sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val ≝ match classify_shr t1 t2 with [ shr_case_I32unsi ⇒ match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ if ltu n2 iwordsize then Some ? (Vint (shru n1 n2)) else None ? | _ ⇒ None ? ] | _ ⇒ None ? ] | shr_case_ii => match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ if ltu n2 iwordsize then Some ? (Vint (shr n1 n2)) else None ? | _ ⇒ None ? ] | _ ⇒ None ? ] | shr_default ⇒ None ? ]. let rec sem_cmp_mismatch (c: comparison): option val ≝ match c with [ Ceq => Some ? Vfalse | Cne => Some ? Vtrue | _ => None ? ]. let rec sem_cmp_match (c: comparison): option val ≝ match c with [ Ceq => Some ? Vtrue | Cne => Some ? Vfalse | _ => None ? ]. let rec sem_cmp (c:comparison) (v1: val) (t1: type) (v2: val) (t2: type) (m: mem): option val ≝ match classify_cmp t1 t2 with [ cmp_case_I32unsi ⇒ match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ Some ? (of_bool (cmpu c n1 n2)) | _ ⇒ None ? ] | _ ⇒ None ? ] | cmp_case_ii ⇒ match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2)) | _ ⇒ None ? ] | _ ⇒ None ? ] | cmp_case_pp ⇒ match v1 with [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with [ Vptr r2 b2 p2 ofs2 ⇒ if valid_pointer m r1 b1 ofs1 ∧ valid_pointer m r2 b2 ofs2 then if eq_block b1 b2 then Some ? (of_bool (cmp_offset c ofs1 ofs2)) else sem_cmp_mismatch c else None ? | Vnull r2 ⇒ sem_cmp_mismatch c | _ ⇒ None ? ] | Vnull r1 ⇒ match v2 with [ Vptr r2 b2 p2 ofs2 ⇒ sem_cmp_mismatch c | Vnull r2 ⇒ sem_cmp_match c | _ ⇒ None ? ] | _ ⇒ None ? ] | cmp_case_ff ⇒ match v1 with [ Vfloat f1 ⇒ match v2 with [ Vfloat f2 ⇒ Some ? (of_bool (Fcmp c f1 f2)) | _ ⇒ None ? ] | _ ⇒ None ? ] | cmp_default ⇒ None ? ]. definition sem_unary_operation : unary_operation → val → type → option val ≝ λop,v,ty. match op with [ Onotbool => sem_notbool v ty | Onotint => sem_notint v | Oneg => sem_neg v ty ]. let rec sem_binary_operation (op: binary_operation) (v1: val) (t1: type) (v2: val) (t2:type) (m: mem): option val ≝ match op with [ Oadd ⇒ sem_add v1 t1 v2 t2 | Osub ⇒ sem_sub v1 t1 v2 t2 | Omul ⇒ sem_mul v1 t1 v2 t2 | Omod ⇒ sem_mod v1 t1 v2 t2 | Odiv ⇒ sem_div v1 t1 v2 t2 | Oand ⇒ sem_and v1 v2 | Oor ⇒ sem_or v1 v2 | Oxor ⇒ sem_xor v1 v2 | Oshl ⇒ sem_shl v1 v2 | Oshr ⇒ sem_shr v1 t1 v2 t2 | Oeq ⇒ sem_cmp Ceq v1 t1 v2 t2 m | One ⇒ sem_cmp Cne v1 t1 v2 t2 m | Olt ⇒ sem_cmp Clt v1 t1 v2 t2 m | Ogt ⇒ sem_cmp Cgt v1 t1 v2 t2 m | Ole ⇒ sem_cmp Cle v1 t1 v2 t2 m | Oge ⇒ sem_cmp Cge v1 t1 v2 t2 m ]. (* * Semantic of casts. [cast v1 t1 t2 v2] holds if value [v1], viewed with static type [t1], can be cast to type [t2], resulting in value [v2]. *) let rec cast_int_int (sz: intsize) (sg: signedness) (i: int) : int ≝ match sz with [ I8 ⇒ match sg with [ Signed ⇒ sign_ext 8 i | Unsigned ⇒ zero_ext 8 i ] | I16 ⇒ match sg with [ Signed => sign_ext 16 i | Unsigned ⇒ zero_ext 16 i ] | I32 ⇒ i ]. let rec cast_int_float (si : signedness) (i: int) : float ≝ match si with [ Signed ⇒ floatofint i | Unsigned ⇒ floatofintu i ]. let rec cast_float_int (si : signedness) (f: float) : int ≝ match si with [ Signed ⇒ intoffloat f | Unsigned ⇒ intuoffloat f ]. let rec cast_float_float (sz: floatsize) (f: float) : float ≝ match sz with [ F32 ⇒ singleoffloat f | F64 ⇒ f ]. inductive type_region : type → region → Prop ≝ | type_rgn_pointer : ∀s,t. type_region (Tpointer s t) s | type_rgn_array : ∀s,t,n. type_region (Tarray s t n) s (* XXX Is the following necessary? *) | type_rgn_code : ∀tys,ty. type_region (Tfunction tys ty) Code. inductive cast : mem → val → type → type → val → Prop ≝ | cast_ii: ∀m,i,sz2,sz1,si1,si2. (**r int to int *) cast m (Vint i) (Tint sz1 si1) (Tint sz2 si2) (Vint (cast_int_int sz2 si2 i)) | cast_fi: ∀m,f,sz1,sz2,si2. (**r float to int *) cast m (Vfloat f) (Tfloat sz1) (Tint sz2 si2) (Vint (cast_int_int sz2 si2 (cast_float_int si2 f))) | cast_if: ∀m,i,sz1,sz2,si1. (**r int to float *) cast m (Vint i) (Tint sz1 si1) (Tfloat sz2) (Vfloat (cast_float_float sz2 (cast_int_float si1 i))) | cast_ff: ∀m,f,sz1,sz2. (**r float to float *) cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2) (Vfloat (cast_float_float sz2 f)) | cast_pp: ∀m,r,r',ty,ty',b,pc,ofs. type_region ty r → type_region ty' r' → ∀pc':pointer_compat b r'. cast m (Vptr r b pc ofs) ty ty' (Vptr r' b pc' ofs) | cast_ip_z: ∀m,sz,sg,ty',r. type_region ty' r → cast m (Vint zero) (Tint sz sg) ty' (Vnull r) | cast_pp_z: ∀m,ty,ty',r,r'. type_region ty r → type_region ty' r' → cast m (Vnull r) ty ty' (Vnull r'). (* * * Operational semantics *) (* * The semantics uses two environments. The global environment maps names of functions and global variables to memory block references, and function pointers to their definitions. (See module [Globalenvs].) *) definition genv ≝ (genv_t Genv) clight_fundef. (* * The local environment maps local variables to block references. The current value of the variable is stored in the associated memory block. *) definition env ≝ (tree_t ? PTree) block. (* map variable -> location *) definition empty_env: env ≝ (empty …). (* * [load_value_of_type ty m b ofs] computes the value of a datum of type [ty] residing in memory [m] at block [b], offset [ofs]. If the type [ty] indicates an access by value, the corresponding memory load is performed. If the type [ty] indicates an access by reference, the pointer [Vptr b ofs] is returned. *) let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: offset) : option val ≝ match access_mode ty with [ By_value chunk ⇒ loadv chunk m (Vptr Any b ? ofs) | By_reference r ⇒ match pointer_compat_dec b r with [ inl p ⇒ Some ? (Vptr r b p ofs) | inr _ ⇒ None ? ] | By_nothing ⇒ None ? ]. cases b // qed. (* * Symmetrically, [store_value_of_type ty m b ofs v] returns the memory state after storing the value [v] in the datum of type [ty] residing in memory [m] at block [b], offset [ofs]. This is allowed only if [ty] indicates an access by value. *) let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: offset) (v: val) : option mem ≝ match access_mode ty_dest with [ By_value chunk ⇒ storev chunk m (Vptr Any loc ? ofs) v | By_reference _ ⇒ None ? | By_nothing ⇒ None ? ]. cases loc // qed. (* * Allocation of function-local variables. [alloc_variables e1 m1 vars e2 m2] allocates one memory block for each variable declared in [vars], and associates the variable name with this block. [e1] and [m1] are the initial local environment and memory state. [e2] and [m2] are the final local environment and memory state. *) inductive alloc_variables: env → mem → list (ident × type) → env → mem → Prop ≝ | alloc_variables_nil: ∀e,m. alloc_variables e m (nil ?) e m | alloc_variables_cons: ∀e,m,id,ty,vars,m1,b1,m2,e2. alloc m 0 (sizeof ty) Any = 〈m1, b1〉 → alloc_variables (set … id b1 e) m1 vars e2 m2 → alloc_variables e m (〈id, ty〉 :: vars) e2 m2. (* * Initialization of local variables that are parameters to a function. [bind_parameters e m1 params args m2] stores the values [args] in the memory blocks corresponding to the variables [params]. [m1] is the initial memory state and [m2] the final memory state. *) inductive bind_parameters: env → mem → list (ident × type) → list val → mem → Prop ≝ | bind_parameters_nil: ∀e,m. bind_parameters e m (nil ?) (nil ?) m | bind_parameters_cons: ∀e,m,id,ty,params,v1,vl,b,m1,m2. get ??? id e = Some ? b → store_value_of_type ty m b zero_offset v1 = Some ? m1 → bind_parameters e m1 params vl m2 → bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2. (* * Return the list of blocks in the codomain of [e]. *) definition blocks_of_env : env → list block ≝ λe. map ?? (λx. snd ?? x) (elements ??? e). (* * Selection of the appropriate case of a [switch], given the value [n] of the selector expression. *) let rec select_switch (n: int) (sl: labeled_statements) on sl : labeled_statements ≝ match sl with [ LSdefault _ ⇒ sl | LScase c s sl' ⇒ if eq c n then sl else select_switch n sl' ]. (* * Turn a labeled statement into a sequence *) let rec seq_of_labeled_statement (sl: labeled_statements) : statement ≝ match sl with [ LSdefault s ⇒ s | LScase c s sl' ⇒ Ssequence s (seq_of_labeled_statement sl') ]. (* Section SEMANTICS. Variable ge: genv. (** ** Evaluation of expressions *) Section EXPR. Variable e: env. Variable m: mem. *) (* * [eval_expr ge e m a v] defines the evaluation of expression [a] in r-value position. [v] is the value of the expression. [e] is the current environment and [m] is the current memory state. *) inductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝ | eval_Econst_int: ∀i,ty. eval_expr ge e m (Expr (Econst_int i) ty) (Vint i) E0 | eval_Econst_float: ∀f,ty. eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0 | eval_Elvalue: ∀a,ty,loc,ofs,v,tr. eval_lvalue ge e m (Expr a ty) loc ofs tr → load_value_of_type ty m loc ofs = Some ? v → eval_expr ge e m (Expr a ty) v tr | eval_Eaddrof: ∀a,ty,r,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → ∀pc:pointer_compat loc r. eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr r loc pc ofs) tr | eval_Esizeof: ∀ty',ty. eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) E0 | eval_Eunop: ∀op,a,ty,v1,v,tr. eval_expr ge e m a v1 tr → sem_unary_operation op v1 (typeof a) = Some ? v → eval_expr ge e m (Expr (Eunop op a) ty) v tr | eval_Ebinop: ∀op,a1,a2,ty,v1,v2,v,tr1,tr2. eval_expr ge e m a1 v1 tr1 → eval_expr ge e m a2 v2 tr2 → sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some ? v → eval_expr ge e m (Expr (Ebinop op a1 a2) ty) v (tr1⧺tr2) | eval_Econdition_true: ∀a1,a2,a3,ty,v1,v2,tr1,tr2. eval_expr ge e m a1 v1 tr1 → is_true v1 (typeof a1) → eval_expr ge e m a2 v2 tr2 → eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v2 (tr1⧺tr2) | eval_Econdition_false: ∀a1,a2,a3,ty,v1,v3,tr1,tr2. eval_expr ge e m a1 v1 tr1 → is_false v1 (typeof a1) → eval_expr ge e m a3 v3 tr2 → eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v3 (tr1⧺tr2) | eval_Eorbool_1: ∀a1,a2,ty,v1,tr. eval_expr ge e m a1 v1 tr → is_true v1 (typeof a1) → eval_expr ge e m (Expr (Eorbool a1 a2) ty) Vtrue tr | eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2. eval_expr ge e m a1 v1 tr1 → is_false v1 (typeof a1) → eval_expr ge e m a2 v2 tr2 → bool_of_val v2 (typeof a2) v → eval_expr ge e m (Expr (Eorbool a1 a2) ty) v (tr1⧺tr2) | eval_Eandbool_1: ∀a1,a2,ty,v1,tr. eval_expr ge e m a1 v1 tr → is_false v1 (typeof a1) → eval_expr ge e m (Expr (Eandbool a1 a2) ty) Vfalse tr | eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2. eval_expr ge e m a1 v1 tr1 → is_true v1 (typeof a1) → eval_expr ge e m a2 v2 tr2 → bool_of_val v2 (typeof a2) v → eval_expr ge e m (Expr (Eandbool a1 a2) ty) v (tr1⧺tr2) | eval_Ecast: ∀a,ty,ty',v1,v,tr. eval_expr ge e m a v1 tr → cast m v1 (typeof a) ty v → eval_expr ge e m (Expr (Ecast ty a) ty') v tr | eval_Ecost: ∀a,ty,v,l,tr. eval_expr ge e m a v tr → eval_expr ge e m (Expr (Ecost l a) ty) v (tr⧺Echarge l) (* * [eval_lvalue ge e m a r b ofs] defines the evaluation of expression [a] in l-value position. The result is the memory location [b, ofs] that contains the value of the expression [a]. The memory location should be representable in a pointer of region r. *) with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → block → offset → trace → Prop ≝ | eval_Evar_local: ∀id,l,ty. (* XXX notation? e!id*) get ??? id e = Some ? l → eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0 | eval_Evar_global: ∀id,l,ty. (* XXX e!id *) get ??? id e = None ? → find_symbol ?? ge id = Some ? l → eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0 | eval_Ederef: ∀a,ty,r,l,p,ofs,tr. eval_expr ge e m a (Vptr r l p ofs) tr → eval_lvalue ge e m (Expr (Ederef a) ty) l ofs tr (* Aside: note that each block of memory is entirely contained within one memory region; hence adding a field offset will not produce a location outside of the original location's region. *) | eval_Efield_struct: ∀a,i,ty,l,ofs,id,fList,delta,tr. eval_lvalue ge e m a l ofs tr → typeof a = Tstruct id fList → field_offset i fList = OK ? delta → eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ofs (repr delta)) tr | eval_Efield_union: ∀a,i,ty,l,ofs,id,fList,tr. eval_lvalue ge e m a l ofs tr → typeof a = Tunion id fList → eval_lvalue ge e m (Expr (Efield a i) ty) l ofs tr. let rec eval_expr_ind (ge:genv) (e:env) (m:mem) (P:∀a,v,tr. eval_expr ge e m a v tr → Prop) (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty)) (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2)) (ead:∀a,ty,r,loc,pc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty r loc pc ofs tr H)) (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty)) (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2)) (ebi:∀op,a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H2 → P ??? (eval_Ebinop ge e m op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3)) (ect:∀a1,a2,a3,ty,v1,v2,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Econdition_true ge e m a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3)) (ecf:∀a1,a2,a3,ty,v1,v3,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a3 v3 tr2 H3 → P ??? (eval_Econdition_false ge e m a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3)) (eo1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr H1 H2)) (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) (ea1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr H1 H2)) (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2)) (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H)) (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝ match ev with [ eval_Econst_int i ty ⇒ eci i ty | eval_Econst_float f ty ⇒ ecF f ty | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 | eval_Eaddrof a ty r loc pc ofs tr H ⇒ ead a ty r loc pc ofs tr H | eval_Esizeof ty' ty ⇒ esz ty' ty | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1) | eval_Ebinop op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 ⇒ ebi op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H2) | eval_Econdition_true a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 ⇒ ect a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3) | eval_Econdition_false a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 ⇒ ecf a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a3 v3 tr2 H3) | eval_Eorbool_1 a1 a2 ty v1 tr H1 H2 ⇒ eo1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1) | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3) | eval_Eandbool_1 a1 a2 ty v1 tr H1 H2 ⇒ ea1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1) | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3) | eval_Ecast a ty ty' v1 v tr H1 H2 ⇒ ecs a ty ty' v1 v tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1) | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v tr H) ]. inverter eval_expr_inv_ind for eval_expr : Prop. let rec eval_lvalue_ind (ge:genv) (e:env) (m:mem) (P:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop) (lvl:∀id,l,ty,H. P ???? (eval_Evar_local ge e m id l ty H)) (lvg:∀id,l,ty,H1,H2. P ???? (eval_Evar_global ge e m id l ty H1 H2)) (lde:∀a,ty,r,l,pc,ofs,tr,H. P ???? (eval_Ederef ge e m a ty r l pc ofs tr H)) (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. P a l ofs tr H1 → P ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3)) (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. P a l ofs tr H1 → P ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2)) (a:expr) (loc:block) (ofs:offset) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : P a loc ofs tr ev ≝ match ev with [ eval_Evar_local id l ty H ⇒ lvl id l ty H | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2 | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc ofs tr H | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1) | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1) ]. (* ninverter eval_lvalue_inv_ind for eval_lvalue : Prop. *) definition eval_lvalue_inv_ind : ∀x1: genv. ∀x2: env. ∀x3: mem. ∀x4: expr. ∀x6: block. ∀x7: offset. ∀x8: trace. ∀P: ∀_z1430: expr. ∀_z1428: block. ∀_z1427: offset. ∀_z1426: trace. Prop. ∀_H1: ?. ∀_H2: ?. ∀_H3: ?. ∀_H4: ?. ∀_H5: ?. ∀_Hterm: eval_lvalue x1 x2 x3 x4 x6 x7 x8. P x4 x6 x7 x8 := (λx1:genv. (λx2:env. (λx3:mem. (λx4:expr. (λx6:block. (λx7:offset. (λx8:trace. (λP:∀_z1430: expr. ∀_z1428: block. ∀_z1427: offset. ∀_z1426: trace. Prop. (λH1:?. (λH2:?. (λH3:?. (λH4:?. (λH5:?. (λHterm:eval_lvalue x1 x2 x3 x4 x6 x7 x8. ((λHcut:∀z1435: eq expr x4 x4. ∀z1433: eq block x6 x6. ∀z1432: eq offset x7 x7. ∀z1431: eq trace x8 x8. P x4 x6 x7 x8. (Hcut (refl expr x4) (refl block x6) (refl offset x7) (refl trace x8))) ?))))))))))))))). [ @(eval_lvalue_ind x1 x2 x3 (λa,loc,ofs,tr,e. ∀e1:eq ? x4 a. ∀e3:eq ? x6 loc. ∀e4:eq ? x7 ofs. ∀e5:eq ? x8 tr. P a loc ofs tr) … Hterm) [ @H1 | @H2 | @H3 | @H4 | @H5 ] | *: skip ] qed. let rec eval_expr_ind2 (ge:genv) (e:env) (m:mem) (P:∀a,v,tr. eval_expr ge e m a v tr → Prop) (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop) (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty)) (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2)) (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc)) (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty)) (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2)) (ebi:∀op,a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H2 → P ??? (eval_Ebinop ge e m op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3)) (ect:∀a1,a2,a3,ty,v1,v2,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Econdition_true ge e m a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3)) (ecf:∀a1,a2,a3,ty,v1,v3,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a3 v3 tr2 H3 → P ??? (eval_Econdition_false ge e m a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3)) (eo1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr H1 H2)) (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) (ea1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr H1 H2)) (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2)) (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H)) (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H)) (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2)) (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr r l pc ofs) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H)) (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3)) (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2)) (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝ match ev with [ eval_Econst_int i ty ⇒ eci i ty | eval_Econst_float f ty ⇒ ecF f ty | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu (Expr a ty) loc ofs tr H1) | eval_Eaddrof a ty r loc ofs tr H pc ⇒ ead a ty r loc pc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H) | eval_Esizeof ty' ty ⇒ esz ty' ty | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1) | eval_Ebinop op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 ⇒ ebi op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H2) | eval_Econdition_true a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 ⇒ ect a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3) | eval_Econdition_false a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 ⇒ ecf a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a3 v3 tr2 H3) | eval_Eorbool_1 a1 a2 ty v1 tr H1 H2 ⇒ eo1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1) | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3) | eval_Eandbool_1 a1 a2 ty v1 tr H1 H2 ⇒ ea1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1) | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3) | eval_Ecast a ty ty' v1 v tr H1 H2 ⇒ ecs a ty ty' v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1) | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v tr H) ] and eval_lvalue_ind2 (ge:genv) (e:env) (m:mem) (P:∀a,v,tr. eval_expr ge e m a v tr → Prop) (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop) (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty)) (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2)) (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc)) (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty)) (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2)) (ebi:∀op,a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H2 → P ??? (eval_Ebinop ge e m op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3)) (ect:∀a1,a2,a3,ty,v1,v2,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Econdition_true ge e m a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3)) (ecf:∀a1,a2,a3,ty,v1,v3,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a3 v3 tr2 H3 → P ??? (eval_Econdition_false ge e m a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3)) (eo1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr H1 H2)) (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) (ea1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr H1 H2)) (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4)) (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2)) (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H)) (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H)) (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2)) (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr r l pc ofs) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H)) (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3)) (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2)) (a:expr) (loc:block) (ofs:offset) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : Q a loc ofs tr ev ≝ match ev with [ eval_Evar_local id l ty H ⇒ lvl id l ty H | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2 | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc ofs tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a (Vptr r l pc ofs) tr H) | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1) | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1) ]. definition combined_expr_lvalue_ind ≝ λge,e,m,P,Q,eci,ecF,elv,ead,esz,eun,ebi,ect,ecf,eo1,eo2,ea1,ea2,ecs,eco,lvl,lvg,lde,lfs,lfu. conj ?? (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu) (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu). (* * [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a] in l-value position. The result is the memory location [b, ofs] that contains the value of the expression [a]. *) (* Scheme eval_expr_ind22 := Minimality for eval_expr Sort Prop with eval_lvalue_ind2 := Minimality for eval_lvalue Sort Prop. *) (* * [eval_exprlist ge e m al vl] evaluates a list of r-value expressions [al] to their values [vl]. *) inductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr → list val → trace → Prop ≝ | eval_Enil: eval_exprlist ge e m (nil ?) (nil ?) E0 | eval_Econs: ∀a,bl,v,vl,tr1,tr2. eval_expr ge e m a v tr1 → eval_exprlist ge e m bl vl tr2 → eval_exprlist ge e m (a :: bl) (v :: vl) (tr1⧺tr2). (*End EXPR.*) (* * ** Transition semantics for statements and functions *) (* * Continuations *) inductive cont: Type[0] := | Kstop: cont | Kseq: statement -> cont -> cont (**r [Kseq s2 k] = after [s1] in [s1;s2] *) | Kwhile: expr -> statement -> cont -> cont (**r [Kwhile e s k] = after [s] in [while (e) s] *) | Kdowhile: expr -> statement -> cont -> cont (**r [Kdowhile e s k] = after [s] in [do s while (e)] *) | Kfor2: expr -> statement -> statement -> cont -> cont (**r [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *) | Kfor3: expr -> statement -> statement -> cont -> cont (**r [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *) | Kswitch: cont -> cont (**r catches [break] statements arising out of [switch] *) | Kcall: option (block × offset × type) -> (**r where to store result *) function -> (**r calling function *) env -> (**r local env of calling function *) cont -> cont. (* * Pop continuation until a call or stop *) let rec call_cont (k: cont) : cont := match k with [ Kseq s k => call_cont k | Kwhile e s k => call_cont k | Kdowhile e s k => call_cont k | Kfor2 e2 e3 s k => call_cont k | Kfor3 e2 e3 s k => call_cont k | Kswitch k => call_cont k | _ => k ]. definition is_call_cont : cont → Prop ≝ λk. match k with [ Kstop => True | Kcall _ _ _ _ => True | _ => False ]. (* * States *) inductive state: Type[0] := | State: ∀f: function. ∀s: statement. ∀k: cont. ∀e: env. ∀m: mem. state | Callstate: ∀fd: clight_fundef. ∀args: list val. ∀k: cont. ∀m: mem. state | Returnstate: ∀res: val. ∀k: cont. ∀m: mem. state. (* * Find the statement and manufacture the continuation corresponding to a label *) let rec find_label (lbl: label) (s: statement) (k: cont) on s: option (statement × cont) := match s with [ Ssequence s1 s2 => match find_label lbl s1 (Kseq s2 k) with [ Some sk => Some ? sk | None => find_label lbl s2 k ] | Sifthenelse a s1 s2 => match find_label lbl s1 k with [ Some sk => Some ? sk | None => find_label lbl s2 k ] | Swhile a s1 => find_label lbl s1 (Kwhile a s1 k) | Sdowhile a s1 => find_label lbl s1 (Kdowhile a s1 k) | Sfor a1 a2 a3 s1 => match find_label lbl a1 (Kseq (Sfor Sskip a2 a3 s1) k) with [ Some sk => Some ? sk | None => match find_label lbl s1 (Kfor2 a2 a3 s1 k) with [ Some sk => Some ? sk | None => find_label lbl a3 (Kfor3 a2 a3 s1 k) ] ] | Sswitch e sl => find_label_ls lbl sl (Kswitch k) | Slabel lbl' s' => match ident_eq lbl lbl' with [ inl _ ⇒ Some ? 〈s', k〉 | inr _ ⇒ find_label lbl s' k ] | _ => None ? ] and find_label_ls (lbl: label) (sl: labeled_statements) (k: cont) on sl: option (statement × cont) := match sl with [ LSdefault s => find_label lbl s k | LScase _ s sl' => match find_label lbl s (Kseq (seq_of_labeled_statement sl') k) with [ Some sk => Some ? sk | None => find_label_ls lbl sl' k ] ]. (* * Transition relation *) (* Strip off outer pointer for use when comparing function types. *) definition fun_typeof ≝ λe. match typeof e with [ Tvoid ⇒ Tvoid | Tint a b ⇒ Tint a b | Tfloat a ⇒ Tfloat a | Tpointer _ ty ⇒ ty | Tarray a b c ⇒ Tarray a b c | Tfunction a b ⇒ Tfunction a b | Tstruct a b ⇒ Tstruct a b | Tunion a b ⇒ Tunion a b | Tcomp_ptr a b ⇒ Tcomp_ptr a b ]. (* XXX: note that cost labels in exprs expose a particular eval order. *) inductive step (ge:genv) : state → trace → state → Prop ≝ | step_assign: ∀f,a1,a2,k,e,m,loc,ofs,v2,m',tr1,tr2. eval_lvalue ge e m a1 loc ofs tr1 → eval_expr ge e m a2 v2 tr2 → store_value_of_type (typeof a1) m loc ofs v2 = Some ? m' → step ge (State f (Sassign a1 a2) k e m) (tr1⧺tr2) (State f Sskip k e m') | step_call_none: ∀f,a,al,k,e,m,vf,vargs,fd,tr1,tr2. eval_expr ge e m a vf tr1 → eval_exprlist ge e m al vargs tr2 → find_funct ?? ge vf = Some ? fd → type_of_fundef fd = fun_typeof a → step ge (State f (Scall (None ?) a al) k e m) (tr1⧺tr2) (Callstate fd vargs (Kcall (None ?) f e k) m) | step_call_some: ∀f,lhs,a,al,k,e,m,loc,ofs,vf,vargs,fd,tr1,tr2,tr3. eval_lvalue ge e m lhs loc ofs tr1 → eval_expr ge e m a vf tr2 → eval_exprlist ge e m al vargs tr3 → find_funct ?? ge vf = Some ? fd → type_of_fundef fd = fun_typeof a → step ge (State f (Scall (Some ? lhs) a al) k e m) (tr1⧺tr2⧺tr3) (Callstate fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m) | step_seq: ∀f,s1,s2,k,e,m. step ge (State f (Ssequence s1 s2) k e m) E0 (State f s1 (Kseq s2 k) e m) | step_skip_seq: ∀f,s,k,e,m. step ge (State f Sskip (Kseq s k) e m) E0 (State f s k e m) | step_continue_seq: ∀f,s,k,e,m. step ge (State f Scontinue (Kseq s k) e m) E0 (State f Scontinue k e m) | step_break_seq: ∀f,s,k,e,m. step ge (State f Sbreak (Kseq s k) e m) E0 (State f Sbreak k e m) | step_ifthenelse_true: ∀f,a,s1,s2,k,e,m,v1,tr. eval_expr ge e m a v1 tr → is_true v1 (typeof a) → step ge (State f (Sifthenelse a s1 s2) k e m) tr (State f s1 k e m) | step_ifthenelse_false: ∀f,a,s1,s2,k,e,m,v1,tr. eval_expr ge e m a v1 tr → is_false v1 (typeof a) → step ge (State f (Sifthenelse a s1 s2) k e m) tr (State f s2 k e m) | step_while_false: ∀f,a,s,k,e,m,v,tr. eval_expr ge e m a v tr → is_false v (typeof a) → step ge (State f (Swhile a s) k e m) tr (State f Sskip k e m) | step_while_true: ∀f,a,s,k,e,m,v,tr. eval_expr ge e m a v tr → is_true v (typeof a) → step ge (State f (Swhile a s) k e m) tr (State f s (Kwhile a s k) e m) | step_skip_or_continue_while: ∀f,x,a,s,k,e,m. x = Sskip ∨ x = Scontinue → step ge (State f x (Kwhile a s k) e m) E0 (State f (Swhile a s) k e m) | step_break_while: ∀f,a,s,k,e,m. step ge (State f Sbreak (Kwhile a s k) e m) E0 (State f Sskip k e m) | step_dowhile: ∀f,a,s,k,e,m. step ge (State f (Sdowhile a s) k e m) E0 (State f s (Kdowhile a s k) e m) | step_skip_or_continue_dowhile_false: ∀f,x,a,s,k,e,m,v,tr. x = Sskip ∨ x = Scontinue → eval_expr ge e m a v tr → is_false v (typeof a) → step ge (State f x (Kdowhile a s k) e m) tr (State f Sskip k e m) | step_skip_or_continue_dowhile_true: ∀f,x,a,s,k,e,m,v,tr. x = Sskip ∨ x = Scontinue → eval_expr ge e m a v tr → is_true v (typeof a) → step ge (State f x (Kdowhile a s k) e m) tr (State f (Sdowhile a s) k e m) | step_break_dowhile: ∀f,a,s,k,e,m. step ge (State f Sbreak (Kdowhile a s k) e m) E0 (State f Sskip k e m) | step_for_start: ∀f,a1,a2,a3,s,k,e,m. a1 ≠ Sskip → step ge (State f (Sfor a1 a2 a3 s) k e m) E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m) | step_for_false: ∀f,a2,a3,s,k,e,m,v,tr. eval_expr ge e m a2 v tr → is_false v (typeof a2) → step ge (State f (Sfor Sskip a2 a3 s) k e m) tr (State f Sskip k e m) | step_for_true: ∀f,a2,a3,s,k,e,m,v,tr. eval_expr ge e m a2 v tr → is_true v (typeof a2) → step ge (State f (Sfor Sskip a2 a3 s) k e m) tr (State f s (Kfor2 a2 a3 s k) e m) | step_skip_or_continue_for2: ∀f,x,a2,a3,s,k,e,m. x = Sskip ∨ x = Scontinue → step ge (State f x (Kfor2 a2 a3 s k) e m) E0 (State f a3 (Kfor3 a2 a3 s k) e m) | step_break_for2: ∀f,a2,a3,s,k,e,m. step ge (State f Sbreak (Kfor2 a2 a3 s k) e m) E0 (State f Sskip k e m) | step_skip_for3: ∀f,a2,a3,s,k,e,m. step ge (State f Sskip (Kfor3 a2 a3 s k) e m) E0 (State f (Sfor Sskip a2 a3 s) k e m) | step_return_0: ∀f,k,e,m. fn_return f = Tvoid → step ge (State f (Sreturn (None ?)) k e m) E0 (Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))) | step_return_1: ∀f,a,k,e,m,v,tr. fn_return f ≠ Tvoid → eval_expr ge e m a v tr → step ge (State f (Sreturn (Some ? a)) k e m) tr (Returnstate v (call_cont k) (free_list m (blocks_of_env e))) | step_skip_call: ∀f,k,e,m. is_call_cont k → fn_return f = Tvoid → step ge (State f Sskip k e m) E0 (Returnstate Vundef k (free_list m (blocks_of_env e))) | step_switch: ∀f,a,sl,k,e,m,n,tr. eval_expr ge e m a (Vint n) tr → step ge (State f (Sswitch a sl) k e m) tr (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m) | step_skip_break_switch: ∀f,x,k,e,m. x = Sskip ∨ x = Sbreak → step ge (State f x (Kswitch k) e m) E0 (State f Sskip k e m) | step_continue_switch: ∀f,k,e,m. step ge (State f Scontinue (Kswitch k) e m) E0 (State f Scontinue k e m) | step_label: ∀f,lbl,s,k,e,m. step ge (State f (Slabel lbl s) k e m) E0 (State f s k e m) | step_goto: ∀f,lbl,k,e,m,s',k'. find_label lbl (fn_body f) (call_cont k) = Some ? 〈s', k'〉 → step ge (State f (Sgoto lbl) k e m) E0 (State f s' k' e m) | step_internal_function: ∀f,vargs,k,m,e,m1,m2. alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 → bind_parameters e m1 (fn_params f) vargs m2 → step ge (Callstate (CL_Internal f) vargs k m) E0 (State f (fn_body f) k e m2) | step_external_function: ∀id,targs,tres,vargs,k,m,vres,t. event_match (external_function id targs tres) vargs t vres → step ge (Callstate (CL_External id targs tres) vargs k m) t (Returnstate vres k m) | step_returnstate_0: ∀v,f,e,k,m. step ge (Returnstate v (Kcall (None ?) f e k) m) E0 (State f Sskip k e m) | step_returnstate_1: ∀v,f,e,k,m,m',loc,ofs,ty. store_value_of_type ty m loc ofs v = Some ? m' → step ge (Returnstate v (Kcall (Some ? 〈〈loc, ofs〉, ty〉) f e k) m) E0 (State f Sskip k e m') | step_cost: ∀f,lbl,s,k,e,m. step ge (State f (Scost lbl s) k e m) (Echarge lbl) (State f s k e m). (* (** * Alternate big-step semantics *) (** ** Big-step semantics for terminating statements and functions *) (** The execution of a statement produces an ``outcome'', indicating how the execution terminated: either normally or prematurely through the execution of a [break], [continue] or [return] statement. *) inductive outcome: Type[0] := | Out_break: outcome (**r terminated by [break] *) | Out_continue: outcome (**r terminated by [continue] *) | Out_normal: outcome (**r terminated normally *) | Out_return: option val -> outcome. (**r terminated by [return] *) inductive out_normal_or_continue : outcome -> Prop := | Out_normal_or_continue_N: out_normal_or_continue Out_normal | Out_normal_or_continue_C: out_normal_or_continue Out_continue. inductive out_break_or_return : outcome -> outcome -> Prop := | Out_break_or_return_B: out_break_or_return Out_break Out_normal | Out_break_or_return_R: ∀ov. out_break_or_return (Out_return ov) (Out_return ov). Definition outcome_switch (out: outcome) : outcome := match out with | Out_break => Out_normal | o => o end. Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop := match out, t with | Out_normal, Tvoid => v = Vundef | Out_return None, Tvoid => v = Vundef | Out_return (Some v'), ty => ty <> Tvoid /\ v'=v | _, _ => False end. (** [exec_stmt ge e m1 s t m2 out] describes the execution of the statement [s]. [out] is the outcome for this execution. [m1] is the initial memory state, [m2] the final memory state. [t] is the trace of input/output events performed during this evaluation. *) inductive exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := | exec_Sskip: ∀e,m. exec_stmt e m Sskip E0 m Out_normal | exec_Sassign: ∀e,m,a1,a2,loc,ofs,v2,m'. eval_lvalue e m a1 loc ofs -> eval_expr e m a2 v2 -> store_value_of_type (typeof a1) m loc ofs v2 = Some m' -> exec_stmt e m (Sassign a1 a2) E0 m' Out_normal | exec_Scall_none: ∀e,m,a,al,vf,vargs,f,t,m',vres. eval_expr e m a vf -> eval_exprlist e m al vargs -> Genv.find_funct ge vf = Some f -> type_of_fundef f = typeof a -> eval_funcall m f vargs t m' vres -> exec_stmt e m (Scall None a al) t m' Out_normal | exec_Scall_some: ∀e,m,lhs,a,al,loc,ofs,vf,vargs,f,t,m',vres,m''. eval_lvalue e m lhs loc ofs -> eval_expr e m a vf -> eval_exprlist e m al vargs -> Genv.find_funct ge vf = Some f -> type_of_fundef f = typeof a -> eval_funcall m f vargs t m' vres -> store_value_of_type (typeof lhs) m' loc ofs vres = Some m'' -> exec_stmt e m (Scall (Some lhs) a al) t m'' Out_normal | exec_Sseq_1: ∀e,m,s1,s2,t1,m1,t2,m2,out. exec_stmt e m s1 t1 m1 Out_normal -> exec_stmt e m1 s2 t2 m2 out -> exec_stmt e m (Ssequence s1 s2) (t1 ** t2) m2 out | exec_Sseq_2: ∀e,m,s1,s2,t1,m1,out. exec_stmt e m s1 t1 m1 out -> out <> Out_normal -> exec_stmt e m (Ssequence s1 s2) t1 m1 out | exec_Sifthenelse_true: ∀e,m,a,s1,s2,v1,t,m',out. eval_expr e m a v1 -> is_true v1 (typeof a) -> exec_stmt e m s1 t m' out -> exec_stmt e m (Sifthenelse a s1 s2) t m' out | exec_Sifthenelse_false: ∀e,m,a,s1,s2,v1,t,m',out. eval_expr e m a v1 -> is_false v1 (typeof a) -> exec_stmt e m s2 t m' out -> exec_stmt e m (Sifthenelse a s1 s2) t m' out | exec_Sreturn_none: ∀e,m. exec_stmt e m (Sreturn None) E0 m (Out_return None) | exec_Sreturn_some: ∀e,m,a,v. eval_expr e m a v -> exec_stmt e m (Sreturn (Some a)) E0 m (Out_return (Some v)) | exec_Sbreak: ∀e,m. exec_stmt e m Sbreak E0 m Out_break | exec_Scontinue: ∀e,m. exec_stmt e m Scontinue E0 m Out_continue | exec_Swhile_false: ∀e,m,a,s,v. eval_expr e m a v -> is_false v (typeof a) -> exec_stmt e m (Swhile a s) E0 m Out_normal | exec_Swhile_stop: ∀e,m,a,v,s,t,m',out',out. eval_expr e m a v -> is_true v (typeof a) -> exec_stmt e m s t m' out' -> out_break_or_return out' out -> exec_stmt e m (Swhile a s) t m' out | exec_Swhile_loop: ∀e,m,a,s,v,t1,m1,out1,t2,m2,out. eval_expr e m a v -> is_true v (typeof a) -> exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> exec_stmt e m1 (Swhile a s) t2 m2 out -> exec_stmt e m (Swhile a s) (t1 ** t2) m2 out | exec_Sdowhile_false: ∀e,m,s,a,t,m1,out1,v. exec_stmt e m s t m1 out1 -> out_normal_or_continue out1 -> eval_expr e m1 a v -> is_false v (typeof a) -> exec_stmt e m (Sdowhile a s) t m1 Out_normal | exec_Sdowhile_stop: ∀e,m,s,a,t,m1,out1,out. exec_stmt e m s t m1 out1 -> out_break_or_return out1 out -> exec_stmt e m (Sdowhile a s) t m1 out | exec_Sdowhile_loop: ∀e,m,s,a,m1,m2,t1,t2,out,out1,v. exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expr e m1 a v -> is_true v (typeof a) -> exec_stmt e m1 (Sdowhile a s) t2 m2 out -> exec_stmt e m (Sdowhile a s) (t1 ** t2) m2 out | exec_Sfor_start: ∀e,m,s,a1,a2,a3,out,m1,m2,t1,t2. a1 <> Sskip -> exec_stmt e m a1 t1 m1 Out_normal -> exec_stmt e m1 (Sfor Sskip a2 a3 s) t2 m2 out -> exec_stmt e m (Sfor a1 a2 a3 s) (t1 ** t2) m2 out | exec_Sfor_false: ∀e,m,s,a2,a3,v. eval_expr e m a2 v -> is_false v (typeof a2) -> exec_stmt e m (Sfor Sskip a2 a3 s) E0 m Out_normal | exec_Sfor_stop: ∀e,m,s,a2,a3,v,m1,t,out1,out. eval_expr e m a2 v -> is_true v (typeof a2) -> exec_stmt e m s t m1 out1 -> out_break_or_return out1 out -> exec_stmt e m (Sfor Sskip a2 a3 s) t m1 out | exec_Sfor_loop: ∀e,m,s,a2,a3,v,m1,m2,m3,t1,t2,t3,out1,out. eval_expr e m a2 v -> is_true v (typeof a2) -> exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> exec_stmt e m1 a3 t2 m2 Out_normal -> exec_stmt e m2 (Sfor Sskip a2 a3 s) t3 m3 out -> exec_stmt e m (Sfor Sskip a2 a3 s) (t1 ** t2 ** t3) m3 out | exec_Sswitch: ∀e,m,a,t,n,sl,m1,out. eval_expr e m a (Vint n) -> exec_stmt e m (seq_of_labeled_statement (select_switch n sl)) t m1 out -> exec_stmt e m (Sswitch a sl) t m1 (outcome_switch out) (** [eval_funcall m1 fd args t m2 res] describes the invocation of function [fd] with arguments [args]. [res] is the value returned by the call. *) with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := | eval_funcall_internal: ∀m,f,vargs,t,e,m1,m2,m3,out,vres. alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> bind_parameters e m1 f.(fn_params) vargs m2 -> exec_stmt e m2 f.(fn_body) t m3 out -> outcome_result_value out f.(fn_return) vres -> eval_funcall m (Internal f) vargs t (Mem.free_list m3 (blocks_of_env e)) vres | eval_funcall_external: ∀m,id,targs,tres,vargs,t,vres. event_match (external_function id targs tres) vargs t vres -> eval_funcall m (External id targs tres) vargs t m vres. Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop. (** ** Big-step semantics for diverging statements and functions *) (** Coinductive semantics for divergence. [execinf_stmt ge e m s t] holds if the execution of statement [s] diverges, i.e. loops infinitely. [t] is the possibly infinite trace of observable events performed during the execution. *) Coinductive execinf_stmt: env -> mem -> statement -> traceinf -> Prop := | execinf_Scall_none: ∀e,m,a,al,vf,vargs,f,t. eval_expr e m a vf -> eval_exprlist e m al vargs -> Genv.find_funct ge vf = Some f -> type_of_fundef f = typeof a -> evalinf_funcall m f vargs t -> execinf_stmt e m (Scall None a al) t | execinf_Scall_some: ∀e,m,lhs,a,al,loc,ofs,vf,vargs,f,t. eval_lvalue e m lhs loc ofs -> eval_expr e m a vf -> eval_exprlist e m al vargs -> Genv.find_funct ge vf = Some f -> type_of_fundef f = typeof a -> evalinf_funcall m f vargs t -> execinf_stmt e m (Scall (Some lhs) a al) t | execinf_Sseq_1: ∀e,m,s1,s2,t. execinf_stmt e m s1 t -> execinf_stmt e m (Ssequence s1 s2) t | execinf_Sseq_2: ∀e,m,s1,s2,t1,m1,t2. exec_stmt e m s1 t1 m1 Out_normal -> execinf_stmt e m1 s2 t2 -> execinf_stmt e m (Ssequence s1 s2) (t1 *** t2) | execinf_Sifthenelse_true: ∀e,m,a,s1,s2,v1,t. eval_expr e m a v1 -> is_true v1 (typeof a) -> execinf_stmt e m s1 t -> execinf_stmt e m (Sifthenelse a s1 s2) t | execinf_Sifthenelse_false: ∀e,m,a,s1,s2,v1,t. eval_expr e m a v1 -> is_false v1 (typeof a) -> execinf_stmt e m s2 t -> execinf_stmt e m (Sifthenelse a s1 s2) t | execinf_Swhile_body: ∀e,m,a,v,s,t. eval_expr e m a v -> is_true v (typeof a) -> execinf_stmt e m s t -> execinf_stmt e m (Swhile a s) t | execinf_Swhile_loop: ∀e,m,a,s,v,t1,m1,out1,t2. eval_expr e m a v -> is_true v (typeof a) -> exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> execinf_stmt e m1 (Swhile a s) t2 -> execinf_stmt e m (Swhile a s) (t1 *** t2) | execinf_Sdowhile_body: ∀e,m,s,a,t. execinf_stmt e m s t -> execinf_stmt e m (Sdowhile a s) t | execinf_Sdowhile_loop: ∀e,m,s,a,m1,t1,t2,out1,v. exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expr e m1 a v -> is_true v (typeof a) -> execinf_stmt e m1 (Sdowhile a s) t2 -> execinf_stmt e m (Sdowhile a s) (t1 *** t2) | execinf_Sfor_start_1: ∀e,m,s,a1,a2,a3,t. execinf_stmt e m a1 t -> execinf_stmt e m (Sfor a1 a2 a3 s) t | execinf_Sfor_start_2: ∀e,m,s,a1,a2,a3,m1,t1,t2. a1 <> Sskip -> exec_stmt e m a1 t1 m1 Out_normal -> execinf_stmt e m1 (Sfor Sskip a2 a3 s) t2 -> execinf_stmt e m (Sfor a1 a2 a3 s) (t1 *** t2) | execinf_Sfor_body: ∀e,m,s,a2,a3,v,t. eval_expr e m a2 v -> is_true v (typeof a2) -> execinf_stmt e m s t -> execinf_stmt e m (Sfor Sskip a2 a3 s) t | execinf_Sfor_next: ∀e,m,s,a2,a3,v,m1,t1,t2,out1. eval_expr e m a2 v -> is_true v (typeof a2) -> exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> execinf_stmt e m1 a3 t2 -> execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2) | execinf_Sfor_loop: ∀e,m,s,a2,a3,v,m1,m2,t1,t2,t3,out1. eval_expr e m a2 v -> is_true v (typeof a2) -> exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> exec_stmt e m1 a3 t2 m2 Out_normal -> execinf_stmt e m2 (Sfor Sskip a2 a3 s) t3 -> execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2 *** t3) | execinf_Sswitch: ∀e,m,a,t,n,sl. eval_expr e m a (Vint n) -> execinf_stmt e m (seq_of_labeled_statement (select_switch n sl)) t -> execinf_stmt e m (Sswitch a sl) t (** [evalinf_funcall ge m fd args t] holds if the invocation of function [fd] on arguments [args] diverges, with observable trace [t]. *) with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop := | evalinf_funcall_internal: ∀m,f,vargs,t,e,m1,m2. alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> bind_parameters e m1 f.(fn_params) vargs m2 -> execinf_stmt e m2 f.(fn_body) t -> evalinf_funcall m (Internal f) vargs t. End SEMANTICS. *) (* * * Whole-program semantics *) (* * Execution of whole programs are described as sequences of transitions from an initial state to a final state. An initial state is a [Callstate] corresponding to the invocation of the ``main'' function of the program without arguments and with an empty continuation. *) inductive initial_state (p: clight_program): state -> Prop := | initial_state_intro: ∀b,f,ge,m0. globalenv Genv ?? p = OK ? ge → init_mem Genv ?? p = OK ? m0 → find_symbol ?? ge (prog_main ?? p) = Some ? b → find_funct_ptr ?? ge b = Some ? f → initial_state p (Callstate f (nil ?) Kstop m0). (* * A final state is a [Returnstate] with an empty continuation. *) inductive final_state: state -> int -> Prop := | final_state_intro: ∀r,m. final_state (Returnstate (Vint r) Kstop m) r. (* * Execution of a whole program: [exec_program p beh] holds if the application of [p]'s main function to no arguments in the initial memory state for [p] has [beh] as observable behavior. *) definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh. ∀ge. globalenv ??? p = OK ? ge → program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh. (* (** Big-step execution of a whole program. *) inductive bigstep_program_terminates (p: program): trace -> int -> Prop := | bigstep_program_terminates_intro: ∀b,f,m1,t,r. let ge := Genv.globalenv p in let m0 := Genv.init_mem p in Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> eval_funcall ge m0 f nil t m1 (Vint r) -> bigstep_program_terminates p t r. inductive bigstep_program_diverges (p: program): traceinf -> Prop := | bigstep_program_diverges_intro: ∀b,f,t. let ge := Genv.globalenv p in let m0 := Genv.init_mem p in Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> evalinf_funcall ge m0 f nil t -> bigstep_program_diverges p t. (** * Implication from big-step semantics to transition semantics *) Section BIGSTEP_TO_TRANSITIONS. Variable prog: program. Let ge : genv := Genv.globalenv prog. Definition exec_stmt_eval_funcall_ind (PS: env -> mem -> statement -> trace -> mem -> outcome -> Prop) (PF: mem -> fundef -> list val -> trace -> mem -> val -> Prop) := fun a b c d e f g h i j k l m n o p q r s t u v w x y => conj (exec_stmt_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y) (eval_funcall_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y). inductive outcome_state_match (e: env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop := | osm_normal: outcome_state_match e m f k Out_normal (State f Sskip k e m) | osm_break: outcome_state_match e m f k Out_break (State f Sbreak k e m) | osm_continue: outcome_state_match e m f k Out_continue (State f Scontinue k e m) | osm_return_none: ∀k'. call_cont k' = call_cont k -> outcome_state_match e m f k (Out_return None) (State f (Sreturn None) k' e m) | osm_return_some: ∀a,v,k'. call_cont k' = call_cont k -> eval_expr ge e m a v -> outcome_state_match e m f k (Out_return (Some v)) (State f (Sreturn (Some a)) k' e m). Lemma is_call_cont_call_cont: ∀k. is_call_cont k -> call_cont k = k. Proof. destruct k; simpl; intros; contradiction || auto. Qed. Lemma exec_stmt_eval_funcall_steps: (∀e,m,s,t,m',out. exec_stmt ge e m s t m' out -> ∀f,k. exists S, star step ge (State f s k e m) t S /\ outcome_state_match e m' f k out S) /\ (∀m,fd,args,t,m',res. eval_funcall ge m fd args t m' res -> ∀k. is_call_cont k -> star step ge (Callstate fd args k m) t (Returnstate res k m')). Proof. apply exec_stmt_eval_funcall_ind; intros. (* skip *) econstructor; split. apply star_refl. constructor. (* assign *) econstructor; split. apply star_one. econstructor; eauto. constructor. (* call none *) econstructor; split. eapply star_left. econstructor; eauto. eapply star_right. apply H4. simpl; auto. econstructor. reflexivity. traceEq. constructor. (* call some *) econstructor; split. eapply star_left. econstructor; eauto. eapply star_right. apply H5. simpl; auto. econstructor; eauto. reflexivity. traceEq. constructor. (* sequence 2 *) destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. inv B1. destruct (H2 f k) as [S2 [A2 B2]]. econstructor; split. eapply star_left. econstructor. eapply star_trans. eexact A1. eapply star_left. constructor. eexact A2. reflexivity. reflexivity. traceEq. auto. (* sequence 1 *) destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. set (S2 := match out with | Out_break => State f Sbreak k e m1 | Out_continue => State f Scontinue k e m1 | _ => S1 end). exists S2; split. eapply star_left. econstructor. eapply star_trans. eexact A1. unfold S2; inv B1. congruence. apply star_one. apply step_break_seq. apply star_one. apply step_continue_seq. apply star_refl. apply star_refl. reflexivity. traceEq. unfold S2; inv B1; congruence || econstructor; eauto. (* ifthenelse true *) destruct (H2 f k) as [S1 [A1 B1]]. exists S1; split. eapply star_left. eapply step_ifthenelse_true; eauto. eexact A1. traceEq. auto. (* ifthenelse false *) destruct (H2 f k) as [S1 [A1 B1]]. exists S1; split. eapply star_left. eapply step_ifthenelse_false; eauto. eexact A1. traceEq. auto. (* return none *) econstructor; split. apply star_refl. constructor. auto. (* return some *) econstructor; split. apply star_refl. econstructor; eauto. (* break *) econstructor; split. apply star_refl. constructor. (* continue *) econstructor; split. apply star_refl. constructor. (* while false *) econstructor; split. apply star_one. eapply step_while_false; eauto. constructor. (* while stop *) destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]]. set (S2 := match out' with | Out_break => State f Sskip k e m' | _ => S1 end). exists S2; split. eapply star_left. eapply step_while_true; eauto. eapply star_trans. eexact A1. unfold S2. inversion H3; subst. inv B1. apply star_one. constructor. apply star_refl. reflexivity. traceEq. unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto. (* while loop *) destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]]. destruct (H5 f k) as [S2 [A2 B2]]. exists S2; split. eapply star_left. eapply step_while_true; eauto. eapply star_trans. eexact A1. eapply star_left. inv H3; inv B1; apply step_skip_or_continue_while; auto. eexact A2. reflexivity. reflexivity. traceEq. auto. (* dowhile false *) destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]]. exists (State f Sskip k e m1); split. eapply star_left. constructor. eapply star_right. eexact A1. inv H1; inv B1; eapply step_skip_or_continue_dowhile_false; eauto. reflexivity. traceEq. constructor. (* dowhile stop *) destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]]. set (S2 := match out1 with | Out_break => State f Sskip k e m1 | _ => S1 end). exists S2; split. eapply star_left. apply step_dowhile. eapply star_trans. eexact A1. unfold S2. inversion H1; subst. inv B1. apply star_one. constructor. apply star_refl. reflexivity. traceEq. unfold S2. inversion H1; subst. constructor. inv B1; econstructor; eauto. (* dowhile loop *) destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]]. destruct (H5 f k) as [S2 [A2 B2]]. exists S2; split. eapply star_left. apply step_dowhile. eapply star_trans. eexact A1. eapply star_left. inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto. eexact A2. reflexivity. reflexivity. traceEq. auto. (* for start *) destruct (H1 f (Kseq (Sfor Sskip a2 a3 s) k)) as [S1 [A1 B1]]. inv B1. destruct (H3 f k) as [S2 [A2 B2]]. exists S2; split. eapply star_left. apply step_for_start; auto. eapply star_trans. eexact A1. eapply star_left. constructor. eexact A2. reflexivity. reflexivity. traceEq. auto. (* for false *) econstructor; split. eapply star_one. eapply step_for_false; eauto. constructor. (* for stop *) destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]]. set (S2 := match out1 with | Out_break => State f Sskip k e m1 | _ => S1 end). exists S2; split. eapply star_left. eapply step_for_true; eauto. eapply star_trans. eexact A1. unfold S2. inversion H3; subst. inv B1. apply star_one. constructor. apply star_refl. reflexivity. traceEq. unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto. (* for loop *) destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]]. destruct (H5 f (Kfor3 a2 a3 s k)) as [S2 [A2 B2]]. inv B2. destruct (H7 f k) as [S3 [A3 B3]]. exists S3; split. eapply star_left. eapply step_for_true; eauto. eapply star_trans. eexact A1. eapply star_trans with (s2 := State f a3 (Kfor3 a2 a3 s k) e m1). inv H3; inv B1. apply star_one. constructor. auto. apply star_one. constructor. auto. eapply star_trans. eexact A2. eapply star_left. constructor. eexact A3. reflexivity. reflexivity. reflexivity. reflexivity. traceEq. auto. (* switch *) destruct (H1 f (Kswitch k)) as [S1 [A1 B1]]. set (S2 := match out with | Out_normal => State f Sskip k e m1 | Out_break => State f Sskip k e m1 | Out_continue => State f Scontinue k e m1 | _ => S1 end). exists S2; split. eapply star_left. eapply step_switch; eauto. eapply star_trans. eexact A1. unfold S2; inv B1. apply star_one. constructor. auto. apply star_one. constructor. auto. apply star_one. constructor. apply star_refl. apply star_refl. reflexivity. traceEq. unfold S2. inv B1; simpl; econstructor; eauto. (* call internal *) destruct (H2 f k) as [S1 [A1 B1]]. eapply star_left. eapply step_internal_function; eauto. eapply star_right. eexact A1. inv B1; simpl in H3; try contradiction. (* Out_normal *) assert (fn_return f = Tvoid /\ vres = Vundef). destruct (fn_return f); auto || contradiction. destruct H5. subst vres. apply step_skip_call; auto. (* Out_return None *) assert (fn_return f = Tvoid /\ vres = Vundef). destruct (fn_return f); auto || contradiction. destruct H6. subst vres. rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5. apply step_return_0; auto. (* Out_return Some *) destruct H3. subst vres. rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5. eapply step_return_1; eauto. reflexivity. traceEq. (* call external *) apply star_one. apply step_external_function; auto. Qed. Lemma exec_stmt_steps: ∀e,m,s,t,m',out. exec_stmt ge e m s t m' out -> ∀f,k. exists S, star step ge (State f s k e m) t S /\ outcome_state_match e m' f k out S. Proof (proj1 exec_stmt_eval_funcall_steps). Lemma eval_funcall_steps: ∀m,fd,args,t,m',res. eval_funcall ge m fd args t m' res -> ∀k. is_call_cont k -> star step ge (Callstate fd args k m) t (Returnstate res k m'). Proof (proj2 exec_stmt_eval_funcall_steps). Definition order (x y: unit) := False. Lemma evalinf_funcall_forever: ∀m,fd,args,T,k. evalinf_funcall ge m fd args T -> forever_N step order ge tt (Callstate fd args k m) T. Proof. cofix CIH_FUN. assert (∀e,m,s,T,f,k. execinf_stmt ge e m s T -> forever_N step order ge tt (State f s k e m) T). cofix CIH_STMT. intros. inv H. (* call none *) eapply forever_N_plus. apply plus_one. eapply step_call_none; eauto. apply CIH_FUN. eauto. traceEq. (* call some *) eapply forever_N_plus. apply plus_one. eapply step_call_some; eauto. apply CIH_FUN. eauto. traceEq. (* seq 1 *) eapply forever_N_plus. apply plus_one. econstructor. apply CIH_STMT; eauto. traceEq. (* seq 2 *) destruct (exec_stmt_steps _ _ _ _ _ _ H0 f (Kseq s2 k)) as [S1 [A1 B1]]. inv B1. eapply forever_N_plus. eapply plus_left. constructor. eapply star_trans. eexact A1. apply star_one. constructor. reflexivity. reflexivity. apply CIH_STMT; eauto. traceEq. (* ifthenelse true *) eapply forever_N_plus. apply plus_one. eapply step_ifthenelse_true; eauto. apply CIH_STMT; eauto. traceEq. (* ifthenelse false *) eapply forever_N_plus. apply plus_one. eapply step_ifthenelse_false; eauto. apply CIH_STMT; eauto. traceEq. (* while body *) eapply forever_N_plus. eapply plus_one. eapply step_while_true; eauto. apply CIH_STMT; eauto. traceEq. (* while loop *) destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kwhile a s0 k)) as [S1 [A1 B1]]. eapply forever_N_plus with (s2 := State f (Swhile a s0) k e m1). eapply plus_left. eapply step_while_true; eauto. eapply star_right. eexact A1. inv H3; inv B1; apply step_skip_or_continue_while; auto. reflexivity. reflexivity. apply CIH_STMT; eauto. traceEq. (* dowhile body *) eapply forever_N_plus. eapply plus_one. eapply step_dowhile. apply CIH_STMT; eauto. traceEq. (* dowhile loop *) destruct (exec_stmt_steps _ _ _ _ _ _ H0 f (Kdowhile a s0 k)) as [S1 [A1 B1]]. eapply forever_N_plus with (s2 := State f (Sdowhile a s0) k e m1). eapply plus_left. eapply step_dowhile. eapply star_right. eexact A1. inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto. reflexivity. reflexivity. apply CIH_STMT. eauto. traceEq. (* for start 1 *) assert (a1 <> Sskip). red; intros; subst. inv H0. eapply forever_N_plus. eapply plus_one. apply step_for_start; auto. apply CIH_STMT; eauto. traceEq. (* for start 2 *) destruct (exec_stmt_steps _ _ _ _ _ _ H1 f (Kseq (Sfor Sskip a2 a3 s0) k)) as [S1 [A1 B1]]. inv B1. eapply forever_N_plus. eapply plus_left. eapply step_for_start; eauto. eapply star_right. eexact A1. apply step_skip_seq. reflexivity. reflexivity. apply CIH_STMT; eauto. traceEq. (* for body *) eapply forever_N_plus. apply plus_one. eapply step_for_true; eauto. apply CIH_STMT; eauto. traceEq. (* for next *) destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]]. eapply forever_N_plus. eapply plus_left. eapply step_for_true; eauto. eapply star_trans. eexact A1. apply star_one. inv H3; inv B1; apply step_skip_or_continue_for2; auto. reflexivity. reflexivity. apply CIH_STMT; eauto. traceEq. (* for body *) destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]]. destruct (exec_stmt_steps _ _ _ _ _ _ H4 f (Kfor3 a2 a3 s0 k)) as [S2 [A2 B2]]. inv B2. eapply forever_N_plus. eapply plus_left. eapply step_for_true; eauto. eapply star_trans. eexact A1. eapply star_left. inv H3; inv B1; apply step_skip_or_continue_for2; auto. eapply star_right. eexact A2. constructor. reflexivity. reflexivity. reflexivity. reflexivity. apply CIH_STMT; eauto. traceEq. (* switch *) eapply forever_N_plus. eapply plus_one. eapply step_switch; eauto. apply CIH_STMT; eauto. traceEq. (* call internal *) intros. inv H0. eapply forever_N_plus. eapply plus_one. econstructor; eauto. apply H; eauto. traceEq. Qed. Theorem bigstep_program_terminates_exec: ∀t,r. bigstep_program_terminates prog t r -> exec_program prog (Terminates t r). Proof. intros. inv H. unfold ge0, m0 in *. econstructor. econstructor. eauto. eauto. apply eval_funcall_steps. eauto. red; auto. econstructor. Qed. Theorem bigstep_program_diverges_exec: ∀T. bigstep_program_diverges prog T -> exec_program prog (Reacts T) \/ exists t, exec_program prog (Diverges t) /\ traceinf_prefix t T. Proof. intros. inv H. set (st := Callstate f nil Kstop m0). assert (forever step ge0 st T). eapply forever_N_forever with (order := order). red; intros. constructor; intros. red in H. elim H. eapply evalinf_funcall_forever; eauto. destruct (forever_silent_or_reactive _ _ _ _ _ _ H) as [A | [t [s' [T' [B [C D]]]]]]. left. econstructor. econstructor. eauto. eauto. auto. right. exists t. split. econstructor. econstructor; eauto. eauto. auto. subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor. Qed. End BIGSTEP_TO_TRANSITIONS. *)