Changeset 820 for src/ASM/Assembly.ma
 Timestamp:
 May 20, 2011, 6:09:00 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r757 r820 5 5 include "ASM/Status.ma". 6 6 7 definition assembly1 ≝ 8 λi: instruction. 9 match i with 10 [ ACALL addr ⇒ 11 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 12 [ ADDR11 w ⇒ λ_. 13 let 〈v1,v2〉 ≝ split ? 3 8 w in 14 [ (v1 @@ [[true; false; false; false; true]]) ; v2 ] 15  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 16  ADD addr1 addr2 ⇒ 7 definition assembly_preinstruction ≝ 8 λA: Type[0]. 9 λaddr_of: A → Byte. (* relative *) 10 λpre: preinstruction A. 11 match pre with 12 [ ADD addr1 addr2 ⇒ 17 13 match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with 18 14 [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ] … … 28 24  DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ] 29 25  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 30  AJMP addr ⇒31 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with32 [ ADDR11 w ⇒ λ_.33 let 〈v1,v2〉 ≝ split ? 3 8 w in34 [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]35  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)36 26  ANL addrs ⇒ 37 27 match addrs with … … 90 80 [ ([[false; false; false; true; false; true; true; i1]]) ] 91 81  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 92  DIV addr1 addr2 ⇒ 93 [ ([[true;false;false;false;false;true;false;false]]) ] 94  Jump j ⇒ 95 match j with 96 [ DJNZ addr1 addr2 ⇒ 97 let b2 ≝ 98 match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 99 [ RELATIVE b2 ⇒ λ_. b2 100  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 82  DJNZ addr1 addr2 ⇒ 83 let b2 ≝ addr_of addr2 in 101 84 match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with 102 85 [ REGISTER r ⇒ λ_. … … 106 89  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 107 90  JC addr ⇒ 108 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 109 [ RELATIVE b1 ⇒ λ_. 110 [ ([[false; true; false; false; false; false; false; false]]); b1 ] 111  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 91 let b1 ≝ addr_of addr in 92 [ ([[false; true; false; false; false; false; false; false]]); b1 ] 112 93  JNC addr ⇒ 113 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 114 [ RELATIVE b1 ⇒ λ_. 115 [ ([[false; true; false; true; false; false; false; false]]); b1 ] 116  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 94 let b1 ≝ addr_of addr in 95 [ ([[false; true; false; true; false; false; false; false]]); b1 ] 117 96  JZ addr ⇒ 118 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 119 [ RELATIVE b1 ⇒ λ_. 120 [ ([[false; true; true; false; false; false; false; false]]); b1 ] 121  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 97 let b1 ≝ addr_of addr in 98 [ ([[false; true; true; false; false; false; false; false]]); b1 ] 122 99  JNZ addr ⇒ 123 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 124 [ RELATIVE b1 ⇒ λ_. 125 [ ([[false; true; true; true; false; false; false; false]]); b1 ] 126  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 100 let b1 ≝ addr_of addr in 101 [ ([[false; true; true; true; false; false; false; false]]); b1 ] 127 102  JB addr1 addr2 ⇒ 128 let b2 ≝ 129 match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 130 [ RELATIVE b2 ⇒ λ_. b2 131  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 103 let b2 ≝ addr_of addr2 in 132 104 match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 133 105 [ BIT_ADDR b1 ⇒ λ_. … … 135 107  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 136 108  JNB addr1 addr2 ⇒ 137 let b2 ≝ 138 match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 139 [ RELATIVE b2 ⇒ λ_. b2 140  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 109 let b2 ≝ addr_of addr2 in 141 110 match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 142 111 [ BIT_ADDR b1 ⇒ λ_. … … 144 113  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 145 114  JBC addr1 addr2 ⇒ 146 let b2 ≝ 147 match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 148 [ RELATIVE b2 ⇒ λ_. b2 149  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 115 let b2 ≝ addr_of addr2 in 150 116 match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 151 117 [ BIT_ADDR b1 ⇒ λ_. … … 153 119  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 154 120  CJNE addrs addr3 ⇒ 155 let b3 ≝ 156 match addr3 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 157 [ RELATIVE b3 ⇒ λ_. b3 158  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in 121 let b3 ≝ addr_of addr3 in 159 122 match addrs with 160 123 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in … … 171 134  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 172 135 match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with 173 [ REGISTER r ⇒ λ_.136 [ REGISTER r ⇒ λ_. 174 137 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ] 175 138  INDIRECT i1 ⇒ λ_. 176 139 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ] 177  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) ]] 140  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 141 ] 142  DIV addr1 addr2 ⇒ 143 [ ([[true;false;false;false;false;true;false;false]]) ] 178 144  INC addr ⇒ 179 145 match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with … … 188 154  DPTR ⇒ λ_. 189 155 [ ([[true;false;true;false;false;false;true;true]]) ] 190  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)191  JMP addr ⇒192 [ ([[false;true;true;true;false;false;true;true]]) ]193  LCALL addr ⇒194 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with195 [ ADDR16 w ⇒ λ_.196 let 〈b1,b2〉 ≝ split ? 8 8 w in197 [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]198  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)199  LJMP addr ⇒200 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with201 [ ADDR16 w ⇒ λ_.202 let 〈b1,b2〉 ≝ split ? 8 8 w in203 [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]204 156  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 205 157  MOV addrs ⇒ … … 263 215 [ ([[true;false;false;true;false;false;true;false]]); b1 ] 264 216  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)] 265  MOVC addr1 addr2 ⇒266 match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with267 [ ACC_DPTR ⇒ λ_.268 [ ([[true;false;false;true;false;false;true;true]]) ]269  ACC_PC ⇒ λ_.270 [ ([[true;false;false;false;false;false;true;true]]) ]271  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)272 217  MOVX addrs ⇒ 273 218 match addrs with … … 348 293 [ ([[true;true;false;true;false;false;true;false]]); b1 ] 349 294  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 350  SJMP addr ⇒351 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with352 [ RELATIVE b1 ⇒ λ_.353 [ ([[true;false;false;false;false;false;false;false]]); b1 ]354  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)355 295  SUBB addr1 addr2 ⇒ 356 296 match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with … … 403 343  DATA b2 ⇒ λ_. 404 344 [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ] 405  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]]. 406 407 definition assembly_jump: (jump Identifier) → (Identifier → [[relative]]) → instruction ≝ 408 λj: jump Identifier. 409 λaddr_of: Identifier → [[relative]]. 410 match j with 411 [ JC jmp ⇒ Jump ? (JC ? (addr_of jmp)) 412  JNC jmp ⇒ Jump ? (JNC ? (addr_of jmp)) 413  JZ jmp ⇒ Jump ? (JZ ? (addr_of jmp)) 414  JNZ jmp ⇒ Jump ? (JNZ ? (addr_of jmp)) 415  JB jmp jmp' ⇒ Jump ? (JB ? jmp (addr_of jmp')) 416  JNB jmp jmp' ⇒ Jump ? (JNB ? jmp (addr_of jmp')) 417  JBC jmp jmp' ⇒ Jump ? (JBC ? jmp (addr_of jmp')) 418  CJNE jmp jmp' ⇒ Jump ? (CJNE ? jmp (addr_of jmp')) 419  DJNZ jmp jmp' ⇒ Jump ? (DJNZ ? jmp (addr_of jmp')) 420 ]. 345  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 346 ]. 421 347 422 definition address_of: BitVectorTrie Word 16 → Identifier → addressing_mode ≝ 348 definition assembly1 ≝ 349 λi: instruction. 350 match i with 351 [ ACALL addr ⇒ 352 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 353 [ ADDR11 w ⇒ λ_. 354 let 〈v1,v2〉 ≝ split ? 3 8 w in 355 [ (v1 @@ [[true; false; false; false; true]]) ; v2 ] 356  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 357  AJMP addr ⇒ 358 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 359 [ ADDR11 w ⇒ λ_. 360 let 〈v1,v2〉 ≝ split ? 3 8 w in 361 [ (v1 @@ [[false; false; false; false; true]]) ; v2 ] 362  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 363  JMP adptr ⇒ 364 [ ([[false;true;true;true;false;false;true;true]]) ] 365  LCALL addr ⇒ 366 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with 367 [ ADDR16 w ⇒ λ_. 368 let 〈b1,b2〉 ≝ split ? 8 8 w in 369 [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ] 370  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 371  LJMP addr ⇒ 372 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with 373 [ ADDR16 w ⇒ λ_. 374 let 〈b1,b2〉 ≝ split ? 8 8 w in 375 [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ] 376  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 377  MOVC addr1 addr2 ⇒ 378 match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with 379 [ ACC_DPTR ⇒ λ_. 380 [ ([[true;false;false;true;false;false;true;true]]) ] 381  ACC_PC ⇒ λ_. 382 [ ([[true;false;false;false;false;false;true;true]]) ] 383  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 384  SJMP addr ⇒ 385 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 386 [ RELATIVE b1 ⇒ λ_. 387 [ ([[true;false;false;false;false;false;false;false]]); b1 ] 388  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 389  RealInstruction instr ⇒ 390 assembly_preinstruction [[ relative ]] 391 (λx. 392 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with 393 [ RELATIVE r ⇒ λ_. r 394  _ ⇒ λabsd. ⊥ 395 ] (subaddressing_modein … x)) instr 396 ]. 397 cases absd 398 qed. 399 400 definition address_of: BitVectorTrie Word 16 → Identifier → Byte ≝ 423 401 λmap. 424 402 λid: Identifier. … … 426 404 let 〈high, low〉 ≝ split ? 8 8 address in 427 405 if eq_bv ? high (zero ?) then 428 RELATIVElow406 low 429 407 else 430 408 ?. … … 432 410 qed. 433 411 434 definition assembly: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝412 definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 435 413 λp. 436 414 let 〈preamble, instr_list〉 ≝ p in … … 458 436 match i with 459 437 [ Instruction instr ⇒ 460 let code_memory ≝ load_code_memory (assembly 1instr) in438 let code_memory ≝ load_code_memory (assembly_preinstruction Identifier (λx. zero 8) instr) in 461 439 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in 462 440 let 〈instr', program_counter'〉 ≝ instr_pc' in … … 472 450 〈program_counter + 3, costs〉 473 451  Mov dptr trgt ⇒ pc_costs 474  WithLabel jmp ⇒475 let fake_addr ≝ RELATIVE (zero 8) in476 let fake_jump ≝ assembly_jump jmp (λx: Identifier. fake_addr) in477 let code_memory ≝ load_code_memory (assembly1 fake_jump) in478 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in479 let 〈instr', program_counter'〉 ≝ instr_pc' in480 let program_counter_n' ≝ nat_of_bitvector 16 program_counter' in481 〈program_counter + program_counter_n', costs〉482 452 ]〉 483 453 ) 〈(Stub ? ?), 〈0,(Stub ? ?)〉〉 instr_list in … … 496 466 let pc_offset ≝ lookup ? ? call labels (zero ?) in 497 467 let address ≝ ADDR16 pc_offset in 498 assembly1 (LCALL ?address)468 assembly1 (LCALL address) 499 469  Mov d trgt ⇒ 500 470 let pc_offset ≝ lookup ? ? trgt datalabels (zero ?) in 501 471 let address ≝ DATA16 pc_offset in 502 472 assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉)))) 503  Instruction instr ⇒ assembly 1instr473  Instruction instr ⇒ assembly_preinstruction ? (address_of labels) instr 504 474  Jmp jmp ⇒ 505 475 let pc_offset ≝ lookup ? ? jmp labels (zero ?) in 506 476 let address ≝ ADDR16 pc_offset in 507 assembly1 (LJMP ? address) 508  WithLabel jmp ⇒ assembly1 (assembly_jump jmp (address_of labels)) 477 assembly1 (LJMP address) 478 (*  WithLabel jmp ⇒ assembly1 (assembly_jump jmp (address_of labels)) 479 *) 509 480 ] 510 481 ) instr_list … … 514 485 normalize; %; 515 486  whd in ⊢ (? (? ? ? %)); 516 cases (split bool 8 8 (lookup Word 16 c0labels (zero 16)))487 cases (split bool 8 8 (lookup Word 16 trgt labels (zero 16))) 517 488 # high 518 489 # low … … 526 497 qed. 527 498 528 definition assembly_unlabelled_program: list instruction→ option (list Byte × (BitVectorTrie Identifier 16)) ≝499 definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 529 500 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉). 530 501
Note: See TracChangeset
for help on using the changeset viewer.