Changeset 1451 for src/RTL/semantics.ma


Ignore:
Timestamp:
Oct 22, 2011, 4:18:11 AM (8 years ago)
Author:
sacerdot
Message:
  1. All axioms in LIN/semantics.ma closed
  2. succ_pc and pointer_of_label moved to more_sem_params1; their type have been changed too to implement LIN/semantics.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1415 r1451  
    1414definition rtl_more_sem_params: more_sem_params rtl_params_ :=
    1515 mk_more_sem_params rtl_params_
    16   (list frame) [] (register_env beval) (λ_.empty_map …) [] [](*dummy*) graph_succ_p
     16  (list frame) [] (register_env beval) (λ_.empty_map …) [] [](*dummy*)
    1717   reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve
    1818    reg_store reg_retrieve reg_store reg_retrieve
    1919     (λlocals,dest_src.
    2020       do v ← reg_retrieve locals (\snd dest_src) ;
    21        reg_store (\fst dest_src) v locals)
    22      pointer_of_label.
     21       reg_store (\fst dest_src) v locals).
    2322definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
    2423
     
    9998definition rtl_more_sem_params1: ∀globals. more_sem_params1 … (rtl_params globals) ≝
    10099 λglobals.
    101   mk_more_sem_params1 … rtl_more_sem_params
     100  mk_more_sem_params1 … rtl_more_sem_params graph_succ_p (graph_pointer_of_label …)
    102101   (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
    103102   rtl_init_locals rtl_save_frame (rtl_pop_frame …)
    104103   rtl_fetch_external_args rtl_set_result.
     104definition rtl_sem_params1: ∀globals. sem_params1 … globals ≝
     105 λglobals. mk_sem_params1 … (rtl_more_sem_params1 globals).
    105106
    106107definition block_of_register_pair: register → register → state rtl_sem_params → res block ≝
     
    123124      let regs ≝ rtl_init_locals … (joint_if_locals … fn) (regs … st) in
    124125      let l' ≝ joint_if_entry … fn in
    125        ret ? 〈 E0, goto … l' (set_regs rtl_sem_params regs st)〉
     126      ! st ← next … (rtl_sem_params1 …) l' (set_regs rtl_sem_params regs st) ;
     127       ret ? 〈 E0, st〉
    126128    | External fn ⇒ ?(*
    127129      ! params ← fetch_external_args … fn st;
     
    151153      ! st ← greg_store rtl_sem_params dreg1 dpl st ;
    152154      ! st ← greg_store rtl_sem_params dreg2 dph st ;
    153        ret ? 〈E0, goto … l st〉
     155      ! st ← next … (rtl_sem_params1 globals) l st ;
     156       ret ? 〈E0, st〉
    154157   | rtl_st_ext_call_ptr r1 r2 args dest ⇒
    155158      ! b ← block_of_register_pair r1 r2 st ;
Note: See TracChangeset for help on using the changeset viewer.