Changeset 2233 for src/RTL


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

Legend:

Unmodified
Added
Removed
  • 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)).
Note: See TracChangeset for help on using the changeset viewer.