source: src/Clight/addRuntime.ma @ 3178

Last change on this file since 3178 was 1618, checked in by campbell, 8 years ago

Minor updates due to recent changes.

File size: 11.8 KB
Line 
1
2include "basics/lists/listb.ma".
3
4include "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
13definition specific_op ≝ (unary_operation ⊎ binary_operation) × intsize.
14
15definition unop_dec_eq : ∀x,y:unary_operation. (x = y) ⊎ (x ≠ y).
16* *; try @(inl … (refl …)) %2 % #E destruct
17qed.
18
19definition binop_dec_eq : ∀x,y:binary_operation. (x = y) ⊎ (x ≠ y).
20* *; try @(inl … (refl …)) %2 % #E destruct
21qed.
22
23definition 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
41record 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
51definition add_op ≝
52λop:unary_operation ⊎ binary_operation.λty,tl.
53  match ty with
54  [ Tint sz _ ⇒ 〈op,sz〉::tl
55  | _ ⇒ tl
56  ].
57
58let rec expr_ops (e:expr) : list specific_op ≝
59match 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
76let rec stmt_ops (s:statement) : list specific_op ≝
77match 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]
92and lstmt_ops (ls:labeled_statements) : list ((unary_operation ⊎ binary_operation) × intsize) ≝
93match ls with
94[ LSdefault s1 ⇒ stmt_ops s1
95| LScase _ _ s1 ls ⇒ stmt_ops s1 @ lstmt_ops ls
96].
97
98definition 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
103definition 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
119definition 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
126let rec rev_prepend_stmts (l:list statement) (s:statement) : statement ≝
127match l with
128[ nil ⇒ s
129| cons h t ⇒ rev_prepend_stmts t (Ssequence h s)
130].
131
132let rec subst_expr (e:expr) (rs:list replace_op) (u:universe SymbolTag × (list (ident×type))) : (list statement) × expr × (universe SymbolTag × (list (ident×type))) ≝
133match 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
177let rec append_stmts (s:statement) (ls:list statement) on ls : statement ≝
178match ls with
179[ nil ⇒ s
180| cons h t ⇒ append_stmts (Ssequence s h) t
181].
182
183let rec subst_stmt (s:statement) (rs:list replace_op) (u:universe SymbolTag × (list (ident×type))) : statement × (universe SymbolTag × (list (ident×type))) ≝
184match 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]
244and subst_lstmts (lbs:labeled_statements) rs u ≝
245match 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
255definition 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
261definition 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
268definition 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
278definition 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
302definition 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 
Note: See TracBrowser for help on using the repository browser.