Changeset 1615
- Timestamp:
- Dec 14, 2011, 5:28:11 PM (8 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.