Changeset 1411 for src/RTL


Ignore:
Timestamp:
Oct 19, 2011, 1:39:54 PM (8 years ago)
Author:
sacerdot
Message:
  1. sem_params2 splitted into sem_params1 + sem_params2 to take out the semantics of the extended statements
  2. pointer call semantics given in RTL/semantics
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1408 r1411  
    9292axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params).
    9393
     94definition rtl_more_sem_params1: ∀globals. more_sem_params1 … (rtl_params globals) ≝
     95 λglobals.
     96  mk_more_sem_params1 … rtl_more_sem_params
     97   (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
     98   rtl_init_locals rtl_save_frame (rtl_pop_frame …)
     99   rtl_fetch_external_args rtl_set_result.
     100
     101definition block_of_register_pair: register → register → state rtl_sem_params → res block ≝
     102 λr1,r2,st.
     103 do v1 ← greg_retrieve rtl_sem_params st r1 ;
     104 do v2 ← greg_retrieve rtl_sem_params st r2 ;
     105 do ptr ← pointer_of_address 〈v1,v2〉 ;
     106 OK … (pblock ptr). 
     107
    94108definition rtl_exec_extended:
    95109 ∀globals. genv globals (rtl_params globals) →
     
    104118      ! st ← greg_store rtl_sem_params dreg2 dph st ;
    105119       ret ? 〈E0, goto … l st〉
    106    | rtl_st_ext_call_ptr _ _ _ _ ⇒ ?
     120   | rtl_st_ext_call_ptr r1 r2 args dest ⇒
     121      ! b ← block_of_register_pair r1 r2 st ;
     122      ! ra ← succ_pc … (rtl_more_sem_params1 globals) l (pc … st) ;
     123      eval_call_block … (mk_sem_params1 … (rtl_more_sem_params1 globals))
     124       ge st b args dest ra
    107125   | rtl_st_ext_tailcall_id id regs ⇒ ?
    108    | rtl_st_ext_tailcall_ptr _ _ _ ⇒ ?
     126   | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
     127      ! b ← block_of_register_pair r1 r2 st ;
     128      ?
    109129   ].
    110 [1,2,3: cases not_implemented ] (*CSC: tailcalls and pointer calls not implemented ATM *)
     130[1,2: cases not_implemented ] (*CSC: tailcall semantics not implemented ATM *)
    111131qed.
    112132
    113133definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
    114  λglobals.
    115   mk_more_sem_params2 … rtl_more_sem_params
    116    (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
    117    rtl_init_locals rtl_save_frame (rtl_pop_frame …)
    118    rtl_fetch_external_args rtl_set_result (rtl_exec_extended …).
     134 λglobals. mk_more_sem_params2 … (rtl_more_sem_params1 globals) (rtl_exec_extended …).
    119135
    120136definition rtl_fullexec ≝
Note: See TracChangeset for help on using the changeset viewer.