Changeset 1415


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
Location:
src
Files:
1 added
5 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 ⇒
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1411 r1415  
    11include "LIN/joint_LTL_LIN.ma".
    22include "joint/SemanticUtils.ma".
     3
     4definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e).
     5definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r).
    36
    47(*CSC: re-organize to take succ_pc out of lin_more_sem_params? *)
     
    69 λsuccT,succ,pointer_of_label.
    710 mk_more_sem_params ?
    8   unit it hw_register_env empty_hw_register_env 0 it succ
    9    hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
    10     (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
    11     (λ_.hwreg_store RegisterDPL) (λe.λ_.hwreg_retrieve e RegisterDPL)
    12     (λ_.hwreg_store RegisterDPH) (λe.λ_.hwreg_retrieve e RegisterDPH)
     11  unit it hw_register_env init_hw_register_env 0 it succ
     12   hw_reg_store hw_reg_retrieve (λ_.hw_reg_store RegisterA) (λe.λ_.hw_reg_retrieve e RegisterA)
     13    (λ_.hw_reg_store RegisterB) (λe.λ_.hw_reg_retrieve e RegisterB)
     14    (λ_.hw_reg_store RegisterDPL) (λe.λ_.hw_reg_retrieve e RegisterDPL)
     15    (λ_.hw_reg_store RegisterDPH) (λe.λ_.hw_reg_retrieve e RegisterDPH)
    1316     (λlocals,dest_src.
    1417       match dest_src with
    1518       [ from_acc reg ⇒
    16           do v ← hwreg_retrieve locals RegisterA ;
    17           hwreg_store reg v locals
     19          do v ← hw_reg_retrieve locals RegisterA ;
     20          hw_reg_store reg v locals
    1821       | to_acc reg ⇒
    19           do v ← hwreg_retrieve locals reg ;
    20           hwreg_store RegisterA v locals ])
     22          do v ← hw_reg_retrieve locals reg ;
     23          hw_reg_store RegisterA v locals ])
    2124     pointer_of_label.
    2225
  • src/RTL/semantics.ma

    r1412 r1415  
    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*) graph_succ_p
    1717   reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve
    1818    reg_store reg_retrieve reg_store reg_retrieve
  • src/joint/SemanticUtils.ma

    r1408 r1415  
    1515axiom hw_register_env: Type[0]. (* CSC: use the one in I8051? *)
    1616axiom empty_hw_register_env: hw_register_env.
    17 axiom hwreg_retrieve : hw_register_env → Register → res beval.
    18 axiom hwreg_store : Register → beval → hw_register_env → res hw_register_env.
     17axiom hwreg_retrieve : hw_register_env → Register → beval.
     18axiom hwreg_store : Register → beval → hw_register_env → hw_register_env.
     19
     20definition init_hw_register_env: address → hw_register_env ≝
     21 λaddr.
     22  let 〈dpl,dph〉 ≝ addr in
     23  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
     24   hwreg_store RegisterDPL dpl env.
    1925
    2026(****************************************************************************)
  • src/joint/semantics.ma

    r1411 r1415  
    44include "common/SmallstepExec.ma".
    55include "joint/Joint.ma".
     6include "ASM/I8051bis.ma".
    67
    78(* CSC: external functions never fail (??) and always return something of the
     
    1415 ; empty_framesT: framesT
    1516 ; regsT: Type[0]
    16  ; empty_regsT: regsT
     17 ; empty_regsT: address → regsT (* Stack pointer *)
    1718 ; call_args_for_main: call_args p
    1819 ; call_dest_for_main: call_dest p
     
    396397  let ge ≝ genv2 sem_globals in
    397398  let m ≝ init_mem Genv … p in
    398   let dummy_pc ≝ 〈BVundef,BVundef〉 in
    399   let sp ≝ ? in
     399  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
     400  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
     401  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
     402  do sp ← address_of_pointer spp ;
    400403  let main ≝ prog_main … p in
    401   let st0 ≝ mk_state … (empty_framesT …) dummy_pc sp BVfalse (empty_regsT …) m in
     404  let st0 ≝ mk_state … (empty_framesT …) sp dummy_pc BVfalse (empty_regsT … sp) m in
    402405  let trace_state ≝
    403406   eval_call_id … (mk_sem_params1 … (sparams …)) ge st0 main (call_args_for_main … (sparams …))
     
    408411  | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
    409412  ].
    410 cases daemon qed.
     413[2: % | cases spb *; #r #off #E >E %]
     414qed.
    411415(*
    412416RTL:
Note: See TracChangeset for help on using the changeset viewer.