Module Csem


Require Import Arith.
Require Import Bool.
Require Import List.




Require Import Coqlib.
Require Import Values.
Require Import Pointers.
Require Import Integers.
Require Import Floats.
Require Import Events.
Require Import Ast.
Require Import Csyntax.
Require Import Globalenvs.
Require Import Errors.
Require Import Maps.
Require Import Libtactics.
Require Import Memcomp.
Require Import Mergesort.
Require Import Ctyping.

Module Clight.

The semantics uses two environments. The global environment maps names of functions and global variables to pointers, and function pointers to their definitions. (See module Globalenvs.)

Definition genv := Genv.t fundef.

The local environment maps local variables to pointers. *
Definition env := PTree.t pointer.
Definition empty_env: env := (PTree.empty pointer).

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: forall sz sg,
      is_false (Vint Int.zero) (Tint sz sg)
  | is_false_pointer: forall t,
      is_false (Vint Int.zero) (Tpointer t)
 | is_false_float: forall f sz,
      Float.cmp Ceq f Float.zero ->
      is_false (Vfloat f) (Tfloat sz).

Inductive is_true: val -> type -> Prop :=
  | is_true_int_int: forall n sz sg,
      n <> Int.zero ->
      is_true (Vint n) (Tint sz sg)
  | is_true_pointer_int: forall p sz sg,
      is_true (Vptr p) (Tint sz sg)
  | is_true_int_pointer: forall n t,
      n <> Int.zero ->
      is_true (Vint n) (Tpointer t)
  | is_true_pointer_pointer: forall p t,
      is_true (Vptr p) (Tpointer t)
 | is_true_float: forall f sz,
      Float.cmp Cne f Float.zero ->
      is_true (Vfloat f) (Tfloat sz).


Executable versions of the above

Definition eval_true (v: val) (ty: type) : {is_true v ty} + {~ is_true v ty}.
Proof.
  intros. destruct v; destruct ty;
  try (destruct (Int.eq_dec i Int.zero); subst);
  try (destruct (Float.cmp Cne f Float.zero) as [] _eqn: X);
  try (by right; intro H; inv H; try rewrite X in *; auto);
  try (by left; constructor; auto).
Defined.

Definition eval_false (v: val) (ty: type) : {is_false v ty} + {~ is_false v ty}.
Proof.
  intros. destruct v; destruct ty;
  try (destruct (Int.eq_dec i Int.zero); subst);
  try (destruct (Float.cmp Ceq f Float.zero) as [] _eqn: X);
  try (by right; intro H; inv H; try rewrite X in *; auto);
  try (by left; constructor; auto).
Defined.

Basic soundness property for booleans.

Lemma is_true_is_false_contr:
  forall v t,
    is_true v t -> is_false v t -> False.
Proof.
  intros v t IST ISF.
  inv IST; inv ISF; auto.
  by rewrite Float.cmp_ne_eq in H; case (negP H).
Qed.

Inductive bool_of_val : val -> type -> val -> Prop :=
  | bool_of_val_true: forall v ty,
         is_true v ty ->
         bool_of_val v ty Vtrue
  | bool_of_val_false: forall v ty,
        is_false v ty ->
        bool_of_val v ty Vfalse.

Definition blocks_of_env (e:env) : list pointer :=
   (List.map (@snd ident pointer) (PTree.elements e)).

Definition sorted_pointers_of_env (e:env) : list pointer :=
 let (l,_) := mergesort _
                (fun x y => Ple (fst x) (fst y))
                (fun x y z => Ple_trans (fst x) (fst y) (fst z))
                (fun x y => Ple_total (fst x) (fst y))
                (fun x y => ple (fst x) (fst y))
                (PTree.elements e)
 in List.map (fun idpk => (snd idpk)) l.


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.

Function sem_neg (v: val) (ty: type) : option val :=
  match ty with
  | Tint _ _ =>
      match v with
      | Vint n => Some (Vint (Int.neg n))
      | _ => None
      end
  | Tfloat _ =>
      match v with
      | Vfloat f => Some (Vfloat (Float.neg f))
      | _ => None
      end
  | _ => None
  end.

Function sem_notint (v: val) : option val :=
  match v with
  | Vint n => Some (Vint (Int.xor n Int.mone))
  | _ => None
  end.

Function sem_notbool (v: val) (ty: type) : option val :=
  match ty with
  | Tint _ _ =>
      match v with
      | Vint n => Some (Val.of_bool (Int.eq n Int.zero))
      | Vptr _ => Some Vfalse
      | _ => None
      end
  | Tpointer _ =>
      match v with
      | Vint n => Some (Val.of_bool (Int.eq n Int.zero))
      | Vptr _ => Some Vfalse
      | _ => None
      end
  | Tfloat _ =>
      match v with
      | Vfloat f => Some (Val.of_bool (Float.cmp Ceq f Float.zero))
      | _ => None
      end
  | _ => None
  end.

Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  match classify_add t1 t2 with
  | add_case_ii => (* integer addition *)
      match v1, v2 with
      | Vint n1, Vint n2 => Some (Vint (Int.add n1 n2))
      | _, _ => None
      end
  | add_case_ff => (* float addition *)
      match v1, v2 with
      | Vfloat n1, Vfloat n2 => Some (Vfloat (Float.add n1 n2))
      | _, _ => None
      end
  | add_case_pi ty => (* pointer plus integer *)
      match v1,v2 with
      | Vptr p, Vint n2 => Some (Vptr (Ptr.add p (Int.mul (Int.repr (sizeof ty)) n2)))
      | _, _ => None
      end
  | add_case_ip ty => (* integer plus pointer *)
      match v1,v2 with
      | Vint n1, Vptr p => Some (Vptr (Ptr.add p (Int.mul (Int.repr (sizeof ty)) n1)))
      | _, _ => None
      end
  | add_default => None
end.

Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  match classify_sub t1 t2 with
  | sub_case_ii => (* integer subtraction *)
      match v1,v2 with
      | Vint n1, Vint n2 => Some (Vint (Int.sub n1 n2))
      | _, _ => None
      end
  | sub_case_ff => (* float subtraction *)
      match v1,v2 with
      | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.sub f1 f2))
      | _, _ => None
      end
  | sub_case_pi ty => (* pointer minus *)
      match v1,v2 with
      | Vptr p, Vint n2 => Some (Vptr (Ptr.sub_int p (Int.mul (Int.repr (sizeof ty)) n2)))
      | _, _ => None
      end
  | sub_case_pp ty => (* pointer minus pointer *)
      match v1,v2 with
      | Vptr p1, Vptr p2 =>
          if zeq (Ptr.block p1) (Ptr.block p2) then
            if Int.eq (Int.repr (sizeof ty)) Int.zero then None
            else Some (Vint (Int.divu (Int.sub (Ptr.offset p1) (Ptr.offset p2))
                            (Int.repr (sizeof ty))))
          else None
      | _, _ => None
      end
  | sub_default => None
  end.
 
Function sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
 match classify_mul t1 t2 with
  | mul_case_ii =>
      match v1,v2 with
      | Vint n1, Vint n2 => Some (Vint (Int.mul n1 n2))
      | _, _ => None
      end
  | mul_case_ff =>
      match v1,v2 with
      | Vfloat f1, Vfloat f2 => Some (Vfloat (Float.mul f1 f2))
      | _, _ => None
      end
  | mul_default =>
      None
end.

Function sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
   match classify_div t1 t2 with
  | div_case_I32unsi =>
      match v1,v2 with
      | Vint n1, Vint n2 =>
          if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2))
      | _,_ => None
      end
  | div_case_ii =>
      match v1,v2 with
       | Vint n1, Vint n2 =>
          if Int.eq n2 Int.zero then None else Some (Vint(Int.divs n1 n2))
      | _,_ => None
      end
  | div_case_ff =>
      match v1,v2 with
      | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.div f1 f2))
      | _, _ => None
      end
  | div_default =>
      None
end.

Function sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
  match classify_mod t1 t2 with
  | mod_case_I32unsi =>
      match v1, v2 with
      | Vint n1, Vint n2 =>
          if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2))
      | _, _ => None
      end
  | mod_case_ii =>
      match v1,v2 with
      | Vint n1, Vint n2 =>
          if Int.eq n2 Int.zero then None else Some (Vint (Int.mods n1 n2))
      | _, _ => None
      end
  | mod_default =>
      None
  end.

Function sem_and (v1 v2: val) : option val :=
  match v1, v2 with
  | Vint n1, Vint n2 => Some (Vint(Int.and n1 n2))
  | _, _ => None
  end .

Function sem_or (v1 v2: val) : option val :=
  match v1, v2 with
  | Vint n1, Vint n2 => Some (Vint(Int.or n1 n2))
  | _, _ => None
  end.

Function sem_xor (v1 v2: val): option val :=
  match v1, v2 with
  | Vint n1, Vint n2 => Some (Vint(Int.xor n1 n2))
  | _, _ => None
  end.

Function sem_shl (v1 v2: val): option val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
     if Int.ltu n2 (Int.repr 32) then Some (Vint(Int.shl n1 n2)) else None
  | _, _ => None
  end.

Function sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val :=
  match classify_shr t1 t2 with
  | shr_case_I32unsi =>
      match v1,v2 with
      | Vint n1, Vint n2 =>
          if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None
      | _,_ => None
      end
   | shr_case_ii =>
      match v1,v2 with
      | Vint n1, Vint n2 =>
          if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None
      | _, _ => None
      end
   | shr_default=>
      None
   end.

Function sem_cmp_mismatch (c: comparison): option val :=
  match c with
  | Ceq => Some Vfalse
  | Cne => Some Vtrue
  | _ => None
  end.

Function sem_cmp (c:comparison)
                  (v1: val) (t1: type) (v2: val) (t2: type) : option val :=
  match classify_cmp t1 t2 with
  | cmp_case_I32unsi =>
      match v1,v2 with
      | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2))
      | _, _ => None
      end
  | cmp_case_ipip =>
      match v1,v2 with
      | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmp c n1 n2))
      | Vptr p1, Vptr p2 => Val.option_val_of_bool3 (Ptr.cmp c p1 p2)
      | Vptr p, Vint n =>
          if Int.eq n Int.zero then sem_cmp_mismatch c else None
      | Vint n, Vptr p =>
          if Int.eq n Int.zero then sem_cmp_mismatch c else None
      | _, _ => None
      end
  | cmp_case_ff =>
      match v1,v2 with
      | Vfloat f1, Vfloat f2 => Some (Val.of_bool (Float.cmp c f1 f2))
      | _, _ => None
      end
  | cmp_default => None
  end.

