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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.