Changeset 1411 for src/RTL

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:

• src/RTL/semantics.ma (modified) (2 diffs)

src/RTL/semantics.ma

@@ -92 +92 @@
 axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params).
 
+definition rtl_more_sem_params1: ∀globals. more_sem_params1 … (rtl_params globals) ≝
+ λglobals.
+  mk_more_sem_params1 … rtl_more_sem_params
+   (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
+   rtl_init_locals rtl_save_frame (rtl_pop_frame …)
+   rtl_fetch_external_args rtl_set_result.
+
+definition block_of_register_pair: register → register → state rtl_sem_params → res block ≝
+ λr1,r2,st.
+ do v1 ← greg_retrieve rtl_sem_params st r1 ;
+ do v2 ← greg_retrieve rtl_sem_params st r2 ;
+ do ptr ← pointer_of_address 〈v1,v2〉 ;
+ OK … (pblock ptr).  
+
 definition rtl_exec_extended:
  ∀globals. genv globals (rtl_params globals) →
@@ -104 +118 @@
       ! st ← greg_store rtl_sem_params dreg2 dph st ;
        ret ? 〈E0, goto … l st〉
-   | rtl_st_ext_call_ptr _ _ _ _ ⇒ ?
+   | rtl_st_ext_call_ptr r1 r2 args dest ⇒
+      ! b ← block_of_register_pair r1 r2 st ;
+      ! ra ← succ_pc … (rtl_more_sem_params1 globals) l (pc … st) ;
+      eval_call_block … (mk_sem_params1 … (rtl_more_sem_params1 globals))
+       ge st b args dest ra
    | rtl_st_ext_tailcall_id id regs ⇒ ?
-   | rtl_st_ext_tailcall_ptr _ _ _ ⇒ ?
+   | rtl_st_ext_tailcall_ptr r1 r2 args ⇒ 
+      ! b ← block_of_register_pair r1 r2 st ;
+      ?
    ].
-[1,2,3: cases not_implemented ] (*CSC: tailcalls and pointer calls not implemented ATM *)
+[1,2: cases not_implemented ] (*CSC: tailcall semantics not implemented ATM *)
 qed.
 
 definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
- λglobals.
-  mk_more_sem_params2 … rtl_more_sem_params
-   (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
-   rtl_init_locals rtl_save_frame (rtl_pop_frame …)
-   rtl_fetch_external_args rtl_set_result (rtl_exec_extended …).
+ λglobals. mk_more_sem_params2 … (rtl_more_sem_params1 globals) (rtl_exec_extended …).
 
 definition rtl_fullexec ≝