Changeset 1372


Ignore:
Timestamp:
Oct 14, 2011, 2:48:34 PM (8 years ago)
Author:
sacerdot
Message:

save_frame now takes the stacksize to allow RTL to allocate the stack frame

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1371 r1372  
    5151     OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
    5252
    53 definition ertl_save_frame: nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
    54  λ_.λ_.λ_.λst.
     53definition ertl_save_frame: nat → nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
     54 λ_.λ_.λ_.λ_.λst.
    5555  OK …
    5656   (set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st))
  • src/LIN/semantics.ma

    r1371 r1372  
    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 → nat → unit → state … lin_sem_params → res (state … lin_sem_params) ≝ λ_.λ_.λ_.λst.OK … st.
     29definition lin_save_frame: nat → 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

    r1371 r1372  
    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 → nat → unit → state … ltl_sem_params → res (state … ltl_sem_params) ≝ λ_.λ_.λ_.λst.OK … st.
     24definition ltl_save_frame: nat → 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

    r1371 r1372  
    6262
    6363definition 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.
     64 nat → list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
     65 λstacksize,formal_arg_regs,actual_arg_regs,retregs,st.
     66  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
    6667  do new_regs ←
    6768   mfold_left2 …
     
    7374   (set_frms rtl_sem_params
    7475    (mk_frame retregs (pc … st) (sp … st) (carry … st) (regs … st) :: (st_frms … st))
    75      (set_regs rtl_sem_params new_regs st)).
     76     (set_regs rtl_sem_params new_regs
     77      (set_m … mem
     78       (set_sp … (mk_pointer XData b ? (mk_offset 0)) st)))).
     79cases daemon (*CSC: XXXX*)
     80qed.
    7681
    7782(*+ USARE GLI ARGSNO CHE SONO IN VERITA' I VALORI DEI PARAMETRI COME IN RTLABS
  • src/joint/semantics.ma

    r1371 r1372  
    5353   (*CSC: save_frame returns a res only because we can call a function with the wrong number and
    5454     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))
     55 ; save_frame: nat → paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
    5656 }.
    5757
     
    294294          [ Internal fn ⇒
    295295            ! st ← save_ra … st l;
    296             ! st ← save_frame … (joint_if_params … fn) args dest st ;
     296            ! st ← save_frame … (joint_if_stacksize … fn) (joint_if_params … fn) args dest st ;
    297297            let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    298298            let l' ≝ joint_if_entry … fn in
Note: See TracChangeset for help on using the changeset viewer.