Changeset 3044
 Timestamp:
 Mar 29, 2013, 8:16:50 PM (7 years ago)
 Location:
 src/Clight
 Files:

 1 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/switchRemoval.ma
r2734 r3044 2755 2755 exec_step ge s1 = Value … 〈tr,s2〉 → 2756 2756 ∃n. after_n_steps (S n) … clight_exec ge' s1' (λ_. true) 2757 (λtr',s2'. tr = tr' ∧ switch_state_sim ge 's2 s2').2757 (λtr',s2'. tr = tr' ∧ switch_state_sim ge s2 s2'). 2758 2758 #ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state 2759 2759 inversion Hsim_state … … 2798 2798 <sss_func_hyp 2799 2799 lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') 2800 %1{u (refl ? (switch_removal s u))} try assumption try @refl 2801 #id #Hmem lapply (Hext_fresh_for_ge id Hmem) #Hfind <(rg_find_symbol … Hrelated id) @Hfind 2800 %1{u (refl ? (switch_removal s u))} assumption 2802 2801  3: #cond #body #k #k' #fgen #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ 2803 2802 lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') … … 2810 2809  3: whd in match (switch_removal ??); 2811 2810 cases (switch_removal body fgen) in Hincl; * #body' #fvs' #fgen' normalize nodelta #H @H 2812  4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem]2811 ] 2813 2812  4: #cond #body #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ 2814 2813 lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') … … 2825 2824  2: whd in match (switch_removal ??); 2826 2825 cases (switch_removal body u) in Hincl; * #body' #fvs' #u' normalize nodelta #H @H 2827  3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem]2826 ] 2828 2827  2: %{u … (switch_removal Sskip u) } try assumption try // 2829 [ 1:@(fresh_for_Sskip … Hfresh)2830  2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]]2828 @(fresh_for_Sskip … Hfresh) 2829 ] 2831 2830  5: #cond #stmt1 #stmt2 #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ 2832 2831 #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ … … 2834 2833 #Hexec_step %{0} whd whd in Hresult:(??%?) Hexec_step:(??%?); destruct (Hexec_step) 2835 2834 @conj try @refl 2836 %{u … new_vars … sss_mem_hyp … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} try // try assumption 2837 #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem 2835 %{u … new_vars … sss_mem_hyp … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} try // assumption 2838 2836  6: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars 2839 2837 #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ … … 2847 2845 whd in match (ret_vars ??); /2 by All_append_l/ 2848 2846  3: @(swc_for3 … u) // 2849  4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem]2847 ] 2850 2848  7: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars 2851 2849 #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ … … 2854 2852 %1{u … new_vars … sss_writeable … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} 2855 2853 try // try assumption 2856 [ 1: whd in match (switch_removal ??) in ⊢ (??%%); destruct normalize 2857 cases (switch_removal stmt1 u) * #stmt1' #fvs1' #u' normalize 2858 cases (switch_removal stmt2 u') * #stmt2' #fvs2' #u'' @refl 2859  2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] 2854 whd in match (switch_removal ??) in ⊢ (??%%); destruct normalize 2855 cases (switch_removal stmt1 u) * #stmt1' #fvs1' #u' normalize 2856 cases (switch_removal stmt2 u') * #stmt2' #fvs2' #u'' @refl 2860 2857  8: #k #k' #new_vars #Hsimcont #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ 2861 2858 lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') 2862 2859 #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl 2863 2860 %1{sss_lu … new_vars … sss_writeable} try // try assumption 2864 [ 1: destruct (sss_result_hyp) @refl 2865  2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] 2861 destruct (sss_result_hyp) @refl 2866 2862  9: #en #en' #r #f #k #k' #old_vars #new_vars #Hsimcont #Hnew_vars_eq #Hdisjoint_k #_ 2867 2863 #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ … … 2898 2894 try // try assumption 2899 2895 [ 1: @(fresh_for_Sskip … sss_lu_fresh) 2900  3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem2901 2896  2: #v #Hmem #vb #Hlookup lapply (sss_new_alloc v Hmem vb Hlookup) * * #Hvb #Hlow #Hhigh 2902 2897 cut (store_value_of_type' (typeof lhs) sss_m (\fst xl) (\fst xr) = Some ? m') … … 2962 2957  2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta 2963 2958 /2 by All_append_l/ 2964  4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem]2959 ] 2965 2960 @(swc_seq … u') try // 2966 2961 [ 2: >HeqB @refl … … 2985 2980  2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta 2986 2981 /2 by All_append_l/ 2987  3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem]2982 ] 2988 2983  2: %1{u' … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqB} try assumption try // 2989 2984 [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize #_ … … 2991 2986  2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta 2992 2987 /2 by All_append_r/ 2993  3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem] ]2988 ] ] 2994 2989  6: (* While loop *) 2995 2990 #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp … … 3005 3000 [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize // 3006 3001  2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H 3007  4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem3008 3002  3: @(swc_while … sss_lu) try // 3009 3003 [ 1: >HeqA @refl … … 3011 3005 ] 3012 3006  2: %{… sss_func_hyp … (switch_removal Sskip u')} try assumption try // 3013 [ 1:lapply (switch_removal_fte body sss_lu) >HeqA #Hfte whd in match (ret_u ??) in Hfte;3014 3015  2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]]3007 lapply (switch_removal_fte body sss_lu) >HeqA #Hfte whd in match (ret_u ??) in Hfte; 3008 @(fresher_for_univ … Hfte) @(fresh_for_Sskip … sss_lu_fresh) 3009 ] 3016 3010  7: (* do while loop *) 3017 3011 #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp … … 3024 3018  2: >HeqA @refl 3025 3019  3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H 3026  5: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem3027 3020  4: @(swc_dowhile … sss_lu) try assumption try // 3028 3021 [ 1: >HeqA @refl … … 3091 3084 ] 3092 3085  2: %1{u' … sss_func_hyp … (switch_removal Sskip u')} try assumption try // 3093 [ 1: @(fresh_for_Sskip … sss_lu_fresh) ] ] ] 3094 #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem 3086 @(fresh_for_Sskip … sss_lu_fresh) ] ] 3095 3087  9: (* break *) 3096 3088 (* sss_enclosing_label TODO : switch case *) … … 3122 3114 #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); 3123 3115 #Heq destruct (Heq) ] 3124 #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem3125 3116  10: (* continue *) 3126 3117 #Hexec %{0} whd whd in sss_result_hyp:(??%?); >sss_result_proj <sss_result_hyp normalize nodelta … … 3175 3166 #_ #Hnew_vars_eq #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); 3176 3167 #Heq destruct (Heq) ] 3177 #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem3178 3168  11: (* return *) 3179 3169 #Hexec %{0} whd whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec Hexec
Note: See TracChangeset
for help on using the changeset viewer.