Changeset 1385 for src/RTL


Ignore:
Timestamp:
Oct 17, 2011, 1:40:13 AM (8 years ago)
Author:
sacerdot
Message:
  1. fetch_result and pop_frame now takes the genv in input
  2. implementation of fetch_result for RTL completed All RTL axioms but the ones related to external functions are now closed.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1384 r1385  
    3939  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
    4040
    41 
    42 (*CSC: XXXXX, for is_final only *)
    43 axiom rtl_fetch_result: state rtl_sem_params → res (list beval).
    44 (*  let ret_vals ≝ map … (λreg.greg_retrieve rtl_sem_params st reg) ret_val_regs in
    45 *)
     41definition rtl_fetch_result:
     42 ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (list beval) ≝
     43 λglobals,ge,st.
     44  do fn ← graph_fetch_function … globals ge st ;
     45  let ret_val_regs ≝ joint_if_result … fn in
     46   mmap … (λreg.greg_retrieve rtl_sem_params st reg) ret_val_regs.
    4647
    4748(*CSC: we could use a dependent type here: the list of return values should have
     
    4950  saves the OutOfBounds exception *)
    5051definition rtl_pop_frame:
    51  state … rtl_sem_params → res (state … rtl_sem_params) ≝
    52  λst.
    53   do ret_vals ← rtl_fetch_result … st ;
    54   let frms ≝ st_frms ? st in
    55   match frms with
     52 ∀globals. genv … (rtl_params globals) → state … rtl_sem_params → res (state … rtl_sem_params) ≝
     53 λglobals,ge,st.
     54  do ret_vals ← rtl_fetch_result … ge st ;
     55  match st_frms ? st with
    5656  [ nil ⇒ Error ? [MSG EmptyStack]
    5757  | cons hd tl ⇒
     
    9090definition rtl_more_sem_params1 : more_sem_params1 … rtl_params1 ≝
    9191 mk_more_sem_params1 ? rtl_params1 rtl_more_sem_params
    92   rtl_init_locals rtl_pop_frame rtl_save_frame.
     92  rtl_init_locals rtl_save_frame.
    9393
    9494(*CSC: XXXX, for external functions only*)
     
    118118 λglobals.
    119119  mk_more_sem_params2 … rtl_more_sem_params1
    120    (graph_fetch_statement …) rtl_fetch_ra rtl_fetch_result rtl_fetch_external_args
    121     rtl_set_result (rtl_exec_extended …).
     120   (graph_fetch_statement …) rtl_fetch_ra (rtl_fetch_result …)
     121   (rtl_pop_frame …) rtl_fetch_external_args rtl_set_result (rtl_exec_extended …).
    122122
    123123definition rtl_fullexec ≝
Note: See TracChangeset for help on using the changeset viewer.