Require Import Coqlib Maps AST Integers Values Memory Events Globalenvs Smallstep.
Require Import Op Machregs Locations Stacklayout Conventions.
Require Import Mach Machblock OptionMonad.


(** Registers and States *)

Inductive preg: Type :=
  | PC: preg (* program counter *)
  | RA: preg (* return-address *)
  | SP: preg (* stack-pointer *)
  | preg_of: mreg -> preg.
Coercion preg_of: mreg >-> preg.

Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
Proof.
 decide equality.
 apply mreg_eq.
Defined.

Module PregEq.
  Definition t := preg.
  Definition eq := preg_eq.
End PregEq.

Module Pregmap := EMap(PregEq).

Definition regset := Pregmap.t val.

Module AsmNotations.

(* Declare Scope asm. *)
Notation "a # b" := (a b) (at level 1, only parsing) : asm.
Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
Open Scope asm.

End AsmNotations.

Import AsmNotations.

Definition to_Machrs (rs: regset): Mach.regset :=
 fun (r:mreg) => rs r.
Coercion to_Machrs: regset >-> Mach.regset.

Definition set_from_Machrs (mrs: Mach.regset) (rs: regset): regset :=
 fun (r:preg) => 
   match r with 
   | preg_of mr => mrs mr
   | _ => rs r
   end.

Local Open Scope option_monad_scope.

Record state: Type := State { _rs: regset; _m: mem }.
Definition outcome := option state.
Definition Next rs m: outcome := Some (State rs m).
Definition Stuck: outcome := None.

(* Asm semantic on Mach *)

Section RELSEM.

(** "oracle" stating the successive position (ie offset) of each block in the final assembly function *)
Variable next: function -> Z -> Z.

Inductive is_pos (f: function): Z -> code -> Prop :=
  | First_pos: is_pos f 0 (fn_code f)
  | Next_pos pos b c: is_pos f pos (b::c) -> is_pos f (next f pos) c.

Fixpoint label_pos (f: function) (lbl: label) (pos: Z) (c: code) {struct c} : option Z :=
  match c with
  | nil => None
  | b :: c' =>
    if is_label lbl b then Some pos else label_pos f lbl (next f pos) c'
  end.

Definition goto_label (f: function) (lbl: label) (rs: regset) : option val :=
  SOME pos <- label_pos f lbl 0 (fn_code f) IN
  match rs#PC with
  | Vptr b _ => Some (Vptr b (Ptrofs.repr pos))
  | _        => None
  end.

Definition next_addr (f: function) (rs: regset): option val :=
  match rs#PC with
  | Vptr b ofs => Some (Vptr b (Ptrofs.repr (next f (Ptrofs.unsigned ofs))))
  | _          => None
  end.

Variable ge:genv.

