Changeset 3049
 Timestamp:
 Apr 1, 2013, 12:06:08 AM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/SimplifyCasts.ma
r3048 r3049 1890 1890 . 1891 1891 1892 record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {1893 rg_find_symbol: ∀s.1894 find_symbol ? ge s = find_symbol ? ge' s;1895 rg_find_funct: ∀v,f,id.1896 find_funct_id ? ge v = Some ? 〈f,id〉 →1897 find_funct_id ? ge' v = Some ? 〈t f,id〉;1898 rg_find_funct_ptr: ∀b,f.1899 find_funct_ptr ? ge b = Some ? f →1900 find_funct_ptr ? ge' b = Some ? (t f)1901 }.1902 1903 1892 (* The return type of any function is invariant under cast simplification *) 1904 1893 lemma fn_return_simplify : ∀f. fn_return (simplify_function f) = fn_return f. … … 1914 1903 ] qed. 1915 1904 1916 lemma sim_related_globals : ∀ge,ge',en,m. related_globals ?simplify_fundef ge ge' →1905 lemma sim_related_globals : ∀ge,ge',en,m. related_globals … simplify_fundef ge ge' → 1917 1906 (∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧ 1918 1907 (∀ed, ty. res_sim ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)). … … 1936 1925 cases (lookup SymbolTag block en v) normalize nodelta 1937 1926 [ 2: #block @SimOk // 1938  1: elim Hrelated #Hsymbol #_ #_ >(Hsymbolv) @SimOk //1927  1: >(rg_find_symbol … Hrelated … v) @SimOk // 1939 1928 ] 1940 1929  4: #e #ty #Hsim_expr whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????); … … 2064 2053 2065 2054 lemma related_globals_expr_simulation : ∀ge,ge',en,m. 2066 related_globals ?simplify_fundef ge ge' →2055 related_globals … simplify_fundef ge ge' → 2067 2056 ∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m (simplify_e e)) ∧ 2068 2057 typeof e = typeof (simplify_e e). … … 2080 2069 2081 2070 lemma related_globals_lvalue_simulation : ∀ge,ge',en,m. 2082 related_globals ?simplify_fundef ge ge' →2071 related_globals … simplify_fundef ge ge' → 2083 2072 ∀e. res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge' en m (simplify_e e)) ∧ 2084 2073 typeof e = typeof (simplify_e e). … … 2099 2088 2100 2089 lemma related_globals_exprlist_simulation : ∀ge,ge',en,m. 2101 related_globals ?simplify_fundef ge ge' →2090 related_globals … simplify_fundef ge ge' → 2102 2091 ∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m (map expr expr simplify_e args)). 2103 2092 #ge #ge' #en #m #Hrelated #args … … 2406 2395 2407 2396 theorem cast_correction : ∀ge, ge'. 2408 related_globals ?simplify_fundef ge ge' →2397 related_globals … simplify_fundef ge ge' → 2409 2398 ∀s1, s1', tr, s2. 2410 2399 state_cast s1 s1' → … … 2555 2544  1: #l Hsim #Hsim lapply (Hsim l (refl ? (OK ? l))) #Heq >Heq 2556 2545 whd in match (bindIO ??????) in ⊢ (% → %); 2557 elim Hrelated #_ #Hfunct #_ lapply (Hfunct(\fst a))2546 lapply (rg_find_funct_id … Hrelated … (\fst a)) 2558 2547 cases (find_funct_id clight_fundef ge (\fst a)); 2559 2548 [ 1: #_ #Habsurd normalize in Habsurd; destruct (Habsurd) … … 2872 2861 #Habsurd destruct (Habsurd) 2873 2862 ] qed. 2863 2864 lemma initial_state_casts : ∀p,s. 2865 make_initial_state p = OK ? s → 2866 ∃s'. 2867 make_initial_state (simplify_program p) = OK ? s' ∧ 2868 related_globals … simplify_fundef (make_global p) (make_global (simplify_program p)) ∧ 2869 state_cast s s'. 2870 * #vars #fns #main #s 2871 whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX 2872 cases (bind_inversion ????? EX) EX #m * #Em #EX 2873 cases (bind_inversion ????? EX) EX #b * #Emain #EX 2874 cases (bind_inversion ????? EX) EX #fd * #Emain' #EX 2875 whd in EX:(??%%); destruct 2876 whd in match (make_initial_state ?); 2877 letin ge' ≝ (make_global ?) 2878 cut (related_globals … simplify_fundef ge ge') 2879 [ // ] #RG 2880 lapply (rg_find_funct_ptr … RG … Emain') #FFP 2881 % [2: % 2882 [ % 2883 [whd in ⊢ (??%?); 2884 change with (transform_program ??? (mk_program …) (λ_.?)) in match (mk_program ??? (transf_program ????) ?); 2885 >(init_mem_transf … (mk_program ?? vars fns main)) >Em in ⊢ (??%?); 2886 whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?); 2887 whd in ⊢ (??%?); >FFP in ⊢ (??%?); 2888 whd in ⊢ (??%?); @refl 2889  /3/ 2890 ]  /3/ ]  skip ] 2891 qed. 2892 2893
Note: See TracChangeset
for help on using the changeset viewer.