Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Events.
Require Import Values.
Require Import Memory MemReserve.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Switch.
Require Import Values_symbolictype.
Require Import Values_symbolic.
Require Import Normalise.

Abstract syntax

Inductive constant : Type :=
  | Ointconst: int -> constant (* integer constant *)
  | Ofloatconst: float -> constant (* double-precision floating-point constant *)
  | Osingleconst: float32 -> constant (* single-precision floating-point constant *)
  | Olongconst: int64 -> constant (* long integer constant *)
  | Oaddrsymbol: ident -> int -> constant (* address of the symbol plus the offset *)
  | Oaddrstack: int -> constant. (* stack pointer plus the given offset *)

Inductive unary_operation : Type :=
  | Ocast8unsigned: unary_operation (* 8-bit zero extension *)
  | Ocast8signed: unary_operation (* 8-bit sign extension *)
  | Ocast16unsigned: unary_operation (* 16-bit zero extension *)
  | Ocast16signed: unary_operation (* 16-bit sign extension *)
  | Onegint: unary_operation (* integer opposite *)
  | Onotint: unary_operation (* bitwise complement *)
  | Onegf: unary_operation (* float64 opposite *)
  | Oabsf: unary_operation (* float64 absolute value *)
  | Onegfs: unary_operation (* float32 opposite *)
  | Oabsfs: unary_operation (* float32 absolute value *)
  | Osingleoffloat: unary_operation (* float truncation to float32 *)
  | Ofloatofsingle: unary_operation (* float extension to float64 *)
  | Ointoffloat: unary_operation (* signed integer to float64 *)
  | Ointuoffloat: unary_operation (* unsigned integer to float64 *)
  | Ofloatofint: unary_operation (* float64 to signed integer *)
  | Ofloatofintu: unary_operation (* float64 to unsigned integer *)
  | Ointofsingle: unary_operation (* signed integer to float32 *)
  | Ointuofsingle: unary_operation (* unsigned integer to float32 *)
  | Osingleofint: unary_operation (* float32 to signed integer *)
  | Osingleofintu: unary_operation (* float32 to unsigned integer *)
  | Onegl: unary_operation (* long integer opposite *)
  | Onotl: unary_operation (* long bitwise complement *)
  | Ointoflong: unary_operation (* long to int *)
  | Olongofint: unary_operation (* signed int to long *)
  | Olongofintu: unary_operation (* unsigned int to long *)
  | Olongoffloat: unary_operation (* float64 to signed long *)
  | Olonguoffloat: unary_operation (* float64 to unsigned long *)
  | Ofloatoflong: unary_operation (* signed long to float64 *)
  | Ofloatoflongu: unary_operation (* unsigned long to float64 *)
  | Olongofsingle: unary_operation (* float32 to signed long *)
  | Olonguofsingle: unary_operation (* float32 to unsigned long *)
  | Osingleoflong: unary_operation (* signed long to float32 *)
  | Osingleoflongu: unary_operation (* unsigned long to float32 *)
.
                      
Inductive binary_operation : Type :=
  | Oadd: binary_operation (* integer addition *)
  | Osub: binary_operation (* integer subtraction *)
  | Omul: binary_operation (* integer multiplication *)
  | Odiv: binary_operation (* integer signed division *)
  | Odivu: binary_operation (* integer unsigned division *)
  | Omod: binary_operation (* integer signed modulus *)
  | Omodu: binary_operation (* integer unsigned modulus *)
  | Oand: binary_operation (* integer bitwise ``and'' *)
  | Oor: binary_operation (* integer bitwise ``or'' *)
  | Oxor: binary_operation (* integer bitwise ``xor'' *)
  | Oshl: binary_operation (* integer left shift *)
  | Oshr: binary_operation (* integer right signed shift *)
  | Oshru: binary_operation (* integer right unsigned shift *)
  | Oaddf: binary_operation (* float64 addition *)
  | Osubf: binary_operation (* float64 subtraction *)
  | Omulf: binary_operation (* float64 multiplication *)
  | Odivf: binary_operation (* float64 division *)
  | Oaddfs: binary_operation (* float32 addition *)
  | Osubfs: binary_operation (* float32 subtraction *)
  | Omulfs: binary_operation (* float32 multiplication *)
  | Odivfs: binary_operation (* float32 division *)
  | Oaddl: binary_operation (* long addition *)
  | Osubl: binary_operation (* long subtraction *)
  | Omull: binary_operation (* long multiplication *)
  | Odivl: binary_operation (* long signed division *)
  | Odivlu: binary_operation (* long unsigned division *)
  | Omodl: binary_operation (* long signed modulus *)
  | Omodlu: binary_operation (* long unsigned modulus *)
  | Oandl: binary_operation (* long bitwise ``and'' *)
  | Oorl: binary_operation (* long bitwise ``or'' *)
  | Oxorl: binary_operation (* long bitwise ``xor'' *)
  | Oshll: binary_operation (* long left shift *)
  | Oshrl: binary_operation (* long right signed shift *)
  | Oshrlu: binary_operation (* long right unsigned shift *)
  | Ocmp: comparison -> binary_operation (* integer signed comparison *)
  | Ocmpu: comparison -> binary_operation (* integer unsigned comparison *)
  | Ocmpf: comparison -> binary_operation (* float64 comparison *)
  | Ocmpfs: comparison -> binary_operation (* float32 comparison *)
  | Ocmpl: comparison -> binary_operation (* long signed comparison *)
  | Ocmplu: comparison -> binary_operation (* long unsigned comparison *)

