source: src/Clight/label.ma @ 2392

Last change on this file since 2392 was 2392, checked in by campbell, 7 years ago
Labelling translations of && and
need a lot of cost labelling to meet

criteria.

File size: 10.0 KB
Line 
1include "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 ⇒ 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 ≝
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 *)
53
54definition add_cost_before : statement → universe CostTag → statement × (universe CostTag) ≝
55λs,gen.
56  let 〈l,gen〉 ≝ fresh … gen in
57  〈Scost l s, gen〉.
58
59definition add_cost_after : statement → universe CostTag → statement × (universe CostTag) ≝
60λs,gen.
61  let 〈l,gen〉 ≝ fresh … gen in
62  〈Ssequence s (Scost l Sskip), gen〉.
63
64definition add_cost_expr : expr → universe CostTag → expr × (universe CostTag) ≝
65λe,gen.
66  let 〈l,gen〉 ≝ fresh … gen in
67  〈Expr (Ecost l e) (typeof e), gen〉.
68
69definition const_int : nat → expr ≝
70λn. Expr (Econst_int ? (repr I32 n)) (Tint I32 Signed).
71
72let rec label_expr (e:expr) (costgen:universe CostTag)
73        on e : expr × (universe CostTag) ≝
74match e with
75[ Expr ed ty ⇒ let 〈ed,costgen〉 ≝ label_expr_descr ed costgen ty in
76               〈Expr ed ty, costgen〉
77]
78and label_expr_descr (e:expr_descr) (costgen:universe CostTag) (ty:type)
79    on e : expr_descr × (universe CostTag) ≝
80match e with
81[ Ederef e' ⇒
82    let 〈e',costgen〉 ≝ label_expr e' costgen in
83    〈Ederef e', costgen〉
84| Eaddrof e' ⇒
85    let 〈e',costgen〉 ≝ label_expr e' costgen in
86    〈Eaddrof e', costgen〉
87| Eunop op e' ⇒
88    let 〈e',costgen〉 ≝ label_expr e' costgen in
89    〈Eunop op e', costgen〉
90| Ebinop op e1 e2 ⇒
91    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
92    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
93    〈Ebinop op e1 e2, costgen〉
94| Ecast ty e' ⇒
95    let 〈e',costgen〉 ≝ label_expr e' costgen in
96    〈Ecast ty e', costgen〉
97| Econdition e' e1 e2 ⇒
98    let 〈e',costgen〉 ≝ label_expr e' costgen in
99    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
100    let 〈e1,costgen〉 ≝ add_cost_expr e1 costgen in
101    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
102    let 〈e2,costgen〉 ≝ add_cost_expr e2 costgen in
103    〈Econdition e' e1 e2, costgen〉
104(* andbool and orbool are changed to conditionals to capture their
105   short-circuiting cost difference; note that we have to return 0 or 1, and
106   we get rather more cost labels than I'd like *)
107| Eandbool e1 e2 ⇒
108    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
109    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
110    let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
111    let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
112    let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
113    let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
114    〈Econdition e1 e2 ef, costgen〉
115| Eorbool e1 e2 ⇒
116    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
117    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
118    let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
119    let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
120    let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
121    let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
122    〈Econdition e1 et e2, costgen〉
123
124| Efield e' id ⇒
125    let 〈e',costgen〉 ≝ label_expr e' costgen in
126    〈Efield e' id, costgen〉
127(* The prototype asserts on preexisting cost labels, but I'd quite like to
128   keep them. *)
129| Ecost l e' ⇒
130    let 〈e',costgen〉 ≝ label_expr e' costgen in
131    〈Ecost l e', costgen〉
132
133(* The remaining expressions don't have subexpressions. *)
134| _ ⇒ 〈e,costgen〉
135].
136
137let rec label_exprs (l:list expr) (costgen:universe CostTag)
138        on l : list expr × (universe CostTag) ≝
139match l with
140[ nil ⇒ 〈nil ?,costgen〉
141| cons e es ⇒
142    let 〈e,costgen〉 ≝ label_expr e costgen in
143    let 〈es,costgen〉 ≝ label_exprs es costgen in
144    〈e::es,costgen〉
145].
146
147definition label_opt_expr ≝
148λoe,costgen. match oe with
149[ None ⇒ 〈None ?, costgen〉
150| Some e ⇒ let 〈e,costgen〉 ≝ label_expr e costgen in 〈Some ? e,costgen〉
151].
152
153
154let rec label_statement (s:statement) (costgen:universe CostTag)
155        on s : statement × (universe CostTag) ≝
156match s with
157[ Sskip ⇒ 〈Sskip,costgen〉
158| Sassign e1 e2 ⇒
159    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
160    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
161    〈Sassign e1 e2, costgen〉
162| Scall e_ret e_fn e_args ⇒
163    let 〈e_ret,costgen〉 ≝ label_opt_expr e_ret costgen in
164    let 〈e_fn,costgen〉 ≝ label_expr e_fn costgen in
165    let 〈e_args,costgen〉 ≝ label_exprs e_args costgen in
166    〈Scall e_ret e_fn e_args, costgen〉
167| Ssequence s1 s2 ⇒
168    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
169    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
170    〈Ssequence s1 s2, costgen〉
171| Sifthenelse e s1 s2 ⇒
172    let 〈e,costgen〉 ≝ label_expr e costgen in
173    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
174    let 〈s1,costgen〉 ≝ add_cost_before s1 costgen in
175    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
176    let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in
177    〈Sifthenelse e s1 s2, costgen〉
178| Swhile e s' ⇒
179    let 〈e,costgen〉 ≝ label_expr e costgen in
180    let 〈s',costgen〉 ≝ label_statement s' costgen in
181    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
182    let 〈s,costgen〉 ≝ add_cost_after (Swhile e s') costgen in
183    〈s,costgen〉
184| Sdowhile e s' ⇒
185    let 〈e,costgen〉 ≝ label_expr e costgen in
186    let 〈s',costgen〉 ≝ label_statement s' costgen in
187    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
188    let 〈s,costgen〉 ≝ add_cost_after (Sdowhile e s') costgen in
189    〈s,costgen〉
190| Sfor s1 e s2 s3 ⇒
191    let 〈e,costgen〉 ≝ label_expr e costgen in
192    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
193    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
194    let 〈s3,costgen〉 ≝ label_statement s3 costgen in
195    let 〈s3,costgen〉 ≝ add_cost_before s3 costgen in
196    let 〈s,costgen〉 ≝ add_cost_after (Sfor s1 e s2 s3) costgen in
197    〈s,costgen〉
198| Sbreak ⇒ 〈Sbreak,costgen〉
199| Scontinue ⇒ 〈Scontinue,costgen〉
200| Sreturn opt_e ⇒
201    let 〈opt_e,costgen〉 ≝ label_opt_expr opt_e costgen in
202    〈Sreturn opt_e,costgen〉
203| Sswitch e ls ⇒
204    let 〈e,costgen〉 ≝ label_expr e costgen in
205    let 〈ls,costgen〉 ≝ label_lstatements ls costgen in
206    〈Sswitch e ls, costgen〉
207| Slabel l s' ⇒
208    let 〈s',costgen〉 ≝ label_statement s' costgen in
209    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
210    〈Slabel l s', costgen〉
211| Sgoto l ⇒ 〈Sgoto l, costgen〉
212
213(* The prototype asserts on preexisting cost labels, but I'd quite like to
214   keep them. *)
215| Scost l s' ⇒
216    let 〈s',costgen〉 ≝ label_statement s' costgen in
217    〈Scost l s', costgen〉
218]
219and label_lstatements (ls:labeled_statements) (costgen:universe CostTag)
220        on ls : labeled_statements × (universe CostTag) ≝
221match ls with
222[ LSdefault s ⇒
223    let 〈s,costgen〉 ≝ label_statement s costgen in
224    let 〈s,costgen〉 ≝ add_cost_before s costgen in
225    〈LSdefault s, costgen〉
226| LScase sz i s ls' ⇒
227    let 〈s,costgen〉 ≝ label_statement s costgen in
228    let 〈s,costgen〉 ≝ add_cost_before s costgen in
229    let 〈ls',costgen〉 ≝ label_lstatements ls' costgen in
230    〈LScase sz i s ls', costgen〉
231].
232
233definition label_function : universe CostTag → function → function × (universe CostTag) ≝
234λcostgen,f.
235  let 〈body,costgen〉 ≝ label_statement (fn_body f) costgen in
236  let 〈body,costgen〉 ≝ add_cost_before body costgen in
237    〈mk_function (fn_return f) (fn_params f) (fn_vars f) body, costgen〉.
238
239definition label_fundef : universe CostTag → clight_fundef → clight_fundef × (universe CostTag) ≝
240λgen,f. match f with
241[ CL_Internal f ⇒
242    let 〈f',gen'〉 ≝ label_function gen f in
243    〈CL_Internal f', gen'〉
244| CL_External id args ty ⇒ 〈CL_External id args ty, gen〉
245].
246
247
248
249definition clight_label : clight_program → clight_program × costlabel ≝
250λp.
251  let costgen ≝ new_universe CostTag in
252  let 〈init_cost, costgen〉 ≝ fresh … costgen in
253  〈\fst (transform_program_gen … costgen p (λ_.label_fundef)), init_cost〉.
Note: See TracBrowser for help on using the repository browser.