Require Import Axioms.
Require Import Classical.
Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import AST.
Require Import NormaliseSpec.
Require Import ExprEval.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Determinism.
Require Import Ctypes.
Require Import Cop.
Require Import Csyntax.
Require Import Csem.
Require Cstrategy.
Require Import Values_symbolictype.
Require Import Values_symbolic.
Require Import Normalise.
Require Import VarSort.

Notation "'do' X <- A ; B" := (match A with Some X => B | None => None end)
  (at level 200, X ident, A at level 100, B at level 200)
  : option_monad_scope.

Notation "'do' X , Y <- A ; B" := (match A with Some (X, Y) => B | None => None end)
  (at level 200, X ident, Y ident, A at level 100, B at level 200)
  : option_monad_scope.

Notation "'do' X , Y , Z <- A ; B" := (match A with Some (X, Y, Z) => B | None => None end)
  (at level 200, X ident, Y ident, Z ident, A at level 100, B at level 200)
  : option_monad_scope.

Notation " 'check' A ; B" := (if A then B else None)
  (at level 200, A at level 100, B at level 200)
  : option_monad_scope.

Notation "'do' X <- A ; B" := (match A with Some X => B | None => nil end)
  (at level 200, X ident, A at level 100, B at level 200)
  : list_monad_scope.

Notation " 'check' A ; B" := (if A then B else nil)
  (at level 200, A at level 100, B at level 200)
  : list_monad_scope.

Definition is_val (a: expr) : option (expr_sym * type) :=
  match a with
  | Csyntax.Eval v ty => Some(v, ty)
  | _ => None
  end.

Lemma is_val_inv:
  forall a v ty, is_val a = Some(v, ty) -> a = Csyntax.Eval v ty.

Definition is_loc (a: expr) : option (expr_sym * type) :=
  match a with
  | Eloc ptr ty => Some(ptr, ty)
  | _ => None
  end.

Lemma is_loc_inv:
  forall a ptr ty, is_loc a = Some(ptr, ty) -> a = Eloc ptr ty.

Local Open Scope option_monad_scope.

Fixpoint is_val_list (al: exprlist) : option (list (expr_sym * type)) :=
  match al with
  | Enil => Some nil
  | Econs a1 al => do vt1 <- is_val a1; do vtl <- is_val_list al; Some(vt1::vtl)
  end.

Definition is_skip (s: statement) : {s = Sskip} + {s <> Sskip}.

Events, volatile memory accesses, and external functions.

Section EXEC.

Variable ge: genv.

Variable needed_stackspace : ident -> nat.

Definition eventval_of_val (v: val) (t: typ) : option eventval :=
  match v, t with
  | (Vint i), AST.Tint => Some (EVint i)
  | (Vfloat f), AST.Tfloat => Some (EVfloat f)
  | (Vsingle f), AST.Tsingle => Some (EVsingle f)
  | (Vlong n), AST.Tlong => Some (EVlong n)
  | (Vptr b ofs), AST.Tint => do id <- Genv.invert_symbol ge b; Some (EVptr_global id ofs)
  | _, _ => None
  end.

Fixpoint list_eventval_of_val (vl: list val) (tl: list typ) : option (list eventval) :=
  match vl, tl with
  | nil, nil => Some nil
  | v1::vl, t1::tl =>
      do ev1 <- eventval_of_val v1 t1;
      do evl <- list_eventval_of_val vl tl;
      Some (ev1 :: evl)
  | _, _ => None
  end.

Definition val_of_eventval (ev: eventval) (t: typ) : option val :=
  match ev, t with
  | EVint i, AST.Tint => Some ( (Vint i))
  | EVfloat f, AST.Tfloat => Some ( (Vfloat f))
  | EVsingle f, AST.Tsingle => Some ( (Vsingle f))
  | EVlong n, AST.Tlong => Some ( (Vlong n))
  | EVptr_global id ofs, AST.Tint => do b <- Genv.find_symbol ge id; Some ( (Vptr b ofs))
  | _, _ => None
  end.

Lemma eventval_of_val_sound:
  forall v t ev, eventval_of_val v t = Some ev -> eventval_match ge ev t v.

Lemma eventval_of_val_complete:
  forall ev t v, eventval_match ge ev t v -> eventval_of_val v t = Some ev.

Lemma list_eventval_of_val_sound:
  forall vl tl evl,
    list_eventval_of_val vl tl = Some evl ->
    eventval_list_match ge evl tl vl.

Lemma list_eventval_of_val_complete:
  forall evl tl vl, eventval_list_match ge evl tl vl ->
               list_eventval_of_val vl tl = Some evl.

Lemma val_of_eventval_sound:
  forall ev t v, val_of_eventval ev t = Some v -> eventval_match ge ev t v.

Lemma val_of_eventval_complete:
  forall ev t v, eventval_match ge ev t v -> val_of_eventval ev t = Some v.


Definition in_bound o m b : bool :=
  let (lo,hi) := Mem.bounds_of_block m b in
  if zle lo o && zlt o hi then true else false.

Require Import Tactics.
Lemma in_bound_true:
  forall o m b,
    in_bound o m b = true <-> Mem.in_bound_m o m b.


