Ignore:
Timestamp:
Jul 23, 2012, 4:51:51 PM (7 years ago)
Author:
tranquil
Message:
  • completed update of ERTL semantics
  • some minor changes in joint semantics
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics_paolo.ma

    r2208 r2233  
    1 include "joint/SemanticUtils.ma".
    2 include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
     1include "joint/semanticsUtils_paolo.ma".
     2include "ERTL/ERTL_paolo.ma". (* CSC: syntax.ma in RTLabs *)
    33include alias "common/Identifiers.ma".
    44
     5record 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
     11definition set_psd_regs ≝ λx,env.mk_ertl_psd_env x (need_spilled_no env).
     12definition add_need_spilled_no ≝
     13  λr,env.mk_ertl_psd_env (psd_regs env) (add_set … (need_spilled_no env) r).
     14definition rm_need_spilled_no ≝
     15  λr,env.mk_ertl_psd_env (psd_regs env) (need_spilled_no env ∖  {(r)}).
     16
     17definition ertl_reg_env ≝ ertl_psd_env × hw_register_env.
     18
    519definition ps_reg_store ≝
    6  λr,v.λlocal_env:(register_env beval) × hw_register_env.
    7   do res ← reg_store r v (\fst local_env) ;
    8   OK … 〈res, \snd local_env〉.
     20 λ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〉.
    924
    1025definition ps_reg_retrieve ≝
    11  λlocal_env:(register_env beval) × hw_register_env. reg_retrieve … (\fst local_env).
     26 λlocal_env:ertl_reg_env. reg_retrieve … (psd_regs (\fst local_env)).
    1227
    1328definition hw_reg_store ≝
    14  λr,v.λlocal_env:(register_env beval) × hw_register_env.
     29 λr,v.λlocal_env:ertl_reg_env.
    1530  OK … 〈\fst local_env,hwreg_store r v (\snd local_env)〉.
    1631
    1732definition hw_reg_retrieve ≝
    18  λlocal_env:(register_env beval) × hw_register_env.λreg.
     33 λlocal_env:ertl_reg_env.λreg.
    1934  OK … (hwreg_retrieve … (\snd local_env) reg).
    2035
    21 definition ertl_more_sem_params: more_sem_params ertl_params_ :=
    22  mk_more_sem_params ertl_params_
    23   (list (register_env beval)) [] ((register_env beval) × hw_register_env)
    24    (λsp.〈empty_map …,init_hw_register_env sp〉) 0 it
    25    ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
    26     ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
    27      (λlocals,dest_src.
    28        do v ←
    29         match \snd dest_src with
    30         [ pseudo reg ⇒ ps_reg_retrieve locals reg
    31         | hardware reg ⇒ hw_reg_retrieve locals reg] ;
    32        match \fst dest_src with
    33        [ pseudo reg ⇒ ps_reg_store reg v locals
    34        | hardware reg ⇒ hw_reg_store reg v locals]).
    35 definition ertl_sem_params: sem_params ≝ mk_sem_params … ertl_more_sem_params.
     36definition ps_arg_retrieve ≝
     37  λlocal_env,a.
     38  match a with
     39  [ Reg r ⇒ ps_reg_retrieve local_env r
     40  | Imm b ⇒ return b
     41  ].
    3642
    37 definition ertl_init_locals :
    38  list register →
    39   (register_env beval) × hw_register_env → (register_env beval) × hw_register_env ≝
    40  λlocals,lenv.
    41   〈foldl … (λlenv,reg. add … lenv reg BVundef) (empty_map …) locals, \snd lenv〉.
     43definition ERTL_state : sem_state_params ≝
     44  mk_sem_state_params
     45 (* framesT ≝ *) (list ertl_psd_env)
     46 (* empty_framesT ≝ *) [ ]
     47 (* regsT ≝ *) ertl_reg_env
     48 (* empty_regsT ≝ *) (λsp.〈mk_ertl_psd_env (empty_map …) ∅,init_hw_register_env sp〉).
    4249
    43 (*CSC: could we use here a dependent type to avoid the Error case? *)
    44 axiom EmptyStack: String.
    45 definition ertl_pop_frame:
    46  ∀globals. genv … (ertl_params globals) → state … ertl_sem_params → res (state … ertl_sem_params) ≝
    47  λglobals,ge,st.
    48   let frms ≝ st_frms ? st in
    49   match frms with
    50   [ nil ⇒ Error ? [MSG EmptyStack]
    51   | cons hd tl ⇒
    52      OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
     50(* we ignore need_spilled_no as we never move framesize based values around in the
     51   translation *)
     52definition ertl_eval_move ≝ λenv,pr.
     53      ! v ←
     54        match \snd pr with
     55        [ Reg src ⇒
     56          match src with
     57          [ PSD r ⇒ ps_reg_retrieve env r
     58          | HDW r ⇒ hw_reg_retrieve env r
     59          ]
     60        | Imm bv ⇒ return bv ] ;
     61      match \fst pr with
     62      [ PSD r ⇒ ps_reg_store r v env
     63      | HDW r ⇒ hw_reg_store r v env
     64      ].
     65
     66definition ertl_allocate_local ≝
     67  λreg.λlenv : ertl_reg_env.
     68  〈set_psd_regs (add … (psd_regs (\fst lenv)) reg BVundef) (\fst lenv), \snd lenv〉.
    5369
    5470definition ertl_save_frame:
    55  address → nat → nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
    56  λl.λ_.λ_.λ_.λ_.λst.
    57   do st ← save_ra … st l ;
     71 cpointer → unit → state … ERTL_state → res (state … ERTL_state) ≝
     72 λpc.λ_.λst.
     73  do st ← save_ra … st pc ;
    5874  OK …
    59    (set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st))
    60     (set_regs ertl_sem_params 〈empty_map …,\snd (regs … st)〉 st)).
    61 
    62 definition ertl_result_regs:
    63  ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list register) ≝
    64  λglobals,ge,st.
    65   do fn ← graph_fetch_function … globals ge st ;
    66   OK … (joint_if_result … fn).
     75   (set_frms ERTL_state (\fst (regs ERTL_state st) :: (st_frms … st))
     76    (set_regs ERTL_state 〈mk_ertl_psd_env (empty_map …) ∅,\snd (regs … st)〉 st)).
    6777
    6878(*CSC: XXXX, for external functions only*)
    69 axiom ertl_fetch_external_args: external_function → state ertl_sem_params → res (list val).
    70 axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params).
     79axiom ertl_fetch_external_args: external_function → state ERTL_state → res (list val).
     80axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state).
     81(* I think there should be a list beval in place of list val here
     82  λvals.λ_.λst.
     83  (* set all RegisterRets to 0 *)
     84  let reset ≝ λenv,r.hwreg_store r (BVByte (bv_zero …)) env in
     85  let env ≝ foldl … reset (\snd (regs … st)) RegisterRets in
     86  let set_vals ≝ λenv,pr.hwreg_store (\fst pr) (\snd pr) env in ?.
     87  let env' ≝ foldl … set_vals env (zip_pottier … RegisterRets vals) in
     88  return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)
    7189
    72 definition framesize:
    73  ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res nat ≝
    74   λglobals,ge,st.
    75    do f ← graph_fetch_function … ge st ;
    76    OK ? (joint_if_stacksize globals … f).
     90definition xdata_pointer_of_address: address → res xpointer ≝
     91λp.let 〈v1,v2〉 ≝ p in
     92! p ← pointer_of_bevals [v1;v2] ;
     93match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = XData) with
     94[ XData ⇒ λE.OK ? (mk_Sig … p E)
     95| _ ⇒ λ_.Error … [MSG BadPointer]
     96] (refl …).
    7797
    78 definition get_hwsp : state ertl_sem_params → address ≝
     98definition address_of_xdata_pointer: xpointer → address ≝
     99λp.list_to_pair … (bevals_of_pointer p) ?. % qed.
     100
     101definition get_hwsp : ERTL_state → res xpointer ≝
    79102 λst.
    80103  let spl ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPL in
    81104  let sph ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPH in
    82   〈spl,sph〉.
     105  xdata_pointer_of_address 〈spl,sph〉.
    83106
    84 definition set_hwsp : address → state ertl_sem_params → state ertl_sem_params
     107definition set_hwsp : xpointer → ERTL_state → ERTL_state
    85108 λsp,st.
    86   let 〈spl,sph〉 ≝ sp in
     109  let 〈spl,sph〉 ≝ address_of_xdata_pointer sp in
    87110  let hwregs ≝ hwreg_store RegisterSPL spl (\snd (regs … st)) in
    88111  let hwregs ≝ hwreg_store RegisterSPH sph hwregs in
    89   set_regs ertl_sem_params 〈\fst (regs … st),hwregs〉 st.
     112  set_regs ERTL_state 〈\fst (regs … st),hwregs〉 st.
    90113
    91 definition ertl_more_sem_params1: ∀globals. more_sem_params1 … (ertl_params globals) ≝
    92  λglobals.
    93   mk_more_sem_params1 … ertl_more_sem_params graph_succ_p (graph_pointer_of_label …)
    94     (graph_fetch_statement …) (load_ra …) (ertl_result_regs …)
    95     ertl_init_locals ertl_save_frame (ertl_pop_frame …)
    96     ertl_fetch_external_args ertl_set_result.
    97 definition ertl_sem_params1: ∀globals. sem_params1 globals ≝
    98  λglobals. mk_sem_params1 … (ertl_more_sem_params1 globals).
     114definition eval_ertl_seq:
     115 ∀globals. genv ERTL globals →
     116  ertl_seq → joint_internal_function ERTL globals → ERTL_state →
     117   IO io_out io_in ERTL_state ≝
     118 λglobals,ge,stm,curr_fn,st.
     119 let framesize : Byte ≝ bitvector_of_nat 8 (joint_if_stacksize … curr_fn) in
     120  match stm with
     121   [ ertl_new_frame ⇒
     122      ! sp ← get_hwsp st ;
     123      let newsp ≝ shift_pointer … sp framesize in
     124      return set_hwsp newsp st
     125   | ertl_del_frame ⇒
     126      ! sp ← get_hwsp st ;
     127      let newsp ≝ shift_pointer … sp framesize in
     128      return set_hwsp newsp st
     129   | ertl_frame_size dst ⇒
     130      let env ≝ regs … st in
     131      ! env' ← ps_reg_store dst (BVByte framesize) env ;
     132      let env'' ≝ 〈add_need_spilled_no dst (\fst env'), \snd env'〉 in
     133      return set_regs ERTL_state env'' st
     134   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed. 
    99135
    100 definition ertl_exec_extended:
    101  ∀globals. genv globals (ertl_params globals) →
    102   ertl_statement_extension → label → state ertl_sem_params →
    103    IO io_out io_in (trace × (state ertl_sem_params)) ≝
    104  λglobals,ge,stm,l,st.
    105   match stm with
    106    [ ertl_st_ext_new_frame ⇒
    107       ! v ← framesize globals … ge st;
    108       let sp ≝ get_hwsp st in
    109       ! newsp ← addr_sub sp v;
    110       let st ≝ set_hwsp newsp st in
    111       ! st ← next … (ertl_sem_params1 globals) l st ;
    112         return 〈E0,st〉
    113    | ertl_st_ext_del_frame ⇒
    114       ! v ← framesize … ge st;
    115       let sp ≝ get_hwsp st in
    116       ! newsp ← addr_add sp v;
    117       let st ≝ set_hwsp newsp st in
    118       ! st ← next … (ertl_sem_params1 …) l st ;
    119         return 〈E0,st〉
    120    | ertl_st_ext_frame_size dst ⇒
    121       ! v ← framesize … ge st;
    122       ! st ← greg_store ertl_sem_params dst (BVByte (bitvector_of_nat … v)) st;
    123       ! st ← next … (ertl_sem_params1 …) l st ;
    124         return 〈E0, st〉
    125    ].
     136definition ertl_post_op2 ≝
     137  λop,dst,arg1,arg2,st.
     138  let local_env ≝ regs ERTL_state st in
     139  let f ≝ λarg,st.match arg with
     140     [ Reg r ⇒
     141       if r ∈ need_spilled_no (\fst local_env) then
     142         set_regs ERTL_state 〈add_need_spilled_no dst (\fst local_env),\snd local_env〉 st
     143       else
     144         st
     145     | _ ⇒ st
     146     ] in
     147  match op with
     148  [ Add ⇒ f arg1 (f arg2 st) (* won't happen both *)
     149  | Addc ⇒ f arg1 (f arg2 st) (* we have to think about what should we do with carry bit *)
     150  | Sub ⇒ f arg1 st
     151  | _ ⇒ st].
     152         
    126153
    127 definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
    128  λglobals. mk_more_sem_params2 … (ertl_more_sem_params1 …) (ertl_exec_extended …).
    129 
    130 definition ertl_fullexec: fullexec io_out io_in ≝
    131  joint_fullexec … (λp. ertl_more_sem_params2 (prog_var_names … p)).
     154definition ERTL_semantics ≝
     155  make_sem_graph_params ERTL
     156  (mk_more_sem_unserialized_params ??
     157  (* st_pars            ≝ *) ERTL_state
     158  (* acca_store_        ≝ *) ps_reg_store
     159  (* acca_retrieve_     ≝ *) ps_reg_retrieve
     160  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
     161  (* accb_store_        ≝ *) ps_reg_store
     162  (* accb_retrieve_     ≝ *) ps_reg_retrieve
     163  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
     164  (* dpl_store_         ≝ *) ps_reg_store
     165  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
     166  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
     167  (* dph_store_         ≝ *) ps_reg_store
     168  (* dph_retrieve_      ≝ *) ps_reg_retrieve
     169  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
     170  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
     171  (* pair_reg_move_     ≝ *) ertl_eval_move
     172  (* fetch_ra           ≝ *) (load_ra …)
     173  (* allocate_local     ≝ *) ertl_allocate_local
     174  (* save_frame         ≝ *) ertl_save_frame
     175  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
     176  (* fetch_external_args≝ *) ertl_fetch_external_args
     177  (* set_result         ≝ *) ertl_set_result
     178  (* call_args_for_main ≝ *) 0
     179  (* call_dest_for_main ≝ *) it
     180  (* read_result        ≝ *) (λ_.λ_.λ_.
     181     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
     182  (* eval_ext_seq       ≝ *) eval_ertl_seq
     183  (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
     184  (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
     185  (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st)
     186  (* post_op2           ≝ *) (λ_.λ_.ertl_post_op2)).
Note: See TracChangeset for help on using the changeset viewer.