source: src/Clight/label.ma

Last change on this file was 3030, checked in by campbell, 7 years ago

Break up front-end for correctness proof.
Use let rec to prevent labelling function from unfolding.

File size: 11.9 KB
RevLine 
[781]1include "Clight/Csyntax.ma".
2
[2399]3(* Extract cost labels from a program. *)
[2353]4
[2399]5let rec labels_of_expr (e:expr) : list costlabel ≝
[2353]6match e with
7[ Expr e' _ ⇒
8  match e' with
[2399]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  | _ ⇒ [ ]
[2353]20  ]
21].
22
[2399]23let rec labels_of_statement (s:statement) : list costlabel ≝
[2353]24match s with
[2399]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 ≝
[2353]38match ls with
[2399]39[ LSdefault s1 ⇒ labels_of_statement s1
40| LScase _ _ s1 ls1 ⇒ labels_of_statement s1 @ labels_of_labeled_statements ls1
[2353]41].
42
[2399]43definition labels_of_clight_fundef : ident × clight_fundef → list costlabel ≝
[2353]44λifd. match \snd ifd with
[2399]45[ CL_Internal f ⇒ labels_of_statement (fn_body f)
46| _ ⇒ [ ]
[2353]47].
48
[2399]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).
54
[2505]55definition in_clight_label ≝
56  λp. Σl. in_clight_program p l.
57
[3021]58(* Providing these proofs isn't easy, and doesn't seem to have any benefit, so
59   let's stick with a simpler form.
[2505]60definition clight_cost_map ≝
61  λp. (in_clight_label p) → ℕ.
[3021]62*)
[2505]63
[3021]64definition clight_cost_map ≝ costlabel → ℕ.
65
[2353]66definition clight_label_free : clight_program → bool ≝
[2399]67λp. match labels_of_clight p with [ nil ⇒ true | _ ⇒ false ].
[2353]68
69(* Adding labels *)
70
[1056]71definition add_cost_before : statement → universe CostTag → statement × (universe CostTag) ≝
[781]72λs,gen.
[1056]73  let 〈l,gen〉 ≝ fresh … gen in
74  〈Scost l s, gen〉.
[781]75
[1056]76definition add_cost_after : statement → universe CostTag → statement × (universe CostTag) ≝
[781]77λs,gen.
[1056]78  let 〈l,gen〉 ≝ fresh … gen in
79  〈Ssequence s (Scost l Sskip), gen〉.
[781]80
[1056]81definition add_cost_expr : expr → universe CostTag → expr × (universe CostTag) ≝
[781]82λe,gen.
[1056]83  let 〈l,gen〉 ≝ fresh … gen in
84  〈Expr (Ecost l e) (typeof e), gen〉.
[781]85
[2588]86definition const_int : intsize → nat → expr ≝
87λsz,n. Expr (Econst_int ? (repr sz n)) (Tint sz Signed).
[1888]88
[781]89let rec label_expr (e:expr) (costgen:universe CostTag)
[1056]90        on e : expr × (universe CostTag) ≝
[781]91match e with
[1888]92[ Expr ed ty ⇒ let 〈ed,costgen〉 ≝ label_expr_descr ed costgen ty in
[1056]93               〈Expr ed ty, costgen〉
[781]94]
[1888]95and label_expr_descr (e:expr_descr) (costgen:universe CostTag) (ty:type)
[1056]96    on e : expr_descr × (universe CostTag) ≝
[781]97match e with
98[ Ederef e' ⇒
[1056]99    let 〈e',costgen〉 ≝ label_expr e' costgen in
100    〈Ederef e', costgen〉
[781]101| Eaddrof e' ⇒
[1056]102    let 〈e',costgen〉 ≝ label_expr e' costgen in
103    〈Eaddrof e', costgen〉
[781]104| Eunop op e' ⇒
[1056]105    let 〈e',costgen〉 ≝ label_expr e' costgen in
106    〈Eunop op e', costgen〉
[781]107| Ebinop op e1 e2 ⇒
[1056]108    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
109    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
110    〈Ebinop op e1 e2, costgen〉
[781]111| Ecast ty e' ⇒
[1056]112    let 〈e',costgen〉 ≝ label_expr e' costgen in
113    〈Ecast ty e', costgen〉
[781]114| Econdition e' e1 e2 ⇒
[1056]115    let 〈e',costgen〉 ≝ label_expr e' costgen in
116    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
117    let 〈e1,costgen〉 ≝ add_cost_expr e1 costgen in
118    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
119    let 〈e2,costgen〉 ≝ add_cost_expr e2 costgen in
120    〈Econdition e' e1 e2, costgen〉
[781]121(* andbool and orbool are changed to conditionals to capture their
[2392]122   short-circuiting cost difference; note that we have to return 0 or 1, and
123   we get rather more cost labels than I'd like *)
[781]124| Eandbool e1 e2 ⇒
[1056]125    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
[2588]126    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
127    match ty with
128    [ Tint sz sg ⇒
129      let 〈et,costgen〉 ≝ add_cost_expr (const_int sz 1) costgen in
130      let 〈ef,costgen〉 ≝ add_cost_expr (const_int sz 0) costgen in
131      let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
132      let 〈ef,costgen〉 ≝ add_cost_expr (const_int sz 0) costgen in
133      〈Econdition e1 e2 ef, costgen〉
134    | _ ⇒ (* default on 32 bit consts if inconsistent type. *)
135      let 〈et,costgen〉 ≝ add_cost_expr (const_int I32 1) costgen in
136      let 〈ef,costgen〉 ≝ add_cost_expr (const_int I32 0) costgen in
137      let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
138      let 〈ef,costgen〉 ≝ add_cost_expr (const_int I32 0) costgen in
139      〈Econdition e1 e2 ef, costgen〉       
140    ]
[781]141| Eorbool e1 e2 ⇒
[1056]142    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
[2392]143    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
[2588]144    match ty with
145    [ Tint sz sg ⇒   
146      let 〈et,costgen〉 ≝ add_cost_expr (const_int sz 1) costgen in
147      let 〈ef,costgen〉 ≝ add_cost_expr (const_int sz 0) costgen in
148      let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
149      let 〈et,costgen〉 ≝ add_cost_expr (const_int sz 1) costgen in
150      〈Econdition e1 et e2, costgen〉
151    | _ ⇒
152      let 〈et,costgen〉 ≝ add_cost_expr (const_int I32 1) costgen in
153      let 〈ef,costgen〉 ≝ add_cost_expr (const_int I32 0) costgen in
154      let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
155      let 〈et,costgen〉 ≝ add_cost_expr (const_int I32 1) costgen in
156      〈Econdition e1 et e2, costgen〉
157    ]
[781]158| Efield e' id ⇒
[1056]159    let 〈e',costgen〉 ≝ label_expr e' costgen in
160    〈Efield e' id, costgen〉
[781]161(* The prototype asserts on preexisting cost labels, but I'd quite like to
162   keep them. *)
163| Ecost l e' ⇒
[1056]164    let 〈e',costgen〉 ≝ label_expr e' costgen in
165    〈Ecost l e', costgen〉
[781]166
167(* The remaining expressions don't have subexpressions. *)
[1056]168| _ ⇒ 〈e,costgen〉
[781]169].
170
171let rec label_exprs (l:list expr) (costgen:universe CostTag)
[1056]172        on l : list expr × (universe CostTag) ≝
[781]173match l with
[1056]174[ nil ⇒ 〈nil ?,costgen〉
[781]175| cons e es ⇒
[1056]176    let 〈e,costgen〉 ≝ label_expr e costgen in
177    let 〈es,costgen〉 ≝ label_exprs es costgen in
178    〈e::es,costgen〉
[781]179].
180
181definition label_opt_expr ≝
182λoe,costgen. match oe with
[1056]183[ None ⇒ 〈None ?, costgen〉
184| Some e ⇒ let 〈e,costgen〉 ≝ label_expr e costgen in 〈Some ? e,costgen〉
[781]185].
186
187
188let rec label_statement (s:statement) (costgen:universe CostTag)
[1056]189        on s : statement × (universe CostTag) ≝
[781]190match s with
[1056]191[ Sskip ⇒ 〈Sskip,costgen〉
[781]192| Sassign e1 e2 ⇒
[1056]193    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
194    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
195    〈Sassign e1 e2, costgen〉
[781]196| Scall e_ret e_fn e_args ⇒
[1056]197    let 〈e_ret,costgen〉 ≝ label_opt_expr e_ret costgen in
198    let 〈e_fn,costgen〉 ≝ label_expr e_fn costgen in
199    let 〈e_args,costgen〉 ≝ label_exprs e_args costgen in
200    〈Scall e_ret e_fn e_args, costgen〉
[781]201| Ssequence s1 s2 ⇒
[1056]202    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
203    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
204    〈Ssequence s1 s2, costgen〉
[781]205| Sifthenelse e s1 s2 ⇒
[1056]206    let 〈e,costgen〉 ≝ label_expr e costgen in
207    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
208    let 〈s1,costgen〉 ≝ add_cost_before s1 costgen in
209    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
210    let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in
211    〈Sifthenelse e s1 s2, costgen〉
[2391]212| Swhile e s' ⇒
[1056]213    let 〈e,costgen〉 ≝ label_expr e costgen in
214    let 〈s',costgen〉 ≝ label_statement s' costgen in
215    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
[2391]216    let 〈s,costgen〉 ≝ add_cost_after (Swhile e s') costgen in
217    〈s,costgen〉
[781]218| Sdowhile e s' ⇒
[1056]219    let 〈e,costgen〉 ≝ label_expr e costgen in
220    let 〈s',costgen〉 ≝ label_statement s' costgen in
221    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
222    let 〈s,costgen〉 ≝ add_cost_after (Sdowhile e s') costgen in
223    〈s,costgen〉
[781]224| Sfor s1 e s2 s3 ⇒
[1056]225    let 〈e,costgen〉 ≝ label_expr e costgen in
226    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
227    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
228    let 〈s3,costgen〉 ≝ label_statement s3 costgen in
229    let 〈s3,costgen〉 ≝ add_cost_before s3 costgen in
230    let 〈s,costgen〉 ≝ add_cost_after (Sfor s1 e s2 s3) costgen in
231    〈s,costgen〉
232| Sbreak ⇒ 〈Sbreak,costgen〉
233| Scontinue ⇒ 〈Scontinue,costgen〉
[781]234| Sreturn opt_e ⇒
[1056]235    let 〈opt_e,costgen〉 ≝ label_opt_expr opt_e costgen in
236    〈Sreturn opt_e,costgen〉
[781]237| Sswitch e ls ⇒
[1056]238    let 〈e,costgen〉 ≝ label_expr e costgen in
239    let 〈ls,costgen〉 ≝ label_lstatements ls costgen in
240    〈Sswitch e ls, costgen〉
[781]241| Slabel l s' ⇒
[1056]242    let 〈s',costgen〉 ≝ label_statement s' costgen in
243    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
244    〈Slabel l s', costgen〉
245| Sgoto l ⇒ 〈Sgoto l, costgen〉
[781]246
247(* The prototype asserts on preexisting cost labels, but I'd quite like to
248   keep them. *)
249| Scost l s' ⇒
[1056]250    let 〈s',costgen〉 ≝ label_statement s' costgen in
251    〈Scost l s', costgen〉
[781]252]
253and label_lstatements (ls:labeled_statements) (costgen:universe CostTag)
[1056]254        on ls : labeled_statements × (universe CostTag) ≝
[781]255match ls with
256[ LSdefault s ⇒
[1056]257    let 〈s,costgen〉 ≝ label_statement s costgen in
258    let 〈s,costgen〉 ≝ add_cost_before s costgen in
259    〈LSdefault s, costgen〉
[961]260| LScase sz i s ls' ⇒
[1056]261    let 〈s,costgen〉 ≝ label_statement s costgen in
262    let 〈s,costgen〉 ≝ add_cost_before s costgen in
263    let 〈ls',costgen〉 ≝ label_lstatements ls' costgen in
264    〈LScase sz i s ls', costgen〉
[781]265].
266
[2319]267definition label_function : universe CostTag → function → function × (universe CostTag) ≝
268λcostgen,f.
[1056]269  let 〈body,costgen〉 ≝ label_statement (fn_body f) costgen in
270  let 〈body,costgen〉 ≝ add_cost_before body costgen in
[2319]271    〈mk_function (fn_return f) (fn_params f) (fn_vars f) body, costgen〉.
[781]272
[2319]273definition label_fundef : universe CostTag → clight_fundef → clight_fundef × (universe CostTag) ≝
274λgen,f. match f with
275[ CL_Internal f ⇒
276    let 〈f',gen'〉 ≝ label_function gen f in
277    〈CL_Internal f', gen'〉
278| CL_External id args ty ⇒ 〈CL_External id args ty, gen〉
[781]279].
280
[2319]281
[3030]282(* Use a let rec to prevent premature unfolding in correctness.ma. *)
[2319]283
[3030]284let rec clight_label (p:clight_program) : clight_program × costlabel ≝
[2319]285  let costgen ≝ new_universe CostTag in
286  let 〈init_cost, costgen〉 ≝ fresh … costgen in
287  〈\fst (transform_program_gen … costgen p (λ_.label_fundef)), init_cost〉.
[3030]288
289
290lemma unfold_clight_label : ∀p.
291  clight_label p =
292  (let costgen ≝ new_universe CostTag in
293  let 〈init_cost, costgen〉 ≝ fresh … costgen in
294  〈\fst (transform_program_gen … costgen p (λ_.label_fundef)), init_cost〉).
295* //
296qed.
Note: See TracBrowser for help on using the repository browser.