Changeset 822
 Timestamp:
 May 23, 2011, 4:22:13 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r821 r822 158 158 include alias "ASM/BitVectorTrie.ma". 159 159 160 definition execute_1_preinstruction: ∀A, M: Type[0]. (A → Byte) → preinstruction A → PreStatus M → PreStatus M ≝160 definition execute_1_preinstruction: ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝ 161 161 λA, M: Type[0]. 162 λaddr_of: A → Byte.162 λaddr_of: A → (PreStatus M) → Word. 163 163 λinstr: preinstruction A. 164 164 λs: PreStatus M. … … 205 205  inr r ⇒ 206 206 let 〈addr1, addr2〉 ≝ r in 207 let and_val ≝ (get_cy_flag ? s) ∧(get_arg_1 ? s addr2 true) in207 let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in 208 208 set_flags ? s and_val (None ?) (get_ov_flag ? s) 209 209 ] … … 439 439 ] 440 440  JC addr ⇒ 441 let r ≝ addr_of addr in442 441 if get_cy_flag ? s then 443 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 444 set_program_counter ? s new_pc 442 set_program_counter ? s (addr_of addr s) 445 443 else 446 444 s 447 445  JNC addr ⇒ 448 let r ≝ addr_of addr in449 446 if ¬(get_cy_flag ? s) then 450 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 451 set_program_counter ? s new_pc 447 set_program_counter ? s (addr_of addr s) 452 448 else 453 449 s 454 450  JB addr1 addr2 ⇒ 455 let r ≝ addr_of addr2 in456 451 if get_arg_1 ? s addr1 false then 457 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 458 set_program_counter ? s new_pc 452 set_program_counter ? s (addr_of addr2 s) 459 453 else 460 454 s 461 455  JNB addr1 addr2 ⇒ 462 let r ≝ addr_of addr2 in463 456 if ¬(get_arg_1 ? s addr1 false) then 464 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 465 set_program_counter ? s new_pc 457 set_program_counter ? s (addr_of addr2 s) 466 458 else 467 459 s 468 460  JBC addr1 addr2 ⇒ 469 let r ≝ addr_of addr2 in470 461 let s ≝ set_arg_1 ? s addr1 false in 471 462 if get_arg_1 ? s addr1 false then 472 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 473 set_program_counter ? s new_pc 463 set_program_counter ? s (addr_of addr2 s) 474 464 else 475 465 s 476 466  JZ addr ⇒ 477 let r ≝ addr_of addr in478 467 if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then 479 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 480 set_program_counter ? s new_pc 468 set_program_counter ? s (addr_of addr s) 481 469 else 482 470 s 483 471  JNZ addr ⇒ 484 let r ≝ addr_of addr in485 472 if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then 486 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 487 set_program_counter ? s new_pc 473 set_program_counter ? s (addr_of addr s) 488 474 else 489 475 s 490 476  CJNE addr1 addr2 ⇒ 491 let r ≝ addr_of addr2 in492 477 match addr1 with 493 478 [ inl l ⇒ 494 let 〈addr1, addr2 〉 ≝ l in479 let 〈addr1, addr2'〉 ≝ l in 495 480 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1)) 496 (nat_of_bitvector ? (get_arg_8 ? s false addr2)) in 497 if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2)) then 498 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 499 let s ≝ set_program_counter ? s new_pc in 481 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in 482 if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then 483 let s ≝ set_program_counter ? s (addr_of addr2 s) in 500 484 set_flags ? s new_cy (None ?) (get_ov_flag ? s) 501 485 else 502 486 (set_flags ? s new_cy (None ?) (get_ov_flag ? s)) 503 487  inr r' ⇒ 504 let 〈addr1, addr2 〉 ≝ r' in488 let 〈addr1, addr2'〉 ≝ r' in 505 489 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ? s false addr1)) 506 (nat_of_bitvector ? (get_arg_8 ? s false addr2)) in 507 if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2)) then 508 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 509 let s ≝ set_program_counter ? s new_pc in 490 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in 491 if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then 492 let s ≝ set_program_counter ? s (addr_of addr2 s) in 510 493 set_flags ? s new_cy (None ?) (get_ov_flag ? s) 511 494 else … … 513 496 ] 514 497  DJNZ addr1 addr2 ⇒ 515 let r ≝ addr_of addr2 in516 498 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr1) (bitvector_of_nat 8 1) false in 517 499 let s ≝ set_arg_8 ? s addr1 result in 518 500 if ¬(eq_bv ? result (zero 8)) then 519 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 520 set_program_counter ? s new_pc 501 set_program_counter ? s (addr_of addr2 s) 521 502 else 522 503 s … … 548 529 match instr with 549 530 [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]] ? 550 (λx. 531 (λx. λs. 551 532 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with 552 [ RELATIVE r ⇒ λ_. r533 [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r)) 553 534  _ ⇒ λabsd. ⊥ 554 535 ] (subaddressing_modein … x)) instr s … … 651 632 qed. 652 633 653 axiom fetch_pseudo_instruction: 654 ∀ps: PseudoStatus. 655 ∀pc: Word. 656 (pseudo_instruction × Word) × nat. 657 658 axiom address_of_labels: Identifier → Byte. 659 axiom address_of_word_labels: Identifier → Word. 660 661 definition execute_1_pseudo_instruction: PseudoStatus → PseudoStatus ≝ 634 definition fetch_pseudo_instruction: PseudoStatus → Word → (Word → nat) → ((pseudo_instruction × Word) × nat) ≝ 635 λps: PseudoStatus. 636 λpc: Word. 637 λticks_of: Word → nat. 638 let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … (code_memory ? ps) ? in 639 let 〈flags, new_pc〉 ≝ half_add ? pc (bitvector_of_nat ? 1) in 640 〈〈instr, new_pc〉, ticks_of pc〉. 641 cases not_implemented. 642 qed. 643 644 let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝ 645 match l with 646 [ nil ⇒ ? 647  cons hd tl ⇒ 648 if pred hd then 649 acc 650 else 651 index_of_internal A pred tl (S acc) 652 ]. 653 cases not_implemented. 654 qed. 655 656 definition index_of ≝ 657 λA. 658 λeq. 659 λl. 660 index_of_internal A eq l 0. 661 662 definition address_of_word_labels_internal ≝ 663 λy: Identifier. 664 λx: labelled_instruction. 665 match \fst x with 666 [ None ⇒ false 667  Some x ⇒ eq_bv ? x y 668 ]. 669 670 definition address_of_word_labels ≝ 671 λps: PseudoStatus. 672 λid: Identifier. 673 bitvector_of_nat 16 (index_of ? (address_of_word_labels_internal id) (code_memory ? ps)). 674 675 definition execute_1_pseudo_instruction: (Word → nat) → PseudoStatus → PseudoStatus ≝ 676 λticks_of. 662 677 λs. 663 let 〈instr_pc, ticks〉 ≝ fetch_pseudo_instruction s (program_counter ? s) in678 let 〈instr_pc, ticks〉 ≝ fetch_pseudo_instruction s (program_counter ? s) ticks_of in 664 679 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 665 680 let s ≝ set_clock ? s (clock ? s + ticks) in … … 667 682 let s ≝ 668 683 match instr with 669 [ Instruction instr ⇒ execute_1_preinstruction … address_of_labelsinstr s684 [ Instruction instr ⇒ execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s 670 685  Comment cmt ⇒ s 671 686  Cost cst ⇒ s 672  Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels jmp)687  Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp) 673 688  Call call ⇒ 674 let a ≝ address_of_word_labels call in689 let a ≝ address_of_word_labels s call in 675 690 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 676 691 let s ≝ set_8051_sfr ? s SFR_SP new_sp in … … 681 696 let s ≝ write_at_stack_pointer ? s pc_bu in 682 697 set_program_counter ? s a 683  Mov dptr ident ⇒ set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels ident))) dptr698  Mov dptr ident ⇒ set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr 684 699 ] 685 700 in … … 695 710 ]. 696 711 697 let rec execute_pseudo_instruction (n: nat) ( s: PseudoStatus) on n: PseudoStatus ≝712 let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat) (s: PseudoStatus) on n: PseudoStatus ≝ 698 713 match n with 699 714 [ O ⇒ s 700  S o ⇒ execute_pseudo_instruction o (execute_1_pseudo_instructions)715  S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_of s) 701 716 ].
Note: See TracChangeset
for help on using the changeset viewer.