Changeset 2326


Ignore:
Timestamp:
Sep 7, 2012, 12:15:51 PM (7 years ago)
Author:
campbell
Message:

More accurate notion of labelled states in Clight.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/abstract.ma

    r2325 r2326  
    5252(* Labelled states in Clight are a little tricky because there are cost labels
    5353   in the expressions in addition to the cost statement.  Note that a labelled
    54    state may produce several cost labels due to expressions. *)
     54   state may produce several cost labels due to expressions, and that we should
     55   only check the root of the statement because sub-statements will not be
     56   executed until later.
     57   
     58   Also, a labelled state will only be guaranteed to generate a cost label in
     59   the trace if the program is properly cost labelled - if it isn't then an
     60   Econd might be used to with a cost label in only one branch.
     61    *)
    5562
    5663definition expr_labelled : expr → bool ≝
    5764any_expr (λe. match e with [ Expr e _ ⇒ match e with [ Ecost _ _ ⇒ true | _ ⇒ false ] ]).
    5865
     66definition statement_cont_labelled : statement → cont → bool ≝
     67λs,k.
     68match s with
     69[ Sskip ⇒
     70  match k with
     71  [ Kdowhile e _ _ ⇒ expr_labelled e
     72  | _ ⇒ false
     73  ]
     74| Sassign e1 e2 ⇒ expr_labelled e1 ∨ expr_labelled e2
     75| Scall oe e es ⇒ (option_map_def … expr_labelled false oe) ∨ expr_labelled e ∨ all ? expr_labelled es
     76| Ssequence _ _ ⇒ false
     77| Sifthenelse e _ _ ⇒ expr_labelled e
     78| Swhile e _ ⇒ expr_labelled e
     79| Sdowhile e _ ⇒ false
     80| Sfor s e _ _ ⇒ match s with [ Sskip ⇒ expr_labelled e | _ ⇒ false ]
     81| Sbreak ⇒ false
     82| Scontinue ⇒
     83  match k with
     84  [ Kdowhile e _ _ ⇒ expr_labelled e
     85  | _ ⇒ false
     86  ]
     87| Sreturn oe ⇒ option_map_def … expr_labelled false oe
     88| Sswitch e _ ⇒ expr_labelled e (* should not occur due to early switch removal *)
     89| Slabel _ _ ⇒ false
     90| Sgoto _ ⇒ false
     91| Scost _ _ ⇒ true
     92].
     93
    5994definition Clight_labelled : state → bool ≝
    6095λs. match s with
    61 [ State f s k e m ⇒
    62   any_statement (λs. match s with [ Scost _ _ ⇒ true | _ ⇒ any_expr_statement expr_labelled s ]) s
     96[ State f s k e m ⇒ statement_cont_labelled s k
    6397| _ ⇒ false
    6498].
Note: See TracChangeset for help on using the changeset viewer.