Changeset 1615
 Timestamp:
 Dec 14, 2011, 5:28:11 PM (9 years ago)
 Location:
 src/ASM
 Files:

 2 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 ≝ 
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.