Changeset 1451 for src/ERTL/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/ERTL/semantics.ma

    r1415 r1451  
    2323  (list (register_env beval)) [] ((register_env beval) × hw_register_env)
    2424   (λsp.〈empty_map …,init_hw_register_env sp〉) 0 it
    25    graph_succ_p
    2625   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
    2726    ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
     
    3332       match \fst dest_src with
    3433       [ pseudo reg ⇒ ps_reg_store reg v locals
    35        | hardware reg ⇒ hw_reg_store reg v locals])
    36      pointer_of_label.
     34       | hardware reg ⇒ hw_reg_store reg v locals]).
    3735definition ertl_sem_params: sem_params ≝ mk_sem_params … ertl_more_sem_params.
    3836
     
    9189  set_regs ertl_sem_params 〈\fst (regs … st),hwregs〉 st.
    9290
     91definition ertl_more_sem_params1: ∀globals. more_sem_params1 … (ertl_params globals) ≝
     92 λglobals.
     93  mk_more_sem_params1 … ertl_more_sem_params graph_succ_p (graph_pointer_of_label …)
     94    (graph_fetch_statement …) (load_ra …) (ertl_result_regs …)
     95    ertl_init_locals ertl_save_frame (ertl_pop_frame …)
     96    ertl_fetch_external_args ertl_set_result.
     97definition ertl_sem_params1: ∀globals. sem_params1 globals ≝
     98 λglobals. mk_sem_params1 … (ertl_more_sem_params1 globals).
     99
    93100definition ertl_exec_extended:
    94101 ∀globals. genv globals (ertl_params globals) →
     
    102109      ! newsp ← addr_sub sp v;
    103110      let st ≝ set_hwsp newsp st in
    104         ret ? 〈E0,goto … l st〉
     111      ! st ← next … (ertl_sem_params1 globals) l st ;
     112        ret ? 〈E0,st〉
    105113   | ertl_st_ext_del_frame ⇒
    106114      ! v ← framesize … ge st;
     
    108116      ! newsp ← addr_add sp v;
    109117      let st ≝ set_hwsp newsp st in
    110         ret ? 〈E0,goto … l st〉
     118      ! st ← next … (ertl_sem_params1 …) l st ;
     119        ret ? 〈E0,st〉
    111120   | ertl_st_ext_frame_size dst ⇒
    112121      ! v ← framesize … ge st;
    113122      ! st ← greg_store ertl_sem_params dst (BVByte (bitvector_of_nat … v)) st;
    114         ret ? 〈E0, goto … l st〉
     123      ! st ← next … (ertl_sem_params1 …) l st ;
     124        ret ? 〈E0, st〉
    115125   ].
    116126
    117127definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
    118  λglobals.
    119   mk_more_sem_params2 …
    120    (mk_more_sem_params1 … ertl_more_sem_params
    121     (graph_fetch_statement …) (load_ra …) (ertl_result_regs …)
    122     ertl_init_locals ertl_save_frame (ertl_pop_frame …)
    123     ertl_fetch_external_args ertl_set_result)
    124    (ertl_exec_extended …).
     128 λglobals. mk_more_sem_params2 … (ertl_more_sem_params1 …) (ertl_exec_extended …).
    125129
    126 definition ertl_fullexec
     130definition ertl_fullexec: fullexec io_out io_in
    127131 joint_fullexec … (λp. ertl_more_sem_params2 (prog_var_names … p)).
Note: See TracChangeset for help on using the changeset viewer.