Changeset 1377


Ignore:
Timestamp:
Oct 14, 2011, 7:22:59 PM (8 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

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1372 r1377  
    4343(*CSC: could we use here a dependent type to avoid the Error case? *)
    4444axiom EmptyStack: String.
    45 definition ertl_pop_frame: list beval → state … ertl_sem_params → res (state … ertl_sem_params) ≝
    46  λ_.λst.
     45definition ertl_pop_frame: state … ertl_sem_params → res ((state … ertl_sem_params) × address) ≝
     46 λst.
     47  do 〈st,ra〉 ← fetch_ra … st;
    4748  let frms ≝ st_frms ? st in
    4849  match frms with
    4950  [ nil ⇒ Error ? [MSG EmptyStack]
    5051  | cons hd tl ⇒
    51      OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
    52 
    53 definition ertl_save_frame: nat → nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
    54  λ_.λ_.λ_.λ_.λst.
     52     OK … (〈set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st),ra〉) ].
     53
     54definition ertl_save_frame:
     55 address → nat → nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝
     56 λl.λ_.λ_.λ_.λ_.λst.
     57  do st ← save_ra … st l ;
    5558  OK …
    5659   (set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st))
  • src/LIN/semantics.ma

    r1372 r1377  
    2626
    2727definition lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    28 definition lin_pop_frame: list beval → state … lin_sem_params → res (state … lin_sem_params) ≝ λ_.λst. OK … st.
    29 definition lin_save_frame: nat → unit → nat → unit → state … lin_sem_params → res (state … lin_sem_params) ≝ λ_.λ_.λ_.λ_.λst.OK … st.
     28definition lin_pop_frame: state … lin_sem_params → res ((state … lin_sem_params) × address) ≝
     29 fetch_ra ….
     30definition lin_save_frame:
     31 address → nat → unit → nat → unit → state … lin_sem_params → res (state … lin_sem_params) ≝
     32 λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
    3033
    3134definition lin_more_sem_params1 : more_sem_params1 … lin_params1 ≝
  • src/LTL/semantics.ma

    r1372 r1377  
    2121
    2222definition ltl_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    23 definition ltl_pop_frame: list beval → state … ltl_sem_params → res (state … ltl_sem_params) ≝ λ_.λst. OK … st.
    24 definition ltl_save_frame: nat → unit → nat → unit → state … ltl_sem_params → res (state … ltl_sem_params) ≝ λ_.λ_.λ_.λ_.λst.OK … st.
     23definition ltl_pop_frame: state … ltl_sem_params → res ((state … ltl_sem_params) × address) ≝
     24 fetch_ra ….
     25definition ltl_save_frame:
     26 address → nat → unit → nat → unit → state … ltl_sem_params → res (state … ltl_sem_params) ≝
     27 λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
    2528
    2629definition ltl_more_sem_params1 : more_sem_params1 … ltl_params1 ≝
  • 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*)
  • src/joint/semantics.ma

    r1376 r1377  
    4848 { more_sparams :> more_sem_params (mk_params_ p succT)
    4949
    50    (* Functions that manipulate the st_frms component of the state *)
    5150 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
    52  ; pop_frame: list beval → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
     51 ; pop_frame: state (mk_sem_params … more_sparams) → res ((state (mk_sem_params … more_sparams)) × address)
    5352   (*CSC: save_frame returns a res only because we can call a function with the wrong number and
    5453     type of arguments. To be fixed using a dependent type *)
    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))
     54 ; save_frame: address → nat → paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
    5655 }.
    5756
     
    194193  OK ? 〈st,v〉.
    195194
    196 definition save_ra : ∀p. state p → succ p → res (state p) ≝
     195definition save_ra : ∀p. state p → address → res (state p) ≝
    197196 λp,st,l.
    198   let 〈addrl,addrh〉 ≝ succ_pc … (more_sem_pars p) l (pc … st) in
     197  let 〈addrl,addrh〉 ≝ l in
    199198  do st ← push … st addrl;
    200199  push … st addrh.
     
    293292          match fd with
    294293          [ Internal fn ⇒
    295             ! st ← save_ra … st l;
    296             ! st ← save_frame … (joint_if_stacksize … fn) (joint_if_params … fn) args dest st ;
     294            let l ≝ succ_pc … (more_sem_pars p) l (pc … st) in
     295            ! st ← save_frame … l (joint_if_stacksize … fn) (joint_if_params … fn) args dest st ;
    297296            let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    298297            let l' ≝ joint_if_entry … fn in
     
    309308          ]]
    310309    | RETURN ⇒
    311       ! res ← fetch_result … st;
    312       ! st ← pop_frame … res st;
    313       ! 〈st,pch〉 ← pop … st;
    314       ! 〈st,pcl〉 ← pop … st;
    315         ret ? 〈E0,set_pc … 〈pcl,pch〉 st〉].
     310      ! 〈st,ra〉 ← pop_frame … st;
     311        ret ? 〈E0,set_pc … ra st〉].
    316312cases addr //
    317313qed.
Note: See TracChangeset for help on using the changeset viewer.