Changeset 1298


Ignore:
Timestamp:
Oct 5, 2011, 9:41:42 PM (8 years ago)
Author:
sacerdot
Message:
  • fetch_statement now takes in input the globalenv
  • fetch_statement and rtl_succ implemented for RTL; the implementation should be generic enough to work on every graph language
Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1295 r1298  
    1212  pointer operations on labels are not semantically valid!! *)
    1313axiom rtl_pointer_of_label: label → Σp:pointer. ptype p = Code.
     14axiom rtl_label_of_pointer: pointer → res label.
    1415
    1516(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
     
    4445(*CSC: XXXXX *)
    4546axiom rtl_init_locals : list register → register_env beval.
    46 axiom rtl_fetch_statement: ∀globals. state rtl_sem_params → res (rtl_statement globals).
     47
     48axiom BadProgramCounter: String.
     49definition rtl_fetch_statement:
     50 ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (rtl_statement globals) ≝
     51 λglobals,ge,st.
     52  (*CSC: the next two lines implement pointer_of_address;
     53    duplicated twice in joint/semantics.ma *)
     54  let 〈v1,v2〉 ≝ pc … st in
     55  do p ← pointer_of_bevals [v1;v2] ;
     56
     57  let b ≝ pblock p in
     58  do l ← rtl_label_of_pointer p;
     59  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
     60  match def with
     61  [ Internal def' ⇒
     62     opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … def') l)
     63  | External _ ⇒ Error … [MSG BadProgramCounter]].
    4764
    4865axiom rtl_fetch_result: state rtl_sem_params → nat → res val.
     
    5471axiom rtl_exec_extended: ∀globals. genv globals (rtl_params globals) → rtl_statement_extension → state rtl_sem_params → IO io_out io_in (trace × (state rtl_sem_params)).
    5572
    56 definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) :=
     73definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals)
    5774 λglobals.
    5875  mk_more_sem_params2 … rtl_more_sem_params rtl_init_locals
  • src/joint/semantics.ma

    r1294 r1298  
    6060 ; init_locals : localsT p → regsT … more_sparams
    6161 
    62  ; fetch_statement: state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
     62 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
    6363 ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val
    6464
     
    205205definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
    206206 λglobals,p,ge,st.
    207   ! s ← fetch_statement … st;
     207  ! s ← fetch_statement … ge st;
    208208  match s with
    209209    [ GOTO l ⇒ ret ? 〈E0, goto … l st〉
     
    310310qed.
    311311
    312 definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option int ≝
    313  λglobals,p,exit,registersno,st. res_to_opt … (
    314   do s ← fetch_statement … st;
     312definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. genv … p → address → nat → state p → option int ≝
     313 λglobals,p,ge,exit,registersno,st.res_to_opt … (
     314  do s ← fetch_statement … ge st;
    315315  match s with
    316316   [ RETURN ⇒
     
    335335definition joint_exec: trans_system io_out io_in ≝
    336336  mk_trans_system … evaluation_parameters (λG. state (sparams2 G))
    337    (λG.is_final (globals G) (sparams2 G) (exit G) (registersno G))
     337   (λG.is_final (globals G) (sparams2 G) (genv2 G) (exit G) (registersno G))
    338338   (λG.eval_statement (globals G) (sparams2 G) (genv2 G)).
    339339
Note: See TracChangeset for help on using the changeset viewer.