include "joint/semanticsUtils_paolo.ma".
include "RTL/RTL_paolo.ma". (* CSC: syntax.ma in RTLabs *)
include alias "common/Identifiers.ma".
include alias "ASM/Util.ma".

record frame: Type[0] ≝
 { fr_ret_regs: list register
 ; fr_pc: address
 ; fr_sp: pointer
 ; fr_carry: beval
 ; fr_regs: register_env beval
 }.

definition rtl_sem_state_params : sem_state_params ≝
  mk_sem_state_params
    (list frame)
    [ ]
    (register_env beval)
    (λ_.empty_map …).

definition rtl_arg_retrieve : ?→?→res ? ≝ λenv.λa : rtl_argument.
  match a with
  [ Reg r ⇒ reg_retrieve env r
  | Imm b ⇒ return (BVByte b)
  ].

(*CSC: could we use here a dependent type to avoid the Error case? *)
axiom EmptyStack: String.
axiom OutOfBounds: String.

definition rtl_fetch_ra:
 state rtl_sem_state_params → res ((state rtl_sem_state_params) × address) ≝
 λst.
  match st_frms ? st with
  [ nil ⇒ Error ? [MSG EmptyStack]
  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].

definition rtl_init_locals :
 list register → register_env beval → register_env beval ≝
 λlocals,env.
  foldl ?? (λlenv,reg. add … lenv reg BVundef) env locals.


