Changeset 2233


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
Location:
src
Files:
4 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)).
  • src/LIN/joint_LTL_LIN_semantics_paolo.ma

    r2217 r2233  
    6363  (* read_result        ≝ *) (λ_.λ_.λ_.
    6464  λst.return map … (hwreg_retrieve (regs … st)) RegisterRets)
    65   (* eval_ext_seq       ≝ *) (λ_.λ_.eval_ltl_lin_seq)
     65  (* eval_ext_seq       ≝ *) (λ_.λ_.λs.λ_.eval_ltl_lin_seq s)
    6666  (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
    6767  (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
    68   (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st).
     68  (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st)
     69  (* post_op2           ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st).
  • src/RTL/semantics_paolo.ma

    r2217 r2233  
    3030
    3131definition rtl_fetch_ra:
    32  state RTL_state → res ((state RTL_state) × cpointer) ≝
     32 RTL_state → res (RTL_state × cpointer) ≝
    3333 λst.
    3434  match st_frms ? st with
     
    4141
    4242definition rtl_setup_call:
    43  nat → list register → list psd_argument → state RTL_state → res (state RTL_state)
     43 nat → list register → list psd_argument → RTL_state → res RTL_state
    4444  λstacksize,formal_arg_regs,actual_arg_regs,st.
    4545  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
     
    5757qed.
    5858
    59 definition rtl_save_frame ≝ λl.λretregs.λst : state RTL_state.
     59definition rtl_save_frame ≝ λl.λretregs.λst : RTL_state.
    6060  let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in
    6161  OK … (set_frms RTL_state frame st).
    6262
    6363(*CSC: XXXX, for external functions only*)
    64 axiom rtl_fetch_external_args: external_function → state RTL_state → res (list val).
    65 axiom rtl_set_result: list val → list register → state RTL_state → res (state RTL_state).
     64axiom rtl_fetch_external_args: external_function → RTL_state → res (list val).
     65axiom rtl_set_result: list val → list register → RTL_state → res RTL_state.
    6666
    6767definition rtl_reg_store ≝ λr,v,st.! mem ← reg_store r v (regs RTL_state st) ; return set_regs RTL_state mem st.
     
    6969
    7070definition rtl_read_result :
    71  ∀globals.genv RTL globals → list register → state RTL_state → res (list beval) ≝
     71 ∀globals.genv RTL globals → list register → RTL_state → res (list beval) ≝
    7272 λglobals,ge,rets,st.
    7373 m_list_map … (rtl_reg_retrieve st) rets.
     
    7777  saves the OutOfBounds exception *)
    7878definition rtl_pop_frame:
    79  ∀globals. genv RTL globals → list register → state RTL_state →
    80   res (state RTL_state) ≝
    81  λglobals,ge,ret,st.
     79 ∀globals. genv RTL globals → joint_internal_function RTL globals → RTL_state →
     80  res RTL_state ≝
     81 λglobals,ge,curr_fn,st.
     82  let ret ≝ joint_if_result … curr_fn in
    8283  do ret_vals ← rtl_read_result … ge ret st ;
    8384  match st_frms ? st with
     
    99100(* This code is quite similar to eval_call_block: can we factorize it out? *)
    100101definition eval_tailcall_block:
    101  ∀globals.genv RTL globals → state RTL_state →
     102 ∀globals.genv RTL globals → RTL_state →
    102103  block → call_args RTL →
    103104  (* this is where the result of the current function should be stored *)
    104105  call_dest RTL →
    105106  IO io_out io_in
    106     ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×(state RTL_state)) ≝
     107    ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×RTL_state) ≝
    107108 λglobals,ge,st,b,args,ret.
    108109  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
     
    122123    ].
    123124
    124 definition block_of_register_pair: register → register → state RTL_state → res block ≝
     125definition block_of_register_pair: register → register → RTL_state → res block ≝
    125126 λr1,r2,st.
    126127 do v1 ← rtl_reg_retrieve st r1 ;
     
    131132definition eval_rtl_seq:
    132133 ∀globals. genv RTL globals →
    133   rtl_seq → state RTL_state →
    134    IO io_out io_in (state RTL_state)
    135  λglobals,ge,stm,st.
     134  rtl_seq → joint_internal_function RTL globals → RTL_state →
     135   IO io_out io_in RTL_state
     136 λglobals,ge,stm,curr_fn,st.
    136137  match stm with
    137138   [ rtl_stack_address dreg1 dreg2  ⇒
     
    144145definition eval_rtl_call:
    145146 ∀globals. genv RTL globals →
    146   rtl_call → state RTL_state →
    147    IO io_out io_in ((step_flow RTL ? Call)×(state RTL_state)) ≝
     147  rtl_call → RTL_state →
     148   IO io_out io_in ((step_flow RTL ? Call)×RTL_state) ≝
    148149 λglobals,ge,stm,st.
    149150  match stm with
     
    169170definition eval_rtl_tailcall:
    170171 ∀globals. genv RTL globals →
    171   rtl_tailcall → call_dest RTL → state RTL_state →
    172    IO io_out io_in ((fin_step_flow RTL ? Call)×(state RTL_state)) ≝
    173    λglobals,ge,stm,ret,st.
     172  rtl_tailcall → joint_internal_function RTL globals → RTL_state →
     173   IO io_out io_in ((fin_step_flow RTL ? Call)×RTL_state) ≝
     174   λglobals,ge,stm,curr_fn,st.
     175   let ret ≝ joint_if_result … curr_fn in
    174176   match stm with
    175177   [ rtl_tailcall_id id args ⇒
     
    182184
    183185definition RTL_semantics ≝
    184   mk_more_sem_unserialized_params RTL (joint_internal_function RTL)
    185     RTL_state
    186     reg_store reg_retrieve rtl_arg_retrieve
    187     reg_store reg_retrieve rtl_arg_retrieve
    188     reg_store reg_retrieve rtl_arg_retrieve
    189     reg_store reg_retrieve rtl_arg_retrieve
    190     rtl_arg_retrieve
    191     (λenv,p. let 〈dest,src〉 ≝ p in
    192       ! v ← rtl_arg_retrieve env src ;
    193       reg_store dest v env)
    194     rtl_fetch_ra
    195     rtl_init_local
    196     rtl_save_frame
    197     rtl_setup_call
    198     rtl_fetch_external_args
    199     rtl_set_result
    200     [ ] [ ]
    201     rtl_read_result
    202     eval_rtl_seq
    203     eval_rtl_tailcall
    204     eval_rtl_call.
     186  make_sem_graph_params RTL
     187    (mk_more_sem_unserialized_params ??
     188      RTL_state
     189      reg_store reg_retrieve rtl_arg_retrieve
     190      reg_store reg_retrieve rtl_arg_retrieve
     191      reg_store reg_retrieve rtl_arg_retrieve
     192      reg_store reg_retrieve rtl_arg_retrieve
     193      rtl_arg_retrieve
     194      (λenv,p. let 〈dest,src〉 ≝ p in
     195        ! v ← rtl_arg_retrieve env src ;
     196        reg_store dest v env)
     197      rtl_fetch_ra
     198      rtl_init_local
     199      rtl_save_frame
     200      rtl_setup_call
     201      rtl_fetch_external_args
     202      rtl_set_result
     203      [ ] [ ]
     204      rtl_read_result
     205      eval_rtl_seq
     206      eval_rtl_tailcall
     207      eval_rtl_call
     208      rtl_pop_frame
     209      (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)).
  • src/joint/semantics_paolo.ma

    r2217 r2233  
    3333 ; m: bemem
    3434 }.
     35
     36coercion sem_state_params_to_state nocomposites:
     37  ∀p : sem_state_params.Type[0] ≝ state on _p : sem_state_params to Type[0].
    3538
    3639record state_pc (semp : sem_state_params) : Type[0] ≝
     
    134137  (* change of pc must be left to *_flow execution *)
    135138  ; eval_ext_seq: ∀globals.genv_t (fundef (F globals)) → ext_seq uns_pars →
    136       state st_pars → IO io_out io_in (state st_pars)
     139      F globals → state st_pars → IO io_out io_in (state st_pars)
    137140  ; eval_ext_tailcall : ∀globals.genv_t (fundef (F globals)) → ext_tailcall uns_pars →
    138       call_dest uns_pars → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
    139   ; eval_ext_call: ∀globals.genv_t (fundef (F globals)) → ∀s : ext_call uns_pars.
    140       state st_pars →
     141      F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
     142  ; eval_ext_call: ∀globals.genv_t (fundef (F globals)) →
     143      ext_call uns_pars → state st_pars →
    141144      IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars))
    142   ; pop_frame: ∀globals.genv_t (fundef (F globals)) → call_dest uns_pars → state st_pars → res (state st_pars)
     145  ; pop_frame: ∀globals.genv_t (fundef (F globals)) → F globals → state st_pars → res (state st_pars)
     146  (* do something more in some op2 calculations (e.g. mark a register for correction
     147     with spilled_no in ERTL) *)
     148  ; post_op2 : ∀globals.genv_t (fundef (F globals)) →
     149    Op2 → acc_a_reg uns_pars → acc_a_arg uns_pars → snd_arg uns_pars →
     150    state st_pars → state st_pars
    143151  }.
    144152
     
    407415
    408416definition eval_seq_no_pc :
    409  ∀globals.∀p:sem_params. genv p globals → state p
    410   ∀s:joint_seq p globals.
     417 ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals
     418  state p → ∀s:joint_seq p globals.
    411419  IO io_out io_in (state p) ≝
    412  λglobals,p,ge,st,seq.
     420 λp,globals,ge,curr_fn,st,seq.
    413421  match seq return λx.IO ??? with
    414422  [ extension_seq c ⇒
    415     eval_ext_seq … ge c st
     423    eval_ext_seq … ge c curr_fn st
    416424  | LOAD dst addrl addrh ⇒
    417425    ! vaddrh ← dph_arg_retrieve … st addrh ;
     
    447455      let carry ≝ beval_of_bool carry in
    448456    ! st' ← acca_store … dacc_a v' st;
    449     return set_carry … carry st'
     457    return set_carry … carry (post_op2 … p … ge op dacc_a sacc_a src st')
    450458  | CLEAR_CARRY ⇒
    451459    return set_carry … BVfalse st
     
    484492
    485493definition eval_seq_pc :
    486  ∀globals.∀p:sem_params. genv p globals → state p →
     494 ∀p:sem_params.∀globals. genv p globals → state p →
    487495  ∀s:joint_seq p globals.
    488496  IO io_out io_in (step_flow p ? (step_flows … s)) ≝
    489   λg,p,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
     497  λp,g,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
    490498  [ CALL_ID id args dest ⇒
    491499    ! b ← opt_to_res \ldots  [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
     
    499507
    500508definition eval_step :
    501  ∀globals.∀p:sem_params. genv p globals → state p →
     509 ∀p:sem_params.∀globals. genv p globals →
     510  joint_internal_function p globals → state p →
    502511  ∀s:joint_step p globals.
    503512  IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝
    504   λglobals,p,ge,st,s.
     513  λp,globals,ge,curr_fn,st,s.
    505514  match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with
    506515  [ step_seq s ⇒
    507516    ! flow ← eval_seq_pc ?? ge st s ;
    508     ! st' ← eval_seq_no_pc ?? ge st s ;
     517    ! st' ← eval_seq_no_pc ?? ge curr_fn st s ;
    509518    return 〈flow,st'〉
    510519  | COND src ltrue ⇒
     
    518527  %1 % qed.
    519528
    520 definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv p globals →
    521   (* result registers of current function *) call_dest p → state p → ∀s : joint_fin_step p.
     529definition eval_fin_step_no_pc : ∀p:sem_params.∀globals. genv p globals →
     530  (* current function *) joint_internal_function p globals → state p → ∀s : joint_fin_step p.
    522531  IO io_out io_in (state p) ≝
    523  λglobals,p,ge,ret,st,s.
     532 λp,globals,ge,curr_fn,st,s.
    524533  match s return λx.IO ??? with
    525534    [ tailcall c ⇒
    526       !〈flow,st'〉 ← eval_ext_tailcall … ge c ret st ;
     535      !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
    527536      return st'
    528537    | _ ⇒ return st
     
    530539
    531540definition eval_fin_step_pc :
    532  ∀globals.∀p:sem_params. genv p globals → call_dest p → state p →
     541 ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals → state p →
    533542  ∀s:joint_fin_step p.
    534543  IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
    535   λg,p,ge,ret,st,s.
     544  λp,g,ge,curr_fn,st,s.
    536545  match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
    537546  [ tailcall c ⇒
    538     !〈flow,st'〉 ← eval_ext_tailcall … ge c ret st ;
     547    !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
    539548    return flow 
    540549  | GOTO l ⇒ return FRedirect … l
     
    542551  ]. %1 % qed.
    543552
    544 definition do_call : ∀globals: list ident.∀p:sem_params. genv p globals →
     553definition do_call : ∀p:sem_params.∀globals: list ident. genv p globals →
    545554  state p → Z → joint_internal_function p globals → call_args p →
    546555  res (state_pc p) ≝
    547   λglobals,p,ge,st,id,fn,args.
     556  λp,globals,ge,st,id,fn,args.
    548557    ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
    549558              args st ;
     
    557566(* The pointer provided is the one to the *next* instruction. *)
    558567definition eval_step_flow :
    559  ∀globals.∀p:sem_params.∀flows.genv p globals →
     568 ∀p:sem_params.∀globals.∀flows.genv p globals →
    560569 state p → cpointer → step_flow p ? flows → res (state_pc p) ≝
    561  λglobals,p,flows,ge,st,nxt,cmd.
     570 λp,globals,flows,ge,st,nxt,cmd.
    562571 match cmd with
    563572  [ Redirect _ l ⇒
     
    570579  ].
    571580
    572 definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀flows. genv p globals →
     581definition eval_fin_step_flow : ∀p:sem_params.∀globals: list ident.∀flows. genv p globals →
    573582  state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝
    574   λglobals,p,lbls,ge,st,curr,cmd.
     583  λp,globals,lbls,ge,st,curr,cmd.
    575584  match cmd with
    576585  [ FRedirect _ l ⇒ goto … ge l st curr
     
    580589    ! 〈st',ra〉 ← fetch_ra … st ;
    581590    ! fn ← fetch_function … ge curr ;
    582     ! st'' ← pop_frame … ge (joint_if_result … fn) st';
     591    ! st'' ← pop_frame … ge fn st';
    583592    return mk_state_pc ? st'' ra
    584593  ].
     
    591600 match stmt with
    592601 [ sequential s nxt ⇒
    593    ! 〈flow,st'〉 ← eval_step … ge st s ;
     602   ! 〈flow,st'〉 ← eval_step … ge curr_fn st s ;
    594603   ! nxtptr ← succ_pc ? p (pc … st) nxt ;
    595604   eval_step_flow … ge st' nxtptr flow
    596605 | final s ⇒
    597    let ret ≝ joint_if_result … curr_fn in
    598    ! st' ← eval_fin_step_no_pc … ge ret st s ;
    599    ! flow ← eval_fin_step_pc … ge ret st s ;
     606   ! st' ← eval_fin_step_no_pc … ge curr_fn st s ;
     607   ! flow ← eval_fin_step_pc … ge curr_fn st s ;
    600608   eval_fin_step_flow … ge st' (pc … st) flow
    601609 ].
Note: See TracChangeset for help on using the changeset viewer.