Changeset 1371


Ignore:
Timestamp:
Oct 14, 2011, 1:42:42 PM (8 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.

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1359 r1371  
    5151     OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
    5252
    53 definition ertl_save_frame: unit → state … ertl_sem_params → state … ertl_sem_params ≝
    54  λ_.λst.
    55   set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st)) st.
     53definition ertl_save_frame: nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
     54 λ_.λ_.λ_.λst.
     55  OK …
     56   (set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st))
     57    (set_regs ertl_sem_params 〈empty_map …,\snd (regs … st)〉 st)).
    5658
    5759definition ertl_more_sem_params1 : more_sem_params1 … ertl_params1 ≝
  • src/LIN/semantics.ma

    r1359 r1371  
    2727definition lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    2828definition lin_pop_frame: list beval → state … lin_sem_params → res (state … lin_sem_params) ≝ λ_.λst. OK … st.
    29 definition lin_save_frame: unit → state … lin_sem_params → state … lin_sem_params ≝ λ_.λst.st.
     29definition lin_save_frame: unit → nat → unit → state … lin_sem_params → res (state … lin_sem_params) ≝ λ_.λ_.λ_.λst.OK … st.
    3030
    3131definition lin_more_sem_params1 : more_sem_params1 … lin_params1 ≝
  • src/LTL/semantics.ma

    r1359 r1371  
    2222definition ltl_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    2323definition ltl_pop_frame: list beval → state … ltl_sem_params → res (state … ltl_sem_params) ≝ λ_.λst. OK … st.
    24 definition ltl_save_frame: unit → state … ltl_sem_params → state … ltl_sem_params ≝ λ_.λst.st.
     24definition ltl_save_frame: unit → nat → unit → state … ltl_sem_params → res (state … ltl_sem_params) ≝ λ_.λ_.λ_.λst.OK … st.
    2525
    2626definition ltl_more_sem_params1 : more_sem_params1 … ltl_params1 ≝
  • 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 *)
  • src/joint/semantics.ma

    r1359 r1371  
    5151 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
    5252 ; pop_frame: list beval → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
    53  ; save_frame: call_dest p → state (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams)
     53   (*CSC: save_frame returns a res only because we can call a function with the wrong number and
     54     type of arguments. To be fixed using a dependent type *)
     55 ; save_frame: paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
    5456 }.
    5557
     
    286288        ! st ← pair_reg_move … st dst_src ;
    287289          ret ? 〈E0, next … l st〉
    288       | CALL_ID id argsno dest ⇒
     290      | CALL_ID id args dest ⇒
    289291        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    290292        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
     
    292294          [ Internal fn ⇒
    293295            ! st ← save_ra … st l;
    294               let st ≝ save_frame … dest st in
    295               let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    296 (*+ USARE GLI ARGSNO CHE SONO IN VERITA' I VALORI DEI PARAMETRI COME IN RTLABS
    297 + ALLOCARE LO STACK FRAME*)
    298               let l' ≝ joint_if_entry … fn in
     296            ! st ← save_frame … (joint_if_params … fn) args dest st ;
     297            let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
     298            let l' ≝ joint_if_entry … fn in
    299299             ret ? 〈 E0, goto … l' (set_regs p regs st)〉
    300300          | External fn ⇒
Note: See TracChangeset for help on using the changeset viewer.