.

Inductive expr : Type :=
  | Evar : ident -> expr
  | Econst : constant -> expr
  | Eunop : unary_operation -> expr -> expr
  | Ebinop : binary_operation -> expr -> expr -> expr
  | Eload : memory_chunk -> expr -> expr.


Definition label := ident.

Inductive stmt : Type :=
  | Sskip: stmt
  | Sassign : ident -> expr -> stmt
  | Sstore : memory_chunk -> expr -> expr -> stmt
  | Scall : option ident -> signature -> expr -> list expr -> stmt
  | Stailcall: signature -> expr -> list expr -> stmt
  | Sbuiltin : option ident -> external_function -> list expr -> stmt
  | Sseq: stmt -> stmt -> stmt
  | Sifthenelse: expr -> stmt -> stmt -> stmt
  | Sloop: stmt -> stmt
  | Sblock: stmt -> stmt
  | Sexit: nat -> stmt
  | Sswitch: bool -> expr -> list (Z * nat) -> nat -> stmt
  | Sreturn: option expr -> stmt
  | Slabel: label -> stmt -> stmt
  | Sgoto: label -> stmt.


Record function : Type := mkfunction {
  fn_id: ident;
  fn_sig: signature;
  fn_params: list ident;
  fn_vars: list ident;
  fn_stackspace: Z;
  fn_body: stmt;
  fn_stackspace_pos: 0 <= fn_stackspace
}.

Definition fundef := AST.fundef function.
Definition program := AST.program fundef unit.

Definition funsig (fd: fundef) :=
  match fd with
  | Internal f => fn_sig f
  | External ef => ef_sig ef
  end.

Operational semantics (small-step)

Definition genv := Genv.t fundef unit.
Definition env := PTree.t expr_sym.


Fixpoint set_params (vl: list expr_sym) (il: list ident) {struct il} : env :=
  match il, vl with
  | i1 :: is, v1 :: vs => PTree.set i1 v1 (set_params vs is)
  | i1 :: is, nil => PTree.set i1 (Eval Vundef) (set_params nil is)
  | _, _ => PTree.empty expr_sym
  end.

Fixpoint set_locals (il: list ident) (e: env) {struct il} : env :=
  match il with
  | nil => e
  | i1 :: is => PTree.set i1 (Eval Vundef) (set_locals is e)
  end.

Definition set_optvar (optid: option ident) (v: expr_sym) (e: env) : env :=
  match optid with
  | None => e
  | Some id => PTree.set id v e
  end.


Inductive cont: Type :=
  | Kstop: cont (* stop program execution *)
  | Kseq: stmt -> cont -> cont (* execute stmt, then cont *)
  | Kblock: cont -> cont (* exit a block, then do cont *)
  | Kcall: option ident -> function -> block -> env -> cont -> cont.


Inductive state: Type :=
  | State: (* Execution within a function *)
      forall (f: function) (* currently executing function *)
             (s: stmt) (* statement under consideration *)
             (k: cont) (* its continuation -- what to do next *)
             (sp: block) (* current stack pointer *)
             (e: env) (* current local environment *)
             (m: mem), (* current memory state *)
      state
  | Callstate: (* Invocation of a function *)
      forall (f: fundef) (* function to invoke *)
             (args: list expr_sym) (* arguments provided by caller *)
             (k: cont) (* what to do next *)
             (m: mem), (* memory state *)
      state
  | Returnstate: (* Return from a function *)
      forall (v: expr_sym) (* Return value *)
             (k: cont) (* what to do next *)
             (m: mem), (* memory state *)
      state.
             
Section RELSEM.

  Variable ge: genv.

  Variable needed_stackspace : ident -> nat.



