- Timestamp:
- Oct 19, 2011, 1:39:54 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTL/semantics.ma
r1408 r1411 92 92 axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params). 93 93 94 definition 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 101 definition 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 94 108 definition rtl_exec_extended: 95 109 ∀globals. genv globals (rtl_params globals) → … … 104 118 ! st ← greg_store rtl_sem_params dreg2 dph st ; 105 119 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 107 125 | 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 ? 109 129 ]. 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 *) 111 131 qed. 112 132 113 133 definition 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 …). 119 135 120 136 definition rtl_fullexec ≝
Note: See TracChangeset
for help on using the changeset viewer.