Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import AST.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Csyntax.
Require Import Csem.

Abstract syntax

Expressions

Inductive expr : Type :=
  | Econst_int: int -> type -> expr (* integer literal *)
  | Econst_float: float -> type -> expr (* float literal *)
  | Evar: ident -> type -> expr (* variable *)
  | Etempvar: ident -> type -> expr (* temporary variable *)
  | Ederef: expr -> type -> expr (* pointer dereference (unary *) *)
  | Eaddrof: expr -> type -> expr (* address-of operator (&) *)
  | Eunop: unary_operation -> expr -> type -> expr (* unary operation *)
  | Ebinop: binary_operation -> expr -> expr -> type -> expr (* binary operation *)
  | Ecast: expr -> type -> expr (* type cast ((ty) e) *)
  | Econdition: expr -> expr -> expr -> type -> expr (* conditional (e1 ? e2 : e3) *)
  | Efield: expr -> ident -> type -> expr. (* access to a member of a struct or union *)


Definition Esizeof (ty' ty: type) : expr := Econst_int (Int.repr(sizeof ty')) ty.
Definition Ealignof (ty' ty: type) : expr := Econst_int (Int.repr(alignof ty')) ty.


Definition typeof (e: expr) : type :=
  match e with
  | Econst_int _ ty => ty
  | Econst_float _ ty => ty
  | Evar _ ty => ty
  | Etempvar _ ty => ty
  | Ederef _ ty => ty
  | Eaddrof _ ty => ty
  | Eunop _ _ ty => ty
  | Ebinop _ _ _ ty => ty
  | Ecast _ ty => ty
  | Econdition _ _ _ ty => ty
  | Efield _ _ ty => ty
  end.

Statements

Definition label := ident.

Inductive statement : Type :=
  | Sskip : statement (* do nothing *)
  | Sassign : expr -> expr -> statement (* assignment lvalue = rvalue *)
  | Sset : ident -> expr -> statement (* assignment tempvar = rvalue *)
  | Svolread : ident -> expr -> statement (* volatile read tempvar = volatile lvalue *)
  | Scall: option ident -> expr -> list expr -> statement (* function call *)
  | Ssequence : statement -> statement -> statement (* sequence *)
  | Sifthenelse : expr -> statement -> statement -> statement (* conditional *)
  | Swhile : expr -> statement -> statement (* while loop *)
  | Sdowhile : expr -> statement -> statement (* do loop *)
  | Sfor': expr -> statement -> statement -> statement (* for loop *)
  | Sbreak : statement (* break statement *)
  | Scontinue : statement (* continue statement *)
  | Sreturn : option expr -> statement (* return statement *)
  | Sswitch : expr -> labeled_statements -> statement (* switch statement *)
  | Slabel : label -> statement -> statement
  | Sgoto : label -> statement

with labeled_statements : Type := (* cases of a switch *)
  | LSdefault: statement -> labeled_statements
  | LScase: int -> statement -> labeled_statements -> labeled_statements.