Definition do_volatile_load (w: world) (chunk: memory_chunk) (m: mem) (addr: expr_sym)
: option (world * trace * expr_sym) :=
  match Mem.mem_norm m addr with
    Vptr b ofs =>
      if block_is_volatile ge b then
        if in_bound (Int.unsigned ofs) m b then
          do id <- Genv.invert_symbol ge b;
            match nextworld_vload w chunk id ofs with
            | None => None
            | Some(res, w') =>
              do vres <- val_of_eventval res (AST.type_of_chunk chunk);
                Some(w', Event_vload chunk id ofs res :: nil, Val.load_result chunk (Eval vres))
            end
        else None
      else
        do v <- Mem.load chunk m b (Int.unsigned ofs);
        Some(w, E0, v)
    | _ => None
  end.

Definition do_volatile_store (w: world) (chunk: memory_chunk) (m: mem) (addr:expr_sym) (v: expr_sym)
  : option (world * trace * mem) :=
  match Mem.mem_norm m addr with
      Vptr b ofs =>
      if block_is_volatile ge b then
        if in_bound (Int.unsigned ofs) m b then
          do id <- Genv.invert_symbol ge b;
            do ev <- eventval_of_val (Mem.mem_norm m (Val.load_result chunk v))
               ((AST.type_of_chunk chunk));
            do w' <- nextworld_vstore w chunk id ofs ev;
            Some(w', Event_vstore chunk id ofs ev :: nil, m)
        else None
      else
        do m' <- Mem.store chunk m b (Int.unsigned ofs) v;
        Some(w, E0, m')
    | _ => None
  end.

Ltac mydestr :=
  match goal with
  | [ |- None = Some _ -> _ ] => intro X; discriminate
  | [ |- Some _ = Some _ -> _ ] => intro X; inv X
  | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr
  | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr
  | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr
  | _ => idtac
  end.

Lemma do_volatile_load_sound:
  forall w chunk m addr w' t v,
  do_volatile_load w chunk m addr = Some(w', t, v) ->
  volatile_load ge chunk m addr t v /\ possible_trace w t w'.

Lemma do_volatile_load_complete:
  forall w chunk m addr w' t v,
  volatile_load ge chunk m addr t v -> possible_trace w t w' ->
  do_volatile_load w chunk m addr = Some(w', t, v).

Lemma do_volatile_store_sound:
  forall w chunk m addr v w' t m',
  do_volatile_store w chunk m addr v = Some(w', t, m') ->
  volatile_store ge chunk m addr v t m' /\ possible_trace w t w'.

Lemma do_volatile_store_complete:
  forall w chunk m addr v w' t m',
  volatile_store ge chunk m addr v t m' -> possible_trace w t w' ->
  do_volatile_store w chunk m addr v = Some(w', t, m').


Definition do_deref_loc (w: world) (ty: type) (m: mem) (addr: expr_sym) : option (world * trace * expr_sym) :=
  match access_mode ty with
    | By_value chunk =>
      match type_is_volatile ty with
        | false => do v <- Mem.loadv chunk m addr; Some(w, E0, v)
        | true => do_volatile_load w chunk m addr
      end
    | By_reference => Some(w, E0, addr)
    | By_copy => Some(w, E0, addr)
    | _ => None
  end.

Definition assign_copy_ok (ty: type) (b: block) (ofs: int) (b': block) (ofs': int) : Prop :=
  (alignof_blockcopy ty | Int.unsigned ofs') /\ (alignof_blockcopy ty | Int.unsigned ofs) /\
  (b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs
           \/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs
           \/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs').

Remark check_assign_copy:
  forall (ty: type) (b: block) (ofs: int) (b': block) (ofs': int),
  { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }.

Definition inbound_dec:
  forall b o,
    {NormaliseSpec.in_bound o b} + {~ NormaliseSpec.in_bound o b}.

Definition do_assign_loc (w: world) (ty: type) (m: mem) (addr: expr_sym) (v: expr_sym): option (world * trace * mem) :=
  match access_mode ty with
  | By_value chunk =>
      match type_is_volatile ty with
      | false => do m' <- Mem.storev chunk m addr v; Some(w, E0, m')
      | true => do_volatile_store w chunk m addr v
      end
  | By_copy =>
    if zeq (sizeof ty) 0
    then Some (w,E0,m)
    else
      match Mem.mem_norm m v with
        | Vptr b' ofs' =>
          match Mem.mem_norm m addr with
            | Vptr b ofs =>
              if check_assign_copy ty b ofs b' ofs' then
                do bytes <- Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ty);
                do m' <- Mem.storebytes m b (Int.unsigned ofs) bytes;
                Some(w, E0, m')
              else None
            | _ => None
          end
      | _ => None
      end
  | _ => None
  end.

Lemma do_deref_loc_sound:
  forall w ty m addr w' t v ,
  do_deref_loc w ty m addr = Some(w', t, v) ->
  deref_loc ge ty m addr t v /\ possible_trace w t w'.

Lemma do_deref_loc_complete:
  forall w ty m addr w' t v ,
  deref_loc ge ty m addr t v -> possible_trace w t w' ->
  do_deref_loc w ty m addr = Some(w', t, v).

Lemma do_assign_loc_sound:
  forall w ty m addr v w' t m' ,
  do_assign_loc w ty m addr v = Some(w', t, m') ->
  assign_loc ge ty m addr v t m' /\ possible_trace w t w'.

Lemma do_assign_loc_complete:
  forall w ty m addr v w' t m',
  assign_loc ge ty m addr v t m' -> possible_trace w t w' ->
  do_assign_loc w ty m addr v = Some(w', t, m').


Variable do_external_function:
  ident -> signature -> genv -> world -> list expr_sym -> mem -> option (world * trace * expr_sym * mem).

Hypothesis do_external_function_sound:
  forall id sg ge vargs m t vres m' w w',
  do_external_function id sg ge w vargs m = Some(w', t, vres, m') ->
  external_functions_sem id sg ge vargs m t vres m' /\ possible_trace w t w'.

Hypothesis do_external_function_complete:
  forall id sg ge vargs m t vres m' w w',
  external_functions_sem id sg ge vargs m t vres m' ->
  possible_trace w t w' ->
  do_external_function id sg ge w vargs m = Some(w', t, vres, m').

Variable do_inline_assembly:
  ident -> genv -> world -> list expr_sym -> mem -> option (world * trace * expr_sym * mem).

Hypothesis do_inline_assembly_sound:
  forall txt ge vargs m t vres m' w w',
  do_inline_assembly txt ge w vargs m = Some(w', t, vres, m') ->
  inline_assembly_sem txt ge vargs m t vres m' /\ possible_trace w t w'.

Hypothesis do_inline_assembly_complete:
  forall txt ge vargs m t vres m' w w',
  inline_assembly_sem txt ge vargs m t vres m' ->
  possible_trace w t w' ->
  do_inline_assembly txt ge w vargs m = Some(w', t, vres, m').

Definition do_ef_volatile_load (chunk: memory_chunk)
       (w: world) (vargs: list expr_sym) (m: mem) : option (world * trace * expr_sym * mem) :=
  match vargs with
  | addr :: nil => do w',t,v <- do_volatile_load w chunk m addr; Some(w',t,v,m)
  | _ => None
  end.

Definition do_ef_volatile_store (chunk: memory_chunk)
       (w: world) (vargs: list expr_sym) (m: mem) : option (world * trace * expr_sym * mem) :=
  match vargs with
    | addr :: v :: nil => do w',t,m' <- do_volatile_store w chunk m addr v;
        Some(w',t,Eval Vundef,m')
  | _ => None
  end.

Definition do_ef_volatile_load_global (chunk: memory_chunk) (id: ident) (ofs: int)
       (w: world) (vargs: list expr_sym) (m: mem) : option (world * trace * expr_sym * mem) :=
  do b <- Genv.find_symbol ge id; do_ef_volatile_load chunk w (Eval (Vptr b ofs) :: vargs) m.

Definition do_ef_volatile_store_global (chunk: memory_chunk) (id: ident) (ofs: int)
       (w: world) (vargs: list expr_sym) (m: mem) : option (world * trace * expr_sym * mem) :=
  do b <- Genv.find_symbol ge id; do_ef_volatile_store chunk w (Eval (Vptr b ofs) :: vargs) m.

Definition do_ef_malloc
           (w: world) (vargs: list expr_sym) (m: mem) : option (world * trace * expr_sym * mem) :=
  match vargs with
  | v :: nil =>
    match Mem.mem_norm m v with
      Vint n =>
      do m'b <- Mem.alloc m 0 (Int.unsigned n + 4) Dynamic;
        let (m', b) := m'b in
        do m'' <- Mem.store Mint32 m' b 0 (Eval (Vint n));
          Some(w, E0, Eval (Vptr b (Int.repr 4)), m'')
    | _ => None
    end
    | _ => None
  end.

Definition do_ef_free
       (w: world) (vargs: list expr_sym) (m: mem) : option (world * trace * expr_sym * mem) :=
  match vargs with
  | v :: nil =>
    match Mem.mem_norm m v with
      Vptr b lo =>
      do vsz <- Mem.load Mint32 m b (Int.unsigned lo - 4);
      match Mem.mem_norm m vsz with
      | Vint sz =>
        check (zlt 0 (Int.unsigned sz));
          match PMap.get b (Mem.mem_blocktype m) with
            Some Dynamic =>
            do m' <- Mem.free m b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz);
              Some(w, E0, Eval Vundef, m')
          | _ => None
          end
      | _ => None
      end
    | _ => None
    end
  | _ => None
  end.

Definition memcpy_args_ok
  (sz al: Z) (bdst: block) (odst: Z) (bsrc: block) (osrc: Z) : Prop :=
      (al = 1 \/ al = 2 \/ al = 4 \/ al = 8)
   /\ sz >= 0 /\ (al | sz)
   /\ (sz > 0 -> (al | osrc))
   /\ (sz > 0 -> (al | odst))
   /\ (bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc).

Remark memcpy_check_args:
  forall sz al bdst odst bsrc osrc,
  {memcpy_args_ok sz al bdst odst bsrc osrc} + {~memcpy_args_ok sz al bdst odst bsrc osrc}.


Definition do_ef_memcpy (sz al: Z)
           (w: world) (vargs: list expr_sym) (m: mem) : option (world * trace * expr_sym * mem) :=
  if zeq sz 0
  then
    match vargs with
      v :: v' :: nil => Some (w, E0, Eval Vundef, m)
    | _ => None
    end
  else
  match vargs with
      v :: v' :: nil =>
      match Mem.mem_norm m v, Mem.mem_norm m v' with
          Vptr bdst odst, Vptr bsrc osrc =>
          if memcpy_check_args sz al bdst (Int.unsigned odst) bsrc (Int.unsigned osrc) then
            do bytes <- Mem.loadbytes m bsrc (Int.unsigned osrc) sz;
            do m' <- Mem.storebytes m bdst (Int.unsigned odst) bytes;
            Some(w, E0, Eval Vundef, m')
          else None
        | _, _ => None
      end
  | _ => None
  end.

Definition do_ef_annot (text: ident) (targs: list annot_arg)
       (w: world) (vargs: list expr_sym) (m: mem) : option (world * trace * expr_sym * mem) :=
  do args <- list_eventval_of_val (map (Mem.mem_norm m) vargs) (annot_args_typ targs);
  Some(w, Event_annot text (annot_eventvals targs args) :: E0, Eval Vundef, m).

Definition do_ef_annot_val (text: ident) (targ: typ)
       (w: world) (vargs: list expr_sym) (m: mem) : option (world * trace * expr_sym * mem) :=
  match vargs with
  | varg :: nil =>
      do arg <- eventval_of_val (Mem.mem_norm m varg) targ;
      Some(w, Event_annot text (arg :: nil) :: E0, varg, m)
  | _ => None
  end.

Definition do_external (ef: external_function):
       world -> list expr_sym -> mem -> option (world * trace * expr_sym * mem) :=
  match ef with
  | EF_external name sg => do_external_function name sg ge
  | EF_builtin name sg => do_external_function name sg ge
  | EF_vload chunk => do_ef_volatile_load chunk
  | EF_vstore chunk => do_ef_volatile_store chunk
  | EF_vload_global chunk id ofs => do_ef_volatile_load_global chunk id ofs
  | EF_vstore_global chunk id ofs => do_ef_volatile_store_global chunk id ofs
  | EF_memcpy sz al => do_ef_memcpy sz al
  | EF_inline_asm text => do_inline_assembly text ge
  | EF_malloc => do_ef_malloc
  | EF_free => do_ef_free
  | EF_annot i laa => do_ef_annot i laa
  | EF_annot_val i laa => do_ef_annot_val i laa
  end.

Lemma do_ef_external_sound:
  forall ef w vargs m w' t vres m',
  do_external ef w vargs m = Some(w', t, vres, m') ->
  external_call ef ge vargs m t vres m' /\ possible_trace w t w'.

Lemma do_ef_external_complete:
  forall ef w vargs m w' t vres m',
  external_call ef ge vargs m t vres m' -> possible_trace w t w' ->
  do_external ef w vargs m = Some(w', t, vres, m').

Reduction of expressions

Inductive reduction: Type :=
  | Lred (l': expr) (m': mem)
  | Rred (r': expr) (m': mem) (t: trace)
  | Callred (fd: fundef) (args: list expr_sym) (tyres: type) (m': mem)
  | Stuckred.

Section EXPRS.

Variable e: env.
Variable w: world.

Fixpoint sem_cast_arguments (vtl: list (expr_sym * type)) (tl: typelist): option (list expr_sym) :=
  match vtl, tl with
  | nil, Tnil => Some nil
  | (v1,t1)::vtl, Tcons t1' tl =>
    do v <- sem_cast_expr v1 t1 t1';
      do vl <- sem_cast_arguments vtl tl ;
      Some(v::vl)
  | (v1,t1)::vtl, Tnil => None
  | _, _ => None
  end.


Definition reducts (A: Type): Type := list ((expr -> A) * reduction).

Definition topred (r: reduction) : reducts expr :=
  ((fun (x: expr) => x), r) :: nil.

Definition stuck : reducts expr :=
  ((fun (x: expr) => x), Stuckred) :: nil.

Definition incontext {A B: Type} (ctx: A -> B) (ll: reducts A) : reducts B :=
  map (fun z => ((fun (x: expr) => ctx(fst z x)), snd z)) ll.

Definition incontext2 {A1 A2 B: Type}
                     (ctx1: A1 -> B) (ll1: reducts A1)
                     (ctx2: A2 -> B) (ll2: reducts A2) : reducts B :=
  incontext ctx1 ll1 ++ incontext ctx2 ll2.

Notation "'do' X <- A ; B" := (match A with Some X => B | None => stuck end)
  (at level 200, X ident, A at level 100, B at level 200)
  : reducts_monad_scope.

Notation "'do' X , Y <- A ; B" := (match A with Some (X, Y) => B | None => stuck end)
  (at level 200, X ident, Y ident, A at level 100, B at level 200)
  : reducts_monad_scope.

Notation "'do' X , Y , Z <- A ; B" := (match A with Some (X, Y, Z) => B | None => stuck end)
  (at level 200, X ident, Y ident, Z ident, A at level 100, B at level 200)
  : reducts_monad_scope.

Notation " 'check' A ; B" := (if A then B else stuck)
  (at level 200, A at level 100, B at level 200)
  : reducts_monad_scope.

Local Open Scope reducts_monad_scope.

Fixpoint typelist_to_coq_type_list (tl:typelist) : (list type) :=
  match tl with
    | Tnil => nil
    | Tcons t tl => t::(typelist_to_coq_type_list tl)
  end.


Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
  match k, a with
  | LV, Eloc ptr ty =>
      nil
  | LV, Evar x ty =>
      match e!x with
      | Some(b, ty') =>
          check type_eq ty ty';
          topred (Lred (Eloc (Eval (Vptr b Int.zero)) ty) m)
      | None =>
          do b <- Genv.find_symbol ge x;
          topred (Lred (Eloc (Eval (Vptr b Int.zero)) ty) m)
      end
  | LV, Ederef r ty =>
      match is_val r with
      | Some (e,ty') =>
        topred (Lred (Eloc e ty) m)
      | None =>
          incontext (fun x => Ederef x ty) (step_expr RV r m)
      end
  | LV, Efield r f ty =>
    match is_val r with
      | Some (e, ty') =>
        match ty' with
          | Tstruct id fList _ =>
            match field_offset f fList with
              | Error _ => stuck
              | OK delta =>
                topred (Lred (Eloc
                                (Val.add e (Eval (Vint (Int.repr delta))))
                                ty) m)
            end
          | Tunion id fList _ =>
            topred (Lred (Eloc e ty) m)
          | _ => stuck
        end
      | None =>
          incontext (fun x => Efield x f ty) (step_expr RV r m)
      end
  | RV, Csyntax.Eval v ty =>
      nil
  | RV, Csyntax.Evalof l ty =>
      match is_loc l with
      | Some(ptr, ty') =>
          check type_eq ty ty';
          do w',t,v <- do_deref_loc w ty m ptr ;
          topred (Rred (Csyntax.Eval v ty) m t)
      | None =>
          incontext (fun x => Csyntax.Evalof x ty) (step_expr LV l m)
      end
  | RV, Eaddrof l ty =>
      match is_loc l with
      | Some(ptr, ty') => topred (Rred (Csyntax.Eval ptr ty) m E0)
      | None => incontext (fun x => Eaddrof x ty) (step_expr LV l m)
      end
  | RV, Csyntax.Eunop op r1 ty =>
      match is_val r1 with
      | Some(v1, ty1) =>
          let v := sem_unary_operation_expr op v1 ty1 in
          topred (Rred (Csyntax.Eval v ty) m E0)
      | None =>
          incontext (fun x => Csyntax.Eunop op x ty) (step_expr RV r1 m)
      end
  | RV, Csyntax.Ebinop op r1 r2 ty =>
      match is_val r1, is_val r2 with
      | Some(v1, ty1), Some(v2, ty2) =>
          do v <- sem_binary_operation_expr op v1 ty1 v2 ty2;
          topred (Rred (Csyntax.Eval v ty) m E0)
      | _, _ =>
         incontext2 (fun x => Csyntax.Ebinop op x r2 ty) (step_expr RV r1 m)
                    (fun x => Csyntax.Ebinop op r1 x ty) (step_expr RV r2 m)
      end
  | RV, Ecast r1 ty =>
      match is_val r1 with
      | Some(v1, ty1) =>
          do v <- sem_cast_expr v1 ty1 ty;
          topred (Rred (Csyntax.Eval v ty) m E0)
      | None =>
          incontext (fun x => Ecast x ty) (step_expr RV r1 m)
      end
  | RV, Eseqand r1 r2 ty =>
      match is_val r1 with
      | Some(v1, ty1) =>
        match Mem.mem_norm m (bool_expr v1 ty1) with
            Vint b =>
            if negb (Int.eq b Int.zero) then topred (Rred (Eparen (Eparen r2 type_bool) ty) m E0)
            else topred (Rred (Csyntax.Eval (Eval (Vint Int.zero)) ty) m E0)
          | _ => stuck
        end
      | None =>
          incontext (fun x => Eseqand x r2 ty) (step_expr RV r1 m)
      end
  | RV, Eseqor r1 r2 ty =>
      match is_val r1 with
        | Some(v1, ty1) =>
          match Mem.mem_norm m (bool_expr v1 ty1) with
              Vint b =>
              if negb (Int.eq b Int.zero)
              then topred (Rred (Csyntax.Eval (Eval (Vint Int.one)) ty) m E0)
              else topred (Rred (Eparen (Eparen r2 type_bool) ty) m E0)
            | _ =>
              stuck
          end
      | None =>
          incontext (fun x => Eseqor x r2 ty) (step_expr RV r1 m)
      end
  | RV, Econdition r1 r2 r3 ty =>
    match is_val r1 with
      | Some(v1, ty1) =>
        match Mem.mem_norm m (bool_expr v1 ty1) with
            Vint b =>
            topred (Rred (Eparen (if negb (Int.eq b Int.zero) then r2 else r3) ty) m E0)
          | _ =>
            stuck
        end
      | None =>
        incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m)
    end
  | RV, Esizeof ty' ty =>
      topred (Rred (Csyntax.Eval (Eval (Vint (Int.repr (sizeof ty')))) ty) m E0)
  | RV, Ealignof ty' ty =>
      topred (Rred (Csyntax.Eval (Eval (Vint (Int.repr (alignof ty')))) ty) m E0)
  | RV, Eassign l1 r2 ty =>
      match is_loc l1, is_val r2 with
      | Some(ptr, ty1), Some(v2, ty2) =>
          check type_eq ty1 ty;
          do v <- sem_cast_expr v2 ty2 ty1;
          do w',t,m' <- do_assign_loc w ty1 m ptr v;
          topred (Rred (Csyntax.Eval v ty) m' t)
      | _, _ =>
         incontext2 (fun x => Eassign x r2 ty) (step_expr LV l1 m)
                    (fun x => Eassign l1 x ty) (step_expr RV r2 m)
      end
  | RV, Eassignop op l1 r2 tyres ty =>
      match is_loc l1, is_val r2 with
      | Some(ptr, ty1), Some(v2, ty2) =>
          check type_eq ty1 ty;
          do w',t,v1 <- do_deref_loc w ty1 m ptr;
          let r' := Eassign (Eloc ptr ty1)
                           (Csyntax.Ebinop op (Csyntax.Eval v1 ty1) (Csyntax.Eval v2 ty2) tyres) ty1 in
          topred (Rred r' m t)
      | _, _ =>
         incontext2 (fun x => Eassignop op x r2 tyres ty) (step_expr LV l1 m)
                    (fun x => Eassignop op l1 x tyres ty) (step_expr RV r2 m)
      end
  | RV, Epostincr id l ty =>
      match is_loc l with
      | Some(ptr, ty1) =>
          check type_eq ty1 ty;
          do w',t, v1 <- do_deref_loc w ty m ptr;
          let op := match id with Incr => Oadd | Decr => Osub end in
          let r' :=
            Ecomma (Eassign (Eloc ptr ty)
                           (Csyntax.Ebinop op (Csyntax.Eval v1 ty) (Csyntax.Eval (Eval (Vint Int.one)) type_int32s) (incrdecr_type ty))
                           ty)
                   (Csyntax.Eval v1 ty) ty in
          topred (Rred r' m t)
      | None =>
          incontext (fun x => Epostincr id x ty) (step_expr LV l m)
      end
  | RV, Ecomma r1 r2 ty =>
      match is_val r1 with
      | Some _ =>
          check type_eq (typeof r2) ty;
          topred (Rred r2 m E0)
      | None =>
          incontext (fun x => Ecomma x r2 ty) (step_expr RV r1 m)
      end
  | RV, Eparen r1 ty =>
      match is_val r1 with
      | Some (v1, ty1) =>
          do v <- sem_cast_expr v1 ty1 ty;
          topred (Rred (Csyntax.Eval v ty) m E0)
      | None =>
          incontext (fun x => Eparen x ty) (step_expr RV r1 m)
      end
  | RV, Ecall r1 rargs ty =>
      match is_val r1, is_val_list rargs with
      | Some(vf, tyf), Some vtl =>
          match classify_fun tyf with
          | fun_case_f tyargs tyres cconv =>
              do fd <- Genv.find_funct m ge vf;
              do vargs <- sem_cast_arguments vtl tyargs;
              check type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv);
              
              topred (Callred fd vargs ty m)
          | _ => stuck
          end
      | _, _ =>
          incontext2 (fun x => Ecall x rargs ty) (step_expr RV r1 m)
                     (fun x => Ecall r1 x ty) (step_exprlist rargs m)
      end
  | RV, Ebuiltin ef tyargs rargs ty =>
      match is_val_list rargs with
      | Some vtl =>
          do vargs <- sem_cast_arguments vtl tyargs;
          match do_external ef w vargs m with
          | None => stuck
          | Some(w',t,v,m') => topred (Rred (Csyntax.Eval v ty) m' t)
          end
      | _ =>
          incontext (fun x => Ebuiltin ef tyargs x ty) (step_exprlist rargs m)
      end
  | _, _ => stuck
  end

with step_exprlist (rl: exprlist) (m: mem): reducts exprlist :=
  match rl with
  | Enil =>
      nil
  | Econs r1 rs =>
      incontext2 (fun x => Econs x rs) (step_expr RV r1 m)
                 (fun x => Econs r1 x) (step_exprlist rs m)
  end.


Inductive imm_safe_t: kind -> expr -> mem -> Prop :=
  | imm_safe_t_val: forall v ty m,
      imm_safe_t RV (Csyntax.Eval v ty) m
  | imm_safe_t_loc: forall ptr ty m,
      imm_safe_t LV (Eloc ptr ty) m
  | imm_safe_t_lred: forall to C l m l' m',
      lred ge e l m l' m' ->
      context LV to C ->
      imm_safe_t to (C l) m
  | imm_safe_t_rred: forall to C r m t r' m' w',
      rred ge r m t r' m' -> possible_trace w t w' ->
      context RV to C ->
      imm_safe_t to (C r) m
  | imm_safe_t_callred: forall to C r m fd args ty,
      callred ge m r fd args ty ->
      context RV to C ->
      imm_safe_t to (C r) m.

Remark imm_safe_t_imm_safe:
  forall k a m, imm_safe_t k a m -> imm_safe ge e k a m.


Fixpoint exprlist_all_values (rl: exprlist) : Prop :=
  match rl with
  | Enil => True
  | Econs (Csyntax.Eval v ty) rl' => exprlist_all_values rl'
  | Econs _ _ => False
  end.

Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
  match a with
  | Eloc ptr ty => False
  | Evar x ty =>
      exists b,
      e!x = Some(b, ty)
      \/ (e!x = None /\ Genv.find_symbol ge x = Some b)
  | Ederef (Csyntax.Eval v ty1) ty =>
    True
  | Efield (Csyntax.Eval v ty1) f ty =>
      match ty1 with
      | Tstruct _ fList _ => exists delta, field_offset f fList = Errors.OK delta
      | Tunion _ _ _ => True
      | _ => False
      end
  | Csyntax.Eval v ty => False
  | Csyntax.Evalof (Eloc ptr ty') ty =>
      ty' = ty /\ exists t, exists v, exists w' , deref_loc ge ty m ptr t v /\ possible_trace w t w'
  | Csyntax.Eunop op (Csyntax.Eval v1 ty1) ty =>
      exists v, sem_unary_operation_expr op v1 ty1 = v
  | Csyntax.Ebinop op (Csyntax.Eval v1 ty1) (Csyntax.Eval v2 ty2) ty =>
      exists v, sem_binary_operation_expr op v1 ty1 v2 ty2 = Some v
  | Ecast (Csyntax.Eval v1 ty1) ty =>
      exists v, sem_cast_expr v1 ty1 ty = Some v
  | Eseqand (Csyntax.Eval v1 ty1) r2 ty =>
      exists b, Mem.mem_norm m (bool_expr v1 ty1) = Vint b
  | Eseqor (Csyntax.Eval v1 ty1) r2 ty =>
      exists b, Mem.mem_norm m (bool_expr v1 ty1) = Vint b
  | Econdition (Csyntax.Eval v1 ty1) r1 r2 ty =>
      exists b, Mem.mem_norm m (bool_expr v1 ty1) = Vint b
  | Eassign (Eloc ptr ty1) (Csyntax.Eval v2 ty2) ty =>
      exists v, exists m', exists t, exists w' ,
      ty = ty1 /\ sem_cast_expr v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m ptr v t m' /\ possible_trace w t w'
  | Eassignop op (Eloc ptr ty1) (Csyntax.Eval v2 ty2) tyres ty =>
      exists t, exists v1, exists w' ,
      ty = ty1 /\ deref_loc ge ty1 m ptr t v1 /\ possible_trace w t w'
  | Epostincr id (Eloc ptr ty1) ty =>
      exists t, exists v1, exists w' ,
      ty = ty1 /\ deref_loc ge ty m ptr t v1 /\ possible_trace w t w'
  | Ecomma (Csyntax.Eval v ty1) r2 ty =>
      typeof r2 = ty
  | Eparen (Csyntax.Eval v1 ty1) ty =>
      exists v, sem_cast_expr v1 ty1 ty = Some v
  | Ecall (Csyntax.Eval vf tyf) rargs ty =>
      exprlist_all_values rargs ->
      exists tyargs tyres cconv fd vl,
         classify_fun tyf = fun_case_f tyargs tyres cconv
      /\ Genv.find_funct m ge vf = Some fd
      /\ cast_arguments rargs tyargs vl
      /\ type_of_fundef fd = Tfunction tyargs tyres cconv
  | Ebuiltin ef tyargs rargs ty =>
      exprlist_all_values rargs ->
      exists vargs t vres m' w',
         cast_arguments rargs tyargs vargs
      /\ external_call ef ge vargs m t vres m'
      /\ possible_trace w t w'
  | _ => True
  end.

Lemma lred_invert:
  forall l m l' m', lred ge e l m l' m' -> invert_expr_prop l m.

Lemma rred_invert:
  forall w' r m t r' m', rred ge r m t r' m' -> possible_trace w t w' -> invert_expr_prop r m.

Lemma callred_invert:
  forall r fd args ty m,
  callred ge m r fd args ty ->
  invert_expr_prop r m.

Scheme context_ind2 := Minimality for context Sort Prop
  with contextlist_ind2 := Minimality for contextlist Sort Prop.
Combined Scheme context_contextlist_ind from context_ind2, contextlist_ind2.

Lemma invert_expr_context:
  (forall from to C, context from to C ->
   forall a m,
   invert_expr_prop a m ->
   invert_expr_prop (C a) m)
/\(forall from C, contextlist from C ->
  forall a m,
  invert_expr_prop a m ->
  ~exprlist_all_values (C a)).

Lemma imm_safe_t_inv:
  forall k a m,
  imm_safe_t k a m ->
  match a with
  | Eloc _ _ => True
  | Csyntax.Eval _ _ => True
  | _ => invert_expr_prop a m
  end.


Lemma context_compose:
  forall k2 k3 C2, context k2 k3 C2 ->
  forall k1 C1, context k1 k2 C1 ->
  context k1 k3 (fun x => C2(C1 x))
with contextlist_compose:
  forall k2 C2, contextlist k2 C2 ->
  forall k1 C1, context k1 k2 C1 ->
  contextlist k1 (fun x => C2(C1 x)).

Hint Constructors context contextlist.
Hint Resolve context_compose contextlist_compose.

Definition reduction_ok (k: kind) (a: expr) (m: mem) (rd: reduction) : Prop :=
  match k, rd with
  | LV, Lred l' m' => lred ge e a m l' m'
  | RV, Rred r' m' t => rred ge a m t r' m' /\ exists w', possible_trace w t w'
  | RV, Callred fd args tyres m' => callred ge m a fd args tyres /\ m' = m
  | LV, Stuckred => ~imm_safe_t k a m
  | RV, Stuckred => ~imm_safe_t k a m
  | _, _ => False
  end.

Definition reducts_ok (k: kind) (a: expr) (m: mem) (ll: reducts expr) : Prop :=
  (forall C rd,
      In (C, rd) ll ->
      exists a', exists k', context k' k C /\ a = C a' /\ reduction_ok k' a' m rd)
  /\ (ll = nil -> match k with LV => is_loc a <> None | RV => is_val a <> None end).

Definition list_reducts_ok (al: exprlist) (m: mem) (ll: reducts exprlist) : Prop :=
  (forall C rd,
      In (C, rd) ll ->
      exists a', exists k', contextlist k' C /\ al = C a' /\ reduction_ok k' a' m rd)
  /\ (ll = nil -> is_val_list al <> None).

Ltac monadInv :=
  match goal with
  | [ H: match ?x with Some _ => _ | None => None end = Some ?y |- _ ] =>
      destruct x eqn:?; [monadInv|discriminate]
  | [ H: match ?x with left _ => _ | right _ => None end = Some ?y |- _ ] =>
      destruct x; [monadInv|discriminate]
  | _ => idtac
  end.

Lemma sem_cast_arguments_sound:
  forall rargs vtl tyargs vargs,
  is_val_list rargs = Some vtl ->
  sem_cast_arguments vtl tyargs = Some vargs ->
  cast_arguments rargs tyargs vargs.

Lemma sem_cast_arguments_complete:
  forall al tyl vl,
  cast_arguments al tyl vl ->
  exists vtl, is_val_list al = Some vtl /\ sem_cast_arguments vtl tyl = Some vl.

Lemma topred_ok:
  forall k a m rd,
  reduction_ok k a m rd ->
  reducts_ok k a m (topred rd).

Lemma stuck_ok:
  forall k a m,
  ~imm_safe_t k a m ->
  reducts_ok k a m stuck.

Lemma wrong_kind_ok:
  forall k a m,
  k <> Cstrategy.expr_kind a ->
  reducts_ok k a m stuck.

Lemma not_invert_ok:
  forall k a m,
  match a with
  | Eloc _ _ => False
  | Csyntax.Eval _ _ => False
  | _ => invert_expr_prop a m -> False
  end ->
  reducts_ok k a m stuck.

Lemma incontext_ok:
  forall k a m C res k' a',
  reducts_ok k' a' m res ->
  a = C a' ->
  context k' k C ->
  match k' with LV => is_loc a' = None | RV => is_val a' = None end ->
  reducts_ok k a m (incontext C res).

Lemma incontext2_ok:
  forall k a m k1 a1 res1 k2 a2 res2 C1 C2,
  reducts_ok k1 a1 m res1 ->
  reducts_ok k2 a2 m res2 ->
  a = C1 a1 -> a = C2 a2 ->
  context k1 k C1 -> context k2 k C2 ->
  match k1 with LV => is_loc a1 = None | RV => is_val a1 = None end
  \/ match k2 with LV => is_loc a2 = None | RV => is_val a2 = None end ->
  reducts_ok k a m (incontext2 C1 res1 C2 res2).

Lemma incontext_list_ok:
  forall ef tyargs al ty m res,
  list_reducts_ok al m res ->
  is_val_list al = None ->
  reducts_ok RV (Ebuiltin ef tyargs al ty) m
                (incontext (fun x => Ebuiltin ef tyargs x ty) res).

Lemma incontext2_list_ok:
  forall a1 a2 ty m res1 res2,
  reducts_ok RV a1 m res1 ->
  list_reducts_ok a2 m res2 ->
  is_val a1 = None \/ is_val_list a2 = None ->
  reducts_ok RV (Ecall a1 a2 ty) m
               (incontext2 (fun x => Ecall x a2 ty) res1
                           (fun x => Ecall a1 x ty) res2).

Lemma incontext2_list_ok':
  forall a1 a2 m res1 res2,
  reducts_ok RV a1 m res1 ->
  list_reducts_ok a2 m res2 ->
  list_reducts_ok (Econs a1 a2) m
               (incontext2 (fun x => Econs x a2) res1
                           (fun x => Econs a1 x) res2).

Lemma is_val_list_all_values:
  forall al vtl, is_val_list al = Some vtl -> exprlist_all_values al.

Ltac myinv :=
  match goal with
  | [ H: False |- _ ] => destruct H
  | [ H: _ /\ _ |- _ ] => destruct H; myinv
  | [ H: exists _, _ |- _ ] => destruct H; myinv
  | _ => idtac
  end.

Lemma norm_cmp_one_zero:
  forall m v ty i,
    Mem.mem_norm m (bool_expr v ty) = Vint i ->
    i = Int.one \/ i = Int.zero.

Theorem step_expr_sound:
  forall a k m, reducts_ok k a m (step_expr k a m)
with step_exprlist_sound:
  forall al m, list_reducts_ok al m (step_exprlist al m).

Lemma step_exprlist_val_list:
  forall m al, is_val_list al <> None -> step_exprlist al m = nil.


Lemma lred_topred:
  forall l1 m1 l2 m2,
  lred ge e l1 m1 l2 m2 ->
  step_expr LV l1 m1 = topred (Lred l2 m2).

Lemma rred_topred:
  forall w' r1 m1 t r2 m2,
  rred ge r1 m1 t r2 m2 -> possible_trace w t w' ->
  step_expr RV r1 m1 = topred (Rred r2 m2 t).

Lemma callred_topred:
  forall a fd args ty m,
  callred ge m a fd args ty ->
  step_expr RV a m = topred (Callred fd args ty m).

Definition reducts_incl {A B: Type} (C: A -> B) (res1: reducts A) (res2: reducts B) : Prop :=
  forall C1 rd, In (C1, rd) res1 -> In ((fun x => C(C1 x)), rd) res2.

Lemma reducts_incl_trans:
  forall (A1 A2: Type) (C: A1 -> A2) res1 res2, reducts_incl C res1 res2 ->
  forall (A3: Type) (C': A2 -> A3) res3,
  reducts_incl C' res2 res3 ->
  reducts_incl (fun x => C'(C x)) res1 res3.

Lemma reducts_incl_nil:
  forall (A B: Type) (C: A -> B) res,
  reducts_incl C nil res.

Lemma reducts_incl_val:
  forall (A: Type) a m v ty (C: expr -> A) res,
  is_val a = Some(v, ty) -> reducts_incl C (step_expr RV a m) res.

Lemma reducts_incl_loc:
  forall (A: Type) a m ptr ty (C: expr -> A) res,
  is_loc a = Some(ptr, ty) -> reducts_incl C (step_expr LV a m) res.

Lemma reducts_incl_listval:
  forall (A: Type) a m vtl (C: exprlist -> A) res,
  is_val_list a = Some vtl -> reducts_incl C (step_exprlist a m) res.

Lemma reducts_incl_incontext:
  forall (A B: Type) (C: A -> B) res,
  reducts_incl C res (incontext C res).

Lemma reducts_incl_incontext2_left:
  forall (A1 A2 B: Type) (C1: A1 -> B) res1 (C2: A2 -> B) res2,
  reducts_incl C1 res1 (incontext2 C1 res1 C2 res2).

Lemma reducts_incl_incontext2_right:
  forall (A1 A2 B: Type) (C1: A1 -> B) res1 (C2: A2 -> B) res2,
  reducts_incl C2 res2 (incontext2 C1 res1 C2 res2).

Hint Resolve reducts_incl_val reducts_incl_loc reducts_incl_listval
             reducts_incl_incontext reducts_incl_incontext2_left reducts_incl_incontext2_right.

Lemma step_expr_context:
  forall from to C, context from to C ->
  forall a m, reducts_incl C (step_expr from a m) (step_expr to (C a) m)
with step_exprlist_context:
  forall from C, contextlist from C ->
  forall a m, reducts_incl C (step_expr from a m) (step_exprlist (C a) m).


Lemma not_stuckred_imm_safe:
  forall m a k,
  (forall C, ~In (C, Stuckred) (step_expr k a m)) -> imm_safe_t k a m.

Lemma not_imm_safe_stuck_red:
  forall m a k C,
  context k RV C ->
  ~imm_safe_t k a m ->
  exists C', In (C', Stuckred) (step_expr RV (C a) m).


Lemma imm_safe_imm_safe_t:
  forall k a m,
  imm_safe ge e k a m ->
  imm_safe_t k a m \/
  exists C, exists a1, exists t, exists a1', exists m',
    context RV k C /\ a = C a1 /\ rred ge a1 m t a1' m' /\ forall w', ~possible_trace w t w'.


Definition can_crash_world (w: world) (S: state) : Prop :=
  exists t, exists S', (fun ge => Csem.step ge needed_stackspace) ge S t S' /\ forall w', ~possible_trace w t w'.

Theorem not_imm_safe_t:
  forall K C a m f k,
  context K RV C ->
  ~imm_safe_t K a m ->
  Csem.step ge needed_stackspace (ExprState f (C a) k e m) E0 Stuckstate \/ can_crash_world w (ExprState f (C a) k e m).

End EXPRS.

Transitions over states.

Fixpoint do_alloc_variables (e: env) (m: mem) (l: list (ident * type)) {struct l} : option (env * mem) :=
  match l with
  | nil => Some (e,m)
  | (id, ty) :: l' =>
    match Mem.alloc m 0 (sizeof ty) Normal with
        Some (m1,b1) =>
        do_alloc_variables (PTree.set id (b1, ty) e) m1 l'
      | _ => None
    end
end.

Lemma do_alloc_variables_sound:
  forall l e m e' m',
    do_alloc_variables e m l = Some (e', m') ->
    alloc_variables e m l e' m'.

Lemma do_alloc_variables_complete:
  forall e1 m1 l e2 m2, alloc_variables e1 m1 l e2 m2 ->
  do_alloc_variables e1 m1 l = Some (e2, m2).

Function sem_bind_parameters (w: world) (e: env) (m: mem) (l: list (ident * type)) (lv: list expr_sym)
                          {struct l} : option mem :=
  match l, lv with
  | nil, nil => Some m
  | (id, ty) :: params, v1::lv =>
      match PTree.get id e with
         | Some (b, ty') =>
             check (type_eq ty ty');
             do w', t, m1 <- do_assign_loc w ty m (Eval (Vptr b Int.zero)) v1;
             match t with nil => sem_bind_parameters w e m1 params lv | _ => None end
        | None => None
      end
   | _, _ => None
end.

Lemma sem_bind_parameters_sound : forall w e m l lv m',
  sem_bind_parameters w e m l lv = Some m' ->
  bind_parameters ge e m l lv m'.

Lemma sem_bind_parameters_complete : forall w e m l lv m',
  bind_parameters ge e m l lv m' ->
  sem_bind_parameters w e m l lv = Some m'.

Definition expr_final_state (f: function) (k: cont) (e: env) (C_rd: (expr -> expr) * reduction) :=
  match snd C_rd with
  | Lred a m => (E0, ExprState f (fst C_rd a) k e m)
  | Rred a m t => (t, ExprState f (fst C_rd a) k e m)
  | Callred fd vargs ty m => (E0, Callstate fd vargs (Kcall f e (fst C_rd) ty k) m)
  | Stuck => (E0, Stuckstate)
  end.

Local Open Scope list_monad_scope.

Definition ret (S: state) : list (trace * state) := (E0, S) :: nil.

Definition do_step (w: world) (s: state) : list (trace * state) :=
  match s with

  | ExprState f a k e m =>
      match is_val a with
      | Some(v, ty) =>
        match k with
        | Kdo k => ret (State f Sskip k e m )
        | Kifthenelse s1 s2 k =>
          match Mem.mem_norm m (bool_expr v ty) with
              Vint b => ret (State f (if negb (Int.eq b Int.zero) then s1 else s2) k e m)
            | _ => nil
          end
        | Kwhile1 x s k =>
          match Mem.mem_norm m (bool_expr v ty) with
              Vint b =>
              if negb (Int.eq b Int.zero) then ret (State f s (Kwhile2 x s k) e m) else ret (State f Sskip k e m)
            | _ => nil
          end
        | Kdowhile2 x s k =>
          match Mem.mem_norm m (bool_expr v ty) with
              Vint b =>
              if negb (Int.eq b Int.zero) then ret (State f (Sdowhile x s) k e m) else ret (State f Sskip k e m)
            | _ => nil
          end
        | Kfor2 a2 a3 s k =>
          match Mem.mem_norm m (bool_expr v ty) with
              Vint b =>
              if negb (Int.eq b Int.zero) then ret (State f s (Kfor3 a2 a3 s k) e m) else ret (State f Sskip k e m)
            | _ => nil
          end
        | Kreturn k =>
            do v' <- sem_cast_expr v ty f.(fn_return);
            do m' <- Mem.free_list m (blocks_of_env e);
            do m'' <- MemReserve.release_boxes m' (needed_stackspace (fn_id f));
            ret (Returnstate v' (call_cont k) m'')
        | Kswitch1 sl k =>
            do n <- sem_switch_arg_expr m v ty;
            ret (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m)
        | _ => nil
        end

      | None =>
          map (expr_final_state f k e) (step_expr e w RV a m)
      end

  | State f (Sdo x) k e m => ret(ExprState f x (Kdo k) e m)

  | State f (Ssequence s1 s2) k e m => ret(State f s1 (Kseq s2 k) e m)
  | State f Sskip (Kseq s k) e m => ret (State f s k e m)
  | State f Scontinue (Kseq s k) e m => ret (State f Scontinue k e m)
  | State f Sbreak (Kseq s k) e m => ret (State f Sbreak k e m)

  | State f (Sifthenelse a s1 s2) k e m => ret (ExprState f a (Kifthenelse s1 s2 k) e m)

  | State f (Swhile x s) k e m => ret (ExprState f x (Kwhile1 x s k) e m)
  | State f (Sskip|Scontinue) (Kwhile2 x s k) e m => ret (State f (Swhile x s) k e m)
  | State f Sbreak (Kwhile2 x s k) e m => ret (State f Sskip k e m)

  | State f (Sdowhile a s) k e m => ret (State f s (Kdowhile1 a s k) e m)
  | State f (Sskip|Scontinue) (Kdowhile1 x s k) e m => ret (ExprState f x (Kdowhile2 x s k) e m)
  | State f Sbreak (Kdowhile1 x s k) e m => ret (State f Sskip k e m)

  | State f (Sfor a1 a2 a3 s) k e m =>
      if is_skip a1
      then ret (ExprState f a2 (Kfor2 a2 a3 s k) e m)
      else ret (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m)
  | State f Sskip (Kfor3 a2 a3 s k) e m => ret (State f a3 (Kfor4 a2 a3 s k) e m)
  | State f Scontinue (Kfor3 a2 a3 s k) e m => ret (State f a3 (Kfor4 a2 a3 s k) e m)
  | State f Sbreak (Kfor3 a2 a3 s k) e m => ret (State f Sskip k e m)
  | State f Sskip (Kfor4 a2 a3 s k) e m => ret (State f (Sfor Sskip a2 a3 s) k e m)

  | State f (Sreturn None) k e m =>
    do m' <- Mem.free_list m (blocks_of_env e);
      do m'' <- MemReserve.release_boxes m' (needed_stackspace (fn_id f));
      ret (Returnstate (Eval Vundef) (call_cont k) m'')
  | State f (Sreturn (Some x)) k e m => ret (ExprState f x (Kreturn k) e m)
  | State f Sskip ((Kstop | Kcall _ _ _ _ _) as k) e m =>
    do m' <- Mem.free_list m (blocks_of_env e);
      do m'' <- MemReserve.release_boxes m' (needed_stackspace (fn_id f));
      ret (Returnstate (Eval Vundef) k m'')

  | State f (Sswitch x sl) k e m => ret (ExprState f x (Kswitch1 sl k) e m)
  | State f (Sskip|Sbreak) (Kswitch2 k) e m => ret (State f Sskip k e m)
  | State f Scontinue (Kswitch2 k) e m => ret (State f Scontinue k e m)

  | State f (Slabel lbl s) k e m => ret (State f s k e m)
  | State f (Sgoto lbl) k e m =>
      match find_label lbl f.(fn_body) (call_cont k) with
      | Some(s', k') => ret (State f s' k' e m)
      | None => nil
      end

  | Callstate (Internal f) vargs k m =>
      check (list_norepet_dec ident_eq (var_names (fn_params f) ++ var_names (fn_vars f)));
      match do_alloc_variables empty_env m (VarSort.varsort (f.(fn_params) ++ f.(fn_vars))) with
        Some (e, m1) =>
          match MemReserve.reserve_boxes m1 (needed_stackspace f.(fn_id)) with
            Some m2 =>
            do m3 <- sem_bind_parameters w e m2 f.(fn_params) vargs;
              ret (State f f.(fn_body) k e m3)
          | _ => nil
          end
        | _ => nil
      end
  | Callstate (External ef _ _ _) vargs k m =>
      match do_external ef w vargs m with
      | None => nil
      | Some(w',t,v,m') => (t, Returnstate v k m') :: nil
      end

  | Returnstate v (Kcall f e C ty k) m => ret (ExprState f (C (Csyntax.Eval v ty)) k e m)

  | _ => nil
  end.

Ltac myinv :=
  match goal with
  | [ |- In _ nil -> _ ] => intro X; elim X
  | [ |- In _ (ret _) -> _ ] =>
        intro X; elim X; clear X;
        [intro EQ; unfold ret in EQ; inv EQ; myinv | myinv]
  | [ |- In _ (_ :: nil) -> _ ] =>
        intro X; elim X; clear X; [intro EQ; inv EQ; myinv | myinv]
  | [ |- In _ (match ?x with Some _ => _ | None => _ end) -> _ ] => destruct x eqn:?; myinv
  | [ |- In _ (match ?x with false => _ | true => _ end) -> _ ] => destruct x eqn:?; myinv
  | [ |- In _ (match ?x with left _ => _ | right _ => _ end) -> _ ] => destruct x; myinv
  | _ => idtac
  end.

Hint Extern 3 => exact I.

Theorem do_step_sound:
  forall w S t S',
  In (t, S') (do_step w S) ->
  Csem.step ge needed_stackspace S t S' \/ (t = E0 /\ S' = Stuckstate /\ can_crash_world w S).

Remark estep_not_val:
  forall f a k e m t S, estep ge (ExprState f a k e m) t S -> is_val a = None.

Theorem do_step_complete:
  forall w S t S' w', possible_trace w t w' -> Csem.step ge needed_stackspace S t S' -> In (t, S') (do_step w S).

End EXEC.

Local Open Scope option_monad_scope.

Definition do_initial_state (p: program) sg: option (genv * state) :=
  let ge := Genv.globalenv p in
  do m0 <- Genv.init_mem fid sg p;
  do b <- Genv.find_symbol ge p.(prog_main);
  do f <- Genv.find_funct_ptr ge b;
  check (type_eq (type_of_fundef f) (Tfunction Tnil type_int32s cc_default));
  Some (ge, Callstate f nil Kstop m0).

Definition at_final_state (S: state): option int :=
  match S with
    | Returnstate res Kstop m =>
      match Mem.mem_norm m res with
          Vint r => Some r
        | _ => None
      end
    | _ => None
  end.