source: src/RTL/RTL_semantics.ma @ 3096

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

(* we design here three different semantics of RTL, which differ on how stack
   is treated.
   
   1) the first, RTL_semantics_separate, allocates a new stack for each
      function call, behaving like RTLabs. Each separate stack is finite
      (offsets are bounded by 2^16), but the number of stacks is unbounded
   2) the second, RTL_semantics_separate_overflow, behaves like the previous one,
      but is defined to fail on stack overflow. The idea is that we use the
      hypothesis of not stack overflowing to pass from RTL_semantics_separate to
      RTL_semantics_separate_overflow, without having to trasnform the states in
      any way
   3) the third, RTL_semantics_unique, behaves like ERTL and later languages:
      the stack is unique (allocation happens once in make_initial_state, see
      joint/Traces.ma). However the proof that allows passing from
      RTL_semantics_separate_overflow to RTL_semantics_unique should not
      rely on any hypothesis about stack usage

*)

record reg_sp : Type[0] ≝
{ reg_sp_env :> identifier_map RegisterTag beval
; stackp : xpointer
}.

definition reg_sp_store ≝ λreg,v,locals.
let locals' ≝ reg_store reg v (reg_sp_env locals) in
mk_reg_sp locals' (stackp locals).

definition reg_sp_retrieve ≝ λlocals : reg_sp.reg_retrieve locals.

definition reg_sp_empty ≝ mk_reg_sp (empty_map …).
(*** Store/retrieve on hardware registers ***)

record frame: Type[0] ≝
 { fr_ret_regs: list register
 ; fr_pc: program_counter
 ; fr_carry: bebit
 ; fr_regs: reg_sp
 }.

definition RTL_state_params : sem_state_params ≝
  mk_sem_state_params
    (list frame)
    [ ]
    reg_sp
    reg_sp_empty
    (λenv.OK … (stackp env))
    (λenv.mk_reg_sp env (* coercion*)).

definition RTL_state ≝ state RTL_state_params.

unification hint 0 ≔ X ⊢ register_env X ≡ identifier_map RegisterTag X.

definition rtl_arg_retrieve : reg_sp → psd_argument → res beval ≝
  λenv.λa : psd_argument.
  match a with
  [ Reg r ⇒ reg_retrieve env r
  | Imm b ⇒ OK … (BVByte b)
  ].

(*CSC: could we use here a dependent type to avoid the Error case? *)
definition rtl_fetch_ra:
 RTL_state → res (RTL_state × program_counter) ≝
 λst.
 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
   match frms with
  [ nil ⇒ Error ? [MSG EmptyStack]
  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉
  ].

definition rtl_init_local :
 register → reg_sp → reg_sp ≝
 λlocal.reg_sp_store … local BVundef.

lemma Zlt_to_not_Zle : ∀z1,z2 : Z.z1 < z2 → z2 ≰ z1.
#z1 #z2 #H % #G
lapply (Zlt_to_Zle_to_Zlt … H G) #ABS @(absurd ? ABS ?) @irreflexive_Zlt
qed.

definition rtl_setup_call_separate :
 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
  λstacksize,formal_arg_regs,actual_arg_regs,st.
  let 〈mem,b〉 as E ≝ alloc … (m … st) 0 stacksize in
  let sp ≝ mk_pointer b (mk_offset (bv_zero …)) in
  do new_regs ←
   mfold_left2 …
    (λlenv,dest,src.
      do v ← rtl_arg_retrieve … (regs ? st) src ;
      OK … (reg_sp_store dest v lenv))
    (OK … (reg_sp_empty sp)) formal_arg_regs actual_arg_regs ;
  OK …
   (set_regs RTL_state_params new_regs
    (set_m … mem st)).
