Changeset 1377 for src/RTL


Ignore:
Timestamp:
Oct 14, 2011, 7:22:59 PM (9 years ago)
Author:
sacerdot
Message:

pop_frame now incorporates the fetch_result (that made sense only for RTL).
pop_frame and save_frame are now also more symmetric

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1376 r1377  
    3939axiom OutOfBounds: String.
    4040
     41(*CSC: XXXXX, for is_final only *)
     42axiom rtl_fetch_result: state rtl_sem_params → res (list beval).
     43(*  let ret_vals ≝ map … (λreg.greg_retrieve rtl_sem_params st reg) ret_val_regs in
     44*)
     45
    4146(*CSC: we could use a dependent type here: the list of return values should have
    4247  the same length of the list of return registers that store the values. This
    4348  saves the OutOfBounds exception *)
    44 definition rtl_pop_frame: list beval → state … rtl_sem_params → res (state … rtl_sem_params) ≝
    45  λret_vals,st.
     49definition rtl_pop_frame:
     50 state … rtl_sem_params → res ((state … rtl_sem_params) × address) ≝
     51 λst.
     52  do ret_vals ← rtl_fetch_result … st ;
    4653  let frms ≝ st_frms ? st in
    4754  match frms with
     
    5562       (OK … st) (fr_ret_regs hd) ;
    5663     OK …
    57       (set_frms rtl_sem_params tl
    58        (set_regs rtl_sem_params (fr_regs hd)
    59         (set_sp … (fr_sp hd)
    60          (set_pc … (fr_pc hd)
     64      〈set_frms rtl_sem_params tl
     65        (set_regs rtl_sem_params (fr_regs hd)
     66         (set_sp … (fr_sp hd)
    6167          (set_carry … (fr_carry hd)
    62            (set_m … (free … (m … st) (pblock (sp … st))) st)))))) ].
     68           (set_m … (free … (m … st) (pblock (sp … st))) st)))),
     69       fr_pc hd〉 ].
    6370
    6471definition rtl_save_frame:
    65  nat → list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
    66  λstacksize,formal_arg_regs,actual_arg_regs,retregs,st.
     72 address → nat → list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
     73 λl,stacksize,formal_arg_regs,actual_arg_regs,retregs,st.
    6774  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
    6875  do new_regs ←
     
    7481  OK …
    7582   (set_frms rtl_sem_params
    76     (mk_frame retregs (pc … st) (sp … st) (carry … st) (regs … st) :: (st_frms … st))
     83    (mk_frame retregs l (sp … st) (carry … st) (regs … st) :: (st_frms … st))
    7784     (set_regs rtl_sem_params new_regs
    7885      (set_m … mem
     
    8491 mk_more_sem_params1 ? rtl_params1 rtl_more_sem_params
    8592  rtl_init_locals rtl_pop_frame rtl_save_frame.
    86 
    87 (*CSC: XXXXX, for is_final only *)
    88 axiom rtl_fetch_result: state rtl_sem_params → res (list beval).
    89 (*  let ret_vals ≝ map … (λreg.greg_retrieve rtl_sem_params st reg) ret_val_regs in
    90 *)
    9193
    9294(*CSC: XXXX, for external functions only*)
Note: See TracChangeset for help on using the changeset viewer.