include "joint/SemanticUtils.ma".
include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
include alias "common/Identifiers.ma".

record ertl_psd_env : Type[0] ≝
  { psd_regs : register_env beval
  (* this tells what pseudo-registers should have their value corrected by spilled_no *)
  ; need_spilled_no : identifier_set RegisterTag
  }.

definition set_psd_regs ≝ λx,env.mk_ertl_psd_env x (need_spilled_no env).
definition add_need_spilled_no ≝
  λr,env.mk_ertl_psd_env (psd_regs env) (add_set … (need_spilled_no env) r).
definition rm_need_spilled_no ≝
  λr,env.mk_ertl_psd_env (psd_regs env) (need_spilled_no env ∖  {(r)}).

definition ertl_reg_env ≝ ertl_psd_env × hw_register_env.

definition ps_reg_store ≝
 λr,v.λlocal_env : ertl_reg_env.
  do res ← reg_store r v (psd_regs (\fst local_env)) ;
  let psd_env ≝ set_psd_regs res (\fst local_env) in
  OK … 〈rm_need_spilled_no r psd_env, \snd local_env〉.

definition ps_reg_retrieve ≝
 λlocal_env:ertl_reg_env. reg_retrieve … (psd_regs (\fst local_env)).

definition hw_reg_store ≝
 λr,v.λlocal_env:ertl_reg_env.
  OK … 〈\fst local_env,hwreg_store r v (\snd local_env)〉.

definition hw_reg_retrieve ≝
 λlocal_env:ertl_reg_env.λreg.
  OK … (hwreg_retrieve … (\snd local_env) reg).

definition ps_arg_retrieve ≝
  λlocal_env,a.
  match a with
  [ Reg r ⇒ ps_reg_retrieve local_env r
  | Imm b ⇒ return b
  ]. 

definition ERTL_state : sem_state_params ≝
  mk_sem_state_params
 (* framesT ≝ *) (list ertl_psd_env)
 (* empty_framesT ≝ *) [ ]
 (* regsT ≝ *) ertl_reg_env
 (* empty_regsT ≝ *) (λsp.〈mk_ertl_psd_env (empty_map …) ∅,init_hw_register_env sp〉).

(* we ignore need_spilled_no as we never move framesize based values around in the
   translation *)
definition ertl_eval_move ≝ λenv,pr.
      ! v ←
        match \snd pr with
        [ Reg src ⇒
          match src with
          [ PSD r ⇒ ps_reg_retrieve env r
          | HDW r ⇒ hw_reg_retrieve env r
          ]
        | Imm bv ⇒ return bv ] ;
      match \fst pr with
      [ PSD r ⇒ ps_reg_store r v env
      | HDW r ⇒ hw_reg_store r v env
      ].

definition ertl_allocate_local ≝
  λreg.λlenv : ertl_reg_env.
  〈set_psd_regs (add … (psd_regs (\fst lenv)) reg BVundef) (\fst lenv), \snd lenv〉.

definition ertl_save_frame:
 cpointer → unit → state … ERTL_state → res (state … ERTL_state) ≝
 λpc.λ_.λst.
  do st ← save_ra … st pc ;
  OK …
   (set_frms ERTL_state (\fst (regs ERTL_state st) :: (st_frms … st))
    (set_regs ERTL_state 〈mk_ertl_psd_env (empty_map …) ∅,\snd (regs … st)〉 st)).

(*CSC: XXXX, for external functions only*)
axiom ertl_fetch_external_args: external_function → state ERTL_state → res (list val).
axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state).
(* I think there should be a list beval in place of list val here
  λvals.λ_.λst.
  (* set all RegisterRets to 0 *)
  let reset ≝ λenv,r.hwreg_store r (BVByte (bv_zero …)) env in
  let env ≝ foldl … reset (\snd (regs … st)) RegisterRets in
  let set_vals ≝ λenv,pr.hwreg_store (\fst pr) (\snd pr) env in ?.
  let env' ≝ foldl … set_vals env (zip_pottier … RegisterRets vals) in
  return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)

