| 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 | definition graph_pointer_of_label0: |
|---|
| 24 | pointer → label → Σp:pointer. ptype p = Code ≝ |
|---|
| 25 | λoldpc,l. |
|---|
| 26 | mk_pointer Code |
|---|
| 27 | (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))). |
|---|
| 28 | // qed. |
|---|
| 29 | |
|---|
| 30 | definition graph_pointer_of_label: |
|---|
| 31 | ∀params1.∀globals. genv … (graph_params params1 globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝ |
|---|
| 32 | λ_.λ_.λ_.λoldpc,l. |
|---|
| 33 | OK ? (graph_pointer_of_label0 oldpc l). |
|---|
| 34 | |
|---|
| 35 | definition graph_label_of_pointer: pointer → res label ≝ |
|---|
| 36 | λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])). |
|---|
| 37 | |
|---|
| 38 | (*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label. |
|---|
| 39 | But I can't use it directly because this one uses a concrete definition of |
|---|
| 40 | pointer_of_label and it is used to istantiate the more_sem_params record |
|---|
| 41 | where the abstract version is declared as a field. Is there a better way |
|---|
| 42 | to organize the code? *) |
|---|
| 43 | definition graph_succ_p: label → address → res address ≝ |
|---|
| 44 | λl,old. |
|---|
| 45 | do ptr ← pointer_of_address old ; |
|---|
| 46 | let newptr ≝ graph_pointer_of_label0 ptr l in |
|---|
| 47 | address_of_pointer newptr. |
|---|
| 48 | |
|---|
| 49 | axiom BadProgramCounter: String. |
|---|
| 50 | |
|---|
| 51 | definition graph_fetch_function: |
|---|
| 52 | ∀params1,sem_params,globals. |
|---|
| 53 | genv … (graph_params params1 globals) → |
|---|
| 54 | state sem_params → res (joint_internal_function … (graph_params params1 globals)) ≝ |
|---|
| 55 | λparams1,sem_params,globals,ge,st. |
|---|
| 56 | do p ← code_pointer_of_address (pc … st) ; |
|---|
| 57 | let b ≝ pblock p in |
|---|
| 58 | do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ; |
|---|
| 59 | match def with |
|---|
| 60 | [ Internal def' ⇒ OK … def' |
|---|
| 61 | | External _ ⇒ Error … [MSG BadProgramCounter]]. |
|---|
| 62 | |
|---|
| 63 | definition graph_fetch_statement: |
|---|
| 64 | ∀params1,sem_params,globals. |
|---|
| 65 | genv … (graph_params params1 globals) → |
|---|
| 66 | state sem_params → res (joint_statement (graph_params_ params1) globals) ≝ |
|---|
| 67 | λparams1,sem_params,globals,ge,st. |
|---|
| 68 | do p ← code_pointer_of_address (pc … st) ; |
|---|
| 69 | do f ← graph_fetch_function … ge st ; |
|---|
| 70 | do l ← graph_label_of_pointer p; |
|---|
| 71 | opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l). |
|---|
