Changeset 1298 for src/RTL/semantics.ma


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
File:
1 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
Note: See TracChangeset for help on using the changeset viewer.