Definition Sfor (s1: statement) (e2: expr) (s3 s4: statement) :=
  Ssequence s1 (Sfor' e2 s3 s4).

Functions

Record function : Type := mkfunction {
  fn_return: type;
  fn_params: list (ident * type);
  fn_vars: list (ident * type);
  fn_temps: list (ident * type);
  fn_body: statement
}.

Definition var_names (vars: list(ident * type)) : list ident :=
  List.map (@fst ident type) vars.


Inductive fundef : Type :=
  | Internal: function -> fundef
  | External: external_function -> typelist -> type -> fundef.

Programs

Definition program : Type := AST.program fundef type.

Operations over types

Definition type_of_function (f: function) : type :=
  Tfunction (type_of_params (fn_params f)) (fn_return f).

Definition type_of_fundef (f: fundef) : type :=
  match f with
  | Internal fd => type_of_function fd
  | External id args res => Tfunction args res
  end.

Operational semantics

Definition genv := Genv.t fundef type.


Definition env := PTree.t (block * type).

Definition empty_env: env := (PTree.empty (block * type)).


Definition temp_env := PTree.t val.


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.


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.

Section SEMANTICS.

Variable ge: genv.


Definition type_of_global (b: block) : option type :=
  match Genv.find_var_info ge b with
  | Some gv => Some gv.(gvar_info)
  | None =>
      match Genv.find_funct_ptr ge b with
      | Some fd => Some(type_of_fundef fd)
      | None => None
      end
  end.

Evaluation of expressions

Section EXPR.

Variable e: env.
Variable le: temp_env.
Variable m: mem.


Inductive eval_expr: expr -> val -> Prop :=
  | eval_Econst_int: forall i ty,
      eval_expr (Econst_int i ty) (Vint i)
  | eval_Econst_float: forall f ty,
      eval_expr (Econst_float f ty) (Vfloat f)
  | eval_Etempvar: forall id ty v,
      le!id = Some v ->
      eval_expr (Etempvar id ty) v
  | eval_Eaddrof: forall a ty loc ofs,
      eval_lvalue a loc ofs ->
      eval_expr (Eaddrof a ty) (Vptr loc ofs)
  | eval_Eunop: forall op a ty v1 v,
      eval_expr a v1 ->
      sem_unary_operation op v1 (typeof a) = Some v ->
      eval_expr (Eunop op a ty) v
  | eval_Ebinop: forall op a1 a2 ty v1 v2 v,
      eval_expr a1 v1 ->
      eval_expr a2 v2 ->
      sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some v ->
      eval_expr (Ebinop op a1 a2 ty) v
  | eval_Econdition: forall a1 a2 a3 ty v1 b v' v,
      eval_expr a1 v1 ->
      bool_val v1 (typeof a1) = Some b ->
      eval_expr (if b then a2 else a3) v' ->
      sem_cast v' (typeof (if b then a2 else a3)) ty = Some v ->
      eval_expr (Econdition a1 a2 a3 ty) v
  | eval_Ecast: forall a ty v1 v,
      eval_expr a v1 ->
      sem_cast v1 (typeof a) ty = Some v ->
      eval_expr (Ecast a ty) v
  | eval_Elvalue: forall a loc ofs v,
      eval_lvalue a loc ofs -> type_is_volatile (typeof a) = false ->
      deref_loc ge (typeof a) m loc ofs E0 v ->
      eval_expr a v


with eval_lvalue: expr -> block -> int -> Prop :=
  | eval_Evar_local: forall id l ty,
      e!id = Some(l, ty) ->
      eval_lvalue (Evar id ty) l Int.zero
  | eval_Evar_global: forall id l ty,
      e!id = None ->
      Genv.find_symbol ge id = Some l ->
      type_of_global l = Some ty ->
      eval_lvalue (Evar id ty) l Int.zero
  | eval_Ederef: forall a ty l ofs,
      eval_expr a (Vptr l ofs) ->
      eval_lvalue (Ederef a ty) l ofs
 | eval_Efield_struct: forall a i ty l ofs id fList att delta,
      eval_expr a (Vptr l ofs) ->
      typeof a = Tstruct id fList att ->
      field_offset i fList = OK delta ->
      eval_lvalue (Efield a i ty) l (Int.add ofs (Int.repr delta))
 | eval_Efield_union: forall a i ty l ofs id fList att,
      eval_expr a (Vptr l ofs) ->
      typeof a = Tunion id fList att ->
      eval_lvalue (Efield a i ty) l ofs.

Scheme eval_expr_ind2 := Minimality for eval_expr Sort Prop
  with eval_lvalue_ind2 := Minimality for eval_lvalue Sort Prop.
Combined Scheme eval_expr_lvalue_ind from eval_expr_ind2, eval_lvalue_ind2.


Inductive eval_exprlist: list expr -> typelist -> list val -> Prop :=
  | eval_Enil:
      eval_exprlist nil Tnil nil
  | eval_Econs: forall a bl ty tyl v1 v2 vl,
      eval_expr a v1 ->
      sem_cast v1 (typeof a) ty = Some v2 ->
      eval_exprlist bl tyl vl ->
      eval_exprlist (a :: bl) (Tcons ty tyl) (v2 :: vl).

End EXPR.

Transition semantics for statements and functions

Inductive cont: Type :=
  | Kstop: cont
  | Kseq: statement -> cont -> cont (* Kseq s2 k = after s1 in s1;s2 *)
  | Kwhile: expr -> statement -> cont -> cont (* Kwhile e s k = after s in while (e) s *)
  | Kdowhile: expr -> statement -> cont -> cont (* Kdowhile e s k = after s in do s while (e) *)
  | Kfor2: expr -> statement -> statement -> cont -> cont (* Kfor2 e2 e3 s k = after s in for'(e2;e3) s *)
  | Kfor3: expr -> statement -> statement -> cont -> cont (* Kfor3 e2 e3 s k = after e3 in for'(e2;e3) s *)
  | Kswitch: cont -> cont (* catches break statements arising out of switch *)
  | Kcall: option ident -> (* where to store result *)
           function -> (* calling function *)
           env -> (* local env of calling function *)
           temp_env -> (* temporary env of calling function *)
           cont -> cont.


Fixpoint call_cont (k: cont) : cont :=
  match k with
  | Kseq s k => call_cont k
  | Kwhile e s k => call_cont k
  | Kdowhile e s k => call_cont k
  | Kfor2 e2 e3 s k => call_cont k
  | Kfor3 e2 e3 s k => call_cont k
  | Kswitch k => call_cont k
  | _ => k
  end.

Definition is_call_cont (k: cont) : Prop :=
  match k with
  | Kstop => True
  | Kcall _ _ _ _ _ => True
  | _ => False
  end.


Inductive state: Type :=
  | State
      (f: function)
      (s: statement)
      (k: cont)
      (e: env)
      (le: temp_env)
      (m: mem) : state
  | Callstate
      (fd: fundef)
      (args: list val)
      (k: cont)
      (m: mem) : state
  | Returnstate
      (res: val)
      (k: cont)
      (m: mem) : state.
                 

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 a s1 k)
  | Sfor' a2 a3 s1 =>
      match find_label lbl s1 (Kfor2 a2 a3 s1 k) with
      | Some sk => Some sk
      | None => find_label lbl a3 (Kfor3 a2 a3 s1 k)
      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.


Inductive step: state -> trace -> state -> Prop :=

  | step_assign: forall f a1 a2 k e le m loc ofs v2 v t m',
      eval_lvalue e le m a1 loc ofs ->
      eval_expr e le m a2 v2 ->
      sem_cast v2 (typeof a2) (typeof a1) = Some v ->
      assign_loc ge (typeof a1) m loc ofs v t m' ->
      step (State f (Sassign a1 a2) k e le m)
         t (State f Sskip k e le m')

  | step_set: forall f id a k e le m v,
      eval_expr e le m a v ->
      step (State f (Sset id a) k e le m)
        E0 (State f Sskip k e (PTree.set id v le) m)

  | step_vol_read: forall f id a k e le m loc ofs t v,
      eval_lvalue e le m a loc ofs ->
      deref_loc ge (typeof a) m loc ofs t v ->
      type_is_volatile (typeof a) = true ->
      step (State f (Svolread id a) k e le m)
         t (State f Sskip k e (PTree.set id v le) m)

  | step_call: forall f optid a al k e le m tyargs tyres vf vargs fd,
      classify_fun (typeof a) = fun_case_f tyargs tyres ->
      eval_expr e le m a vf ->
      eval_exprlist e le m al tyargs vargs ->
      Genv.find_funct ge vf = Some fd ->
      type_of_fundef fd = Tfunction tyargs tyres ->
      step (State f (Scall optid a al) k e le m)
        E0 (Callstate fd vargs (Kcall optid f e le k) m)

  | step_seq: forall f s1 s2 k e le m,
      step (State f (Ssequence s1 s2) k e le m)
        E0 (State f s1 (Kseq s2 k) e le m)
  | step_skip_seq: forall f s k e le m,
      step (State f Sskip (Kseq s k) e le m)
        E0 (State f s k e le m)
  | step_continue_seq: forall f s k e le m,
      step (State f Scontinue (Kseq s k) e le m)
        E0 (State f Scontinue k e le m)
  | step_break_seq: forall f s k e le m,
      step (State f Sbreak (Kseq s k) e le m)
        E0 (State f Sbreak k e le m)

  | step_ifthenelse: forall f a s1 s2 k e le m v1 b,
      eval_expr e le m a v1 ->
      bool_val v1 (typeof a) = Some b ->
      step (State f (Sifthenelse a s1 s2) k e le m)
        E0 (State f (if b then s1 else s2) k e le m)

  | step_while_false: forall f a s k e le m v,
      eval_expr e le m a v ->
      bool_val v (typeof a) = Some false ->
      step (State f (Swhile a s) k e le m)
        E0 (State f Sskip k e le m)
  | step_while_true: forall f a s k e le m v,
      eval_expr e le m a v ->
      bool_val v (typeof a) = Some true ->
      step (State f (Swhile a s) k e le m)
        E0 (State f s (Kwhile a s k) e le m)
  | step_skip_or_continue_while: forall f x a s k e le m,
      x = Sskip \/ x = Scontinue ->
      step (State f x (Kwhile a s k) e le m)
        E0 (State f (Swhile a s) k e le m)
  | step_break_while: forall f a s k e le m,
      step (State f Sbreak (Kwhile a s k) e le m)
        E0 (State f Sskip k e le m)

  | step_dowhile: forall f a s k e le m,
      step (State f (Sdowhile a s) k e le m)
        E0 (State f s (Kdowhile a s k) e le m)
  | step_skip_or_continue_dowhile_false: forall f x a s k e le m v,
      x = Sskip \/ x = Scontinue ->
      eval_expr e le m a v ->
      bool_val v (typeof a) = Some false ->
      step (State f x (Kdowhile a s k) e le m)
        E0 (State f Sskip k e le m)
  | step_skip_or_continue_dowhile_true: forall f x a s k e le m v,
      x = Sskip \/ x = Scontinue ->
      eval_expr e le m a v ->
      bool_val v (typeof a) = Some true ->
      step (State f x (Kdowhile a s k) e le m)
        E0 (State f (Sdowhile a s) k e le m)
  | step_break_dowhile: forall f a s k e le m,
      step (State f Sbreak (Kdowhile a s k) e le m)
        E0 (State f Sskip k e le m)

  | step_for_false: forall f a2 a3 s k e le m v,
      eval_expr e le m a2 v ->
      bool_val v (typeof a2) = Some false ->
      step (State f (Sfor' a2 a3 s) k e le m)
        E0 (State f Sskip k e le m)
  | step_for_true: forall f a2 a3 s k e le m v,
      eval_expr e le m a2 v ->
      bool_val v (typeof a2) = Some true ->
      step (State f (Sfor' a2 a3 s) k e le m)
        E0 (State f s (Kfor2 a2 a3 s k) e le m)
  | step_skip_or_continue_for2: forall f x a2 a3 s k e le m,
      x = Sskip \/ x = Scontinue ->
      step (State f x (Kfor2 a2 a3 s k) e le m)
        E0 (State f a3 (Kfor3 a2 a3 s k) e le m)
  | step_break_for2: forall f a2 a3 s k e le m,
      step (State f Sbreak (Kfor2 a2 a3 s k) e le m)
        E0 (State f Sskip k e le m)
  | step_skip_for3: forall f a2 a3 s k e le m,
      step (State f Sskip (Kfor3 a2 a3 s k) e le m)
        E0 (State f (Sfor' a2 a3 s) k e le m)
  | step_break_for3: forall f a2 a3 s k e le m,
      step (State f Sbreak (Kfor3 a2 a3 s k) e le m)
        E0 (State f Sskip k e le m)

  | step_return_0: forall f k e le m m',
      Mem.free_list m (blocks_of_env e) = Some m' ->
      step (State f (Sreturn None) k e le m)
        E0 (Returnstate Vundef (call_cont k) m')
  | step_return_1: forall f a k e le m v v' m',
      eval_expr e le m a v ->
      sem_cast v (typeof a) f.(fn_return) = Some v' ->
      Mem.free_list m (blocks_of_env e) = Some m' ->
      step (State f (Sreturn (Some a)) k e le m)
        E0 (Returnstate v' (call_cont k) m')
  | step_skip_call: forall f k e le m m',
      is_call_cont k ->
      f.(fn_return) = Tvoid ->
      Mem.free_list m (blocks_of_env e) = Some m' ->
      step (State f Sskip k e le m)
        E0 (Returnstate Vundef k m')

  | step_switch: forall f a sl k e le m n,
      eval_expr e le m a (Vint n) ->
      step (State f (Sswitch a sl) k e le m)
        E0 (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e le m)
  | step_skip_break_switch: forall f x k e le m,
      x = Sskip \/ x = Sbreak ->
      step (State f x (Kswitch k) e le m)
        E0 (State f Sskip k e le m)
  | step_continue_switch: forall f k e le m,
      step (State f Scontinue (Kswitch k) e le m)
        E0 (State f Scontinue k e le m)

  | step_label: forall f lbl s k e le m,
      step (State f (Slabel lbl s) k e le m)
        E0 (State f s k e le m)

  | step_goto: forall f lbl k e le m s' k',
      find_label lbl f.(fn_body) (call_cont k) = Some (s', k') ->
      step (State f (Sgoto lbl) k e le m)
        E0 (State f s' k' e le m)

  | step_internal_function: forall f vargs k m e m1 m2,
      list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
      alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
      bind_parameters ge e m1 f.(fn_params) vargs m2 ->
      step (Callstate (Internal f) vargs k m)
        E0 (State f f.(fn_body) k e (PTree.empty val) m2)

  | step_external_function: forall ef targs tres vargs k m vres t m',
      external_call ef ge vargs m t vres m' ->
      step (Callstate (External ef targs tres) vargs k m)
         t (Returnstate vres k m')

  | step_returnstate_none: forall v f e le k m,
      step (Returnstate v (Kcall None f e le k) m)
        E0 (State f Sskip k e le m)
  | step_returnstate_some: forall v id f e le k m,
      step (Returnstate v (Kcall (Some id) f e le k) m)
        E0 (State f Sskip k e (PTree.set id v le) m).

Alternate big-step semantics

Big-step semantics for terminating statements and functions

Inductive outcome: Type :=
   | Out_break: outcome (* terminated by break *)
   | Out_continue: outcome (* terminated by continue *)
   | Out_normal: outcome (* terminated normally *)
   | Out_return: option (val * type) -> outcome. (* terminated by return *)

Inductive out_normal_or_continue : outcome -> Prop :=
  | Out_normal_or_continue_N: out_normal_or_continue Out_normal
  | Out_normal_or_continue_C: out_normal_or_continue Out_continue.

Inductive out_break_or_return : outcome -> outcome -> Prop :=
  | Out_break_or_return_B: out_break_or_return Out_break Out_normal
  | Out_break_or_return_R: forall ov,
      out_break_or_return (Out_return ov) (Out_return ov).

Definition outcome_switch (out: outcome) : outcome :=
  match out with
  | Out_break => Out_normal
  | o => o
  end.

Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop :=
  match out, t with
  | Out_normal, Tvoid => v = Vundef
  | Out_return None, Tvoid => v = Vundef
  | Out_return (Some (v',t')), ty => ty <> Tvoid /\ sem_cast v' t' t = Some v
  | _, _ => False
  end.


Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> mem -> outcome -> Prop :=
  | exec_Sskip: forall e le m,
      exec_stmt e le m Sskip
               E0 le m Out_normal
  | exec_Sassign: forall e le m a1 a2 loc ofs v2 v t m',
      eval_lvalue e le m a1 loc ofs ->
      eval_expr e le m a2 v2 ->
      sem_cast v2 (typeof a2) (typeof a1) = Some v ->
      assign_loc ge (typeof a1) m loc ofs v t m' ->
      exec_stmt e le m (Sassign a1 a2)
               t le m' Out_normal
  | exec_Sset: forall e le m id a v,
      eval_expr e le m a v ->
      exec_stmt e le m (Sset id a)
               E0 (PTree.set id v le) m Out_normal
  | exec_Svol_read: forall e le m id a loc ofs t v,
      eval_lvalue e le m a loc ofs ->
      type_is_volatile (typeof a) = true ->
      deref_loc ge (typeof a) m loc ofs t v ->
      exec_stmt e le m (Svolread id a)
               t (PTree.set id v le) m Out_normal
  | exec_Scall_none: forall e le m a al tyargs tyres vf vargs f t m' vres,
      classify_fun (typeof a) = fun_case_f tyargs tyres ->
      eval_expr e le m a vf ->
      eval_exprlist e le m al tyargs vargs ->
      Genv.find_funct ge vf = Some f ->
      type_of_fundef f = Tfunction tyargs tyres ->
      eval_funcall m f vargs t m' vres ->
      exec_stmt e le m (Scall None a al)
                t le m' Out_normal
  | exec_Scall_some: forall e le m id a al tyargs tyres vf vargs f t m' vres,
      classify_fun (typeof a) = fun_case_f tyargs tyres ->
      eval_expr e le m a vf ->
      eval_exprlist e le m al tyargs vargs ->
      Genv.find_funct ge vf = Some f ->
      type_of_fundef f = Tfunction tyargs tyres ->
      eval_funcall m f vargs t m' vres ->
      exec_stmt e le m (Scall (Some id) a al)
                t (PTree.set id vres le) m' Out_normal
  | exec_Sseq_1: forall e le m s1 s2 t1 le1 m1 t2 le2 m2 out,
      exec_stmt e le m s1 t1 le1 m1 Out_normal ->
      exec_stmt e le1 m1 s2 t2 le2 m2 out ->
      exec_stmt e le m (Ssequence s1 s2)
                (t1 ** t2) le2 m2 out
  | exec_Sseq_2: forall e le m s1 s2 t1 le1 m1 out,
      exec_stmt e le m s1 t1 le1 m1 out ->
      out <> Out_normal ->
      exec_stmt e le m (Ssequence s1 s2)
                t1 le1 m1 out
  | exec_Sifthenelse: forall e le m a s1 s2 v1 b t le' m' out,
      eval_expr e le m a v1 ->
      bool_val v1 (typeof a) = Some b ->
      exec_stmt e le m (if b then s1 else s2) t le' m' out ->
      exec_stmt e le m (Sifthenelse a s1 s2)
                t le' m' out
  | exec_Sreturn_none: forall e le m,
      exec_stmt e le m (Sreturn None)
               E0 le m (Out_return None)
  | exec_Sreturn_some: forall e le m a v,
      eval_expr e le m a v ->
      exec_stmt e le m (Sreturn (Some a))
                E0 le m (Out_return (Some (v, typeof a)))
  | exec_Sbreak: forall e le m,
      exec_stmt e le m Sbreak
               E0 le m Out_break
  | exec_Scontinue: forall e le m,
      exec_stmt e le m Scontinue
               E0 le m Out_continue
  | exec_Swhile_false: forall e le m a s v,
      eval_expr e le m a v ->
      bool_val v (typeof a) = Some false ->
      exec_stmt e le m (Swhile a s)
               E0 le m Out_normal
  | exec_Swhile_stop: forall e le m a v s t le' m' out' out,
      eval_expr e le m a v ->
      bool_val v (typeof a) = Some true ->
      exec_stmt e le m s t le' m' out' ->
      out_break_or_return out' out ->
      exec_stmt e le m (Swhile a s)
                t le' m' out
  | exec_Swhile_loop: forall e le m a s v t1 le1 m1 out1 t2 le2 m2 out,
      eval_expr e le m a v ->
      bool_val v (typeof a) = Some true ->
      exec_stmt e le m s t1 le1 m1 out1 ->
      out_normal_or_continue out1 ->
      exec_stmt e le1 m1 (Swhile a s) t2 le2 m2 out ->
      exec_stmt e le m (Swhile a s)
                (t1 ** t2) le2 m2 out
  | exec_Sdowhile_false: forall e le m s a t le1 m1 out1 v,
      exec_stmt e le m s t le1 m1 out1 ->
      out_normal_or_continue out1 ->
      eval_expr e le1 m1 a v ->
      bool_val v (typeof a) = Some false ->
      exec_stmt e le m (Sdowhile a s)
                t le1 m1 Out_normal
  | exec_Sdowhile_stop: forall e le m s a t le1 m1 out1 out,
      exec_stmt e le m s t le1 m1 out1 ->
      out_break_or_return out1 out ->
      exec_stmt e le m (Sdowhile a s)
                t le1 m1 out
  | exec_Sdowhile_loop: forall e le m s a le1 m1 le2 m2 t1 t2 out out1 v,
      exec_stmt e le m s t1 le1 m1 out1 ->
      out_normal_or_continue out1 ->
      eval_expr e le1 m1 a v ->
      bool_val v (typeof a) = Some true ->
      exec_stmt e le1 m1 (Sdowhile a s) t2 le2 m2 out ->
      exec_stmt e le m (Sdowhile a s)
                (t1 ** t2) le2 m2 out

  | exec_Sfor_false: forall e le m s a2 a3 v,
      eval_expr e le m a2 v ->
      bool_val v (typeof a2) = Some false ->
      exec_stmt e le m (Sfor' a2 a3 s)
               E0 le m Out_normal
  | exec_Sfor_stop: forall e le m s a2 a3 v le1 m1 t out1 out,
      eval_expr e le m a2 v ->
      bool_val v (typeof a2) = Some true ->
      exec_stmt e le m s t le1 m1 out1 ->
      out_break_or_return out1 out ->
      exec_stmt e le m (Sfor' a2 a3 s)
                t le1 m1 out
  | exec_Sfor_loop: forall e le m s a2 a3 v le1 m1 le2 m2 le3 m3 t1 t2 t3 out1 out,
      eval_expr e le m a2 v ->
      bool_val v (typeof a2) = Some true ->
      exec_stmt e le m s t1 le1 m1 out1 ->
      out_normal_or_continue out1 ->
      exec_stmt e le1 m1 a3 t2 le2 m2 Out_normal ->
      exec_stmt e le2 m2 (Sfor' a2 a3 s) t3 le3 m3 out ->
      exec_stmt e le m (Sfor' a2 a3 s)
                (t1 ** t2 ** t3) le3 m3 out
  | exec_Sswitch: forall e le m a t n sl le1 m1 out,
      eval_expr e le m a (Vint n) ->
      exec_stmt e le m (seq_of_labeled_statement (select_switch n sl)) t le1 m1 out ->
      exec_stmt e le m (Sswitch a sl)
                t le1 m1 (outcome_switch out)


with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
  | eval_funcall_internal: forall le m f vargs t e m1 m2 m3 out vres m4,
      alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
      list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
      bind_parameters ge e m1 f.(fn_params) vargs m2 ->
      exec_stmt e (PTree.empty val) m2 f.(fn_body) t le m3 out ->
      outcome_result_value out f.(fn_return) vres ->
      Mem.free_list m3 (blocks_of_env e) = Some m4 ->
      eval_funcall m (Internal f) vargs t m4 vres
  | eval_funcall_external: forall m ef targs tres vargs t vres m',
      external_call ef ge vargs m t vres m' ->
      eval_funcall m (External ef targs tres) vargs t m' vres.

Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop
  with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop.

Big-step semantics for diverging statements and functions

CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Prop :=
  | execinf_Scall_none: forall e le m a al vf tyargs tyres vargs f t,
      classify_fun (typeof a) = fun_case_f tyargs tyres ->
      eval_expr e le m a vf ->
      eval_exprlist e le m al tyargs vargs ->
      Genv.find_funct ge vf = Some f ->
      type_of_fundef f = Tfunction tyargs tyres ->
      evalinf_funcall m f vargs t ->
      execinf_stmt e le m (Scall None a al) t
  | execinf_Scall_some: forall e le m id a al vf tyargs tyres vargs f t,
      classify_fun (typeof a) = fun_case_f tyargs tyres ->
      eval_expr e le m a vf ->
      eval_exprlist e le m al tyargs vargs ->
      Genv.find_funct ge vf = Some f ->
      type_of_fundef f = Tfunction tyargs tyres ->
      evalinf_funcall m f vargs t ->
      execinf_stmt e le m (Scall (Some id) a al) t
  | execinf_Sseq_1: forall e le m s1 s2 t,
      execinf_stmt e le m s1 t ->
      execinf_stmt e le m (Ssequence s1 s2) t
  | execinf_Sseq_2: forall e le m s1 s2 t1 le1 m1 t2,
      exec_stmt e le m s1 t1 le1 m1 Out_normal ->
      execinf_stmt e le1 m1 s2 t2 ->
      execinf_stmt e le m (Ssequence s1 s2) (t1 *** t2)
  | execinf_Sifthenelse: forall e le m a s1 s2 v1 b t,
      eval_expr e le m a v1 ->
      bool_val v1 (typeof a) = Some b ->
      execinf_stmt e le m (if b then s1 else s2) t ->
      execinf_stmt e le m (Sifthenelse a s1 s2) t
  | execinf_Swhile_body: forall e le m a v s t,
      eval_expr e le m a v ->
      bool_val v (typeof a) = Some true ->
      execinf_stmt e le m s t ->
      execinf_stmt e le m (Swhile a s) t
  | execinf_Swhile_loop: forall e le m a s v t1 le1 m1 out1 t2,
      eval_expr e le m a v ->
      bool_val v (typeof a) = Some true ->
      exec_stmt e le m s t1 le1 m1 out1 ->
      out_normal_or_continue out1 ->
      execinf_stmt e le1 m1 (Swhile a s) t2 ->
      execinf_stmt e le m (Swhile a s) (t1 *** t2)
  | execinf_Sdowhile_body: forall e le m s a t,
      execinf_stmt e le m s t ->
      execinf_stmt e le m (Sdowhile a s) t
  | execinf_Sdowhile_loop: forall e le m s a le1 m1 t1 t2 out1 v,
      exec_stmt e le m s t1 le1 m1 out1 ->
      out_normal_or_continue out1 ->
      eval_expr e le1 m1 a v ->
      bool_val v (typeof a) = Some true ->
      execinf_stmt e le1 m1 (Sdowhile a s) t2 ->
      execinf_stmt e le m (Sdowhile a s) (t1 *** t2)
  | execinf_Sfor_body: forall e le m s a2 a3 v t,
      eval_expr e le m a2 v ->
      bool_val v (typeof a2) = Some true ->
      execinf_stmt e le m s t ->
      execinf_stmt e le m (Sfor' a2 a3 s) t
  | execinf_Sfor_next: forall e le m s a2 a3 v le1 m1 t1 t2 out1,
      eval_expr e le m a2 v ->
      bool_val v (typeof a2) = Some true ->
      exec_stmt e le m s t1 le1 m1 out1 ->
      out_normal_or_continue out1 ->
      execinf_stmt e le1 m1 a3 t2 ->
      execinf_stmt e le m (Sfor' a2 a3 s) (t1 *** t2)
  | execinf_Sfor_loop: forall e le m s a2 a3 v le1 m1 le2 m2 t1 t2 t3 out1,
      eval_expr e le m a2 v ->
      bool_val v (typeof a2) = Some true ->
      exec_stmt e le m s t1 le1 m1 out1 ->
      out_normal_or_continue out1 ->
      exec_stmt e le1 m1 a3 t2 le2 m2 Out_normal ->
      execinf_stmt e le2 m2 (Sfor' a2 a3 s) t3 ->
      execinf_stmt e le m (Sfor' a2 a3 s) (t1 *** t2 *** t3)
  | execinf_Sswitch: forall e le m a t n sl,
      eval_expr e le m a (Vint n) ->
      execinf_stmt e le m (seq_of_labeled_statement (select_switch n sl)) t ->
      execinf_stmt e le m (Sswitch a sl) t


with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop :=
  | evalinf_funcall_internal: forall m f vargs t e m1 m2,
      alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
      list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
      bind_parameters ge e m1 f.(fn_params) vargs m2 ->
      execinf_stmt e (PTree.empty val) m2 f.(fn_body) t ->
      evalinf_funcall m (Internal f) vargs t.

End SEMANTICS.

Whole-program semantics

Inductive initial_state (p: program): state -> Prop :=
  | initial_state_intro: forall b f m0,
      let ge := Genv.globalenv p in
      Genv.init_mem p = Some m0 ->
      Genv.find_symbol ge p.(prog_main) = Some b ->
      Genv.find_funct_ptr ge b = Some f ->
      type_of_fundef f = Tfunction Tnil type_int32s ->
      initial_state p (Callstate f nil Kstop m0).


Inductive final_state: state -> int -> Prop :=
  | final_state_intro: forall r m,
      final_state (Returnstate (Vint r) Kstop m) r.


Definition semantics (p: program) :=
  Semantics step (initial_state p) final_state (Genv.globalenv p).


Lemma semantics_receptive:
  forall (p: program), receptive (semantics p).


Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
  | bigstep_program_terminates_intro: forall b f m0 m1 t r,
      let ge := Genv.globalenv p in
      Genv.init_mem p = Some m0 ->
      Genv.find_symbol ge p.(prog_main) = Some b ->
      Genv.find_funct_ptr ge b = Some f ->
      type_of_fundef f = Tfunction Tnil type_int32s ->
      eval_funcall ge m0 f nil t m1 (Vint r) ->
      bigstep_program_terminates p t r.

Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
  | bigstep_program_diverges_intro: forall b f m0 t,
      let ge := Genv.globalenv p in
      Genv.init_mem p = Some m0 ->
      Genv.find_symbol ge p.(prog_main) = Some b ->
      Genv.find_funct_ptr ge b = Some f ->
      type_of_fundef f = Tfunction Tnil type_int32s ->
      evalinf_funcall ge m0 f nil t ->
      bigstep_program_diverges p t.

Definition bigstep_semantics (p: program) :=
  Bigstep_semantics (bigstep_program_terminates p) (bigstep_program_diverges p).

Implication from big-step semantics to transition semantics

Section BIGSTEP_TO_TRANSITIONS.

Variable prog: program.
Let ge : genv := Genv.globalenv prog.

Definition exec_stmt_eval_funcall_ind
  (PS: env -> temp_env -> mem -> statement -> trace -> temp_env -> mem -> outcome -> Prop)
  (PF: mem -> fundef -> list val -> trace -> mem -> val -> Prop) :=
  fun a b c d e f g h i j k l m n o p q r s t u v w x y =>
  conj (exec_stmt_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y)
       (eval_funcall_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y).

Inductive outcome_state_match
       (e: env) (le: temp_env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop :=
  | osm_normal:
      outcome_state_match e le m f k Out_normal (State f Sskip k e le m)
  | osm_break:
      outcome_state_match e le m f k Out_break (State f Sbreak k e le m)
  | osm_continue:
      outcome_state_match e le m f k Out_continue (State f Scontinue k e le m)
  | osm_return_none: forall k',
      call_cont k' = call_cont k ->
      outcome_state_match e le m f k
        (Out_return None) (State f (Sreturn None) k' e le m)
  | osm_return_some: forall a v k',
      call_cont k' = call_cont k ->
      eval_expr ge e le m a v ->
      outcome_state_match e le m f k
        (Out_return (Some (v,typeof a))) (State f (Sreturn (Some a)) k' e le m).

Lemma is_call_cont_call_cont:
  forall k, is_call_cont k -> call_cont k = k.

Lemma exec_stmt_eval_funcall_steps:
  (forall e le m s t le' m' out,
   exec_stmt ge e le m s t le' m' out ->
   forall f k, exists S,
   star step ge (State f s k e le m) t S
   /\ outcome_state_match e le' m' f k out S)
/\
  (forall m fd args t m' res,
   eval_funcall ge m fd args t m' res ->
   forall k,
   is_call_cont k ->
   star step ge (Callstate fd args k m) t (Returnstate res k m')).

Lemma exec_stmt_steps:
   forall e le m s t le' m' out,
   exec_stmt ge e le m s t le' m' out ->
   forall f k, exists S,
   star step ge (State f s k e le m) t S
   /\ outcome_state_match e le' m' f k out S.
Proof (proj1 exec_stmt_eval_funcall_steps).

Lemma eval_funcall_steps:
   forall m fd args t m' res,
   eval_funcall ge m fd args t m' res ->
   forall k,
   is_call_cont k ->
   star step ge (Callstate fd args k m) t (Returnstate res k m').
Proof (proj2 exec_stmt_eval_funcall_steps).

Definition order (x y: unit) := False.

Lemma evalinf_funcall_forever:
  forall m fd args T k,
  evalinf_funcall ge m fd args T ->
  forever_N step order ge tt (Callstate fd args k m) T.

Theorem bigstep_semantics_sound:
  bigstep_sound (bigstep_semantics prog) (semantics prog).

End BIGSTEP_TO_TRANSITIONS.