- Timestamp:
- Jul 25, 2012, 4:37:34 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplit.ma
r2258 r2259 414 414 ] 415 415 qed. 416 417 (* 418 lemma write_at_stack_pointer_status_of_pseudo_status: 419 ∀M, M'. 420 ∀cm. 421 ∀sigma. 422 ∀policy. 423 ∀s, s'. 424 ∀new_b, new_b'. 425 M = M' → 426 map_internal_ram_address_using_pseudo_address_map M sigma new_b = new_b' → 427 status_of_pseudo_status M cm s sigma policy = s' → 428 write_at_stack_pointer ?? s' new_b' = 429 status_of_pseudo_status M cm (write_at_stack_pointer ? cm s new_b) sigma policy. 430 #M #M' #cm #sigma #policy #s #s' #new_b #new_b' 431 #Mrefl #new_b_refl #s_refl <Mrefl <new_b_refl <s_refl 432 whd in match write_at_stack_pointer; normalize nodelta 433 @pair_elim #nu #nl #nu_nl_refl normalize nodelta 434 @(pair_replace ?????????? (eq_to_jmeq … nu_nl_refl)) 435 [1: 436 @eq_f 437 whd in match get_8051_sfr; normalize nodelta 438 whd in match sfr_8051_index; normalize nodelta 439 whd in match status_of_pseudo_status; normalize nodelta 440 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 441 cases (\snd M) [2: * #address ] normalize nodelta 442 [1,2: 443 cases (vsplit bool ???) #high #low normalize nodelta 444 whd in match sfr_8051_index; normalize nodelta 445 >get_index_v_set_index_miss % 446 #absurd destruct(absurd) 447 |3: 448 % 449 ] 450 |2: 451 cases (get_index_v bool ????) normalize nodelta 452 whd in match status_of_pseudo_status; normalize nodelta 453 whd in match set_low_internal_ram; normalize nodelta 454 @split_eq_status try % 455 [1: 456 @(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma) 457 |2: 458 @(insert_high_internal_ram_of_pseudo_high_internal_ram … sigma) 459 ] 460 *) 416 461 417 462 lemma main_lemma_preinstruction: … … 622 667 s 623 668 | CLR addr ⇒ λinstr_refl. 624 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm.? with669 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → ? with 625 670 [ ACC_A ⇒ λacc_a: True. λEQaddr. 626 671 let s ≝ add_ticks1 s in … … 635 680 ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) 636 681 | CPL addr ⇒ λinstr_refl. 637 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm.? with682 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → ? with 638 683 [ ACC_A ⇒ λacc_a: True. λEQaddr. 639 684 let s ≝ add_ticks1 s in … … 689 734 set_8051_sfr … s SFR_ACC_A new_acc 690 735 | PUSH addr ⇒ λinstr_refl. 691 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → Σs': PreStatus m cm.? with736 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → ? with 692 737 [ DIRECT d ⇒ λdirect: True. λEQaddr. 693 738 let s ≝ add_ticks1 s in … … 906 951 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 907 952 ] 908 |3: % 953 |3: 954 % 909 955 |6: 910 956 @sym_eq @(get_cy_flag_status_of_pseudo_status M') … … 917 963 @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1) 918 964 ] 919 |3: (* SUB *)965 |3: (* SUBB *) 920 966 (* XXX: work on the right hand side *) 921 967 (* XXX: switch to the left hand side *) … … 1717 1763 ] 1718 1764 |32: (* CLR *) 1719 >EQP -P normalize nodelta 1765 >EQP -P normalize nodelta lapply instr_refl 1766 @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta 1720 1767 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1721 1768 whd in maps_assm:(??%%); 1722 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1723 [2: normalize nodelta #absurd destruct(absurd) ] 1724 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1725 whd in ⊢ (??%?); 1726 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1727 whd in ⊢ (??%?); normalize nodelta 1728 generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %); 1729 normalize nodelta #subaddressing_modein_witness 1730 @set_arg_8_status_of_pseudo_status try % 1731 [1: 1732 @sym_eq @set_clock_status_of_pseudo_status 1733 >EQs >EQticks <instr_refl % 1734 |2: 1769 [1,2: 1770 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1771 [2,4: normalize nodelta #absurd destruct(absurd) ] 1772 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1735 1773 whd in ⊢ (??%?); 1736 >(addressing_mode_ok_to_snd_M_data M' cm … addr addressing_mode_ok_assm_1) 1737 [2: <EQaddr % ] % 1738 ] 1739 |33: (* CLR *) 1740 >EQP -P normalize nodelta 1774 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1775 [1: 1776 >EQs >EQticks <instr_refl 1777 change with (set_arg_1 ??? (BIT_ADDR w) ? = ?) 1778 @set_arg_1_status_of_pseudo_status try % 1779 [1: 1780 @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … (BIT_ADDR w) … false (refl …) addressing_mode_ok_assm_1) % 1781 |2: 1782 @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … (BIT_ADDR w) … false (refl …) addressing_mode_ok_assm_1) % 1783 ] 1784 |2: 1785 >EQs >EQticks <instr_refl 1786 change with (set_arg_8 ??? ACC_A ? = ?) try % 1787 @set_arg_8_status_of_pseudo_status try % 1788 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) % 1789 ] 1790 |3: 1791 lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1792 whd in ⊢ (??%?); 1793 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1794 >EQs >EQticks <instr_refl 1795 change with (set_arg_1 ??? CARRY ? = ?) try % 1796 @set_arg_1_status_of_pseudo_status % 1797 ] 1798 |33: (* CPL *) 1799 >EQP -P normalize nodelta lapply instr_refl 1800 @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta 1741 1801 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1742 1802 whd in maps_assm:(??%%); 1743 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1744 [2: normalize nodelta #absurd destruct(absurd) ] 1745 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1746 whd in ⊢ (??%?); 1747 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1748 whd in ⊢ (??%?); normalize nodelta 1749 generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %); 1750 normalize nodelta #subaddressing_modein_witness 1751 @set_arg_1_status_of_pseudo_status try % 1752 @sym_eq @set_clock_status_of_pseudo_status 1753 >EQs >EQticks <instr_refl % 1754 |34: (* CLR *) 1755 >EQP -P normalize nodelta 1756 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1757 whd in maps_assm:(??%%); 1758 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1759 [2: normalize nodelta #absurd destruct(absurd) ] 1760 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1761 whd in ⊢ (??%?); 1762 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1763 whd in ⊢ (??%?); normalize nodelta 1764 generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %); 1765 normalize nodelta #subaddressing_modein_witness 1766 @set_arg_1_status_of_pseudo_status try % 1767 [1: 1768 @sym_eq @set_clock_status_of_pseudo_status 1769 >EQs >EQticks <instr_refl % 1770 |*: 1771 cases daemon (* XXX: requires changes to addressing_mode_ok *) 1772 ] 1773 |35: (* CPL *) 1774 >EQP -P normalize nodelta 1775 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1776 whd in maps_assm:(??%%); 1777 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1778 [2: normalize nodelta #absurd destruct(absurd) ] 1779 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1780 whd in ⊢ (??%?); 1781 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1782 whd in ⊢ (??%?); normalize nodelta 1783 generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %); 1784 normalize nodelta #subaddressing_modein_witness 1785 @set_8051_sfr_status_of_pseudo_status 1786 [1: 1787 @sym_eq @set_clock_status_of_pseudo_status 1788 >EQs >EQticks <instr_refl % 1789 |2: 1790 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data M' cm … addr addressing_mode_ok_assm_1) 1791 [2: <EQaddr % ] normalize nodelta @eq_f 1792 @(pose … (set_clock ????)) #status #status_refl 1793 @sym_eq @(get_8051_sfr_status_of_pseudo_status M' … status) >status_refl 1794 >EQs >EQticks <instr_refl try % 1795 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addr addressing_mode_ok_assm_1) 1796 [2: <EQaddr % ] % 1797 ] 1798 |36: (* CPL *) 1799 >EQP -P normalize nodelta 1800 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1801 whd in maps_assm:(??%%); 1802 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1803 [2: normalize nodelta #absurd destruct(absurd) ] 1804 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1805 whd in ⊢ (??%?); 1806 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1807 whd in ⊢ (??%?); normalize nodelta 1808 generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %); 1809 normalize nodelta #subaddressing_modein_witness 1810 @set_arg_1_status_of_pseudo_status try % 1811 [1: 1812 @eq_f @(get_arg_1_status_of_pseudo_status … M') try % 1813 @sym_eq @set_clock_status_of_pseudo_status 1814 >EQs >EQticks <instr_refl <EQaddr % 1815 |2: 1816 @sym_eq @set_clock_status_of_pseudo_status 1817 >EQs >EQticks <instr_refl <EQaddr % 1818 ] 1819 |37: (* CPL *) 1820 >EQP -P normalize nodelta 1821 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1822 whd in maps_assm:(??%%); 1823 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1824 [2: normalize nodelta #absurd destruct(absurd) ] 1825 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1826 whd in ⊢ (??%?); 1827 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1828 whd in ⊢ (??%?); normalize nodelta 1829 generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %); 1830 normalize nodelta #subaddressing_modein_witness 1831 @set_arg_1_status_of_pseudo_status 1832 [1: 1803 [1,2: 1804 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1805 [2,4: normalize nodelta #absurd destruct(absurd) ] 1806 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1807 whd in ⊢ (??%?); 1808 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1809 [1: 1810 >EQs >EQticks <instr_refl 1811 change with (set_arg_1 ??? (BIT_ADDR w) ? = ?) 1812 @set_arg_1_status_of_pseudo_status 1813 [1: 1814 @eq_f 1815 @sym_eq @(pose … (set_clock ????)) #status #status_refl 1816 @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try % 1817 @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … (BIT_ADDR w) … addressing_mode_ok_assm_1) % 1818 |2: 1819 % 1820 |3: 1821 @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … (BIT_ADDR w) … true (refl …) addressing_mode_ok_assm_1) % 1822 |4: 1823 @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … (BIT_ADDR w) … (refl …) addressing_mode_ok_assm_1) % 1824 ] 1825 |2: 1826 >EQs >EQticks <instr_refl 1827 change with (set_8051_sfr ????? = ?) 1828 @set_8051_sfr_status_of_pseudo_status try % 1829 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) try % 1830 normalize nodelta @eq_f 1831 @(pose … (set_clock ????)) #status #status_refl 1832 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try % 1833 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) % 1834 ] 1835 |3: 1836 lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1837 whd in ⊢ (??%?); 1838 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 1839 >EQs >EQticks <instr_refl 1840 change with (set_arg_1 ??? CARRY ? = ?) try % 1841 @set_arg_1_status_of_pseudo_status try % 1833 1842 @eq_f 1834 @(pose … (set_clock ????)) #status #status_refl 1835 @(get_arg_1_status_of_pseudo_status … M' … status) try % >status_refl 1836 >EQs >EQticks <instr_refl <EQaddr 1837 [1: 1838 @sym_eq @set_clock_status_of_pseudo_status % 1839 |2: 1840 cases daemon (* XXX: require changes to addressing_mode_ok *) 1841 ] 1842 |2: 1843 @sym_eq @set_clock_status_of_pseudo_status 1844 >EQs >EQticks <instr_refl <EQaddr % 1845 |*: 1846 cases daemon (* XXX: require changes to addressing_mode_ok *) 1847 ] 1848 |38,40: (* RL and RR *) 1843 @sym_eq @(pose … (set_clock ????)) #status #status_refl 1844 @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl % 1845 ] 1846 |34,36: (* RL and RR *) 1849 1847 (* XXX: work on the right hand side *) 1850 1848 (* XXX: switch to the left hand side *) … … 1869 1867 ] 1870 1868 @sym_eq @set_program_counter_status_of_pseudo_status % 1871 |3 9,41: (* RLC and RRC *)1869 |35,37: (* RLC and RRC *) 1872 1870 (* XXX: work on the right hand side *) 1873 1871 (* XXX: switch to the left hand side *) … … 1897 1895 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) % 1898 1896 ] 1899 | 42: (* SWAP *)1897 |38: (* SWAP *) 1900 1898 >EQP -P normalize nodelta 1901 1899 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} … … 1935 1933 ] 1936 1934 ] 1937 | 43: (* MOV *)1935 |39: (* MOV *) 1938 1936 >EQP -P normalize nodelta 1939 1937 inversion addr … … 2062 2060 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 2063 2061 |2: 2064 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) % 2062 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 2063 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] % 2065 2064 ] 2066 2065 ] … … 2128 2127 |2: 2129 2128 >EQs >EQticks <instr_refl >addr_refl % 2130 |3,4: (* XXX: following two cases same proof but Matita is too slow if merged *)2129 |3,4: 2131 2130 @(pose … (set_clock ????)) #status #status_refl 2132 2131 [1: … … 2140 2139 ] 2141 2140 ] 2142 |4 4: (* MOVX *)2141 |40: (* MOVX *) 2143 2142 >EQP -P normalize nodelta 2144 2143 inversion addr … … 2213 2212 ] 2214 2213 ] 2215 | *)45: (* SETB *)2214 |41: (* SETB *) 2216 2215 >EQs >EQticks <instr_refl 2217 2216 >EQP -P normalize nodelta … … 2230 2229 @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … b … false (refl …) addressing_mode_ok_assm_1) 2231 2230 ] 2232 |46: (* PUSH *) 2231 |*)42: (* PUSH *) 2232 >EQP -P normalize nodelta lapply instr_refl 2233 @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta 2234 #sigma_increment_commutation 2235 whd in ⊢ (??%? → ?); inversion M #callM #accM #callM_accM_refl normalize nodelta 2236 @Some_Some_elim #Mrefl destruct(Mrefl) #fetch_many_assm %{1} 2237 whd in ⊢ (??%?); 2238 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 2239 whd in ⊢ (??%?); 2240 @pair_elim #carry #new_sp #carry_new_sp_refl normalize nodelta 2241 @(pair_replace ?????????? (eq_to_jmeq … carry_new_sp_refl)) 2242 [1: 2243 @eq_f2 try % 2244 @(pose … (set_clock ????)) #status #status_refl 2245 @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈callM, accM〉 … status) >status_refl -status_refl try % 2246 @sym_eq @set_clock_status_of_pseudo_status 2247 >EQs >EQticks <instr_refl % 2248 |2: 2249 >EQs >EQticks <instr_refl 2250 XXX 2251 ] 2252 |46: (* RET *) 2233 2253 >EQP -P normalize nodelta 2234 #sigma_increment_commutation whd in ⊢ (??%% → ?); 2235 inversion M #callM #accM #callM_accM_refl normalize nodelta 2236 @(subaddressing_mode_elim … addr) #w normalize nodelta 2237 @Some_Some_elim #Mrefl destruct(Mrefl) 2238 cases daemon (* XXX *) 2254 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2255 whd in maps_assm:(??%%); normalize nodelta in maps_assm; 2256 lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta 2257 inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_1 2258 [2: normalize nodelta #absurd destruct(absurd) ] 2259 inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_2 2260 [2: normalize nodelta #absurd destruct(absurd) ] 2261 normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl) 2262 whd in ⊢ (??%?); 2263 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 2264 whd in ⊢ (??%?); 2265 @(pair_replace ?????????? p) normalize nodelta 2266 >EQs >EQticks <instr_refl 2267 [1: 2268 @eq_f3 try % 2269 @sym_eq @(pose … (set_clock ????)) #status #status_refl 2270 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl % 2271 |2: 2272 @(pair_replace ?????????? p1) normalize nodelta 2273 >EQs >EQticks <instr_refl 2274 [1: 2275 @eq_f3 try % 2276 @sym_eq @(pose … (set_clock ????)) #status #status_refl 2277 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl 2278 [1: 2279 cases daemon 2280 (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *) 2281 |2: 2282 whd in match get_8051_sfr in ⊢ (???%); normalize nodelta 2283 whd in match set_8051_sfr in ⊢ (???%); normalize nodelta 2284 whd in match sfr_8051_index; normalize nodelta 2285 >get_index_v_set_index_hit 2286 change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp) 2287 cases daemon 2288 (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *) 2289 ] 2290 |2: 2291 cases daemon (* XXX *) 2292 ] 2293 ] 2239 2294 |47: (* POP *) 2240 2295 |48: (* XCH *) … … 2363 2418 ] 2364 2419 |50: (* RET *) 2365 >EQP -P normalize nodelta2366 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}2367 whd in maps_assm:(??%%); normalize nodelta in maps_assm;2368 lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta2369 inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_12370 [2: normalize nodelta #absurd destruct(absurd) ]2371 inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_22372 [2: normalize nodelta #absurd destruct(absurd) ]2373 normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl)2374 whd in ⊢ (??%?);2375 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm2376 whd in ⊢ (??%?);2377 @(pair_replace ?????????? p) normalize nodelta2378 >EQs >EQticks <instr_refl2379 [1:2380 @eq_f3 try %2381 @sym_eq @(pose … (set_clock ????)) #status #status_refl2382 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl %2383 |2:2384 @(pair_replace ?????????? p1) normalize nodelta2385 >EQs >EQticks <instr_refl2386 [1:2387 @eq_f3 try %2388 @sym_eq @(pose … (set_clock ????)) #status #status_refl2389 @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl2390 [1:2391 cases daemon2392 (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)2393 |2:2394 whd in match get_8051_sfr in ⊢ (???%); normalize nodelta2395 whd in match set_8051_sfr in ⊢ (???%); normalize nodelta2396 whd in match sfr_8051_index; normalize nodelta2397 >get_index_v_set_index_hit2398 change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp)2399 cases daemon2400 (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)2401 ]2402 |2:2403 cases daemon (* XXX *)2404 ]2405 ]2406 2420 |51: (* RETI *) 2407 2421 |52: (* NOP *)
Note: See TracChangeset
for help on using the changeset viewer.