Changeset 2428


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.

Location:
src
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r2391 r2428  
    461461  | Sswitch a sl ⇒
    462462      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    463       match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉
    464                    | _ ⇒ Wrong ??? (msg TypeMismatch)]
     463      match v with
     464      [ Vint sz n ⇒
     465        match typeof a with
     466        [ Tint sz' _ ⇒
     467          match sz_eq_dec sz sz' with
     468          [ inl _ ⇒
     469            ! sl' ← opt_to_io … (msg TypeMismatch) (select_switch sz n sl);
     470            ret ? 〈tr, State f (seq_of_labeled_statement sl') (Kswitch k) e m〉
     471          | _ ⇒ Wrong ??? (msg TypeMismatch)
     472          ]
     473        | _ ⇒ Wrong ??? (msg TypeMismatch)
     474        ]
     475      | _ ⇒ Wrong ??? (msg TypeMismatch)]
    465476  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
    466477  | Sgoto lbl ⇒
  • src/Clight/CexecComplete.ma

    r2391 r2428  
    429429    | #r #f' #env' #k' #H1 #H2 whd in ⊢ (??%?); >H2 @refl
    430430    ]
    431 | #f #e #s #k #env #m #sz #i #tr #H1 whd in ⊢ (??%?);
    432     >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     431| #f #e #sl #sl' #k #env #m #sz #sg #i #tr #H1 #H2 #H3 whd in ⊢ (??%?);
     432    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
     433    >H2 whd in ⊢ (??%?); @(dec_true … (sz_eq_dec … sz) (refl ??)) #SZ
     434    whd in ⊢ (??%?); >H3
    433435    @refl
    434436| #f #s #k #env #m *; #es >es @refl
  • src/Clight/CexecEquiv.ma

    r2391 r2428  
    522522  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @I
    523523  | 4,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
    524   | @err2_does_not_interact #x1 #x2 cases x1; //;
     524  | @err2_does_not_interact * // #x1 #x2 #x3 cases (typeof a) // #x4 #x5 whd nodelta in ⊢ (???%); cases (sz_eq_dec ??) // #x6 cases (select_switch ???) //
    525525  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5  @err_does_not_interact #x6 cases a;
    526526      [ @I | #x7 @err2_does_not_interact #x8 #x9 @I ]
  • src/Clight/CexecSound.ma

    r2391 r2428  
    428428    ]
    429429  | #ex #ls @res_bindIO2_OK * // #sz #n #tr #Hv
    430     @step_switch @(exec_expr_sound' … Hv)
     430    lapply (refl ? (typeof ex)) cases (typeof ex) in ⊢ (???% → %); // #sz' #sg #TY
     431    whd in ⊢ (?????%); cases (sz_eq_dec sz sz') // #SZ destruct (SZ)
     432    whd in ⊢ (?????%); @opt_bindIO_OK #ls' #LS
     433    @(step_switch … TY LS) @(exec_expr_sound' … Hv)
    431434  | #l #s' //
    432435  | #l whd in ⊢ (?????%); lapply (refl ? (find_label l (fn_body f) (call_cont k)));
  • src/Clight/Csem.ma

    r2395 r2428  
    576576
    577577(* * Selection of the appropriate case of a [switch], given the value [n]
    578   of the selector expression. *)
    579 (* FIXME: now that we have several sizes of integer, it isn't clear whether we
    580    should allow case labels to be of a different size to the switch expression. *)
     578  of the selector expression.  We fail if any of the cases has an integer of
     579  the wrong size.  (NB: ideally, we'd change the syntax so that there is only
     580  one size, but we're trying to keep the impact of changes on existing code
     581  down.) *)
     582
    581583let rec select_switch (sz:intsize) (n: BitVector (bitsize_of_intsize sz)) (sl: labeled_statements)
    582                        on sl : labeled_statements ≝
     584                       on sl : option labeled_statements ≝
    583585  match sl with
    584   [ LSdefault _ ⇒ sl
     586  [ LSdefault _ ⇒ Some ? sl
    585587  | LScase sz' c s sl' ⇒ intsize_eq_elim ? sz sz' ? n
    586                          (λn. if eq_bv ? c n then sl else select_switch sz' n sl') (select_switch sz n sl')
     588                         (λn. if eq_bv ? c n then Some ? sl else select_switch sz' n sl') (None ?)
    587589  ].
    588590
     
    11731175           E0 (Returnstate Vundef k (free_list m (blocks_of_env e)))
    11741176
    1175   | step_switch: ∀f,a,sl,k,e,m,sz,n,tr.
     1177  | step_switch: ∀f,a,sl,sl',k,e,m,sz,sg,n,tr.
    11761178      eval_expr ge e m a (Vint sz n) tr →
     1179      typeof a = Tint sz sg →
     1180      select_switch sz n sl = Some ? sl' →
    11771181      step ge (State f (Sswitch a sl) k e m)
    1178            tr (State f (seq_of_labeled_statement (select_switch ? n sl)) (Kswitch k) e m)
     1182           tr (State f (seq_of_labeled_statement sl') (Kswitch k) e m)
    11791183  | step_skip_break_switch: ∀f,x,k,e,m.
    11801184      x = Sskip ∨ x = Sbreak →
  • 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
  • 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
  • src/common/IOMonad.ma

    r2145 r2428  
    426426  on _E:eq (IO ???) ?? to eq (res ?) ??.
    427427
     428(* Similarly for opt *)
     429
     430lemma io_eq_to_opt : ∀O,I. ∀T:Type[0]. ∀e:option T. ∀m,v.
     431  opt_to_io … m e = Value O I T v →
     432  e = Some T v.
     433#O #I #T *
     434[ #m #v #E normalize in E; destruct
     435| #t #m #v #E normalize in E; destruct %
     436]
     437qed.
     438
     439coercion io_eq_from_opt :
     440  ∀O,I,T,e,m,v. ∀E:opt_to_io O I T m e = Value O I T v. e = Some T v ≝ io_eq_to_opt
     441  on _E:eq (IO ???) ?? to eq (option ?) ??.
     442
     443
     444
Note: See TracChangeset for help on using the changeset viewer.