Changeset 2353 for src/Clight/label.ma
- Timestamp:
- Sep 26, 2012, 6:14:38 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/label.ma
r2319 r2353 1 1 include "Clight/Csyntax.ma". 2 3 (* Label freedom *) 4 5 let rec expr_label_free (e:expr) : bool ≝ 6 match e with 7 [ Expr e' _ ⇒ 8 match e' with 9 [ Ederef e1 ⇒ expr_label_free e1 10 | Eaddrof e1 ⇒ expr_label_free e1 11 | Eunop _ e1 ⇒ expr_label_free e1 12 | Ebinop _ e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2 13 | Ecast _ e1 ⇒ expr_label_free e1 14 | Econdition e1 e2 e3 ⇒ expr_label_free e1 ∧ expr_label_free e2 ∧ expr_label_free e3 15 | Eandbool e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2 16 | Eorbool e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2 17 | Efield e1 _ ⇒ expr_label_free e1 18 | Ecost _ _ ⇒ false 19 | _ ⇒ true 20 ] 21 ]. 22 23 let rec statement_label_free (s:statement) : bool ≝ 24 match s with 25 [ Sassign e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2 26 | Scall oe e1 es ⇒ option_map_def … expr_label_free true oe ∧ expr_label_free e1 ∧ all … expr_label_free es 27 | Ssequence s1 s2 ⇒ statement_label_free s1 ∧ statement_label_free s2 28 | Sifthenelse e1 s1 s2 ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ statement_label_free s2 29 | Swhile e1 s1 cl ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ match cl with [ None ⇒ true | _ ⇒ false ] 30 | Sdowhile e1 s1 ⇒ expr_label_free e1 ∧ statement_label_free s1 31 | Sfor s1 e1 s2 s3 ⇒ statement_label_free s1 ∧ expr_label_free e1 ∧ statement_label_free s2 ∧ statement_label_free s3 32 | Sreturn oe ⇒ option_map_def … expr_label_free true oe 33 | Sswitch e1 ls ⇒ expr_label_free e1 ∧ labeled_statements_label_free ls 34 | Slabel _ s1 ⇒ statement_label_free s1 35 | Scost _ _ ⇒ false 36 | _ ⇒ true 37 ] and labeled_statements_label_free (ls:labeled_statements) : bool ≝ 38 match ls with 39 [ LSdefault s1 ⇒ statement_label_free s1 40 | LScase _ _ s1 ls1 ⇒ statement_label_free s1 ∧ labeled_statements_label_free ls1 41 ]. 42 43 definition clight_fundef_label_free : ident × clight_fundef → bool ≝ 44 λifd. match \snd ifd with 45 [ CL_Internal f ⇒ statement_label_free (fn_body f) 46 | _ ⇒ true 47 ]. 48 49 definition clight_label_free : clight_program → bool ≝ 50 λp. all ? clight_fundef_label_free (prog_funct ?? p). 51 52 (* Adding labels *) 2 53 3 54 definition add_cost_before : statement → universe CostTag → statement × (universe CostTag) ≝ … … 94 145 | Some e ⇒ let 〈e,costgen〉 ≝ label_expr e costgen in 〈Some ? e,costgen〉 95 146 ]. 147 148 definition ensure_label : option costlabel → universe CostTag → costlabel × (universe CostTag) ≝ 149 λo,u. 150 match o with 151 [ Some cl ⇒ 〈cl,u〉 152 | None ⇒ fresh … u 153 ]. 96 154 97 155 … … 120 178 let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in 121 179 〈Sifthenelse e s1 s2, costgen〉 122 | Swhile e s' ⇒180 | Swhile e s' cl ⇒ 123 181 let 〈e,costgen〉 ≝ label_expr e costgen in 124 182 let 〈s',costgen〉 ≝ label_statement s' costgen in 125 183 let 〈s',costgen〉 ≝ add_cost_before s' costgen in 126 let 〈 s,costgen〉 ≝ add_cost_after (Swhile e s')costgen in127 〈 s,costgen〉184 let 〈after,costgen〉 ≝ ensure_label cl costgen in 185 〈Swhile e s' (Some ? after), costgen〉 128 186 | Sdowhile e s' ⇒ 129 187 let 〈e,costgen〉 ≝ label_expr e costgen in
Note: See TracChangeset
for help on using the changeset viewer.