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

 1 edited
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.