- Timestamp:
- Jun 10, 2011, 4:20:47 PM (10 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r935 r936 834 834 P [[true;true;false]] → P [[true;true;true]] → ∀v. P v. 835 835 836 definition ticks_of_instruction ≝ 837 λi. 838 let trivial_code_memory ≝ assembly1 i in 839 let trivial_status ≝ load_code_memory trivial_code_memory in 840 \snd (fetch trivial_status (zero ?)). 841 836 842 axiom fetch_assembly: 837 843 ∀pc,i,code_memory,assembled. … … 842 848 let 〈instr_pc, ticks〉 ≝ fetched in 843 849 let 〈instr,pc'〉 ≝ instr_pc in 844 (eq_instruction instr i ∧ eq _bv … pc' (bitvector_of_nat … (pc + len))) = true.850 (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true. 845 851 (* #pc #i #code_memory #assembled cases i [8: *] 846 852 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]] … … 876 882 let 〈instr_pc, ticks〉 ≝ fetched in 877 883 let 〈instr,pc'〉 ≝ instr_pc in 878 eq_instruction instr i = true ∧ fetch_many code_memory final_pc pc' tl]. 884 eq_instruction instr i = true ∧ 885 ticks = (ticks_of_instruction i) ∧ 886 fetch_many code_memory final_pc pc' tl]. 879 887 880 888 lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b. … … 887 895 888 896 axiom eq_bv_to_eq: ∀n.∀v1,v2: BitVector n. eq_bv … v1 v2 = true → v1=v2. 897 898 axiom eq_instruction_to_eq: ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2. 889 899 890 900 lemma fetch_assembly_pseudo: … … 906 916 generalize in match (fetch_assembly pc i code_memory … (refl …) H1) 907 917 cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %) 908 cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1 #K2 % // 909 >(eq_bv_to_eq … K2) @IH @H2 ] 918 cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1 919 cases (conjunction_true … K1) -K1; #K1 #K2 #K3 % try % // 920 [ @eqb_true_to_eq <(eq_instruction_to_eq … K1) // | >(eq_bv_to_eq … K3) @IH @H2 ] 910 921 qed. 911 922 … … 1602 1613 qed. 1603 1614 1604 definition ticks_of : pseudo_assembly_program → Word→ nat × nat ≝1615 definition ticks_of0: pseudo_assembly_program → Word → ? → nat × nat ≝ 1605 1616 λprogram: pseudo_assembly_program. 1606 1617 λppc: Word. 1607 let 〈preamble, pseudo〉 ≝ program in 1608 let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in 1618 λfetched. 1609 1619 match fetched with 1610 1620 [ Instruction instr ⇒ … … 1664 1674 | long_jump ⇒ 〈4, 4〉 1665 1675 ] 1666 | ADD arg1 arg2 ⇒ 1667 let trivial_code_memory ≝ assembly1 (ADD ? arg1 arg2) in 1668 let trivial_status ≝ load_code_memory trivial_code_memory in 1669 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1670 〈0, ticks〉 1676 | ADD arg1 arg2 ⇒ 1677 let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in 1678 〈ticks, ticks〉 1671 1679 | ADDC arg1 arg2 ⇒ 1672 let trivial_code_memory ≝ assembly1 (ADDC ? arg1 arg2) in 1673 let trivial_status ≝ load_code_memory trivial_code_memory in 1674 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1675 〈0, ticks〉 1680 let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in 1681 〈ticks, ticks〉 1676 1682 | SUBB arg1 arg2 ⇒ 1677 let trivial_code_memory ≝ assembly1 (SUBB ? arg1 arg2) in 1678 let trivial_status ≝ load_code_memory trivial_code_memory in 1679 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1680 〈0, ticks〉 1683 let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in 1684 〈ticks, ticks〉 1681 1685 | INC arg ⇒ 1682 let trivial_code_memory ≝ assembly1 (INC ? arg) in 1683 let trivial_status ≝ load_code_memory trivial_code_memory in 1684 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1685 〈0, ticks〉 1686 let ticks ≝ ticks_of_instruction (INC ? arg) in 1687 〈ticks, ticks〉 1686 1688 | DEC arg ⇒ 1687 let trivial_code_memory ≝ assembly1 (DEC ? arg) in 1688 let trivial_status ≝ load_code_memory trivial_code_memory in 1689 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1690 〈0, ticks〉 1689 let ticks ≝ ticks_of_instruction (DEC ? arg) in 1690 〈ticks, ticks〉 1691 1691 | MUL arg1 arg2 ⇒ 1692 let trivial_code_memory ≝ assembly1 (MUL ? arg1 arg2) in 1693 let trivial_status ≝ load_code_memory trivial_code_memory in 1694 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1695 〈0, ticks〉 1692 let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in 1693 〈ticks, ticks〉 1696 1694 | DIV arg1 arg2 ⇒ 1697 let trivial_code_memory ≝ assembly1 (DIV ? arg1 arg2) in 1698 let trivial_status ≝ load_code_memory trivial_code_memory in 1699 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1700 〈0, ticks〉 1695 let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in 1696 〈ticks, ticks〉 1701 1697 | DA arg ⇒ 1702 let trivial_code_memory ≝ assembly1 (DA ? arg) in 1703 let trivial_status ≝ load_code_memory trivial_code_memory in 1704 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1705 〈0, ticks〉 1698 let ticks ≝ ticks_of_instruction (DA ? arg) in 1699 〈ticks, ticks〉 1706 1700 | ANL arg ⇒ 1707 let trivial_code_memory ≝ assembly1 (ANL ? arg) in 1708 let trivial_status ≝ load_code_memory trivial_code_memory in 1709 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1710 〈0, ticks〉 1701 let ticks ≝ ticks_of_instruction (ANL ? arg) in 1702 〈ticks, ticks〉 1711 1703 | ORL arg ⇒ 1712 let trivial_code_memory ≝ assembly1 (ORL ? arg) in 1713 let trivial_status ≝ load_code_memory trivial_code_memory in 1714 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1715 〈0, ticks〉 1704 let ticks ≝ ticks_of_instruction (ORL ? arg) in 1705 〈ticks, ticks〉 1716 1706 | XRL arg ⇒ 1717 let trivial_code_memory ≝ assembly1 (XRL ? arg) in 1718 let trivial_status ≝ load_code_memory trivial_code_memory in 1719 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1720 〈0, ticks〉 1707 let ticks ≝ ticks_of_instruction (XRL ? arg) in 1708 〈ticks, ticks〉 1721 1709 | CLR arg ⇒ 1722 let trivial_code_memory ≝ assembly1 (CLR ? arg) in 1723 let trivial_status ≝ load_code_memory trivial_code_memory in 1724 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1725 〈0, ticks〉 1710 let ticks ≝ ticks_of_instruction (CLR ? arg) in 1711 〈ticks, ticks〉 1726 1712 | CPL arg ⇒ 1727 let trivial_code_memory ≝ assembly1 (CPL ? arg) in 1728 let trivial_status ≝ load_code_memory trivial_code_memory in 1729 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1730 〈0, ticks〉 1713 let ticks ≝ ticks_of_instruction (CPL ? arg) in 1714 〈ticks, ticks〉 1731 1715 | RL arg ⇒ 1732 let trivial_code_memory ≝ assembly1 (RL ? arg) in 1733 let trivial_status ≝ load_code_memory trivial_code_memory in 1734 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1735 〈0, ticks〉 1716 let ticks ≝ ticks_of_instruction (RL ? arg) in 1717 〈ticks, ticks〉 1736 1718 | RLC arg ⇒ 1737 let trivial_code_memory ≝ assembly1 (RLC ? arg) in 1738 let trivial_status ≝ load_code_memory trivial_code_memory in 1739 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1740 〈0, ticks〉 1719 let ticks ≝ ticks_of_instruction (RLC ? arg) in 1720 〈ticks, ticks〉 1741 1721 | RR arg ⇒ 1742 let trivial_code_memory ≝ assembly1 (RR ? arg) in 1743 let trivial_status ≝ load_code_memory trivial_code_memory in 1744 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1745 〈0, ticks〉 1722 let ticks ≝ ticks_of_instruction (RR ? arg) in 1723 〈ticks, ticks〉 1746 1724 | RRC arg ⇒ 1747 let trivial_code_memory ≝ assembly1 (RRC ? arg) in 1748 let trivial_status ≝ load_code_memory trivial_code_memory in 1749 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1750 〈0, ticks〉 1725 let ticks ≝ ticks_of_instruction (RRC ? arg) in 1726 〈ticks, ticks〉 1751 1727 | SWAP arg ⇒ 1752 let trivial_code_memory ≝ assembly1 (SWAP ? arg) in 1753 let trivial_status ≝ load_code_memory trivial_code_memory in 1754 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1755 〈0, ticks〉 1728 let ticks ≝ ticks_of_instruction (SWAP ? arg) in 1729 〈ticks, ticks〉 1756 1730 | MOV arg ⇒ 1757 let trivial_code_memory ≝ assembly1 (MOV ? arg) in 1758 let trivial_status ≝ load_code_memory trivial_code_memory in 1759 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1760 〈0, ticks〉 1731 let ticks ≝ ticks_of_instruction (MOV ? arg) in 1732 〈ticks, ticks〉 1761 1733 | MOVX arg ⇒ 1762 let trivial_code_memory ≝ assembly1 (MOVX ? arg) in 1763 let trivial_status ≝ load_code_memory trivial_code_memory in 1764 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1765 〈0, ticks〉 1734 let ticks ≝ ticks_of_instruction (MOVX ? arg) in 1735 〈ticks, ticks〉 1766 1736 | SETB arg ⇒ 1767 let trivial_code_memory ≝ assembly1 (SETB ? arg) in 1768 let trivial_status ≝ load_code_memory trivial_code_memory in 1769 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1770 〈0, ticks〉 1737 let ticks ≝ ticks_of_instruction (SETB ? arg) in 1738 〈ticks, ticks〉 1771 1739 | PUSH arg ⇒ 1772 let trivial_code_memory ≝ assembly1 (PUSH ? arg) in 1773 let trivial_status ≝ load_code_memory trivial_code_memory in 1774 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1775 〈0, ticks〉 1740 let ticks ≝ ticks_of_instruction (PUSH ? arg) in 1741 〈ticks, ticks〉 1776 1742 | POP arg ⇒ 1777 let trivial_code_memory ≝ assembly1 (POP ? arg) in 1778 let trivial_status ≝ load_code_memory trivial_code_memory in 1779 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1780 〈0, ticks〉 1743 let ticks ≝ ticks_of_instruction (POP ? arg) in 1744 〈ticks, ticks〉 1781 1745 | XCH arg1 arg2 ⇒ 1782 let trivial_code_memory ≝ assembly1 (XCH ? arg1 arg2) in 1783 let trivial_status ≝ load_code_memory trivial_code_memory in 1784 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1785 〈0, ticks〉 1746 let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in 1747 〈ticks, ticks〉 1786 1748 | XCHD arg1 arg2 ⇒ 1787 let trivial_code_memory ≝ assembly1 (XCHD ? arg1 arg2) in 1788 let trivial_status ≝ load_code_memory trivial_code_memory in 1789 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1790 〈0, ticks〉 1749 let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in 1750 〈ticks, ticks〉 1791 1751 | RET ⇒ 1792 let trivial_code_memory ≝ assembly1 (RET ?) in 1793 let trivial_status ≝ load_code_memory trivial_code_memory in 1794 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1795 〈0, ticks〉 1752 let ticks ≝ ticks_of_instruction (RET ?) in 1753 〈ticks, ticks〉 1796 1754 | RETI ⇒ 1797 let trivial_code_memory ≝ assembly1 (RETI ?) in 1798 let trivial_status ≝ load_code_memory trivial_code_memory in 1799 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1800 〈0, ticks〉 1755 let ticks ≝ ticks_of_instruction (RETI ?) in 1756 〈ticks, ticks〉 1801 1757 | NOP ⇒ 1802 let trivial_code_memory ≝ assembly1 (NOP ?) in 1803 let trivial_status ≝ load_code_memory trivial_code_memory in 1804 let ticks ≝ \snd (fetch trivial_status (zero ?)) in 1805 〈0, ticks〉 1758 let ticks ≝ ticks_of_instruction (NOP ?) in 1759 〈ticks, ticks〉 1806 1760 ] 1807 1761 | Comment comment ⇒ 〈0, 0〉 … … 1814 1768 qed. 1815 1769 1816 axiom eq_instruction_to_eq: ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2. 1770 definition ticks_of: pseudo_assembly_program → Word → nat × nat ≝ 1771 λprogram: pseudo_assembly_program. 1772 λppc: Word. 1773 let 〈preamble, pseudo〉 ≝ program in 1774 let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in 1775 ticks_of0 program ppc fetched. 1817 1776 1818 1777 lemma get_register_set_program_counter: … … 1844 1803 qed. 1845 1804 1846 lemma set_arg_8_set_program_counter:1847 ∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) →1848 ∀T,s.∀pc:Word.∀b:l.1849 set_arg_8 T (set_program_counter … s pc) b = set_arg_8 … s b.1850 [2,3: cases b; *; normalize //]1851 #n #l #prf #T #s #pc #b * *;1852 qed.1853 1854 1805 lemma get_arg_8_set_code_memory: 1855 1806 ∀T1,T2,s,code_mem,b,arg. … … 1877 1828 #T1 #s #f1 #f2 #f3 % 1878 1829 qed. 1879 1880 axiom ignore_clock: ∀T,ps,x.set_clock T ps x = ps.1881 1830 1882 1831 lemma eq_rect_Type1_r: … … 1892 1841 1893 1842 lemma main_thm: 1894 ∀ticks_of.1895 1843 ∀ps,s,s''. 1896 1844 status_of_pseudo_status ps = Some … s → 1897 status_of_pseudo_status (execute_1_pseudo_instruction ticks_ofps) = Some … s'' →1845 status_of_pseudo_status (execute_1_pseudo_instruction (ticks_of (code_memory … ps)) ps) = Some … s'' → 1898 1846 ∃n. execute n s = s''. 1899 # ticks_of #ps #s #s''1847 #ps #s #s'' 1900 1848 generalize in match (fetch_assembly_pseudo2 (code_memory … ps)) 1901 1849 whd in ⊢ (? → ??%? → ??%? → ?) … … 1917 1865 (∃n. 1918 1866 execute n (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?) 1919 = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_ofps) (load_code_memory assembled)) ?)1867 = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled)) ?) 1920 1868 whd in match (\snd 〈preamble,instr_list〉) in H; 1921 1869 whd in match (\fst 〈preamble,instr_list〉) in H; 1922 1870 whd in match (\snd 〈final_pc,assembled〉) in H; 1923 1871 -s s'' labels costs final_ppc final_pc; 1924 letin ps' ≝ (execute_1_pseudo_instruction ticks_ofps)1872 letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉) ps) 1925 1873 (* NICE STATEMENT HERE *) 1926 1874 generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; -ps'; #ps' 1927 1875 #K <K generalize in match K; -K; 1928 1876 (* STATEMENT WITH EQUALITY HERE *) 1929 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) >EQ0 normalize nodelta; 1877 whd in ⊢ (???(?%?) → ?) 1878 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) -H; >EQ0 normalize nodelta; 1930 1879 cases (fetch_pseudo_instruction instr_list (program_counter … ps)) 1931 1880 #pi #newppc normalize nodelta; * #instructions *; … … 1933 1882 [2,3: (* Comment, Cost *) #ARG #H1 #H2 #EQ %[1,3:@0] 1934 1883 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 1935 #H2 >(eq_bv_to_eq … H2) > ignore_clock in EQ; #EQ >EQ %1884 #H2 >(eq_bv_to_eq … H2) >EQ % 1936 1885 |4: (* Jmp *) 1937 1886 |5: (* Call *) … … 1942 1891 change in ⊢ (? → ??%?) with (execute_1_0 ??) 1943 1892 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 1944 * #H2a whd in ⊢ (% → ?) #H2b 1945 >ignore_clock in EQ; 1946 >(eq_instruction_to_eq … H2a) 1947 whd in ⊢ (???% → ??%?); 1948 >ignore_clock 1893 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 1894 >H2b >(eq_instruction_to_eq … H2a) 1895 generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); 1949 1896 @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; 1950 1897 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2 … … 1952 1899 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)] 1953 1900 #result #flags 1954 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2 b) -newppc';%1901 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) % 1955 1902 | (* INC *) #arg1 #H1 #H2 #EQ %[@1] 1956 1903 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 1957 1904 change in ⊢ (? → ??%?) with (execute_1_0 ??) 1958 1905 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 1959 * #H2a whd in ⊢ (% → ?) #H2b 1960 >ignore_clock in EQ; 1961 >(eq_instruction_to_eq … H2a) 1962 whd in ⊢ (???% → ??%?); 1963 >ignore_clock 1906 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 1907 >H2b >(eq_instruction_to_eq … H2a) 1908 generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); 1964 1909 @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG] 1965 1910 [1,2,3,4: cases (half_add ???) #carry #result 1966 1911 | cases (half_add ???) #carry #bl normalize nodelta; 1967 1912 cases (full_add ????) #carry' #bu normalize nodelta ] 1968 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2 b) -newppc';1913 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) -newppc'; 1969 1914 [5: % 1970 |1: >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags % 1971 1972 XXX 1973 % 1974 1915 |1: -
src/ASM/Interpret.ma
r928 r936 159 159 include alias "ASM/BitVectorTrie.ma". 160 160 161 definition execute_1_preinstruction: ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝ 161 definition execute_1_preinstruction: 162 ∀ticks: nat × nat. 163 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → PreStatus M → PreStatus M ≝ 164 λticks. 162 165 λA, M: Type[0]. 163 166 λaddr_of: A → (PreStatus M) → Word. 164 167 λinstr: preinstruction A. 165 168 λs: PreStatus M. 169 let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in 170 let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in 166 171 match instr with 167 172 [ ADD addr1 addr2 ⇒ 173 let s ≝ add_ticks1 s in 168 174 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1) 169 175 (get_arg_8 ? s false addr2) false in … … 174 180 set_flags ? s cy_flag (Some Bit ac_flag) ov_flag 175 181 | ADDC addr1 addr2 ⇒ 182 let s ≝ add_ticks1 s in 176 183 let old_cy_flag ≝ get_cy_flag ? s in 177 184 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ? s false addr1) … … 183 190 set_flags ? s cy_flag (Some Bit ac_flag) ov_flag 184 191 | SUBB addr1 addr2 ⇒ 192 let s ≝ add_ticks1 s in 185 193 let old_cy_flag ≝ get_cy_flag ? s in 186 194 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ? s false addr1) … … 192 200 set_flags ? s cy_flag (Some Bit ac_flag) ov_flag 193 201 | ANL addr ⇒ 202 let s ≝ add_ticks1 s in 194 203 match addr with 195 204 [ inl l ⇒ … … 210 219 ] 211 220 | ORL addr ⇒ 221 let s ≝ add_ticks1 s in 212 222 match addr with 213 223 [ inl l ⇒ … … 228 238 ] 229 239 | XRL addr ⇒ 240 let s ≝ add_ticks1 s in 230 241 match addr with 231 242 [ inl l' ⇒ … … 239 250 ] 240 251 | INC addr ⇒ 252 let s ≝ add_ticks1 s in 241 253 match addr return λx. bool_to_Prop (is_in … [[ acc_a; 242 254 registr; … … 264 276 ] (subaddressing_modein … addr) 265 277 | DEC addr ⇒ 278 let s ≝ add_ticks1 s in 266 279 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in 267 280 set_arg_8 ? s addr result 268 281 | MUL addr1 addr2 ⇒ 282 let s ≝ add_ticks1 s in 269 283 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in 270 284 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in … … 276 290 set_8051_sfr ? s SFR_ACC_B high 277 291 | DIV addr1 addr2 ⇒ 292 let s ≝ add_ticks1 s in 278 293 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_A) in 279 294 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ? s SFR_ACC_B) in … … 288 303 ] 289 304 | DA addr ⇒ 305 let s ≝ add_ticks1 s in 290 306 let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in 291 307 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then … … 303 319 s 304 320 | CLR addr ⇒ 321 let s ≝ add_ticks1 s in 305 322 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with 306 323 [ ACC_A ⇒ λacc_a: True. set_arg_8 ? s ACC_A (zero 8) … … 310 327 ] (subaddressing_modein … addr) 311 328 | CPL addr ⇒ 329 let s ≝ add_ticks1 s in 312 330 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with 313 331 [ ACC_A ⇒ λacc_a: True. … … 325 343 | _ ⇒ λother: False. ? 326 344 ] (subaddressing_modein … addr) 327 | SETB b ⇒ set_arg_1 ? s b false 345 | SETB b ⇒ 346 let s ≝ add_ticks1 s in 347 set_arg_1 ? s b false 328 348 | RL _ ⇒ (* DPM: always ACC_A *) 349 let s ≝ add_ticks1 s in 329 350 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 330 351 let new_acc ≝ rotate_left … 1 old_acc in 331 352 set_8051_sfr ? s SFR_ACC_A new_acc 332 353 | RR _ ⇒ (* DPM: always ACC_A *) 354 let s ≝ add_ticks1 s in 333 355 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 334 356 let new_acc ≝ rotate_right … 1 old_acc in 335 357 set_8051_sfr ? s SFR_ACC_A new_acc 336 358 | RLC _ ⇒ (* DPM: always ACC_A *) 359 let s ≝ add_ticks1 s in 337 360 let old_cy_flag ≝ get_cy_flag ? s in 338 361 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in … … 342 365 set_8051_sfr ? s SFR_ACC_A new_acc 343 366 | RRC _ ⇒ (* DPM: always ACC_A *) 367 let s ≝ add_ticks1 s in 344 368 let old_cy_flag ≝ get_cy_flag ? s in 345 369 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in … … 349 373 set_8051_sfr ? s SFR_ACC_A new_acc 350 374 | SWAP _ ⇒ (* DPM: always ACC_A *) 375 let s ≝ add_ticks1 s in 351 376 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 352 377 let 〈nu,nl〉 ≝ split ? 4 4 old_acc in … … 354 379 set_8051_sfr ? s SFR_ACC_A new_acc 355 380 | PUSH addr ⇒ 381 let s ≝ add_ticks1 s in 356 382 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with 357 383 [ DIRECT d ⇒ λdirect: True. … … 362 388 ] (subaddressing_modein … addr) 363 389 | POP addr ⇒ 390 let s ≝ add_ticks1 s in 364 391 let contents ≝ read_at_stack_pointer ? s in 365 392 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in … … 367 394 set_arg_8 ? s addr contents 368 395 | XCH addr1 addr2 ⇒ 396 let s ≝ add_ticks1 s in 369 397 let old_addr ≝ get_arg_8 ? s false addr2 in 370 398 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in … … 372 400 set_arg_8 ? s addr2 old_acc 373 401 | XCHD addr1 addr2 ⇒ 402 let s ≝ add_ticks1 s in 374 403 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in 375 404 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ? s false addr2) in … … 379 408 set_arg_8 ? s addr2 new_arg 380 409 | RET ⇒ 410 let s ≝ add_ticks1 s in 381 411 let high_bits ≝ read_at_stack_pointer ? s in 382 412 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in … … 388 418 set_program_counter ? s new_pc 389 419 | RETI ⇒ 420 let s ≝ add_ticks1 s in 390 421 let high_bits ≝ read_at_stack_pointer ? s in 391 422 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) false in … … 397 428 set_program_counter ? s new_pc 398 429 | MOVX addr ⇒ 430 let s ≝ add_ticks1 s in 399 431 (* DPM: only copies --- doesn't affect I/O *) 400 432 match addr with … … 407 439 ] 408 440 | MOV addr ⇒ 441 let s ≝ add_ticks1 s in 409 442 match addr with 410 443 [ inl l ⇒ … … 441 474 | JC addr ⇒ 442 475 if get_cy_flag ? s then 443 set_program_counter ? s (addr_of addr s) 476 let s ≝ add_ticks1 s in 477 set_program_counter ? s (addr_of addr s) 444 478 else 479 let s ≝ add_ticks2 s in 445 480 s 446 481 | JNC addr ⇒ 447 482 if ¬(get_cy_flag ? s) then 448 set_program_counter ? s (addr_of addr s) 483 let s ≝ add_ticks1 s in 484 set_program_counter ? s (addr_of addr s) 449 485 else 486 let s ≝ add_ticks2 s in 450 487 s 451 488 | JB addr1 addr2 ⇒ 452 489 if get_arg_1 ? s addr1 false then 453 set_program_counter ? s (addr_of addr2 s) 490 let s ≝ add_ticks1 s in 491 set_program_counter ? s (addr_of addr2 s) 454 492 else 493 let s ≝ add_ticks2 s in 455 494 s 456 495 | JNB addr1 addr2 ⇒ 457 496 if ¬(get_arg_1 ? s addr1 false) then 458 set_program_counter ? s (addr_of addr2 s) 497 let s ≝ add_ticks1 s in 498 set_program_counter ? s (addr_of addr2 s) 459 499 else 500 let s ≝ add_ticks2 s in 460 501 s 461 502 | JBC addr1 addr2 ⇒ 462 503 let s ≝ set_arg_1 ? s addr1 false in 463 504 if get_arg_1 ? s addr1 false then 464 set_program_counter ? s (addr_of addr2 s) 505 let s ≝ add_ticks1 s in 506 set_program_counter ? s (addr_of addr2 s) 465 507 else 508 let s ≝ add_ticks2 s in 466 509 s 467 510 | JZ addr ⇒ 468 511 if eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8) then 469 set_program_counter ? s (addr_of addr s) 512 let s ≝ add_ticks1 s in 513 set_program_counter ? s (addr_of addr s) 470 514 else 515 let s ≝ add_ticks2 s in 471 516 s 472 517 | JNZ addr ⇒ 473 518 if ¬(eq_bv ? (get_8051_sfr ? s SFR_ACC_A) (zero 8)) then 474 set_program_counter ? s (addr_of addr s) 519 let s ≝ add_ticks1 s in 520 set_program_counter ? s (addr_of addr s) 475 521 else 522 let s ≝ add_ticks2 s in 476 523 s 477 524 | CJNE addr1 addr2 ⇒ … … 482 529 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in 483 530 if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then 531 let s ≝ add_ticks1 s in 484 532 let s ≝ set_program_counter ? s (addr_of addr2 s) in 485 533 set_flags ? s new_cy (None ?) (get_ov_flag ? s) 486 534 else 535 let s ≝ add_ticks2 s in 487 536 (set_flags ? s new_cy (None ?) (get_ov_flag ? s)) 488 537 | inr r' ⇒ … … 491 540 (nat_of_bitvector ? (get_arg_8 ? s false addr2')) in 492 541 if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ? s false addr2')) then 542 let s ≝ add_ticks1 s in 493 543 let s ≝ set_program_counter ? s (addr_of addr2 s) in 494 544 set_flags ? s new_cy (None ?) (get_ov_flag ? s) 495 545 else 546 let s ≝ add_ticks2 s in 496 547 (set_flags ? s new_cy (None ?) (get_ov_flag ? s)) 497 548 ] … … 500 551 let s ≝ set_arg_8 ? s addr1 result in 501 552 if ¬(eq_bv ? result (zero 8)) then 502 set_program_counter ? s (addr_of addr2 s) 553 let s ≝ add_ticks1 s in 554 set_program_counter ? s (addr_of addr2 s) 503 555 else 556 let s ≝ add_ticks2 s in 504 557 s 505 | NOP ⇒ s 558 | NOP ⇒ 559 let s ≝ add_ticks2 s in 560 s 506 561 ]. 507 562 try assumption … … 517 572 let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in 518 573 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 519 let s ≝ set_clock ? s (clock ? s + ticks) in520 574 let s ≝ set_program_counter ? s pc in 521 575 let s ≝ 522 576 match instr with 523 [ RealInstruction instr ⇒ execute_1_preinstruction [[ relative ]] ?577 [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ? 524 578 (λx. λs. 525 579 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with … … 528 582 ] (subaddressing_modein … x)) instr s 529 583 | ACALL addr ⇒ 584 let s ≝ set_clock ? s (ticks + clock ? s) in 530 585 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 531 586 [ ADDR11 a ⇒ λaddr11: True. … … 544 599 ] (subaddressing_modein … addr) 545 600 | LCALL addr ⇒ 601 let s ≝ set_clock ? s (ticks + clock ? s) in 546 602 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 547 603 [ ADDR16 a ⇒ λaddr16: True. … … 557 613 ] (subaddressing_modein … addr) 558 614 | MOVC addr1 addr2 ⇒ 615 let s ≝ set_clock ? s (ticks + clock ? s) in 559 616 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with 560 617 [ ACC_DPTR ⇒ λacc_dptr: True. … … 576 633 ] (subaddressing_modein … addr2) 577 634 | JMP _ ⇒ (* DPM: always indirect_dptr *) 635 let s ≝ set_clock ? s (ticks + clock ? s) in 578 636 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 579 637 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in … … 582 640 set_program_counter ? s new_pc 583 641 | LJMP addr ⇒ 642 let s ≝ set_clock ? s (ticks + clock ? s) in 584 643 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 585 644 [ ADDR16 a ⇒ λaddr16: True. … … 588 647 ] (subaddressing_modein … addr) 589 648 | SJMP addr ⇒ 649 let s ≝ set_clock ? s (ticks + clock ? s) in 590 650 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 591 651 [ RELATIVE r ⇒ λrelative: True. … … 595 655 ] (subaddressing_modein … addr) 596 656 | AJMP addr ⇒ 657 let s ≝ set_clock ? s (ticks + clock ? s) in 597 658 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 598 659 [ ADDR11 a ⇒ λaddr11: True. … … 666 727 address_of_word_labels_code_mem (\snd (code_memory ? ps)) id. 667 728 668 definition execute_1_pseudo_instruction: (Word → nat ) → PseudoStatus → PseudoStatus ≝729 definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝ 669 730 λticks_of. 670 731 λs. 671 732 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in 672 733 let ticks ≝ ticks_of (program_counter ? s) in 673 let s ≝ set_clock ? s (clock ? s + ticks) in674 734 let s ≝ set_program_counter ? s pc in 675 735 let s ≝ 676 736 match instr with 677 [ Instruction instr ⇒ execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s 678 | Comment cmt ⇒ s 737 [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s 738 | Comment cmt ⇒ 739 let s ≝ set_clock ? s (\fst ticks + clock ? s) in 740 s 679 741 | Cost cst ⇒ s 680 | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp) 742 | Jmp jmp ⇒ 743 let s ≝ set_clock ? s (\fst ticks + clock ? s) in 744 set_program_counter ? s (address_of_word_labels s jmp) 681 745 | Call call ⇒ 746 let s ≝ set_clock ? s (\fst ticks + clock ? s) in 682 747 let a ≝ address_of_word_labels s call in 683 748 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in … … 690 755 set_program_counter ? s a 691 756 | Mov dptr ident ⇒ 757 let s ≝ set_clock ? s (\fst ticks + clock ? s) in 692 758 let preamble ≝ \fst (code_memory ? s) in 693 759 let data_labels ≝ construct_datalabels preamble in … … 706 772 ]. 707 773 708 let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat ) (s: PseudoStatus) on n: PseudoStatus ≝774 let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (s: PseudoStatus) on n: PseudoStatus ≝ 709 775 match n with 710 776 [ O ⇒ s
Note: See TracChangeset
for help on using the changeset viewer.