source: src/Clight/label.ma @ 2391

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

Revert "Put the post-loop cost label into the Clight while statement ..."
Rely on the Cminor to RTLabs stage ignoring Cminor skips instead.
This reverts commit 2353.

File size: 9.8 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 *)
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
148
149let rec label_statement (s:statement) (costgen:universe CostTag)
150        on s : statement × (universe CostTag) ≝
151match s with
152[ Sskip ⇒ 〈Sskip,costgen〉
153| Sassign e1 e2 ⇒
154    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
155    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
156    〈Sassign e1 e2, costgen〉
157| Scall e_ret e_fn e_args ⇒
158    let 〈e_ret,costgen〉 ≝ label_opt_expr e_ret costgen in
159    let 〈e_fn,costgen〉 ≝ label_expr e_fn costgen in
160    let 〈e_args,costgen〉 ≝ label_exprs e_args costgen in
161    〈Scall e_ret e_fn e_args, costgen〉
162| Ssequence s1 s2 ⇒
163    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
164    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
165    〈Ssequence s1 s2, costgen〉
166| Sifthenelse e s1 s2 ⇒
167    let 〈e,costgen〉 ≝ label_expr e costgen in
168    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
169    let 〈s1,costgen〉 ≝ add_cost_before s1 costgen in
170    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
171    let 〈s2,costgen〉 ≝ add_cost_before s2 costgen in
172    〈Sifthenelse e s1 s2, costgen〉
173| Swhile e s' ⇒
174    let 〈e,costgen〉 ≝ label_expr e costgen in
175    let 〈s',costgen〉 ≝ label_statement s' costgen in
176    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
177    let 〈s,costgen〉 ≝ add_cost_after (Swhile e s') costgen in
178    〈s,costgen〉
179| Sdowhile e s' ⇒
180    let 〈e,costgen〉 ≝ label_expr e costgen in
181    let 〈s',costgen〉 ≝ label_statement s' costgen in
182    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
183    let 〈s,costgen〉 ≝ add_cost_after (Sdowhile e s') costgen in
184    〈s,costgen〉
185| Sfor s1 e s2 s3 ⇒
186    let 〈e,costgen〉 ≝ label_expr e costgen in
187    let 〈s1,costgen〉 ≝ label_statement s1 costgen in
188    let 〈s2,costgen〉 ≝ label_statement s2 costgen in
189    let 〈s3,costgen〉 ≝ label_statement s3 costgen in
190    let 〈s3,costgen〉 ≝ add_cost_before s3 costgen in
191    let 〈s,costgen〉 ≝ add_cost_after (Sfor s1 e s2 s3) costgen in
192    〈s,costgen〉
193| Sbreak ⇒ 〈Sbreak,costgen〉
194| Scontinue ⇒ 〈Scontinue,costgen〉
195| Sreturn opt_e ⇒
196    let 〈opt_e,costgen〉 ≝ label_opt_expr opt_e costgen in
197    〈Sreturn opt_e,costgen〉
198| Sswitch e ls ⇒
199    let 〈e,costgen〉 ≝ label_expr e costgen in
200    let 〈ls,costgen〉 ≝ label_lstatements ls costgen in
201    〈Sswitch e ls, costgen〉
202| Slabel l s' ⇒
203    let 〈s',costgen〉 ≝ label_statement s' costgen in
204    let 〈s',costgen〉 ≝ add_cost_before s' costgen in
205    〈Slabel l s', costgen〉
206| Sgoto l ⇒ 〈Sgoto l, costgen〉
207
208(* The prototype asserts on preexisting cost labels, but I'd quite like to
209   keep them. *)
210| Scost l s' ⇒
211    let 〈s',costgen〉 ≝ label_statement s' costgen in
212    〈Scost l s', costgen〉
213]
214and label_lstatements (ls:labeled_statements) (costgen:universe CostTag)
215        on ls : labeled_statements × (universe CostTag) ≝
216match ls with
217[ LSdefault s ⇒
218    let 〈s,costgen〉 ≝ label_statement s costgen in
219    let 〈s,costgen〉 ≝ add_cost_before s costgen in
220    〈LSdefault s, costgen〉
221| LScase sz i s ls' ⇒
222    let 〈s,costgen〉 ≝ label_statement s costgen in
223    let 〈s,costgen〉 ≝ add_cost_before s costgen in
224    let 〈ls',costgen〉 ≝ label_lstatements ls' costgen in
225    〈LScase sz i s ls', costgen〉
226].
227
228definition label_function : universe CostTag → function → function × (universe CostTag) ≝
229λcostgen,f.
230  let 〈body,costgen〉 ≝ label_statement (fn_body f) costgen in
231  let 〈body,costgen〉 ≝ add_cost_before body costgen in
232    〈mk_function (fn_return f) (fn_params f) (fn_vars f) body, costgen〉.
233
234definition label_fundef : universe CostTag → clight_fundef → clight_fundef × (universe CostTag) ≝
235λgen,f. match f with
236[ CL_Internal f ⇒
237    let 〈f',gen'〉 ≝ label_function gen f in
238    〈CL_Internal f', gen'〉
239| CL_External id args ty ⇒ 〈CL_External id args ty, gen〉
240].
241
242
243
244definition clight_label : clight_program → clight_program × costlabel ≝
245λp.
246  let costgen ≝ new_universe CostTag in
247  let 〈init_cost, costgen〉 ≝ fresh … costgen in
248  〈\fst (transform_program_gen … costgen p (λ_.label_fundef)), init_cost〉.
Note: See TracBrowser for help on using the repository browser.