Changeset 1709 for src/ASM/Interpret.ma
 Timestamp:
 Feb 17, 2012, 11:52:36 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r1666 r1709 1 1 include "ASM/StatusProofs.ma". 2 include "common/StructuredTraces.ma". 2 3 include "ASM/Fetch.ma". 3 4 … … 119 120 include alias "ASM/BitVectorTrie.ma". 120 121 122 definition ASM_classify0: instruction → status_class ≝ 123 λi: instruction. 124 match i with 125 [ RealInstruction pre ⇒ 126 match pre with 127 [ RET ⇒ cl_return 128  JZ _ ⇒ cl_jump 129  JNZ _ ⇒ cl_jump 130  JC _ ⇒ cl_jump 131  JNC _ ⇒ cl_jump 132  JB _ _ ⇒ cl_jump 133  JNB _ _ ⇒ cl_jump 134  JBC _ _ ⇒ cl_jump 135  CJNE _ _ ⇒ cl_jump 136  DJNZ _ _ ⇒ cl_jump 137  _ ⇒ cl_other 138 ] 139  ACALL _ ⇒ cl_call 140  LCALL _ ⇒ cl_call 141  JMP _ ⇒ cl_call 142  AJMP _ ⇒ cl_jump 143  LJMP _ ⇒ cl_jump 144  SJMP _ ⇒ cl_jump 145  _ ⇒ cl_other 146 ]. 147 148 definition current_instruction0 ≝ 149 λcode_memory: BitVectorTrie Byte 16. 150 λprogram_counter: Word. 151 \fst (\fst (fetch … code_memory program_counter)). 152 153 definition current_instruction ≝ 154 λcode_memory. 155 λs: Status code_memory. 156 current_instruction0 code_memory (program_counter … s). 157 158 definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝ 159 λcode_memory. 160 λs: Status code_memory. 161 ASM_classify0 (current_instruction … s). 162 121 163 definition execute_1_preinstruction': 122 164 ∀ticks: nat × nat. … … 124 166 ∀s: PreStatus m cm. 125 167 Σs': PreStatus m cm. 126 Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) ≝ 168 And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s)) 169 (ASM_classify cm s' = cl_other → program_counter … s' = \fst (\snd (fetch … s))) ≝ 127 170 λticks: nat × nat. 128 171 λa, m: Type[0]. λcm. … … 132 175 let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in 133 176 let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in 134 match instr in preinstruction return λx. Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock ?? s) (clock ?? s' = \snd ticks + clock ?? s)with177 match instr in preinstruction return λx. Σs': ?. ? with 135 178 [ ADD addr1 addr2 ⇒ 136 179 let s ≝ add_ticks1 s in … … 554 597 qed. 555 598 599 discriminator Prod. 600 556 601 definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat. 557 Σs': Status cm. clock ?? s' = \snd current + clock … s ≝ 602 Σs': Status cm. 603 And (clock ?? s' = \snd current + clock … s) 604 (ASM_classify0 (\fst (\fst current)) = cl_other → 605 program_counter ? ? s' = \snd (\fst current)) ≝ 558 606 λcm,s0,instr_pc_ticks. 559 let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in560 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in607 let 〈instr_pc, ticks〉 as INSTR_PC_TICKS ≝ instr_pc_ticks in 608 let 〈instr, pc〉 as INSTR_PC ≝ 〈fst … instr_pc, snd … instr_pc〉 in 561 609 let s ≝ set_program_counter … s0 pc in 562 match instr return λ _.Status cmwith563 [ RealInstruction instr ⇒execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] …610 match instr return λx. x = instr → Σs:?.? with 611 [ RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] … 564 612 (λx. λs. 565 613 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with 566 614 [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r)) 567 615  _ ⇒ λabsd. ⊥ 568 ] (subaddressing_modein … x)) instr s569  MOVC addr1 addr2 ⇒ 570 let s ≝ set_clock …s (ticks + clock … s) in571 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0with616 ] (subaddressing_modein … x)) instr' s 617  MOVC addr1 addr2 ⇒ λinstr_refl. 618 let s ≝ set_clock ?? s (ticks + clock … s) in 619 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':?. ? with 572 620 [ ACC_DPTR ⇒ λacc_dptr: True. 573 621 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in … … 578 626  ACC_PC ⇒ λacc_pc: True. 579 627 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in 580 let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ?? s) (bitvector_of_nat 16 1) in581 628 (* DPM: Under specified: does the carry from PC incrementation affect the *) 582 629 (* addition of the PC with the DPTR? At the moment, no. *) 583 let s ≝ set_program_counter … s inc_pc in 584 let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in 630 let 〈carry, new_addr〉 ≝ half_add ? (program_counter … s) big_acc in 585 631 let result ≝ lookup ? ? new_addr cm (zero ?) in 586 632 set_8051_sfr … s SFR_ACC_A result 587 633  _ ⇒ λother: False. ⊥ 588 634 ] (subaddressing_modein … addr2) 589  JMP _ ⇒ (* DPM: always indirect_dptr *)590 let s ≝ set_clock …s (ticks + clock … s) in635  JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *) 636 let s ≝ set_clock ?? s (ticks + clock … s) in 591 637 let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in 592 638 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in … … 594 640 let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) jmp_addr in 595 641 set_program_counter … s new_pc 596  LJMP addr ⇒ 597 let s ≝ set_clock …s (ticks + clock … s) in598 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0with642  LJMP addr ⇒ λinstr_refl. 643 let s ≝ set_clock ?? s (ticks + clock … s) in 644 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': ?.? with 599 645 [ ADDR16 a ⇒ λaddr16: True. 600 646 set_program_counter … s a 601 647  _ ⇒ λother: False. ⊥ 602 648 ] (subaddressing_modein … addr) 603  SJMP addr ⇒ 604 let s ≝ set_clock …s (ticks + clock … s) in605 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0with649  SJMP addr ⇒ λinstr_refl. 650 let s ≝ set_clock ?? s (ticks + clock … s) in 651 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with 606 652 [ RELATIVE r ⇒ λrelative: True. 607 653 let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) (sign_extension r) in … … 609 655  _ ⇒ λother: False. ⊥ 610 656 ] (subaddressing_modein … addr) 611  AJMP addr ⇒ 612 let s ≝ set_clock …s (ticks + clock … s) in613 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0with657  AJMP addr ⇒ λinstr_refl. 658 let s ≝ set_clock ?? s (ticks + clock … s) in 659 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with 614 660 [ ADDR11 a ⇒ λaddr11: True. 615 661 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in … … 622 668  _ ⇒ λother: False. ⊥ 623 669 ] (subaddressing_modein … addr) 624  ACALL addr ⇒ 625 let s ≝ set_clock …s (ticks + clock … s) in626 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0with670  ACALL addr ⇒ λinstr_refl. 671 let s ≝ set_clock ?? s (ticks + clock … s) in 672 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with 627 673 [ ADDR11 a ⇒ λaddr11: True. 628 674 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in … … 639 685  _ ⇒ λother: False. ⊥ 640 686 ] (subaddressing_modein … addr) 641  LCALL addr ⇒ 642 let s ≝ set_clock …s (ticks + clock … s) in643 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0with687  LCALL addr ⇒ λinstr_refl. 688 let s ≝ set_clock ?? s (ticks + clock … s) in 689 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with 644 690 [ ADDR16 a ⇒ λaddr16: True. 645 691 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in … … 653 699  _ ⇒ λother: False. ⊥ 654 700 ] (subaddressing_modein … addr) 655 ]. (*10s*) 656 [*:try assumption] 701 ] (refl … instr). (*10s*) 702 try assumption 703 [1,2,3,4,5,6,7,8: 704 normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS % 705 try // 706 destruct(INSTR_PC) <instr_refl 707 #absurd normalize in absurd; try destruct(absurd) try % 708 9: 709 657 710 [1,2,3,4,5,7: @pi2 (*35s*) 658 8: lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] … 711 8: cases daemon (* 712 lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] … 659 713 (λx. λs. 660 714 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with 661 715 [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r)) 662 716  _ ⇒ λabsd. ⊥ 663 ] (subaddressing_modein … x)) instr1 s1) try @absd * #H @H 717 ] (subaddressing_modein … x)) instr1 s1) try @absd * #H @H *) 718 (*XXX : propagate further *) 719 28,48,68,88,108,128: skip 720 *: 721 try assumption 722 normalize nodelta 723 try // >clock_set_program_counter % 724 try // destruct destruct (* XXX: for wilmer! *) >e1 725 whd in match ASM_classify; normalize nodelta 726 whd in match current_instruction; normalize nodelta 727 whd in match current_instruction0; normalize nodelta 728 [*:try assumption] 664 729 *: normalize nodelta try // (*17s*) 665 730 >clock_set_program_counter // (* Andrea:??*) ]
Note: See TracChangeset
for help on using the changeset viewer.