Changeset 1415 for src/ERTL


Ignore:
Timestamp:
Oct 19, 2011, 4:22:52 PM (8 years ago)
Author:
sacerdot
Message:
  1. hwreg_store/retrieve no longer returns a res (but it is still axiomatized)
  2. added initialization of local environment that sets the sp in the appropriate way
  3. ASM/I8051 splitted into ASM/I8051bis because of some bugs with disambiguation
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1411 r1415  
    1313definition hw_reg_store ≝
    1414 λr,v.λlocal_env:(register_env beval) × hw_register_env.
    15   do res ← hwreg_store r v (\snd local_env) ;
    16   OK … 〈\fst local_env,res〉.
     15  OK … 〈\fst local_env,hwreg_store r v (\snd local_env)〉.
    1716
    1817definition hw_reg_retrieve ≝
    19  λlocal_env:(register_env beval) × hw_register_env. hwreg_retrieve … (\snd local_env).
     18 λlocal_env:(register_env beval) × hw_register_env.λreg.
     19  OK … (hwreg_retrieve … (\snd local_env) reg).
    2020
    2121definition ertl_more_sem_params: more_sem_params ertl_params_ :=
    2222 mk_more_sem_params ertl_params_
    2323  (list (register_env beval)) [] ((register_env beval) × hw_register_env)
    24    〈empty_map …,empty_hw_register_env〉 0 it
     24   (λsp.〈empty_map …,init_hw_register_env sp〉) 0 it
    2525   graph_succ_p
    2626   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
     
    7878   OK ? (joint_if_stacksize globals … f).
    7979
    80 definition get_hwsp : state ertl_sem_params → res address ≝
     80definition get_hwsp : state ertl_sem_params → address ≝
    8181 λst.
    82   do spl ← hwreg_retrieve (\snd (regs … st)) RegisterSPL ;
    83   do sph ← hwreg_retrieve (\snd (regs … st)) RegisterSPH ;
    84   OK ? 〈spl,sph〉.
     82  let spl ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPL in
     83  let sph ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPH in
     84  〈spl,sph〉.
    8585
    86 definition set_hwsp : address → state ertl_sem_params → res (state ertl_sem_params)
     86definition set_hwsp : address → state ertl_sem_params → state ertl_sem_params
    8787 λsp,st.
    8888  let 〈spl,sph〉 ≝ sp in
    89   do hwregs ← hwreg_store RegisterSPL spl (\snd (regs … st)) ;
    90   do hwregs ← hwreg_store RegisterSPH sph hwregs ;
    91   OK ? (set_regs ertl_sem_params 〈\fst (regs … st),hwregs〉 st).
     89  let hwregs ≝ hwreg_store RegisterSPL spl (\snd (regs … st)) in
     90  let hwregs ≝ hwreg_store RegisterSPH sph hwregs in
     91  set_regs ertl_sem_params 〈\fst (regs … st),hwregs〉 st.
    9292
    9393definition ertl_exec_extended:
     
    9999   [ ertl_st_ext_new_frame ⇒
    100100      ! v ← framesize globals … ge st;
    101       ! sp ← get_hwsp st;
     101      let sp ≝ get_hwsp st in
    102102      ! newsp ← addr_sub sp v;
    103       ! st ← set_hwsp newsp st;
     103      let st ≝ set_hwsp newsp st in
    104104        ret ? 〈E0,goto … l st〉
    105105   | ertl_st_ext_del_frame ⇒
    106106      ! v ← framesize … ge st;
    107       ! sp ← get_hwsp st;
     107      let sp ≝ get_hwsp st in
    108108      ! newsp ← addr_add sp v;
    109       ! st ← set_hwsp newsp st;
     109      let st ≝ set_hwsp newsp st in
    110110        ret ? 〈E0,goto … l st〉
    111111   | ertl_st_ext_frame_size dst ⇒
Note: See TracChangeset for help on using the changeset viewer.