Changeset 2328

Ignore:
Timestamp:
Sep 10, 2012, 6:18:56 PM (7 years ago)
Message:

Cut down the notion of a Clight labelled state to those where we pick out
the cost label, rather than allowing it to appear in the middle of some
complex computation.

File:
1 edited

Unmodified
Removed
• src/Clight/abstract.ma

 r2326 include "Clight/Csem.ma". (* Definitions about Clight syntax and semantics for use in overall results. *) let rec any_expr (P:expr → bool) (e:expr) on e : bool ≝ P e ∨ match e with [ Expr e _ ⇒ match e with [ Ederef e' ⇒ any_expr P e' | Eunop _ e' ⇒ any_expr P e' | Ebinop _ e1 e2 ⇒ any_expr P e1 ∨ any_expr P e2 | Ecast _ e' ⇒ any_expr P e' | Econdition e1 e2 e3 ⇒ any_expr P e1 ∨ any_expr P e2 ∨ any_expr P e3 | Eandbool e1 e2 ⇒ any_expr P e1 ∨ any_expr P e2 | Eorbool e1 e2 ⇒ any_expr P e1 ∨ any_expr P e2 | Efield e' _ ⇒ any_expr P e' | Ecost _ e' ⇒ any_expr P e' | _ ⇒ false ] ]. definition any_expr_statement : (expr → bool) → statement → bool ≝ λP,s. match s with [ Sassign e1 e2 ⇒ P e1 ∨ P e2 | Scall oe e es ⇒ (option_map_def … P false oe) ∨ P e ∨ all ? P es | Sifthenelse e _ _ ⇒ P e | Swhile e _ ⇒ P e | Sdowhile e _ ⇒ P e | Sfor _ e _ _ ⇒ P e | Sreturn oe ⇒ option_map_def … P false oe | _ ⇒ false ]. let rec any_statement (P:statement → bool) (s:statement) on s : bool ≝ P s ∨ match s with [ Ssequence s1 s2 ⇒ any_statement P s1 ∨ any_statement P s2 | Sifthenelse _ s1 s2 ⇒ any_statement P s1 ∨ any_statement P s2 | Swhile _ s1 ⇒ any_statement P s1 | Sdowhile _ s1 ⇒ any_statement P s1 | Sfor s1 _ s2 s3 ⇒ any_statement P s1 ∨ any_statement P s2 ∨ any_statement P s3 | Sswitch _ ls ⇒ any_labeled_statement P ls | Slabel _ s1 ⇒ any_statement P s1 | Scost _ s1 ⇒ any_statement P s1 | _ ⇒ false ] and any_labeled_statement (P:statement → bool) (ls:labeled_statements) on ls : bool ≝ match ls with [ LSdefault s ⇒ any_statement P s | LScase _ _ s ls' ⇒ any_statement P s ∨ any_labeled_statement P ls' ]. (* 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, and that we should only check the root of the statement because sub-statements will not be executed until later. (* I previously had a complicated definition that said a labelled Clight state was one with a syntactic form that would emit a cost label in the trace when the next step is evaluated.  This is the wrong notion. 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 ]. We want a labelled Clight state to indicate that we can measure the time of some correspondingly labelled machine code from there.  Only explicit statement level cost labels are useful for this.  Cost labels that appear in the middle of expressions are only useful for allowing the amount of time measured to differ. (Otherwise you see something silly like "x=(y-1) ? c1: 1 : c2: z;" as a labelled state, even though the labels c1 and c2 will appear in the *middle* of the corresponding machine code, and so you measure the wrong thing and can't prove it.) *) definition Clight_labelled : state → bool ≝ λs. match s with [ State f s k e m ⇒ statement_cont_labelled s k [ State f s k e m ⇒ match s with [ Scost _ _ ⇒ true | _ ⇒ false ] | _ ⇒ false ].
Note: See TracChangeset for help on using the changeset viewer.