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