Changeset 1300 for src/RTL


Ignore:
Timestamp:
Oct 5, 2011, 10:43:26 PM (8 years ago)
Author:
sacerdot
Message:

More (graph) axioms implemented. Look at the comments marked with XXX for
potential problems in the proof of preservation of the semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1299 r1300  
    1212axiom rtl_save_frame: unit → register_env beval → unit.
    1313
    14 
    15 axiom BadRegister : String.
    16 definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
    17 definition reg_retrieve : register_env beval → register → res beval ≝
    18  λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
    19 
    2014definition rtl_more_sem_params: more_sem_params rtl_params_ :=
    2115 mk_more_sem_params rtl_params_
    22   unit(*framesT*) (register_env beval) rtl_succ_p rtl_pop_frame rtl_save_frame
     16  unit(*framesT*) (register_env beval) graph_succ_p rtl_pop_frame rtl_save_frame
    2317   reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve
    2418    reg_store reg_retrieve reg_store reg_retrieve
     
    2620       do v ← reg_retrieve locals (\snd dest_src) ;
    2721       reg_store (\fst dest_src) v locals)
    28      rtl_pointer_of_label.
     22     pointer_of_label.
    2923definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
    3024
    3125(*CSC: XXXXX *)
    3226axiom rtl_init_locals : list register → register_env beval.
    33 
    34 axiom BadProgramCounter: String.
    35 definition rtl_fetch_statement:
    36  ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (rtl_statement globals) ≝
    37  λglobals,ge,st.
    38   (*CSC: the next two lines implement pointer_of_address;
    39     duplicated twice in joint/semantics.ma *)
    40   let 〈v1,v2〉 ≝ pc … st in
    41   do p ← pointer_of_bevals [v1;v2] ;
    42 
    43   let b ≝ pblock p in
    44   do l ← rtl_label_of_pointer p;
    45   do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
    46   match def with
    47   [ Internal def' ⇒
    48      opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … def') l)
    49   | External _ ⇒ Error … [MSG BadProgramCounter]].
    5027
    5128axiom rtl_fetch_result: state rtl_sem_params → nat → res val.
Note: See TracChangeset for help on using the changeset viewer.