1 | |
---|
2 | include "basics/lists/listb.ma". |
---|
3 | |
---|
4 | include "Clight/Csyntax.ma". |
---|
5 | |
---|
6 | (* TODO: - check signedness - it's almost certainly wrong |
---|
7 | - this is horrific, let's do it further down the compilation chain |
---|
8 | and tweak the semantics to issue extra cost labels for particular |
---|
9 | operations. *) |
---|
10 | |
---|
11 | (* We define replacements for operations on a particular size of integers. *) |
---|
12 | |
---|
13 | definition specific_op ≝ (unary_operation ⊎ binary_operation) × intsize. |
---|
14 | |
---|
15 | definition unop_dec_eq : ∀x,y:unary_operation. (x = y) ⊎ (x ≠ y). |
---|
16 | * *; try @(inl … (refl …)) %2 % #E destruct |
---|
17 | qed. |
---|
18 | |
---|
19 | definition binop_dec_eq : ∀x,y:binary_operation. (x = y) ⊎ (x ≠ y). |
---|
20 | * *; try @(inl … (refl …)) %2 % #E destruct |
---|
21 | qed. |
---|
22 | |
---|
23 | definition specific_op_dec_eq : ∀x,y:specific_op. (x = y) ⊎ (x ≠ y). |
---|
24 | * * #op #sz * * #op' #sz' |
---|
25 | [ 2,3: %2 % #E destruct ] |
---|
26 | @(eq_intsize_elim sz sz') |
---|
27 | [ 1,3: * #NE %2 % #E destruct @NE @refl ] |
---|
28 | #E >E |
---|
29 | [ cases (unop_dec_eq op op') |
---|
30 | [ #E2 >E2 %1 @refl |
---|
31 | | * #NE %2 % #E2 @NE destruct @refl |
---|
32 | ] |
---|
33 | | cases (binop_dec_eq op op') |
---|
34 | [ #E2 >E2 %1 @refl |
---|
35 | | * #NE %2 % #E2 @NE destruct @refl |
---|
36 | ] |
---|
37 | ] qed. |
---|
38 | |
---|
39 | (* How to specify a replacement *) |
---|
40 | |
---|
41 | record replace_op : Type[0] ≝ |
---|
42 | { op_to_replace : specific_op |
---|
43 | ; op_requires : list specific_op |
---|
44 | ; function_id : ident |
---|
45 | ; function_fd : clight_fundef |
---|
46 | }. |
---|
47 | |
---|
48 | (* Find out which operations are used so that we only add the runtime support |
---|
49 | functions that we need. *) |
---|
50 | |
---|
51 | definition add_op ≝ |
---|
52 | λop:unary_operation ⊎ binary_operation.λty,tl. |
---|
53 | match ty with |
---|
54 | [ Tint sz _ ⇒ 〈op,sz〉::tl |
---|
55 | | _ ⇒ tl |
---|
56 | ]. |
---|
57 | |
---|
58 | let rec expr_ops (e:expr) : list specific_op ≝ |
---|
59 | match e with |
---|
60 | [ Expr e _ ⇒ |
---|
61 | match e with |
---|
62 | [ Ederef e ⇒ expr_ops e |
---|
63 | | Eaddrof e ⇒ expr_ops e |
---|
64 | | Eunop op e ⇒ add_op (inl … op) (typeof e) (expr_ops e) |
---|
65 | | Ebinop op e1 e2 ⇒ add_op (inr … op) (typeof e1) (expr_ops e1 @ expr_ops e2) |
---|
66 | | Ecast _ e ⇒ expr_ops e |
---|
67 | | Econdition e1 e2 e3 ⇒ expr_ops e1 @ expr_ops e2 @ expr_ops e3 |
---|
68 | | Eandbool e1 e2 ⇒ expr_ops e1 @ expr_ops e2 |
---|
69 | | Eorbool e1 e2 ⇒ expr_ops e1 @ expr_ops e2 |
---|
70 | | Efield e _ ⇒ expr_ops e |
---|
71 | | Ecost _ e ⇒ expr_ops e |
---|
72 | | _ ⇒ [ ] |
---|
73 | ] |
---|
74 | ]. |
---|
75 | |
---|
76 | let rec stmt_ops (s:statement) : list specific_op ≝ |
---|
77 | match s with |
---|
78 | [ Sassign e1 e2 ⇒ expr_ops e1 @ expr_ops e2 |
---|
79 | | Scall oe ef es ⇒ let l ≝ foldr ?? (λe,l. expr_ops e @ l) (expr_ops ef) es in |
---|
80 | match oe with [ Some e ⇒ expr_ops e @ l | None ⇒ l ] |
---|
81 | | Ssequence s1 s2 ⇒ stmt_ops s1 @ stmt_ops s2 |
---|
82 | | Sifthenelse e1 s1 s2 ⇒ expr_ops e1 @ stmt_ops s1 @ stmt_ops s2 |
---|
83 | | Swhile e1 s1 ⇒ expr_ops e1 @ stmt_ops s1 |
---|
84 | | Sdowhile e1 s1 ⇒ expr_ops e1 @ stmt_ops s1 |
---|
85 | | Sfor s1 e1 s2 s3 ⇒ expr_ops e1 @ stmt_ops s1 @ stmt_ops s2 @ stmt_ops s3 |
---|
86 | | Sreturn oe ⇒ match oe with [ Some e ⇒ expr_ops e | None ⇒ [ ] ] |
---|
87 | | Sswitch e1 ls ⇒ expr_ops e1 @ lstmt_ops ls |
---|
88 | | Slabel _ s1 ⇒ stmt_ops s1 |
---|
89 | | Scost _ s1 ⇒ stmt_ops s1 |
---|
90 | | _ ⇒ [ ] |
---|
91 | ] |
---|
92 | and lstmt_ops (ls:labeled_statements) : list ((unary_operation ⊎ binary_operation) × intsize) ≝ |
---|
93 | match ls with |
---|
94 | [ LSdefault s1 ⇒ stmt_ops s1 |
---|
95 | | LScase _ _ s1 ls ⇒ stmt_ops s1 @ lstmt_ops ls |
---|
96 | ]. |
---|
97 | |
---|
98 | definition prog_ops : clight_program → list specific_op ≝ |
---|
99 | λp. foldr ?? (λf,l. match \snd f with [ CL_Internal f ⇒ stmt_ops (fn_body f) @ l | _ ⇒ l ]) [ ] (prog_funct ?? p). |
---|
100 | |
---|
101 | (* Actually add the functions. *) |
---|
102 | |
---|
103 | definition add_op_replacements : clight_program → list replace_op → clight_program ≝ |
---|
104 | λp,rs. |
---|
105 | let ops ≝ prog_ops p in |
---|
106 | let 〈ops,extra〉 ≝ foldr ?? (λr,a. |
---|
107 | let 〈ops,fns〉 ≝ a in |
---|
108 | if exists ? (λo. match specific_op_dec_eq o (op_to_replace r) with [ inl _ ⇒ true | _ ⇒ false ]) ops |
---|
109 | then 〈op_requires r @ ops, 〈function_id r, function_fd r〉::fns〉 else 〈ops,fns〉) 〈ops, [ ]〉 rs in |
---|
110 | mk_program ?? (prog_vars ?? p) (extra @ prog_funct ?? p) (prog_main ?? p). |
---|
111 | |
---|
112 | |
---|
113 | (* Now replace the operations by function calls. Unfortunately, Clight is |
---|
114 | about the worst possible place to do this - we need to split up expressions |
---|
115 | because we can't put a function call in an expression. |
---|
116 | |
---|
117 | Also, we need to thread name generation throughout. *) |
---|
118 | |
---|
119 | definition find_replacement ≝ |
---|
120 | λop,ty,rs. |
---|
121 | match ty with |
---|
122 | [ Tint sz _ ⇒ find ?? (λr.match specific_op_dec_eq 〈op,sz〉 (op_to_replace r) with [ inl _ ⇒ Some ? 〈function_id r, type_of_fundef (function_fd r)〉 | _ ⇒ None ? ]) rs |
---|
123 | | _ ⇒ None ? |
---|
124 | ]. |
---|
125 | |
---|
126 | let rec rev_prepend_stmts (l:list statement) (s:statement) : statement ≝ |
---|
127 | match l with |
---|
128 | [ nil ⇒ s |
---|
129 | | cons h t ⇒ rev_prepend_stmts t (Ssequence h s) |
---|
130 | ]. |
---|
131 | |
---|
132 | let rec subst_expr (e:expr) (rs:list replace_op) (u:universe SymbolTag × (list (ident×type))) : (list statement) × expr × (universe SymbolTag × (list (ident×type))) ≝ |
---|
133 | match e with |
---|
134 | [ Expr e ty ⇒ |
---|
135 | match e with |
---|
136 | [ Ederef e1 ⇒ let 〈ls,e1,u〉 ≝ subst_expr e1 rs u in 〈ls, Expr (Ederef e1) ty, u〉 |
---|
137 | | Eaddrof e1 ⇒ let 〈ls,e1,u〉 ≝ subst_expr e1 rs u in 〈ls, Expr (Eaddrof e1) ty, u〉 |
---|
138 | | Eunop op e1 ⇒ |
---|
139 | let 〈ls,e1,u〉 ≝ subst_expr e1 rs u in |
---|
140 | match find_replacement (inl ?? op) (typeof e1) rs with |
---|
141 | [ Some idty ⇒ |
---|
142 | let 〈tmp,u1〉 ≝ fresh … (\fst u) in |
---|
143 | 〈(Scall (Some ? (Expr (Evar tmp) ty)) (Expr (Evar (\fst idty)) (\snd idty)) [e1])::ls, |
---|
144 | (Expr (Evar tmp) ty), 〈u1, 〈tmp, ty〉::(\snd u)〉 〉 |
---|
145 | | None ⇒ 〈ls, (Expr (Eunop op e1) ty), u〉 |
---|
146 | ] |
---|
147 | | Ebinop op e1 e2 ⇒ |
---|
148 | let 〈ls1,e1,u〉 ≝ subst_expr e1 rs u in |
---|
149 | let 〈ls2,e2,u〉 ≝ subst_expr e2 rs u in |
---|
150 | match find_replacement (inr ?? op) (typeof e1) rs with |
---|
151 | [ Some idty ⇒ |
---|
152 | let 〈tmp,u1〉 ≝ fresh … (\fst u) in |
---|
153 | 〈(Scall (Some ? (Expr (Evar tmp) ty)) (Expr (Evar (\fst idty)) (\snd idty)) [e1; e2])::ls1@ls2, |
---|
154 | (Expr (Evar tmp) ty), 〈u1, 〈tmp, ty〉::(\snd u)〉〉 |
---|
155 | | None ⇒ 〈ls1@ls2, (Expr (Ebinop op e1 e2) ty), u〉 |
---|
156 | ] |
---|
157 | | Ecast ty1 e1 ⇒ let 〈ls,e1,u〉 ≝ subst_expr e1 rs u in 〈ls, Expr (Ecast ty1 e1) ty, u〉 |
---|
158 | | Econdition e1 e2 e3 ⇒ |
---|
159 | let 〈ls1,e1,u〉 ≝ subst_expr e1 rs u in |
---|
160 | let 〈ls2,e2,u〉 ≝ subst_expr e2 rs u in |
---|
161 | let 〈ls3,e3,u〉 ≝ subst_expr e3 rs u in |
---|
162 | 〈ls1@ls2@ls3, Expr (Econdition e1 e2 e3) ty, u〉 |
---|
163 | | Eandbool e1 e2 ⇒ |
---|
164 | let 〈ls1,e1,u〉 ≝ subst_expr e1 rs u in |
---|
165 | let 〈ls2,e2,u〉 ≝ subst_expr e2 rs u in |
---|
166 | 〈ls1@ls2, Expr (Eandbool e1 e2) ty, u〉 |
---|
167 | | Eorbool e1 e2 ⇒ |
---|
168 | let 〈ls1,e1,u〉 ≝ subst_expr e1 rs u in |
---|
169 | let 〈ls2,e2,u〉 ≝ subst_expr e2 rs u in |
---|
170 | 〈ls1@ls2, Expr (Eorbool e1 e2) ty, u〉 |
---|
171 | | Efield e1 id ⇒ let 〈ls,e1,u〉 ≝ subst_expr e1 rs u in 〈ls, Expr (Efield e1 id) ty, u〉 |
---|
172 | | Ecost l e1 ⇒ let 〈ls,e1,u〉 ≝ subst_expr e1 rs u in 〈ls, Expr (Ecost l e1) ty, u〉 |
---|
173 | | _ ⇒ 〈[ ], Expr e ty, u〉 |
---|
174 | ] |
---|
175 | ]. |
---|
176 | |
---|
177 | let rec append_stmts (s:statement) (ls:list statement) on ls : statement ≝ |
---|
178 | match ls with |
---|
179 | [ nil ⇒ s |
---|
180 | | cons h t ⇒ append_stmts (Ssequence s h) t |
---|
181 | ]. |
---|
182 | |
---|
183 | let rec subst_stmt (s:statement) (rs:list replace_op) (u:universe SymbolTag × (list (ident×type))) : statement × (universe SymbolTag × (list (ident×type))) ≝ |
---|
184 | match s with |
---|
185 | [ Sassign e1 e2 ⇒ |
---|
186 | let 〈ls1,e1,u〉 ≝ subst_expr e1 rs u in |
---|
187 | let 〈ls2,e2,u〉 ≝ subst_expr e2 rs u in |
---|
188 | 〈rev_prepend_stmts (ls1@ls2) (Sassign e1 e2), u〉 |
---|
189 | | Scall oe ef es ⇒ |
---|
190 | let 〈ls1,oe,u〉 ≝ |
---|
191 | match oe with |
---|
192 | [ Some e ⇒ let 〈ls1,e,u〉 ≝ subst_expr e rs u in 〈ls1, Some ? e, u〉 |
---|
193 | | None ⇒ 〈[ ], None ?, u〉 |
---|
194 | ] in |
---|
195 | let 〈ls2,ef,u〉 ≝ subst_expr ef rs u in |
---|
196 | let 〈lss,es,u〉 ≝ foldr ?? (λe,x. |
---|
197 | let 〈lss,es,u〉 ≝ x in |
---|
198 | let 〈ls,e,u〉 ≝ subst_expr e rs u in |
---|
199 | 〈ls@lss,e::es,u〉) 〈[ ], [ ], u〉 es |
---|
200 | in 〈rev_prepend_stmts (ls1@ls2@lss) (Scall oe ef es), u〉 |
---|
201 | | Ssequence s1 s2 ⇒ |
---|
202 | let 〈s1,u〉 ≝ subst_stmt s1 rs u in |
---|
203 | let 〈s2,u〉 ≝ subst_stmt s2 rs u in |
---|
204 | 〈Ssequence s1 s2, u〉 |
---|
205 | | Sifthenelse e1 s1 s2 ⇒ |
---|
206 | let 〈ls1,e1,u〉 ≝ subst_expr e1 rs u in |
---|
207 | let 〈s1,u〉 ≝ subst_stmt s1 rs u in |
---|
208 | let 〈s2,u〉 ≝ subst_stmt s2 rs u in |
---|
209 | 〈rev_prepend_stmts ls1 (Sifthenelse e1 s1 s2), u〉 |
---|
210 | |
---|
211 | (* This is particularly bad - for loops we end up duplicating the code. *) |
---|
212 | |
---|
213 | | Swhile e1 s1 ⇒ |
---|
214 | let 〈ls1,e1,u〉 ≝ subst_expr e1 rs u in |
---|
215 | let 〈s1,u〉 ≝ subst_stmt s1 rs u in |
---|
216 | 〈rev_prepend_stmts ls1 (Swhile e1 (append_stmts s1 ls1)), u〉 |
---|
217 | | Sdowhile e1 s1 ⇒ |
---|
218 | let 〈ls1,e1,u〉 ≝ subst_expr e1 rs u in |
---|
219 | let 〈s1,u〉 ≝ subst_stmt s1 rs u in |
---|
220 | 〈Sdowhile e1 (append_stmts s1 ls1), u〉 |
---|
221 | | Sfor s1 e1 s2 s3 ⇒ |
---|
222 | let 〈ls1,e1,u〉 ≝ subst_expr e1 rs u in |
---|
223 | let 〈s1,u〉 ≝ subst_stmt s1 rs u in |
---|
224 | let 〈s2,u〉 ≝ subst_stmt s2 rs u in |
---|
225 | let 〈s3,u〉 ≝ subst_stmt s3 rs u in |
---|
226 | 〈Sfor (append_stmts s1 ls1) e1 s2 (append_stmts s3 ls1), u〉 |
---|
227 | | Sreturn oe ⇒ |
---|
228 | match oe with |
---|
229 | [ Some e ⇒ let 〈ls1,e,u〉 ≝ subst_expr e rs u in 〈rev_prepend_stmts ls1 (Sreturn (Some ? e)), u〉 |
---|
230 | | None ⇒ 〈Sreturn (None ?), u〉 |
---|
231 | ] |
---|
232 | | Sswitch e1 lbs ⇒ |
---|
233 | let 〈ls1,e1,u〉 ≝ subst_expr e1 rs u in |
---|
234 | let 〈lbs,u〉 ≝ subst_lstmts lbs rs u in |
---|
235 | 〈rev_prepend_stmts ls1 (Sswitch e1 lbs), u〉 |
---|
236 | | Slabel l s1 ⇒ |
---|
237 | let 〈s1,u〉 ≝ subst_stmt s1 rs u in |
---|
238 | 〈Slabel l s1, u〉 |
---|
239 | | Scost l s1 ⇒ |
---|
240 | let 〈s1,u〉 ≝ subst_stmt s1 rs u in |
---|
241 | 〈Scost l s1, u〉 |
---|
242 | | _ ⇒ 〈s, u〉 |
---|
243 | ] |
---|
244 | and subst_lstmts (lbs:labeled_statements) rs u ≝ |
---|
245 | match lbs with |
---|
246 | [ LSdefault s1 ⇒ |
---|
247 | let 〈s1,u〉 ≝ subst_stmt s1 rs u in |
---|
248 | 〈LSdefault s1, u〉 |
---|
249 | | LScase sz i s1 lbs ⇒ |
---|
250 | let 〈s1,u〉 ≝ subst_stmt s1 rs u in |
---|
251 | let 〈lbs,u〉 ≝ subst_lstmts lbs rs u in |
---|
252 | 〈LScase sz i s1 lbs, u〉 |
---|
253 | ]. |
---|
254 | |
---|
255 | definition subst_fn : function → list replace_op → universe SymbolTag → function × (universe SymbolTag) ≝ |
---|
256 | λf,rs,u. |
---|
257 | let 〈body,u〉 ≝ subst_stmt (fn_body f) rs 〈u, [ ]〉 in |
---|
258 | let 〈u,vs〉 ≝ u in |
---|
259 | 〈mk_function (fn_return f) (fn_params f) (vs @ (fn_vars f)) body, u〉. |
---|
260 | |
---|
261 | definition subst_fundef : clight_fundef → list replace_op → universe SymbolTag → clight_fundef × (universe SymbolTag) ≝ |
---|
262 | λfd,rs,u. |
---|
263 | match fd with |
---|
264 | [ CL_Internal f ⇒ let 〈f,u〉 ≝ subst_fn f rs u in 〈CL_Internal f, u〉 |
---|
265 | | _ ⇒ 〈fd, u〉 |
---|
266 | ]. |
---|
267 | |
---|
268 | definition subst_prog : clight_program → list replace_op → universe SymbolTag → clight_program × (universe SymbolTag) ≝ |
---|
269 | λp,rs,u. |
---|
270 | let 〈fns, u〉 ≝ foldr ?? (λf,a. |
---|
271 | let 〈fns, u〉 ≝ a in |
---|
272 | let 〈fd,u〉 ≝ subst_fundef (\snd f) rs u in |
---|
273 | 〈〈\fst f, fd〉::fns, u〉) 〈[ ], u〉 (prog_funct ?? p) |
---|
274 | in 〈mk_program ?? (prog_vars ?? p) fns (prog_main ?? p), u〉. |
---|
275 | |
---|
276 | (* Now define some functions in Clight. *) |
---|
277 | |
---|
278 | definition divu : universe SymbolTag → intsize → replace_op × (universe SymbolTag) ≝ |
---|
279 | λu,sz. |
---|
280 | let uint ≝ Tint sz Unsigned in |
---|
281 | let 〈fn_id, u〉 ≝ fresh … u in |
---|
282 | let 〈x, u〉 ≝ fresh … u in |
---|
283 | let 〈y, u〉 ≝ fresh … u in |
---|
284 | let 〈quo, u〉 ≝ fresh … u in |
---|
285 | 〈mk_replace_op 〈inr ?? Odiv, sz〉 [ ] fn_id |
---|
286 | (CL_Internal (mk_function uint |
---|
287 | [〈x, uint〉; 〈y, uint〉] |
---|
288 | [〈quo, uint〉] |
---|
289 | (Ssequence |
---|
290 | (Sassign (Expr (Evar quo) uint) (Expr (Econst_int sz (repr sz 0)) uint)) |
---|
291 | (Ssequence |
---|
292 | (Swhile |
---|
293 | (Expr (Ebinop Oge (Expr (Evar x) uint) (Expr (Evar y) uint)) uint) |
---|
294 | (Ssequence |
---|
295 | (Sassign (Expr (Evar x) uint) (Expr (Ebinop Osub (Expr (Evar x) uint) (Expr (Evar y) uint)) uint)) |
---|
296 | (Sassign (Expr (Evar quo) uint) (Expr (Ebinop Oadd (Expr (Evar quo) uint) (Expr (Econst_int sz (repr sz 1)) uint)) uint)))) |
---|
297 | (Sreturn (Some ? (Expr (Evar quo) uint))))))), |
---|
298 | u〉. |
---|
299 | |
---|
300 | (* And do everything... *) |
---|
301 | |
---|
302 | definition add_runtime_replacements : clight_program → universe SymbolTag → clight_program × (universe SymbolTag) ≝ |
---|
303 | λp,u. |
---|
304 | let 〈divu16,u〉 ≝ divu u I16 in |
---|
305 | let 〈divu32,u〉 ≝ divu u I32 in |
---|
306 | let rs ≝ [divu16;divu32] in |
---|
307 | let p ≝ add_op_replacements p rs in |
---|
308 | subst_prog p rs u. |
---|
309 | |
---|
310 | |
---|
311 | |
---|
312 | |
---|