Changeset 1371 for src/RTL


Ignore:
Timestamp:
Oct 14, 2011, 1:42:42 PM (9 years ago)
Author:
sacerdot
Message:

save_frame changed to accept also the formal/actual argument pairs, required
in the RTL semantics. The function returns now a res, but this could be fixed
with a dependent type for function call to disallow calling a function with the
wrong arguments.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1359 r1371  
    99include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
    1010include alias "common/Identifiers.ma".
    11 
    12 (* CSC: a streamlined version of the ERTL state *)
     11include alias "ASM/Util.ma".
     12
    1313record frame: Type[0] ≝
    1414 { fr_ret_regs: list register
     
    3232definition rtl_init_locals :
    3333 list register → register_env beval → register_env beval ≝
    34  λlocals.λ_.
    35   foldl ?? (λlenv,reg. add … lenv reg BVundef) (empty_map …) locals.
     34 λlocals,env.
     35  foldl ?? (λlenv,reg. add … lenv reg BVundef) env locals.
    3636
    3737(*CSC: could we use here a dependent type to avoid the Error case? *)
    3838axiom EmptyStack: String.
    3939axiom OutOfBounds: String.
    40 include alias "ASM/Util.ma".
    4140
    4241(*CSC: we could use a dependent type here: the list of return values should have
     
    6261          (set_carry … (fr_carry hd) st))))) ].
    6362
    64 definition rtl_save_frame: list register → state … rtl_sem_params → state … rtl_sem_params ≝
    65  λretregs.λst.
    66   set_frms rtl_sem_params
    67    (mk_frame retregs (pc … st) (sp … st) (carry … st) (regs ? st) :: (st_frms … st)) st.
     63definition rtl_save_frame:
     64 list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
     65 λformal_arg_regs,actual_arg_regs,retregs,st.
     66  do new_regs ←
     67   mfold_left2 …
     68    (λlenv,dest,src.
     69      do v ← greg_retrieve … st src ;
     70      OK … (add … lenv dest v))
     71    (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
     72  OK …
     73   (set_frms rtl_sem_params
     74    (mk_frame retregs (pc … st) (sp … st) (carry … st) (regs … st) :: (st_frms … st))
     75     (set_regs rtl_sem_params new_regs st)).
     76
     77(*+ USARE GLI ARGSNO CHE SONO IN VERITA' I VALORI DEI PARAMETRI COME IN RTLABS
     78+ ALLOCARE LO STACK FRAME*)
    6879
    6980definition rtl_more_sem_params1 : more_sem_params1 … rtl_params1 ≝
    7081 mk_more_sem_params1 ? rtl_params1 rtl_more_sem_params
    7182  rtl_init_locals rtl_pop_frame rtl_save_frame.
    72 
    7383
    7484(*CSC: XXXXX, for is_final only *)
Note: See TracChangeset for help on using the changeset viewer.