Changeset 1974
 Timestamp:
 May 21, 2012, 5:03:20 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/SimplifyCasts.ma
r1970 r1974 1109 1109 «Expr (Ebinop op lhs1 rhs1) ty, ?» 1110 1110  Ecast cast_ty castee ⇒ λHdesc_eq. 1111 match cast_ty with 1112 [ Tint cast_sz cast_sg ⇒ 1113 let «〈success, castee〉, Htrans_inv» as Hsimplify, Hpair ≝ simplify_expr2 castee cast_sz cast_sg in 1114 match success with 1115 [ true ⇒ 1116 «castee, ?» 1117  false ⇒ 1118 «Expr (Ecast cast_ty castee) ty, ?» 1119 ] 1120  _ ⇒ 1121 «e, ?» 1122 ] 1111 match type_eq_dec ty cast_ty with 1112 [ inl Hcast_eq ⇒ 1113 match cast_ty return λx. x = cast_ty → Σresult:expr. (∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result) 1114 ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result) 1115 ∧ typeof e = typeof result) 1116 with 1117 [ Tint cast_sz cast_sg ⇒ λHcast_ty_eq. 1118 let «〈success, castee1〉, Htrans_inv» as Hsimplify, Hpair ≝ simplify_expr2 castee cast_sz cast_sg in 1119 match success return λx. x = success → Σresult:expr. (∀ge,en,m. simulate ? (exec_expr ge en m e) (exec_expr ge en m result) 1120 ∧ simulate ? (exec_lvalue ge en m e) (exec_lvalue ge en m result) 1121 ∧ typeof e = typeof result) 1122 with 1123 [ true ⇒ λHsuccess_eq. 1124 «castee1, ?» 1125  false ⇒ λHsuccess_eq. 1126 «Expr (Ecast cast_ty castee1) ty, ?» 1127 ] (refl ? success) 1128  _ ⇒ λHcast_ty_eq. 1129 «e, ?» 1130 ] (refl ? cast_ty) 1131  inr Hcast_neq ⇒ 1132 «e, ?» 1133 ] 1134  Econdition cond iftrue iffalse ⇒ λHdesc_eq. 1135 let «cond1, Hequiv_cond» as Eq_cond ≝ simplify_inside cond in 1136 let «iftrue1, Hequiv_iftrue» as Eq_iftrue ≝ simplify_inside iftrue in 1137 let «iffalse1, Hequiv_iffalse» as Eq_iffalse ≝ simplify_inside iffalse in 1138 «Expr (Econdition cond1 iftrue1 iffalse1) ty, ?» 1139  Eandbool lhs rhs ⇒ λHdesc_eq. 1140 let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in 1141 let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in 1142 «Expr (Eandbool lhs1 rhs1) ty, ?» 1143  Eorbool lhs rhs ⇒ λHdesc_eq. 1144 let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in 1145 let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in 1146 «Expr (Eorbool lhs1 rhs1) ty, ?» 1147  Efield rec_expr f ⇒ λHdesc_eq. 1148 let «rec_expr1, Hequiv_rec» as Eq_rec ≝ simplify_inside rec_expr in 1149 «Expr (Efield rec_expr1 f) ty, ?» 1150  Ecost l e1 ⇒ λHdesc_eq. 1151 let «e2, Hequiv» as Eq ≝ simplify_inside e1 in 1152 «Expr (Ecost l e2) ty, ?» 1123 1153  _ ⇒ λHdesc_eq. 1124 (* TODO, replace this stub by the actual recursive calls to simplify_inside. Should be nonproblematic. *)1125 1154 «e, ?» 1126 1155 ] (refl ? ed) … … 1715 1744 whd in match (exec_expr ??? (Expr ??)); 1716 1745 cases Hsim_expr 1717 [ 2: * #error #Hexec_error >Hexec_error normalize nodelta@SimFail /2 by ex_intro/1746 [ 2: * #error #Hexec_error >Hexec_error @SimFail /2 by ex_intro/ 1718 1747  1: cases (exec_expr ge en m e1) 1719 [ 2: #error #_ normalize nodelta@SimFail /2 by ex_intro/1748 [ 2: #error #_ @SimFail /2 by ex_intro/ 1720 1749  1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #He2_exec >He2_exec 1721 normalize nodelta@SimOk #a #H @H1750 @SimOk #a #H @H 1722 1751 ] 1723 1752 ] 1724  3: normalize@SimFail /2 by ex_intro/1753  3: @SimFail /2 by ex_intro/ 1725 1754 ] 1726 1755 ] 1727 1756  46: destruct elim (Hexpr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 1728 whd in match (exec_expr ??? (Expr ??));1729 whd in match (exec_expr ??? (Expr ??));1730 1757 %1 try @refl 1731 [ 1: >Htype_eq // 1732  2: whd in match (exec_expr ??? (Expr ??)); 1733 whd in match (exec_expr ??? (Expr ??)); 1734 cases Hsim_expr 1735 [ 2: * #error #Hexec_error >Hexec_error normalize nodelta @SimFail /2 by ex_intro/ 1736  1: cases (exec_expr ge en m e1) 1737 [ 2: #error #_ normalize nodelta @SimFail /2 by ex_intro/ 1738  1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #He2_exec >He2_exec 1739 normalize nodelta @SimOk #a #H @H 1740 ] 1758 [ 1: whd in match (exec_expr ??? (Expr ??)); 1759 whd in match (exec_expr ??? (Expr ??)); 1760 cases Hsim_expr 1761 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ 1762  1: cases (exec_expr ge en m e1) 1763 [ 2: #error #_ @SimFail /2 by ex_intro/ 1764  1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hsim2 >Hsim2 @SimOk #a #H @H ] 1765 ] 1766  2: @SimFail /2 by ex_intro/ ] 1767 (* simplify_inside cases. Amounts to propagate a simulation result, except for the /cast/ case which actually calls 1768 * simplify_expr2 *) 1769  47, 48, 49: (* trivial const_int, const_float and var cases *) 1770 try @conj try @conj try @refl 1771 @SimOk #a #H @H 1772  50: (* Deref case *) destruct 1773 elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 1774 try @conj try @conj 1775 [ 1: 1776 whd in match (exec_expr ??? (Expr ??)); 1777 whd in match (exec_expr ??? (Expr ??)); 1778 whd in match (exec_lvalue' ?????); 1779 whd in match (exec_lvalue' ?????); 1780  2: 1781 whd in match (exec_lvalue ??? (Expr ??)); 1782 whd in match (exec_lvalue ??? (Expr ??)); 1783 ] 1784 [ 1,2: 1785 cases Hsim_expr 1786 [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ 1787  1,3: cases (exec_expr ge en m e1) 1788 [ 2,4: #error #_ @SimFail /2 by ex_intro/ 1789  1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ] 1790  3: // ] 1791  51: (* Addrof *) destruct 1792 elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 1793 try @conj try @conj 1794 [ 1: 1795 whd in match (exec_expr ??? (Expr ??)); 1796 whd in match (exec_expr ??? (Expr ??)); 1797 cases Hsim_lvalue 1798 [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/ 1799  1: cases (exec_lvalue ge en m e1) 1800 [ 2: #error #_ @SimFail /2 by ex_intro/ 1801  1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ] 1802  2: @SimFail /2 by ex_intro/ 1803  3: // ] 1804  52: (* Unop *) destruct 1805 elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 1806 try @conj try @conj 1807 [ 1: 1808 whd in match (exec_expr ??? (Expr ??)); 1809 whd in match (exec_expr ??? (Expr ??)); 1810 cases Hsim_expr 1811 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ 1812  1: cases (exec_expr ge en m e1) 1813 [ 2: #error #_ @SimFail /2 by ex_intro/ 1814  1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk 1815 >Htype_eq #a #H @H ] ] 1816  2: @SimFail /2 by ex_intro/ 1817  3: // ] 1818  53: (* Binop *) destruct 1819 elim (Hequiv_lhs ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs 1820 elim (Hequiv_rhs ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs 1821 try @conj try @conj 1822 [ 1: 1823 whd in match (exec_expr ??? (Expr ??)); 1824 whd in match (exec_expr ??? (Expr ??)); 1825 cases Hsim_expr_lhs 1826 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ 1827  1: cases (exec_expr ge en m lhs) 1828 [ 2: #error #_ @SimFail /2 by ex_intro/ 1829  1: #lhs_value #Hsim_lhs cases Hsim_expr_rhs 1830 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ 1831  1: cases (exec_expr ge en m rhs) 1832 [ 2: #error #_ @SimFail /2 by ex_intro/ 1833  1: #rhs_value #Hsim_rhs 1834 lapply (Hsim_lhs lhs_value (refl ? (OK ? lhs_value))) 1835 lapply (Hsim_rhs rhs_value (refl ? (OK ? rhs_value))) 1836 #Hrhs >Hrhs #Hlhs >Hlhs >Htype_eq_rhs >Htype_eq_lhs 1837 @SimOk #a #H @H 1838 ] 1839 ] 1840 ] 1841 ] 1842  2: @SimFail /2 by ex_intro/ 1843  3: // 1844 ] 1845  54: (* Cast, fallback case *) 1846 try @conj try @conj try @refl 1847 @SimOk #a #H @H 1848  55: (* Cast, success case *) destruct 1849 inversion (Htrans_inv ge en m) 1850 [ 1: (* contradiction *) 1851 #result_flag #Hresult_flag #Htype_eq #Hsim_epr #Hsim_lvalue #Hresult_flag_true 1852 <Hresult_flag_true in Hresult_flag; #Habsurd destruct 1853  2: #src_sz #src_sg #Hsrc_type_eq #Htarget_type_eq #Hsmaller #_ #_ 1854 try @conj try @conj try @conj 1855 [ 1: whd in match (exec_expr ??? (Expr ??)); 1856 cases (exec_expr ge en m castee) in Hsmaller; 1857 [ 2: #error #_ @SimFail /2 by ex_intro/ 1858  1: * #val #trace cases (exec_expr ge en m castee1) 1859 [ 2: #error #Habsurd @(False_ind … Habsurd) 1860  1: * #val1 #trace1 #Hsmaller elim (smaller_integer_val_spec … Hsmaller) 1861 #v1 * #v2 * * * * #Hval1 #Hval2 #Hcast #Htrace #Hle 1862 >Hsrc_type_eq normalize nodelta cases val in Hval1; 1863 [ 1: #Hval1  2: #sz #i #Hval1  3,4,5: #irrelevant #Hval1 ] 1864 [ 1,3,4,5: normalize @SimFail /2 by ex_intro/ ] 1865 whd in match (exec_cast ????); 1866 cases (sz_eq_dec sz src_sz) 1867 [ 2: #Hneq normalize nodelta 1868 >(intsize_eq_elim_false (res ?) sz src_sz ???? Hneq) 1869 @SimFail /2 by ex_intro/ 1870  1: #Heq <Heq normalize nodelta >intsize_eq_elim_true 1871 destruct normalize 1872 @SimOk #a #H @H 1873 ] 1874 ] 1875 ] 1876  2: @SimFail /2 by ex_intro/ 1877  3: >Htarget_type_eq // 1878 ] 1879 ] 1880  56: (* Cast, "failure" case *) destruct 1881 inversion (Htrans_inv ge en m) 1882 [ 2: (* contradiction *) 1883 #src_sz #src_sg #Htype_castee #Htype_castee1 #Hsmaller #Habsurd 1884 lapply (jmeq_to_eq ??? Habsurd) Habsurd #Herror destruct 1885  1: #result_flag #Hresult_flag #Htype_eq #Hsim_expr #Hsim_lvalue #_ #_ 1886 try @conj try @conj try @conj 1887 [ 1: whd in match (exec_expr ????); 1888 whd in match (exec_expr ??? (Expr ??)); 1889 cases Hsim_expr 1890 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ 1891  1: cases (exec_expr ??? castee) 1892 [ 2: #error #_ @SimFail /2 by ex_intro/ 1893  1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec_ok >Hexec_ok 1894 @SimOk >Htype_eq #a #H @H ] 1895 ] 1896  2: @SimFail /2 by ex_intro/ 1897  3: // 1898 ] 1899 ] 1900  57,58,59,60,61,62,63,64,68: 1901 try @conj try @conj try @refl 1902 @SimOk #a #H @H 1903  65: destruct 1904 elim (Hequiv_cond ge en m) * #Hsim_exec_cond #Hsim_lvalue_cond #Htype_eq_cond 1905 elim (Hequiv_iftrue ge en m) * #Hsim_exec_true #Hsim_lvalue_true #Htype_eq_true 1906 elim (Hequiv_iffalse ge en m) * #Hsim_exec_false #Hsim_lvalue_false #Htype_eq_false 1907 try @conj try @conj 1908 [ 1: whd in match (exec_expr ??? (Expr ??)); 1909 whd in match (exec_expr ??? (Expr ??)); 1910 cases Hsim_exec_cond 1911 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ 1912  1: cases (exec_expr ??? cond) 1913 [ 2: #error #_ @SimFail /2 by ex_intro/ 1914  1: * #condb #condtrace #Hcond_sim lapply (Hcond_sim 〈condb, condtrace〉 (refl ? (OK ? 〈condb, condtrace〉))) 1915 #Hcond_ok >Hcond_ok >Htype_eq_cond 1916 normalize nodelta 1917 cases (exec_bool_of_val condb (typeof cond1)) 1918 [ 2: #error @SimFail /2 by ex_intro/ 1919  1: * whd in match (m_bind ?????); whd in match (m_bind ?????); 1920 normalize nodelta 1921 [ 1: (* true branch taken *) 1922 cases Hsim_exec_true 1923 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ 1924  1: cases (exec_expr ??? iftrue) 1925 [ 2: #error #_ @SimFail /2 by ex_intro/ 1926  1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H 1927 @SimOk #a #H @H 1928 ] 1929 ] 1930  2: (* false branch taken *) 1931 cases Hsim_exec_false 1932 [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ 1933  1: cases (exec_expr ??? iffalse) 1934 [ 2: #error #_ @SimFail /2 by ex_intro/ 1935  1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H 1936 @SimOk #a #H @H 1937 ] 1938 ] 1939 ] 1940 ] 1941 ] 1942 ] 1943  2: @SimFail /2 by ex_intro/ 1944  3: // 1945 ] 1946  66,67: destruct 1947 elim (Hequiv_lhs ge en m) * #Hsim_exec_lhs #Hsim_lvalue_lhs #Htype_eq_lhs 1948 elim (Hequiv_rhs ge en m) * #Hsim_exec_rhs #Hsim_lvalue_rhs #Htype_eq_rhs 1949 try @conj try @conj 1950 whd in match (exec_expr ??? (Expr ??)); 1951 whd in match (exec_expr ??? (Expr ??)); 1952 [ 1,4: cases Hsim_exec_lhs 1953 [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ 1954  1,3: cases (exec_expr ??? lhs) 1955 [ 2,4: #error #_ @SimFail /2 by ex_intro/ 1956  1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hlhs >Hlhs >Htype_eq_lhs 1957 normalize nodelta elim a #lhs_val #lhs_trace 1958 cases (exec_bool_of_val lhs_val (typeof lhs1)) 1959 [ 2,4: #error @SimFail /2 by ex_intro/ 1960  1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????); 1961 [ 2,3: @SimOk // 1962  1,4: cases Hsim_exec_rhs 1963 [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/ 1964  1,3: cases (exec_expr ??? rhs) 1965 [ 2,4: #error #_ @SimFail /2 by ex_intro/ 1966  1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrhs >Hrhs >Htype_eq_rhs 1967 @SimOk #a #H @H 1968 ] 1969 ] 1970 ] 1971 ] 1741 1972 ] 1742  3: normalize @SimFail 1743 ] 1744 1745 1746 1747 1748 1749 1750 1973 ] 1974  2,5: @SimFail /2 by ex_intro/ 1975  3,6: // 1976 ] 1977  69: (* record field *) destruct 1978 elim (Hequiv_rec ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 1979 try @conj try @conj 1980 whd in match (exec_expr ??? (Expr ??)); 1981 whd in match (exec_expr ??? (Expr ??)); 1982 whd in match (exec_lvalue' ??? (Efield rec_expr f) ty); 1983 whd in match (exec_lvalue' ??? (Efield rec_expr1 f) ty); 1984 [ 1: >Htype_eq cases (typeof rec_expr1) normalize nodelta 1985 [ 2: #sz #sg  3: #fl  4: #rg #ty'  5: #rg #ty #n  6: #tl #ty' 1986  7: #id #fl  8: #id #fl  9: #rg #id ] 1987 try (@SimFail /2 by ex_intro/) 1988 cases Hsim_lvalue 1989 [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/ 1990  1,3: cases (exec_lvalue ge en m rec_expr) 1991 [ 2,4: #error #_ @SimFail /2 by ex_intro/ 1992  1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec 1993 @SimOk #a #H @H ] 1994 ] 1995  2: (* Note: identical to previous case. Too lazy to merge and manually shift indices. *) 1996 >Htype_eq cases (typeof rec_expr1) normalize nodelta 1997 [ 2: #sz #sg  3: #fl  4: #rg #ty'  5: #rg #ty #n  6: #tl #ty' 1998  7: #id #fl  8: #id #fl  9: #rg #id ] 1999 try (@SimFail /2 by ex_intro/) 2000 cases Hsim_lvalue 2001 [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/ 2002  1,3: cases (exec_lvalue ge en m rec_expr) 2003 [ 2,4: #error #_ @SimFail /2 by ex_intro/ 2004  1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec 2005 @SimOk #a #H @H ] 2006 ] 2007  3: // ] 2008  70: (* cost label *) destruct 2009 elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 2010 try @conj try @conj 2011 whd in match (exec_expr ??? (Expr ??)); 2012 whd in match (exec_expr ??? (Expr ??)); 2013 [ 1: 2014 cases Hsim_expr 2015 [ 2: * #error #Hexec >Hexec @SimFail /2 by ex_intro/ 2016  1: cases (exec_expr ??? e1) 2017 [ 2: #error #_ @SimFail /2 by ex_intro/ 2018  1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H 2019 @SimOk #a #H @H ] 2020 ] 2021  2: @SimFail /2 by ex_intro/ 2022  3: // 2023 ] 2024 ] qed. 1751 2025 1752 2026 … … 1754 2028 returns a flag stating whether the desired type was achieved and a simplified 1755 2029 version of e. *) 1756 let rec simplify_expr (e:expr) (ty':type) : bool × expr ≝ 2030 let rec simplify_expr (e:expr) (ty':type) : bool × expr ≝ 1757 2031 match e with 1758 2032 [ Expr ed ty ⇒
Note: See TracChangeset
for help on using the changeset viewer.