Changeset 1384


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
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1381 r1384  
    4343(*CSC: could we use here a dependent type to avoid the Error case? *)
    4444axiom EmptyStack: String.
    45 definition ertl_pop_frame: state … ertl_sem_params → res ((state … ertl_sem_params) × address) ≝
     45definition ertl_pop_frame: state … ertl_sem_params → res (state … ertl_sem_params) ≝
    4646 λst.
    47   do 〈st,ra〉 ← fetch_ra … st;
    4847  let frms ≝ st_frms ? st in
    4948  match frms with
    5049  [ nil ⇒ Error ? [MSG EmptyStack]
    5150  | cons hd tl ⇒
    52      OK … (〈set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st),ra〉) ].
     51     OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ].
    5352
    5453definition ertl_save_frame:
     
    118117 λglobals.
    119118  mk_more_sem_params2 … ertl_more_sem_params1
    120    (graph_fetch_statement …) ertl_fetch_result ertl_fetch_external_args ertl_set_result
    121     (ertl_exec_extended …).
     119   (graph_fetch_statement …) (load_ra …) ertl_fetch_result
     120    ertl_fetch_external_args ertl_set_result (ertl_exec_extended …).
    122121
    123122definition ertl_fullexec ≝
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1383 r1384  
    2828definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    2929definition ltl_lin_pop_frame:
    30  ∀succT,succ,pointer_of_label. state … (ltl_lin_sem_params succT succ pointer_of_label) → res ((state … (ltl_lin_sem_params … succ pointer_of_label)) × address) ≝
    31  λ_.λ_.λ_.fetch_ra ….
     30 ∀succT,succ,pointer_of_label. state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝
     31 λ_.λ_.λ_.λt.OK … t.
    3232definition ltl_lin_save_frame:
    3333 ∀succT,succ,pointer_of_label. address → nat → unit → nat → unit → state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝
     
    5555 λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
    5656  mk_more_sem_params2 … (ltl_lin_more_sem_params1 … succ pointer_of_label)
    57    (fetch globals) (ltl_lin_fetch_result …) (ltl_lin_fetch_external_args …)
     57   (fetch globals) (load_ra …) (ltl_lin_fetch_result …)
     58   (ltl_lin_fetch_external_args …)
    5859   (ltl_lin_set_result …) (ltl_lin_exec_extended …).
    5960
  • src/RTL/semantics.ma

    r1381 r1384  
    3232axiom OutOfBounds: String.
    3333
     34definition rtl_fetch_ra:
     35 state … rtl_sem_params → res ((state … rtl_sem_params) × address) ≝
     36 λst.
     37  match st_frms ? st with
     38  [ nil ⇒ Error ? [MSG EmptyStack]
     39  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
     40
     41
    3442(*CSC: XXXXX, for is_final only *)
    3543axiom rtl_fetch_result: state rtl_sem_params → res (list beval).
     
    4149  saves the OutOfBounds exception *)
    4250definition rtl_pop_frame:
    43  state … rtl_sem_params → res ((state … rtl_sem_params) × address) ≝
     51 state … rtl_sem_params → res (state … rtl_sem_params) ≝
    4452 λst.
    4553  do ret_vals ← rtl_fetch_result … st ;
     
    5563       (OK … st) (fr_ret_regs hd) ;
    5664     OK …
    57       set_frms rtl_sem_params tl
     65      (set_frms rtl_sem_params tl
    5866        (set_regs rtl_sem_params (fr_regs hd)
    5967         (set_sp … (fr_sp hd)
    6068          (set_carry … (fr_carry hd)
    61            (set_m … (free … (m … st) (pblock (sp … st))) st)))),
    62        fr_pc hd〉 ].
     69           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
    6370
    6471definition rtl_save_frame:
     
    111118 λglobals.
    112119  mk_more_sem_params2 … rtl_more_sem_params1
    113    (graph_fetch_statement …) rtl_fetch_result rtl_fetch_external_args rtl_set_result
    114     (rtl_exec_extended …).
     120   (graph_fetch_statement …) rtl_fetch_ra rtl_fetch_result rtl_fetch_external_args
     121    rtl_set_result (rtl_exec_extended …).
    115122
    116123definition rtl_fullexec ≝
  • 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.