Changeset 1615 for src/ASM/Policy.ma
 Timestamp:
 Dec 14, 2011, 5:28:11 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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