| 1 | include "joint/semantics_paolo.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 | (******************************** GRAPHS **************************************) |
|---|
| 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 | ∀pars : graph_params.∀globals. genv globals pars → pointer → label → |
|---|
| 32 | res (Σp:pointer. ptype p = Code) ≝ |
|---|
| 33 | λ_.λ_.λ_.λoldpc,l. |
|---|
| 34 | OK ? (graph_pointer_of_label0 oldpc l). |
|---|
| 35 | |
|---|
| 36 | definition graph_label_of_pointer: pointer → res label ≝ |
|---|
| 37 | λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])). |
|---|
| 38 | |
|---|
| 39 | (*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label. |
|---|
| 40 | But I can't use it directly because this one uses a concrete definition of |
|---|
| 41 | pointer_of_label and it is used to istantiate the more_sem_params record |
|---|
| 42 | where the abstract version is declared as a field. Is there a better way |
|---|
| 43 | to organize the code? *) |
|---|
| 44 | definition graph_succ_p: label → address → res address ≝ |
|---|
| 45 | λl,old. |
|---|
| 46 | do ptr ← pointer_of_address old ; |
|---|
| 47 | let newptr ≝ graph_pointer_of_label0 ptr l in |
|---|
| 48 | address_of_pointer newptr. |
|---|
| 49 | |
|---|
| 50 | definition graph_fetch_statement: |
|---|
| 51 | ∀pars : graph_params. |
|---|
| 52 | ∀sem_pars : sem_state_params. |
|---|
| 53 | ∀globals. |
|---|
| 54 | genv globals pars → |
|---|
| 55 | state sem_pars → |
|---|
| 56 | res (joint_statement pars globals) ≝ |
|---|
| 57 | λpars,sem_pars,globals,ge,st. |
|---|
| 58 | do p ← code_pointer_of_address (pc … st) ; |
|---|
| 59 | do f ← fetch_function … ge p ; |
|---|
| 60 | do l ← graph_label_of_pointer p; |
|---|
| 61 | opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l). |
|---|
| 62 | |
|---|
| 63 | definition make_sem_graph_params : |
|---|
| 64 | ∀pars : graph_params. |
|---|
| 65 | ∀g_pars : more_sem_genv_params pars. |
|---|
| 66 | sem_params ≝ |
|---|
| 67 | λpars,g_pars. |
|---|
| 68 | mk_sem_params |
|---|
| 69 | pars |
|---|
| 70 | (mk_more_sem_params |
|---|
| 71 | pars |
|---|
| 72 | g_pars |
|---|
| 73 | graph_succ_p |
|---|
| 74 | (graph_pointer_of_label ?) |
|---|
| 75 | (graph_fetch_statement ? ?) |
|---|
| 76 | ). |
|---|
| 77 | |
|---|
| 78 | (******************************** LINEAR **************************************) |
|---|
| 79 | |
|---|
| 80 | definition lin_succ_p: unit → address → res address := |
|---|
| 81 | λ_.λaddr. addr_add addr 1. |
|---|
| 82 | |
|---|
| 83 | |
|---|
| 84 | axiom BadLabel: String. |
|---|
| 85 | |
|---|
| 86 | definition lin_pointer_of_label: |
|---|
| 87 | ∀pars : lin_params. |
|---|
| 88 | ∀globals. genv globals pars → pointer → label → |
|---|
| 89 | res (Σp:pointer. ptype p = Code) ≝ |
|---|
| 90 | λpars,globals,ge,old,l. |
|---|
| 91 | do fn ← fetch_function … ge old ; |
|---|
| 92 | do pos ← |
|---|
| 93 | opt_to_res ? [MSG BadLabel] |
|---|
| 94 | (position_of ? |
|---|
| 95 | (λs. let 〈l',x〉 ≝ s in |
|---|
| 96 | match l' with [ None ⇒ false | Some l'' ⇒ if eq_identifier … l l'' then true else false]) |
|---|
| 97 | (joint_if_code … pars fn)) ; |
|---|
| 98 | OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?). |
|---|
| 99 | // qed. |
|---|
| 100 | |
|---|
| 101 | definition lin_fetch_statement: |
|---|
| 102 | ∀pars : lin_params. |
|---|
| 103 | ∀sem_pars : sem_state_params. |
|---|
| 104 | ∀globals. |
|---|
| 105 | genv globals pars → state sem_pars → res (joint_statement pars globals) ≝ |
|---|
| 106 | λpars,sem_pars,globals,ge,st. |
|---|
| 107 | do ppc ← pointer_of_address (pc … st) ; |
|---|
| 108 | do fn ← fetch_function … ge ppc ; |
|---|
| 109 | let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *) |
|---|
| 110 | do found ← opt_to_res ? [MSG BadProgramCounter] (nth_opt ? off (joint_if_code … fn)) ; |
|---|
| 111 | return (\snd found). |
|---|
| 112 | |
|---|
| 113 | definition make_sem_lin_params : |
|---|
| 114 | ∀pars : lin_params. |
|---|
| 115 | ∀g_pars : more_sem_genv_params pars. |
|---|
| 116 | sem_params ≝ |
|---|
| 117 | λpars,g_pars. |
|---|
| 118 | mk_sem_params |
|---|
| 119 | pars |
|---|
| 120 | (mk_more_sem_params |
|---|
| 121 | pars |
|---|
| 122 | g_pars |
|---|
| 123 | lin_succ_p |
|---|
| 124 | (lin_pointer_of_label ?) |
|---|
| 125 | (lin_fetch_statement ? ?) |
|---|
| 126 | ). |
|---|
| 127 | |
|---|
| 128 | |
|---|
