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 (ty:typ) (e:expr ty) (ptrs:list ident) on e : 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 | axiom UnknownVariable : String. |
---|
96 | |
---|
97 | definition choose_reg : env → ∀t.expr t → list ident → internal_function → res (register × internal_function) ≝ |
---|
98 | λenv,ty,e,ptrs,f. |
---|
99 | match e with |
---|
100 | [ Id _ i ⇒ |
---|
101 | do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup … env i); |
---|
102 | OK ? 〈r, f〉 |
---|
103 | | _ ⇒ |
---|
104 | if expr_yields_pointer ? e ptrs then fresh_ptr_reg f else fresh_reg f |
---|
105 | ]. |
---|
106 | |
---|
107 | definition choose_regs : env → list (Σt:typ.expr t) → list ident → internal_function → res (list register × internal_function) ≝ |
---|
108 | λenv,es,ptrs,f. |
---|
109 | foldr (Σt:typ.expr t) ? |
---|
110 | (λe,acc. do 〈rs,f〉 ← acc; |
---|
111 | do 〈r,f'〉 ← match e with [ dp t e ⇒ choose_reg env t e ptrs f ]; |
---|
112 | OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es. |
---|
113 | |
---|
114 | axiom BadCminorProgram : String. |
---|
115 | |
---|
116 | let rec add_expr (env:env) (ty:typ) (e:expr ty) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝ |
---|
117 | match e with |
---|
118 | [ Id _ i ⇒ |
---|
119 | do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i); |
---|
120 | match register_eq r dst with |
---|
121 | [ inl _ ⇒ OK ? f |
---|
122 | | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f |
---|
123 | ] |
---|
124 | | Cst _ c ⇒ add_fresh_to_graph (St_const dst c) f |
---|
125 | | Op1 _ _ op e' ⇒ |
---|
126 | do 〈r,f〉 ← choose_reg env ? e' ptrs f; |
---|
127 | do f ← add_fresh_to_graph (St_op1 op dst r) f; |
---|
128 | add_expr env ? e' r ptrs f |
---|
129 | | Op2 _ _ _ op e1 e2 ⇒ |
---|
130 | do 〈r1,f〉 ← choose_reg env ? e1 ptrs f; |
---|
131 | do 〈r2,f〉 ← choose_reg env ? e2 ptrs f; |
---|
132 | do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f; |
---|
133 | do f ← add_expr env ? e2 r2 ptrs f; |
---|
134 | add_expr env ? e1 r1 ptrs f |
---|
135 | | Mem _ q e' ⇒ |
---|
136 | add_with_addressing_internal env ? e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env ? e') |
---|
137 | | Cond _ _ _ e' e1 e2 ⇒ |
---|
138 | let resume_at ≝ f_entry f in |
---|
139 | do f ← add_expr env ? e2 dst ptrs f; |
---|
140 | let lfalse ≝ f_entry f in |
---|
141 | do f ← add_fresh_to_graph (λ_.St_skip resume_at) f; |
---|
142 | do f ← add_expr env ? e1 dst ptrs f; |
---|
143 | add_branch_internal env ? e' (f_entry f) lfalse ptrs f (add_expr env ? e') |
---|
144 | | Ecost _ l e' ⇒ |
---|
145 | do f ← add_expr env ? e' dst ptrs f; |
---|
146 | add_fresh_to_graph (St_cost l) f |
---|
147 | |
---|
148 | (* Ugh, the termination checker isn't smart enough to notice that calling |
---|
149 | add_expr with e is OK, so we take it partially applied and define a proper |
---|
150 | add_<whatever> afterwards. *) |
---|
151 | ] |
---|
152 | and add_with_addressing_internal (env:env) (ty:typ) (e:expr ty) |
---|
153 | (s:∀m:addressing. addr m → label → statement) |
---|
154 | (ptrs:list ident) |
---|
155 | (f:internal_function) |
---|
156 | (termination_hack:register → list ident → internal_function → res internal_function) |
---|
157 | on e : res internal_function ≝ |
---|
158 | let add_default : unit → res internal_function ≝ λ_. |
---|
159 | do 〈r, f〉 ← choose_reg env ? e ptrs f; |
---|
160 | do f ← add_fresh_to_graph (s (Aindexed zero) [[ r ]]) f; |
---|
161 | termination_hack r ptrs f |
---|
162 | in |
---|
163 | match e with |
---|
164 | [ Cst _ c ⇒ |
---|
165 | match c with |
---|
166 | [ Oaddrsymbol id i ⇒ add_fresh_to_graph (s (Aglobal id i) [[ ]]) f |
---|
167 | | Oaddrstack i ⇒ add_fresh_to_graph (s (Ainstack i) [[ ]]) f |
---|
168 | | _ ⇒ Error ? (msg BadCminorProgram) (* int and float constants are nonsense here *) |
---|
169 | ] |
---|
170 | | Op2 _ _ _ op e1 e2 ⇒ |
---|
171 | match op with |
---|
172 | [ Oaddp ⇒ |
---|
173 | let add_generic_addp : unit → res internal_function ≝ λ_. |
---|
174 | do 〈r1, f〉 ← choose_reg env ? e1 ptrs f; |
---|
175 | do 〈r2, f〉 ← choose_reg env ? e2 ptrs f; |
---|
176 | do f ← add_fresh_to_graph (s Aindexed2 [[ r1 ; r2 ]]) f; |
---|
177 | do f ← add_expr env ? e2 r2 ptrs f; |
---|
178 | add_expr env ? e1 r1 ptrs f |
---|
179 | in |
---|
180 | match e1 with |
---|
181 | [ Cst _ c ⇒ |
---|
182 | match c with |
---|
183 | [ Oaddrsymbol id i ⇒ |
---|
184 | do 〈r, f〉 ← choose_reg env ? e ptrs f; |
---|
185 | do f ← add_fresh_to_graph (s (Abased id i) [[ r ]]) f; |
---|
186 | add_expr env ? e2 r ptrs f |
---|
187 | | _ ⇒ add_generic_addp it |
---|
188 | ] |
---|
189 | | _ ⇒ add_generic_addp it |
---|
190 | ] |
---|
191 | | _ ⇒ add_default it |
---|
192 | ] |
---|
193 | | _ ⇒ add_default it |
---|
194 | ] |
---|
195 | (* and again *) |
---|
196 | and add_branch_internal (env:env) (ty:typ) (e:expr ty) (ltrue:label) (lfalse:label) (ptrs:list ident) (f:internal_function) |
---|
197 | (termination_hack_add_expr : register → list ident → internal_function → res internal_function) on e : res internal_function ≝ |
---|
198 | match e with |
---|
199 | [ Id _ i ⇒ |
---|
200 | do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i); |
---|
201 | add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f |
---|
202 | | Cst _ c ⇒ |
---|
203 | add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f |
---|
204 | | Op1 _ _ op e' ⇒ |
---|
205 | do 〈r,f〉 ← choose_reg env ? e' ptrs f; |
---|
206 | do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f; |
---|
207 | add_expr env ? e' r ptrs f |
---|
208 | | Op2 _ _ _ op e1 e2 ⇒ |
---|
209 | do 〈r1,f〉 ← choose_reg env ? e1 ptrs f; |
---|
210 | do 〈r2,f〉 ← choose_reg env ? e2 ptrs f; |
---|
211 | do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f; |
---|
212 | do f ← add_expr env ? e2 r2 ptrs f; |
---|
213 | add_expr env ? e1 r1 ptrs f |
---|
214 | | _ ⇒ |
---|
215 | do 〈r,f〉 ← choose_reg env ? e ptrs f; |
---|
216 | do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f; |
---|
217 | termination_hack_add_expr r ptrs f |
---|
218 | ]. |
---|
219 | |
---|
220 | (* See comment above. *) |
---|
221 | definition add_with_addressing ≝ |
---|
222 | λenv,ty,e,s,ptrs,f. add_with_addressing_internal env ty e s ptrs f (add_expr env ty e). |
---|
223 | definition add_branch ≝ |
---|
224 | λenv,ty,e,ltrue,lfalse,ptrs,f. add_branch_internal env ty e ltrue lfalse ptrs f (add_expr env ty e). |
---|
225 | |
---|
226 | (* This shouldn't occur; maybe use vectors? *) |
---|
227 | axiom WrongNumberOfArguments : String. |
---|
228 | |
---|
229 | let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝ |
---|
230 | match es with |
---|
231 | [ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ] |
---|
232 | | cons e et ⇒ |
---|
233 | match dsts with |
---|
234 | [ nil ⇒ Error ? (msg WrongNumberOfArguments) |
---|
235 | | cons r rt ⇒ |
---|
236 | do f ← add_exprs env et rt ptrs f; |
---|
237 | match e with [ dp ty e ⇒ add_expr env ty e r ptrs f ] |
---|
238 | ] |
---|
239 | ]. |
---|
240 | |
---|
241 | axiom UnknownLabel : String. |
---|
242 | axiom ReturnMismatch : String. |
---|
243 | |
---|
244 | 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 ≝ |
---|
245 | match s with |
---|
246 | [ St_skip ⇒ OK ? f |
---|
247 | | St_assign _ x e ⇒ |
---|
248 | do dst ← opt_to_res … [MSG UnknownVariable; CTX ? x] (lookup ?? env x); |
---|
249 | add_expr env ? e dst ptrs f |
---|
250 | | St_store _ q e1 e2 ⇒ |
---|
251 | do 〈val_reg, f〉 ← choose_reg env ? e2 ptrs f; |
---|
252 | do f ← add_with_addressing env ? e1 (λm,rs. St_store q m rs val_reg) ptrs f; |
---|
253 | add_expr env ? e2 val_reg ptrs f |
---|
254 | | St_call return_opt_id e args ⇒ |
---|
255 | do return_opt_reg ← |
---|
256 | match return_opt_id with |
---|
257 | [ None ⇒ OK ? (None ?) |
---|
258 | | Some id ⇒ do r ← opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id); OK ? (Some ? r) |
---|
259 | ]; |
---|
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_call_id id args_regs return_opt_reg) f |
---|
264 | | _ ⇒ |
---|
265 | do 〈fnr, f〉 ← choose_reg env ? e ptrs f; |
---|
266 | do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f; |
---|
267 | add_expr env ? e fnr ptrs f |
---|
268 | ]; |
---|
269 | add_exprs env args args_regs ptrs f |
---|
270 | | St_tailcall e args ⇒ |
---|
271 | do 〈args_regs, f〉 ← choose_regs env args ptrs f; |
---|
272 | do f ← |
---|
273 | match e with |
---|
274 | [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f |
---|
275 | | _ ⇒ |
---|
276 | do 〈fnr, f〉 ← choose_reg env ? e ptrs f; |
---|
277 | do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f; |
---|
278 | add_expr env ? e fnr ptrs f |
---|
279 | ]; |
---|
280 | add_exprs env args args_regs ptrs f |
---|
281 | | St_seq s1 s2 ⇒ |
---|
282 | do f ← add_stmt env label_env s2 exits ptrs f; |
---|
283 | add_stmt env label_env s1 exits ptrs f |
---|
284 | | St_ifthenelse _ _ e s1 s2 ⇒ |
---|
285 | let l_next ≝ f_entry f in |
---|
286 | do f ← add_stmt env label_env s2 exits ptrs f; |
---|
287 | let l2 ≝ f_entry f in |
---|
288 | do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f; |
---|
289 | do f ← add_stmt env label_env s1 exits ptrs f; |
---|
290 | add_branch env ? e (f_entry f) l2 ptrs f |
---|
291 | | St_loop s ⇒ |
---|
292 | do f ← add_loop_label_to_graph f; |
---|
293 | let l_loop ≝ f_entry f in |
---|
294 | do f ← add_stmt env label_env s exits ptrs f; |
---|
295 | OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f) |
---|
296 | | St_block s ⇒ |
---|
297 | add_stmt env label_env s ((f_entry f)::exits) ptrs f |
---|
298 | | St_exit n ⇒ |
---|
299 | do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); |
---|
300 | add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f |
---|
301 | | St_switch _ _ e tab n ⇒ |
---|
302 | do 〈r,f〉 ← choose_reg env ? e ptrs f; |
---|
303 | do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); |
---|
304 | do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f; |
---|
305 | do f ← foldr ?? (λcs,f. |
---|
306 | do f ← f; |
---|
307 | let 〈i,n〉 ≝ cs in |
---|
308 | do 〈cr,f〉 ← fresh_reg … f; |
---|
309 | do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); |
---|
310 | do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f; |
---|
311 | add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab; |
---|
312 | add_expr env ? e r ptrs f |
---|
313 | | St_return opt_e ⇒ |
---|
314 | do f ← add_fresh_to_graph (λ_. St_return) f; |
---|
315 | match opt_e with |
---|
316 | [ None ⇒ OK ? f |
---|
317 | | Some e ⇒ |
---|
318 | match f_result f with |
---|
319 | [ None ⇒ Error ? (msg ReturnMismatch) |
---|
320 | | Some r ⇒ match e with [ dp ty e ⇒ add_expr env ? e r ptrs f ] |
---|
321 | ] |
---|
322 | ] |
---|
323 | | St_label l s' ⇒ |
---|
324 | do f ← add_stmt env label_env s' exits ptrs f; |
---|
325 | do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l); |
---|
326 | OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f) |
---|
327 | | St_goto l ⇒ |
---|
328 | do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l); |
---|
329 | add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f |
---|
330 | | St_cost l s' ⇒ |
---|
331 | do f ← add_stmt env label_env s' exits ptrs f; |
---|
332 | add_fresh_to_graph (St_cost l) f |
---|
333 | ]. |
---|
334 | [ @(λ_. St_skip l_next) |
---|
335 | | @(St_skip (f_entry f)) |
---|
336 | | @(λ_. St_skip l) |
---|
337 | | @(λ_. St_skip l_default) |
---|
338 | | @(St_skip (f_entry f)) |
---|
339 | | @(λ_.St_skip l') |
---|
340 | ] qed. |
---|
341 | |
---|
342 | (* Get labels from a Cminor statement. *) |
---|
343 | let rec labels_of (s:stmt) : list ident ≝ |
---|
344 | match s with |
---|
345 | [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2) |
---|
346 | | St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2) |
---|
347 | | St_loop s ⇒ labels_of s |
---|
348 | | St_block s ⇒ labels_of s |
---|
349 | | St_label l s ⇒ l::(labels_of s) |
---|
350 | | St_cost _ s ⇒ labels_of s |
---|
351 | | _ ⇒ [ ] |
---|
352 | ]. |
---|
353 | |
---|
354 | definition c2ra_function (*: internal_function → internal_function*) ≝ |
---|
355 | λf. |
---|
356 | let labgen0 ≝ new_universe LabelTag in |
---|
357 | let reggen0 ≝ new_universe RegisterTag in |
---|
358 | let cminor_labels ≝ labels_of (f_body f) in |
---|
359 | do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f); |
---|
360 | do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f); |
---|
361 | do 〈result, locals, reggen〉 ← |
---|
362 | match sig_res (f_sig f) with |
---|
363 | [ None ⇒ OK ? 〈None ?, locals0, reggen2〉 |
---|
364 | | Some _ ⇒ |
---|
365 | do 〈r,gen〉 ← fresh … reggen2; |
---|
366 | OK ? 〈Some ? r, r::locals0, gen〉 ]; |
---|
367 | do ptrs ← mmap ?? (λid. opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id)) (f_ptrs f); |
---|
368 | do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels; |
---|
369 | do 〈l,labgen〉 ← fresh … labgen1; |
---|
370 | let emptyfn ≝ |
---|
371 | mk_internal_function |
---|
372 | labgen |
---|
373 | reggen |
---|
374 | (f_sig f) |
---|
375 | result |
---|
376 | params |
---|
377 | locals |
---|
378 | ptrs |
---|
379 | (f_stacksize f) |
---|
380 | (add ?? (empty_map …) l St_return) |
---|
381 | l |
---|
382 | l in |
---|
383 | add_stmt env label_env (f_body f) [ ] (f_ptrs f) emptyfn |
---|
384 | . |
---|
385 | |
---|
386 | definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝ |
---|
387 | transform_partial_program ??? |
---|
388 | (transf_partial_fundef ?? c2ra_function). |
---|
389 | |
---|
390 | include "Cminor/initialisation.ma". |
---|
391 | |
---|
392 | definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝ |
---|
393 | λp. let p' ≝ replace_init p in cminor_to_rtlabs p. |
---|