[1641] | 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 | |
---|
[1882] | 23 | definition graph_pointer_of_label : cpointer → label → res cpointer ≝ |
---|
| 24 | λoldpc,l. |
---|
| 25 | return (mk_pointer Code |
---|
| 26 | (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))) : cpointer). |
---|
| 27 | % qed. |
---|
[1641] | 28 | |
---|
| 29 | definition graph_label_of_pointer: pointer → res label ≝ |
---|
| 30 | λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])). |
---|
| 31 | |
---|
| 32 | definition graph_fetch_statement: |
---|
| 33 | ∀pars : graph_params. |
---|
| 34 | ∀sem_pars : sem_state_params. |
---|
| 35 | ∀globals. |
---|
| 36 | genv globals pars → |
---|
[1882] | 37 | cpointer → |
---|
[1641] | 38 | res (joint_statement pars globals) ≝ |
---|
[1882] | 39 | λpars,sem_pars,globals,ge,p. |
---|
[1641] | 40 | do f ← fetch_function … ge p ; |
---|
| 41 | do l ← graph_label_of_pointer p; |
---|
| 42 | opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l). |
---|
| 43 | |
---|
| 44 | definition make_sem_graph_params : |
---|
| 45 | ∀pars : graph_params. |
---|
| 46 | ∀g_pars : more_sem_genv_params pars. |
---|
| 47 | sem_params ≝ |
---|
| 48 | λpars,g_pars. |
---|
| 49 | mk_sem_params |
---|
| 50 | pars |
---|
| 51 | (mk_more_sem_params |
---|
| 52 | pars |
---|
| 53 | g_pars |
---|
[1882] | 54 | graph_pointer_of_label |
---|
| 55 | (λ_.λ_.graph_pointer_of_label) |
---|
| 56 | (graph_fetch_statement ? g_pars) |
---|
[1641] | 57 | ). |
---|
| 58 | |
---|
| 59 | (******************************** LINEAR **************************************) |
---|
[1882] | 60 | check mk_pointer |
---|
| 61 | definition lin_succ_p: cpointer → unit → res cpointer := |
---|
| 62 | λptr.λ_.return «mk_pointer Code (pblock ptr) ? (mk_offset (offv (poff ptr) + 1)), ?». |
---|
| 63 | [%| cases ptr //] qed. |
---|
[1641] | 64 | |
---|
| 65 | axiom BadLabel: String. |
---|
| 66 | |
---|
| 67 | definition lin_pointer_of_label: |
---|
| 68 | ∀pars : lin_params. |
---|
[1882] | 69 | ∀globals. genv globals pars → cpointer → label → res cpointer ≝ |
---|
[1641] | 70 | λpars,globals,ge,old,l. |
---|
| 71 | do fn ← fetch_function … ge old ; |
---|
| 72 | do pos ← |
---|
| 73 | opt_to_res ? [MSG BadLabel] |
---|
| 74 | (position_of ? |
---|
| 75 | (λs. let 〈l',x〉 ≝ s in |
---|
| 76 | match l' with [ None ⇒ false | Some l'' ⇒ if eq_identifier … l l'' then true else false]) |
---|
| 77 | (joint_if_code … pars fn)) ; |
---|
| 78 | OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?). |
---|
[1882] | 79 | % qed. |
---|
[1641] | 80 | |
---|
| 81 | definition lin_fetch_statement: |
---|
| 82 | ∀pars : lin_params. |
---|
| 83 | ∀sem_pars : sem_state_params. |
---|
| 84 | ∀globals. |
---|
[1882] | 85 | genv globals pars → cpointer → res (joint_statement pars globals) ≝ |
---|
| 86 | λpars,sem_pars,globals,ge,ppc. |
---|
[1641] | 87 | do fn ← fetch_function … ge ppc ; |
---|
| 88 | let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *) |
---|
| 89 | do found ← opt_to_res ? [MSG BadProgramCounter] (nth_opt ? off (joint_if_code … fn)) ; |
---|
| 90 | return (\snd found). |
---|
| 91 | |
---|
| 92 | definition make_sem_lin_params : |
---|
| 93 | ∀pars : lin_params. |
---|
| 94 | ∀g_pars : more_sem_genv_params pars. |
---|
| 95 | sem_params ≝ |
---|
| 96 | λpars,g_pars. |
---|
| 97 | mk_sem_params |
---|
| 98 | pars |
---|
| 99 | (mk_more_sem_params |
---|
| 100 | pars |
---|
| 101 | g_pars |
---|
| 102 | lin_succ_p |
---|
| 103 | (lin_pointer_of_label ?) |
---|
[1882] | 104 | (lin_fetch_statement ? g_pars) |
---|
[1641] | 105 | ). |
---|
| 106 | |
---|
[1882] | 107 | definition step_unbranching : ∀p,globals.joint_step p globals → bool ≝ |
---|
| 108 | λp,globals,stp.match stp with |
---|
| 109 | [ COND _ _ ⇒ false |
---|
| 110 | | CALL_ID _ _ _ ⇒ false |
---|
| 111 | | extension c' ⇒ (* FIXME: does not care about calling extensions!! *) |
---|
| 112 | match ext_step_labels … c' with |
---|
| 113 | [ nil ⇒ true |
---|
| 114 | | _ ⇒ false |
---|
| 115 | ] |
---|
| 116 | | _ ⇒ true |
---|
| 117 | ]. |
---|
[1641] | 118 | |
---|
[1882] | 119 | definition is_not_seq : ∀p,globals.joint_statement p globals → bool ≝ |
---|
| 120 | λp,globals,stp.match stp with |
---|
| 121 | [ sequential _ _ ⇒ false |
---|
| 122 | | _ ⇒ true |
---|
| 123 | ]. |
---|
| 124 | |
---|
| 125 | inductive s_block (p : params) (globals : list ident) : Type[0] ≝ |
---|
| 126 | | Skip : s_block p globals |
---|
| 127 | | FinStep : (Σs.bool_to_Prop (¬step_unbranching p globals s)) → s_block p globals |
---|
| 128 | | FinStmt : (Σs.bool_to_Prop (is_not_seq p globals s)) → s_block p globals |
---|
| 129 | | Cons : (Σs.bool_to_Prop (step_unbranching p globals s)) → s_block p globals → s_block p globals. |
---|
| 130 | |
---|
| 131 | include "utilities/bind_new.ma". |
---|
| 132 | |
---|
| 133 | definition Block ≝ λp : params.λglobals.bind_new (localsT p) (s_block p globals). |
---|
| 134 | |
---|
| 135 | definition Bcons ≝ λp : params.λglobals. |
---|
| 136 | λs : Σs.bool_to_Prop (step_unbranching p globals s). |
---|
| 137 | λB : Block p globals. |
---|
| 138 | ! b ← B ; return Cons ?? s b. |
---|
| 139 | |
---|
| 140 | interpretation "block cons" 'vcons hd tl = (Bcons ??? hd tl). |
---|
| 141 | |
---|
| 142 | let rec is_unbranching p globals (b1 : s_block p globals) on b1 : bool ≝ |
---|
| 143 | match b1 with |
---|
| 144 | [ Skip ⇒ true |
---|
| 145 | | FinStep _ ⇒ false |
---|
| 146 | | FinStmt _ ⇒ false |
---|
| 147 | | Cons _ tl ⇒ is_unbranching ?? tl |
---|
| 148 | ]. |
---|
| 149 | |
---|
| 150 | let rec Is_unbranching p globals (b1 : Block p globals) on b1 : Prop ≝ |
---|
| 151 | match b1 with |
---|
| 152 | [ bret b ⇒ bool_to_Prop (is_unbranching … b) |
---|
| 153 | | bnew f ⇒ ∀x.Is_unbranching … (f x) |
---|
| 154 | ]. |
---|
| 155 | |
---|
| 156 | let rec s_block_append_aux p globals (b1 : s_block p globals) (b2 : s_block p globals) on b1 : is_unbranching … b1 → s_block p globals ≝ |
---|
| 157 | match b1 return λx.is_unbranching ?? x → ? with |
---|
| 158 | [ Skip ⇒ λ_.b2 |
---|
| 159 | | Cons x tl ⇒ λprf.Cons ?? x (s_block_append_aux ?? tl b2 prf) |
---|
| 160 | | _ ⇒ Ⓧ |
---|
| 161 | ]. |
---|
| 162 | |
---|
| 163 | definition s_block_append ≝ |
---|
| 164 | λp,globals.λb1 : Σb.bool_to_Prop (is_unbranching … b).λb2. |
---|
| 165 | match b1 with |
---|
| 166 | [ mk_Sig b1 prf ⇒ s_block_append_aux p globals b1 b2 prf ]. |
---|
| 167 | |
---|
| 168 | definition Is_to_is_unbr : ∀p,globals.(ΣB.Is_unbranching p globals B) → |
---|
| 169 | bind_new (localsT p) (Σb.bool_to_Prop (is_unbranching p globals b)) ≝ |
---|
| 170 | λp,globals. ?. |
---|
| 171 | * #b elim b -b |
---|
| 172 | [ #b #H @bret @b @H |
---|
| 173 | | #f #IH #H @bnew #x @(IH x) @H |
---|
| 174 | ] |
---|
| 175 | qed. |
---|
| 176 | |
---|
| 177 | lemma Is_to_is_unbr_OK : ∀p,globals,B.! b ← Is_to_is_unbr p globals B ; return pi1 … b = pi1 … B. |
---|
| 178 | #p #globals * #b elim b |
---|
| 179 | [ // |
---|
| 180 | | #f #IH #H @bnew_proper |
---|
| 181 | #x @IH |
---|
| 182 | ] |
---|
| 183 | qed. |
---|
| 184 | |
---|
| 185 | definition Block_append ≝ |
---|
| 186 | λp,globals.λB : Σb.Is_unbranching … b.λB'. |
---|
| 187 | ! b1 ← Is_to_is_unbr … B; |
---|
| 188 | ! b2 ← B'; |
---|
| 189 | return s_block_append p globals b1 b2. |
---|
| 190 | |
---|
| 191 | definition all_unbranching ≝ λp,globals.All ? (λs.bool_to_Prop (step_unbranching p globals s)). |
---|
| 192 | |
---|
| 193 | let rec step_list_to_s_block (p : params) globals (l : list (joint_step p globals)) on l : |
---|
| 194 | s_block p globals ≝ |
---|
| 195 | match l with |
---|
| 196 | [ nil ⇒ Skip ?? |
---|
| 197 | | cons hd tl ⇒ |
---|
| 198 | If step_unbranching … hd then with prf do |
---|
| 199 | Cons ?? hd (step_list_to_s_block ?? tl) |
---|
| 200 | else with prf do |
---|
| 201 | FinStep ?? hd |
---|
| 202 | ]. [assumption | >prf % ] qed. |
---|
| 203 | |
---|
| 204 | definition step_list_to_block : ∀R,p,g.? → Block R p g ≝ |
---|
| 205 | λR,p,globals,l.bret R ? (step_list_to_s_block p globals l). |
---|
| 206 | |
---|
| 207 | record sem_rel (p1 : sem_params) (p2 : sem_params) (globals : list ident) : Type[0] ≝ |
---|
| 208 | { function_rel : joint_function globals p1 → joint_function globals p2 → Prop |
---|
| 209 | ; genv_rel : genv globals p1 → genv globals p2 → Prop |
---|
| 210 | ; pc_rel : cpointer → cpointer → Prop |
---|
| 211 | ; st_rel : state p1 → state p2 → Prop |
---|
| 212 | ; stmt_rel : joint_statement p1 globals → Block |
---|
| 213 | (* TODO: state what do we need of genv_rel (like finding the same symbols and what relation to above rels ) *) |
---|
| 214 | ; st_to_pc_rel : ∀st1,st2.st_rel st1 st2 → pc_rel (pc ? st1) (pc ? st2) |
---|
| 215 | }. |
---|
| 216 | |
---|
| 217 | (* move *) |
---|
| 218 | definition beval_pair_of_xdata_pointer: (Σp:pointer. ptype p = XData) → beval × beval ≝ |
---|
| 219 | λp. match p return λp. ptype p = XData → ? with [ mk_pointer pty pbl pok poff ⇒ |
---|
| 220 | match pty return λpty. ? → pty = XData → ? with |
---|
| 221 | [ XData ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer XData pbl ? poff)) ? |
---|
| 222 | | _ ⇒ λpok'.λabs. ⊥] pok] ?. |
---|
| 223 | [@(pi2 … p) |6: // |7: %] destruct (abs) |
---|
| 224 | qed. |
---|
| 225 | |
---|
| 226 | definition safe_address_of_xdata_pointer: (Σp:pointer. ptype p = XData) → safe_address ≝ beval_pair_of_xdata_pointer. |
---|
| 227 | cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H |
---|
| 228 | lapply (pointer_compat_from_ind … H) -H cases b * #z * #H |
---|
| 229 | %{«mk_pointer ? (mk_block ? z) H o,I»} |
---|
| 230 | % [2,4: % [2,4: % [1,3: % [1,3: % ]] % |*:]|*:] |
---|
| 231 | qed. |
---|
| 232 | |
---|
| 233 | definition state_rel : ∀p1,p2.∀R : sem_rel p1 p2.good_state p1 → good_state p2 → Prop ≝ |
---|
| 234 | λp1,p2,R,st1,st2. |
---|
| 235 | frames_rel p1 p2 R (st_frms … st1) (st_frms … st2) ∧ |
---|
| 236 | pc_rel p1 p2 R (pc … st1) (pc … st2) ∧ |
---|
| 237 | sp_rel p1 p2 R |
---|
| 238 | (safe_address_of_xdata_pointer (sp … st1)) |
---|
| 239 | (safe_address_of_xdata_pointer (sp … st2)) ∧ |
---|
| 240 | isp_rel p1 p2 R |
---|
| 241 | (safe_address_of_xdata_pointer (isp … st1)) |
---|
| 242 | (safe_address_of_xdata_pointer (isp … st2)) ∧ |
---|
| 243 | sp_rel p1 p2 R |
---|
| 244 | (safe_address_of_xdata_pointer (sp … st1)) |
---|
| 245 | (safe_address_of_xdata_pointer (sp … st2)) ∧ |
---|
| 246 | carry … st1 = carry … st2 ∧ |
---|
| 247 | regs_rel p1 p2 R (regs … st1) (regs … st2) ∧ |
---|
| 248 | mem_rel p1 p2 R (m … st1) (m … st2). |
---|
| 249 | elim st1 -st1 #st1 ** #good_pc1 #good_sp1 #good_isp1 |
---|
| 250 | elim st2 -st2 #st2 ** #good_pc2 #good_sp2 #good_isp2 |
---|
| 251 | assumption |
---|
| 252 | qed. |
---|
| 253 | elim st2 |
---|
| 254 | -st1 -st2 #st2 ** #good_pc2 # ∧ |
---|
| 255 | frames_rel … R (st_frms … st1) (st_frms … st2) ∧ |
---|
| 256 | frames_rel … R (st_frms … st1) (st_frms … st2) ∧ |
---|
| 257 | frames_rel … R (st_frms … st1) (st_frms … st2) ∧ |
---|
| 258 | |
---|
| 259 | |
---|
| 260 | |
---|