Ignore:
Timestamp:
May 9, 2013, 12:49:38 AM (6 years ago)
Author:
piccolo
Message:

changed ERTL semantics:
1) added manipulation of stack pointer directly in the semantics
2) added values of Callee Saved in frames

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_semantics.ma

    r2946 r3259  
    3434definition set_hwsp : ertl_reg_env → xpointer → ertl_reg_env ≝
    3535 λst,sp.〈\fst st, hwreg_store_sp (\snd st) sp〉.
     36 
     37record ERTL_frame : Type[0] ≝
     38{ psd_reg_env : register_env beval
     39; funct_block : Σb:block.block_region b=Code
     40; callee_values : Σl : list beval. |l| = |RegisterCalleeSaved|
     41}.
    3642
    3743definition ERTL_state : sem_state_params ≝
    3844  mk_sem_state_params
    39  (* framesT ≝ *) (list (register_env beval × (Σb:block.block_region b=Code)))
     45 (* framesT ≝ *) (list (ERTL_frame))
    4046 (* empty_framesT ≝ *) [ ]
    4147 (* regsT ≝ *) ertl_reg_env
     
    4652(* we ignore need_spilled_no as we never move framesize based values around in the
    4753   translation *)
    48 definition ertl_eval_move ≝ λenv,pr.
     54definition ertl_eval_move ≝ λenv.λpr : move_dst × move_src.
    4955      ! v ←
    5056        match \snd pr with
     
    6975  ! st' ← push_ra … st (pc … st) ;
    7076  ! frms ← opt_to_res ? [MSG FrameErrorOnPush] (st_frms … st');
     77  let callee_val ≝ map … (λr.hwreg_retrieve (\snd (regs …  st')) r)
     78                    RegisterCalleeSaved in
    7179  return
    7280  (set_frms ERTL_state
    73   (〈\fst (regs ERTL_state st'),(pc_block (pc ? st))〉 :: frms)
     81  ((mk_ERTL_frame (\fst (regs ERTL_state st')) (pc_block (pc ? st))
     82      «callee_val,length_map … ») :: frms)
    7483    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
    7584
     85definition callee_values_ok : hw_register_env →
     86   (Σl : list beval.|l| = |RegisterCalleeSaved|) → bool ≝
     87λregs,l.
     88foldl … andb true
     89 (map2 … (λr : Register.λbv :beval.eq_beval (hwreg_retrieve regs r) bv)
     90  RegisterCalleeSaved l ?).
     91@hide_prf >(pi2 … l) % qed.
     92
     93
    7694definition ertl_pop_frame:
    77  state ERTL_state →
     95 ∀F. ∀globals. genv_gen F globals → ident →  state ERTL_state →
    7896   res (state ERTL_state × program_counter) ≝
    79  λst.
     97 λF,globals,ge,id,st.
    8098 ! frms ← opt_to_res ? [MSG FrameErrorOnPop] (st_frms … st);
    8199 match frms with
    82100 [ nil ⇒ Error ? [MSG FramesEmptyOnPop]
    83101 | cons hd tl ⇒
    84    let 〈local_mem, bl〉 ≝ hd in
    85    let st' ≝ set_regs ERTL_state 〈local_mem, \snd (regs … st)〉
    86       (set_frms ERTL_state tl st) in
    87    ! 〈st'', pc〉 ← pop_ra … st' ;
    88    if eq_block bl (pc_block pc) then
    89      OK … 〈st'', pc〉
    90    else Error ? [MSG BlockInFramesCorrupted]
     102   if callee_values_ok (\snd (regs … st)) (callee_values hd) then
     103    let st' ≝ set_regs ERTL_state 〈(psd_reg_env hd), \snd (regs … st)〉
     104       (set_frms ERTL_state tl st) in
     105    ! 〈st'', pc〉 ← pop_ra … st' ;
     106    if eq_block (funct_block hd) (pc_block pc) then
     107      ! sp ← sp … st'' ;
     108      ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
     109      let framesize : Byte ≝ bitvector_of_nat 8 framesize in
     110      let newsp ≝ shift_pointer … sp framesize in
     111      OK … 〈set_sp … newsp st'', pc〉
     112    else Error ? [MSG BlockInFramesCorrupted]
     113   else Error ? [MSG BadRegister]
    91114 ].
     115@hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.
    92116
    93117(*CSC: XXXX, for external functions only*)
     
    112136  return set_regs ERTL_state env' st.
    113137
     138
     139definition ertl_setup_call : ∀F. ∀globals. genv_gen F globals →
     140ident → state ERTL_state → res (state ERTL_state) ≝
     141λF,globals,ge,id,st.
     142  ! sp ← sp … st ;
     143  ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
     144  let framesize : Byte ≝ bitvector_of_nat 8 framesize in
     145  let newsp ≝ neg_shift_pointer … sp framesize in
     146  return set_sp … newsp st.
     147@hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.
     148 
     149definition eval_ertl_seq:
     150 ∀F. ∀globals. genv_gen F globals →
     151  ertl_seq → ident → state ERTL_state →
     152   res (state ERTL_state) ≝
     153 λF,globals,ge,stm,id,st.
     154 ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
     155 let framesize : Byte ≝ bitvector_of_nat 8 framesize in
     156   match stm with
     157   [ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st].
     158   
     159(*
    114160definition eval_ertl_seq:
    115161 ∀F. ∀globals. genv_gen F globals →
     
    129175      return set_sp … newsp st
    130176   | ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st
    131    ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed. 
     177   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.  *)
    132178
    133179definition ERTL_sem_uns ≝ 
     
    149195  (* pair_reg_move_     ≝ *) ertl_eval_move
    150196  (* save_frame         ≝ *) ertl_save_frame
    151   (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
     197  (* setup_call         ≝ *) (λgl,ge.λ_.λ_.λ_.λid,st.ertl_setup_call F gl ge id st)
    152198  (* fetch_external_args≝ *) ertl_fetch_external_args
    153199  (* set_result         ≝ *) ertl_set_result
     
    157203     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    158204  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.eval_ertl_seq F gl ge stm id)
    159   (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.ertl_pop_frame).
     205  (* pop_frame          ≝ *) (λglobals,ge,id.λ_.λst.ertl_pop_frame F globals ge id st).
    160206
    161207definition ERTL_semantics ≝
Note: See TracChangeset for help on using the changeset viewer.