Changeset 1300


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.

Location:
src
Files:
2 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.
  • src/joint/SemanticUtils.ma

    r1299 r1300  
    11include "joint/semantics.ma".
    22
    3 (*CSC: XXXX; we need to create a brand new chunk per label, so that
    4   pointer operations on labels are not semantically valid!! *)
    5 axiom rtl_pointer_of_label: label → Σp:pointer. ptype p = Code.
    6 axiom rtl_label_of_pointer: pointer → res label.
     3(*** Store/retrieve on registers ***)
     4
     5axiom BadRegister : String.
     6
     7definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
     8
     9definition reg_retrieve : register_env beval → register → res beval ≝
     10 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
     11
     12(****************************************************************************)
     13
     14(*CSC: XXXX; do we need to create a brand new chunk per label, so that
     15  pointer operations on labels are not semantically valid?
     16  ATM, the pointers are not valid (they do not point to allocated regions)
     17  and, moreover, they conflict with function blocks and with other pointers
     18  in other functions. However, there could be simpler ways to invalidate
     19  pointer arithmetics on Code pointers.
     20*)
     21definition pointer_of_label: label → Σp:pointer. ptype p = Code ≝
     22 λl.
     23  mk_pointer Code
     24   (mk_block Code (Zopp (nat_of_bitvector ? (word_of_identifier … l))))
     25   ? (mk_offset OZ).
     26// qed.
     27
     28(*CSC: XXXX; inverse of the previous function, but it does not check that
     29  the offset is zero and thus it never fails. *)
     30definition label_of_pointer: pointer → res label ≝
     31 λp. OK … (an_identifier ? (bitvector_of_nat … (abs (block_id (pblock p))))).
    732
    833(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
    934  Maybe there is a better way to organize the code!!! *)
    10 definition rtl_succ_p: label → address → address.
    11  #l #_ generalize in match (refl … (beval_pair_of_pointer (rtl_pointer_of_label l)))
    12  cases (beval_pair_of_pointer (rtl_pointer_of_label l)) in ⊢ (???% → ?)
     35definition graph_succ_p: label → address → address.
     36 #l #_ generalize in match (refl … (beval_pair_of_pointer (pointer_of_label l)))
     37 cases (beval_pair_of_pointer (pointer_of_label l)) in ⊢ (???% → ?)
    1338  [ #res #_ @res
    14   | #msg cases (rtl_pointer_of_label l) * * #q #com #off #E1 #E2 destruct ]
     39  | #msg cases (pointer_of_label l) * * #q #com #off #E1 #E2 destruct ]
    1540qed.
    1641
     
    2752
    2853  let b ≝ pblock p in
    29   do l ← rtl_label_of_pointer p;
     54  do l ← label_of_pointer p;
    3055  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
    3156  match def with
Note: See TracChangeset for help on using the changeset viewer.