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: cpointer
 ; fr_sp: xpointer
 ; fr_carry: beval
 ; fr_regs: register_env beval
 }.

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

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

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

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

definition rtl_init_local :
 register → register_env beval → register_env beval ≝
 λlocal,env.add … env local BVundef.

definition rtl_setup_call:
 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
  λ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_state new_regs
    (set_m … mem
     (set_sp … (mk_pointer b (mk_offset (bv_zero …))) st))).
cases b * #r #off #E >E %
qed.

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

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

definition rtl_reg_store ≝ λr,v,st.! mem ← reg_store r v (regs RTL_state st) ; return set_regs RTL_state mem st.
definition rtl_reg_retrieve ≝ λst.reg_retrieve (regs RTL_state st).

definition rtl_read_result :
 ∀globals.genv RTL globals → list register → RTL_state → res (list beval) ≝
 λglobals,ge,rets,st.
 m_list_map … (rtl_reg_retrieve st) rets.

(*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 RTL globals → joint_internal_function RTL globals → RTL_state →
  res RTL_state ≝
 λglobals,ge,curr_fn,st.
  let ret ≝ joint_if_result … curr_fn in
  do ret_vals ← rtl_read_result … ge ret 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_state tl
        (set_regs RTL_state (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_tailcall_block:
 ∀globals.genv RTL globals → RTL_state →
  block → call_args RTL →
  (* this is where the result of the current function should be stored *)
  call_dest RTL →
  IO io_out io_in
    ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×RTL_state) ≝
 λglobals,ge,st,b,args,ret.
  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?); 
    match fd with
    [ Internal fd ⇒
      return 〈FTailInit ?? (block_id b) fd args, st〉
    | External fn ⇒
      ! params ← rtl_fetch_external_args … fn st : IO ???;
      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
      (* CSC: XXX bug here; I think I should split it into Byte-long
         components; instead I am making a singleton out of it. To be
         fixed once we fully implement external functions. *)
      let vs ≝ [mk_val ? evres] in
      ! st ← rtl_set_result … vs ret st : IO ???;
      return 〈FEnd2 ??, st〉
    ].

definition block_of_register_pair: register → register → RTL_state → 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 eval_rtl_seq:
 ∀globals. genv RTL globals →
  rtl_seq → joint_internal_function RTL globals → RTL_state →
   IO io_out io_in RTL_state ≝
 λglobals,ge,stm,curr_fn,st.
  match stm with
   [ rtl_stack_address dreg1 dreg2  ⇒
      let sp ≝ sp ? st in
      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
      ! st ← rtl_reg_store dreg1 dpl st ;
      rtl_reg_store dreg2 dph st
   ].

definition eval_rtl_call:
 ∀globals. genv RTL globals →
  rtl_call → RTL_state →
   IO io_out io_in ((step_flow RTL ? Call)×RTL_state) ≝
 λglobals,ge,stm,st.
  match stm with
  [ rtl_call_ptr r1 r2 args dest ⇒
    ! b ← block_of_register_pair r1 r2 st : IO ???;
    ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?); 
    match fd with
    [ Internal fd ⇒
      return 〈Init ?? (block_id b) fd args dest, st〉
    | External fn ⇒
      ! params ← rtl_fetch_external_args … fn st : IO ???;
      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
      (* CSC: XXX bug here; I think I should split it into Byte-long
         components; instead I am making a singleton out of it. To be
         fixed once we fully implement external functions. *)
      let vs ≝ [mk_val ? evres] in
      ! st ← rtl_set_result … vs dest st : IO ???;
      return 〈Proceed ???, st〉
    ]
  ].

definition eval_rtl_tailcall:
 ∀globals. genv RTL globals →
  rtl_tailcall → joint_internal_function RTL globals → RTL_state →
   IO io_out io_in ((fin_step_flow RTL ? Call)×RTL_state) ≝
   λglobals,ge,stm,curr_fn,st.
   let ret ≝ joint_if_result … curr_fn in
   match stm with
   [ rtl_tailcall_id id args ⇒
      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
      eval_tailcall_block … ge st b args ret
   | rtl_tailcall_ptr r1 r2 args ⇒
      ! b ← block_of_register_pair r1 r2 st : IO ???;
      eval_tailcall_block … ge st b args ret
   ].

definition RTL_semantics ≝
  make_sem_graph_params RTL
    (mk_more_sem_unserialized_params ??
      RTL_state
      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_local
      rtl_save_frame
      rtl_setup_call
      rtl_fetch_external_args
      rtl_set_result
      [ ] [ ]
      rtl_read_result
      eval_rtl_seq
      eval_rtl_tailcall
      eval_rtl_call
      rtl_pop_frame
      (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)).