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/ERTLptr/semantics.ma

    r2566 r2590  
    22include "ERTLptr/ERTLptr.ma". (* CSC: syntax.ma in RTLabs *)
    33include "ERTL/semantics.ma".
    4 include "common/extraGlobalenvs.ma".
    54include alias "common/Identifiers.ma".
    6 (*
    7 record ertl_psd_env : Type[0] ≝
    8   { psd_regs : register_env beval
    9   (* this tells what pseudo-registers should have their value corrected by spilled_no *)
    10   ; need_spilled_no : identifier_set RegisterTag
    11   }.
    12 
    13 definition set_psd_regs ≝ λx,env.mk_ertl_psd_env x (need_spilled_no env).
    14 definition add_need_spilled_no ≝
    15   λr,env.mk_ertl_psd_env (psd_regs env) (add_set … (need_spilled_no env) r).
    16 definition rm_need_spilled_no ≝
    17   λr,env.mk_ertl_psd_env (psd_regs env) (need_spilled_no env ∖  {(r)}).
    18 
    19 definition ertl_reg_env ≝ ertl_psd_env × hw_register_env.
    20 
    21 definition ps_reg_store: ? → ? → ? → res ? ≝
    22  λr,v.λlocal_env : ertl_reg_env.
    23   do res ← reg_store r v (psd_regs (\fst local_env)) ;
    24   let psd_env ≝ set_psd_regs res (\fst local_env) in
    25   OK … 〈rm_need_spilled_no r psd_env, \snd local_env〉.
    26 
    27 definition ps_reg_retrieve ≝
    28  λlocal_env:ertl_reg_env. reg_retrieve … (psd_regs (\fst local_env)).
    29 
    30 definition hw_reg_store ≝
    31  λr,v.λlocal_env:ertl_reg_env.
    32   OK … 〈\fst local_env,hwreg_store r v (\snd local_env)〉.
    33 
    34 definition hw_reg_retrieve ≝
    35  λlocal_env:ertl_reg_env.λreg.
    36   OK … (hwreg_retrieve … (\snd local_env) reg).
    37 
    38 
    39 definition ps_arg_retrieve : ertl_reg_env → argument ? → res beval ≝
    40   λlocal_env,a.
    41   match a with
    42   [ Reg r ⇒ ps_reg_retrieve local_env r
    43   | Imm b ⇒ return BVByte b
    44   ].
    45 
    46 
    47 
    48 definition ERTL_state : sem_state_params ≝
    49   mk_sem_state_params
    50  (* framesT ≝ *) (list ertl_psd_env)
    51  (* empty_framesT ≝ *) [ ]
    52  (* regsT ≝ *) ertl_reg_env
    53  (* empty_regsT ≝ *) (λsp.〈mk_ertl_psd_env (empty_map …) ∅,init_hw_register_env sp〉)
    54  (*load_sp ≝ *) ?
    55   (*save_sp ≝ *) ?. cases daemon qed.
    56 
    57 (* we ignore need_spilled_no as we never move framesize based values around in the
    58    translation *)
    59 definition ertl_eval_move ≝ λenv,pr.
    60       ! v ←
    61         match \snd pr with
    62         [ Reg src ⇒
    63           match src with
    64           [ PSD r ⇒ ps_reg_retrieve env r
    65           | HDW r ⇒ hw_reg_retrieve env r
    66           ]
    67         | Imm b ⇒ return BVByte b ] ;
    68       match \fst pr with
    69       [ PSD r ⇒ ps_reg_store r v env
    70       | HDW r ⇒ hw_reg_store r v env
    71       ].
    72 
    73 definition ertl_allocate_local ≝
    74   λreg.λlenv : ertl_reg_env.
    75   〈set_psd_regs (add … (psd_regs (\fst lenv)) reg BVundef) (\fst lenv), \snd lenv〉.
    76 *)
    775
    786definition ertlptr_save_frame:
    79  call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝
    80  λk.λ_.λst.
     7 call_kind → unit → ident → state_pc ERTL_state → res (state … ERTL_state) ≝
     8 λk.λ_.λid.λst.
    819 do st ← match k with [ID ⇒ push_ra … st (pc … st) |
    8210 PTR ⇒ return (st_no_pc … st)] ; OK …
    83    (set_frms ERTL_state (\fst (regs ERTL_state st) :: (st_frms … st))
    84     (set_regs ERTL_state 〈mk_ertl_psd_env (empty_map …) ∅,\snd (regs … st)〉 st)).
    85 
    86 (*
    87 (*CSC: XXXX, for external functions only*)
    88 axiom ertl_fetch_external_args: external_function → state ERTL_state → call_args ERTL → res (list val).
    89 axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state).
    90 (* I think there should be a list beval in place of list val here
    91   λvals.λ_.λst.
    92   (* set all RegisterRets to 0 *)
    93   let reset ≝ λenv,r.hwreg_store r (BVByte (bv_zero …)) env in
    94   let env ≝ foldl … reset (\snd (regs … st)) RegisterRets in
    95   let set_vals ≝ λenv,pr.hwreg_store (\fst pr) (\snd pr) env in ?.
    96   let env' ≝ foldl … set_vals env (zip_pottier … RegisterRets vals) in
    97   return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)
    98 
    99 definition xdata_pointer_of_address: address → res xpointer ≝
    100 λp.let 〈v1,v2〉 ≝ p in
    101 ! p ← pointer_of_bevals [v1;v2] ;
    102 match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = XData) with
    103 [ XData ⇒ λE.OK ? (mk_Sig … p E)
    104 | _ ⇒ λ_.Error … [MSG BadPointer]
    105 ] (refl …).
    106 
    107 definition address_of_xdata_pointer: xpointer → address ≝
    108 λp.list_to_pair … (bevals_of_pointer p) ?. % qed.
    109 
    110 definition get_hwsp : state ERTL_state → res xpointer ≝
    111  λst.
    112   let spl ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPL in
    113   let sph ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPH in
    114   xdata_pointer_of_address 〈spl,sph〉.
    115 
    116 definition set_hwsp : xpointer → state ERTL_state → state ERTL_state ≝
    117  λsp,st.
    118   let 〈spl,sph〉 ≝ address_of_xdata_pointer sp in
    119   let hwregs ≝ hwreg_store RegisterSPL spl (\snd (regs … st)) in
    120   let hwregs ≝ hwreg_store RegisterSPH sph hwregs in
    121   set_regs ERTL_state 〈\fst (regs … st),hwregs〉 st.
    122 
    123 axiom FunctionNotFound: errmsg.*)
     11   (set_frms ERTL_state (〈\fst (regs ERTL_state st),id〉 :: (st_frms … st))
     12    (set_regs ERTL_state 〈empty_map …,\snd (regs … st)〉 st)).
    12413
    12514definition eval_ertlptr_seq:
     
    13019  match stm with
    13120   [ ertlptr_ertl seq ⇒ eval_ertl_seq F globals ge seq id st
    132    | LOW_ADDRESS r l ⇒  ! pc_lab ←  (pc_of_label ?? ? (block_of_funct … ge id) l);
    133                         let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
     21   | LOW_ADDRESS r l ⇒  ! pc_lab ← get_pc_from_label … ge id l;
     22                        let 〈addrl,addrh〉 ≝ beval_pair_of_pc pc_lab in
    13423                        ps_reg_store_status r addrl st
    135    | HIGH_ADDRESS r l ⇒ ! pc_lab ←  (pc_of_label ?? ? (block_of_funct … ge id) l);
     24   | HIGH_ADDRESS r l ⇒ ! pc_lab ← get_pc_from_label … ge id l;
    13625                        let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
    13726                        ps_reg_store_status r addrh st
    13827   ].
    139  [3,8: (* PAOLO, HELP: we should pass ge, but the type is abstracted over F! *)
    140        cases daemon
    141  |4,5,9,10: cases daemon (* Closed by side effect for 3,8 *)
    142  |1,6: (* PAOLO, HELP: this should be an hypothesis that needs to propagate
    143           a long way and then be discarded in Joint/semantics.ma *)
    144        cases daemon
    145  |2,7: @block_of_funct_ident_is_code ]
    146 qed.
    147 
    148 (*
    149 definition ertl_post_op2 ≝
    150   λop,dst,arg1,arg2,st.
    151   let local_env ≝ regs ERTL_state st in
    152   let f ≝ λarg,st.match arg with
    153      [ Reg r ⇒
    154        if r ∈ need_spilled_no (\fst local_env) then
    155          set_regs ERTL_state 〈add_need_spilled_no dst (\fst local_env),\snd local_env〉 st
    156        else
    157          st
    158      | _ ⇒ st
    159      ] in
    160   match op with
    161   [ Add ⇒ f arg1 (f arg2 st) (* won't happen both *)
    162   | Addc ⇒ f arg1 (f arg2 st) (* we have to think about what should we do with carry bit *)
    163   | Sub ⇒ f arg1 st
    164   | _ ⇒ st].
    165 *)
    166 
     28   
    16729definition ERTLptr_semantics ≝
    16830  make_sem_graph_params ERTLptr
Note: See TracChangeset for help on using the changeset viewer.