Changeset 2353 for src/Clight/label.ma

Timestamp:

Sep 26, 2012, 6:14:38 PM (8 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:

• src/Clight/label.ma (modified) (3 diffs)

src/Clight/label.ma

@@ -1 +1 @@
 include "Clight/Csyntax.ma".
+
+(* Label freedom *)
+
+let rec expr_label_free (e:expr) : bool ≝
+match e with
+[ Expr e' _ ⇒
+  match e' with
+  [ Ederef e1 ⇒ expr_label_free e1
+  | Eaddrof e1 ⇒ expr_label_free e1
+  | Eunop _ e1 ⇒ expr_label_free e1
+  | Ebinop _ e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2
+  | Ecast _ e1 ⇒ expr_label_free e1
+  | Econdition e1 e2 e3 ⇒ expr_label_free e1 ∧ expr_label_free e2 ∧ expr_label_free e3
+  | Eandbool e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2
+  | Eorbool e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2
+  | Efield e1 _ ⇒ expr_label_free e1
+  | Ecost _ _ ⇒ false
+  | _ ⇒ true
+  ]
+].
+
+let rec statement_label_free (s:statement) : bool ≝
+match s with
+[ Sassign e1 e2 ⇒ expr_label_free e1 ∧ expr_label_free e2
+| Scall oe e1 es ⇒ option_map_def … expr_label_free true oe ∧ expr_label_free e1 ∧ all … expr_label_free es
+| Ssequence s1 s2 ⇒ statement_label_free s1 ∧ statement_label_free s2
+| Sifthenelse e1 s1 s2 ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ statement_label_free s2
+| Swhile e1 s1 cl ⇒ expr_label_free e1 ∧ statement_label_free s1 ∧ match cl with [ None ⇒ true | _ ⇒ false ]
+| Sdowhile e1 s1 ⇒ expr_label_free e1 ∧ statement_label_free s1
+| Sfor s1 e1 s2 s3 ⇒ statement_label_free s1 ∧ expr_label_free e1 ∧ statement_label_free s2 ∧ statement_label_free s3
+| Sreturn oe ⇒ option_map_def … expr_label_free true oe
+| Sswitch e1 ls ⇒ expr_label_free e1 ∧ labeled_statements_label_free ls
+| Slabel _ s1 ⇒ statement_label_free s1
+| Scost _ _ ⇒ false
+| _ ⇒ true
+] and labeled_statements_label_free (ls:labeled_statements) : bool ≝
+match ls with
+[ LSdefault s1 ⇒ statement_label_free s1
+| LScase _ _ s1 ls1 ⇒ statement_label_free s1 ∧ labeled_statements_label_free ls1
+].
+
+definition clight_fundef_label_free : ident × clight_fundef → bool ≝
+λifd. match \snd ifd with
+[ CL_Internal f ⇒ statement_label_free (fn_body f)
+| _ ⇒ true
+].
+
+definition clight_label_free : clight_program → bool ≝
+λp. all ? clight_fundef_label_free (prog_funct ?? p).
+
+(* Adding labels *)
 
 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〉
 ].
+
+definition ensure_label : option costlabel → universe CostTag → costlabel × (universe CostTag) ≝
+λo,u.
+  match o with
+  [ Some cl ⇒ 〈cl,u〉
+  | None ⇒ fresh … u
+  ].
 
 
@@ -120 +178 @@
     let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in
     〈Sifthenelse e s1 s2, costgen〉
-| Swhile e s' ⇒
+| Swhile e s' cl ⇒
     let 〈e,costgen〉 ≝ label_expr e costgen in 
     let 〈s',costgen〉 ≝ label_statement s' costgen in
     let 〈s',costgen〉 ≝ add_cost_before s' costgen in
-    let 〈s,costgen〉 ≝ add_cost_after (Swhile e s') costgen in
-    〈s,costgen〉
+    let 〈after,costgen〉 ≝ ensure_label cl costgen in
+    〈Swhile e s' (Some ? after), costgen〉
 | Sdowhile e s' ⇒
     let 〈e,costgen〉 ≝ label_expr e costgen in