source: src/Clight/label.ma @ 2353

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

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 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 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 *)
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 *)
106| Eandbool e1 e2 ⇒
107    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
108    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
109    let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 (const_int 1) (const_int 0)) ty) costgen in
110    let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
111    〈Econdition e1 e2 ef, costgen〉
112| Eorbool e1 e2 ⇒
113    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
114    let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
115    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
116    let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 (const_int 1) (const_int 0)) ty) costgen in
117    〈Econdition e1 et e2, costgen〉
118
119| Efield e' id ⇒
120    let 〈e',costgen〉 ≝ label_expr e' costgen in
121    〈Efield e' id, costgen〉
122(* The prototype asserts on preexisting cost labels, but I'd quite like to
123   keep them. *)
124| Ecost l e' ⇒
125    let 〈e',costgen〉 ≝ label_expr e' costgen in
126    〈Ecost l e', costgen〉
127
128(* The remaining expressions don't have subexpressions. *)
129| _ ⇒ 〈e,costgen〉
130].
131
132let rec label_exprs (l:list expr) (costgen:universe CostTag)
133        on l : list expr × (universe CostTag) ≝
134match l with
135[ nil ⇒ 〈nil ?,costgen〉
136| cons e es ⇒
137    let 〈e,costgen〉 ≝ label_expr e costgen in
138    let 〈es,costgen〉 ≝ label_exprs es costgen in
139    〈e::es,costgen〉
140].
141
142definition label_opt_expr ≝
143λoe,costgen. match oe with
144[ None ⇒ 〈None ?, costgen〉
145| Some e ⇒ let 〈e,costgen〉 ≝ label_expr e costgen in 〈Some ? e,costgen〉
146].
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  ].
154
155
156let rec label_statement (s:statement) (costgen:universe CostTag)
157        on s : statement × (universe CostTag) ≝
158match s with
159[ Sskip ⇒ 〈Sskip,costgen〉
160| Sassign e1 e2 ⇒
161    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
162    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
163    〈Sassign e1 e2, costgen〉
164| Scall e_ret e_fn e_args ⇒
165    let 〈e_ret,costgen〉 ≝ label_opt_expr e_ret costgen in
166    let 〈e_fn,costgen〉 ≝ label_expr e_fn costgen in
167    let 〈e_args,costgen〉 ≝ label_exprs e_args costgen in
168    〈Scall e_ret e_fn e_args, costgen〉
169| Ssequence s1 s2 ⇒
170    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
171    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
172    〈Ssequence s1 s2, costgen〉
173| Sifthenelse e s1 s2 ⇒
174    let 〈e,costgen〉 ≝ label_expr e costgen in
175    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
176    let 〈s1,costgen〉 ≝ add_cost_before s1 costgen in
177    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
178    let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in
179    〈Sifthenelse e s1 s2, costgen〉
180| Swhile e s' cl ⇒
181    let 〈e,costgen〉 ≝ label_expr e costgen in
182    let 〈s',costgen〉 ≝ label_statement s' costgen in
183    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
184    let 〈after,costgen〉 ≝ ensure_label cl costgen in
185    〈Swhile e s' (Some ? after), costgen〉
186| Sdowhile e s' ⇒
187    let 〈e,costgen〉 ≝ label_expr e costgen in
188    let 〈s',costgen〉 ≝ label_statement s' costgen in
189    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
190    let 〈s,costgen〉 ≝ add_cost_after (Sdowhile e s') costgen in
191    〈s,costgen〉
192| Sfor s1 e s2 s3 ⇒
193    let 〈e,costgen〉 ≝ label_expr e costgen in
194    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
195    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
196    let 〈s3,costgen〉 ≝ label_statement s3 costgen in
197    let 〈s3,costgen〉 ≝ add_cost_before s3 costgen in
198    let 〈s,costgen〉 ≝ add_cost_after (Sfor s1 e s2 s3) costgen in
199    〈s,costgen〉
200| Sbreak ⇒ 〈Sbreak,costgen〉
201| Scontinue ⇒ 〈Scontinue,costgen〉
202| Sreturn opt_e ⇒
203    let 〈opt_e,costgen〉 ≝ label_opt_expr opt_e costgen in
204    〈Sreturn opt_e,costgen〉
205| Sswitch e ls ⇒
206    let 〈e,costgen〉 ≝ label_expr e costgen in
207    let 〈ls,costgen〉 ≝ label_lstatements ls costgen in
208    〈Sswitch e ls, costgen〉
209| Slabel l s' ⇒
210    let 〈s',costgen〉 ≝ label_statement s' costgen in
211    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
212    〈Slabel l s', costgen〉
213| Sgoto l ⇒ 〈Sgoto l, costgen〉
214
215(* The prototype asserts on preexisting cost labels, but I'd quite like to
216   keep them. *)
217| Scost l s' ⇒
218    let 〈s',costgen〉 ≝ label_statement s' costgen in
219    〈Scost l s', costgen〉
220]
221and label_lstatements (ls:labeled_statements) (costgen:universe CostTag)
222        on ls : labeled_statements × (universe CostTag) ≝
223match ls with
224[ LSdefault s ⇒
225    let 〈s,costgen〉 ≝ label_statement s costgen in
226    let 〈s,costgen〉 ≝ add_cost_before s costgen in
227    〈LSdefault s, costgen〉
228| LScase sz i s ls' ⇒
229    let 〈s,costgen〉 ≝ label_statement s costgen in
230    let 〈s,costgen〉 ≝ add_cost_before s costgen in
231    let 〈ls',costgen〉 ≝ label_lstatements ls' costgen in
232    〈LScase sz i s ls', costgen〉
233].
234
235definition label_function : universe CostTag → function → function × (universe CostTag) ≝
236λcostgen,f.
237  let 〈body,costgen〉 ≝ label_statement (fn_body f) costgen in
238  let 〈body,costgen〉 ≝ add_cost_before body costgen in
239    〈mk_function (fn_return f) (fn_params f) (fn_vars f) body, costgen〉.
240
241definition label_fundef : universe CostTag → clight_fundef → clight_fundef × (universe CostTag) ≝
242λgen,f. match f with
243[ CL_Internal f ⇒
244    let 〈f',gen'〉 ≝ label_function gen f in
245    〈CL_Internal f', gen'〉
246| CL_External id args ty ⇒ 〈CL_External id args ty, gen〉
247].
248
249
250
251definition clight_label : clight_program → clight_program × costlabel ≝
252λp.
253  let costgen ≝ new_universe CostTag in
254  let 〈init_cost, costgen〉 ≝ fresh … costgen in
255  〈\fst (transform_program_gen … costgen p (λ_.label_fundef)), init_cost〉.
Note: See TracBrowser for help on using the repository browser.