definition xdata_pointer_of_address: address → res xpointer ≝
λp.let 〈v1,v2〉 ≝ p in
! p ← pointer_of_bevals [v1;v2] ;
match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = XData) with
[ XData ⇒ λE.OK ? (mk_Sig … p E)
| _ ⇒ λ_.Error … [MSG BadPointer]
] (refl …).

definition address_of_xdata_pointer: xpointer → address ≝
λp.list_to_pair … (bevals_of_pointer p) ?. % qed.

definition get_hwsp : ERTL_state → res xpointer ≝
 λst.
  let spl ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPL in
  let sph ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPH in
  xdata_pointer_of_address 〈spl,sph〉.

definition set_hwsp : xpointer → ERTL_state → ERTL_state ≝
 λsp,st.
  let 〈spl,sph〉 ≝ address_of_xdata_pointer sp in
  let hwregs ≝ hwreg_store RegisterSPL spl (\snd (regs … st)) in
  let hwregs ≝ hwreg_store RegisterSPH sph hwregs in
  set_regs ERTL_state 〈\fst (regs … st),hwregs〉 st.

definition eval_ertl_seq:
 ∀globals. genv ERTL globals →
  ertl_seq → joint_internal_function ERTL globals → ERTL_state →
   IO io_out io_in ERTL_state ≝
 λglobals,ge,stm,curr_fn,st.
 let framesize : Byte ≝ bitvector_of_nat 8 (joint_if_stacksize … curr_fn) in
  match stm with
   [ ertl_new_frame ⇒
      ! sp ← get_hwsp st ;
      let newsp ≝ shift_pointer … sp framesize in
      return set_hwsp newsp st
   | ertl_del_frame ⇒
      ! sp ← get_hwsp st ;
      let newsp ≝ shift_pointer … sp framesize in
      return set_hwsp newsp st
   | ertl_frame_size dst ⇒
      let env ≝ regs … st in
      ! env' ← ps_reg_store dst (BVByte framesize) env ;
      let env'' ≝ 〈add_need_spilled_no dst (\fst env'), \snd env'〉 in
      return set_regs ERTL_state env'' st
   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.  

definition ertl_post_op2 ≝
  λop,dst,arg1,arg2,st.
  let local_env ≝ regs ERTL_state st in
  let f ≝ λarg,st.match arg with
     [ Reg r ⇒
       if r ∈ need_spilled_no (\fst local_env) then
         set_regs ERTL_state 〈add_need_spilled_no dst (\fst local_env),\snd local_env〉 st
       else
         st
     | _ ⇒ st
     ] in
  match op with
  [ Add ⇒ f arg1 (f arg2 st) (* won't happen both *)
  | Addc ⇒ f arg1 (f arg2 st) (* we have to think about what should we do with carry bit *)
  | Sub ⇒ f arg1 st
  | _ ⇒ st].
         

definition ERTL_semantics ≝
  make_sem_graph_params ERTL
  (mk_more_sem_unserialized_params ??
  (* st_pars            ≝ *) ERTL_state
  (* acca_store_        ≝ *) ps_reg_store
  (* acca_retrieve_     ≝ *) ps_reg_retrieve
  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
  (* accb_store_        ≝ *) ps_reg_store
  (* accb_retrieve_     ≝ *) ps_reg_retrieve
  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
  (* dpl_store_         ≝ *) ps_reg_store
  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
  (* dph_store_         ≝ *) ps_reg_store
  (* dph_retrieve_      ≝ *) ps_reg_retrieve
  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
  (* pair_reg_move_     ≝ *) ertl_eval_move
  (* fetch_ra           ≝ *) (load_ra …)
  (* allocate_local     ≝ *) ertl_allocate_local
  (* save_frame         ≝ *) ertl_save_frame
  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
  (* fetch_external_args≝ *) ertl_fetch_external_args
  (* set_result         ≝ *) ertl_set_result
  (* call_args_for_main ≝ *) 0
  (* call_dest_for_main ≝ *) it
  (* read_result        ≝ *) (λ_.λ_.λ_.
     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
  (* eval_ext_seq       ≝ *) eval_ertl_seq
  (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
  (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
  (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st)
  (* post_op2           ≝ *) (λ_.λ_.ertl_post_op2)).