Changeset 2353 for src/Clight/Csem.ma


Ignore:
Timestamp:
Sep 26, 2012, 6:14:38 PM (7 years ago)
Author:
campbell
Message:

Put the post-loop cost label into the Clight while statement to get rid
of extra skips. (Soon to be followed by other loop constructs.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r2263 r2353  
    910910  | Kseq: statement -> cont -> cont
    911911       (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
    912   | Kwhile: expr -> statement -> cont -> cont
     912  | Kwhile: expr -> statement → option costlabel -> cont -> cont
    913913       (**r [Kwhile e s k] = after [s] in [while (e) s] *)
    914914  | Kdowhile: expr -> statement -> cont -> cont
     
    930930  match k with
    931931  [ Kseq s k => call_cont k
    932   | Kwhile e s k => call_cont k
     932  | Kwhile e s l k => call_cont k
    933933  | Kdowhile e s k => call_cont k
    934934  | Kfor2 e2 e3 s k => call_cont k
     
    983983      | None => find_label lbl s2 k
    984984      ]
    985   | Swhile a s1 =>
    986       find_label lbl s1 (Kwhile a s1 k)
     985  | Swhile a s1 l =>
     986      find_label lbl s1 (Kwhile a s1 l k)
    987987  | Sdowhile a s1 =>
    988988      find_label lbl s1 (Kdowhile a s1 k)
     
    10351035].
    10361036
     1037definition optional_cost : option costlabel → statement → statement ≝
     1038λo,s. match o with [ Some cl ⇒ Scost cl s | None ⇒ s ].
     1039
    10371040(* XXX: note that cost labels in exprs expose a particular eval order. *)
    10381041
     
    10871090           tr (State f s2 k e m)
    10881091
    1089   | step_while_false: ∀f,a,s,k,e,m,v,tr.
     1092  | step_while_false: ∀f,a,s,cl,k,e,m,v,tr.
    10901093      eval_expr ge e m a v tr →
    10911094      is_false v (typeof a) →
    1092       step ge (State f (Swhile a s) k e m)
    1093            tr (State f Sskip k e m)
    1094   | step_while_true: ∀f,a,s,k,e,m,v,tr.
     1095      step ge (State f (Swhile a s cl) k e m)
     1096           tr (State f (optional_cost cl Sskip) k e m)
     1097  | step_while_true: ∀f,a,s,cl,k,e,m,v,tr.
    10951098      eval_expr ge e m a v tr →
    10961099      is_true v (typeof a) →
    1097       step ge (State f (Swhile a s) k e m)
    1098            tr (State f s (Kwhile a s k) e m)
    1099   | step_skip_or_continue_while: ∀f,x,a,s,k,e,m.
     1100      step ge (State f (Swhile a s cl) k e m)
     1101           tr (State f s (Kwhile a s cl k) e m)
     1102  | step_skip_or_continue_while: ∀f,x,a,s,cl,k,e,m.
    11001103      x = Sskip ∨ x = Scontinue →
    1101       step ge (State f x (Kwhile a s k) e m)
    1102            E0 (State f (Swhile a s) k e m)
    1103   | step_break_while: ∀f,a,s,k,e,m.
    1104       step ge (State f Sbreak (Kwhile a s k) e m)
    1105            E0 (State f Sskip k e m)
     1104      step ge (State f x (Kwhile a s cl k) e m)
     1105           E0 (State f (Swhile a s cl) k e m)
     1106  | step_break_while: ∀f,a,s,cl,k,e,m.
     1107      step ge (State f Sbreak (Kwhile a s cl k) e m)
     1108           E0 (State f (optional_cost cl Sskip) k e m)
    11061109
    11071110  | step_dowhile: ∀f,a,s,k,e,m.
Note: See TracChangeset for help on using the changeset viewer.