Changeset 2326 for src/Clight/abstract.ma

Timestamp:

Sep 7, 2012, 12:15:51 PM (8 years ago)

Author:

campbell

Message:

More accurate notion of labelled states in Clight.

File:

• src/Clight/abstract.ma (modified) (1 diff)

src/Clight/abstract.ma

@@ -52 +52 @@
 (* Labelled states in Clight are a little tricky because there are cost labels
    in the expressions in addition to the cost statement.  Note that a labelled
-   state may produce several cost labels due to expressions. *)
+   state may produce several cost labels due to expressions, and that we should
+   only check the root of the statement because sub-statements will not be
+   executed until later.
+   
+   Also, a labelled state will only be guaranteed to generate a cost label in
+   the trace if the program is properly cost labelled - if it isn't then an
+   Econd might be used to with a cost label in only one branch.
+    *)
 
 definition expr_labelled : expr → bool ≝
 any_expr (λe. match e with [ Expr e _ ⇒ match e with [ Ecost _ _ ⇒ true | _ ⇒ false ] ]).
 
+definition statement_cont_labelled : statement → cont → bool ≝
+λs,k.
+match s with
+[ Sskip ⇒
+  match k with
+  [ Kdowhile e _ _ ⇒ expr_labelled e
+  | _ ⇒ false
+  ]
+| Sassign e1 e2 ⇒ expr_labelled e1 ∨ expr_labelled e2
+| Scall oe e es ⇒ (option_map_def … expr_labelled false oe) ∨ expr_labelled e ∨ all ? expr_labelled es
+| Ssequence _ _ ⇒ false
+| Sifthenelse e _ _ ⇒ expr_labelled e
+| Swhile e _ ⇒ expr_labelled e
+| Sdowhile e _ ⇒ false
+| Sfor s e _ _ ⇒ match s with [ Sskip ⇒ expr_labelled e | _ ⇒ false ]
+| Sbreak ⇒ false
+| Scontinue ⇒
+  match k with
+  [ Kdowhile e _ _ ⇒ expr_labelled e
+  | _ ⇒ false
+  ]
+| Sreturn oe ⇒ option_map_def … expr_labelled false oe
+| Sswitch e _ ⇒ expr_labelled e (* should not occur due to early switch removal *)
+| Slabel _ _ ⇒ false
+| Sgoto _ ⇒ false
+| Scost _ _ ⇒ true
+].
+
 definition Clight_labelled : state → bool ≝
 λs. match s with
-[ State f s k e m ⇒
-  any_statement (λs. match s with [ Scost _ _ ⇒ true | _ ⇒ any_expr_statement expr_labelled s ]) s
+[ State f s k e m ⇒ statement_cont_labelled s k
 | _ ⇒ false
 ].