@hide_prf
whd in match sp; -sp
cases (m ??) in E; #m #next #prf
whd in ⊢ (???%→?); #EQ destruct
whd in ⊢ (??%?); @Zleb_elim_Type0 [2: #_ %]
#abs cases (absurd ? abs ?) @Zlt_to_not_Zle assumption
qed.

definition rtl_setup_call_separate_overflow :
 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
  λstacksize,formal_arg_regs,actual_arg_regs,st.
  (* using nats is highly inefficient... *)
  if leb (S (stacksize + stack_usage … st)) (2^16) then
    rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st
  else Error … [MSG StackOverflow].

definition rtl_setup_call_unique :
 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
  λstacksize,formal_arg_regs,actual_arg_regs,st.
  ! sp ← sp … st ; (* always succeeds in RTL *)
  let newsp ≝ neg_shift_pointer … sp (bitvector_of_nat 8 stacksize) in
  do new_regs ←
   mfold_left2 …
    (λlenv,dest,src.
      do v ← rtl_arg_retrieve … (regs ? st) src ;
      OK … (reg_sp_store dest v lenv))
    (OK … (reg_sp_empty newsp)) formal_arg_regs actual_arg_regs ;
  OK …
   (set_regs RTL_state_params new_regs st).
@(pi2 … sp) qed.

definition RTL_state_pc ≝ state_pc RTL_state_params.

unification hint 0 ≔ ⊢ RTL_state ≡ state RTL_state_params.
unification hint 0 ≔ ⊢ RTL_state_pc ≡ state_pc RTL_state_params.

definition rtl_save_frame ≝ λretregs.λst : RTL_state_pc.
 ! frms ← opt_to_res … [MSG … FrameErrorOnPush] (st_frms … st) ;
 let frame ≝ mk_frame retregs (pc ? st) (carry ? st) (regs ? st) :: frms in
  OK … (set_frms RTL_state_params frame st).

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

definition rtl_reg_store ≝ λr,v,st.
  let mem ≝ reg_sp_store r v (regs RTL_state_params st) in
  set_regs RTL_state_params mem st.

definition rtl_reg_retrieve ≝ λst,l.reg_sp_retrieve (regs RTL_state_params st) l.

definition rtl_read_result :
 list register → RTL_state → res (list beval) ≝
 λ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_separate:
 list register → RTL_state →
  res (RTL_state × program_counter) ≝
 λret,st.
 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
 match frms with
  [ nil ⇒ Error ? [MSG EmptyStack]
  | cons hd tl ⇒
    ! ret_vals ← rtl_read_result … ret st ;
    (* Paolo: no more OutOfBounds exception, but is it right? should be for
       compiled programs *)
    let reg_vals ≝ zip_pottier … (fr_ret_regs hd) ret_vals in
    ! sp ← sp … st ;  (* always succeeds in RTL *)
    let st ≝ set_frms RTL_state_params tl
        (set_regs RTL_state_params (fr_regs hd) (* <- this resets the sp too *)
          (set_carry RTL_state_params (fr_carry hd)
            (set_m … (free … (m … st) (pblock sp)) st))) in
    let pc ≝ fr_pc hd in
    let st ≝ foldl …
      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
      st reg_vals in
    return 〈st, pc〉
  ].

(* as the stack pointer is reobtained from the frame, there is no need
   to shift it back into position. We still need to avoid freeing
   the memory *)
definition rtl_pop_frame_unique:
 list register → RTL_state →
  res (RTL_state × program_counter) ≝
 λret,st.
 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
 match frms with
  [ nil ⇒ Error ? [MSG EmptyStack]
  | cons hd tl ⇒
    ! ret_vals ← rtl_read_result … ret st ;
    (* Paolo: no more OutOfBounds exception, but is it right? should be for
       compiled programs *)
    let reg_vals ≝ zip_pottier … (fr_ret_regs hd) ret_vals in
    ! sp ← sp … st ;  (* always succeeds in RTL *)
    let st ≝ set_frms RTL_state_params tl
        (set_regs RTL_state_params (fr_regs hd) (* <- this resets the sp too *)
          (set_carry RTL_state_params (fr_carry hd) st)) in
    let pc ≝ fr_pc hd in
    let st ≝ foldl …
      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
      st reg_vals in
    return 〈st, pc〉
  ].

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:
  rtl_seq → ident → RTL_state →
   res RTL_state ≝
 λstm,curr_fn,st.
  match stm with
   [ rtl_stack_address dreg1 dreg2  ⇒
      ! sp ← sp ? st ; (* always succeeds in RTL *)
      let 〈dpl,dph〉 ≝ beval_pair_of_pointer sp in
      let st ≝ rtl_reg_store dreg1 dpl st in
      return rtl_reg_store dreg2 dph st
   ].

(* for a store living in res *)
definition reg_res_store ≝ λr,v,s.OK ? (reg_sp_store r v s).

definition RTL_semantics_separate ≝
  mk_sem_graph_params RTL
    (λF.mk_sem_unserialized_params RTL F
      RTL_state_params
      reg_res_store reg_sp_retrieve rtl_arg_retrieve
      reg_res_store reg_sp_retrieve rtl_arg_retrieve
      reg_res_store reg_sp_retrieve rtl_arg_retrieve
      reg_res_store reg_sp_retrieve rtl_arg_retrieve
      rtl_arg_retrieve
      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
        ! v ← rtl_arg_retrieve env src ;
        return reg_sp_store dest v env)
      (λ_.rtl_save_frame)
      rtl_setup_call_separate
      rtl_fetch_external_args
      rtl_set_result
      [ ]
      [an_identifier … one ; an_identifier … (p0 one) ;
       an_identifier … (p1 one) ; an_identifier … (p0 (p0 one)) ]
      (λ_.λ_.rtl_read_result)  
      (λ_.λ_.eval_rtl_seq)
      (λ_.λ_.λ_.rtl_pop_frame_separate))
    RTL_premain.

