Changeset 2428 for src/Clight/Csem.ma


Ignore:
Timestamp:
Nov 6, 2012, 12:02:13 PM (8 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/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 →
Note: See TracChangeset for help on using the changeset viewer.