1 | include "joint/semantics.ma". |
---|
2 | |
---|
3 | (*** Store/retrieve on pseudo-registers ***) |
---|
4 | |
---|
5 | axiom BadRegister : String. |
---|
6 | |
---|
7 | definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v. |
---|
8 | |
---|
9 | definition reg_retrieve : register_env beval → register → res beval ≝ |
---|
10 | λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg). |
---|
11 | |
---|
12 | (*** Store/retrieve on hardware registers ***) |
---|
13 | |
---|
14 | axiom hw_register_env: Type[0]. (* CSC: use the one in I8051? *) |
---|
15 | axiom hwreg_retrieve : hw_register_env → Register → res beval. |
---|
16 | axiom hwreg_store : Register → beval → hw_register_env → res hw_register_env. |
---|
17 | |
---|
18 | (****************************************************************************) |
---|
19 | |
---|
20 | (*CSC: XXXX; do we need to create a brand new chunk per label, so that |
---|
21 | pointer operations on labels are not semantically valid? |
---|
22 | ATM, the pointers are not valid (they do not point to allocated regions) |
---|
23 | and, moreover, they conflict with function blocks and with other pointers |
---|
24 | in other functions. However, there could be simpler ways to invalidate |
---|
25 | pointer arithmetics on Code pointers. |
---|
26 | *) |
---|
27 | definition pointer_of_label: label → Σp:pointer. ptype p = Code ≝ |
---|
28 | λl. |
---|
29 | mk_pointer Code |
---|
30 | (mk_block Code (Zopp (nat_of_bitvector ? (word_of_identifier … l)))) |
---|
31 | ? (mk_offset OZ). |
---|
32 | // qed. |
---|
33 | |
---|
34 | (*CSC: XXXX; inverse of the previous function, but it does not check that |
---|
35 | the offset is zero and thus it never fails. *) |
---|
36 | definition label_of_pointer: pointer → res label ≝ |
---|
37 | λp. OK … (an_identifier ? (bitvector_of_nat … (abs (block_id (pblock p))))). |
---|
38 | |
---|
39 | (*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label. |
---|
40 | Maybe there is a better way to organize the code!!! *) |
---|
41 | definition graph_succ_p: label → address → address. |
---|
42 | #l #_ generalize in match (refl … (address_of_pointer (pointer_of_label l))) |
---|
43 | cases (address_of_pointer (pointer_of_label l)) in ⊢ (???% → ?) |
---|
44 | [ #res #_ @res |
---|
45 | | #msg cases (pointer_of_label l) * * #q #com #off #E1 #E2 destruct ] |
---|
46 | qed. |
---|
47 | |
---|
48 | axiom BadProgramCounter: String. |
---|
49 | definition graph_fetch_statement: |
---|
50 | ∀params1,sem_params,globals. |
---|
51 | genv … (graph_params params1 globals) → |
---|
52 | state sem_params → res (joint_statement (graph_params_ params1) globals) ≝ |
---|
53 | λparams1,sem_params,globals,ge,st. |
---|
54 | do p ← pointer_of_address (pc … st) ; |
---|
55 | let b ≝ pblock p in |
---|
56 | do l ← label_of_pointer p; |
---|
57 | do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ; |
---|
58 | match def with |
---|
59 | [ Internal def' ⇒ |
---|
60 | opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … def') l) |
---|
61 | | External _ ⇒ Error … [MSG BadProgramCounter]]. |
---|