Changeset 2590 for src/ERTL


Ignore:
Timestamp:
Jan 24, 2013, 7:52:38 PM (8 years ago)
Author:
piccolo
Message:

added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc case in place in ERTLptr translation

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r2566 r2590  
    33include alias "common/Identifiers.ma".
    44
    5 record ertl_psd_env : Type[0] ≝
    6   { psd_regs : register_env beval
    7   (* this tells what pseudo-registers should have their value corrected by spilled_no *)
    8   ; need_spilled_no : identifier_set RegisterTag
    9   }.
    10 
    11 definition set_psd_regs ≝ λx,env.mk_ertl_psd_env x (need_spilled_no env).
    12 definition add_need_spilled_no ≝
    13   λr,env.mk_ertl_psd_env (psd_regs env) (add_set … (need_spilled_no env) r).
    14 definition rm_need_spilled_no ≝
    15   λr,env.mk_ertl_psd_env (psd_regs env) (need_spilled_no env ∖  {(r)}).
    16 
    17 definition ertl_reg_env ≝ ertl_psd_env × hw_register_env.
     5definition ertl_reg_env ≝ register_env beval × hw_register_env.
    186
    197definition ps_reg_store: ? → ? → ? → res ? ≝
    208 λr,v.λlocal_env : ertl_reg_env.
    21   do res ← reg_store r v (psd_regs (\fst local_env)) ;
    22   let psd_env ≝ set_psd_regs res (\fst local_env) in
    23   OK … 〈rm_need_spilled_no r psd_env, \snd local_env〉.
     9  do res ← reg_store r v (\fst local_env) ;
     10  OK … 〈res, \snd local_env〉.
    2411
    2512definition ps_reg_retrieve ≝
    26  λlocal_env:ertl_reg_env. reg_retrieve … (psd_regs (\fst local_env)).
     13 λlocal_env:ertl_reg_env. reg_retrieve … (\fst local_env).
    2714
    2815definition hw_reg_store ≝
     
    4229  ].
    4330
     31definition get_hwsp : ertl_reg_env → res xpointer ≝
     32 λst.hwreg_retrieve_sp (\snd st).
    4433
     34definition set_hwsp : ertl_reg_env → xpointer → ertl_reg_env ≝
     35 λst,sp.〈\fst st, hwreg_store_sp (\snd st) sp〉.
    4536
    4637definition ERTL_state : sem_state_params ≝
    4738  mk_sem_state_params
    48  (* framesT ≝ *) (list ertl_psd_env)
     39 (* framesT ≝ *) (list (register_env beval × ident))
    4940 (* empty_framesT ≝ *) [ ]
    5041 (* regsT ≝ *) ertl_reg_env
    51  (* empty_regsT ≝ *) (λsp.〈mk_ertl_psd_env (empty_map …) ∅,init_hw_register_env sp〉)
    52  (*load_sp ≝ *) ?
    53   (*save_sp ≝ *) ?. cases daemon qed.
     42 (* empty_regsT ≝ *) (λsp.〈empty_map …,init_hw_register_env sp〉)
     43 (*load_sp ≝ *) get_hwsp
     44 (*save_sp ≝ *) set_hwsp.
    5445
    5546(* we ignore need_spilled_no as we never move framesize based values around in the
     
    7162definition ertl_allocate_local ≝
    7263  λreg.λlenv : ertl_reg_env.
    73   〈set_psd_regs (add … (psd_regs (\fst lenv)) reg BVundef) (\fst lenv), \snd lenv〉.
     64  〈 add … (\fst lenv) reg BVundef, \snd lenv〉.
     65
    7466
    7567definition ertl_save_frame:
    76  call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝
    77  λ_.λ_.λst.
     68 call_kind → unit → ident → state_pc ERTL_state → res (state … ERTL_state) ≝
     69 λ_.λ_.λid.λst.
    7870  do st ← push_ra … st (pc … st) ;
    7971  OK …
    80    (set_frms ERTL_state (\fst (regs ERTL_state st) :: (st_frms … st))
    81     (set_regs ERTL_state 〈mk_ertl_psd_env (empty_map …) ∅,\snd (regs … st)〉 st)).
     72   (set_frms ERTL_state (〈\fst (regs ERTL_state st),id〉 :: (st_frms … st))
     73    (set_regs ERTL_state 〈empty_map …,\snd (regs … st)〉 st)).
    8274
    8375(*CSC: XXXX, for external functions only*)
     
    9385  return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)
    9486
    95 definition xdata_pointer_of_address: address → res xpointer ≝
    96 λp.let 〈v1,v2〉 ≝ p in
    97 ! p ← pointer_of_bevals [v1;v2] ;
    98 match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = XData) with
    99 [ XData ⇒ λE.OK ? (mk_Sig … p E)
    100 | _ ⇒ λ_.Error … [MSG BadPointer]
    101 ] (refl …).
    102 
    103 definition address_of_xdata_pointer: xpointer → address ≝
    104 λp.list_to_pair … (bevals_of_pointer p) ?. % qed.
    105 
    106 definition get_hwsp : state ERTL_state → res xpointer ≝
    107  λst.
    108   let spl ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPL in
    109   let sph ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPH in
    110   xdata_pointer_of_address 〈spl,sph〉.
    111 
    112 definition set_hwsp : xpointer → state ERTL_state → state ERTL_state ≝
    113  λsp,st.
    114   let 〈spl,sph〉 ≝ address_of_xdata_pointer sp in
    115   let hwregs ≝ hwreg_store RegisterSPL spl (\snd (regs … st)) in
    116   let hwregs ≝ hwreg_store RegisterSPH sph hwregs in
    117   set_regs ERTL_state 〈\fst (regs … st),hwregs〉 st.
    118 
    11987axiom FunctionNotFound: errmsg.
    12088
     
    12694  let env ≝ regs … st in
    12795  ! env' ← ps_reg_store dst v env ;
    128   let env'' ≝ 〈add_need_spilled_no dst (\fst env'), \snd env'〉 in
    129   return set_regs ERTL_state env'' st.
     96  return set_regs ERTL_state env' st.
    13097
    13198definition eval_ertl_seq:
     
    138105  match stm with
    139106   [ ertl_new_frame ⇒
    140       ! sp ← get_hwsp st ;
     107      ! sp ← sp … st ;
    141108      let newsp ≝ shift_pointer … sp framesize in
    142       return set_hwsp newsp st
     109      return set_sp … newsp st
    143110   | ertl_del_frame ⇒
    144       ! sp ← get_hwsp st ;
     111      ! sp ← sp … st ;
    145112      let newsp ≝ shift_pointer … sp framesize in
    146       return set_hwsp newsp st
     113      return set_sp … newsp st
    147114   | ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st
    148115   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed. 
    149 
    150 definition ertl_post_op2 ≝
    151   λop,dst,arg1,arg2,st.
    152   let local_env ≝ regs ERTL_state st in
    153   let f ≝ λarg,st.match arg with
    154      [ Reg r ⇒
    155        if r ∈ need_spilled_no (\fst local_env) then
    156          set_regs ERTL_state 〈add_need_spilled_no dst (\fst local_env),\snd local_env〉 st
    157        else
    158          st
    159      | _ ⇒ st
    160      ] in
    161   match op with
    162   [ Add ⇒ f arg1 (f arg2 st) (* won't happen both *)
    163   | Addc ⇒ f arg1 (f arg2 st) (* we have to think about what should we do with carry bit *)
    164   | Sub ⇒ f arg1 st
    165   | _ ⇒ st].
    166116         
    167117definition ERTL_semantics ≝
Note: See TracChangeset for help on using the changeset viewer.