Definition eval_constant (sp: block) (cst: constant) : option expr_sym :=
  match cst with
  | Ointconst n => Some (Eval (Vint n))
  | Ofloatconst n => Some (Eval (Vfloat n))
  | Osingleconst n => Some (Eval (Vsingle n))
  | Olongconst n => Some (Eval (Vlong n))
  | Oaddrsymbol s ofs =>
    match Genv.find_symbol ge s with
      | None => None
      | Some b => Some (Eval (Vptr b ofs))
    end
  | Oaddrstack ofs => Some (Eval (Vptr sp ofs))
  end.


Definition eval_unop (op: unary_operation) (arg: expr_sym) : option expr_sym :=
  match op with
  | Ocast8unsigned => Some (Val.zero_ext 8 arg)
  | Ocast8signed => Some (Val.sign_ext 8 arg)
  | Ocast16unsigned => Some (Val.zero_ext 16 arg)
  | Ocast16signed => Some (Val.sign_ext 16 arg)
  | Onegint => Some (Val.negint arg)
  | Onotint => Some (Val.notint arg)
  | Onegf => Some (Val.negf arg)
  | Oabsf => Some (Val.absf arg)
  | Onegfs => Some (Val.negfs arg)
  | Oabsfs => Some (Val.absfs arg)
  | Osingleoffloat => Some (Val.singleoffloat arg)
  | Ofloatofsingle => Some (Val.floatofsingle arg)
  | Ointoffloat => Some (Val.intoffloat arg)
  | Ointuoffloat => Some (Val.intuoffloat arg)
  | Ofloatofint => Some (Val.floatofint arg)
  | Ofloatofintu => Some (Val.floatofintu arg)
  | Ointofsingle => Some (Val.intofsingle arg)
  | Ointuofsingle => Some (Val.intuofsingle arg)
  | Osingleofint => Some (Val.singleofint arg)
  | Osingleofintu => Some (Val.singleofintu arg)
  | Onegl => Some (Val.negl arg)
  | Onotl => Some (Val.notl arg)
  | Ointoflong => Some (Val.loword arg)
  | Olongofint => Some (Val.longofint arg)
  | Olongofintu => Some (Val.longofintu arg)
  | Olongoffloat => Some (Val.longoffloat arg)
  | Olonguoffloat => Some (Val.longuoffloat arg)
  | Ofloatoflong => Some (Val.floatoflong arg)
  | Ofloatoflongu => Some (Val.floatoflongu arg)
  | Olongofsingle => Some (Val.longofsingle arg)
  | Olonguofsingle => Some (Val.longuofsingle arg)
  | Osingleoflong => Some (Val.singleoflong arg)
  | Osingleoflongu => Some (Val.singleoflongu arg)
  end.

Definition eval_binop
            (op: binary_operation) (arg1 arg2: expr_sym) (m: mem): option expr_sym :=
  match op with
  | Oadd => Some (Val.add arg1 arg2)
  | Osub => Some (Val.sub arg1 arg2)
  | Omul => Some (Val.mul arg1 arg2)
  | Odiv => Some (Val.divs arg1 arg2)
  | Odivu => Some (Val.divu arg1 arg2)
  | Omod => Some (Val.mods arg1 arg2)
  | Omodu => Some (Val.modu arg1 arg2)
  | Oand => Some (Val.and arg1 arg2)
  | Oor => Some (Val.or arg1 arg2)
  | Oxor => Some (Val.xor arg1 arg2)
  | Oshl => Some (Val.shl arg1 arg2)
  | Oshr => Some (Val.shr arg1 arg2)
  | Oshru => Some (Val.shru arg1 arg2)
  | Oaddf => Some (Val.addf arg1 arg2)
  | Osubf => Some (Val.subf arg1 arg2)
  | Omulf => Some (Val.mulf arg1 arg2)
  | Odivf => Some (Val.divf arg1 arg2)
  | Oaddfs => Some (Val.addfs arg1 arg2)
  | Osubfs => Some (Val.subfs arg1 arg2)
  | Omulfs => Some (Val.mulfs arg1 arg2)
  | Odivfs => Some (Val.divfs arg1 arg2)
  | Oaddl => Some (Val.addl arg1 arg2)
  | Osubl => Some (Val.subl arg1 arg2)
  | Omull => Some (Val.mull arg1 arg2)
  | Odivl => Some (Val.divls arg1 arg2)
  | Odivlu => Some (Val.divlu arg1 arg2)
  | Omodl => Some (Val.modls arg1 arg2)
  | Omodlu => Some (Val.modlu arg1 arg2)
  | Oandl => Some (Val.andl arg1 arg2)
  | Oorl => Some (Val.orl arg1 arg2)
  | Oxorl => Some (Val.xorl arg1 arg2)
  | Oshll => Some (Val.shll arg1 arg2)
  | Oshrl => Some (Val.shrl arg1 arg2)
  | Oshrlu => Some (Val.shrlu arg1 arg2)
  | Ocmp c => Some (Val.cmp c arg1 arg2)
  | Ocmpu c => Some (Val.cmpu c arg1 arg2)
  | Ocmpf c => Some (Val.cmpf c arg1 arg2)
  | Ocmpfs c => Some (Val.cmpfs c arg1 arg2)
  | Ocmpl c => Some (Val.cmpl c arg1 arg2)
  | Ocmplu c => Some (Val.cmplu c arg1 arg2)
  end.


