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

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r757 r820 158 158 include alias "ASM/BitVectorTrie.ma". 159 159 160 definition execute_1: Status → Status ≝ 160 definition execute_1_preinstruction: ∀A: Type[0]. (A → Byte) → preinstruction A → Status → Status ≝ 161 λA: Type[0]. 162 λaddr_of: A → Byte. 163 λinstr: preinstruction A. 161 164 λs: Status. 162 let 〈instr_pc, ticks〉 ≝ fetch (code_memory s) (program_counter s) in 163 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 164 let s ≝ set_clock s (clock s + ticks) in 165 let s ≝ set_program_counter s pc in 166 let s ≝ 167 match instr with 165 match instr with 168 166 [ ADD addr1 addr2 ⇒ 169 167 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1) … … 397 395 let new_pc ≝ high_bits @@ low_bits in 398 396 set_program_counter s new_pc 399  JMP _ ⇒ (* DPM: always indirect_dptr *)400 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in401 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in402 let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in403 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in404 set_program_counter s new_pc405  LJMP addr ⇒406 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with407 [ ADDR16 a ⇒ λaddr16: True.408 set_program_counter s a409  _ ⇒ λother: False. ⊥410 ] (subaddressing_modein … addr)411  SJMP addr ⇒412 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with413 [ RELATIVE r ⇒ λrelative: True.414 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in415 set_program_counter s new_pc416  _ ⇒ λother: False. ⊥417 ] (subaddressing_modein … addr)418  AJMP addr ⇒419 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with420 [ ADDR11 a ⇒ λaddr11: True.421 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in422 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in423 let bit ≝ get_index' ? O ? nl in424 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in425 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in426 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in427 set_program_counter s new_pc428  _ ⇒ λother: False. ⊥429 ] (subaddressing_modein … addr)430 397  MOVX addr ⇒ 431 398 (* DPM: only copies  doesn't affect I/O *) … … 471 438 set_arg_1 s addr1 (get_arg_1 s addr2 false) 472 439 ] 473  LCALL addr ⇒ 474 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 475 [ ADDR16 a ⇒ λaddr16: True. 476 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 477 let s ≝ set_8051_sfr s SFR_SP new_sp in 478 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in 479 let s ≝ write_at_stack_pointer s pc_bl in 480 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 481 let s ≝ set_8051_sfr s SFR_SP new_sp in 482 let s ≝ write_at_stack_pointer s pc_bu in 483 set_program_counter s a 484  _ ⇒ λother: False. ⊥ 485 ] (subaddressing_modein … addr) 486  ACALL addr ⇒ 487 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 488 [ ADDR11 a ⇒ λaddr11: True. 489 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 490 let s ≝ set_8051_sfr s SFR_SP new_sp in 491 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in 492 let s ≝ write_at_stack_pointer s pc_bl in 493 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 494 let s ≝ set_8051_sfr s SFR_SP new_sp in 495 let s ≝ write_at_stack_pointer s pc_bu in 496 let 〈thr, eig〉 ≝ split ? 3 8 a in 497 let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in 498 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 499 set_program_counter s new_addr 500  _ ⇒ λother: False. ⊥ 501 ] (subaddressing_modein … addr) 502  Jump j ⇒ 503 match j with 504 [ JC addr ⇒ 505 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 506 [ RELATIVE r ⇒ λrel: True. 440  JC addr ⇒ 441 let r ≝ addr_of addr in 507 442 if get_cy_flag s then 508 443 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in … … 510 445 else 511 446 s 512  _ ⇒ λother: False. ⊥513 ] (subaddressing_modein … addr)514 447  JNC addr ⇒ 515 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 516 [ RELATIVE r ⇒ λrel: True. 448 let r ≝ addr_of addr in 517 449 if ¬(get_cy_flag s) then 518 450 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in … … 520 452 else 521 453 s 522  _ ⇒ λother: False. ⊥523 ] (subaddressing_modein … addr)524 454  JB addr1 addr2 ⇒ 525 match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 526 [ RELATIVE r ⇒ λrel: True. 455 let r ≝ addr_of addr2 in 527 456 if get_arg_1 s addr1 false then 528 457 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in … … 530 459 else 531 460 s 532  _ ⇒ λother: False. ⊥533 ] (subaddressing_modein … addr2)534 461  JNB addr1 addr2 ⇒ 535 match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 536 [ RELATIVE r ⇒ λrel: True. 462 let r ≝ addr_of addr2 in 537 463 if ¬(get_arg_1 s addr1 false) then 538 464 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in … … 540 466 else 541 467 s 542  _ ⇒ λother: False. ⊥543 ] (subaddressing_modein … addr2)544 468  JBC addr1 addr2 ⇒ 545 match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 546 [ RELATIVE r ⇒ λrel: True. 469 let r ≝ addr_of addr2 in 547 470 let s ≝ set_arg_1 s addr1 false in 548 471 if get_arg_1 s addr1 false then … … 551 474 else 552 475 s 553  _ ⇒ λother: False. ⊥554 ] (subaddressing_modein … addr2)555 476  JZ addr ⇒ 556 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 557 [ RELATIVE r ⇒ λrel: True. 477 let r ≝ addr_of addr in 558 478 if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8) then 559 479 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in … … 561 481 else 562 482 s 563  _ ⇒ λother: False. ⊥564 ] (subaddressing_modein … addr)565 483  JNZ addr ⇒ 566 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 567 [ RELATIVE r ⇒ λrel: True. 484 let r ≝ addr_of addr in 568 485 if ¬(eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then 569 486 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in … … 571 488 else 572 489 s 573  _ ⇒ λother: False. ⊥574 ] (subaddressing_modein … addr)575 490  CJNE addr1 addr2 ⇒ 576 match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 577 [ RELATIVE r ⇒ λrelative: True. 491 let r ≝ addr_of addr2 in 578 492 match addr1 with 579 493 [ inl l ⇒ … … 598 512 (set_flags s new_cy (None ?) (get_ov_flag s)) 599 513 ] 600  _ ⇒ λother: False. ⊥601 ] (subaddressing_modein … addr2)602 514  DJNZ addr1 addr2 ⇒ 603 match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 604 [ RELATIVE r ⇒ λrel: True. 605 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in 606 let s ≝ set_arg_8 s addr1 result in 607 if ¬(eq_bv ? result (zero 8)) then 608 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in 609 set_program_counter s new_pc 610 else 611 s 612  _ ⇒ λother: False. ⊥ 613 ] (subaddressing_modein … addr2) 614 ] 515 let r ≝ addr_of addr2 in 516 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in 517 let s ≝ set_arg_8 s addr1 result in 518 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 521 else 522 s 523  NOP ⇒ s 524 ]. 525 try assumption 526 try ( 527 normalize 528 repeat (@ (le_S_S)) 529 @ (le_O_n) 530 ) 531 try ( 532 @ (execute_1_technical … (subaddressing_modein …)) 533 @ I 534 ) 535 try ( 536 normalize 537 @ I 538 ) 539 qed. 540 541 definition execute_1: Status → Status ≝ 542 λs: Status. 543 let 〈instr_pc, ticks〉 ≝ fetch (code_memory s) (program_counter s) in 544 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 545 let s ≝ set_clock s (clock s + ticks) in 546 let s ≝ set_program_counter s pc in 547 let s ≝ 548 match instr with 549 [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]] 550 (λx. 551 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with 552 [ RELATIVE r ⇒ λ_. r 553  _ ⇒ λabsd. ⊥ 554 ] (subaddressing_modein … x)) instr s 555  ACALL addr ⇒ 556 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 557 [ ADDR11 a ⇒ λaddr11: True. 558 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 559 let s ≝ set_8051_sfr s SFR_SP new_sp in 560 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in 561 let s ≝ write_at_stack_pointer s pc_bl in 562 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 563 let s ≝ set_8051_sfr s SFR_SP new_sp in 564 let s ≝ write_at_stack_pointer s pc_bu in 565 let 〈thr, eig〉 ≝ split ? 3 8 a in 566 let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in 567 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 568 set_program_counter s new_addr 569  _ ⇒ λother: False. ⊥ 570 ] (subaddressing_modein … addr) 571  LCALL addr ⇒ 572 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 573 [ ADDR16 a ⇒ λaddr16: True. 574 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 575 let s ≝ set_8051_sfr s SFR_SP new_sp in 576 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in 577 let s ≝ write_at_stack_pointer s pc_bl in 578 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 579 let s ≝ set_8051_sfr s SFR_SP new_sp in 580 let s ≝ write_at_stack_pointer s pc_bu in 581 set_program_counter s a 582  _ ⇒ λother: False. ⊥ 583 ] (subaddressing_modein … addr) 615 584  MOVC addr1 addr2 ⇒ 616 585 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with … … 632 601  _ ⇒ λother: False. ⊥ 633 602 ] (subaddressing_modein … addr2) 634  NOP ⇒ s 635 ] 603  JMP _ ⇒ (* DPM: always indirect_dptr *) 604 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 605 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in 606 let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in 607 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in 608 set_program_counter s new_pc 609  LJMP addr ⇒ 610 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 611 [ ADDR16 a ⇒ λaddr16: True. 612 set_program_counter s a 613  _ ⇒ λother: False. ⊥ 614 ] (subaddressing_modein … addr) 615  SJMP addr ⇒ 616 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 617 [ RELATIVE r ⇒ λrelative: True. 618 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in 619 set_program_counter s new_pc 620  _ ⇒ λother: False. ⊥ 621 ] (subaddressing_modein … addr) 622  AJMP addr ⇒ 623 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 624 [ ADDR11 a ⇒ λaddr11: True. 625 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in 626 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in 627 let bit ≝ get_index' ? O ? nl in 628 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in 629 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 630 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in 631 set_program_counter s new_pc 632  _ ⇒ λother: False. ⊥ 633 ] (subaddressing_modein … addr) 634 ] 636 635 in 637 636 s. … … 652 651 qed. 653 652 653 axiom fetch_pseudo_instruction: 654 ∀p: list labelled_instruction. 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: pseudo_assembly_program → Status → Status ≝ 662 λp. 663 λs. 664 let 〈instr_pc, ticks〉 ≝ fetch_pseudo_instruction (\snd p) (program_counter s) in 665 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 666 let s ≝ set_clock s (clock s + ticks) in 667 let s ≝ set_program_counter s pc in 668 let s ≝ 669 match instr with 670 [ Instruction instr ⇒ execute_1_preinstruction ? address_of_labels instr s 671  Comment cmt ⇒ s 672  Cost cst ⇒ s 673  Jmp jmp ⇒ set_program_counter s (address_of_word_labels jmp) 674  Call call ⇒ 675 let a ≝ address_of_word_labels call in 676 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 677 let s ≝ set_8051_sfr s SFR_SP new_sp in 678 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in 679 let s ≝ write_at_stack_pointer s pc_bl in 680 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in 681 let s ≝ set_8051_sfr s SFR_SP new_sp in 682 let s ≝ write_at_stack_pointer s pc_bu in 683 set_program_counter s a 684  Mov dptr ident ⇒ set_arg_16 s (get_arg_16 s (DATA16 (address_of_word_labels ident))) dptr 685 ] 686 in 687 s. 688 normalize 689 @ I 690 qed. 691 654 692 let rec execute (n: nat) (s: Status) on n: Status ≝ 655 693 match n with … … 657 695  S o ⇒ execute o (execute_1 s) 658 696 ]. 697 698 let rec execute_pseudo_instruction (n: nat) (p: pseudo_assembly_program) (s: Status) on n: Status ≝ 699 match n with 700 [ O ⇒ s 701  S o ⇒ execute_pseudo_instruction o p (execute_1_pseudo_instruction p s) 702 ].
Note: See TracChangeset
for help on using the changeset viewer.