Ignore:
Timestamp:
Nov 6, 2012, 12:02:13 PM (7 years ago)
Author:
campbell
Message:

Tighten requirements on switch statements in Clight to only give semantics
when the controlling expression's type and values match up and the cases'
labels make sense.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r2391 r2428  
    23312331] qed.
    23322332
    2333 lemma select_switch_commute : ∀sz,i,l.
    2334  select_switch sz i (simplify_ls l) = simplify_ls (select_switch sz i l).
    2335 #sz #i #l @(labeled_statements_ind … l)
     2333lemma select_switch_simplify_elim : ∀sz,i,l. ∀P:option labeled_statements → option labeled_statements → Prop.
     2334 (P (None ?) (None ?)) →
     2335 (∀l'. P (Some ? l') (Some ? (simplify_ls l'))) →
     2336 P (select_switch sz i l) (select_switch sz i (simplify_ls l)).
     2337#sz #i #l #P #NONE #SOME @(labeled_statements_ind … l)
    23362338[ 1: #default_statement //
    23372339| 2: #sz' #i' #s #tl #Hind
    2338      whd in match (simplify_ls ?) in ⊢ (??%?);
    2339      whd in match (select_switch ???) in ⊢ (??%%);
     2340     whd in match (simplify_ls ?);
     2341     whd in match (select_switch ???); whd in match (select_switch ???);
    23402342     cases (sz_eq_dec sz sz')
    23412343     [ 1: #Hsz_eq destruct >intsize_eq_elim_true >intsize_eq_elim_true
    2342            cases (eq_bv (bitsize_of_intsize sz') i' i) normalize nodelta
    2343            whd in match (simplify_ls ?) in ⊢ (???%);
    2344            [ 1: // | 2: @Hind ]
     2344           cases (eq_bv (bitsize_of_intsize sz') i' i) normalize nodelta //
    23452345     | 2: #Hneq >(intsize_eq_elim_false ? sz sz' ???? Hneq) >(intsize_eq_elim_false ? sz sz' ???? Hneq)
    2346           @Hind
     2346          @NONE
    23472347     ]
    23482348] qed.
     
    29312931                    cases (\fst a) normalize nodelta
    29322932                    [ 1,3,4,5: #a destruct (a) #b destruct (b)
    2933                     | 2: #sz #i whd in match (ret ??) in ⊢ (% → %); #Heq destruct (Heq)
     2933                    | 2: #sz #i <Htype_eq_cond cases (typeof cond)
     2934                      [ 1,3,4,5,6,7,8,9: normalize nodelta #a try #b try #c destruct]
     2935                      #sz' #sg normalize nodelta cases (sz_eq_dec sz sz')
     2936                      #SZ [2: normalize nodelta #E destruct ]
     2937                      normalize nodelta @select_switch_simplify_elim
     2938                      [ #H whd in H:(??%?); destruct ]
     2939                      #l' whd in ⊢ (??%? → ??(λ_.?(??%?)?));
     2940                      #Heq destruct (Heq)
    29342941                         %{(State (simplify_function f)
    2935                                   (seq_of_labeled_statement (select_switch sz i (simplify_ls switchcases)))
     2942                                  (seq_of_labeled_statement (simplify_ls l'))
    29362943                                  (Kswitch k') en m)} @conj
    29372944                         [ 1: //
    2938                          | 2: @(labeled_statements_ind … switchcases)
     2945                         | 2: @(labeled_statements_ind … l')
    29392946                              [ 1: #default_s
    29402947                                   whd in match (simplify_ls ?);
     
    29432950                                   %1 @cc_switch //
    29442951                              | 2: #sz' #i' #top_case #tail #Hind
    2945                                    cut ((seq_of_labeled_statement (select_switch sz i (simplify_ls (LScase sz' i' top_case tail))))
    2946                                          = (simplify_statement (seq_of_labeled_statement (select_switch sz i (LScase sz' i' top_case tail)))))
    2947                                    [ 1: >select_switch_commute >simplify_ls_commute @refl
    2948                                    | 2: #Hrewrite >Hrewrite
    2949                                         %1 @cc_switch //
    2950          ] ] ] ] ] ]
     2952                                   <simplify_ls_commute
     2953                                   %1 @cc_switch //
     2954         ] ] ] ] ]
    29512955    | 13: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
    29522956          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
Note: See TracChangeset for help on using the changeset viewer.