Changeset 1615 for src/ASM/Assembly.ma
- Timestamp:
- Dec 14, 2011, 5:28:11 PM (8 years ago)
- File:
-
- 1 edited
-
src/ASM/Assembly.ma (modified) (1 diff)
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r1614 r1615 6 6 include alias "arithmetics/nat.ma". 7 7 include "utilities/extralib.ma". 8 include "ASM/Policy.ma".9 8 10 9 (**************************************** START OF POLICY ABSTRACTION ********************) 11 10 11 (* definition of & operations on jump length *) 12 inductive jump_length: Type[0] ≝ 13 | short_jump: jump_length 14 | medium_jump: jump_length 15 | long_jump: jump_length. 16 12 17 definition policy_type ≝ Word → jump_length. 13 18 14 definition jump_expansion': 15 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16). 16 policy_type ≝ 17 λprogram.λpc. 18 let policy ≝ 19 transform_policy (|\snd program|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in 20 lookup ? ? pc policy long_jump. 21 /2 by Stub, mk_Sig/ 22 qed. 19 definition assembly_preinstruction ≝ 20 λA: Type[0]. 21 λaddr_of: A → Byte. (* relative *) 22 λpre: preinstruction A. 23 match pre with 24 [ ADD addr1 addr2 ⇒ 25 match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with 26 [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ] 27 | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ] 28 | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ] 29 | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ] 30 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 31 | ADDC addr1 addr2 ⇒ 32 match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with 33 [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ] 34 | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ] 35 | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ] 36 | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ] 37 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 38 | ANL addrs ⇒ 39 match addrs with 40 [ inl addrs ⇒ match addrs with 41 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 42 match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with 43 [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ] 44 | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ] 45 | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ] 46 | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ] 47 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 48 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 49 let b1 ≝ 50 match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with 51 [ DIRECT b1 ⇒ λ_.b1 52 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in 53 match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with 54 [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ] 55 | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ] 56 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 57 ] 58 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 59 match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with 60 [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ] 61 | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ] 62 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 63 | CLR addr ⇒ 64 match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with 65 [ ACC_A ⇒ λ_. 66 [ ([[true; true; true; false; false; true; false; false]]) ] 67 | CARRY ⇒ λ_. 68 [ ([[true; true; false; false; false; false; true; true]]) ] 69 | BIT_ADDR b1 ⇒ λ_. 70 [ ([[true; true; false; false; false; false; true; false]]) ; b1 ] 71 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 72 | CPL addr ⇒ 73 match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with 74 [ ACC_A ⇒ λ_. 75 [ ([[true; true; true; true; false; true; false; false]]) ] 76 | CARRY ⇒ λ_. 77 [ ([[true; false; true; true; false; false; true; true]]) ] 78 | BIT_ADDR b1 ⇒ λ_. 79 [ ([[true; false; true; true; false; false; true; false]]) ; b1 ] 80 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 81 | DA addr ⇒ 82 [ ([[true; true; false; true; false; true; false; false]]) ] 83 | DEC addr ⇒ 84 match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with 85 [ ACC_A ⇒ λ_. 86 [ ([[false; false; false; true; false; true; false; false]]) ] 87 | REGISTER r ⇒ λ_. 88 [ ([[false; false; false; true; true]]) @@ r ] 89 | DIRECT b1 ⇒ λ_. 90 [ ([[false; false; false; true; false; true; false; true]]); b1 ] 91 | INDIRECT i1 ⇒ λ_. 92 [ ([[false; false; false; true; false; true; true; i1]]) ] 93 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 94 | DJNZ addr1 addr2 ⇒ 95 let b2 ≝ addr_of addr2 in 96 match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with 97 [ REGISTER r ⇒ λ_. 98 [ ([[true; true; false; true; true]]) @@ r ; b2 ] 99 | DIRECT b1 ⇒ λ_. 100 [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ] 101 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 102 | JC addr ⇒ 103 let b1 ≝ addr_of addr in 104 [ ([[false; true; false; false; false; false; false; false]]); b1 ] 105 | JNC addr ⇒ 106 let b1 ≝ addr_of addr in 107 [ ([[false; true; false; true; false; false; false; false]]); b1 ] 108 | JZ addr ⇒ 109 let b1 ≝ addr_of addr in 110 [ ([[false; true; true; false; false; false; false; false]]); b1 ] 111 | JNZ addr ⇒ 112 let b1 ≝ addr_of addr in 113 [ ([[false; true; true; true; false; false; false; false]]); b1 ] 114 | JB addr1 addr2 ⇒ 115 let b2 ≝ addr_of addr2 in 116 match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 117 [ BIT_ADDR b1 ⇒ λ_. 118 [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ] 119 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 120 | JNB addr1 addr2 ⇒ 121 let b2 ≝ addr_of addr2 in 122 match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 123 [ BIT_ADDR b1 ⇒ λ_. 124 [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ] 125 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 126 | JBC addr1 addr2 ⇒ 127 let b2 ≝ addr_of addr2 in 128 match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 129 [ BIT_ADDR b1 ⇒ λ_. 130 [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ] 131 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 132 | CJNE addrs addr3 ⇒ 133 let b3 ≝ addr_of addr3 in 134 match addrs with 135 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 136 match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with 137 [ DIRECT b1 ⇒ λ_. 138 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ] 139 | DATA b1 ⇒ λ_. 140 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ] 141 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 142 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 143 let b2 ≝ 144 match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with 145 [ DATA b2 ⇒ λ_. b2 146 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 147 match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with 148 [ REGISTER r ⇒ λ_. 149 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ] 150 | INDIRECT i1 ⇒ λ_. 151 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ] 152 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 153 ] 154 | DIV addr1 addr2 ⇒ 155 [ ([[true;false;false;false;false;true;false;false]]) ] 156 | INC addr ⇒ 157 match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with 158 [ ACC_A ⇒ λ_. 159 [ ([[false;false;false;false;false;true;false;false]]) ] 160 | REGISTER r ⇒ λ_. 161 [ ([[false;false;false;false;true]]) @@ r ] 162 | DIRECT b1 ⇒ λ_. 163 [ ([[false; false; false; false; false; true; false; true]]); b1 ] 164 | INDIRECT i1 ⇒ λ_. 165 [ ([[false; false; false; false; false; true; true; i1]]) ] 166 | DPTR ⇒ λ_. 167 [ ([[true;false;true;false;false;false;true;true]]) ] 168 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 169 | MOV addrs ⇒ 170 match addrs with 171 [ inl addrs ⇒ 172 match addrs with 173 [ inl addrs ⇒ 174 match addrs with 175 [ inl addrs ⇒ 176 match addrs with 177 [ inl addrs ⇒ 178 match addrs with 179 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 180 match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with 181 [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ] 182 | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ] 183 | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ] 184 | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ] 185 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 186 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 187 match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with 188 [ REGISTER r ⇒ λ_. 189 match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with 190 [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ] 191 | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ] 192 | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ] 193 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 194 | INDIRECT i1 ⇒ λ_. 195 match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with 196 [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ] 197 | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ] 198 | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ] 199 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 200 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)] 201 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 202 let b1 ≝ 203 match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with 204 [ DIRECT b1 ⇒ λ_. b1 205 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in 206 match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with 207 [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1] 208 | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ] 209 | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ] 210 | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ] 211 | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ] 212 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 213 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 214 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with 215 [ DATA16 w ⇒ λ_. 216 let b1_b2 ≝ split ? 8 8 w in 217 let b1 ≝ \fst b1_b2 in 218 let b2 ≝ \snd b1_b2 in 219 [ ([[true;false;false;true;false;false;false;false]]); b1; b2] 220 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 221 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 222 match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 223 [ BIT_ADDR b1 ⇒ λ_. 224 [ ([[true;false;true;false;false;false;true;false]]); b1 ] 225 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 226 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 227 match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 228 [ BIT_ADDR b1 ⇒ λ_. 229 [ ([[true;false;false;true;false;false;true;false]]); b1 ] 230 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)] 231 | MOVX addrs ⇒ 232 match addrs with 233 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 234 match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with 235 [ EXT_INDIRECT i1 ⇒ λ_. 236 [ ([[true;true;true;false;false;false;true;i1]]) ] 237 | EXT_INDIRECT_DPTR ⇒ λ_. 238 [ ([[true;true;true;false;false;false;false;false]]) ] 239 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 240 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 241 match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with 242 [ EXT_INDIRECT i1 ⇒ λ_. 243 [ ([[true;true;true;true;false;false;true;i1]]) ] 244 | EXT_INDIRECT_DPTR ⇒ λ_. 245 [ ([[true;true;true;true;false;false;false;false]]) ] 246 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)] 247 | MUL addr1 addr2 ⇒ 248 [ ([[true;false;true;false;false;true;false;false]]) ] 249 | NOP ⇒ 250 [ ([[false;false;false;false;false;false;false;false]]) ] 251 | ORL addrs ⇒ 252 match addrs with 253 [ inl addrs ⇒ 254 match addrs with 255 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 256 match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with 257 [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ] 258 | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ] 259 | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ] 260 | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ] 261 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 262 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 263 let b1 ≝ 264 match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with 265 [ DIRECT b1 ⇒ λ_. b1 266 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in 267 match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with 268 [ ACC_A ⇒ λ_. 269 [ ([[false;true;false;false;false;false;true;false]]); b1 ] 270 | DATA b2 ⇒ λ_. 271 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ] 272 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 273 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 274 match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with 275 [ BIT_ADDR b1 ⇒ λ_. 276 [ ([[false;true;true;true;false;false;true;false]]); b1 ] 277 | N_BIT_ADDR b1 ⇒ λ_. 278 [ ([[true;false;true;false;false;false;false;false]]); b1 ] 279 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 280 | POP addr ⇒ 281 match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with 282 [ DIRECT b1 ⇒ λ_. 283 [ ([[true;true;false;true;false;false;false;false]]) ; b1 ] 284 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 285 | PUSH addr ⇒ 286 match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with 287 [ DIRECT b1 ⇒ λ_. 288 [ ([[true;true;false;false;false;false;false;false]]) ; b1 ] 289 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 290 | RET ⇒ 291 [ ([[false;false;true;false;false;false;true;false]]) ] 292 | RETI ⇒ 293 [ ([[false;false;true;true;false;false;true;false]]) ] 294 | RL addr ⇒ 295 [ ([[false;false;true;false;false;false;true;true]]) ] 296 | RLC addr ⇒ 297 [ ([[false;false;true;true;false;false;true;true]]) ] 298 | RR addr ⇒ 299 [ ([[false;false;false;false;false;false;true;true]]) ] 300 | RRC addr ⇒ 301 [ ([[false;false;false;true;false;false;true;true]]) ] 302 | SETB addr ⇒ 303 match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with 304 [ CARRY ⇒ λ_. 305 [ ([[true;true;false;true;false;false;true;true]]) ] 306 | BIT_ADDR b1 ⇒ λ_. 307 [ ([[true;true;false;true;false;false;true;false]]); b1 ] 308 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 309 | SUBB addr1 addr2 ⇒ 310 match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with 311 [ REGISTER r ⇒ λ_. 312 [ ([[true;false;false;true;true]]) @@ r ] 313 | DIRECT b1 ⇒ λ_. 314 [ ([[true;false;false;true;false;true;false;true]]); b1] 315 | INDIRECT i1 ⇒ λ_. 316 [ ([[true;false;false;true;false;true;true;i1]]) ] 317 | DATA b1 ⇒ λ_. 318 [ ([[true;false;false;true;false;true;false;false]]); b1] 319 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 320 | SWAP addr ⇒ 321 [ ([[true;true;false;false;false;true;false;false]]) ] 322 | XCH addr1 addr2 ⇒ 323 match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with 324 [ REGISTER r ⇒ λ_. 325 [ ([[true;true;false;false;true]]) @@ r ] 326 | DIRECT b1 ⇒ λ_. 327 [ ([[true;true;false;false;false;true;false;true]]); b1] 328 | INDIRECT i1 ⇒ λ_. 329 [ ([[true;true;false;false;false;true;true;i1]]) ] 330 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 331 | XCHD addr1 addr2 ⇒ 332 match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with 333 [ INDIRECT i1 ⇒ λ_. 334 [ ([[true;true;false;true;false;true;true;i1]]) ] 335 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 336 | XRL addrs ⇒ 337 match addrs with 338 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 339 match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with 340 [ REGISTER r ⇒ λ_. 341 [ ([[false;true;true;false;true]]) @@ r ] 342 | DIRECT b1 ⇒ λ_. 343 [ ([[false;true;true;false;false;true;false;true]]); b1] 344 | INDIRECT i1 ⇒ λ_. 345 [ ([[false;true;true;false;false;true;true;i1]]) ] 346 | DATA b1 ⇒ λ_. 347 [ ([[false;true;true;false;false;true;false;false]]); b1] 348 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 349 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 350 let b1 ≝ 351 match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with 352 [ DIRECT b1 ⇒ λ_. b1 353 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in 354 match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with 355 [ ACC_A ⇒ λ_. 356 [ ([[false;true;true;false;false;false;true;false]]); b1 ] 357 | DATA b2 ⇒ λ_. 358 [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ] 359 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 360 ]. 361 362 definition assembly1 ≝ 363 λi: instruction. 364 match i with 365 [ ACALL addr ⇒ 366 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 367 [ ADDR11 w ⇒ λ_. 368 let v1_v2 ≝ split ? 3 8 w in 369 let v1 ≝ \fst v1_v2 in 370 let v2 ≝ \snd v1_v2 in 371 [ (v1 @@ [[true; false; false; false; true]]) ; v2 ] 372 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 373 | AJMP addr ⇒ 374 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 375 [ ADDR11 w ⇒ λ_. 376 let v1_v2 ≝ split ? 3 8 w in 377 let v1 ≝ \fst v1_v2 in 378 let v2 ≝ \snd v1_v2 in 379 [ (v1 @@ [[false; false; false; false; true]]) ; v2 ] 380 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 381 | JMP adptr ⇒ 382 [ ([[false;true;true;true;false;false;true;true]]) ] 383 | LCALL addr ⇒ 384 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with 385 [ ADDR16 w ⇒ λ_. 386 let b1_b2 ≝ split ? 8 8 w in 387 let b1 ≝ \fst b1_b2 in 388 let b2 ≝ \snd b1_b2 in 389 [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ] 390 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 391 | LJMP addr ⇒ 392 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with 393 [ ADDR16 w ⇒ λ_. 394 let b1_b2 ≝ split ? 8 8 w in 395 let b1 ≝ \fst b1_b2 in 396 let b2 ≝ \snd b1_b2 in 397 [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ] 398 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 399 | MOVC addr1 addr2 ⇒ 400 match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with 401 [ ACC_DPTR ⇒ λ_. 402 [ ([[true;false;false;true;false;false;true;true]]) ] 403 | ACC_PC ⇒ λ_. 404 [ ([[true;false;false;false;false;false;true;true]]) ] 405 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 406 | SJMP addr ⇒ 407 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 408 [ RELATIVE b1 ⇒ λ_. 409 [ ([[true;false;false;false;false;false;false;false]]); b1 ] 410 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 411 | RealInstruction instr ⇒ 412 assembly_preinstruction [[ relative ]] 413 (λx. 414 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with 415 [ RELATIVE r ⇒ λ_. r 416 | _ ⇒ λabsd. ⊥ 417 ] (subaddressing_modein … x)) instr 418 ]. 419 cases absd 420 qed. 421 422 definition expand_relative_jump_internal: 423 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) → 424 option (list instruction) 425 ≝ 426 λlookup_labels,jmp_len.λjmp:Identifier.λpc,i. 427 match jmp_len with 428 [ short_jump ⇒ 429 let lookup_address ≝ lookup_labels jmp in 430 let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in 431 let 〈upper, lower〉 ≝ split ? 8 8 result in 432 if eq_bv ? upper (zero 8) then 433 let address ≝ RELATIVE lower in 434 Some ? [ RealInstruction (i address) ] 435 else 436 None ? 437 | medium_jump ⇒ None … 438 | long_jump ⇒ 439 Some ? 440 [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2))); 441 SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *) 442 LJMP (ADDR16 (lookup_labels jmp)) 443 ] 444 ]. 445 @ I 446 qed. 447 448 definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝ 449 λlookup_labels. 450 λjmp_len: jump_length. 451 λpc. 452 λi: preinstruction Identifier. 453 let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in 454 match i with 455 [ JC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JC ?) 456 | JNC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNC ?) 457 | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JB ? baddr) 458 | JZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JZ ?) 459 | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNZ ?) 460 | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JBC ? baddr) 461 | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNB ? baddr) 462 | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (CJNE ? addr) 463 | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (DJNZ ? addr) 464 | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ] 465 | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ] 466 | SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ] 467 | INC arg ⇒ Some ? [ INC ? arg ] 468 | DEC arg ⇒ Some ? [ DEC ? arg ] 469 | MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ] 470 | DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ] 471 | DA arg ⇒ Some ? [ DA ? arg ] 472 | ANL arg ⇒ Some ? [ ANL ? arg ] 473 | ORL arg ⇒ Some ? [ ORL ? arg ] 474 | XRL arg ⇒ Some ? [ XRL ? arg ] 475 | CLR arg ⇒ Some ? [ CLR ? arg ] 476 | CPL arg ⇒ Some ? [ CPL ? arg ] 477 | RL arg ⇒ Some ? [ RL ? arg ] 478 | RR arg ⇒ Some ? [ RR ? arg ] 479 | RLC arg ⇒ Some ? [ RLC ? arg ] 480 | RRC arg ⇒ Some ? [ RRC ? arg ] 481 | SWAP arg ⇒ Some ? [ SWAP ? arg ] 482 | MOV arg ⇒ Some ? [ MOV ? arg ] 483 | MOVX arg ⇒ Some ? [ MOVX ? arg ] 484 | SETB arg ⇒ Some ? [ SETB ? arg ] 485 | PUSH arg ⇒ Some ? [ PUSH ? arg ] 486 | POP arg ⇒ Some ? [ POP ? arg ] 487 | XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ] 488 | XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ] 489 | RET ⇒ Some ? [ RET ? ] 490 | RETI ⇒ Some ? [ RETI ? ] 491 | NOP ⇒ Some ? [ RealInstruction (NOP ?) ] 492 ]. 493 494 495 definition expand_pseudo_instruction_safe: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝ 496 λlookup_labels. 497 λlookup_datalabels. 498 λpc. 499 λjmp_len. 500 λi. 501 match i with 502 [ Cost cost ⇒ Some ? [ ] 503 | Comment comment ⇒ Some ? [ ] 504 | Call call ⇒ 505 match jmp_len with 506 [ short_jump ⇒ None ? 507 | medium_jump ⇒ 508 let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in 509 let 〈fst_5, rest〉 ≝ split ? 5 11 pc in 510 if eq_bv ? ignore fst_5 then 511 let address ≝ ADDR11 address in 512 Some ? ([ ACALL address ]) 513 else 514 None ? 515 | long_jump ⇒ 516 let address ≝ ADDR16 (lookup_labels call) in 517 Some ? [ LCALL address ] 518 ] 519 | Mov d trgt ⇒ 520 let address ≝ DATA16 (lookup_datalabels trgt) in 521 Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))] 522 | Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr 523 | Jmp jmp ⇒ 524 match jmp_len with 525 [ short_jump ⇒ 526 let lookup_address ≝ lookup_labels jmp in 527 let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in 528 let 〈upper, lower〉 ≝ split ? 8 8 result in 529 if eq_bv ? upper (zero 8) then 530 let address ≝ RELATIVE lower in 531 Some ? [ SJMP address ] 532 else 533 None ? 534 | medium_jump ⇒ 535 let address ≝ lookup_labels jmp in 536 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in 537 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in 538 if eq_bv ? fst_5_addr fst_5_pc then 539 let address ≝ ADDR11 rest_addr in 540 Some ? ([ AJMP address ]) 541 else 542 None ? 543 | long_jump ⇒ 544 let address ≝ ADDR16 (lookup_labels jmp) in 545 Some ? [ LJMP address ] 546 ] 547 ]. 548 @ I 549 qed. 550 23 551 24 552 definition assembly_1_pseudoinstruction_safe ≝
Note: See TracChangeset
for help on using the changeset viewer.