Definition sem_unary_operation
            (op: unary_operation) (v: val) (ty: type): option val :=
  match op with
  | Onotbool => sem_notbool v ty
  | Onotint => sem_notint v
  | Oneg => sem_neg v ty
  end.

Definition sem_binary_operation
    (op: binary_operation)
    (v1: val) (t1: type) (v2: val) (t2:type) : 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
  | One => sem_cmp Cne v1 t1 v2 t2
  | Olt => sem_cmp Clt v1 t1 v2 t2
  | Ogt => sem_cmp Cgt v1 t1 v2 t2
  | Ole => sem_cmp Cle v1 t1 v2 t2
  | Oge => sem_cmp Cge v1 t1 v2 t2
  end.

Definition valid_arg (op : binary_operation) (ty1 : type) (ty2 : type) (v : val) : bool :=
 match op with
 | Oadd => match ty1 with
           | (Tint _ _) => match ty2 with
                           | (Tpointer _) =>
                              match v with
                              | (Vint _) => true
                              | _ => false
                              end
                           | (Tarray t0 z) =>
                             match v with
                             | (Vint _) => true
                             | _ => false
                             end
                           | _ => true
                           end
            | (Tpointer _) => match v with
                              | (Vptr _) => true
                              | _ => false
                              end
            | _ => true
            end
 | Osub => match ty1 with
            | (Tpointer _) => match ty2 with
                              | (Tpointer _ ) =>
                                match v with
                                | (Vptr _ ) => true
                                | _ => false
                                end
                              | (Tarray t0 z) =>
                                match v with
                                | (Vptr _ ) => true
                                | _ => false
                                end
                              | _ => true
                              end
            | (Tarray t0 z) => match ty2 with
                               | (Tarray t1 z1) =>
                                 match v with
                                 | (Vptr _) => true
                                 | _ => false
                                 end
                               | _ => true
                              end
              | _ => true
             end
  | _ => true
 end.
                           
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.

Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
  match sz, sg with
  | I8, Signed => Int.sign_ext 8 i
  | I8, Unsigned => Int.zero_ext 8 i
  | I16, Signed => Int.sign_ext 16 i
  | I16, Unsigned => Int.zero_ext 16 i
  | I32, _ => i
  end.

Definition cast_int_float (si : signedness) (i: int) : float :=
  match si with
  | Signed => Float.floatofint i
  | Unsigned => Float.floatofintu i
  end.

Definition cast_float_int (si : signedness) (f: float) : int :=
  match si with
  | Signed => Float.intoffloat f
  | Unsigned => Float.intuoffloat f
  end.

Definition cast_float_float (sz: floatsize) (f: float) : float :=
  match sz with
  | F32 => Float.singleoffloat f
  | F64 => f
  end.

Inductive neutral_for_cast: type -> Prop :=
  | nfc_int: forall sg,
      neutral_for_cast (Tint I32 sg)
  | nfc_ptr: forall ty,
      neutral_for_cast (Tpointer ty)
  | nfc_array: forall ty sz,
      neutral_for_cast (Tarray ty sz)
  | nfc_fun: forall targs tres,
      neutral_for_cast (Tfunction targs tres).

