Changeset 1384 for src/joint


Ignore:
Timestamp:
Oct 16, 2011, 7:42:25 PM (8 years ago)
Author:
sacerdot
Message:
  • fetch_ra taken out of pop_frame again since it is used uniformly and it is also required for is_final
  • fetch_ra made abstract since it gets a different implementation in RTL
  • old fetch_ra renamed into load_ra (to match the save_ra name)
Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/SemanticUtils.ma

    r1383 r1384  
    6161  do p ← pointer_of_address (pc … st) ;
    6262  let b ≝ pblock p in
    63   do l ← label_of_pointer p;
    6463  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
    6564  match def with
    6665  [ Internal def' ⇒
     66     do l ← label_of_pointer p;
    6767     opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … def') l)
    6868  | External _ ⇒ Error … [MSG BadProgramCounter]].
  • src/joint/semantics.ma

    r1383 r1384  
    5252
    5353 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
    54  ; pop_frame: state (mk_sem_params … more_sparams) → res ((state (mk_sem_params … more_sparams)) × address)
     54 ; pop_frame: state (mk_sem_params … more_sparams) → res ((state (mk_sem_params … more_sparams)))
    5555   (*CSC: save_frame returns a res only because we can call a function with the wrong number and
    5656     type of arguments. To be fixed using a dependent type *)
     
    7474
    7575 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams1) → res (joint_statement (mk_sem_params … more_sparams1) globals)
     76
     77 ; fetch_ra: state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)) × address)
    7678 ; fetch_result: state (mk_sem_params … more_sparams1) → res (list beval)
    7779
     
    204206  push … st addrh.
    205207
    206 definition fetch_ra : ∀p.state p → res (state p × address) ≝
     208definition load_ra : ∀p.state p → res (state p × address) ≝
    207209 λp,st.
    208210  do 〈st,addrh〉 ← pop … st;
     
    338340          ]]
    339341    | RETURN ⇒
    340       ! 〈st,ra〉 ← pop_frame … st;
     342      ! 〈st,ra〉 ← fetch_ra … st;
     343      ! st ← pop_frame … st;
    341344        ret ? 〈E0,set_pc … ra st〉].
    342345cases addr //
     
    348351  match s with
    349352   [ RETURN ⇒
    350       do 〈st,l〉 ← fetch_ra … st;
    351       if eq_address l exit then
     353      do 〈st,ra〉 ← fetch_ra … st;
     354      if eq_address ra exit then
    352355       do vals ← fetch_result … st ;
    353356       Word_of_list_beval vals
Note: See TracChangeset for help on using the changeset viewer.