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 choose_reg : env → expr → internal_function → res (register × internal_function) ≝ |
---|
63 | λenv,e,f. |
---|
64 | match e with |
---|
65 | [ Id i ⇒ |
---|
66 | do r ← opt_to_res … (lookup … env i); |
---|
67 | OK ? 〈r, f〉 |
---|
68 | | _ ⇒ fresh_reg f (* FIXME: add to pointers list if necessary *) |
---|
69 | ]. |
---|
70 | |
---|
71 | definition choose_regs : env → list expr → internal_function → res (list register × internal_function) ≝ |
---|
72 | λenv,es,f. |
---|
73 | foldr ?? (λe,acc. do 〈rs,f〉 ← acc; |
---|
74 | do 〈r,f'〉 ← choose_reg env e f; |
---|
75 | OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es. |
---|
76 | |
---|
77 | let rec add_expr (env:env) (e:expr) (dst:register) (f:internal_function) on e: res internal_function ≝ |
---|
78 | match e with |
---|
79 | [ Id i ⇒ |
---|
80 | do r ← opt_to_res … (lookup ?? env i); |
---|
81 | match register_eq r dst with |
---|
82 | [ inl _ ⇒ OK ? f |
---|
83 | | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f |
---|
84 | ] |
---|
85 | | Cst c ⇒ add_fresh_to_graph (St_const dst c) f |
---|
86 | | Op1 op e' ⇒ |
---|
87 | do 〈r,f〉 ← choose_reg env e' f; |
---|
88 | do f ← add_fresh_to_graph (St_op1 op dst r) f; |
---|
89 | add_expr env e' r f |
---|
90 | | Op2 op e1 e2 ⇒ |
---|
91 | do 〈r1,f〉 ← choose_reg env e1 f; |
---|
92 | do 〈r2,f〉 ← choose_reg env e2 f; |
---|
93 | do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f; |
---|
94 | do f ← add_expr env e2 r2 f; |
---|
95 | add_expr env e1 r1 f |
---|
96 | | Mem q e' ⇒ |
---|
97 | (* FIXME: inefficient - make proper use of addressing *) |
---|
98 | do 〈r, f〉 ← choose_reg env e' f; |
---|
99 | do f ← add_fresh_to_graph (St_load q (Aindexed zero) [[ r ]] dst) f; |
---|
100 | add_expr env e' r f |
---|
101 | | Cond e' e1 e2 ⇒ |
---|
102 | let resume_at ≝ f_entry f in |
---|
103 | do f ← add_expr env e2 dst f; |
---|
104 | let lfalse ≝ f_entry f in |
---|
105 | do f ← add_fresh_to_graph (λ_.St_skip resume_at) f; |
---|
106 | do f ← add_expr env e1 dst f; |
---|
107 | add_branch_internal env e' (f_entry f) lfalse f (add_expr env e') |
---|
108 | | Ecost l e' ⇒ |
---|
109 | do f ← add_expr env e' dst f; |
---|
110 | add_fresh_to_graph (St_cost l) f |
---|
111 | |
---|
112 | (* Ugh, the termination checker isn't smart enough to notice that calling |
---|
113 | add_expr with e is OK, so we take it partially applied and define a proper |
---|
114 | add_branch afterwards. *) |
---|
115 | ] and add_branch_internal (env:env) (e:expr) (ltrue:label) (lfalse:label) (f:internal_function) |
---|
116 | (termination_hack_add_expr : register → internal_function → res internal_function) on e : res internal_function ≝ |
---|
117 | match e with |
---|
118 | [ Id i ⇒ |
---|
119 | do r ← opt_to_res … (lookup ?? env i); |
---|
120 | add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f |
---|
121 | | Cst c ⇒ |
---|
122 | add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f |
---|
123 | | Op1 op e' ⇒ |
---|
124 | do 〈r,f〉 ← choose_reg env e' f; |
---|
125 | do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f; |
---|
126 | add_expr env e' r f |
---|
127 | | Op2 op e1 e2 ⇒ |
---|
128 | do 〈r1,f〉 ← choose_reg env e1 f; |
---|
129 | do 〈r2,f〉 ← choose_reg env e2 f; |
---|
130 | do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f; |
---|
131 | do f ← add_expr env e2 r2 f; |
---|
132 | add_expr env e1 r1 f |
---|
133 | | _ ⇒ |
---|
134 | do 〈r,f〉 ← choose_reg env e f; |
---|
135 | do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f; |
---|
136 | termination_hack_add_expr r f |
---|
137 | ]. |
---|
138 | |
---|
139 | (* See add_branch_internal above. *) |
---|
140 | definition add_branch ≝ |
---|
141 | λenv,e,ltrue,lfalse,f. add_branch_internal env e ltrue lfalse f (add_expr env e). |
---|
142 | |
---|
143 | let rec add_exprs (env:env) (es:list expr) (dsts:list register) (f:internal_function) on es: res internal_function ≝ |
---|
144 | match es with |
---|
145 | [ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? ] |
---|
146 | | cons e et ⇒ |
---|
147 | match dsts with |
---|
148 | [ nil ⇒ Error ? |
---|
149 | | cons r rt ⇒ |
---|
150 | do f ← add_exprs env et rt f; |
---|
151 | add_expr env e r f |
---|
152 | ] |
---|
153 | ]. |
---|
154 | |
---|
155 | let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (f:internal_function) on s : res internal_function ≝ |
---|
156 | match s with |
---|
157 | [ St_skip ⇒ OK ? f |
---|
158 | | St_assign x e ⇒ |
---|
159 | do dst ← opt_to_res … (lookup ?? env x); |
---|
160 | add_expr env e dst f |
---|
161 | | St_store q e1 e2 ⇒ |
---|
162 | (* FIXME: inefficient - make proper use of addressing *) |
---|
163 | do 〈addr_reg, f〉 ← choose_reg env e1 f; |
---|
164 | do 〈val_reg, f〉 ← choose_reg env e2 f; |
---|
165 | do f ← add_fresh_to_graph (St_store q (Aindexed zero) [[ addr_reg ]] val_reg) f; |
---|
166 | do f ← add_expr env e1 addr_reg f; |
---|
167 | add_expr env e2 val_reg f |
---|
168 | | St_call return_opt_id e args sig ⇒ |
---|
169 | do return_opt_reg ← |
---|
170 | match return_opt_id with |
---|
171 | [ None ⇒ OK ? (None ?) |
---|
172 | | Some id ⇒ do r ← opt_to_res … (lookup ?? env id); OK ? (Some ? r) |
---|
173 | ]; |
---|
174 | do 〈args_regs, f〉 ← choose_regs env args f; |
---|
175 | do f ← |
---|
176 | match e with |
---|
177 | [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg sig) f |
---|
178 | | _ ⇒ |
---|
179 | do 〈fnr, f〉 ← choose_reg env e f; |
---|
180 | do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg sig) f; |
---|
181 | add_expr env e fnr f |
---|
182 | ]; |
---|
183 | add_exprs env args args_regs f |
---|
184 | | St_tailcall e args sig ⇒ |
---|
185 | do 〈args_regs, f〉 ← choose_regs env args f; |
---|
186 | do f ← |
---|
187 | match e with |
---|
188 | [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs sig) f |
---|
189 | | _ ⇒ |
---|
190 | do 〈fnr, f〉 ← choose_reg env e f; |
---|
191 | do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs sig) f; |
---|
192 | add_expr env e fnr f |
---|
193 | ]; |
---|
194 | add_exprs env args args_regs f |
---|
195 | | St_seq s1 s2 ⇒ |
---|
196 | do f ← add_stmt env label_env s2 exits f; |
---|
197 | add_stmt env label_env s1 exits f |
---|
198 | | St_ifthenelse e s1 s2 ⇒ |
---|
199 | let l_next ≝ f_entry f in |
---|
200 | do f ← add_stmt env label_env s2 exits f; |
---|
201 | let l2 ≝ f_entry f in |
---|
202 | do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f; |
---|
203 | do f ← add_stmt env label_env s1 exits f; |
---|
204 | add_branch env e (f_entry f) l2 f |
---|
205 | | St_loop s ⇒ |
---|
206 | do f ← add_loop_label_to_graph f; |
---|
207 | let l_loop ≝ f_entry f in |
---|
208 | do f ← add_stmt env label_env s exits f; |
---|
209 | OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f) |
---|
210 | | St_block s ⇒ |
---|
211 | add_stmt env label_env s ((f_entry f)::exits) f |
---|
212 | | St_exit n ⇒ |
---|
213 | do l ← opt_to_res … (nth_opt ? n exits); |
---|
214 | add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f |
---|
215 | | St_switch e tab n ⇒ Error ? (* FIXME: implement *) |
---|
216 | | St_return opt_e ⇒ |
---|
217 | do f ← add_fresh_to_graph (λ_. St_return) f; |
---|
218 | match opt_e with |
---|
219 | [ None ⇒ OK ? f |
---|
220 | | Some e ⇒ |
---|
221 | match f_result f with |
---|
222 | [ None ⇒ Error ? |
---|
223 | | Some r ⇒ add_expr env e r f |
---|
224 | ] |
---|
225 | ] |
---|
226 | | St_label l s' ⇒ |
---|
227 | do f ← add_stmt env label_env s' exits f; |
---|
228 | do l' ← opt_to_res … (lookup ?? label_env l); |
---|
229 | OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f) |
---|
230 | | St_goto l ⇒ |
---|
231 | do l' ← opt_to_res … (lookup ?? label_env l); |
---|
232 | add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f |
---|
233 | | St_cost l s' ⇒ |
---|
234 | do f ← add_stmt env label_env s' exits f; |
---|
235 | add_fresh_to_graph (St_cost l) f |
---|
236 | | _ ⇒ Error ? (* XXX implement *) |
---|
237 | ]. |
---|
238 | [ @(λ_. St_skip l_next) |
---|
239 | | @(St_skip (f_entry f)) |
---|
240 | | @(λ_. St_skip l) |
---|
241 | | @(St_skip (f_entry f)) |
---|
242 | | @(λ_.St_skip l') |
---|
243 | ] qed. |
---|
244 | |
---|
245 | (* Get labels from a Cminor statement. *) |
---|
246 | let rec labels_of (s:stmt) : list ident ≝ |
---|
247 | match s with |
---|
248 | [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2) |
---|
249 | | St_ifthenelse _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2) |
---|
250 | | St_loop s ⇒ labels_of s |
---|
251 | | St_block s ⇒ labels_of s |
---|
252 | | St_label l s ⇒ l::(labels_of s) |
---|
253 | | St_cost _ s ⇒ labels_of s |
---|
254 | | _ ⇒ [ ] |
---|
255 | ]. |
---|
256 | |
---|
257 | definition c2ra_function (*: internal_function → internal_function*) ≝ |
---|
258 | λf. |
---|
259 | let labgen0 ≝ new_universe LabelTag in |
---|
260 | let reggen0 ≝ new_universe RegisterTag in |
---|
261 | let cminor_labels ≝ labels_of (f_body f) in |
---|
262 | do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f); |
---|
263 | do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f); |
---|
264 | do 〈result, locals, reggen〉 ← |
---|
265 | match sig_res (f_sig f) with |
---|
266 | [ None ⇒ OK ? 〈None ?, locals0, reggen2〉 |
---|
267 | | Some _ ⇒ |
---|
268 | do 〈r,gen〉 ← fresh … reggen2; |
---|
269 | OK ? 〈Some ? r, r::locals0, gen〉 ]; |
---|
270 | do ptrs ← mmap ?? (λid. opt_to_res … (lookup ?? env id)) (f_ptrs f); |
---|
271 | do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels; |
---|
272 | do 〈l,labgen〉 ← fresh … labgen1; |
---|
273 | let emptyfn ≝ |
---|
274 | mk_internal_function |
---|
275 | labgen |
---|
276 | reggen |
---|
277 | (f_sig f) |
---|
278 | result |
---|
279 | params |
---|
280 | locals |
---|
281 | ptrs |
---|
282 | (f_stacksize f) |
---|
283 | (add ?? (empty_map …) l St_return) |
---|
284 | l |
---|
285 | l in |
---|
286 | add_stmt env label_env (f_body f) [ ] emptyfn |
---|
287 | . |
---|
288 | |
---|
289 | definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝ |
---|
290 | transform_partial_program ??? |
---|
291 | (transf_partial_fundef ?? c2ra_function). |
---|
292 | |
---|
293 | include "Cminor/initialisation.ma". |
---|
294 | |
---|
295 | definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝ |
---|
296 | λp. let p' ≝ replace_init p in cminor_to_rtlabs p. |
---|