1 | include "utilities/lists.ma". |
---|
2 | include "common/Globalenvs.ma". |
---|
3 | include "Cminor/syntax.ma". |
---|
4 | include "RTLabs/syntax.ma". |
---|
5 | |
---|
6 | definition env ≝ identifier_map SymbolTag register. |
---|
7 | definition label_env ≝ identifier_map SymbolTag label. |
---|
8 | definition populate_env : env → universe RegisterTag → list ident → res (list register × env × (universe RegisterTag)) ≝ |
---|
9 | λen,gen. foldr ?? |
---|
10 | (λid,rsengen. |
---|
11 | do 〈rs,en,gen〉 ← rsengen; |
---|
12 | do 〈r,gen'〉 ← fresh … gen; |
---|
13 | OK ? 〈r::rs, add ?? en id r, gen'〉) (OK ? 〈[ ], en, gen〉). |
---|
14 | |
---|
15 | definition populate_label_env : label_env → universe LabelTag → list ident → res (label_env × (universe LabelTag)) ≝ |
---|
16 | λen,gen. foldr ?? |
---|
17 | (λid,engen. |
---|
18 | do 〈en,gen〉 ← engen; |
---|
19 | do 〈r,gen'〉 ← fresh … gen; |
---|
20 | OK ? 〈add ?? en id r, gen'〉) (OK ? 〈en, gen〉). |
---|
21 | |
---|
22 | (* Add a statement to the graph, *without* updating the entry label. *) |
---|
23 | definition fill_in_statement : label → statement → internal_function → internal_function ≝ |
---|
24 | λl,s,f. |
---|
25 | mk_internal_function (f_labgen f) (f_reggen f) (f_sig f) |
---|
26 | (f_result f) (f_params f) (f_locals f) (f_ptrs f) |
---|
27 | (f_stacksize f) (add ?? (f_graph f) l s) (f_entry f) (f_exit f). |
---|
28 | |
---|
29 | (* Add a statement to the graph, making it the entry label. *) |
---|
30 | definition add_to_graph : label → statement → internal_function → internal_function ≝ |
---|
31 | λl,s,f. |
---|
32 | mk_internal_function (f_labgen f) (f_reggen f) (f_sig f) |
---|
33 | (f_result f) (f_params f) (f_locals f) (f_ptrs f) |
---|
34 | (f_stacksize f) (add ?? (f_graph f) l s) l (f_exit f). |
---|
35 | |
---|
36 | (* Add a statement with a fresh label to the start of the function. The |
---|
37 | statement is parametrised by the *next* instruction's label. *) |
---|
38 | definition add_fresh_to_graph : (label → statement) → internal_function → res internal_function ≝ |
---|
39 | λs,f. |
---|
40 | do 〈l,g〉 ← fresh … (f_labgen f); |
---|
41 | let s' ≝ s (f_entry f) in |
---|
42 | OK ? (mk_internal_function g (f_reggen f) (f_sig f) |
---|
43 | (f_result f) (f_params f) (f_locals f) (f_ptrs f) |
---|
44 | (f_stacksize f) (add ?? (f_graph f) l s') l (f_exit f)). |
---|
45 | |
---|
46 | (* Generate a fresh label and use it as a dangling entry point, to be filled in |
---|
47 | later with the loop head. *) |
---|
48 | definition add_loop_label_to_graph : internal_function → res internal_function ≝ |
---|
49 | λf. |
---|
50 | do 〈l,g〉 ← fresh … (f_labgen f); |
---|
51 | OK ? (mk_internal_function g (f_reggen f) (f_sig f) |
---|
52 | (f_result f) (f_params f) (f_locals f) (f_ptrs f) |
---|
53 | (f_stacksize f) (f_graph f) l (f_exit f)). |
---|
54 | |
---|
55 | definition fresh_reg : internal_function → res (register × internal_function) ≝ |
---|
56 | λf. |
---|
57 | do 〈r,g〉 ← fresh … (f_reggen f); |
---|
58 | OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f) |
---|
59 | (f_result f) (f_params f) (r::(f_locals f)) (f_ptrs f) |
---|
60 | (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. |
---|
61 | |
---|
62 | definition fresh_ptr_reg : internal_function → res (register × internal_function) ≝ |
---|
63 | λf. |
---|
64 | do 〈r,g〉 ← fresh … (f_reggen f); |
---|
65 | OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f) |
---|
66 | (f_result f) (f_params f) (r::(f_locals f)) (r::(f_ptrs f)) |
---|
67 | (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. |
---|
68 | |
---|
69 | let rec expr_yields_pointer (e:expr) (ptrs:list ident) : bool ≝ |
---|
70 | match e with |
---|
71 | [ Id i ⇒ exists ? (eq_identifier ? i) ptrs |
---|
72 | | Cst c ⇒ match c with [ Oaddrsymbol _ _ ⇒ true | Oaddrstack _ ⇒ true | _ ⇒ false ] |
---|
73 | | Op1 op e' ⇒ |
---|
74 | match op with |
---|
75 | [ Oid ⇒ expr_yields_pointer e' ptrs |
---|
76 | | Optrofint _ ⇒ true |
---|
77 | | _ ⇒ false |
---|
78 | ] |
---|
79 | | Op2 op e1 e2 ⇒ |
---|
80 | match op with |
---|
81 | [ Oaddp ⇒ true |
---|
82 | | Osubpi ⇒ true |
---|
83 | | _ ⇒ false |
---|
84 | ] |
---|
85 | | Mem q e' ⇒ |
---|
86 | match q with |
---|
87 | [ Mpointer _ ⇒ true |
---|
88 | | _ ⇒ false |
---|
89 | ] |
---|
90 | (* Both branches ought to be the same? *) |
---|
91 | | Cond e' e1 e2 ⇒ (expr_yields_pointer e1 ptrs) ∨ (expr_yields_pointer e2 ptrs) |
---|
92 | | Ecost _ e' ⇒ expr_yields_pointer e' ptrs |
---|
93 | ]. |
---|
94 | |
---|
95 | definition choose_reg : env → expr → list ident → internal_function → res (register × internal_function) ≝ |
---|
96 | λenv,e,ptrs,f. |
---|
97 | match e with |
---|
98 | [ Id i ⇒ |
---|
99 | do r ← opt_to_res … (lookup … env i); |
---|
100 | OK ? 〈r, f〉 |
---|
101 | | _ ⇒ |
---|
102 | if expr_yields_pointer e ptrs then fresh_ptr_reg f else fresh_reg f |
---|
103 | ]. |
---|
104 | |
---|
105 | definition choose_regs : env → list expr → list ident → internal_function → res (list register × internal_function) ≝ |
---|
106 | λenv,es,ptrs,f. |
---|
107 | foldr ?? (λe,acc. do 〈rs,f〉 ← acc; |
---|
108 | do 〈r,f'〉 ← choose_reg env e ptrs f; |
---|
109 | OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es. |
---|
110 | |
---|
111 | let rec add_expr (env:env) (e:expr) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝ |
---|
112 | match e with |
---|
113 | [ Id i ⇒ |
---|
114 | do r ← opt_to_res … (lookup ?? env i); |
---|
115 | match register_eq r dst with |
---|
116 | [ inl _ ⇒ OK ? f |
---|
117 | | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f |
---|
118 | ] |
---|
119 | | Cst c ⇒ add_fresh_to_graph (St_const dst c) f |
---|
120 | | Op1 op e' ⇒ |
---|
121 | do 〈r,f〉 ← choose_reg env e' ptrs f; |
---|
122 | do f ← add_fresh_to_graph (St_op1 op dst r) f; |
---|
123 | add_expr env e' r ptrs f |
---|
124 | | Op2 op e1 e2 ⇒ |
---|
125 | do 〈r1,f〉 ← choose_reg env e1 ptrs f; |
---|
126 | do 〈r2,f〉 ← choose_reg env e2 ptrs f; |
---|
127 | do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f; |
---|
128 | do f ← add_expr env e2 r2 ptrs f; |
---|
129 | add_expr env e1 r1 ptrs f |
---|
130 | | Mem q e' ⇒ |
---|
131 | add_with_addressing_internal env e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env e') |
---|
132 | | Cond e' e1 e2 ⇒ |
---|
133 | let resume_at ≝ f_entry f in |
---|
134 | do f ← add_expr env e2 dst ptrs f; |
---|
135 | let lfalse ≝ f_entry f in |
---|
136 | do f ← add_fresh_to_graph (λ_.St_skip resume_at) f; |
---|
137 | do f ← add_expr env e1 dst ptrs f; |
---|
138 | add_branch_internal env e' (f_entry f) lfalse ptrs f (add_expr env e') |
---|
139 | | Ecost l e' ⇒ |
---|
140 | do f ← add_expr env e' dst ptrs f; |
---|
141 | add_fresh_to_graph (St_cost l) f |
---|
142 | |
---|
143 | (* Ugh, the termination checker isn't smart enough to notice that calling |
---|
144 | add_expr with e is OK, so we take it partially applied and define a proper |
---|
145 | add_<whatever> afterwards. *) |
---|
146 | ] |
---|
147 | and add_with_addressing_internal (env:env) (e:expr) |
---|
148 | (s:∀m:addressing. addr m → label → statement) |
---|
149 | (ptrs:list ident) |
---|
150 | (f:internal_function) |
---|
151 | (termination_hack:register → list ident → internal_function → res internal_function) |
---|
152 | on e : res internal_function ≝ |
---|
153 | let add_default : unit → res internal_function ≝ λ_. |
---|
154 | do 〈r, f〉 ← choose_reg env e ptrs f; |
---|
155 | do f ← add_fresh_to_graph (s (Aindexed zero) [[ r ]]) f; |
---|
156 | termination_hack r ptrs f |
---|
157 | in |
---|
158 | match e with |
---|
159 | [ Cst c ⇒ |
---|
160 | match c with |
---|
161 | [ Oaddrsymbol id i ⇒ add_fresh_to_graph (s (Aglobal id i) [[ ]]) f |
---|
162 | | Oaddrstack i ⇒ add_fresh_to_graph (s (Ainstack i) [[ ]]) f |
---|
163 | | _ ⇒ Error ? (* int and float constants are nonsense here *) |
---|
164 | ] |
---|
165 | | Op2 op e1 e2 ⇒ |
---|
166 | match op with |
---|
167 | [ Oaddp ⇒ |
---|
168 | let add_generic_addp : unit → res internal_function ≝ λ_. |
---|
169 | do 〈r1, f〉 ← choose_reg env e1 ptrs f; |
---|
170 | do 〈r2, f〉 ← choose_reg env e2 ptrs f; |
---|
171 | do f ← add_fresh_to_graph (s Aindexed2 [[ r1 ; r2 ]]) f; |
---|
172 | do f ← add_expr env e2 r2 ptrs f; |
---|
173 | add_expr env e1 r1 ptrs f |
---|
174 | in |
---|
175 | match e1 with |
---|
176 | [ Cst c ⇒ |
---|
177 | match c with |
---|
178 | [ Oaddrsymbol id i ⇒ |
---|
179 | do 〈r, f〉 ← choose_reg env e ptrs f; |
---|
180 | do f ← add_fresh_to_graph (s (Abased id i) [[ r ]]) f; |
---|
181 | add_expr env e2 r ptrs f |
---|
182 | | _ ⇒ add_generic_addp it |
---|
183 | ] |
---|
184 | | _ ⇒ add_generic_addp it |
---|
185 | ] |
---|
186 | | _ ⇒ add_default it |
---|
187 | ] |
---|
188 | | _ ⇒ add_default it |
---|
189 | ] |
---|
190 | (* and again *) |
---|
191 | and add_branch_internal (env:env) (e:expr) (ltrue:label) (lfalse:label) (ptrs:list ident) (f:internal_function) |
---|
192 | (termination_hack_add_expr : register → list ident → internal_function → res internal_function) on e : res internal_function ≝ |
---|
193 | match e with |
---|
194 | [ Id i ⇒ |
---|
195 | do r ← opt_to_res … (lookup ?? env i); |
---|
196 | add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f |
---|
197 | | Cst c ⇒ |
---|
198 | add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f |
---|
199 | | Op1 op e' ⇒ |
---|
200 | do 〈r,f〉 ← choose_reg env e' ptrs f; |
---|
201 | do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f; |
---|
202 | add_expr env e' r ptrs f |
---|
203 | | Op2 op e1 e2 ⇒ |
---|
204 | do 〈r1,f〉 ← choose_reg env e1 ptrs f; |
---|
205 | do 〈r2,f〉 ← choose_reg env e2 ptrs f; |
---|
206 | do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f; |
---|
207 | do f ← add_expr env e2 r2 ptrs f; |
---|
208 | add_expr env e1 r1 ptrs f |
---|
209 | | _ ⇒ |
---|
210 | do 〈r,f〉 ← choose_reg env e ptrs f; |
---|
211 | do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f; |
---|
212 | termination_hack_add_expr r ptrs f |
---|
213 | ]. |
---|
214 | |
---|
215 | (* See comment above. *) |
---|
216 | definition add_with_addressing ≝ |
---|
217 | λenv,e,s,ptrs,f. add_with_addressing_internal env e s ptrs f (add_expr env e). |
---|
218 | definition add_branch ≝ |
---|
219 | λenv,e,ltrue,lfalse,ptrs,f. add_branch_internal env e ltrue lfalse ptrs f (add_expr env e). |
---|
220 | |
---|
221 | let rec add_exprs (env:env) (es:list expr) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝ |
---|
222 | match es with |
---|
223 | [ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? ] |
---|
224 | | cons e et ⇒ |
---|
225 | match dsts with |
---|
226 | [ nil ⇒ Error ? |
---|
227 | | cons r rt ⇒ |
---|
228 | do f ← add_exprs env et rt ptrs f; |
---|
229 | add_expr env e r ptrs f |
---|
230 | ] |
---|
231 | ]. |
---|
232 | |
---|
233 | let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (ptrs:list ident) (f:internal_function) on s : res internal_function ≝ |
---|
234 | match s with |
---|
235 | [ St_skip ⇒ OK ? f |
---|
236 | | St_assign x e ⇒ |
---|
237 | do dst ← opt_to_res … (lookup ?? env x); |
---|
238 | add_expr env e dst ptrs f |
---|
239 | | St_store q e1 e2 ⇒ |
---|
240 | do 〈val_reg, f〉 ← choose_reg env e2 ptrs f; |
---|
241 | do f ← add_with_addressing env e1 (λm,rs. St_store q m rs val_reg) ptrs f; |
---|
242 | add_expr env e2 val_reg ptrs f |
---|
243 | | St_call return_opt_id e args sig ⇒ |
---|
244 | do return_opt_reg ← |
---|
245 | match return_opt_id with |
---|
246 | [ None ⇒ OK ? (None ?) |
---|
247 | | Some id ⇒ do r ← opt_to_res … (lookup ?? env id); OK ? (Some ? r) |
---|
248 | ]; |
---|
249 | do 〈args_regs, f〉 ← choose_regs env args ptrs f; |
---|
250 | do f ← |
---|
251 | match e with |
---|
252 | [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg sig) f |
---|
253 | | _ ⇒ |
---|
254 | do 〈fnr, f〉 ← choose_reg env e ptrs f; |
---|
255 | do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg sig) f; |
---|
256 | add_expr env e fnr ptrs f |
---|
257 | ]; |
---|
258 | add_exprs env args args_regs ptrs f |
---|
259 | | St_tailcall e args sig ⇒ |
---|
260 | do 〈args_regs, f〉 ← choose_regs env args ptrs f; |
---|
261 | do f ← |
---|
262 | match e with |
---|
263 | [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs sig) f |
---|
264 | | _ ⇒ |
---|
265 | do 〈fnr, f〉 ← choose_reg env e ptrs f; |
---|
266 | do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs sig) f; |
---|
267 | add_expr env e fnr ptrs f |
---|
268 | ]; |
---|
269 | add_exprs env args args_regs ptrs f |
---|
270 | | St_seq s1 s2 ⇒ |
---|
271 | do f ← add_stmt env label_env s2 exits ptrs f; |
---|
272 | add_stmt env label_env s1 exits ptrs f |
---|
273 | | St_ifthenelse e s1 s2 ⇒ |
---|
274 | let l_next ≝ f_entry f in |
---|
275 | do f ← add_stmt env label_env s2 exits ptrs f; |
---|
276 | let l2 ≝ f_entry f in |
---|
277 | do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f; |
---|
278 | do f ← add_stmt env label_env s1 exits ptrs f; |
---|
279 | add_branch env e (f_entry f) l2 ptrs f |
---|
280 | | St_loop s ⇒ |
---|
281 | do f ← add_loop_label_to_graph f; |
---|
282 | let l_loop ≝ f_entry f in |
---|
283 | do f ← add_stmt env label_env s exits ptrs f; |
---|
284 | OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f) |
---|
285 | | St_block s ⇒ |
---|
286 | add_stmt env label_env s ((f_entry f)::exits) ptrs f |
---|
287 | | St_exit n ⇒ |
---|
288 | do l ← opt_to_res … (nth_opt ? n exits); |
---|
289 | add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f |
---|
290 | | St_switch e tab n ⇒ |
---|
291 | do 〈r,f〉 ← choose_reg env e ptrs f; |
---|
292 | do l_default ← opt_to_res … (nth_opt ? n exits); |
---|
293 | do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f; |
---|
294 | do f ← foldr ?? (λcs,f. |
---|
295 | do f ← f; |
---|
296 | let 〈i,n〉 ≝ cs in |
---|
297 | do 〈cr,f〉 ← fresh_reg … f; |
---|
298 | do l_case ← opt_to_res … (nth_opt ? n exits); |
---|
299 | do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f; |
---|
300 | add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab; |
---|
301 | add_expr env e r ptrs f |
---|
302 | | St_return opt_e ⇒ |
---|
303 | do f ← add_fresh_to_graph (λ_. St_return) f; |
---|
304 | match opt_e with |
---|
305 | [ None ⇒ OK ? f |
---|
306 | | Some e ⇒ |
---|
307 | match f_result f with |
---|
308 | [ None ⇒ Error ? |
---|
309 | | Some r ⇒ add_expr env e r ptrs f |
---|
310 | ] |
---|
311 | ] |
---|
312 | | St_label l s' ⇒ |
---|
313 | do f ← add_stmt env label_env s' exits ptrs f; |
---|
314 | do l' ← opt_to_res … (lookup ?? label_env l); |
---|
315 | OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f) |
---|
316 | | St_goto l ⇒ |
---|
317 | do l' ← opt_to_res … (lookup ?? label_env l); |
---|
318 | add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f |
---|
319 | | St_cost l s' ⇒ |
---|
320 | do f ← add_stmt env label_env s' exits ptrs f; |
---|
321 | add_fresh_to_graph (St_cost l) f |
---|
322 | ]. |
---|
323 | [ @(λ_. St_skip l_next) |
---|
324 | | @(St_skip (f_entry f)) |
---|
325 | | @(λ_. St_skip l) |
---|
326 | | @(λ_. St_skip l_default) |
---|
327 | | @(St_skip (f_entry f)) |
---|
328 | | @(λ_.St_skip l') |
---|
329 | ] qed. |
---|
330 | |
---|
331 | (* Get labels from a Cminor statement. *) |
---|
332 | let rec labels_of (s:stmt) : list ident ≝ |
---|
333 | match s with |
---|
334 | [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2) |
---|
335 | | St_ifthenelse _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2) |
---|
336 | | St_loop s ⇒ labels_of s |
---|
337 | | St_block s ⇒ labels_of s |
---|
338 | | St_label l s ⇒ l::(labels_of s) |
---|
339 | | St_cost _ s ⇒ labels_of s |
---|
340 | | _ ⇒ [ ] |
---|
341 | ]. |
---|
342 | |
---|
343 | definition c2ra_function (*: internal_function → internal_function*) ≝ |
---|
344 | λf. |
---|
345 | let labgen0 ≝ new_universe LabelTag in |
---|
346 | let reggen0 ≝ new_universe RegisterTag in |
---|
347 | let cminor_labels ≝ labels_of (f_body f) in |
---|
348 | do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f); |
---|
349 | do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f); |
---|
350 | do 〈result, locals, reggen〉 ← |
---|
351 | match sig_res (f_sig f) with |
---|
352 | [ None ⇒ OK ? 〈None ?, locals0, reggen2〉 |
---|
353 | | Some _ ⇒ |
---|
354 | do 〈r,gen〉 ← fresh … reggen2; |
---|
355 | OK ? 〈Some ? r, r::locals0, gen〉 ]; |
---|
356 | do ptrs ← mmap ?? (λid. opt_to_res … (lookup ?? env id)) (f_ptrs f); |
---|
357 | do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels; |
---|
358 | do 〈l,labgen〉 ← fresh … labgen1; |
---|
359 | let emptyfn ≝ |
---|
360 | mk_internal_function |
---|
361 | labgen |
---|
362 | reggen |
---|
363 | (f_sig f) |
---|
364 | result |
---|
365 | params |
---|
366 | locals |
---|
367 | ptrs |
---|
368 | (f_stacksize f) |
---|
369 | (add ?? (empty_map …) l St_return) |
---|
370 | l |
---|
371 | l in |
---|
372 | add_stmt env label_env (f_body f) [ ] (f_ptrs f) emptyfn |
---|
373 | . |
---|
374 | |
---|
375 | definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝ |
---|
376 | transform_partial_program ??? |
---|
377 | (transf_partial_fundef ?? c2ra_function). |
---|
378 | |
---|
379 | include "Cminor/initialisation.ma". |
---|
380 | |
---|
381 | definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝ |
---|
382 | λp. let p' ≝ replace_init p in cminor_to_rtlabs p. |
---|