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

definition ps_reg_store ≝
 λr,v.λlocal_env:(register_env beval) × hw_register_env.
  do res ← reg_store r v (\fst local_env) ;
  OK … 〈res, \snd local_env〉.

definition ps_reg_retrieve ≝
 λlocal_env:(register_env beval) × hw_register_env. reg_retrieve … (\fst local_env).

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

definition hw_reg_retrieve ≝
 λlocal_env:(register_env beval) × hw_register_env.λreg.
  OK … (hwreg_retrieve … (\snd local_env) reg).

definition ertl_more_sem_params: more_sem_params ertl_params_ :=
 mk_more_sem_params ertl_params_
  (list (register_env beval)) [] ((register_env beval) × hw_register_env)
   (λsp.〈empty_map …,init_hw_register_env sp〉) 0 it
   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
    ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
     (λlocals,dest_src.
       do v ←
        match \snd dest_src with
        [ pseudo reg ⇒ ps_reg_retrieve locals reg
        | hardware reg ⇒ hw_reg_retrieve locals reg] ;
       match \fst dest_src with
       [ pseudo reg ⇒ ps_reg_store reg v locals
       | hardware reg ⇒ hw_reg_store reg v locals]).
definition ertl_sem_params: sem_params ≝ mk_sem_params … ertl_more_sem_params.

definition ertl_init_locals :
 list register →
  (register_env beval) × hw_register_env → (register_env beval) × hw_register_env ≝
 λlocals,lenv.
  〈foldl … (λlenv,reg. add … lenv reg BVundef) (empty_map …) locals, \snd lenv〉.

(*CSC: could we use here a dependent type to avoid the Error case? *)
axiom EmptyStack: String.
definition ertl_pop_frame:
 ∀globals. genv … (ertl_params globals) → state … ertl_sem_params → res (state … ertl_sem_params) ≝
 λglobals,ge,st.
  let frms ≝ st_frms ? st in
  match frms with
  [ nil ⇒ Error ? [MSG EmptyStack]
  | cons hd tl ⇒
     OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].

definition ertl_save_frame:
 address → nat → nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
 λl.λ_.λ_.λ_.λ_.λst.
  do st ← save_ra … st l ;
  OK …
   (set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st))
    (set_regs ertl_sem_params 〈empty_map …,\snd (regs … st)〉 st)).

definition ertl_result_regs:
 ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list register) ≝
 λglobals,ge,st.
  do fn ← graph_fetch_function … globals ge st ;
  OK … (joint_if_result … fn).

(*CSC: XXXX, for external functions only*)
axiom ertl_fetch_external_args: external_function → state ertl_sem_params → res (list val).
axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params).

definition framesize:
 ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res nat ≝
  λglobals,ge,st.
   do f ← graph_fetch_function … ge st ;
   OK ? (joint_if_stacksize globals … f).

definition get_hwsp : state ertl_sem_params → address ≝
 λst.
  let spl ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPL in
  let sph ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPH in
   〈spl,sph〉.

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

definition ertl_more_sem_params1: ∀globals. more_sem_params1 … (ertl_params globals) ≝
 λglobals.
  mk_more_sem_params1 … ertl_more_sem_params graph_succ_p (graph_pointer_of_label …)
    (graph_fetch_statement …) (load_ra …) (ertl_result_regs …)
    ertl_init_locals ertl_save_frame (ertl_pop_frame …)
    ertl_fetch_external_args ertl_set_result.
definition ertl_sem_params1: ∀globals. sem_params1 globals ≝
 λglobals. mk_sem_params1 … (ertl_more_sem_params1 globals).

definition ertl_exec_extended:
 ∀globals. genv globals (ertl_params globals) →
  ertl_statement_extension → label → state ertl_sem_params →
   IO io_out io_in (trace × (state ertl_sem_params)) ≝
 λglobals,ge,stm,l,st.
  match stm with
   [ ertl_st_ext_new_frame ⇒
      ! v ← framesize globals … ge st;
      let sp ≝ get_hwsp st in
      ! newsp ← addr_sub sp v;
      let st ≝ set_hwsp newsp st in
      ! st ← next … (ertl_sem_params1 globals) l st ;
        return 〈E0,st〉
   | ertl_st_ext_del_frame ⇒
      ! v ← framesize … ge st;
      let sp ≝ get_hwsp st in
      ! newsp ← addr_add sp v;
      let st ≝ set_hwsp newsp st in
      ! st ← next … (ertl_sem_params1 …) l st ;
        return 〈E0,st〉
   | ertl_st_ext_frame_size dst ⇒
      ! v ← framesize … ge st;
      ! st ← greg_store ertl_sem_params dst (BVByte (bitvector_of_nat … v)) st;
      ! st ← next … (ertl_sem_params1 …) l st ;
        return 〈E0, st〉
   ].

definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
 λglobals. mk_more_sem_params2 … (ertl_more_sem_params1 …) (ertl_exec_extended …).

definition ertl_fullexec: fullexec io_out io_in ≝
 joint_fullexec … (λp. ertl_more_sem_params2 (prog_var_names … p)).