Changeset 2247 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jul 24, 2012, 6:00:48 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r2209 r2247 464 464 465 465 definition addressing_mode_ok ≝ 466 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm. 467 λaddr:addressing_mode. 468 match addr with 466 λT. 467 λM: internal_pseudo_address_map. 468 λcm. 469 λs: PreStatus T cm. 470 λaddr: addressing_mode. 471 match addr with 469 472 [ DIRECT d ⇒ 470 473 if eq_bv … d (bitvector_of_nat … 224) then … … 481 484 let address ≝ bit_address_of_register … s r in 482 485 ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) 483 | ACC_A ⇒ match \snd M with [ data ⇒ true | _ ⇒ false ] 486 | ACC_A ⇒ 487 match \snd M with 488 [ data ⇒ true 489 | _ ⇒ false 490 ] 484 491 | ACC_B ⇒ true 485 492 | DPTR ⇒ true … … 491 498 | INDIRECT_DPTR ⇒ true 492 499 | CARRY ⇒ true 493 | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *) 494 | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *) 500 | BIT_ADDR b ⇒ 501 let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in 502 if head' bool 0 bit_one then 503 eq_accumulator_address_map_entry (\snd M) data 504 else 505 let address ≝ nat_of_bitvector 7 seven_bits in 506 let address' ≝ bitvector_of_nat 7 ((address÷8)+32) in 507 ¬assoc_list_exists ?? (false:::address') (eq_bv 8) (\fst M) 508 | N_BIT_ADDR b ⇒ ¬true (* TO BE COMPLETED *) 495 509 | RELATIVE _ ⇒ true 496 510 | ADDR11 _ ⇒ true … … 650 664 | RET ⇒ 651 665 let 〈callM, accM〉 ≝ M in 652 let sp_plus_1 ≝ assoc_list_exists ?? ( add8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in653 let sp_plus_2 ≝ assoc_list_exists ?? ( add8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in666 let sp_plus_1 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in 667 let sp_plus_2 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in 654 668 if sp_plus_1 ∧ sp_plus_2 then 655 669 Some … M … … 658 672 | RETI ⇒ 659 673 let 〈callM, accM〉 ≝ M in 660 let sp_plus_1 ≝ assoc_list_exists ?? ( add8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in661 let sp_plus_2 ≝ assoc_list_exists ?? ( add8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in674 let sp_plus_1 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in 675 let sp_plus_2 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in 662 676 if sp_plus_1 ∧ sp_plus_2 then 663 677 Some … M … … 745 759 None ? 746 760 ] 747 | MOV addr1 ⇒ Some … M 761 | MOV addr1 ⇒ 762 match addr1 with 763 [ inl l ⇒ 764 match l with 765 [ inl l' ⇒ 766 match l' with 767 [ inl l'' ⇒ 768 match l'' with 769 [ inl l''' ⇒ 770 match l''' with 771 [ inl l'''' ⇒ 772 let 〈acc_a, others〉 ≝ l'''' in 773 if addressing_mode_ok T M … s acc_a ∧ addressing_mode_ok T M … s others then 774 Some ? M 775 else 776 None ? 777 | inr r ⇒ 778 let 〈others, others'〉 ≝ r in 779 if addressing_mode_ok T M … s others ∧ addressing_mode_ok T M … s others' then 780 Some ? M 781 else 782 None ? 783 ] 784 | inr r ⇒ 785 let 〈direct, others〉 ≝ r in 786 if addressing_mode_ok T M … s direct ∧ addressing_mode_ok T M … s others then 787 Some ? M 788 else 789 None ? 790 ] 791 | inr r ⇒ 792 let 〈dptr, data_16〉 ≝ r in 793 if addressing_mode_ok T M … s dptr ∧ addressing_mode_ok T M … s data_16 then 794 Some ? M 795 else 796 None ? 797 ] 798 | inr r ⇒ 799 let 〈carry, bit_addr〉 ≝ r in 800 if addressing_mode_ok T M … s carry ∧ addressing_mode_ok T M … s bit_addr then 801 Some ? M 802 else 803 None ? 804 ] 805 | inr r ⇒ 806 let 〈bit_addr, carry〉 ≝ r in 807 if addressing_mode_ok T M … s bit_addr ∧ addressing_mode_ok T M … s carry then 808 Some ? M 809 else 810 None ? 811 ] 748 812 ] 749 813 ].
Note: See TracChangeset
for help on using the changeset viewer.