Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Switch.
Require Export Csharpminor.
Require Import Smallstep.
Require Import Annotations.
Require Import AssocList.


Inductive expr : Type :=
  | Evar : ident -> expr (* reading a temporary variable *)
  | Eaddrof : ident -> expr (* taking the address of a variable *)
  | Econst : constant -> expr (* constants *)
  | Eunop : unary_operation -> expr -> expr (* unary operation *)
  | Ebinop : binary_operation -> expr -> expr -> expr (* binary operation *)
  | Eload : annotation -> memory_chunk -> expr -> expr. (* memory read *)

Fixpoint expr_erase (e: expr) : Csharpminor.expr :=
  match e with
  | Evar i => Csharpminor.Evar i
  | Eaddrof x => Csharpminor.Eaddrof x
  | Econst c => Csharpminor.Econst c
  | Eunop op e => Csharpminor.Eunop op (expr_erase e)
  | Ebinop op e e' => Csharpminor.Ebinop op (expr_erase e) (expr_erase e')
  | Eload _ κ e => Csharpminor.Eload κ (expr_erase e)
  end.


Inductive stmt : Type :=
  | Sskip: stmt
  | Sset : ident -> expr -> stmt
  | Sstore : annotation -> memory_chunk -> expr -> expr -> stmt
  | Scall : option ident -> 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 -> lbl_stmt -> stmt
  | Sreturn: option expr -> stmt
  | Slabel: label -> stmt -> stmt
  | Sgoto: label -> stmt

with lbl_stmt : Type :=
  | LSnil: lbl_stmt
  | LScons: option Z -> stmt -> lbl_stmt -> lbl_stmt.


Record function : Type := mkfunction {
  fn_sig: signature;
  fn_params: list ident;
  fn_vars: list (ident * Z);
  fn_temps: list ident;
  fn_body: stmt
}.

Definition fundef := AST.fundef function.

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

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

Operational semantics

Definition genv := Genv.t fundef unit.


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 -> env -> temp_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 *)
             (e: env) (* current local environment *)
             (le: temp_env) (* current temporary environment *)
             (m: mem) (* current memory state *)
             ,
      state
  | Callstate: (* Invocation of a function *)
      forall (f: fundef) (* function to invoke *)
             (args: list val) (* arguments provided by caller *)
             (k: cont) (* what to do next *)
             (m: mem) (* memory state *)
      ,
      state
  | Returnstate: (* Return from a function *)
      forall (v: val) (* Return value *)
             (k: cont) (* what to do next *)
             (m: mem) (* memory state *)
             ,
      state.


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 select_switch_default (sl: lbl_stmt): lbl_stmt :=
  match sl with
  | LSnil => sl
  | LScons None s sl' => sl
  | LScons (Some i) s sl' => select_switch_default sl'
  end.

Fixpoint select_switch_case (n: Z) (sl: lbl_stmt): option lbl_stmt :=
  match sl with
  | LSnil => None
  | LScons None s sl' => select_switch_case n sl'
  | LScons (Some c) s sl' => if zeq c n then Some sl else select_switch_case n sl'
  end.

Definition select_switch (n: Z) (sl: lbl_stmt): lbl_stmt :=
  match select_switch_case n sl with
  | Some sl' => sl'
  | None => select_switch_default sl
  end.

Fixpoint seq_of_lbl_stmt (sl: lbl_stmt) : stmt :=
  match sl with
  | LSnil => Sskip
  | LScons c s sl' => Sseq s (seq_of_lbl_stmt sl')
  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)
  | Sswitch long a sl =>
      find_label_ls lbl sl 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: lbl_stmt) (k: cont)
                   {struct sl}: option (stmt * cont) :=
  match sl with
  | LSnil => None
  | LScons _ s sl' =>
      match find_label lbl s (Kseq (seq_of_lbl_stmt sl') k) with
      | Some sk => Some sk
      | None => find_label_ls lbl sl' k
      end
  end.

Section RELSEM.

Variable ge: genv.
Let eval_var_addr := eval_var_addr ge.
Let eval_expr ε τ m e := eval_expr ge ε τ m (expr_erase e).
Let eval_exprlist ε τ m e := eval_exprlist ge ε τ m (List.map expr_erase e).


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

  | 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_skip_block: forall f k e le m,
      step (State f Sskip (Kblock k) e le m)
        E0 (State f Sskip k e le m)
  | step_skip_call: forall f k e le m m',
      is_call_cont k ->
      Mem.free_list m (blocks_of_env e) = Some m' ->
      step (State f Sskip k e le m)
        E0 (Returnstate Vundef k 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_store: forall f chunk addr a k e le m vaddr v m' n annot,
      eval_expr e le m addr vaddr ->
      eval_expr e le m a v ->
      Mem.storev chunk m vaddr v = Some m' ->
      step (State f (Sstore (n, annot) chunk addr a) k e le m)
        E0 (State f Sskip k e le m')

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

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

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

  | step_ifthenelse: forall f a s1 s2 k e le m v b,
      eval_expr e le m a v ->
      Val.bool_of_val v 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_loop: forall f s k e le m,
      step (State f (Sloop s) k e le m)
        E0 (State f s (Kseq (Sloop s) k) e le m)

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

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

  | step_switch: forall f islong a cases k e le m v n,
      eval_expr e le m a v ->
      switch_argument islong v n ->
      step (State f (Sswitch islong a cases) k e le m)
        E0 (State f (seq_of_lbl_stmt (select_switch n cases)) 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 m',
      eval_expr e le m a 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_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 m1 e le,
      list_norepet (map fst f.(fn_vars)) ->
      list_norepet f.(fn_params) ->
      list_disjoint f.(fn_params) f.(fn_temps) ->
      alloc_variables empty_env m (fn_vars f) e m1 ->
      bind_parameters f.(fn_params) vargs (create_undef_temps f.(fn_temps)) = Some le ->
      step (Callstate (Internal f) vargs k m)
        E0 (State f f.(fn_body) k e le m1)

  | 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 e le k m,
      step (Returnstate v (Kcall optid f e le k) m)
        E0 (State f Sskip k e (Cminor.set_optvar optid v le) m).

End RELSEM.


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 ->
      funsig f = signature_main ->
      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, receptive (semantics p).