Changeset 1359 for src/RTL/semantics.ma


Ignore:
Timestamp:
Oct 11, 2011, 6:00:03 PM (9 years ago)
Author:
sacerdot
Message:
  1. more work on the RTL semantics
  2. changes to joint/semantics to accomodate the RTL one
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1326 r1359  
    88*)
    99include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
     10include alias "common/Identifiers.ma".
    1011
    1112(* CSC: a streamlined version of the ERTL state *)
    1213record frame: Type[0] ≝
    13  { fr_pc: address
     14 { fr_ret_regs: list register
     15 ; fr_pc: address
    1416 ; fr_sp: pointer
    1517 ; fr_carry: beval
     
    3537(*CSC: could we use here a dependent type to avoid the Error case? *)
    3638axiom EmptyStack: String.
    37 definition rtl_pop_frame: state … rtl_sem_params → res (state … rtl_sem_params) ≝
    38  λst.
     39axiom OutOfBounds: String.
     40include alias "ASM/Util.ma".
     41
     42(*CSC: we could use a dependent type here: the list of return values should have
     43  the same length of the list of return registers that store the values. This
     44  saves the OutOfBounds exception *)
     45definition rtl_pop_frame: list beval → state … rtl_sem_params → res (state … rtl_sem_params) ≝
     46 λret_vals,st.
    3947  let frms ≝ st_frms ? st in
    4048  match frms with
    4149  [ nil ⇒ Error ? [MSG EmptyStack]
    4250  | cons hd tl ⇒
     51     do st ←
     52      mfold_left_i ??
     53       (λi.λst.λreg.
     54         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
     55         greg_store rtl_sem_params reg v st)
     56       (OK … st) (fr_ret_regs hd) ;
    4357     OK …
    4458      (set_frms rtl_sem_params tl
     
    4862          (set_carry … (fr_carry hd) st))))) ].
    4963
    50 definition rtl_save_frame: state … rtl_sem_params → state … rtl_sem_params ≝
    51  λst.
     64definition rtl_save_frame: list register → state … rtl_sem_params → state … rtl_sem_params ≝
     65 λretregs.λst.
    5266  set_frms rtl_sem_params
    53    (mk_frame (pc … st) (sp … st) (carry … st) (regs ? st) :: (st_frms … st)) st.
     67   (mk_frame retregs (pc … st) (sp … st) (carry … st) (regs ? st) :: (st_frms … st)) st.
    5468
    5569definition rtl_more_sem_params1 : more_sem_params1 … rtl_params1 ≝
     
    5973
    6074(*CSC: XXXXX, for is_final only *)
    61 axiom rtl_fetch_result: state rtl_sem_params → nat → res val.
     75axiom rtl_fetch_result: state rtl_sem_params → res (list beval).
     76(*  let ret_vals ≝ map … (λreg.greg_retrieve rtl_sem_params st reg) ret_val_regs in
     77*)
    6278
    6379(*CSC: XXXX, for external functions only*)
Note: See TracChangeset for help on using the changeset viewer.