 Timestamp:
 Sep 10, 2012, 6:18:56 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/abstract.ma
r2326 r2328 1 1 include "Clight/Csem.ma". 2 2 3 (* Definitions about Clight syntax and semantics for use in overall results. *) 4 5 let rec any_expr (P:expr → bool) (e:expr) on e : bool ≝ 6 P e ∨ 7 match e with [ Expr e _ ⇒ 8 match e with 9 [ Ederef e' ⇒ any_expr P e' 10  Eunop _ e' ⇒ any_expr P e' 11  Ebinop _ e1 e2 ⇒ any_expr P e1 ∨ any_expr P e2 12  Ecast _ e' ⇒ any_expr P e' 13  Econdition e1 e2 e3 ⇒ any_expr P e1 ∨ any_expr P e2 ∨ any_expr P e3 14  Eandbool e1 e2 ⇒ any_expr P e1 ∨ any_expr P e2 15  Eorbool e1 e2 ⇒ any_expr P e1 ∨ any_expr P e2 16  Efield e' _ ⇒ any_expr P e' 17  Ecost _ e' ⇒ any_expr P e' 18  _ ⇒ false 19 ] ]. 20 21 definition any_expr_statement : (expr → bool) → statement → bool ≝ 22 λP,s. 23 match s with 24 [ Sassign e1 e2 ⇒ P e1 ∨ P e2 25  Scall oe e es ⇒ (option_map_def … P false oe) ∨ P e ∨ all ? P es 26  Sifthenelse e _ _ ⇒ P e 27  Swhile e _ ⇒ P e 28  Sdowhile e _ ⇒ P e 29  Sfor _ e _ _ ⇒ P e 30  Sreturn oe ⇒ option_map_def … P false oe 31  _ ⇒ false 32 ]. 33 34 let rec any_statement (P:statement → bool) (s:statement) on s : bool ≝ 35 P s ∨ 36 match s with 37 [ Ssequence s1 s2 ⇒ any_statement P s1 ∨ any_statement P s2 38  Sifthenelse _ s1 s2 ⇒ any_statement P s1 ∨ any_statement P s2 39  Swhile _ s1 ⇒ any_statement P s1 40  Sdowhile _ s1 ⇒ any_statement P s1 41  Sfor s1 _ s2 s3 ⇒ any_statement P s1 ∨ any_statement P s2 ∨ any_statement P s3 42  Sswitch _ ls ⇒ any_labeled_statement P ls 43  Slabel _ s1 ⇒ any_statement P s1 44  Scost _ s1 ⇒ any_statement P s1 45  _ ⇒ false 46 ] and any_labeled_statement (P:statement → bool) (ls:labeled_statements) on ls : bool ≝ 47 match ls with 48 [ LSdefault s ⇒ any_statement P s 49  LScase _ _ s ls' ⇒ any_statement P s ∨ any_labeled_statement P ls' 50 ]. 51 52 (* Labelled states in Clight are a little tricky because there are cost labels 53 in the expressions in addition to the cost statement. Note that a labelled 54 state may produce several cost labels due to expressions, and that we should 55 only check the root of the statement because substatements will not be 56 executed until later. 3 (* I previously had a complicated definition that said a labelled Clight state 4 was one with a syntactic form that would emit a cost label in the trace when 5 the next step is evaluated. This is the wrong notion. 57 6 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 *) 62 63 definition expr_labelled : expr → bool ≝ 64 any_expr (λe. match e with [ Expr e _ ⇒ match e with [ Ecost _ _ ⇒ true  _ ⇒ false ] ]). 65 66 definition statement_cont_labelled : statement → cont → bool ≝ 67 λs,k. 68 match 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 ]. 7 We want a labelled Clight state to indicate that we can measure the time of 8 some correspondingly labelled machine code from there. Only explicit 9 statement level cost labels are useful for this. Cost labels that appear 10 in the middle of expressions are only useful for allowing the amount of time 11 measured to differ. 12 13 (Otherwise you see something silly like "x=(y1) ? c1: 1 : c2: z;" as a 14 labelled state, even though the labels c1 and c2 will appear in the *middle* 15 of the corresponding machine code, and so you measure the wrong thing and 16 can't prove it.) 17 *) 93 18 94 19 definition Clight_labelled : state → bool ≝ 95 20 λs. match s with 96 [ State f s k e m ⇒ statement_cont_labelled s k21 [ State f s k e m ⇒ match s with [ Scost _ _ ⇒ true  _ ⇒ false ] 97 22  _ ⇒ false 98 23 ].
Note: See TracChangeset
for help on using the changeset viewer.