Inductive basic_step (f: function) (rs: regset) (m:mem): basic_inst -> regset -> mem -> Prop :=
  | exec_MBgetstack:
      forall ofs ty dst v,
      load_stack m (rs#SP) ty ofs = Some v ->
      basic_step f rs m (MBgetstack ofs ty dst) (rs#dst <- v) m
  | exec_MBsetstack:
      forall (src: mreg) ofs ty m' rs',
      store_stack m (rs#SP) ty ofs (rs src) = Some m' ->
      rs' = set_from_Machrs (undef_regs (destroyed_by_setstack ty) rs) rs ->
      basic_step f rs m (MBsetstack src ofs ty) rs' m'
  | exec_MBgetparam:
      forall ofs ty (dst: mreg) v rs' psp,
      load_stack m (rs#SP) Tptr f.(fn_link_ofs) = Some psp ->
      load_stack m psp ty ofs = Some v ->
      rs' = (rs # temp_for_parent_frame <- Vundef # dst <- v) ->
      basic_step f rs m (MBgetparam ofs ty dst) rs' m
  | exec_MBop:
      forall op args v rs' (res: mreg),
      eval_operation ge (rs#SP) op (to_Machrs rs)##args m = Some v ->
      rs' = (set_from_Machrs (undef_regs (destroyed_by_op op) rs) rs)#res <- v ->
      basic_step f rs m (MBop op args res) rs' m
  | exec_MBload:
      forall addr args a v rs' trap chunk (dst: mreg),
      eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = Some a ->
      Mem.loadv chunk m a = Some v ->
      rs' = (set_from_Machrs (undef_regs (destroyed_by_load chunk addr) rs) rs)#dst <- v ->
      basic_step f rs m (MBload trap chunk addr args dst) rs' m
  | exec_MBload_notrap1:
      forall addr args rs' chunk (dst: mreg),
      eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = None ->
      rs' = (set_from_Machrs (undef_regs (destroyed_by_load chunk addr) rs) rs)#dst <- (default_notrap_load_value chunk) ->
      basic_step f rs m (MBload NOTRAP chunk addr args dst) rs' m
  | exec_MBload_notrap2:
      forall addr args a rs' chunk (dst: mreg),
      eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = Some a ->
      Mem.loadv chunk m a = None ->
      rs' = (set_from_Machrs (undef_regs (destroyed_by_load chunk addr) rs) rs)#dst <- (default_notrap_load_value chunk) ->
      basic_step f rs m (MBload NOTRAP chunk addr args dst) rs' m
  | exec_MBstore:
      forall chunk addr args (src: mreg) m' a rs',
      eval_addressing ge (rs#SP) addr (to_Machrs rs)##args = Some a ->
      Mem.storev chunk m a (rs src) = Some m' ->
      rs' = set_from_Machrs (undef_regs (destroyed_by_store chunk addr) rs) rs ->
      basic_step f rs m (MBstore chunk addr args src) rs' m'
  .


Inductive body_step (f: function) : bblock_body -> regset -> mem -> regset -> mem -> Prop :=
   | exec_nil_body rs m:
       body_step f nil rs m rs m
   | exec_cons_body rs m bi p rs' m' rs'' m'':
       basic_step f rs m bi rs' m' ->
       body_step f p rs' m' rs'' m'' ->
       body_step f (bi::p) rs m rs'' m''
   .


Definition find_function_ptr (ros: mreg + ident) (rs: regset) : option val :=
  match ros with
  | inl r => Some (rs#r)
  | inr symb =>
      SOME b <- Genv.find_symbol ge symb IN
      Some (Vptr b Ptrofs.zero)
  end.

Definition exec_epilogue (f: function) (rs: regset) (m: mem) : outcome :=
   SOME sp <- load_stack m rs#SP Tptr f.(fn_link_ofs) IN
   SOME ra <- load_stack m rs#SP Tptr f.(fn_retaddr_ofs) IN
   match rs#SP with
   | Vptr stk ofs =>
     SOME m' <- Mem.free m stk 0 f.(fn_stacksize) IN
     Next (rs#SP <- sp #RA <- ra) m'
   | _ => Stuck
   end.

Inductive cfi_step (f: function): control_flow_inst -> regset -> mem -> trace -> regset -> mem -> Prop :=
  | exec_MBcall sig ros rs m pc:
      find_function_ptr ros rs = Some pc ->
      cfi_step f (MBcall sig ros) rs m E0 ((rs#RA <- (rs#PC))#PC <- pc) m
  | exec_MBtailcall sig ros rs m rs' m' pc:
      find_function_ptr ros rs = Some pc ->
      exec_epilogue f rs m = Next rs' m' ->
      cfi_step f (MBtailcall sig ros) rs m E0 (rs'#PC <- pc) m'
  | exec_MBreturn rs m rs' m':
      exec_epilogue f rs m = Next rs' m' ->
      cfi_step f MBreturn rs m E0 (rs'#PC <- (rs'#RA)) m'
  | exec_MBgoto lbl rs m pc:
      goto_label f lbl rs = Some pc ->
      cfi_step f (MBgoto lbl) rs m E0 (rs#PC <- pc) m
  | exec_MBcond_true cond args lbl rs m pc rs':
      eval_condition cond (to_Machrs rs)##args m = Some true ->
      goto_label f lbl rs = Some pc ->
      rs' = set_from_Machrs (undef_regs (destroyed_by_cond cond) rs) rs ->
      cfi_step f (MBcond cond args lbl) rs m E0 (rs'#PC <- pc) m
  | exec_MBcond_false cond args lbl rs m rs':
      eval_condition cond (to_Machrs rs)##args m = Some false ->
      rs' = set_from_Machrs (undef_regs (destroyed_by_cond cond) rs) rs ->
      cfi_step f (MBcond cond args lbl) rs m E0 rs' m
  | exec_MBjumptable arg tbl rs m index lbl pc rs':
      to_Machrs rs arg = Vint index ->
      list_nth_z tbl (Int.unsigned index) = Some lbl ->
      goto_label f lbl rs = Some pc ->
      rs' = set_from_Machrs (undef_regs destroyed_by_jumptable rs) rs ->
      cfi_step f (MBjumptable arg tbl) rs m E0 (rs'#PC <- pc) m
  | exec_MBbuiltin rs m ef args res vargs t vres rs' m':
      eval_builtin_args ge (to_Machrs rs) (rs#SP) m args vargs ->
      external_call ef ge vargs m t vres m' ->
      rs' = set_from_Machrs (set_res res vres (undef_regs (destroyed_by_builtin ef) rs)) rs ->
      cfi_step f (MBbuiltin ef args res) rs m t rs' m'
  .

Inductive exit_step f : option control_flow_inst -> regset -> mem -> trace -> regset -> mem -> Prop :=
  | exec_Some_exit ctl rs m t rs' m':
      cfi_step f ctl rs m t rs' m' ->
      exit_step f (Some ctl) rs m t rs' m'
  | exec_None_exit rs m:
      exit_step f None rs m E0 rs m
  .

Inductive exec_bblock f: bblock -> regset -> mem -> trace -> regset -> mem -> Prop :=
  | exec_bblock_all (bb: bblock) rs0 m0 rs1 m1 pc t rs2 m2: 
       body_step f (body bb) rs0 m0 rs1 m1 ->
       next_addr f rs1 = Some pc ->
       exit_step f (exit bb) (rs1#PC <- pc) m1 t rs2 m2 ->
       exec_bblock f bb rs0 m0 t rs2 m2.

Definition exec_prologue f (pos:Z) (rs: regset) (m:mem) : option state :=
    if Z.eq_dec pos 0 then
      let (m1, stk) := Mem.alloc m 0 f.(fn_stacksize) in
      let sp := Vptr stk Ptrofs.zero in
      SOME m2 <- store_stack m1 sp Tptr f.(fn_link_ofs) rs#SP IN
      SOME m3 <- store_stack m2 sp Tptr f.(fn_retaddr_ofs) rs#RA IN
      Next ((set_from_Machrs (undef_regs destroyed_at_function_entry rs) rs)#SP <- sp) m3
    else
      Next rs m.


Inductive step: state -> trace -> state -> Prop :=
  | exec_step_internal b ofs f bb c rs0 m0 rs1 m1 t rs2 m2:
      rs0 PC = Vptr b ofs ->
      Genv.find_funct_ptr ge b = Some (Internal f) ->
      is_pos f (Ptrofs.unsigned ofs) (bb::c) ->
      exec_prologue f (Ptrofs.unsigned ofs) rs0 m0 = Next rs1 m1 ->
      exec_bblock f bb rs1 m1 t rs2 m2 ->
      step (State rs0 m0) t (State rs2 m2)
  | exec_step_external:
      forall b ef args res rs m t rs' m',
      rs PC = Vptr b Ptrofs.zero ->
      Genv.find_funct_ptr ge b = Some (External ef) ->
      extcall_arguments (to_Machrs rs) m (rs#SP) (ef_sig ef) args ->
      external_call ef ge args m t res m' ->
      rs' = (set_from_Machrs (set_pair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs)) rs) #PC <- (rs RA) ->
      step (State rs m) t (State rs' m').

End RELSEM.

Inductive initial_state (p: program): state -> Prop :=
  | initial_state_intro: forall m0,
      let ge := Genv.globalenv p in
      Genv.init_mem p = Some m0 ->
      let rs0 :=
        (Pregmap.init Vundef)
        # PC <- (Genv.symbol_address ge p.(prog_main) Ptrofs.zero)
        # SP <- Vnullptr
        # RA <- Vnullptr in
      initial_state p (State rs0 m0).

Inductive final_state: state -> int -> Prop :=
  | final_state_intro: forall rs m r retcode,
      loc_result signature_main = One r ->
      rs PC = Vnullptr ->
      rs r = Vint retcode ->
      final_state (State rs m) retcode.

Definition semantics (next: function -> Z -> Z) (p: program) :=
  Semantics (step next) (initial_state p) final_state (Genv.globalenv p).