Changeset 2353 for src/Clight/label.ma


Ignore:
Timestamp:
Sep 26, 2012, 6:14:38 PM (7 years ago)
Author:
campbell
Message:

Put the post-loop cost label into the Clight while statement to get rid
of extra skips. (Soon to be followed by other loop constructs.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r2319 r2353  
    11include "Clight/Csyntax.ma".
     2
     3(* Label freedom *)
     4
     5let rec expr_label_free (e:expr) : bool ≝
     6match 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
     23let rec statement_label_free (s:statement) : bool ≝
     24match 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 ≝
     38match ls with
     39[ LSdefault s1 ⇒ statement_label_free s1
     40| LScase _ _ s1 ls1 ⇒ statement_label_free s1 ∧ labeled_statements_label_free ls1
     41].
     42
     43definition 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
     49definition clight_label_free : clight_program → bool ≝
     50λp. all ? clight_fundef_label_free (prog_funct ?? p).
     51
     52(* Adding labels *)
    253
    354definition add_cost_before : statement → universe CostTag → statement × (universe CostTag) ≝
     
    94145| Some e ⇒ let 〈e,costgen〉 ≝ label_expr e costgen in 〈Some ? e,costgen〉
    95146].
     147
     148definition 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  ].
    96154
    97155
     
    120178    let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in
    121179    〈Sifthenelse e s1 s2, costgen〉
    122 | Swhile e s'
     180| Swhile e s' cl
    123181    let 〈e,costgen〉 ≝ label_expr e costgen in
    124182    let 〈s',costgen〉 ≝ label_statement s' costgen in
    125183    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
    126     let 〈s,costgen〉 ≝ add_cost_after (Swhile e s') costgen in
    127     〈s,costgen〉
     184    let 〈after,costgen〉 ≝ ensure_label cl costgen in
     185    〈Swhile e s' (Some ? after), costgen〉
    128186| Sdowhile e s' ⇒
    129187    let 〈e,costgen〉 ≝ label_expr e costgen in
Note: See TracChangeset for help on using the changeset viewer.