Section EVAL_EXPR.

Variable sp: block.
Variable e: env.
Variable m: mem.

Inductive eval_expr: expr -> expr_sym -> Prop :=
  | eval_Evar: forall id v,
      PTree.get id e = Some v ->
      eval_expr (Evar id) v
  | eval_Econst: forall cst v,
      eval_constant sp cst = Some v ->
      eval_expr (Econst cst) v
  | eval_Eunop: forall op a1 v1 v,
      eval_expr a1 v1 ->
      eval_unop op v1 = Some v ->
      eval_expr (Eunop op a1) v
  | eval_Ebinop: forall op a1 a2 v1 v2 v,
      eval_expr a1 v1 ->
      eval_expr a2 v2 ->
      eval_binop op v1 v2 m = Some v ->
      eval_expr (Ebinop op a1 a2) v
  | eval_Eload: forall chunk addr vaddr v,
      eval_expr addr vaddr ->
      Mem.loadv chunk m vaddr = Some v ->
      eval_expr (Eload chunk addr) v.

Inductive eval_exprlist: list expr -> list expr_sym -> Prop :=
  | eval_Enil:
      eval_exprlist nil nil
  | eval_Econs: forall a1 al v1 vl,
      eval_expr a1 v1 -> eval_exprlist al vl ->
      eval_exprlist (a1 :: al) (v1 :: vl).

End EVAL_EXPR.


Fixpoint call_cont (k: cont) : cont :=
  match k with
  | Kseq s k => call_cont k
  | Kblock k => call_cont k
  | _ => k
  end.

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


