Changeset 1300 for src/joint


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/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.