definition RTL_semantics_separate_overflow ≝
  mk_sem_graph_params RTL
    (λF.mk_sem_unserialized_params RTL F
      RTL_state_params
      reg_res_store reg_sp_retrieve rtl_arg_retrieve
      reg_res_store reg_sp_retrieve rtl_arg_retrieve
      reg_res_store reg_sp_retrieve rtl_arg_retrieve
      reg_res_store reg_sp_retrieve rtl_arg_retrieve
      rtl_arg_retrieve
      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
        ! v ← rtl_arg_retrieve env src ;
        return reg_sp_store dest v env)
      (λ_.rtl_save_frame)
      rtl_setup_call_separate_overflow
      rtl_fetch_external_args
      rtl_set_result
      [ ]
      [an_identifier … one ; an_identifier … (p0 one) ;
       an_identifier … (p1 one) ; an_identifier … (p0 (p0 one)) ]
      (λ_.λ_.rtl_read_result)  
      (λ_.λ_.eval_rtl_seq)
      (λ_.λ_.λ_.rtl_pop_frame_separate))
    RTL_premain.

definition RTL_semantics_unique ≝
  mk_sem_graph_params RTL
    (λF.mk_sem_unserialized_params RTL F
      RTL_state_params
      reg_res_store reg_sp_retrieve rtl_arg_retrieve
      reg_res_store reg_sp_retrieve rtl_arg_retrieve
      reg_res_store reg_sp_retrieve rtl_arg_retrieve
      reg_res_store reg_sp_retrieve rtl_arg_retrieve
      rtl_arg_retrieve
      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
        ! v ← rtl_arg_retrieve env src ;
        return reg_sp_store dest v env)
      (λ_.rtl_save_frame)
      rtl_setup_call_unique
      rtl_fetch_external_args
      rtl_set_result
      [ ]
      [an_identifier … one ; an_identifier … (p0 one) ;
       an_identifier … (p1 one) ; an_identifier … (p0 (p0 one)) ]
      (λ_.λ_.rtl_read_result)  
      (λ_.λ_.eval_rtl_seq)
      (λ_.λ_.λ_.rtl_pop_frame_unique))
    RTL_premain.