Changeset 1974


Ignore:
Timestamp:
May 21, 2012, 5:03:20 PM (5 years ago)
Author:
garnier
Message:

Progress on the cast simplification proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r1970 r1974  
    11091109    «Expr (Ebinop op lhs1 rhs1) ty, ?»
    11101110  | 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, ?»       
    11231153  | _ ⇒ λHdesc_eq.
    1124     (* TODO, replace this stub by the actual recursive calls to simplify_inside. Should be non-problematic. *)
    11251154    «e, ?»
    11261155  ] (refl ? ed)
     
    17151744             whd in match (exec_expr ??? (Expr ??));
    17161745             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/
    17181747             | 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/
    17201749                  | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #He2_exec >He2_exec
    1721                         normalize nodelta @SimOk #a #H @H
     1750                        @SimOk #a #H @H
    17221751                  ]
    17231752             ]
    1724         | 3: normalize @SimFail /2 by ex_intro/
     1753        | 3: @SimFail /2 by ex_intro/
    17251754        ]
    17261755   ]
    17271756| 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 ??));
    17301757      %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                   ]
    17411972             ]
    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.   
    17512025
    17522026
     
    17542028   returns a flag stating whether the desired type was achieved and a simplified
    17552029   version of e. *)
    1756 let rec simplify_expr (e:expr) (ty':type) : bool × expr ≝
     2030let rec simplify_expr (e:expr) (ty':type) : bool × expr ≝ 
    17572031match e with
    17582032[ Expr ed ty ⇒
Note: See TracChangeset for help on using the changeset viewer.