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/labelSimulation.ma

    r2392 r2428  
    392392] qed.
    393393
    394 lemma label_select_ls : ∀sz,i,ls,u.
     394lemma label_select_ls : ∀sz,i,ls,ls',u.
     395    select_switch sz i ls = Some ? ls' →
    395396  ∃u'.
    396397    select_switch sz i (\fst (label_lstatements ls u)) =
    397     \fst (label_lstatements (select_switch sz i ls) u').
     398    Some ? (\fst (label_lstatements ls' u')).
    398399#sz #i #ls @(labeled_statements_ind … ls)
    399 [ #s #u % [2: whd in match (label_lstatements ??);
     400[ #s #ls' #u #S normalize in S; destruct
     401  % [2: whd in match (label_lstatements ??);
    400402  @label_gen_elim #u1 >shift_fst @refl | skip ]
    401 | #sz' #i' #s #tl #IH #u
    402   whd in match (label_lstatements ??);
    403   whd in match (select_switch ?? (LScase ????));
    404   @intsize_eq_elim_elim
    405   [ #NE
     403| #sz' #i' #s #tl #IH #ls' #u
     404  whd in ⊢ (??%? → ?); @intsize_eq_elim_elim [ #NE #E destruct ]
     405  #E destruct whd @eq_bv_elim
     406  [ #E' destruct #S whd in S:(??%%); destruct
     407    % [2: whd in match (label_lstatements ??);
    406408    @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
    407     cases (IH u2)
    408     #u4 #E %{u4} whd in ⊢ (??%?);
    409     >intsize_eq_elim_false //
    410   | #E <E in i' ⊢ %; #i' whd
    411     @eq_bv_elim
    412     [ #Ei >Ei
    413       %{u}
    414       whd in match (label_lstatements (if ? then ? else ?) ?);
    415       @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
    416       whd in ⊢ (??%?);
    417       >intsize_eq_elim_true
    418       >eq_bv_true
    419       @refl
    420     | #NEi
    421       @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
    422        whd in ⊢ (??(λ_.??%?));
    423        >intsize_eq_elim_true
    424        >eq_bv_false //
    425     ]
     409    whd in ⊢ (??%%); >intsize_eq_elim_true >eq_bv_true %
     410    | skip ]
     411  | #NE #S whd in S:(??%?);
     412    whd in match (label_lstatements ??); 
     413    @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
     414    whd in match (select_switch ?? (LScase ????));
     415    >intsize_eq_elim_true >(eq_bv_false … NE)
     416    @IH assumption
    426417  ]
    427418] qed.
     
    867858    | >label_function_return >Ety
    868859    ] whd in ⊢ (??%?); % /4/
    869   | #a #ls #EX
     860  | * #a #ty #ls #EX
    870861    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    871862    cases v1 in EX1 EX;
     
    873864    | *: normalize #A #B try #C destruct
    874865    ]
    875     whd in EX:(??%%); destruct
     866    whd in EX:(??%%); cases ty in EX1 EX ⊢ %; normalize nodelta #sz' try #sg try #EX1 try #EX destruct
     867    cases (sz_eq_dec sz sz') in EX; #SZ #EX whd in EX:(??%%); destruct
     868    cases (bindIO_inversion ??????? EX) -EX #ls' * #EXls #EX
     869    whd in EX:(??%%); destruct
    876870    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    877871    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
    878872    %{0} whd
    879     whd in ⊢ (??%?); >EX1' % //
    880     cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/
     873    whd in ⊢ (??%?); >EX1'
     874    whd in ⊢ (??%?); >label_expr_type
     875    whd in ⊢ (??%?); @(dec_true ? (sz_eq_dec sz' sz') (refl ??)) #SZ'
     876    whd in ⊢ (??%?); cases (label_select_ls ????? EXls)
     877    [ #u3 #Els' >Els' whd % /3/ | skip ]
    881878  | #l #st #EX
    882879    whd in EX:(??%?); destruct
     
    10051002  | @bindIO_res_interact #l #El @bindIO_res_interact #vt #Evt @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct
    10061003  | 4,7: @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 #EX whd in EX:(??%?); destruct
    1007   | @bindIO_res_interact * * normalize #A #B #C try #D try #E destruct
     1004  | @bindIO_res_interact * * normalize nodelta #A #B #C try #D try #E destruct
     1005    cases (typeof a) in E; normalize nodelta #E try #F try #G destruct
     1006    cases (sz_eq_dec A E) in G; normalize nodelta #G [2: #H destruct]
     1007    @bindIO_opt_interact #ls' #H #I normalize in I; destruct
    10081008  | @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 @bindIO_opt_interact #x5 #x6 @bindIO_res_interact #x7 #x8 cases a
    10091009      [ 2: #x9 @bindIO_res_interact #x10 #x11 ] #EX whd in EX:(??%?); destruct
Note: See TracChangeset for help on using the changeset viewer.