Changeset 1327


Ignore:
Timestamp:
Oct 7, 2011, 4:15:42 PM (8 years ago)
Author:
sacerdot
Message:

More progress in the implementation of the ERTL specific statements.
The file does not compile ATM because of unimplemented addr_sub and addr_add.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1324 r1327  
    6565axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params).
    6666
    67 axiom ertl_exec_extended: ∀globals. genv globals (ertl_params globals) → ertl_statement_extension → label → state ertl_sem_params → IO io_out io_in (trace × (state ertl_sem_params)).
     67(*CSC: XXXX *)
     68axiom framesize: list ident → state ertl_sem_params → res nat. (* ≝
     69  λglobals: list ident.
     70  λst.
     71   do f ← fetch_function globals st ;
     72   OK ? (joint_if_stacksize globals … f).*)
     73
     74definition get_hwsp : state ertl_sem_params → res address ≝
     75 λst.
     76  do spl ← hwreg_retrieve (\snd (regs … st)) RegisterSPL ;
     77  do sph ← hwreg_retrieve (\snd (regs … st)) RegisterSPH ;
     78  OK ? 〈spl,sph〉.
     79
     80definition set_hwsp : address → state ertl_sem_params → res (state ertl_sem_params) ≝
     81 λsp,st.
     82  let 〈spl,sph〉 ≝ sp in
     83  do hwregs ← hwreg_store RegisterSPL spl (\snd (regs … st)) ;
     84  do hwregs ← hwreg_store RegisterSPH sph hwregs ;
     85  OK ? (set_regs ertl_sem_params 〈\fst (regs … st),hwregs〉 st).
     86
     87definition ertl_exec_extended:
     88 ∀globals. genv globals (ertl_params globals) →
     89  ertl_statement_extension → label → state ertl_sem_params →
     90   IO io_out io_in (trace × (state ertl_sem_params)) ≝
     91 λglobals,ge,stm,l,st.
     92  match stm with
     93   [ ertl_st_ext_new_frame ⇒
     94      ! v ← framesize globals st;
     95      ! sp ← get_hwsp st;
     96        let newsp ≝ ?(*addr_sub sp v*) in
     97      ! st ← set_hwsp newsp st;
     98        ret ? 〈E0,goto … l st〉
     99   | ertl_st_ext_del_frame ⇒
     100      ! v ← framesize globals st;
     101      ! sp ← get_hwsp st;
     102        let newsp ≝ ?(*addr_add sp v*) in
     103      ! st ← set_hwsp newsp st;
     104        ret ? 〈E0,goto … l st〉
     105   | ertl_st_ext_frame_size dst ⇒
     106      ! v ← framesize globals st;
     107      ! st ← greg_store ertl_sem_params dst (BVByte (bitvector_of_nat … v)) st;
     108        ret ? 〈E0, goto … l st〉
     109   ].
     110qed.
    68111
    69112definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
Note: See TracChangeset for help on using the changeset viewer.