Changeset 2391 for src/Clight/Csem.ma


Ignore:
Timestamp:
Oct 9, 2012, 3:10:07 PM (8 years ago)
Author:
campbell
Message:

Revert "Put the post-loop cost label into the Clight while statement ..."
Rely on the Cminor to RTLabs stage ignoring Cminor skips instead.
This reverts commit 2353.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r2353 r2391  
    910910  | Kseq: statement -> cont -> cont
    911911       (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
    912   | Kwhile: expr -> statement → option costlabel -> cont -> cont
     912  | Kwhile: expr -> statement -> 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 l k => call_cont k
     932  | Kwhile e s 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 l =>
    986       find_label lbl s1 (Kwhile a s1 l k)
     985  | Swhile a s1 =>
     986      find_label lbl s1 (Kwhile a s1 k)
    987987  | Sdowhile a s1 =>
    988988      find_label lbl s1 (Kdowhile a s1 k)
     
    10351035].
    10361036
    1037 definition optional_cost : option costlabel → statement → statement ≝
    1038 λo,s. match o with [ Some cl ⇒ Scost cl s | None ⇒ s ].
    1039 
    10401037(* XXX: note that cost labels in exprs expose a particular eval order. *)
    10411038
     
    10901087           tr (State f s2 k e m)
    10911088
    1092   | step_while_false: ∀f,a,s,cl,k,e,m,v,tr.
     1089  | step_while_false: ∀f,a,s,k,e,m,v,tr.
    10931090      eval_expr ge e m a v tr →
    10941091      is_false v (typeof a) →
    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.
     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.
    10981095      eval_expr ge e m a v tr →
    10991096      is_true v (typeof a) →
    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.
     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.
    11031100      x = Sskip ∨ x = Scontinue →
    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)
     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)
    11091106
    11101107  | step_dowhile: ∀f,a,s,k,e,m.
Note: See TracChangeset for help on using the changeset viewer.