1 | |
---|
2 | (** This module translates a [Cminor] program into a [RTLabs] program. *) |
---|
3 | |
---|
4 | open Driver |
---|
5 | |
---|
6 | |
---|
7 | let error_prefix = "Cminor to RTLabs" |
---|
8 | let error = Error.global_error error_prefix |
---|
9 | let error_float () = error "float not supported." |
---|
10 | |
---|
11 | |
---|
12 | (* Helper functions *) |
---|
13 | |
---|
14 | let allocate (rtlabs_fun : RTLabs.internal_function) (sig_type : AST.sig_type) |
---|
15 | : RTLabs.internal_function * Register.t = |
---|
16 | let r = Register.fresh rtlabs_fun.RTLabs.f_runiverse in |
---|
17 | let locals = rtlabs_fun.RTLabs.f_locals @ [(r, sig_type)] in |
---|
18 | let rtlabs_fun = |
---|
19 | { rtlabs_fun with RTLabs.f_locals = locals } in |
---|
20 | (rtlabs_fun, r) |
---|
21 | |
---|
22 | let type_of (Cminor.Expr (_, t)) = t |
---|
23 | |
---|
24 | let allocate_expr |
---|
25 | (rtlabs_fun : RTLabs.internal_function) |
---|
26 | (e : Cminor.expression) |
---|
27 | : (RTLabs.internal_function * Register.t) = |
---|
28 | allocate rtlabs_fun (type_of e) |
---|
29 | |
---|
30 | type local_env = Register.t StringTools.Map.t |
---|
31 | |
---|
32 | let find_local (lenv : local_env) (x : AST.ident) : Register.t = |
---|
33 | if StringTools.Map.mem x lenv then StringTools.Map.find x lenv |
---|
34 | else error ("Unknown local \"" ^ x ^ "\".") |
---|
35 | |
---|
36 | let find_olocal (lenv : local_env) (ox : AST.ident option) : Register.t option = |
---|
37 | match ox with |
---|
38 | | None -> None |
---|
39 | | Some x -> Some (find_local lenv x) |
---|
40 | |
---|
41 | let choose_destination |
---|
42 | (rtlabs_fun : RTLabs.internal_function) |
---|
43 | (lenv : local_env) |
---|
44 | (e : Cminor.expression) |
---|
45 | : RTLabs.internal_function * Register.t = |
---|
46 | match e with |
---|
47 | | Cminor.Expr (Cminor.Id x, _) -> (rtlabs_fun, find_local lenv x) |
---|
48 | | _ -> allocate_expr rtlabs_fun e |
---|
49 | |
---|
50 | let choose_destinations |
---|
51 | (rtlabs_fun : RTLabs.internal_function) |
---|
52 | (lenv : local_env) |
---|
53 | (args : Cminor.expression list) |
---|
54 | : RTLabs.internal_function * Register.t list = |
---|
55 | let f (rtlabs_fun, regs) e = |
---|
56 | let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in |
---|
57 | (rtlabs_fun, regs @ [r]) in |
---|
58 | List.fold_left f (rtlabs_fun, []) args |
---|
59 | |
---|
60 | let fresh_label (rtlabs_fun : RTLabs.internal_function) : Label.t = |
---|
61 | Label.Gen.fresh rtlabs_fun.RTLabs.f_luniverse |
---|
62 | |
---|
63 | let change_entry |
---|
64 | (rtlabs_fun : RTLabs.internal_function) |
---|
65 | (new_entry : Label.t) |
---|
66 | : RTLabs.internal_function = |
---|
67 | { rtlabs_fun with RTLabs.f_entry = new_entry } |
---|
68 | |
---|
69 | |
---|
70 | (* Add a label and its associated instruction at the beginning of a function's |
---|
71 | graph *) |
---|
72 | let add_graph |
---|
73 | (rtlabs_fun : RTLabs.internal_function) |
---|
74 | (lbl : Label.t) |
---|
75 | (stmt : RTLabs.statement) |
---|
76 | : RTLabs.internal_function = |
---|
77 | let graph = Label.Map.add lbl stmt rtlabs_fun.RTLabs.f_graph in |
---|
78 | let rtlabs_fun = { rtlabs_fun with RTLabs.f_graph = graph } in |
---|
79 | change_entry rtlabs_fun lbl |
---|
80 | |
---|
81 | |
---|
82 | let generate |
---|
83 | (rtlabs_fun : RTLabs.internal_function) |
---|
84 | (stmt : RTLabs.statement) |
---|
85 | : RTLabs.internal_function = |
---|
86 | let lbl = fresh_label rtlabs_fun in |
---|
87 | add_graph rtlabs_fun lbl stmt |
---|
88 | |
---|
89 | |
---|
90 | (* |
---|
91 | (* [addressing e] returns the type of address represented by [e], |
---|
92 | along with its arguments *) |
---|
93 | |
---|
94 | let addressing (Cminor.Expr (ed, t) : Cminor.expression) |
---|
95 | : (RTLabs.addressing * Cminor.expression list) = |
---|
96 | match ed with |
---|
97 | | Cminor.Cst (AST.Cst_addrsymbol id) -> (RTLabs.Aglobal (id, 0), []) |
---|
98 | | Cminor.Cst (AST.Cst_stackoffset n) -> (RTLabs.Ainstack n, []) |
---|
99 | | Cminor.Op2 (AST.Op_addp _, |
---|
100 | Cminor.Cst (AST.Cst_addrsymbol id), |
---|
101 | Cminor.Cst (AST.Cst_int n)) -> |
---|
102 | (RTLabs.Aglobal (id, n), []) |
---|
103 | | Cminor.Op2 (AST.Op_addp _, e1, Cminor.Cst (AST.Cst_int n)) -> |
---|
104 | (RTLabs.Aindexed n, [e1]) |
---|
105 | | Cminor.Op2 (AST.Op_addp _, |
---|
106 | Cminor.Cst (AST.Cst_addrsymbol id), |
---|
107 | e2) -> |
---|
108 | (RTLabs.Abased (id, 0), [e2]) |
---|
109 | | Cminor.Op2 (AST.Op_addp _, e1, e2) -> (RTLabs.Aindexed2, [e1 ; e2]) |
---|
110 | | _ -> (RTLabs.Aindexed 0, [e]) |
---|
111 | *) |
---|
112 | |
---|
113 | |
---|
114 | (* Translating conditions *) |
---|
115 | |
---|
116 | let rec translate_branch |
---|
117 | (rtlabs_fun : RTLabs.internal_function) |
---|
118 | (lenv : local_env) |
---|
119 | (e : Cminor.expression) |
---|
120 | (lbl_true : Label.t) |
---|
121 | (lbl_false : Label.t) |
---|
122 | : RTLabs.internal_function = |
---|
123 | let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in |
---|
124 | let stmt = RTLabs.St_cond (r, lbl_true, lbl_false) in |
---|
125 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
126 | translate_expr rtlabs_fun lenv r e |
---|
127 | |
---|
128 | (* |
---|
129 | let Cminor.Expr (ed, t) = e in |
---|
130 | match ed with |
---|
131 | |
---|
132 | | Cminor.Id x -> |
---|
133 | let stmt = |
---|
134 | RTLabs.St_cond1 (AST.Op_id, find_local lenv x, lbl_true, lbl_false) in |
---|
135 | generate rtlabs_fun stmt |
---|
136 | |
---|
137 | | Cminor.Cst cst -> |
---|
138 | generate rtlabs_fun (RTLabs.St_condcst (cst, t, lbl_true, lbl_false)) |
---|
139 | |
---|
140 | | Cminor.Op1 (op1, e) -> |
---|
141 | let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in |
---|
142 | let stmt = RTLabs.St_cond1 (op1, r, lbl_true, lbl_false) in |
---|
143 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
144 | translate_expr rtlabs_fun lenv r e |
---|
145 | |
---|
146 | | Cminor.Op2 (op2, e1, e2) -> |
---|
147 | let (rtlabs_fun, r1) = choose_destination rtlabs_fun lenv e1 in |
---|
148 | let (rtlabs_fun, r2) = choose_destination rtlabs_fun lenv e2 in |
---|
149 | let stmt = RTLabs.St_cond2 (op2, r1, r2, lbl_true, lbl_false) in |
---|
150 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
151 | translate_exprs rtlabs_fun lenv [r1 ; r2] [e1 ; e2] |
---|
152 | |
---|
153 | | _ -> |
---|
154 | let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in |
---|
155 | let stmt = RTLabs.St_cond1 (AST.Op_id, r, lbl_true, lbl_false) in |
---|
156 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
157 | translate_expr rtlabs_fun lenv r e |
---|
158 | *) |
---|
159 | |
---|
160 | (* Translating expressions *) |
---|
161 | |
---|
162 | and translate_expr |
---|
163 | (rtlabs_fun : RTLabs.internal_function) |
---|
164 | (lenv : local_env) |
---|
165 | (destr : Register.t) |
---|
166 | (e : Cminor.expression) |
---|
167 | : RTLabs.internal_function = |
---|
168 | let Cminor.Expr (ed, t) = e in |
---|
169 | match ed with |
---|
170 | |
---|
171 | | Cminor.Id x -> |
---|
172 | let xr = find_local lenv x in |
---|
173 | (* If the destination and source are the same, just do nothing. *) |
---|
174 | if Register.equal destr xr then rtlabs_fun |
---|
175 | else |
---|
176 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
177 | let stmt = RTLabs.St_op1 (AST.Op_id, destr, xr, old_entry) in |
---|
178 | generate rtlabs_fun stmt |
---|
179 | |
---|
180 | | Cminor.Cst cst -> |
---|
181 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
182 | let stmt = RTLabs.St_cst (destr, cst, old_entry) in |
---|
183 | generate rtlabs_fun stmt |
---|
184 | |
---|
185 | | Cminor.Op1 (op1, e) -> |
---|
186 | let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in |
---|
187 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
188 | let stmt = RTLabs.St_op1 (op1, destr, r, old_entry) in |
---|
189 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
190 | translate_expr rtlabs_fun lenv r e |
---|
191 | |
---|
192 | | Cminor.Op2 (op2, e1, e2) -> |
---|
193 | let (rtlabs_fun, r1) = choose_destination rtlabs_fun lenv e1 in |
---|
194 | let (rtlabs_fun, r2) = choose_destination rtlabs_fun lenv e2 in |
---|
195 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
196 | let r1_arg = RTLabs.Reg r1 in |
---|
197 | let r2_arg = RTLabs.Reg r2 in |
---|
198 | let stmt = RTLabs.St_op2 (op2, destr, r1_arg, r2_arg, old_entry) in |
---|
199 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
200 | translate_exprs rtlabs_fun lenv [r1 ; r2] [e1 ; e2] |
---|
201 | |
---|
202 | | Cminor.Mem (chunk, e) -> |
---|
203 | let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in |
---|
204 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
205 | let stmt = |
---|
206 | RTLabs.St_load (chunk, RTLabs.Reg r, destr, old_entry) in |
---|
207 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
208 | translate_expr rtlabs_fun lenv r e |
---|
209 | |
---|
210 | | Cminor.Cond (e1, e2, e3) -> |
---|
211 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
212 | let rtlabs_fun = translate_expr rtlabs_fun lenv destr e3 in |
---|
213 | let lbl_false = rtlabs_fun.RTLabs.f_entry in |
---|
214 | let rtlabs_fun = change_entry rtlabs_fun old_entry in |
---|
215 | let rtlabs_fun = translate_expr rtlabs_fun lenv destr e2 in |
---|
216 | let lbl_true = rtlabs_fun.RTLabs.f_entry in |
---|
217 | translate_branch rtlabs_fun lenv e1 lbl_true lbl_false |
---|
218 | |
---|
219 | | Cminor.Exp_cost (lbl, e) -> |
---|
220 | let rtlabs_fun = translate_expr rtlabs_fun lenv destr e in |
---|
221 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
222 | generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry)) |
---|
223 | |
---|
224 | and translate_exprs |
---|
225 | (rtlabs_fun : RTLabs.internal_function) |
---|
226 | (lenv : local_env) |
---|
227 | (regs : Register.t list) |
---|
228 | (args : Cminor.expression list) |
---|
229 | : RTLabs.internal_function = |
---|
230 | let f destr e rtlabs_fun = translate_expr rtlabs_fun lenv destr e in |
---|
231 | List.fold_right2 f regs args rtlabs_fun |
---|
232 | |
---|
233 | |
---|
234 | (* |
---|
235 | (* Switch transformation |
---|
236 | |
---|
237 | switch (e) { |
---|
238 | case c0: exit i0; |
---|
239 | case c1: exit i1; |
---|
240 | ... |
---|
241 | default: exit idfl; } |
---|
242 | |
---|
243 | is translated to |
---|
244 | |
---|
245 | if (e == c0) exit i0; |
---|
246 | if (e == c1) exit i1; |
---|
247 | ... |
---|
248 | exit idfl; *) |
---|
249 | |
---|
250 | let transform_switch |
---|
251 | (e : Cminor.expression) |
---|
252 | (cases : (int * int) list) |
---|
253 | (dfl : int) |
---|
254 | : Cminor.statement = |
---|
255 | let rec aux = function |
---|
256 | | [] -> Cminor.St_skip |
---|
257 | | (case, exit) :: cases -> |
---|
258 | let c = |
---|
259 | Cminor.Op2 (AST.Op_cmp (AST.Cmp_eq, uint), |
---|
260 | e, Cminor.Cst (AST.Cst_int case)) in |
---|
261 | let stmt = |
---|
262 | Cminor.St_ifthenelse (c, Cminor.St_exit exit, Cminor.St_skip) in |
---|
263 | Cminor.St_seq (stmt, aux cases) |
---|
264 | in |
---|
265 | Cminor.St_seq (aux cases, Cminor.St_exit dfl) |
---|
266 | *) |
---|
267 | |
---|
268 | |
---|
269 | (* Translating statements *) |
---|
270 | |
---|
271 | let rec translate_stmt |
---|
272 | (rtlabs_fun : RTLabs.internal_function) |
---|
273 | (lenv : local_env) |
---|
274 | (* (exits : Label.t list) *) |
---|
275 | (stmt : Cminor.statement) |
---|
276 | : RTLabs.internal_function = |
---|
277 | match stmt with |
---|
278 | |
---|
279 | | Cminor.St_skip -> rtlabs_fun |
---|
280 | |
---|
281 | | Cminor.St_assign (x, e) -> |
---|
282 | translate_expr rtlabs_fun lenv (find_local lenv x) e |
---|
283 | |
---|
284 | | Cminor.St_store (chunk, e1, e2) -> |
---|
285 | let (rtlabs_fun, addr) = choose_destination rtlabs_fun lenv e1 in |
---|
286 | let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e2 in |
---|
287 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
288 | let stmt = |
---|
289 | RTLabs.St_store (chunk, RTLabs.Reg addr, RTLabs.Reg r, old_entry) in |
---|
290 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
291 | translate_exprs rtlabs_fun lenv [addr ; r] [e1 ; e2] |
---|
292 | |
---|
293 | | Cminor.St_call (oret, |
---|
294 | Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f), _), |
---|
295 | args, sg) -> |
---|
296 | let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in |
---|
297 | let oretr = find_olocal lenv oret in |
---|
298 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
299 | let regs' = List.map (fun reg -> RTLabs.Reg reg) regs in |
---|
300 | let stmt = RTLabs.St_call_id (f, regs', oretr, sg, old_entry) in |
---|
301 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
302 | translate_exprs rtlabs_fun lenv regs args |
---|
303 | |
---|
304 | | Cminor.St_call (oret, f, args, sg) -> |
---|
305 | let (rtlabs_fun, fr) = choose_destination rtlabs_fun lenv f in |
---|
306 | let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in |
---|
307 | let oretr = find_olocal lenv oret in |
---|
308 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
309 | let regs' = List.map (fun reg -> RTLabs.Reg reg) regs in |
---|
310 | let stmt = RTLabs.St_call_ptr (fr, regs', oretr, sg, old_entry) in |
---|
311 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
312 | translate_exprs rtlabs_fun lenv (fr :: regs) (f :: args) |
---|
313 | |
---|
314 | | Cminor.St_tailcall (Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f), _), |
---|
315 | args, sg) -> |
---|
316 | let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in |
---|
317 | let regs' = List.map (fun reg -> RTLabs.Reg reg) regs in |
---|
318 | let stmt = RTLabs.St_tailcall_id (f, regs', sg) in |
---|
319 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
320 | translate_exprs rtlabs_fun lenv regs args |
---|
321 | |
---|
322 | | Cminor.St_tailcall (f, args, sg) -> |
---|
323 | let (rtlabs_fun, fr) = choose_destination rtlabs_fun lenv f in |
---|
324 | let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in |
---|
325 | let regs' = List.map (fun reg -> RTLabs.Reg reg) regs in |
---|
326 | let stmt = RTLabs.St_tailcall_ptr (fr, regs', sg) in |
---|
327 | let rtlabs_fun = generate rtlabs_fun stmt in |
---|
328 | translate_exprs rtlabs_fun lenv (fr :: regs) (f :: args) |
---|
329 | |
---|
330 | | Cminor.St_seq (s1, s2) -> |
---|
331 | let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s2 in |
---|
332 | translate_stmt rtlabs_fun lenv (*exits*) s1 |
---|
333 | |
---|
334 | | Cminor.St_ifthenelse (e, s1, s2) -> |
---|
335 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
336 | let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s2 in |
---|
337 | let lbl_false = rtlabs_fun.RTLabs.f_entry in |
---|
338 | let rtlabs_fun = change_entry rtlabs_fun old_entry in |
---|
339 | let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s1 in |
---|
340 | let lbl_true = rtlabs_fun.RTLabs.f_entry in |
---|
341 | translate_branch rtlabs_fun lenv e lbl_true lbl_false |
---|
342 | |
---|
343 | (* | Cminor.St_loop s -> |
---|
344 | let loop_start = fresh_label rtlabs_fun in |
---|
345 | let rtlabs_fun = change_entry rtlabs_fun loop_start in |
---|
346 | let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in |
---|
347 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
348 | add_graph rtlabs_fun loop_start (RTLabs.St_skip old_entry) |
---|
349 | |
---|
350 | | Cminor.St_block s -> |
---|
351 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
352 | translate_stmt rtlabs_fun lenv (old_entry :: exits) s |
---|
353 | |
---|
354 | | Cminor.St_exit n -> |
---|
355 | change_entry rtlabs_fun (List.nth exits n) *) |
---|
356 | |
---|
357 | | Cminor.St_return eopt -> |
---|
358 | let rtlabs_fun = change_entry rtlabs_fun rtlabs_fun.RTLabs.f_exit in |
---|
359 | (match eopt, rtlabs_fun.RTLabs.f_result with |
---|
360 | | None, None -> rtlabs_fun |
---|
361 | | Some e, Some (retr, _) -> translate_expr rtlabs_fun lenv retr e |
---|
362 | | _ -> assert false (* should be impossible *)) |
---|
363 | |
---|
364 | | Cminor.St_switch (e, cases, dfl) -> |
---|
365 | assert false (* should have been simplified before *) |
---|
366 | (* |
---|
367 | let stmt = transform_switch e cases dfl in |
---|
368 | translate_stmt rtlabs_fun lenv exits stmt |
---|
369 | *) |
---|
370 | |
---|
371 | | Cminor.St_label (lbl, s) -> |
---|
372 | let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s in |
---|
373 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
374 | add_graph rtlabs_fun lbl (RTLabs.St_skip old_entry) |
---|
375 | |
---|
376 | | Cminor.St_cost (lbl, s) -> |
---|
377 | let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s in |
---|
378 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
379 | generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry)) |
---|
380 | |
---|
381 | | Cminor.St_ind_0 (i, s) -> |
---|
382 | let rtlabs_fun = translate_stmt rtlabs_fun lenv s in |
---|
383 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
384 | generate rtlabs_fun (RTLabs.St_ind_0 (i, old_entry)) |
---|
385 | |
---|
386 | | Cminor.St_ind_inc (i, s) -> |
---|
387 | let rtlabs_fun = translate_stmt rtlabs_fun lenv s in |
---|
388 | let old_entry = rtlabs_fun.RTLabs.f_entry in |
---|
389 | generate rtlabs_fun (RTLabs.St_ind_inc (i, old_entry)) |
---|
390 | |
---|
391 | | Cminor.St_goto lbl -> |
---|
392 | change_entry rtlabs_fun lbl |
---|
393 | |
---|
394 | |
---|
395 | (* Translating function definitions *) |
---|
396 | |
---|
397 | (* The translation consists in the following: |
---|
398 | - Create a universe of pseudo-register names |
---|
399 | - Create a universe of label names |
---|
400 | - Create a local environment; that is, a mapping from local |
---|
401 | variables to pseudo-registers |
---|
402 | - Extract the registers representing the formal variables |
---|
403 | - Extract the registers representing the local variables |
---|
404 | - Allocate a fresh register to hold the result of the function |
---|
405 | - Allocate a fresh label representing the exit point |
---|
406 | - Initialize the graph with a return instruction at the end |
---|
407 | - Complete the graph according to the function's body. |
---|
408 | Instructions will be added from end to start following the flow of the |
---|
409 | function. *) |
---|
410 | |
---|
411 | let translate_internal lbl_prefix f_def = |
---|
412 | |
---|
413 | (* Register names *) |
---|
414 | let runiverse = Register.new_universe "%" in |
---|
415 | |
---|
416 | (* Labels of statements *) |
---|
417 | let luniverse = Label.Gen.new_universe lbl_prefix in |
---|
418 | |
---|
419 | (* Local environment *) |
---|
420 | let add_local lenv (x, _) = |
---|
421 | StringTools.Map.add x (Register.fresh runiverse) lenv in |
---|
422 | let lenv = StringTools.Map.empty in |
---|
423 | let lenv = List.fold_left add_local lenv f_def.Cminor.f_params in |
---|
424 | let lenv = List.fold_left add_local lenv f_def.Cminor.f_vars in |
---|
425 | |
---|
426 | let extract vars = |
---|
427 | let f l (x, t) = l @ [(find_local lenv x, t)] in |
---|
428 | List.fold_left f [] vars in |
---|
429 | |
---|
430 | (* Parameter registers *) |
---|
431 | let params = extract f_def.Cminor.f_params in |
---|
432 | |
---|
433 | (* Local registers *) |
---|
434 | let locals = extract f_def.Cminor.f_vars in |
---|
435 | |
---|
436 | (* [result] is the result of the body, if any. *) |
---|
437 | let result = match f_def.Cminor.f_return with |
---|
438 | | AST.Type_void -> None |
---|
439 | | AST.Type_ret t -> Some (Register.fresh runiverse, t) in |
---|
440 | |
---|
441 | let locals = |
---|
442 | locals @ (match result with None -> [] | Some (r, t) -> [(r, t)]) in |
---|
443 | |
---|
444 | (* Exit label of the graph *) |
---|
445 | let exit = Label.Gen.fresh luniverse in |
---|
446 | |
---|
447 | let graph = Label.Map.add exit RTLabs.St_return Label.Map.empty in |
---|
448 | |
---|
449 | let rtlabs_fun = |
---|
450 | { RTLabs.f_luniverse = luniverse ; |
---|
451 | RTLabs.f_runiverse = runiverse ; |
---|
452 | RTLabs.f_result = result ; |
---|
453 | RTLabs.f_params = params ; |
---|
454 | RTLabs.f_locals = locals ; |
---|
455 | RTLabs.f_stacksize = f_def.Cminor.f_stacksize ; |
---|
456 | RTLabs.f_graph = graph ; |
---|
457 | RTLabs.f_entry = exit ; |
---|
458 | RTLabs.f_exit = exit } in |
---|
459 | |
---|
460 | (* Complete the graph *) |
---|
461 | translate_stmt rtlabs_fun lenv (*[]*) f_def.Cminor.f_body |
---|
462 | |
---|
463 | |
---|
464 | let translate_functions lbls (f_id, f_def) = match f_def with |
---|
465 | | Cminor.F_int int_def -> |
---|
466 | let lbl_prefix = StringTools.Gen.fresh_prefix lbls f_id in |
---|
467 | let def = translate_internal lbl_prefix int_def in |
---|
468 | (f_id, RTLabs.F_int def) |
---|
469 | | Cminor.F_ext def -> (f_id, RTLabs.F_ext def) |
---|
470 | |
---|
471 | |
---|
472 | (* Initialization of globals *) |
---|
473 | |
---|
474 | let sum_offsets = |
---|
475 | let f res off = |
---|
476 | let cst_off = |
---|
477 | Cminor.Expr (Cminor.Cst (AST.Cst_offset off), AST.Sig_offset) in |
---|
478 | Cminor.Expr (Cminor.Op2 (AST.Op_add, res, cst_off), AST.Sig_offset) in |
---|
479 | List.fold_left f (Cminor.Expr (Cminor.Cst (AST.Cst_int 0), AST.Sig_offset)) |
---|
480 | |
---|
481 | let quantity_sig_of_data data = |
---|
482 | let i = match data with |
---|
483 | | AST.Data_int8 _ -> 1 |
---|
484 | | AST.Data_int16 _ -> 2 |
---|
485 | | AST.Data_int32 _ -> 4 |
---|
486 | | _ -> assert false (* do not use on these arguments *) in |
---|
487 | (AST.QInt i, AST.Sig_int (i, AST.Unsigned)) |
---|
488 | |
---|
489 | let assign_data x stmt (offsets, data) = |
---|
490 | let off = sum_offsets offsets in |
---|
491 | let addr = Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol x), AST.Sig_ptr) in |
---|
492 | let e = Cminor.Expr (Cminor.Op2 (AST.Op_addp, addr, off), AST.Sig_ptr) in |
---|
493 | let stmt' = match data with |
---|
494 | (* |
---|
495 | | AST.Data_reserve _ -> Cminor.St_skip |
---|
496 | *) |
---|
497 | | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i -> |
---|
498 | let (quantity, etype) = quantity_sig_of_data data in |
---|
499 | let cst = Cminor.Expr (Cminor.Cst (AST.Cst_int i), etype) in |
---|
500 | Cminor.St_store (quantity, e, cst) |
---|
501 | | AST.Data_float32 f | AST.Data_float64 f -> error_float () in |
---|
502 | Cminor.St_seq (stmt, stmt') |
---|
503 | |
---|
504 | let add_global_initializations_body vars body = |
---|
505 | let f stmt (x, size, datas_opt) = match datas_opt with |
---|
506 | | None -> Cminor.St_skip |
---|
507 | | Some datas -> |
---|
508 | let offsets = Memory.all_offsets size in |
---|
509 | if List.length offsets <> List.length datas then |
---|
510 | error "bad global initialization style." |
---|
511 | else |
---|
512 | let offs_datas = List.combine offsets datas in |
---|
513 | List.fold_left (assign_data x) stmt offs_datas in |
---|
514 | Cminor.St_seq (List.fold_left f Cminor.St_skip vars, body) |
---|
515 | |
---|
516 | let add_global_initializations_funct vars = function |
---|
517 | | Cminor.F_int def -> |
---|
518 | let f_body = add_global_initializations_body vars def.Cminor.f_body in |
---|
519 | Cminor.F_int { def with Cminor.f_body = f_body } |
---|
520 | | def -> def |
---|
521 | |
---|
522 | (* [add_global_initializations p] moves the initializations of the globals of |
---|
523 | [p] to the beginning of the main function, if any. *) |
---|
524 | |
---|
525 | let add_global_initializations p = match p.Cminor.main with |
---|
526 | | None -> p.Cminor.functs |
---|
527 | | Some main -> |
---|
528 | let main_def = List.assoc main p.Cminor.functs in |
---|
529 | let main_def = add_global_initializations_funct p.Cminor.vars main_def in |
---|
530 | MiscPottier.update_list_assoc main main_def p.Cminor.functs |
---|
531 | |
---|
532 | (* Translation of a Cminor program to a RTLabs program. *) |
---|
533 | |
---|
534 | let translate p = |
---|
535 | |
---|
536 | (* Fetch the labels already used in the program to create new ones. *) |
---|
537 | let lbls = CminorAnnotator.all_labels p in |
---|
538 | |
---|
539 | (* The initialization of globals are moved at the beginning of the main. *) |
---|
540 | let functs = add_global_initializations p in |
---|
541 | |
---|
542 | (* The globals are associated their size. *) |
---|
543 | let f (id, size, _) = (id, size) in |
---|
544 | |
---|
545 | (* Put all this together and translate each function. *) |
---|
546 | { RTLabs.vars = List.map f p.Cminor.vars ; |
---|
547 | RTLabs.functs = List.map (translate_functions lbls) functs ; |
---|
548 | RTLabs.main = p.Cminor.main } |
---|