source: src/joint/SemanticUtils.ma @ 1300

Last change on this file since 1300 was 1300, checked in by sacerdot, 8 years ago

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

File size: 2.4 KB
Line 
1include "joint/semantics.ma".
2
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))))).
32
33(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
34  Maybe there is a better way to organize the code!!! *)
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 ⊢ (???% → ?)
38  [ #res #_ @res
39  | #msg cases (pointer_of_label l) * * #q #com #off #E1 #E2 destruct ]
40qed.
41
42axiom BadProgramCounter: String.
43definition graph_fetch_statement:
44 ∀params1,sem_params,globals.
45  genv … (graph_params params1 globals) →
46   state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
47 λparams1,sem_params,globals,ge,st.
48  (*CSC: the next two lines implement pointer_of_address;
49    duplicated twice in joint/semantics.ma *)
50  let 〈v1,v2〉 ≝ pc … st in
51  do p ← pointer_of_bevals [v1;v2] ;
52
53  let b ≝ pblock p in
54  do l ← label_of_pointer p;
55  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
56  match def with
57  [ Internal def' ⇒
58     opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … def') l)
59  | External _ ⇒ Error … [MSG BadProgramCounter]].
Note: See TracBrowser for help on using the repository browser.