 Timestamp:
 May 24, 2011, 6:40:13 PM (9 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASM.ma
r820 r832 111 111 ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l 112 112 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?. 113 113 114 114 inductive preinstruction (A: Type[0]) : Type[0] ≝ 115 115 ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A 
src/ASM/Assembly.ma
r825 r832 410 410 qed. 411 411 412 definition assembly_expansion ≝ 412 inductive jump_length: Type[0] ≝ 413  short_jump: jump_length 414  medium_jump: jump_length 415  long_jump: jump_length. 416 417 axiom jump_expansion_policy: 418 ∀program: pseudo_assembly_program. 419 ∀pc: Word. 420 jump_length. 421 422 definition expand_relative_jump_internal ≝ 423 λjmp_len. 413 424 λi. 414 λcosts: BitVectorTrie Identifier 16. 415 λprogram_counter: nat. 416 match i with 417 [ Instruction instr ⇒ 418 let code_memory ≝ load_code_memory (assembly_preinstruction Identifier (λx. zero 8) instr) in 419 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in 420 let 〈instr', program_counter'〉 ≝ instr_pc' in 421 let program_counter_n' ≝ nat_of_bitvector ? program_counter' in 422 〈program_counter + program_counter_n', costs〉 423  Comment comment ⇒ 〈program_counter, costs〉 424  Cost cost ⇒ 425 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 426 〈program_counter, (insert ? ? program_counter_bv cost costs)〉 427  Jmp jmp ⇒ 428 〈program_counter + 3, costs〉 429  Call call ⇒ 430 〈program_counter + 3, costs〉 431  Mov dptr trgt ⇒ 〈program_counter, costs〉 432 ]. 433 434 definition assembly_1_pseudoinstruction ≝ 425 match jmp_len with 426 [ short_jump ⇒ Some ? [ i ] 427  medium_jump ⇒ None ? 428  long_jump ⇒ 429 Some ? [ RealInstruction i; 430 SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *) 431 LJMP (ADDR16 (bitvector_of_nat ? 0)) (* fill in *) 432 ] 433 ]. 434 @ I 435 qed. 436 437 definition expand_relative_jump: jump_length → preinstruction Identifier → option (list instruction) ≝ 438 λjmp_len: jump_length. 439 λi: preinstruction Identifier. 440 let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in 441 match i with 442 [ JC jmp ⇒ expand_relative_jump_internal jmp_len (JC ? rel_jmp) 443  JNC jmp ⇒ expand_relative_jump_internal jmp_len (JNC ? rel_jmp) 444  JB baddr jmp ⇒ expand_relative_jump_internal jmp_len (JB ? baddr rel_jmp) 445  JZ jmp ⇒ expand_relative_jump_internal jmp_len (JZ ? rel_jmp) 446  JNZ jmp ⇒ expand_relative_jump_internal jmp_len (JNZ ? rel_jmp) 447  JBC baddr jmp ⇒ expand_relative_jump_internal jmp_len (JBC ? baddr rel_jmp) 448  JNB baddr jmp ⇒ expand_relative_jump_internal jmp_len (JNB ? baddr rel_jmp) 449  CJNE addr jmp ⇒ expand_relative_jump_internal jmp_len (CJNE ? addr rel_jmp) 450  DJNZ addr jmp ⇒ expand_relative_jump_internal jmp_len (DJNZ ? addr rel_jmp) 451  ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ] 452  ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ] 453  SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ] 454  INC arg ⇒ Some ? [ INC ? arg ] 455  DEC arg ⇒ Some ? [ DEC ? arg ] 456  MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ] 457  DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ] 458  DA arg ⇒ Some ? [ DA ? arg ] 459  ANL arg ⇒ Some ? [ ANL ? arg ] 460  ORL arg ⇒ Some ? [ ORL ? arg ] 461  XRL arg ⇒ Some ? [ XRL ? arg ] 462  CLR arg ⇒ Some ? [ CLR ? arg ] 463  CPL arg ⇒ Some ? [ CPL ? arg ] 464  RL arg ⇒ Some ? [ RL ? arg ] 465  RR arg ⇒ Some ? [ RR ? arg ] 466  RLC arg ⇒ Some ? [ RLC ? arg ] 467  RRC arg ⇒ Some ? [ RRC ? arg ] 468  SWAP arg ⇒ Some ? [ SWAP ? arg ] 469  MOV arg ⇒ Some ? [ MOV ? arg ] 470  MOVX arg ⇒ Some ? [ MOVX ? arg ] 471  SETB arg ⇒ Some ? [ SETB ? arg ] 472  PUSH arg ⇒ Some ? [ PUSH ? arg ] 473  POP arg ⇒ Some ? [ POP ? arg ] 474  XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ] 475  XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ] 476  RET ⇒ Some ? [ RET ? ] 477  RETI ⇒ Some ? [ RETI ? ] 478  NOP ⇒ Some ? [ RealInstruction (NOP ?) ] 479 ]. 480 @ I 481 qed. 482 483 definition expand_pseudo_instruction: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝ 435 484 λlookup_labels. 436 485 λlookup_datalabels. 437 λaddress_of. 438 λi: labelled_instruction. 439 match \snd i with 440 [ Cost cost ⇒ [ ] 441  Comment comment ⇒ [ ] 442  Call call ⇒ 443 let address ≝ ADDR16 (lookup_labels call) in 444 assembly1 (LCALL address) 445  Mov d trgt ⇒ 446 let address ≝ DATA16 (lookup_datalabels trgt) in 447 assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉)))) 448  Instruction instr ⇒ assembly_preinstruction ? address_of instr 449  Jmp jmp ⇒ 450 let address ≝ ADDR16 (lookup_labels jmp) in 451 assembly1 (LJMP address) 452 (*  WithLabel jmp ⇒ assembly1 (assembly_jump jmp (address_of labels)) 453 *) 454 ]. 486 λpc. 487 λjmp_len. 488 λi. 489 match i with 490 [ Cost cost ⇒ Some ? [ ] 491  Comment comment ⇒ Some ? [ ] 492  Call call ⇒ 493 match jmp_len with 494 [ short_jump ⇒ None ? 495  medium_jump ⇒ 496 let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in 497 let 〈fst_5, rest〉 ≝ split ? 5 11 pc in 498 if eq_bv ? ignore fst_5 then 499 let address ≝ ADDR11 address in 500 Some ? ([ ACALL address ]) 501 else 502 None ? 503  long_jump ⇒ 504 let address ≝ ADDR16 (lookup_labels call) in 505 Some ? [ LCALL address ] 506 ] 507  Mov d trgt ⇒ 508 let address ≝ DATA16 (lookup_datalabels trgt) in 509 Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))] 510  Instruction instr ⇒ expand_relative_jump jmp_len instr 511  Jmp jmp ⇒ 512 match jmp_len with 513 [ short_jump ⇒ 514 let lookup_address ≝ lookup_labels jmp in 515 let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in 516 let 〈upper, lower〉 ≝ split ? 8 8 result in 517 if eq_bv ? upper (zero 8) then 518 let address ≝ RELATIVE lower in 519 Some ? [ SJMP address ] 520 else 521 None ? 522  medium_jump ⇒ 523 let address ≝ lookup_labels jmp in 524 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in 525 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in 526 if eq_bv ? fst_5_addr fst_5_pc then 527 let address ≝ ADDR11 rest_addr in 528 Some ? ([ AJMP address ]) 529 else 530 None ? 531  long_jump ⇒ 532 let address ≝ ADDR16 (lookup_labels jmp) in 533 Some ? [ LJMP address ] 534 ] 535 ]. 455 536 @ I 456 537 qed. 538 539 definition assembly_1_pseudoinstruction ≝ 540 λprogram. 541 λpc. 542 λlookup_labels. 543 λlookup_datalabels. 544 λi. 545 let expansion ≝ jump_expansion_policy program pc in 546 match (expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i) with 547 [ None ⇒ None ? 548  Some pseudos ⇒ Some ? (flatten ? (map ? ? assembly1 pseudos)) 549 ]. 457 550 458 551 definition construct_datalabels ≝ … … 466 559 〈(Stub ? ?), 0〉 preamble). 467 560 468 definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 469 λp. 470 let 〈preamble, instr_list〉 ≝ p in 471 let datalabels ≝ construct_datalabels preamble in 472 let 〈labels,pc_costs〉 ≝ 473 foldl ((BitVectorTrie ? ?) × (nat × (BitVectorTrie ? ?))) ? ( 474 λt. λi. 475 let 〈label, i〉 ≝ i in 476 let 〈labels, pc_costs〉 ≝ t in 477 let 〈program_counter, costs〉 ≝ pc_costs in 478 let labels ≝ match label with 479 [ None ⇒ labels 480  Some label ⇒ 481 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 482 insert ? ? label program_counter_bv labels 483 ] in 484 〈labels, assembly_expansion i costs program_counter〉 485 ) 〈(Stub ? ?), 〈0,(Stub ? ?)〉〉 instr_list in 486 let 〈program_counter, costs〉 ≝ pc_costs in 487 if gtb program_counter (2^16) then (* 65536 *) 561 definition is_jump ≝ 562 λi: preinstruction Identifier. 563 match i with 564 [ JC _ ⇒ true 565  JNC _ ⇒ true 566  JB _ _ ⇒ true 567  JNB _ _ ⇒ true 568  JBC _ _ ⇒ true 569  JZ _ ⇒ true 570  JNZ _ ⇒ true 571  CJNE _ _ ⇒ true 572  DJNZ _ _ ⇒ true 573  _ ⇒ false 574 ]. 575 576 definition construct_costs ≝ 577 λprogram. 578 λprogram_counter: nat. 579 λlookup_labels. 580 λlookup_datalabels. 581 λcosts: BitVectorTrie Word 16. 582 λi. 583 match i with 584 [ Comment comment ⇒ Some ? 〈program_counter, costs〉 585  Cost cost ⇒ 586 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 587 Some ? 〈program_counter, (insert ? ? program_counter_bv cost costs)〉 588  _ ⇒ 589 let pc_bv ≝ bitvector_of_nat ? program_counter in 590 let assembled ≝ assembly_1_pseudoinstruction program pc_bv 591 lookup_labels lookup_datalabels i in 592 match assembled with 593 [ None ⇒ None ? 594  Some assembled ⇒ 595 let code_memory ≝ load_code_memory assembled in 596 let pc ≝ foldr ? ? (λy. λpc. 597 let 〈instr_pc', ignore〉 ≝ fetch code_memory pc in 598 let 〈instr', program_counter'〉 ≝ instr_pc' in 599 program_counter') (zero ?) assembled in 600 Some ? 〈(nat_of_bitvector 16 pc) + program_counter, costs〉 601 ] 602 ]. 603 604 definition build_maps ≝ 605 λinstr_list. 606 let result ≝ foldl (option ((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16)))) ? 607 (λt. λi. 608 let 〈label, i〉 ≝ i in 609 match t with 610 [ None ⇒ None ? 611  Some t ⇒ 612 let 〈labels, pc_costs〉 ≝ t in 613 let 〈program_counter, costs〉 ≝ pc_costs in 614 let labels ≝ 615 match label with 616 [ None ⇒ labels 617  Some label ⇒ 618 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 619 insert ? ? label program_counter_bv labels 620 ] 621 in 622 match construct_costs instr_list program_counter (λx. zero ?) (λx. zero ?) costs i with 623 [ None ⇒ None ? 624  Some construct ⇒ Some ? 〈labels, construct〉 625 ] 626 ]) (Some ? 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉) (\snd instr_list) in 627 match result with 628 [ None ⇒ None ? 629  Some result ⇒ 630 let 〈labels, pc_costs〉 ≝ result in 631 let 〈pc, costs〉 ≝ pc_costs in 632 if gtb pc (2^16) then 488 633 None ? 489 634 else 490 let flat_list ≝ flatten ? ( 491 map ? ? ( 492 assembly_1_pseudoinstruction ( 493 λx. lookup ? ? x labels (zero ?)) 494 (λx. lookup ? ? x datalabels (zero ?)) 495 (address_of labels)) instr_list) in 496 Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉. 635 Some ? 〈labels, costs〉 636 ]. 637 638 check lookup. 639 640 definition assembly ≝ 641 λp. 642 λpc. 643 let 〈preamble, instr_list〉 ≝ p in 644 match build_maps p with 645 [ None ⇒ None ? 646  Some maps ⇒ 647 let labels ≝ \fst maps in 648 let datalabels ≝ construct_datalabels preamble in 649 match build_maps p with 650 [ None ⇒ None ? 651  Some labels_costs ⇒ 652 let 〈labels,costs〉 ≝ labels_costs in 653 let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in 654 let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in 655 let to_flatten ≝ map ? ? (λx. assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels x) instr_list in 656 (* 657 foldr ? ? (λx. λy. 658 match y with 659 [ None ⇒ None ? 660  Some lst ⇒ 661 match x with 662 [ None ⇒ None ? 663  Some x ⇒ Some ? (x @ lst) 664 ] 665 ]) (Some ? [ ]) to_flatten *) ? 666 ] 667 ]. 668 669 (* 670 if then (* 65536 *) 671 None ? 672 else 673 let flat_list ≝ flatten ? ( 674 map ? ? ( 675 assembly_1_pseudoinstruction ( 676 λx. lookup ? ? x labels (zero ?)) 677 (λx. lookup ? ? x datalabels (zero ?)) 678 (address_of labels)) instr_list) in 679 Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉 680 *) 681 497 682 (* 498 683 [2,3,4,5,6: … … 511 696 qed. *) 512 697 698 699 513 700 definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 514 701 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉). 
src/ASM/AssemblyProof.ma
r831 r832 50 50 # H 51 51 whd 52 normalize52 whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?]) 53 53 ] 54 54  cases not_implemented
Note: See TracChangeset
for help on using the changeset viewer.