definition rtl_setup_call:
 nat → list register → list rtl_argument → state rtl_sem_state_params → res (state rtl_sem_state_params) ≝
  λstacksize,formal_arg_regs,actual_arg_regs,st.
  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
  do new_regs ←
   mfold_left2 …
    (λlenv,dest,src.
      do v ← rtl_arg_retrieve … (regs ? st) src ;
      OK … (add … lenv dest v))
    (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
  OK …
   (set_regs rtl_sem_state_params new_regs
    (set_m … mem
     (set_sp … (mk_pointer XData b ? (mk_offset 0)) st))).
cases b * #r #off #E >E %
qed.

definition rtl_save_frame ≝ λl.λretregs.λst : state rtl_sem_state_params.
  let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in
  set_frms rtl_sem_state_params frame st.  

(*CSC: XXXX, for external functions only*)
axiom rtl_fetch_external_args: external_function → state rtl_sem_state_params → res (list val).
axiom rtl_set_result: list val → state rtl_sem_state_params → res (state rtl_sem_state_params).

definition rtl_msu_params :
  more_sem_unserialized_params rtl_uns_params ≝
 mk_more_sem_unserialized_params rtl_uns_params rtl_sem_state_params
    reg_store reg_retrieve rtl_arg_retrieve
    reg_store reg_retrieve rtl_arg_retrieve
    reg_store reg_retrieve rtl_arg_retrieve
    reg_store reg_retrieve rtl_arg_retrieve
    rtl_arg_retrieve
    (λenv,p. let 〈dest,src〉 ≝ p in
      ! v ← rtl_arg_retrieve env src ;
      reg_store dest v env)
    rtl_fetch_ra
    rtl_init_locals
    rtl_save_frame
    rtl_setup_call
    rtl_fetch_external_args
    rtl_set_result
    [ ] [ ] (*dummy*).

(* alias *)
definition rtl_reg_store : register→beval→state rtl_sem_state_params→
    res (state rtl_sem_state_params) ≝ acca_store ? rtl_msu_params.
definition rtl_reg_retrieve : state rtl_sem_state_params→register→res beval ≝
    acca_retrieve ? rtl_msu_params.

definition rtl_read_result :
 ∀globals. genv globals rtl_params → state rtl_sem_state_params → res (list beval) ≝
 λglobals,ge,st.
  ! p ← code_pointer_of_address (pc … st) ;
  ! fn ← fetch_function … ge p ;
  m_mmap … (rtl_reg_retrieve st) (joint_if_result … fn).

(*CSC: we could use a dependent type here: the list of return values should have
  the same length of the list of return registers that store the values. This
  saves the OutOfBounds exception *)
definition rtl_pop_frame:
 ∀globals. genv globals rtl_params → state rtl_sem_state_params →
  res (state rtl_sem_state_params) ≝
 λglobals,ge,st.
  do ret_vals ← rtl_read_result … ge st ;
  match st_frms ? st with
  [ nil ⇒ Error ? [MSG EmptyStack]
  | cons hd tl ⇒
     do st ←
      mfold_left_i …
       (λi.λst.λreg.
         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
         rtl_reg_store reg v st)
       (OK … st) (fr_ret_regs hd) ;
     OK …
      (set_frms rtl_sem_state_params tl
        (set_regs rtl_sem_state_params (fr_regs hd)
         (set_sp … (fr_sp hd)
          (set_carry … (fr_carry hd)
           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].


(* This code is quite similar to eval_call_block: can we factorize it out? *)
definition eval_tail_call_block:
 ∀globals.genv globals rtl_params → state rtl_sem_state_params →
  block → call_args rtl_uns_params → IO io_out io_in (trace×(state rtl_sem_state_params)) ≝
 λglobals,ge,st,b,args.
  ! 〈next, tr, st〉 ← eval_call_block_preamble ? rtl_params rtl_msu_params ge st b args (None ?) ;
  match next with
  [ None ⇒ (* Paolo: external tailcall, copied from evaluation of return, is it right? *)
    ! 〈st,ra〉 ← fetch_ra … st ;
    ! st ← rtl_pop_frame … ge st;
    return 〈tr,st〉
  | Some lbl ⇒
    return 〈tr,st〉
  ].

definition block_of_register_pair: register → register → state rtl_sem_state_params → res block ≝
 λr1,r2,st.
 do v1 ← rtl_reg_retrieve st r1 ;
 do v2 ← rtl_reg_retrieve st r2 ;
 do ptr ← pointer_of_address 〈v1,v2〉 ;
 OK … (pblock ptr).  

definition rtl_exec_extended:
 ∀globals. genv globals rtl_params →
  rtl_instruction_extension → state rtl_sem_state_params → address →
   IO io_out io_in ((option (label)) × trace × (state rtl_sem_state_params)) ≝
 λglobals,ge,stm,st,next_addr.
  match stm with
   [ rtl_st_ext_stack_address dreg1 dreg2  ⇒
      let sp ≝ sp ? st in
      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
      ! st ← rtl_reg_store dreg1 dpl st ;
      ! st ← rtl_reg_store dreg2 dph st ;
      return 〈None label,E0, st〉
   | rtl_st_ext_call_ptr r1 r2 args dest ⇒
     ! b ← block_of_register_pair r1 r2 st : IO ???;
     eval_call_block_preamble ? rtl_params rtl_msu_params
                              ge st b args (Some ? 〈dest,next_addr〉) ].

definition rtl_exec_fin_extended:
 ∀globals. genv globals rtl_params →
  rtl_statement_extension → state rtl_sem_state_params →
   IO io_out io_in (trace × (state rtl_sem_state_params)) ≝
   λglobals,ge,stm,st.
   match stm with
   [ rtl_st_ext_tailcall_id id args ⇒
      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
      eval_tail_call_block … ge st b args
   | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
      ! b ← block_of_register_pair r1 r2 st : IO ???;
      eval_tail_call_block … ge st b args
   ].

definition rtl_msg_params : more_sem_genv_params rtl_params ≝
  mk_more_sem_genv_params rtl_params rtl_msu_params
    rtl_read_result
    rtl_exec_extended
    rtl_exec_fin_extended
    rtl_pop_frame.



definition rtl_sem_params : sem_params ≝ make_sem_graph_params … rtl_msg_params.

definition rtl_fullexec ≝ joint_fullexec … rtl_sem_params.