1 | include "joint/semantics.ma". |
---|
2 | include alias "common/Identifiers.ma". |
---|
3 | |
---|
4 | (*** Store/retrieve on pseudo-registers ***) |
---|
5 | |
---|
6 | axiom BadRegister : String. |
---|
7 | |
---|
8 | definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v. |
---|
9 | |
---|
10 | definition reg_retrieve : register_env beval → register → res beval ≝ |
---|
11 | λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg). |
---|
12 | |
---|
13 | (*** Store/retrieve on hardware registers ***) |
---|
14 | |
---|
15 | definition init_hw_register_env: address → hw_register_env ≝ |
---|
16 | λaddr. |
---|
17 | let 〈dpl,dph〉 ≝ addr in |
---|
18 | let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in |
---|
19 | hwreg_store RegisterDPL dpl env. |
---|
20 | |
---|
21 | (****************************************************************************) |
---|
22 | |
---|
23 | (*CSC: XXXXXXXXXXXXXXXXX bug here; we need to change the encoding so that |
---|
24 | the block is the one of the function and the offset corresponds to the |
---|
25 | label. Code pointer arithmetics must be prevented in another way, i.e. |
---|
26 | by not allowing any increment/decrement on Code regions (with the |
---|
27 | exception of LIN's succ_pc function). If we don't do that, then the |
---|
28 | find_funct_ptr (e.g. in graph_fetch_statement) are not correct! *) |
---|
29 | (*CSC: XXXX; do we need to create a brand new chunk per label, so that |
---|
30 | pointer operations on labels are not semantically valid? |
---|
31 | ATM, the pointers are not valid (they do not point to allocated regions) |
---|
32 | and, moreover, they conflict with function blocks and with other pointers |
---|
33 | in other functions. However, there could be simpler ways to invalidate |
---|
34 | pointer arithmetics on Code pointers. |
---|
35 | *) |
---|
36 | definition pointer_of_label: label → Σp:pointer. ptype p = Code ≝ |
---|
37 | λl. |
---|
38 | mk_pointer Code |
---|
39 | (mk_block Code (Zopp (nat_of_bitvector ? (word_of_identifier … l)))) |
---|
40 | ? (mk_offset OZ). |
---|
41 | // qed. |
---|
42 | |
---|
43 | (*CSC: XXXX; inverse of the previous function, but it does not check that |
---|
44 | the offset is zero and thus it never fails. *) |
---|
45 | definition label_of_pointer: pointer → res label ≝ |
---|
46 | λp. OK … (an_identifier ? (bitvector_of_nat … (abs (block_id (pblock p))))). |
---|
47 | |
---|
48 | (*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label. |
---|
49 | But I can't use it directly because this one uses a concrete definition of |
---|
50 | pointer_of_label and it is used to istantiate the more_sem_params record |
---|
51 | where the abstract version is declared as a field. Is there a better way |
---|
52 | to organize the code? *) |
---|
53 | definition graph_succ_p: label → address → res address ≝ |
---|
54 | λl.λ_.address_of_pointer (pointer_of_label l). |
---|
55 | |
---|
56 | axiom BadProgramCounter: String. |
---|
57 | |
---|
58 | definition graph_fetch_function: |
---|
59 | ∀params1,sem_params,globals. |
---|
60 | genv … (graph_params params1 globals) → |
---|
61 | state sem_params → res (joint_internal_function … (graph_params params1 globals)) ≝ |
---|
62 | λparams1,sem_params,globals,ge,st. |
---|
63 | do p ← code_pointer_of_address (pc … st) ; |
---|
64 | let b ≝ pblock p in |
---|
65 | do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ; |
---|
66 | match def with |
---|
67 | [ Internal def' ⇒ OK … def' |
---|
68 | | External _ ⇒ Error … [MSG BadProgramCounter]]. |
---|
69 | |
---|
70 | definition graph_fetch_statement: |
---|
71 | ∀params1,sem_params,globals. |
---|
72 | genv … (graph_params params1 globals) → |
---|
73 | state sem_params → res (joint_statement (graph_params_ params1) globals) ≝ |
---|
74 | λparams1,sem_params,globals,ge,st. |
---|
75 | do p ← code_pointer_of_address (pc … st) ; |
---|
76 | do f ← graph_fetch_function … ge st ; |
---|
77 | do l ← label_of_pointer p; |
---|
78 | opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l). |
---|