Changeset 3044


Ignore:
Timestamp:
Mar 29, 2013, 8:16:50 PM (4 years ago)
Author:
campbell
Message:

Start showing combination of switch removal and labelling is OK.
Fix typo in switch removal statement.

Location:
src/Clight
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2734 r3044  
    27552755  exec_step ge s1 = Value … 〈tr,s2〉 → 
    27562756  ∃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').
    27582758#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state
    27592759inversion Hsim_state
     
    27982798         <sss_func_hyp
    27992799         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
    28022801    | 3: #cond #body #k #k' #fgen #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
    28032802         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
     
    28102809         | 3: whd in match (switch_removal ??);
    28112810              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         ]
    28132812    | 4: #cond #body #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
    28142813         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')   
     
    28252824              | 2: whd in match (switch_removal ??);
    28262825                   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              ]
    28282827         | 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         ]
    28312830    | 5: #cond #stmt1 #stmt2 #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_
    28322831         #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
     
    28342833         #Hexec_step %{0} whd whd in Hresult:(??%?) Hexec_step:(??%?); destruct (Hexec_step)
    28352834         @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
    28382836    | 6: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars
    28392837         #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
     
    28472845              whd in match (ret_vars ??); /2 by All_append_l/
    28482846         | 3: @(swc_for3 … u) //
    2849          | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
     2847         ]
    28502848    | 7: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars
    28512849         #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
     
    28542852         %1{u … new_vars … sss_writeable … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)}
    28552853         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
    28602857    | 8: #k #k' #new_vars #Hsimcont #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
    28612858         lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq')
    28622859         #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl
    28632860         %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
    28662862    | 9: #en #en' #r #f #k #k' #old_vars #new_vars #Hsimcont #Hnew_vars_eq #Hdisjoint_k #_
    28672863         #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_
     
    28982894       try // try assumption
    28992895       [ 1: @(fresh_for_Sskip … sss_lu_fresh)
    2900        | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
    29012896       | 2: #v #Hmem #vb #Hlookup lapply (sss_new_alloc v Hmem vb Hlookup) * * #Hvb #Hlow #Hhigh           
    29022897            cut (store_value_of_type' (typeof lhs) sss_m (\fst  xl) (\fst  xr) = Some ? m')
     
    29622957       | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta
    29632958            /2 by All_append_l/
    2964        | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
     2959       ]
    29652960       @(swc_seq … u') try //
    29662961       [ 2: >HeqB @refl
     
    29852980             | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta
    29862981                  /2 by All_append_l/
    2987              | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ]
     2982             ]
    29882983       | 2: %1{u' … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqB} try assumption try //
    29892984             [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize #_
     
    29912986             | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta
    29922987                  /2 by All_append_r/                   
    2993              | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ]
     2988             ] ]
    29942989  | 6: (* While loop *)
    29952990       #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp
     
    30053000             [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize //
    30063001             | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H
    3007              | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
    30083002             | 3: @(swc_while … sss_lu) try //
    30093003                  [ 1: >HeqA @refl
     
    30113005             ]
    30123006       | 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                  @(fresher_for_univ … Hfte) @(fresh_for_Sskip … sss_lu_fresh)
    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       ]
    30163010  | 7: (* do while loop *)
    30173011       #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp
     
    30243018       | 2: >HeqA @refl
    30253019       | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H
    3026        | 5: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
    30273020       | 4: @(swc_dowhile … sss_lu) try assumption try //
    30283021            [ 1: >HeqA @refl
     
    30913084                 ]
    30923085            | 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) ] ]
    30953087  | 9: (* break *)
    30963088       (* sss_enclosing_label TODO : switch case *)
     
    31223114            #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?));
    31233115            #Heq destruct (Heq) ]
    3124        #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
    31253116  | 10: (* continue *)
    31263117       #Hexec %{0} whd whd in sss_result_hyp:(??%?); >sss_result_proj <sss_result_hyp normalize nodelta
     
    31753166             #_ #Hnew_vars_eq #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?));
    31763167            #Heq destruct (Heq) ]
    3177        #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem
    31783168  | 11: (* return *)
    31793169        #Hexec %{0} whd whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec -Hexec
Note: See TracChangeset for help on using the changeset viewer.