Fixpoint find_label (lbl: label) (s: stmt) (k: cont)
                    {struct s}: option (stmt * cont) :=
  match s with
  | Sseq 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
  | Sloop s1 =>
      find_label lbl s1 (Kseq (Sloop s1) k)
  | Sblock s1 =>
      find_label lbl s1 (Kblock k)
  | Slabel lbl' s' =>
      if ident_eq lbl lbl' then Some(s', k) else find_label lbl s' k
  | _ => None
  end.


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

  | step_skip_seq: forall f s k sp e m,
      step (State f Sskip (Kseq s k) sp e m)
        E0 (State f s k sp e m)
  | step_skip_block: forall f k sp e m,
      step (State f Sskip (Kblock k) sp e m)
        E0 (State f Sskip k sp e m)
  | step_skip_call: forall f k sp e m m' m'',
      is_call_cont k ->
      Mem.free m sp 0 (f.(fn_stackspace)) = Some m' ->
      release_boxes m' (needed_stackspace (fn_id f)) = Some m'' ->
      step (State f Sskip k sp e m)
        E0 (Returnstate (Eval Vundef) k m'')

  | step_assign: forall f id a k sp e m v,
      eval_expr sp e m a v ->
      step (State f (Sassign id a) k sp e m)
        E0 (State f Sskip k sp (PTree.set id v e) m)

  | step_store: forall f chunk addr a k sp e m vaddr v m',
      eval_expr sp e m addr vaddr ->
      eval_expr sp e m a v ->
      Mem.storev chunk m vaddr v = Some m' ->
      step (State f (Sstore chunk addr a) k sp e m)
        E0 (State f Sskip k sp e m')

  | step_call: forall f optid sig a bl k sp e m vf vargs fd,
      eval_expr sp e m a vf ->
      eval_exprlist sp e m bl vargs ->
      Genv.find_funct m ge vf = Some fd ->
      funsig fd = sig ->
      step (State f (Scall optid sig a bl) k sp e m)
        E0 (Callstate fd vargs (Kcall optid f sp e k) m)

  | step_tailcall: forall f sig a bl k sp e m vf vargs fd m' m'',
      eval_expr sp e m a vf ->
      eval_exprlist sp e m bl vargs ->
      Genv.find_funct m'' ge vf = Some fd ->
      funsig fd = sig ->
      Mem.free m sp 0 ( f.(fn_stackspace) ) = Some m' ->
      release_boxes m' (needed_stackspace (fn_id f)) = Some m'' ->
      step (State f (Stailcall sig a bl) k sp e m)
        E0 (Callstate fd vargs (call_cont k) m'')

  | step_builtin: forall f optid ef bl k sp e m vargs t vres m',
      eval_exprlist sp e m bl vargs ->
      external_call ef ge vargs m t vres m' ->
      step (State f (Sbuiltin optid ef bl) k sp e m)
         t (State f Sskip k sp (set_optvar optid vres e) m')

  | step_seq: forall f s1 s2 k sp e m,
      step (State f (Sseq s1 s2) k sp e m)
        E0 (State f s1 (Kseq s2 k) sp e m)

  | step_ifthenelse: forall f a s1 s2 k sp e m v b,
                       eval_expr sp e m a v ->
                       Mem.mem_norm m v = Vint b ->
                       step (State f (Sifthenelse a s1 s2) k sp e m)
                            E0 (State f (if negb (Int.eq b Int.zero) then s1 else s2) k sp e m)

  | step_loop: forall f s k sp e m,
      step (State f (Sloop s) k sp e m)
        E0 (State f s (Kseq (Sloop s) k) sp e m)

  | step_block: forall f s k sp e m,
      step (State f (Sblock s) k sp e m)
        E0 (State f s (Kblock k) sp e m)

  | step_exit_seq: forall f n s k sp e m,
      step (State f (Sexit n) (Kseq s k) sp e m)
        E0 (State f (Sexit n) k sp e m)
  | step_exit_block_0: forall f k sp e m,
      step (State f (Sexit O) (Kblock k) sp e m)
        E0 (State f Sskip k sp e m)
  | step_exit_block_S: forall f n k sp e m,
      step (State f (Sexit (S n)) (Kblock k) sp e m)
        E0 (State f (Sexit n) k sp e m)

  | step_switch: forall f islong a cases default k sp e m v n,
      eval_expr sp e m a v ->
      switch_argument m islong v n ->
      step (State f (Sswitch islong a cases default) k sp e m)
        E0 (State f (Sexit (switch_target n default cases)) k sp e m)

  | step_return_0: forall f k sp e m m' m'',
      Mem.free m sp 0 ( f.(fn_stackspace) ) = Some m' ->
      release_boxes m' (needed_stackspace (fn_id f)) = Some m'' ->
      step (State f (Sreturn None) k sp e m)
        E0 (Returnstate (Eval Vundef) (call_cont k) m'')
  | step_return_1: forall f a k sp e m v m' m'',
      eval_expr sp e m a v ->
      Mem.free m sp 0 ( f.(fn_stackspace)) = Some m' ->
      release_boxes m' (needed_stackspace (fn_id f)) = Some m'' ->
      step (State f (Sreturn (Some a)) k sp e m)
        E0 (Returnstate v (call_cont k) m'')

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

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

  | step_internal_function: forall f vargs k m m' sp e m1 ,
      Mem.alloc m 0 ( f.(fn_stackspace)) Normal = Some (m1, sp) ->
      reserve_boxes m1 (needed_stackspace f.(fn_id)) = Some m' ->
      set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
      step (Callstate (Internal f) vargs k m)
        E0 (State f f.(fn_body) k sp e m')
  | step_external_function: forall ef vargs k m t vres m',
      external_call ef ge vargs m t vres m' ->
      step (Callstate (External ef) vargs k m)
         t (Returnstate vres k m')

  | step_return: forall v optid f sp e k m,
      step (Returnstate v (Kcall optid f sp e k) m)
        E0 (State f Sskip k sp (set_optvar optid v e) m).

End RELSEM.


Definition fid f :=
  match f with
    Internal f => Some (fn_id f)
  | _ => None
  end.

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


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


Definition semantics (p: program) ns sg :=
  Semantics (fun ge => step ge ns) (initial_state p sg) final_state (Genv.globalenv p).


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

Alternate operational semantics (big-step)

Inductive outcome: Type :=
  | Out_normal: outcome (* continue in sequence *)
  | Out_exit: nat -> outcome (* terminate n+1 enclosing blocks *)
  | Out_return: option expr_sym -> outcome (* return immediately to caller *)
  | Out_tailcall_return: expr_sym -> outcome. (* already returned to caller via a tailcall *)

Definition outcome_block (out: outcome) : outcome :=
  match out with
  | Out_exit O => Out_normal
  | Out_exit (S n) => Out_exit n
  | out => out
  end.

Definition outcome_result_value
    (out: outcome) (retsig: option typ) (vres: expr_sym) : Prop :=
  match out with
  | Out_normal => vres = Eval Vundef
  | Out_return None => vres = Eval Vundef
  | Out_return (Some v) => retsig <> None /\ vres = v
  | Out_tailcall_return v => vres = v
  | _ => False
  end.

Definition outcome_free_mem
    (out: outcome) (m: mem) (sp: block) (sz: Z) (m': mem) :=
  match out with
  | Out_tailcall_return _ => m' = m
  | _ => Mem.free m sp 0 sz = Some m'
  end.

Definition outcome_free_mem_extra
    (out: outcome) (m: mem) (n: nat) (m': mem) :=
  match out with
  | Out_tailcall_return _ => m' = m
  | _ => release_boxes m n = Some m'
  end.

Section NATURALSEM.

Variable ge: genv.

Variable needed_stackspace : ident -> nat .


Inductive eval_funcall:
        mem -> fundef -> list expr_sym -> trace ->
        mem -> expr_sym -> Prop :=
  | eval_funcall_internal:
      forall m f vargs m1 sp e t e2 m2 out vres m3 m4 m',
        Mem.alloc m 0 ( f.(fn_stackspace)) Normal = Some (m1, sp) ->
        reserve_boxes m1 (needed_stackspace f.(fn_id)) = Some m' ->
      set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
      exec_stmt f sp e m' f.(fn_body) t e2 m2 out ->
      outcome_result_value out f.(fn_sig).(sig_res) vres ->
      outcome_free_mem out m2 sp ( f.(fn_stackspace) ) m3 ->
      outcome_free_mem_extra out m3 (needed_stackspace (fn_id f)) m4 ->
      eval_funcall m (Internal f) vargs t m4 vres
  | eval_funcall_external:
      forall ef m args t res m',
      external_call ef ge args m t res m' ->
      eval_funcall m (External ef) args t m' res


with exec_stmt:
       function ->
       block ->
         env -> mem -> stmt -> trace ->
         env -> mem -> outcome -> Prop :=
  | exec_Sskip:
      forall f sp e m,
      exec_stmt f sp e m Sskip E0 e m Out_normal
  | exec_Sassign:
      forall f sp e m id a v,
      eval_expr ge sp e m a v ->
      exec_stmt f sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal
  | exec_Sstore:
      forall f sp e m chunk addr a vaddr v m',
      eval_expr ge sp e m addr vaddr ->
      eval_expr ge sp e m a v ->
      Mem.storev chunk m vaddr v = Some m' ->
      exec_stmt f sp e m (Sstore chunk addr a) E0 e m' Out_normal
  | exec_Scall:
      forall f sp e m optid sig a bl vf vargs fd t m' vres e',
      eval_expr ge sp e m a vf ->
      eval_exprlist ge sp e m bl vargs ->
      Genv.find_funct m ge vf = Some fd ->
      funsig fd = sig ->
      eval_funcall m fd vargs t m' vres ->
      e' = set_optvar optid vres e ->
      exec_stmt f sp e m (Scall optid sig a bl) t e' m' Out_normal
  | exec_Sbuiltin:
      forall f sp e m optid ef bl t m' vargs vres e',
      eval_exprlist ge sp e m bl vargs ->
      external_call ef ge vargs m t vres m' ->
      e' = set_optvar optid vres e ->
      exec_stmt f sp e m (Sbuiltin optid ef bl) t e' m' Out_normal
  | exec_Sifthenelse:
      forall f sp e m a s1 s2 v b t e' m' out,
      eval_expr ge sp e m a v ->
      Mem.mem_norm m v = Vint b ->
      exec_stmt f sp e m (if negb (Int.eq b Int.zero) then s1 else s2) t e' m' out ->
      exec_stmt f sp e m (Sifthenelse a s1 s2) t e' m' out
  | exec_Sseq_continue:
      forall f sp e m t s1 t1 e1 m1 s2 t2 e2 m2 out,
      exec_stmt f sp e m s1 t1 e1 m1 Out_normal ->
      exec_stmt f sp e1 m1 s2 t2 e2 m2 out ->
      t = t1 ** t2 ->
      exec_stmt f sp e m (Sseq s1 s2) t e2 m2 out
  | exec_Sseq_stop:
      forall f sp e m t s1 s2 e1 m1 out,
      exec_stmt f sp e m s1 t e1 m1 out ->
      out <> Out_normal ->
      exec_stmt f sp e m (Sseq s1 s2) t e1 m1 out
  | exec_Sloop_loop:
      forall f sp e m s t t1 e1 m1 t2 e2 m2 out,
      exec_stmt f sp e m s t1 e1 m1 Out_normal ->
      exec_stmt f sp e1 m1 (Sloop s) t2 e2 m2 out ->
      t = t1 ** t2 ->
      exec_stmt f sp e m (Sloop s) t e2 m2 out
  | exec_Sloop_stop:
      forall f sp e m t s e1 m1 out,
      exec_stmt f sp e m s t e1 m1 out ->
      out <> Out_normal ->
      exec_stmt f sp e m (Sloop s) t e1 m1 out
  | exec_Sblock:
      forall f sp e m s t e1 m1 out,
      exec_stmt f sp e m s t e1 m1 out ->
      exec_stmt f sp e m (Sblock s) t e1 m1 (outcome_block out)
  | exec_Sexit:
      forall f sp e m n,
      exec_stmt f sp e m (Sexit n) E0 e m (Out_exit n)
  | exec_Sswitch:
      forall f sp e m islong a cases default v n,
      eval_expr ge sp e m a v ->
      switch_argument m islong v n ->
      exec_stmt f sp e m (Sswitch islong a cases default)
                E0 e m (Out_exit (switch_target n default cases))
  | exec_Sreturn_none:
      forall f sp e m,
      exec_stmt f sp e m (Sreturn None) E0 e m (Out_return None)
  | exec_Sreturn_some:
      forall f sp e m a v,
      eval_expr ge sp e m a v ->
      exec_stmt f sp e m (Sreturn (Some a)) E0 e m (Out_return (Some v))
  | exec_Stailcall:
      forall f sp e m sig a bl vf vargs fd t m' m'' vres m''',
      eval_expr ge sp e m a vf ->
      eval_exprlist ge sp e m bl vargs ->
      Genv.find_funct m'' ge vf = Some fd ->
      funsig fd = sig ->
      Mem.free m sp 0 ( f.(fn_stackspace)) = Some m' ->
      release_boxes m' (needed_stackspace (fn_id f)) = Some m'' ->
      eval_funcall m'' fd vargs t m''' vres ->
      exec_stmt f sp e m (Stailcall sig a bl) t e m''' (Out_tailcall_return vres).

Scheme eval_funcall_ind2 := Minimality for eval_funcall Sort Prop
  with exec_stmt_ind2 := Minimality for exec_stmt Sort Prop.
Combined Scheme eval_funcall_exec_stmt_ind2
  from eval_funcall_ind2, exec_stmt_ind2.


CoInductive evalinf_funcall:
        mem -> fundef -> list expr_sym -> traceinf -> Prop :=
  | evalinf_funcall_internal:
      forall m f vargs m1 sp e t m',
        Mem.alloc m 0 (f.(fn_stackspace)) Normal = Some (m1, sp) ->
        reserve_boxes m1 (needed_stackspace f.(fn_id)) = Some m' ->
        set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
        execinf_stmt f sp e m' f.(fn_body) t ->
        evalinf_funcall m (Internal f) vargs t


with execinf_stmt:
         function -> block -> env -> mem -> stmt -> traceinf -> Prop :=
  | execinf_Scall:
      forall f sp e m optid sig a bl vf vargs fd t,
      eval_expr ge sp e m a vf ->
      eval_exprlist ge sp e m bl vargs ->
      Genv.find_funct m ge vf = Some fd ->
      funsig fd = sig ->
      evalinf_funcall m fd vargs t ->
      execinf_stmt f sp e m (Scall optid sig a bl) t
  | execinf_Sifthenelse:
      forall f sp e m a s1 s2 v b t,
      eval_expr ge sp e m a v ->
      Mem.mem_norm m v = Vint b ->
      execinf_stmt f sp e m (if negb (Int.eq b Int.zero) then s1 else s2) t ->
      execinf_stmt f sp e m (Sifthenelse a s1 s2) t
  | execinf_Sseq_1:
      forall f sp e m t s1 s2,
      execinf_stmt f sp e m s1 t ->
      execinf_stmt f sp e m (Sseq s1 s2) t
  | execinf_Sseq_2:
      forall f sp e m t s1 t1 e1 m1 s2 t2,
      exec_stmt f sp e m s1 t1 e1 m1 Out_normal ->
      execinf_stmt f sp e1 m1 s2 t2 ->
      t = t1 *** t2 ->
      execinf_stmt f sp e m (Sseq s1 s2) t
  | execinf_Sloop_body:
      forall f sp e m s t,
      execinf_stmt f sp e m s t ->
      execinf_stmt f sp e m (Sloop s) t
  | execinf_Sloop_loop:
      forall f sp e m s t t1 e1 m1 t2,
      exec_stmt f sp e m s t1 e1 m1 Out_normal ->
      execinf_stmt f sp e1 m1 (Sloop s) t2 ->
      t = t1 *** t2 ->
      execinf_stmt f sp e m (Sloop s) t
  | execinf_Sblock:
      forall f sp e m s t,
      execinf_stmt f sp e m s t ->
      execinf_stmt f sp e m (Sblock s) t
  | execinf_Stailcall:
      forall f sp e m sig a bl vf vargs fd m' t m'',
      eval_expr ge sp e m a vf ->
      eval_exprlist ge sp e m bl vargs ->
      Genv.find_funct m'' ge vf = Some fd ->
      funsig fd = sig ->
      Mem.free m sp 0 (f.(fn_stackspace)) = Some m' ->
      release_boxes m' (needed_stackspace (fn_id f)) = Some m'' ->
      evalinf_funcall m'' fd vargs t ->
      execinf_stmt f sp e m (Stailcall sig a bl) t.

End NATURALSEM.


Inductive bigstep_program_terminates (p: program) ns sg : trace -> int -> Prop :=
  | bigstep_program_terminates_intro:
      forall b f m0 t m r e,
      let ge := Genv.globalenv p in
      Genv.init_mem fid sg p = Some m0 ->
      Genv.find_symbol ge p.(prog_main) = Some b ->
      Genv.find_funct_ptr ge b = Some f ->
      funsig f = signature_main ->
      Mem.mem_norm m e = Vint r ->
      eval_funcall ge ns m0 f nil t m e ->
      bigstep_program_terminates p ns sg t r.

Inductive bigstep_program_diverges (p: program) ns sg: traceinf -> Prop :=
  | bigstep_program_diverges_intro:
      forall b f m0 t,
      let ge := Genv.globalenv p in
      Genv.init_mem fid sg p = Some m0 ->
      Genv.find_symbol ge p.(prog_main) = Some b ->
      Genv.find_funct_ptr ge b = Some f ->
      funsig f = signature_main ->
      evalinf_funcall ge ns m0 f nil t ->
      bigstep_program_diverges p ns sg t.

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

Correctness of the big-step semantics with respect to the transition semantics

Section BIGSTEP_TO_TRANSITION.
 
Variable prog: program.
Let ge := Genv.globalenv prog.

Variable needed_stackspace : ident -> nat .


Inductive outcome_state_match
        (sp: block) (e: env) (m: mem) (f: function) (k: cont):
        outcome -> state -> Prop :=
  | osm_normal:
      outcome_state_match sp e m f k
                          Out_normal
                          (State f Sskip k sp e m)
  | osm_exit: forall n,
      outcome_state_match sp e m f k
                          (Out_exit n)
                          (State f (Sexit n) k sp e m)
  | osm_return_none: forall k',
      call_cont k' = call_cont k ->
      outcome_state_match sp e m f k
                          (Out_return None)
                          (State f (Sreturn None) k' sp e m)
  | osm_return_some: forall k' a v,
      call_cont k' = call_cont k ->
      eval_expr ge sp e m a v ->
      outcome_state_match sp e m f k
                          (Out_return (Some v))
                          (State f (Sreturn (Some a)) k' sp e m)
  | osm_tail: forall v,
      outcome_state_match sp e m f k
                          (Out_tailcall_return v)
                          (Returnstate v (call_cont k) m).

Remark is_call_cont_call_cont:
  forall k, is_call_cont (call_cont k).

Remark call_cont_is_call_cont:
  forall k, is_call_cont k -> call_cont k = k.

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

Lemma eval_funcall_steps:
   forall m fd args t m' res,
   eval_funcall ge needed_stackspace m fd args t m' res ->
   forall k,
   is_call_cont k ->
   star (fun ge => step ge needed_stackspace) ge (Callstate fd args k m)
              t (Returnstate res k m').
Proof (proj1 eval_funcall_exec_stmt_steps).

Lemma exec_stmt_steps:
   forall f sp e m s t e' m' out,
   exec_stmt ge needed_stackspace f sp e m s t e' m' out ->
   forall k,
   exists S,
   star (fun ge => step ge needed_stackspace) ge (State f s k sp e m) t S
   /\ outcome_state_match sp e' m' f k out S.
Proof (proj2 eval_funcall_exec_stmt_steps).

Lemma evalinf_funcall_forever:
  forall m fd args T k,
  evalinf_funcall ge needed_stackspace m fd args T ->
  forever_plus (fun ge => step ge needed_stackspace) ge (Callstate fd args k m) T.

Theorem bigstep_semantics_sound:
  forall sg,
    bigstep_sound
      (bigstep_semantics prog needed_stackspace sg)
      (semantics prog needed_stackspace sg).

End BIGSTEP_TO_TRANSITION.