Inductive cast : val -> type -> type -> val -> Prop :=
  | cast_ii: forall i sz2 sz1 si1 si2, (* int to int *)
      cast (Vint i) (Tint sz1 si1) (Tint sz2 si2)
           (Vint (cast_int_int sz2 si2 i))
  | cast_fi: forall f sz1 sz2 si2, (* float to int *)
      cast (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
           (Vint (cast_int_int sz2 si2 (cast_float_int si2 f)))
  | cast_if: forall i sz1 sz2 si1, (* int to float *)
      cast (Vint i) (Tint sz1 si1) (Tfloat sz2)
          (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
  | cast_ff: forall f sz1 sz2, (* float to float *)
      cast (Vfloat f) (Tfloat sz1) (Tfloat sz2)
           (Vfloat (cast_float_float sz2 f))
  | cast_nn_p: forall p t1 t2, (* no change in data representation *)
      neutral_for_cast t1 -> neutral_for_cast t2 ->
      cast (Vptr p) t1 t2 (Vptr p)
  | cast_nn_i: forall n t1 t2, (* no change in data representation *)
      neutral_for_cast t1 -> neutral_for_cast t2 ->
      cast (Vint n) t1 t2 (Vint n).


load_value_of_type ty v p computes the value v of a datum of type ty addressed by pointer p. If the type ty indicates an access by value, the value is returned. If the type ty indicates an access by reference, the pointer value Vptr p is returned.

Definition load_value_of_type (ty_dest : type) (v: val) (p: pointer): option val :=
  match (access_mode ty_dest) with
  | By_value chunk => Some v
  | By_reference => Some (Vptr p)
  | By_nothing => None
  end.

Selection of the appropriate case of a switch, given the value n of the selector expression.

Fixpoint select_switch (n: int) (sl: labeled_statements)
                       {struct sl}: labeled_statements :=
  match sl with
  | LSdefault _ => sl
  | LScase c s sl' => if Int.eq c n then sl else select_switch n sl'
  end.


Turn a labeled statement into a sequence

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

Definition sem_atomic_statement
  (astmt : atomic_statement) (args : list val) : option (pointer * rmw_instr) :=
  match astmt, args with
    | AScas, Vptr p :: n :: o :: nil =>
        if (Val.eq_dec o Vundef)
          then None
            else if (Val.has_type o Ast.Tint)
              then if (Val.eq_dec n Vundef)
                then None
                else if (Val.has_type n Ast.Tint)
                  then Some (p, rmw_CAS o n)
                  else None
              else None
    | ASlkinc, Vptr p :: nil => Some (p, rmw_ADD (Vint Int.one))
    | _, _ => None
  end.



Continuations *

Section CONT.




Inductive cont : Type :=
 | Kstop : cont
 | Kseq : statement -> cont -> cont
 | Kwhile : expr -> statement -> cont -> cont
 | Kdowhile : statement -> expr -> cont -> cont
 | KforIncr : expr -> statement -> statement -> cont -> cont
 | KforCond : expr -> statement -> statement -> cont -> cont
 | Kcall : opt_lhs -> fundef -> env -> cont -> cont
 | Kswitch : cont -> cont
 | Kfree : list pointer -> option val -> cont -> cont.

Inductive expr_cont : Type :=
 | EKunop : unary_operation -> type -> expr_cont -> expr_cont
 | EKbinop1 : binary_operation -> type -> type -> type -> expr -> expr_cont -> expr_cont
 | EKbinop2 : binary_operation -> type -> type -> type -> val -> expr_cont -> expr_cont
 | EKcast : type -> type -> expr_cont -> expr_cont
 | EKcondition : expr -> expr -> type -> expr_cont -> expr_cont
 | EKfield : Z -> expr_cont -> expr_cont
 | EKlval : type -> expr_cont -> expr_cont
 | EKassign1 : expr -> type -> cont -> expr_cont
 | EKassign2 : val -> type -> cont -> expr_cont
 | EKcall : opt_lhs -> type -> es -> cont -> expr_cont
 | EKargs : opt_lhs -> val -> type -> list val -> es -> cont -> expr_cont
 | EKatargs : opt_lhs -> atomic_statement -> list val -> es -> cont -> expr_cont
 | EKcond : type -> statement -> statement -> cont -> expr_cont
 | EKwhile : expr -> statement -> cont -> expr_cont
 | EKdowhile : statement -> expr -> cont -> expr_cont
 | EKforTest : expr -> statement -> statement -> cont -> expr_cont
 | EKreturn : cont -> expr_cont
 | EKswitch : labeled_statements -> cont -> expr_cont
 | EKthread1 : expr -> cont -> expr_cont
 | EKthread2 : pointer -> cont -> expr_cont .

Inductive state : Type :=
 | SKlval : expr -> env -> expr_cont -> state
 | SKexpr : expr -> env -> expr_cont -> state
 | SKval : val -> env -> expr_cont -> state
 | SKstmt : statement -> env -> cont -> state
 | SKcall : list val -> cont -> state
 | SKbind : function -> list val -> list (ident*type) -> env -> cont -> state
 | SKalloc : list val -> list (ident*type) -> env -> cont -> state
 | SKExternal : fundef -> opt_lhs -> env -> cont -> state
 | SKoptstorevar : opt_lhs -> val -> env -> cont -> state.

Pop continuation until a call or stop

 
Fixpoint call_cont (k: cont) : cont :=
  match k with
  | Kseq s k => call_cont k
  | Kwhile e s k => call_cont k
  | Kdowhile s e k => call_cont k
  | KforIncr e s1 s2 k => call_cont k
  | KforCond e s1 s2 k => call_cont k
  | Kswitch k => call_cont k
  | Kfree p vo k => call_cont k
  | _ => k
  end.

Definition is_call_cont (k: cont) : bool :=
  match k with
  | Kstop => true
  | Kcall _ _ _ _ => true
  | _ => false
  end.

Definition get_fundef (k: cont) : option fundef :=
  match k with
   | Kcall op fd e k => (Some fd)
   | _ => None
  end.

End CONT.

Section STEP.

Variable ge: genv.


Find the statement corresponding to a label

Fixpoint find_label (lbl: label) (s: statement) (k: cont)
                    {struct 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
      end
  | Sifthenelse a s1 s2 =>
      match find_label lbl s1 k with
      | Some sk => Some sk
      | None => find_label lbl s2 k
      end
  | Swhile a s1 =>
      find_label lbl s1 (Kwhile a s1 k)
  | Sdowhile a s1 =>
      find_label lbl s1 (Kdowhile s1 a k)
  | Sfor s1 e2 s3 s =>
      match find_label lbl s1 (KforCond e2 s3 s k) with
      | Some sk => Some sk
      | None =>
          match find_label lbl s (KforIncr e2 s3 s k) with
          | Some sk => Some sk
          | None => find_label lbl s3 (KforCond e2 s3 s k)
          end
      end
  | Sswitch e sl =>
      find_label_ls lbl sl (Kswitch k)
  | Slabel lbl' s' =>
      if ident_eq lbl lbl' then Some(s', k) else find_label lbl s' k
  | _ => None
  end

with find_label_ls (lbl: label) (sl: labeled_statements) (k: cont)
                    {struct 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
      end
  end.

Definition type_to_chunk (ty : type) :=
  match (access_mode ty) with
  | By_value chunk => (Some chunk)
  | _ => None
 end.

Definition cl_init (p : pointer) (vs : list val) : option state :=
  match Genv.find_funct_ptr ge p with
   | Some (Internal f) =>
       if beq_nat (length vs) (length f.(fn_params))
         then Some (SKcall (Val.conv_list vs (typlist_of_typelist (type_of_params f.(fn_params))))
                           (Kcall None (Internal f) empty_env Kstop))
         else None
   | _ => None
  end.



definitions

Inductive cl_step : state -> thread_event -> state -> Prop :=

 | StepConstInt : forall (n:int) (ty:type) (ek:expr_cont) (env:env),
     cl_step (SKexpr (Expr (Econst_int n) ty) env ek )
              TEtau
              (SKval (Vint n) env ek )

 | StepConstFloat : forall (f:float) (ty:type) (ek:expr_cont) (env:env),
     cl_step (SKexpr (Expr (Econst_float f) ty) env ek )
              TEtau
              (SKval (Vfloat f) env ek )

 | StepVarExprByValue : forall (id:ident) (ty:type) (ek:expr_cont) (env:env),
     cl_step (SKexpr (Expr (Evar id) ty) env ek )
              TEtau
              (SKlval (Expr (Evar id) ty) env (EKlval ty ek) )

 | StepVarLocal : forall (id:ident) (ty:type) (ek:expr_cont) (env:env) (p:pointer),
     env!id = Some p ->
     cl_step (SKlval (Expr (Evar id) ty) env ek )
              TEtau
              (SKval (Vptr p) env ek )

 | StepVarGlobal : forall (id:ident) (ty:type) (ek:expr_cont) (env:env) (p:pointer),
     env!id = None ->
     Genv.find_symbol ge id = Some p ->
     cl_step (SKlval (Expr (Evar id) ty) env ek )
              TEtau
              (SKval (Vptr p) env ek )

 | StepLoadByValue : forall (p:pointer) (ty':type) (ek:expr_cont) (env:env) (c:memory_chunk) (v:val) (typ:typ),
     access_mode ty' = By_value c ->
     typ = type_of_chunk c ->
     Val.has_type v typ ->
     cl_step (SKval (Vptr p) env (EKlval ty' ek) ) (TEmem (MEread p c v) ) (SKval v env ek )

 | StepLoadNotByValue : forall (p:pointer) (ty':type) (ek:expr_cont) (env:env),
     access_mode ty' = By_reference \/ access_mode ty' = By_nothing ->
     cl_step (SKval (Vptr p) env (EKlval ty' ek) )
              TEtau
              (SKval (Vptr p) env ek )

 | StepAddr : forall (e:expr) (ty:type) (ek:expr_cont) (env:env),
     cl_step (SKexpr (Expr (Eaddrof e) ty) env ek )
              TEtau
              (SKlval e env ek )

 | StepEcondition : forall (e1 e2 e3:expr) (ty:type) (ek:expr_cont) (env:env),
     cl_step (SKexpr (Expr (Econdition e1 e2 e3) ty) env ek )
              TEtau
              (SKexpr e1 env (EKcondition e2 e3 (typeof e1 ) ek ) )

 | StepEconditiontrue : forall (v:val) (ty:type) (e2 e3:expr) (ek:expr_cont) (env:env),
      is_true v ty ->
     cl_step (SKval v env (EKcondition e2 e3 ty ek ) )
              TEtau
              (SKexpr e2 env ek )

 | StepEconditionfalse : forall (v:val) (ty:type) (e2 e3:expr) (ek:expr_cont) (env:env),
      is_false v ty ->
     cl_step (SKval v env (EKcondition e2 e3 ty ek ) )
              TEtau
              (SKexpr e3 env ek )

 | StepDeref : forall (e:expr) (ty:type) (ek:expr_cont) (env:env),
     cl_step (SKexpr (Expr (Ederef e) ty) env ek )
              TEtau
              (SKexpr e env (EKlval ty ek) )

 | StepDerefLval : forall (e:expr) (ty:type) (ek:expr_cont) (env:env),
     cl_step (SKlval (Expr (Ederef e) ty) env ek )
              TEtau
              (SKexpr e env ek )

 | StepField : forall (e:expr) (id:ident) (ty:type) (ek:expr_cont) (env:env),
     cl_step (SKexpr (Expr (Efield e id) ty) env ek )
              TEtau
              (SKlval (Expr (Efield e id) ty) env (EKlval ty ek) )

 | StepFstruct1 : forall (e:expr) (id:ident) (ty:type) (ek:expr_cont) (env:env) (delta:Z) (id':ident) (phi:fieldlist),
       (typeof e ) = (Tstruct id' phi) ->
     field_offset id phi = OK delta ->
     cl_step (SKlval (Expr (Efield e id) ty) env ek )
              TEtau
              (SKlval e env (EKfield delta ek) )

 | StepFstruct2 : forall (p:pointer) (delta:Z) (ek:expr_cont) (env:env) (p':pointer),
     p' = Ptr.add p (Int.repr delta) ->
     cl_step (SKval (Vptr p) env (EKfield delta ek) )
              TEtau
              (SKval (Vptr p') env ek )

 | StepFunion : forall (e:expr) (id:ident) (ty:type) (ek:expr_cont) (env:env) (id':ident) (phi:fieldlist),
       (typeof e ) = (Tunion id' phi) ->
     cl_step (SKlval (Expr (Efield e id) ty) env ek )
              TEtau
              (SKlval e env ek )

 | StepSizeOf : forall (ty' ty:type) (ek:expr_cont) (env:env) (v:val),
     v=Vint (Int.repr (sizeof ty')) ->
     cl_step (SKexpr (Expr (Esizeof ty') ty) env ek )
              TEtau
              (SKval v env ek )

 | StepUnop1 : forall (op1:unary_operation) (e:expr) (ty:type) (ek:expr_cont) (env:env),
     cl_step (SKexpr (Expr (Eunop op1 e) ty) env ek )
              TEtau
              (SKexpr e env (EKunop op1 (typeof e ) ek ) )

 | StepUnop : forall (v:val) (op1:unary_operation) (ty:type) (ek:expr_cont) (env:env) (v':val),
     sem_unary_operation op1 v ty = Some v' ->
     cl_step (SKval v env (EKunop op1 ty ek ) )
              TEtau
              (SKval v' env ek )

 | StepBinop1 : forall (e1:expr) (op2:binary_operation) (e2:expr) (ty:type) (ek:expr_cont) (env:env),
     cl_step (SKexpr (Expr ( (Ebinop op2 e1 e2 ) ) ty) env ek )
              TEtau
              (SKexpr e1 env (EKbinop1 op2 (typeof e1 ) (typeof e2 ) ty e2 ek ) )

 | StepBinop2 : forall (v:val) (op2:binary_operation) (ty1 ty2 ty:type) (e2:expr) (ek:expr_cont) (env:env),
     valid_arg op2 ty1 ty2 v = true ->
     cl_step (SKval v env (EKbinop1 op2 ty1 ty2 ty e2 ek ) )
              TEtau
              (SKexpr e2 env (EKbinop2 op2 ty1 ty2 ty v ek ) )

 | StepBinop : forall (v2 v1:val) (op2:binary_operation) (ty1 ty2 ty:type) (ek:expr_cont) (env:env) (v:val),
     sem_binary_operation op2 v1 ty1 v2 ty2 = Some v ->
     cl_step (SKval v2 env (EKbinop2 op2 ty1 ty2 ty v1 ek ) )
              TEtau
              (SKval v env ek )

 | StepCast1 : forall (ty:type) (e:expr) (ty':type) (ek:expr_cont) (env:env),
     cl_step (SKexpr (Expr (Ecast ty e) ty') env ek )
              TEtau
              (SKexpr e env (EKcast (typeof e ) ty ek ) )

 | StepCast2 : forall (v:val) (ty ty':type) (ek:expr_cont) (env:env) (v':val),
     cast v ty' ty v' ->
     cl_step (SKval v env (EKcast ty' ty ek ) )
              TEtau
              (SKval v' env ek )

 | StepAndbool : forall (e1 e2:expr) (ty:type) (ek:expr_cont) (env:env) (n1 n0:int),
     n0 = Int.repr 0 ->
     n1 = Int.repr 1 ->
     cl_step (SKexpr (Expr (Eandbool e1 e2) ty) env ek )
              TEtau
              (SKexpr (Expr (Econdition e1 ( (Expr (Econdition e2 ( (Expr (Econst_int n1) ty) ) ( (Expr (Econst_int n0) ty) ) ) ty) ) (Expr (Econst_int n0) ty)) ty) env ek )

 | StepOrbool : forall (e1 e2:expr) (ty:type) (ek:expr_cont) (env:env) (n1 n0:int),
     n0 = Int.repr 0 ->
     n1 = Int.repr 1 ->
     cl_step (SKexpr (Expr (Eorbool e1 e2) ty) env ek )
              TEtau
              (SKexpr (Expr (Econdition e1 ( (Expr (Econst_int n1) ty) ) ( (Expr (Econdition e2 ( (Expr (Econst_int n1) ty) ) ( (Expr (Econst_int n0) ty) ) ) ty) ) ) ty) env ek )

 | StepThread : forall (e1 e2:expr) (k:cont) (env:env),
     cl_step (SKstmt (Sthread_create e1 e2) env k )
              TEtau
              (SKexpr e1 env (EKthread1 e2 k ) )

 | StepThreadFn : forall (p:pointer) (e2:expr) (k:cont) (env:env),
     cl_step (SKval (Vptr p) env (EKthread1 e2 k ) )
              TEtau
              (SKexpr e2 env (EKthread2 p k ) )

 | StepThreadEvt : forall (v:val) (p:pointer) (k:cont) (env:env),
     cl_step (SKval v env (EKthread2 p k ) ) (TEstart p ( v :: nil ) ) (SKstmt Sskip env k )

 | StepAssign1 : forall (e1 e2:expr) (k:cont) (env:env),
     cl_step (SKstmt (Sassign e1 e2) env k )
              TEtau
              (SKlval e1 env (EKassign1 e2 (typeof e1 ) k ) )

 | StepAssign2 : forall (v1:val) (ty:type) (e2:expr) (k:cont) (env:env),
     cl_step (SKval v1 env (EKassign1 e2 ty k ) )
              TEtau
              (SKexpr e2 env (EKassign2 v1 ty k ) )

 | StepAssign : forall (v1:val) (p1:pointer) (ty1:type) (k:cont) (env:env) (c:memory_chunk) (v2:val),
     type_to_chunk ty1 = Some c ->
     cast_value_to_chunk c v1 = v2 ->
     cl_step (SKval v1 env (EKassign2 (Vptr p1) ty1 k ) ) (TEmem (MEwrite p1 c v2) ) (SKstmt Sskip env k )

 | StepSeq : forall (s1 s2:statement) (k:cont) (env:env),
     cl_step (SKstmt (Ssequence s1 s2) env k )
              TEtau
              (SKstmt s1 env (Kseq s2 k) )

 | StepCall : forall (opt_lhs:opt_lhs) (e':expr) (es:es) (k:cont) (env:env),
     cl_step (SKstmt (Scall opt_lhs e' es) env k )
              TEtau
              (SKexpr e' env (EKcall opt_lhs (typeof e' ) es k) )

 | StepCallargsnone : forall (v:val) (opt_lhs:opt_lhs) (ty:type) (k:cont) (env:env) (fd:fundef),
     Genv.find_funct ge v = Some fd ->
     type_of_fundef fd = ty ->
     cl_step (SKval v env (EKcall opt_lhs ty nil k) )
              TEtau
             (SKcall nil (Kcall opt_lhs fd env k))

 | StepCallArgs1 : forall (v:val) (opt_lhs:opt_lhs) (ty:type) (e:expr) (es:es) (k:cont) (env:env),
     cl_step (SKval v env (EKcall opt_lhs ty ( e :: es ) k) )
              TEtau
              (SKexpr e env (EKargs opt_lhs v ty nil es k ) )

 | StepCallArgs2 : forall (v1:val) (opt_lhs:opt_lhs) (v:val) (ty:type) (vs:list val) (e:expr) (es:es) (k:cont) (env:env),
     cl_step (SKval v1 env (EKargs opt_lhs v ty vs ( e :: es ) k ) )
              TEtau
              (SKexpr e env (EKargs opt_lhs v ty (List.app vs ( v1 ::nil)) es k ) )

 | StepCallFinish : forall (v':val) (opt_lhs:opt_lhs) (v:val) (ty:type) (vs:list val) (k:cont) (env:env) (fd:fundef),
     Genv.find_funct ge v = Some fd ->
     type_of_fundef fd = ty ->
     cl_step (SKval v' env (EKargs opt_lhs v ty vs nil k ) )
              TEtau
             (SKcall (List.app vs ( v' ::nil)) (Kcall opt_lhs fd env k))

 | StepAtomic : forall (opt_lhs:opt_lhs) (astmt:atomic_statement) (e:expr) (es:es) (k:cont) (env:env),
     cl_step (SKstmt (Satomic opt_lhs astmt ( e :: es ) ) env k )
              TEtau
              (SKexpr e env (EKatargs opt_lhs astmt nil es k ) )

 | StepAtomicArgs : forall (v:val) (opt_lhs:opt_lhs) (astmt:atomic_statement) (vs:list val) (e:expr) (es:es) (k:cont) (env:env),
     cl_step (SKval v env (EKatargs opt_lhs astmt vs ( e :: es ) k ) )
              TEtau
              (SKexpr e env (EKatargs opt_lhs astmt (List.app vs ( v ::nil)) es k ) )

 | StepAtomicFinishNone : forall (v:val) (astmt:atomic_statement) (vs:list val) (k:cont) (env:env) (p:pointer) (v':val) (rmwi:rmw_instr),
     sem_atomic_statement astmt ( vs ++ v :: nil ) = Some (p, rmwi) ->
     Val.has_type v' (type_of_chunk Mint32) ->
     cl_step (SKval v env (EKatargs None astmt vs nil k ) ) (TEmem (MErmw p Mint32 v' rmwi) ) (SKstmt Sskip env k )

 | StepAtomicFinishSome : forall (v:val) (id:ident) (ty:type) (astmt:atomic_statement) (vs:list val) (k:cont) (env:env) (p:pointer) (v':val) (rmwi:rmw_instr),
     sem_atomic_statement astmt ( vs ++ v :: nil ) = Some (p, rmwi) ->
     Val.has_type v' (type_of_chunk Mint32) ->
     cl_step (SKval v env (EKatargs (Some ( id , ty )) astmt vs nil k ) ) (TEmem (MErmw p Mint32 v' rmwi) ) (SKoptstorevar (Some ( id , ty )) v' env k )

 | StepFence : forall (k:cont) (env:env),
     cl_step (SKstmt Smfence env k ) (TEmem MEfence) (SKstmt Sskip env k )

 | StepContinue : forall (s:statement) (k:cont) (env:env),
     cl_step (SKstmt Scontinue env (Kseq s k) )
              TEtau
              (SKstmt Scontinue env k )

 | StepBreak : forall (s:statement) (k:cont) (env:env),
     cl_step (SKstmt Sbreak env (Kseq s k) )
              TEtau
              (SKstmt Sbreak env k )

 | StepIfThenElse : forall (e:expr) (s1 s2:statement) (k:cont) (env:env),
     cl_step (SKstmt (Sifthenelse e s1 s2) env k )
              TEtau
              (SKexpr e env (EKcond (typeof e ) s1 s2 k ) )

 | StepIfThenElseTrue : forall (v:val) (ty:type) (s1 s2:statement) (k:cont) (env:env),
      is_true v ty ->
     cl_step (SKval v env (EKcond ty s1 s2 k ) )
              TEtau
              (SKstmt s1 env k )

 | StepIfThenElseFalse : forall (v:val) (ty:type) (s1 s2:statement) (k:cont) (env:env),
      is_false v ty ->
     cl_step (SKval v env (EKcond ty s1 s2 k ) )
              TEtau
              (SKstmt s2 env k )

 | StepWhile : forall (e:expr) (s:statement) (k:cont) (env:env),
     cl_step (SKstmt (Swhile e s) env k )
              TEtau
              (SKexpr e env (EKwhile e s k ) )

 | StepWhileTrue : forall (v:val) (e:expr) (s:statement) (k:cont) (env:env),
      is_true v (typeof e ) ->
     cl_step (SKval v env (EKwhile e s k ) )
              TEtau
              (SKstmt s env (Kwhile e s k) )

 | StepWhileFalse : forall (v:val) (e:expr) (s:statement) (k:cont) (env:env),
      is_false v (typeof e ) ->
     cl_step (SKval v env (EKwhile e s k ) )
              TEtau
              (SKstmt Sskip env k )

 | StepContinueWhile : forall (e:expr) (s:statement) (k:cont) (env:env),
     cl_step (SKstmt Scontinue env (Kwhile e s k) )
              TEtau
              (SKstmt (Swhile e s) env k )

 | StepBreakWhile : forall (e:expr) (s:statement) (k:cont) (env:env),
     cl_step (SKstmt Sbreak env (Kwhile e s k) )
              TEtau
              (SKstmt Sskip env k )

 | StepDoWhile : forall (s:statement) (e:expr) (k:cont) (env:env),
     cl_step (SKstmt (Sdowhile e s ) env k )
              TEtau
              (SKstmt s env (Kdowhile s e k) )

 | StepDoWhileTrue : forall (v:val) (s:statement) (e:expr) (k:cont) (env:env),
      is_true v (typeof e ) ->
     cl_step (SKval v env (EKdowhile s e k ) )
              TEtau
              (SKstmt (Sdowhile e s ) env k )

 | StepDoWhileFalse : forall (v:val) (s:statement) (e:expr) (k:cont) (env:env),
      is_false v (typeof e ) ->
     cl_step (SKval v env (EKdowhile s e k ) )
              TEtau
              (SKstmt Sskip env k )

 | StepDoContinueWhile : forall (s:statement) (e:expr) (k:cont) (env:env),
     cl_step (SKstmt Scontinue env (Kdowhile s e k) )
              TEtau
              (SKexpr e env (EKdowhile s e k ) )

 | StepDoBreakWhile : forall (s:statement) (e:expr) (k:cont) (env:env),
     cl_step (SKstmt Sbreak env (Kdowhile s e k) )
              TEtau
              (SKstmt Sskip env k )

 | StepForInit : forall (s1:statement) (e2:expr) (s3 s:statement) (k:cont) (env:env),
     cl_step (SKstmt (Sfor s1 e2 s3 s) env k )
              TEtau
              (SKstmt s1 env (KforCond e2 s3 s k) )

 | StepForCond : forall (e2:expr) (s3 s:statement) (k:cont) (env:env),
     cl_step (SKstmt Sskip env (KforCond e2 s3 s k) )
              TEtau
              (SKexpr e2 env (EKforTest e2 s3 s k ) )

 | StepForTrue : forall (v:val) (e2:expr) (s3 s:statement) (k:cont) (env:env),
      is_true v (typeof e2 ) ->
     cl_step (SKval v env (EKforTest e2 s3 s k ) )
              TEtau
              (SKstmt s env (KforIncr e2 s3 s k) )

 | StepForFalse : forall (v:val) (e2:expr) (s3 s:statement) (k:cont) (env:env),
      is_false v (typeof e2 ) ->
     cl_step (SKval v env (EKforTest e2 s3 s k ) )
              TEtau
              (SKstmt Sskip env k )

 | StepForIncr : forall (e2:expr) (s3 s:statement) (k:cont) (env:env),
     cl_step (SKstmt Sskip env (KforIncr e2 s3 s k) )
              TEtau
              (SKstmt s3 env (KforCond e2 s3 s k) )

 | StepForBreak : forall (e2:expr) (s3 s:statement) (k:cont) (env:env),
     cl_step (SKstmt Sbreak env (KforIncr e2 s3 s k) )
              TEtau
              (SKstmt Sskip env k )

 | StepForContinue : forall (e2:expr) (s3 s:statement) (k:cont) (env:env),
     cl_step (SKstmt Scontinue env (KforIncr e2 s3 s k) )
              TEtau
              (SKstmt s3 env (KforCond e2 s3 s k) )

 | StepReturnNone : forall (k:cont) (envp:env) (ps:list pointer) (fn:function) (envpp:env) (k':cont),
     call_cont k = (Kcall None (Internal fn) envpp k') ->
     fn.(fn_return) = Tvoid ->
     ps = sorted_pointers_of_env envp ->
     cl_step (SKstmt (Sreturn None ) envp k )
              TEtau
              (SKstmt Sskip envp (Kfree ps None k) )

 | StepReturn1 : forall (p:pointer) (ps:list pointer) (opt_v:option val) (k:cont) (env:env),
     cl_step (SKstmt Sskip env (Kfree ( p :: ps ) opt_v k) ) (TEmem (MEfree p MObjStack) ) (SKstmt Sskip env (Kfree ps opt_v k) )

 | StepReturnSome : forall (e:expr) (k:cont) (envp:env) (k':cont) (fn:function),
     call_cont k = k' ->
     get_fundef k' = Some (Internal fn) ->
     fn.(fn_return) <> Tvoid ->
     cl_step (SKstmt (Sreturn (Some e ) ) envp k )
              TEtau
              (SKexpr e envp (EKreturn k) )

 | StepReturnSome1 : forall (v:val) (k:cont) (env:env) (ps:list pointer),
     ps = sorted_pointers_of_env env ->
     cl_step (SKval v env (EKreturn k) )
              TEtau
              (SKstmt Sskip env (Kfree ps (Some v ) k) )

 | StepSwitch : forall (e:expr) (ls:labeled_statements) (k:cont) (env:env),
     cl_step (SKstmt (Sswitch e ls) env k )
              TEtau
              (SKexpr e env (EKswitch ls k ) )

 | StepSelectSwitch : forall (n:int) (ls:labeled_statements) (k:cont) (env:env) (s:statement),
     s = seq_of_labeled_statement (select_switch n ls) ->
     cl_step (SKval (Vint n) env (EKswitch ls k ) )
              TEtau
              (SKstmt s env (Kswitch k) )

 | StepBreakSwitch : forall (k:cont) (env:env),
     cl_step (SKstmt Sbreak env (Kswitch k) )
              TEtau
              (SKstmt Sskip env k )

 | StepContinueSwitch : forall (k:cont) (env:env),
     cl_step (SKstmt Scontinue env (Kswitch k) )
              TEtau
              (SKstmt Scontinue env k )

 | StepLabel : forall (l:label) (s:statement) (k:cont) (env:env),
     cl_step (SKstmt (Slabel l s) env k )
              TEtau
              (SKstmt s env k )

 | StepGoto : forall (l:label) (k:cont) (env:env) (s':statement) (k'' k':cont) (fn:function),
     call_cont k = k' ->
     get_fundef k' = (Some (Internal fn)) ->
     find_label l fn.(fn_body) k' = Some (s', k'') ->
     cl_step (SKstmt (Sgoto l) env k )
              TEtau
              (SKstmt s' env k'' )

 | StepFunctionInternal : forall (vs:list val) (opt_lhs:opt_lhs) (fd:fundef) (env:env) (k:cont) (args:list (ident*type)) (fn:function),
     args = fn.(fn_params) ++ fn.(fn_vars) ->
     fd = Internal fn ->
     cl_step (SKcall vs (Kcall opt_lhs fd env k))
              TEtau
              (SKalloc vs args empty_env (Kcall opt_lhs fd env k) )

 | StepAllocLocal : forall (vs:list val) (id:ident) (ty:type) (args:list (ident*type)) (k:cont) (env:env) (p:pointer) (n:int),
     n = Int.repr(sizeof ty) ->
     cl_step (SKalloc vs (( id , ty ):: args ) env k ) (TEmem (MEalloc p n MObjStack) ) (SKalloc vs args (PTree.set id p env ) k )

 | StepBindArgsStart : forall (vs:list val) (opt_lhs:opt_lhs) (fd:fundef) (envp:env) (k:cont) (envpp:env) (fn:function) (args:list (ident*type)),
     args = fn.(fn_params) ->
     fd = (Internal fn) ->
     cl_step (SKalloc vs nil envpp (Kcall opt_lhs fd envp k) )
              TEtau
              (SKbind fn vs args envpp (Kcall opt_lhs fd envp k) )

 | StepBindArgs : forall (fn:function) (v1:val) (vs:list val) (id:ident) (ty:type) (args:list (ident*type)) (k:cont) (env:env) (p:pointer) (c:memory_chunk) (v2:val),
     env!id = Some p ->
     type_to_chunk ty = (Some c) ->
     cast_value_to_chunk c v1 = v2 ->
     cl_step (SKbind fn ( v1 :: vs ) (( id , ty ):: args ) env k ) (TEmem (MEwrite p c v2) ) (SKbind fn vs args env k )

 | StepTransferFun : forall (fn:function) (k:cont) (env:env) (s:statement),
     s=fn.(fn_body) ->
     cl_step (SKbind fn nil nil env k )
              TEtau
              (SKstmt s env k )

 | StepExternalCall : forall (vs:list val) (opt_lhs:opt_lhs) (fd:fundef) (env:env) (k:cont) (id:ident) (evs:list eventval) (tys:typelist) (ty:type),
     true ->
     fd = External id tys ty ->
     vs = map val_of_eval evs ->
     cl_step (SKcall vs (Kcall opt_lhs fd env k)) (TEext (Ecall id evs) ) (SKExternal fd opt_lhs env k )

 | StepExternalReturn : forall (opt_lhs:opt_lhs) (fd:fundef) (k:cont) (env:env) (typ:typ) (evl:eventval) (v:val) (id:ident) (tys:typelist) (ty:type),
     Val.has_type v typ ->
     fd = External id tys ty ->
     typ = match (opttyp_of_type ty) with | Some x => x | None => Ast.Tint end ->
     v = val_of_eval evl ->
     cl_step (SKExternal fd opt_lhs env k ) (TEext (Ereturn typ evl) ) (SKoptstorevar opt_lhs v env k )

 | StepExternalStoreSomeLocal : forall (id:ident) (ty:type) (v1:val) (k:cont) (env:env) (p:pointer) (c:memory_chunk) (v2:val),
     env!id = Some p ->
     type_to_chunk ty = Some c ->
     cast_value_to_chunk c v1 = v2 ->
     cl_step (SKoptstorevar (Some ( id , ty )) v1 env k ) (TEmem (MEwrite p c v2) ) (SKstmt Sskip env k )

 | StepExternalStoreSomeGlobal : forall (id:ident) (ty:type) (v1:val) (k:cont) (env:env) (p:pointer) (c:memory_chunk) (v2:val),
     env!id = None ->
     Genv.find_symbol ge id = Some p ->
     type_to_chunk ty = Some c ->
     cast_value_to_chunk c v1 = v2 ->
     cl_step (SKoptstorevar (Some ( id , ty )) v1 env k ) (TEmem (MEwrite p c v2) ) (SKstmt Sskip env k )

 | StepExternalStoreNone : forall (v:val) (k:cont) (env:env),
     cl_step (SKoptstorevar None v env k )
              TEtau
              (SKstmt Sskip env k )

 | StepSkip : forall (s2:statement) (k:cont) (env:env),
     cl_step (SKstmt Sskip env (Kseq s2 k) )
              TEtau
              (SKstmt s2 env k )

 | StepWhileLoop : forall (e:expr) (s:statement) (k:cont) (env:env),
     cl_step (SKstmt Sskip env (Kwhile e s k) )
              TEtau
              (SKstmt (Swhile e s) env k )

 | StepDoWhileLoop : forall (s:statement) (e:expr) (k:cont) (env:env),
     cl_step (SKstmt Sskip env (Kdowhile s e k) )
              TEtau
              (SKexpr e env (EKdowhile s e k ) )

 | StepSkipSwitch : forall (k:cont) (env:env),
     cl_step (SKstmt Sskip env (Kswitch k) )
              TEtau
              (SKstmt Sskip env k )

 | StepReturnNoneFinish : forall (opt_v:option val) (k:cont) (envpp:env) (k':cont) (envp:env) (fd:fundef),
     call_cont k = (Kcall None fd envp k') ->
     cl_step (SKstmt Sskip envpp (Kfree nil opt_v k) )
              TEtau
              (SKstmt Sskip envp k' )

 | StepReturnSomeFinishLocal : forall (v1:val) (k:cont) (envpp:env) (p:pointer) (c:memory_chunk) (v2:val) (k':cont) (envp:env) (ty:type) (id:ident) (fd:fundef),
     type_to_chunk ty = (Some c) ->
     envp!id = Some p ->
     call_cont k = (Kcall (Some ( id , ty )) fd envp k') ->
     cast_value_to_chunk c v1 = v2 ->
     cl_step (SKstmt Sskip envpp (Kfree nil (Some v1 ) k) ) (TEmem (MEwrite p c v2) ) (SKstmt Sskip envp k' )

 | StepReturnSomeFinishGlobal : forall (v1:val) (k:cont) (envpp:env) (p:pointer) (c:memory_chunk) (v2:val) (k':cont) (envp:env) (ty:type) (id:ident) (fd:fundef),
     type_to_chunk ty = (Some c) ->
     envp!id = None ->
     Genv.find_symbol ge id = Some p ->
     call_cont k = (Kcall (Some ( id , ty )) fd envp k') ->
     cast_value_to_chunk c v1 = v2 ->
     cl_step (SKstmt Sskip envpp (Kfree nil (Some v1 ) k) ) (TEmem (MEwrite p c v2) ) (SKstmt Sskip envp k' )

 | StepStop : forall (env:env),
     cl_step (SKstmt Sskip env Kstop ) TEexit (SKstmt Sskip env Kstop ) .




Definition neutral_for_cast_dec (ty : type) : {neutral_for_cast ty} +
                                              {~ neutral_for_cast ty}.
Proof.
  intros.
  destruct ty;
    try (destruct i);
    try (left; constructor);
    try (right; intro H; inv H).
Defined.

Definition cast_ex (v : val) (ty ty' : type) : option val :=
  match v, ty, ty' with
    | Vint i, Tint sz1 si1, Tint sz2 si2 =>
        Some (Vint (cast_int_int sz2 si2 i))
    | Vfloat f, Tfloat sz1, Tint sz2 si2 =>
        Some (Vint (cast_int_int sz2 si2 (cast_float_int si2 f)))
    | Vint i, Tint sz1 si1, Tfloat sz2 =>
        Some (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
    | Vfloat f, Tfloat sz1, Tfloat sz2 =>
        Some (Vfloat (cast_float_float sz2 f))
    | Vptr p, _, _ =>
        if neutral_for_cast_dec ty
          then if neutral_for_cast_dec ty'
            then Some (Vptr p)
            else None
          else None
    | Vint i, _, _ =>
        if neutral_for_cast_dec ty
          then if neutral_for_cast_dec ty'
            then Some (Vint i)
            else None
          else None
    | _, _, _ => None
  end.

Inductive cl_step_res : Type :=
  | Rnostep : cl_step_res
  | Rsimple : thread_event -> state -> cl_step_res
  | Rread : pointer -> memory_chunk -> (val -> state) -> cl_step_res
  | Rreturn : typ -> (val -> state) -> cl_step_res
  | Ralloc : int -> mobject_kind -> (pointer -> state) -> cl_step_res
  | Rrmw : pointer -> memory_chunk -> rmw_instr -> (val -> state) -> cl_step_res.


Definition eval_of_val (v : val) : option eventval :=
  match v with
    | Vint i => Some (EVint i)
    | Vfloat f => Some (EVfloat f)
    | _ => None
  end.

Fixpoint map_eval_of_val (vs : list val) : option (list eventval) :=
  match vs with
    | nil => Some nil
    | v :: r =>
        optbind
          (fun er => option_map (fun ev => ev :: er) (eval_of_val v))
            (map_eval_of_val r)
  end.

Definition cl_step_fn1 (s : state) : cl_step_res :=
  match s with
  | (SKexpr (Expr (Econst_int i) ty) env k) =>
      Rsimple
              TEtau
             (SKval (Vint i) env k)
  | (SKexpr (Expr (Econst_float f) ty) env k) =>
      Rsimple
              TEtau
             (SKval (Vfloat f) env k)
  | (SKexpr (Expr (Evar id) ty) env k) =>
      Rsimple
              TEtau
             (SKlval (Expr (Evar id) ty) env (EKlval ty k))
  | (SKlval (Expr (Evar id) ty) env k) =>
      match env!id with
      | Some p =>
          Rsimple
              TEtau
             (SKval (Vptr p) env k)
      | None =>
          match Genv.find_symbol ge id with
          | Some p =>
              Rsimple
              TEtau
             (SKval (Vptr p) env k)
          | None => Rnostep
          end
      end
  | (SKval (Vptr p) env (EKlval ty k)) =>
      match access_mode ty with
      | By_value c => Rread p c (fun v => SKval v env k)
      | _ => Rsimple
              TEtau
             (SKval (Vptr p) env k)
      end
  | (SKexpr (Expr (Eaddrof e) ty) env k) => Rsimple
              TEtau
             (SKlval e env k)
  | (SKexpr (Expr (Ederef e) ty) env k) =>
      Rsimple
              TEtau
             (SKexpr e env (EKlval ty k))
  | (SKlval (Expr (Ederef e) ty) env k) =>
      Rsimple
              TEtau
             (SKexpr e env k)
  | (SKexpr (Expr (Efield e i) ty) env k) =>
      Rsimple
              TEtau
             (SKlval (Expr (Efield e i) ty) env (EKlval ty k))
  | (SKlval (Expr (Efield e i) ty) env k) =>
      match typeof e with
      | Tstruct id fList =>
          match field_offset i fList with
          | OK delta =>
              Rsimple
              TEtau
             (SKlval e env (EKfield delta k))
          | _ => Rnostep
          end
      | Tunion id fList => Rsimple
              TEtau
             (SKlval e env k)
      | _ => Rnostep
      end
  | (SKval (Vptr p) env (EKfield delta k)) =>
      Rsimple
              TEtau
             (SKval (Vptr (Ptr.add p (Int.repr delta))) env k)
  | (SKexpr (Expr (Esizeof ty') ty) env k) =>
      Rsimple
              TEtau
             (SKval (Vint (Int.repr (sizeof ty'))) env k)
  | (SKexpr (Expr (Eunop op e) ty) env k) =>
      Rsimple
              TEtau
             (SKexpr e env (EKunop op (typeof e) k))
  | (SKval v env (EKunop op ty k)) =>
      match sem_unary_operation op v ty with
      | Some v' => Rsimple
              TEtau
             (SKval v' env k)
      | None => Rnostep
      end
  | (SKexpr (Expr (Ebinop op e1 e2) ty) env k) =>
      Rsimple
              TEtau
             (SKexpr e1 env (EKbinop1 op (typeof e1) (typeof e2) ty e2 k))
  | (SKval v env (EKbinop1 op ty1 ty2 ty e2 k)) =>
      if (valid_arg op ty1 ty2 v)
         then Rsimple
              TEtau
             (SKexpr e2 env (EKbinop2 op ty1 ty2 ty v k))
         else Rnostep
  | (SKval v2 env (EKbinop2 op ty1 ty2 ty v1 k)) =>
      match sem_binary_operation op v1 ty1 v2 ty2 with
      | Some v' => Rsimple
              TEtau
             (SKval v' env k)
      | None => Rnostep
      end
  | (SKexpr (Expr (Econdition e1 e2 e3) ty) env k) =>
      Rsimple
              TEtau
             (SKexpr e1 env (EKcondition e2 e3 (typeof e1) k))
  | (SKval v env (EKcondition e2 e3 ty k)) =>
      if eval_true v ty
         then Rsimple
              TEtau
             (SKexpr e2 env k)
         else if eval_false v ty
              then Rsimple
              TEtau
             (SKexpr e3 env k)
              else Rnostep
  | (SKexpr (Expr (Ecast ty a) ty') env k) =>
      Rsimple
              TEtau
             (SKexpr a env (EKcast (typeof a) ty k))
  | (SKexpr (Expr (Eandbool e1 e2) ty) env k) =>
      Rsimple
              TEtau
             (SKexpr (Expr (Econdition e1
                                    (Expr (Econdition e2
                                            (Expr (Econst_int (Int.repr 1)) ty)
                                            (Expr (Econst_int (Int.repr 0)) ty))
                                           ty)
                                    (Expr (Econst_int (Int.repr 0)) ty)) ty)
                        env k)
  | (SKexpr (Expr (Eorbool e1 e2) ty) env k) =>
      Rsimple
              TEtau
             (SKexpr (Expr (Econdition e1
                                    (Expr (Econst_int (Int.repr 1)) ty)
                                    (Expr
                                      (Econdition e2
                                        (Expr (Econst_int (Int.repr 1)) ty)
                                        (Expr (Econst_int (Int.repr 0)) ty))
                                      ty)) ty) env k)
  | (SKval v env (EKcast ty ty' k)) =>
      match cast_ex v ty ty' with
      | Some v' => Rsimple
              TEtau
             (SKval v' env k)
      | None => Rnostep
      end
  | (SKstmt (Sthread_create efn eargs) env k) =>
      Rsimple
              TEtau
             (SKexpr efn env (EKthread1 eargs k))
  | (SKval v env (EKthread1 eargs k)) =>
      match v with
      | Vptr p => Rsimple
              TEtau
             (SKexpr eargs env (EKthread2 p k))
      | _ => Rnostep
      end
  | (SKval v env (EKthread2 p k)) =>
      Rsimple (TEstart p (v::nil)) (SKstmt Sskip env k)
  | (SKstmt (Sassign e1 e2) env k) =>
      Rsimple
              TEtau
             (SKlval e1 env (EKassign1 e2 (typeof e1) k))
  | (SKval v env (EKassign1 e c k)) =>
      Rsimple
              TEtau
             (SKexpr e env (EKassign2 v c k))
  | (SKval v1 env (EKassign2 (Vptr p2) ty1 k)) =>
    match type_to_chunk ty1 with
      | Some c1 => Rsimple (TEmem (MEwrite p2 c1 (cast_value_to_chunk c1 v1))) (SKstmt Sskip env k)
      | None => Rnostep
    end
  | (SKstmt (Ssequence s1 s2) env k) =>
      Rsimple
              TEtau
             (SKstmt s1 env (Kseq s2 k))
  | (SKstmt (Scall None e args) env k) =>
      Rsimple
              TEtau
             (SKexpr e env (EKcall None (typeof e) args k))
  | (SKstmt (Scall (Some lhs) e args) env k) =>
      Rsimple
              TEtau
             (SKexpr e env (EKcall (Some lhs) (typeof e) args k))
  | (SKval v env (EKcall opt ty nil k)) =>
      match Genv.find_funct ge v with
      | Some fd =>
          if type_eq (type_of_fundef fd) ty
            then Rsimple
              TEtau
             (SKcall nil (Kcall opt fd env k))
            else Rnostep
      | None => Rnostep
      end
  | (SKval v env (EKcall opt ty (arg1 :: args) k)) =>
      Rsimple
              TEtau
             (SKexpr arg1 env (EKargs opt v ty nil args k))
  | (SKval v1 env (EKargs opt v ty vs (arg1 :: args) k)) =>
      Rsimple
              TEtau
             (SKexpr arg1 env (EKargs opt v ty (List.app vs (v1::nil)) args k))
  | (SKval v' env (EKargs opt v ty vs nil k)) =>
      match Genv.find_funct ge v with
      | Some fd =>
          if type_eq (type_of_fundef fd) ty
            then Rsimple
              TEtau
             (SKcall (List.app vs (v'::nil)) (Kcall opt fd env k))
            else Rnostep
      | None => Rnostep
      end
  | (SKstmt Scontinue env (Kseq s k)) =>
      Rsimple
              TEtau
             (SKstmt Scontinue env k)
  | (SKstmt Sbreak env (Kseq s k)) =>
      Rsimple
              TEtau
             (SKstmt Sbreak env k)
  | (SKstmt (Sifthenelse e1 s1 s2) env k) =>
      Rsimple
              TEtau
             (SKexpr e1 env (EKcond (typeof e1) s1 s2 k))
  | (SKval v env (EKcond ty s1 s2 k)) =>
      if eval_true v ty
        then Rsimple
              TEtau
             (SKstmt s1 env k)
        else if eval_false v ty
          then Rsimple
              TEtau
             (SKstmt s2 env k)
          else Rnostep
  | SKstmt (Satomic lhs astmt (e :: es)) env k =>
    Rsimple
              TEtau
             (SKexpr e env (EKatargs lhs astmt nil es k))

  | SKval v env (EKatargs lhs astmt vs (e::es) k) =>
    Rsimple
              TEtau
             (SKexpr e env (EKatargs lhs astmt (vs ++ v :: nil) es k))

  | SKval v env (EKatargs None astmt vs nil k) =>
    match sem_atomic_statement astmt (vs ++ v :: nil) with
      | None => Rnostep
      | Some (p, rmwi) =>
        Rrmw p Mint32 rmwi (fun v' => SKstmt Sskip env k)
    end

  | SKval v env (EKatargs (Some (id, ty)) astmt vs nil k) =>
    match sem_atomic_statement astmt (vs ++ v :: nil) with
      | None => Rnostep
      | Some (p, rmwi) =>
        Rrmw p Mint32 rmwi (fun v' => SKoptstorevar (Some (id, ty)) v' env k)
    end

  | SKstmt Smfence env k =>
      Rsimple (TEmem MEfence) (SKstmt Sskip env k)

  | (SKstmt (Swhile e s) env k) =>
      Rsimple
              TEtau
             (SKexpr e env (EKwhile e s k))

  | (SKval v env (EKwhile e s k)) =>
      if eval_true v (typeof e)
        then Rsimple
              TEtau
             (SKstmt s env (Kwhile e s k))
        else if eval_false v (typeof e)
          then Rsimple
              TEtau
             (SKstmt Sskip env k)
          else Rnostep

  | (SKstmt Scontinue env (Kwhile e s k)) =>
      Rsimple
              TEtau
             (SKstmt (Swhile e s) env k)

  | (SKstmt Sbreak env (Kwhile e s k)) =>
      Rsimple
              TEtau
             (SKstmt Sskip env k)


  | (SKstmt (Sdowhile e s) env k) =>
      Rsimple
              TEtau
             (SKstmt s env (Kdowhile s e k))

  | (SKval v env (EKdowhile s e k)) =>
      if eval_true v (typeof e)
        then Rsimple
              TEtau
             (SKstmt (Sdowhile e s) env k)
        else if eval_false v (typeof e)
          then Rsimple
              TEtau
             (SKstmt Sskip env k)
          else Rnostep

  | (SKstmt Scontinue env (Kdowhile s e k)) =>
      Rsimple
              TEtau
             (SKexpr e env (EKdowhile s e k))

  | (SKstmt Sbreak env (Kdowhile s e k)) =>
      Rsimple
              TEtau
             (SKstmt Sskip env k)

  | (SKstmt (Sfor s1 e2 s3 s) env k) =>
      Rsimple
              TEtau
             (SKstmt s1 env (KforCond e2 s3 s k) )

  | (SKstmt Sbreak env (KforIncr e2 s3 s k)) =>
      Rsimple
              TEtau
             (SKstmt Sskip env k)

  | (SKstmt Scontinue env (KforIncr e2 s3 s k)) =>
      Rsimple
              TEtau
             (SKstmt s3 env (KforCond e2 s3 s k))

  | (SKstmt Sskip env (KforIncr e2 s3 s k)) =>
      Rsimple
              TEtau
             (SKstmt s3 env (KforCond e2 s3 s k))

  | (SKval v env (EKforTest e2 s3 s k)) =>
      if eval_true v (typeof e2)
        then Rsimple
              TEtau
             (SKstmt s env (KforIncr e2 s3 s k) )
        else if eval_false v (typeof e2)
          then Rsimple
              TEtau
             (SKstmt Sskip env k)
          else Rnostep
  | (SKstmt (Sreturn None) env k) =>
     match (call_cont k) with
      | (Kcall None (Internal f) envpp k') =>
          match f.(fn_return) with
          | Tvoid => Rsimple
              TEtau
             (SKstmt Sskip env (Kfree (sorted_pointers_of_env env) None k))
          | _ => Rnostep
          end
      | _ => Rnostep
      end
  | (SKstmt (Sreturn (Some e)) envp k) =>
     match (get_fundef (call_cont k)) with
     | Some (Internal fn) =>
        match fn.(fn_return) with
          | Tvoid => Rnostep
          | _ => Rsimple
              TEtau
             (SKexpr e envp (EKreturn k))
          end
      | _ => Rnostep
      end
  | (SKstmt Sskip env (Kfree (p1 :: ps) v k)) =>
      Rsimple (TEmem (MEfree p1 MObjStack)) (SKstmt Sskip env (Kfree ps v k))
  | (SKval v env (EKreturn k)) =>
      Rsimple
              TEtau
             (SKstmt Sskip env (Kfree (sorted_pointers_of_env env) (Some v) k))
  | (SKstmt (Sswitch e sl) env k) =>
      Rsimple
              TEtau
             (SKexpr e env (EKswitch sl k))
  | (SKval (Vint n) env (EKswitch sl k)) =>
      Rsimple
              TEtau
             (SKstmt (seq_of_labeled_statement (select_switch n sl))
                       env (Kswitch k))
  | (SKstmt Sbreak env (Kswitch k)) => Rsimple
              TEtau
             (SKstmt Sskip env k)
  | (SKstmt Scontinue env (Kswitch k)) => Rsimple
              TEtau
             (SKstmt Scontinue env k)
  | (SKstmt (Slabel lbl s) env k) =>
      Rsimple
              TEtau
             (SKstmt s env k)
  | (SKstmt (Sgoto lbl) env k) =>
      let k1 := (call_cont k) in
      match (get_fundef k1) with
      | Some (Internal f) =>
          match find_label lbl f.(fn_body) k1 with
          | Some (s', k') => Rsimple
              TEtau
             (SKstmt s' env k')
          | None => Rnostep
          end
      | _ => Rnostep
      end
  | (SKcall vs (Kcall opt (Internal f) env k)) =>
     Rsimple
              TEtau
            
        (SKalloc vs (f.(fn_params) ++ f.(fn_vars)) empty_env
                             (Kcall opt (Internal f) env k))
  | (SKalloc vs ((id,ty) :: args) env k) =>
      Ralloc (Int.repr(sizeof ty)) MObjStack
           (fun p => SKalloc vs args (PTree.set id p env) k)
  | (SKalloc vs nil env (Kcall opt (Internal f) env' k)) =>
      Rsimple
              TEtau
             (SKbind f vs (f.(fn_params)) env (Kcall opt (Internal f) env' k))
  | (SKbind f (v::vs) ((id,ty)::args) env k) =>
      match PTree.get id env, type_to_chunk ty with
      | Some p, Some c =>
          Rsimple (TEmem (MEwrite p c (cast_value_to_chunk c v))) (SKbind f vs args env k)
      | _, _ => Rnostep
      end
  | (SKbind f nil nil env k) =>
      Rsimple
              TEtau
             (SKstmt f.(fn_body) env k)
  | (SKcall vs (Kcall tgt (External id targs tres) env k)) =>
      match map_eval_of_val vs with
        | Some vs => Rsimple (TEext (Ecall id vs)) (SKExternal (External id targs tres) tgt env k)
        | None => Rnostep
      end
  | (SKExternal (External id tys ty) tgt env k) =>
      match (opttyp_of_type ty) with
      | Some x => Rreturn x (fun vres => SKoptstorevar tgt vres env k)
      | None => Rreturn Ast.Tint (fun vres => SKoptstorevar tgt vres env k)
      end
  | (SKoptstorevar (Some(id,ty)) vres env k) =>
      match type_to_chunk ty with
      | (Some c) => match env!id with
                    | None => match Genv.find_symbol ge id with
                             | Some p => Rsimple (TEmem (MEwrite p c (cast_value_to_chunk c vres))) (SKstmt Sskip env k)
                             | None => Rnostep
                             end
                    | Some p => Rsimple (TEmem (MEwrite p c (cast_value_to_chunk c vres))) (SKstmt Sskip env k)
                    end
      | None => Rnostep
      end
  | (SKoptstorevar None vres env k) =>
      Rsimple
              TEtau
             (SKstmt Sskip env k)
  | (SKstmt Sskip env (Kseq s k)) =>
      Rsimple
              TEtau
             (SKstmt s env k)
  | (SKstmt Sskip env (Kwhile e s k)) =>
      Rsimple
              TEtau
             (SKstmt (Swhile e s) env k)
  | (SKstmt Sskip env (Kdowhile s e k)) =>
      Rsimple
              TEtau
             (SKexpr e env (EKdowhile s e k))
  | (SKstmt Sskip env (Kswitch k)) => Rsimple
              TEtau
             (SKstmt Sskip env k)
  | (SKstmt Sskip env (KforCond e2 s3 s k)) =>
      Rsimple
              TEtau
             (SKexpr e2 env (EKforTest e2 s3 s k))

  | (SKstmt Sskip env (Kfree nil None k)) =>
      match call_cont k with
      | (Kcall None f env k') => Rsimple
              TEtau
             (SKstmt Sskip env k')
      | _ => Rnostep
      end
  | (SKstmt Sskip env' (Kfree nil (Some v) k)) =>
      match call_cont k with
      | (Kcall (Some(id,ty)) f env k') =>
          match type_to_chunk ty with
          | (Some c) => match env!id with
                        | None => match Genv.find_symbol ge id with
                                  | Some p => Rsimple (TEmem (MEwrite p c (cast_value_to_chunk c v)))
                                                      (SKstmt Sskip env k')
                                  | _ => Rnostep
                                  end
                        | Some p => Rsimple (TEmem (MEwrite p c (cast_value_to_chunk c v)))
                                            (SKstmt Sskip env k')
                        end
          | _ => Rnostep
          end
      | (Kcall None f env k') => Rsimple
              TEtau
             (SKstmt Sskip env k')
      | _ => Rnostep
      end
  | (SKstmt Sskip env Kstop) => Rsimple (TEexit) (SKstmt Sskip env Kstop)
  | _ => Rnostep
  end.

Definition cl_step_fn (s : state) (te : thread_event) : option state :=
  match cl_step_fn1 s with
  | Rnostep => None
  | Rsimple te' s => if thread_event_eq_dec te te' then Some s else None
  | Rread p c f =>
      match te with
      | TEmem (MEread p' c' v) =>
           if Ptr.eq_dec p p' then
             if memory_chunk_eq_dec c c' then
               if Val.has_type v (type_of_chunk c) then Some (f v)
               else None
             else None
           else None
      | _ => None
      end
  | Rreturn typ f =>
      match te with
      | TEext (Ereturn typ' v) =>
          if typ_eq_dec typ typ' then
            if Val.has_type (val_of_eval v) typ
              then Some (f (val_of_eval v))
            else None
          else None
      | _ => None
      end
  | Ralloc size k f =>
      match te with
      | TEmem (MEalloc p size' k') =>
          if Int.eq_dec size size'
            then if mobject_kind_eq_dec k k'
              then Some (f p)
              else None
            else None
      | _ => None
      end
  | Rrmw p c i f =>
      match te with
      | TEmem (MErmw p' c' v i') =>
           if Ptr.eq_dec p p' then
             if memory_chunk_eq_dec c c' then
               if rmw_instr_dec i i' then
                 if Val.has_type v (type_of_chunk c) then Some (f v)
                 else None
               else None
             else None
           else None
      | _ => None
      end
  end.

End STEP.

Definition ST := state.
Definition PRG := program.
Definition GE := genv.

Definition step := cl_step.
Definition cl_ge_init (p : program) (ge : genv) (m : Mem.mem) :=
  Genv.globalenv_initmem p ge no_mem_restr m.


Ltac ite_some_asm_destruction :=
  match goal with
    | H : context[if ?E then _ else _] |- _ => destruct E; try discriminate
    | H : Some _ = Some _ |- _ => inversion H; clear H
  end.

Lemma cast_ex_some:
  forall v ty ty' v',
  cast_ex v ty ty' = Some v' ->
  cast v ty ty' v'.
Proof.
  intros v ty ty' v' CEX.
  destruct v; destruct ty; destruct ty'; try discriminate; try constructor;
    unfold cast_ex in CEX; try repeat ite_some_asm_destruction; subst;
      try constructor; try done.
Qed.

Lemma map_eval_of_val_succ:
  forall {vs evs},
    map_eval_of_val vs = Some evs ->
    vs = map val_of_eval evs.
Proof.
  induction vs as [|v vs IH]. destruct evs; try done.
  intros evs. simpl. destruct map_eval_of_val; simpl; [|done].
  specialize (IH _ (refl_equal _)); subst.
  destruct (eval_of_val v) as [ev|] _eqn : Ev; simpl; [|done].
  intro E; inv E. simpl.
  by destruct v; destruct ev; try done; simpl in *; inv Ev.
Qed.

Ltac asm_match_destruction := match goal with
    | H' : is_true ?a ?b, H'' : is_false ?a ?b |- ?P =>
        byContradiction; apply (is_true_is_false_contr _ _ H' H'')
    | H' : ?n <> ?n |- _ => elim H'; reflexivity
    | H : Some _ = Some _ |- _ => inversion H; clear H
    | H : neutral_for_cast (Tfloat _) |- _ => inv H
    | H': ?a = ?b |- ?P => rewrite H'
    | H': ?a = ?b \/ ?c |- ?P => destruct H'
    | H : context[match ?v with (_,_) => _ end] |- _ => destruct v as [] _eqn: ?
    | H : context[if eval_true ?E ?F then _ else _] |- _ => destruct (eval_true E F)
    | H : context[if eval_false ?E ?F then _ else _] |- _ => destruct (eval_false E F)
    | H : context[if Val.has_type ?E ?F then _ else _] |- _ => destruct (Val.has_type E F) as [] _eqn: ?
    | H : context[if valid_arg ?a ?b ?c ?d then _ else _] |- _ => destruct (valid_arg a b c d) as [] _eqn: ?; try discriminate
    | H : context[if ?v then _ else _] |- _ => destruct v; try discriminate
    | H : context[(match ?v with
          | Vundef => _ | Vint _ => _ | Vfloat _ => _ | Vptr _ => _ end)] |- _ => destruct v as [] _eqn: ?
    | H : context[(match ?v with
          | Some _ => _ | None => _ end)] |- _ => destruct v as [] _eqn: ?
    | H : context[(match ?v with
          | OK _ => _ | Error _ => _ end)] |- _ => destruct v as [] _eqn: ?
    | H : context[(match ?v with
          | Internal _ => _ | External _ _ _ => _ end)] |- _ => destruct v as [] _eqn: ?
    | H : context[(match ?v with
          | nil => _ | _::_ => _ end)] |- _ => destruct v as [] _eqn: ?
    | H : context[(match ?v with
          | Tvoid => _ | Tint _ _ => _ | Tfloat _ => _ | Tpointer _ => _
          | Tarray _ _ => _ | Tfunction _ _ => _ | Tstruct _ _ => _
          | Tunion _ _ => _ | Tcomp_ptr _ => _ end)] |- _ => destruct v as [] _eqn: ?
    | H : context[(match ?v with
        | TEext _ => _ | TEmem _ => _ |
              TEtau
               => _ | TEexit => _
        | TEstart _ _ => _ | TEstartmem _ _ => _
        | TEexternalcallmem _ _ => _
        | TEoutofmem => _ end)] |- _ =>
             destruct v as [[] |[] | | | | | |] _eqn: ?
    | H : context[(match ?v with
          | MObjStack => _ | MObjGlobal => _ | MObjHeap => _ end)] |- _ =>
             destruct v as [] _eqn: ?
    | H : context[(match ?v with
           | By_value _ => _ | By_reference => _
           | By_nothing => _ end)] |- _ => destruct v as [] _eqn: ?
    | H : context[(match ?c with
            | Kstop => _
            | Kseq _ _ => _
            | Kwhile _ _ _ => _
            | Kdowhile _ _ _ => _
            | KforIncr _ _ _ _ => _
            | KforCond _ _ _ _ => _
            | Kcall _ _ _ _ => _
            | Kswitch _ => _
            | Kfree _ _ _ => _
            end)] |- _ => destruct c as [] _eqn: ?
    | H : map_eval_of_val _ = Some _ |- _ => rewrite (map_eval_of_val_succ H) in *
    end.

Ltac byRewriteAsm :=
  repeat match goal with
    | |- ?n <> ?m => let X := fresh in intro X; inversion X; fail
    | H: ?a = ?b |- _ => rewrite H
    | H : ?n <> ?n |- _ => elim H; reflexivity
  end.

Lemma cl_step_match_fn1:
    forall ge s l s',
      cl_step_fn ge s l = Some s' -> cl_step ge s l s'.
Proof.

  unfold cl_step_fn.
  intros ge s l s' H.
  destruct s as [[[]] | [[]]|vv ? []|[]| | | | |]; simpl in H;
   clarify;
   try (destruct (cast_ex vv t t0) as [] _eqn : EQ; try apply cast_ex_some in EQ; clarify);
   try (destruct vv; simpl in H; clarify);
   repeat (vauto; asm_match_destruction); vauto;
  try (eapply StepReturnSome; try edone; congruence).
  eapply StepExternalReturn; try edone. rewrite Heqo0; done.
  eapply StepExternalReturn; try edone. rewrite Heqo0; done.
Qed.

Lemma neutral_for_cast_int_cast:
  forall it s i,
    neutral_for_cast (Tint it s) ->
    cast_int_int it s i = i.
Proof.

  by inversion 1.
Qed.

Lemma map_eval_of_val_eq:
  forall evs,
    map_eval_of_val (map val_of_eval evs) = Some evs.
Proof.
  induction evs as [|[] evs IH]; try done; simpl; rewrite IH; done.
Qed.

Ltac goal_match_destruction := match goal with
    | H': ?a = ?b \/ ?c |- ?P => destruct H'
    | H': ?a = ?b |- ?P => rewrite H'
    | |- context[if eval_true ?E ?F then _ else _] => destruct (eval_true E F)
    | |- context[if eval_false ?E ?F then _ else _] => destruct (eval_false E F)
    | |- context[if ?E then _ else _] => destruct E; try discriminate
    | |- context[(match ?v with
          | Vundef => _ | Vint _ => _ | Vfloat _ => _ | Vptr _ => _ end)] => destruct v as [] _eqn: ?
    | |- context[(match ?v with
          | Some _ => _ | None => _ end)] => destruct v as [] _eqn: ?
    | |- context[(match ?v with
          | MObjStack => _ | MObjHeap => _ | MObjGlobal => _ end)] =>
            destruct v as [] _eqn: ?
    | |- context[(match ?v with
          | Internal _ => _ | External _ _ _ => _ end)] => destruct v as [] _eqn: ?
    | |- context[(match ?v with
          | nil => _ | _::_ => _ end)] => destruct v as [] _eqn: ?
    | |- context[(match ?v with
          | Tvoid => _ | Tint _ _ => _ | Tfloat _ => _ | Tpointer _ => _
          | Tarray _ _ => _ | Tfunction _ _ => _ | Tstruct _ _ => _
          | Tunion _ _ => _ | Tcomp_ptr _ => _ end)] => destruct v as [] _eqn: ?
    | |- context[(match ?v with
        | TEext _ => _ | TEmem _ => _ |
              TEtau
             => _ | TEexit => _
        | TEstart _ _ => _ | TEstartmem _ _ => _ | TEexternalcallmem _ _
        | TEoutofmem => _ end)]
          => destruct v as [[] |[] | | | | | |] _eqn: ?
    | H' : is_true ?a ?b, H'' : is_false ?a ?b |- ?P =>
      byContradiction; apply (is_true_is_false_contr _ _ H' H'')
    | H' : ?n <> ?n |- _ => elim H'; reflexivity
    | H : Some _ = Some _ |- _ => inversion H; clear H
    | H : cast _ _ _ _ |- _ => inv H; simpl in *
    | H : context[map_eval_of_val (map val_of_eval _)] |- _ =>
      rewrite map_eval_of_val_eq in H
    | p : (ident * type)%type |- _ => destruct p
    end.

Lemma cl_step_match_fn:
    forall ge s l s',
      cl_step ge s l s' -> cl_step_fn ge s l = Some s'.
Proof.

  unfold cl_step_fn.
  intros ge s l s' H; inversion H; subst; simpl;
    repeat goal_match_destruction; clarify; repeat asm_match_destruction; clarify.
  by rewrite neutral_for_cast_int_cast.


Qed.


Lemma cl_receptive :
  forall ge l l' s s',
    cl_step ge s l s' ->
    te_samekind l' l ->
    exists s'', cl_step ge s l' s''.
Proof.

  intros ge l l' s s' Step Te_Samekind.
  inversion Step;
     subst;
     destruct l'; try destruct ev;
     simpl in *;
     try done;
     try rewrite Te_Samekind;
     try (decompose [and] Te_Samekind; subst);
     econstructor;
     try (by econstructor; try (eby apply H1); eauto);
     try (by eassumption).

Qed.

Lemma cl_determinate:
  forall ge s s' s'' l l',
    cl_step ge s l s' ->
    cl_step ge s l' s'' ->
    (te_samekind l l' /\
      (l = l' -> s' = s'')).
Proof.

  intros ge s s' s'' l l' ST1 ST2.
  apply cl_step_match_fn in ST2.
  split.
    by revert ST2; unfold cl_step_fn; destruct ST1; subst; simpl;
       try done; repeat goal_match_destruction; try done; subst; auto.

  by apply cl_step_match_fn in ST1; intro; subst; rewrite ST2 in ST1; inv ST1.

Qed.

Require Import Classical.

Lemma cl_progress_dec:
  forall ge s, (forall s' l', ~ cl_step ge s l' s') \/
    (exists l', exists s', cl_step ge s l' s').
Proof.

  intros ge s.
  set (P := exists l' : thread_event, exists s' : state, cl_step ge s l' s').
  destruct (classic P). auto.
  left. intros s' l'. revert s'. apply not_ex_all_not.
  revert l'. apply not_ex_all_not. auto.
Qed.

Definition cl_sem : SEM :=
  mkSEM state genv program cl_ge_init (@prog_main _ _) (@Genv.find_symbol _)
  cl_step cl_init cl_progress_dec cl_receptive cl_determinate.

End Clight.







Generated by coq2html