Changeset 2399 for src/Clight/label.ma


Ignore:
Timestamp:
Oct 17, 2012, 6:45:20 PM (7 years ago)
Author:
campbell
Message:

Fill in some details about the statement of correctness.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r2392 r2399  
    11include "Clight/Csyntax.ma".
    22
    3 (* Label freedom *)
    4 
    5 let rec expr_label_free (e:expr) : bool ≝
     3(* Extract cost labels from a program. *)
     4
     5let rec labels_of_expr (e:expr) : list costlabel ≝
    66match e with
    77[ Expr e' _ ⇒
    88  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
     9  [ Ederef e1 ⇒ labels_of_expr e1
     10  | Eaddrof e1 ⇒ labels_of_expr e1
     11  | Eunop _ e1 ⇒ labels_of_expr e1
     12  | Ebinop _ e1 e2 ⇒ labels_of_expr e1 @ labels_of_expr e2
     13  | Ecast _ e1 ⇒ labels_of_expr e1
     14  | Econdition e1 e2 e3 ⇒ labels_of_expr e1 @ labels_of_expr e2 @ labels_of_expr e3
     15  | Eandbool e1 e2 ⇒ labels_of_expr e1 @ labels_of_expr e2
     16  | Eorbool e1 e2 ⇒ labels_of_expr e1 @ labels_of_expr e2
     17  | Efield e1 _ ⇒ labels_of_expr e1
     18  | Ecost cl e1 ⇒ cl::(labels_of_expr e1)
     19  | _ ⇒ [ ]
    2020  ]
    2121].
    2222
    23 let rec statement_label_free (s:statement) : bool ≝
     23let rec labels_of_statement (s:statement) : list costlabel ≝
    2424match 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 ⇒ expr_label_free e1 ∧ statement_label_free s1
    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 ≝
     25[ Sassign e1 e2 ⇒ labels_of_expr e1 @ labels_of_expr e2
     26| Scall oe e1 es ⇒ option_map_def … labels_of_expr [ ] oe @ labels_of_expr e1 @ foldl … (λls,e. labels_of_expr e @ ls) [ ] es
     27| Ssequence s1 s2 ⇒ labels_of_statement s1 @ labels_of_statement s2
     28| Sifthenelse e1 s1 s2 ⇒ labels_of_expr e1 @ labels_of_statement s1 @ labels_of_statement s2
     29| Swhile e1 s1 ⇒ labels_of_expr e1 @ labels_of_statement s1
     30| Sdowhile e1 s1 ⇒ labels_of_expr e1 @ labels_of_statement s1
     31| Sfor s1 e1 s2 s3 ⇒ labels_of_statement s1 @ labels_of_expr e1 @ labels_of_statement s2 @ labels_of_statement s3
     32| Sreturn oe ⇒ option_map_def … labels_of_expr [ ] oe
     33| Sswitch e1 ls ⇒ labels_of_expr e1 @ labels_of_labeled_statements ls
     34| Slabel _ s1 ⇒ labels_of_statement s1
     35| Scost cl s1 ⇒ cl::(labels_of_statement s1)
     36| _ ⇒ [ ]
     37] and labels_of_labeled_statements (ls:labeled_statements) : list costlabel ≝
    3838match 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 ≝
     39[ LSdefault s1 ⇒ labels_of_statement s1
     40| LScase _ _ s1 ls1 ⇒ labels_of_statement s1 @ labels_of_labeled_statements ls1
     41].
     42
     43definition labels_of_clight_fundef : ident × clight_fundef → list costlabel ≝
    4444λifd. match \snd ifd with
    45 [ CL_Internal f ⇒ statement_label_free (fn_body f)
    46 | _ ⇒ true
    47 ].
     45[ CL_Internal f ⇒ labels_of_statement (fn_body f)
     46| _ ⇒ [ ]
     47].
     48
     49definition labels_of_clight : clight_program → list costlabel ≝
     50λp. foldl … (λls,f. labels_of_clight_fundef f @ ls) [ ] (prog_funct ?? p).
     51
     52definition in_clight_program : clight_program → costlabel → Prop ≝
     53λp,l. Exists … (λx.x=l) (labels_of_clight p).
    4854
    4955definition clight_label_free : clight_program → bool ≝
    50 λp. all ? clight_fundef_label_free (prog_funct ?? p).
     56λp. match labels_of_clight p with [ nil ⇒ true | _ ⇒ false ].
    5157
    5258(* Adding labels *)
Note: See TracChangeset for help on using the changeset viewer.