2 (** This module translates a [Cminor] program into a [RTLabs] program. *)
7 let error_prefix = "Cminor to RTLabs"
8 let error = Error.global_error error_prefix
9 let error_float () = error "float not supported."
12 (* Helper functions *)
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
19 { rtlabs_fun with RTLabs.f_locals = locals } in
22 let type_of (Cminor.Expr (_, t)) = t
25 (rtlabs_fun : RTLabs.internal_function)
26 (e : Cminor.expression)
27 : (RTLabs.internal_function * Register.t) =
28 allocate rtlabs_fun (type_of e)
30 type local_env = Register.t StringTools.Map.t
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 ^ "\".")
36 let find_olocal (lenv : local_env) (ox : AST.ident option) : Register.t option =
39 | Some x -> Some (find_local lenv x)
41 let choose_destination
42 (rtlabs_fun : RTLabs.internal_function)
44 (e : Cminor.expression)
45 : RTLabs.internal_function * Register.t =
47 | Cminor.Expr (Cminor.Id x, _) -> (rtlabs_fun, find_local lenv x)
48 | _ -> allocate_expr rtlabs_fun e
50 let choose_destinations
51 (rtlabs_fun : RTLabs.internal_function)
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
60 let fresh_label (rtlabs_fun : RTLabs.internal_function) : Label.t =
61 Label.Gen.fresh rtlabs_fun.RTLabs.f_luniverse
64 (rtlabs_fun : RTLabs.internal_function)
66 : RTLabs.internal_function =
67 { rtlabs_fun with RTLabs.f_entry = new_entry }
70 (* Add a label and its associated instruction at the beginning of a function's
73 (rtlabs_fun : RTLabs.internal_function)
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
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
91 (* [addressing e] returns the type of address represented by [e],
92 along with its arguments *)
94 let addressing (Cminor.Expr (ed, t) : Cminor.expression)
95 : (RTLabs.addressing * Cminor.expression list) =
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),
108 (RTLabs.Abased (id, 0), [e2])
109 | Cminor.Op2 (AST.Op_addp _, e1, e2) -> (RTLabs.Aindexed2, [e1 ; e2])
110 | _ -> (RTLabs.Aindexed 0, [e])
114 (* Translating conditions *)
116 let rec translate_branch
117 (rtlabs_fun : RTLabs.internal_function)
119 (e : Cminor.expression)
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
129 let Cminor.Expr (ed, t) = e in
134 RTLabs.St_cond1 (AST.Op_id, find_local lenv x, lbl_true, lbl_false) in
135 generate rtlabs_fun stmt
138 generate rtlabs_fun (RTLabs.St_condcst (cst, t, lbl_true, lbl_false))
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
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]
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
160 (* Translating expressions *)
163 (rtlabs_fun : RTLabs.internal_function)
166 (e : Cminor.expression)
167 : RTLabs.internal_function =
168 let Cminor.Expr (ed, t) = e in
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
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
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
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
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 stmt = RTLabs.St_op2 (op2, destr, r1, r2, old_entry) in
197 let rtlabs_fun = generate rtlabs_fun stmt in
198 translate_exprs rtlabs_fun lenv [r1 ; r2] [e1 ; e2]
200 | Cminor.Mem (chunk, e) ->
201 let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in
202 let old_entry = rtlabs_fun.RTLabs.f_entry in
203 let stmt = RTLabs.St_load (chunk, r, destr, old_entry) in
204 let rtlabs_fun = generate rtlabs_fun stmt in
205 translate_expr rtlabs_fun lenv r e
207 | Cminor.Cond (e1, e2, e3) ->
208 let old_entry = rtlabs_fun.RTLabs.f_entry in
209 let rtlabs_fun = translate_expr rtlabs_fun lenv destr e3 in
210 let lbl_false = rtlabs_fun.RTLabs.f_entry in
211 let rtlabs_fun = change_entry rtlabs_fun old_entry in
212 let rtlabs_fun = translate_expr rtlabs_fun lenv destr e2 in
213 let lbl_true = rtlabs_fun.RTLabs.f_entry in
214 translate_branch rtlabs_fun lenv e1 lbl_true lbl_false
216 | Cminor.Exp_cost (lbl, e) ->
217 let rtlabs_fun = translate_expr rtlabs_fun lenv destr e in
218 let old_entry = rtlabs_fun.RTLabs.f_entry in
219 generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry))
222 (rtlabs_fun : RTLabs.internal_function)
224 (regs : Register.t list)
225 (args : Cminor.expression list)
226 : RTLabs.internal_function =
227 let f destr e rtlabs_fun = translate_expr rtlabs_fun lenv destr e in
228 List.fold_right2 f regs args rtlabs_fun
232 (* Switch transformation
238 default: exit idfl; }
242 if (e == c0) exit i0;
243 if (e == c1) exit i1;
248 (e : Cminor.expression)
249 (cases : (int * int) list)
252 let rec aux = function
253 | [] -> Cminor.St_skip
254 | (case, exit) :: cases ->
256 Cminor.Op2 (AST.Op_cmp (AST.Cmp_eq, uint),
257 e, Cminor.Cst (AST.Cst_int case)) in
259 Cminor.St_ifthenelse (c, Cminor.St_exit exit, Cminor.St_skip) in
260 Cminor.St_seq (stmt, aux cases)
262 Cminor.St_seq (aux cases, Cminor.St_exit dfl)
266 (* Translating statements *)
268 let rec translate_stmt
269 (rtlabs_fun : RTLabs.internal_function)
271 (exits : Label.t list)
272 (stmt : Cminor.statement)
273 : RTLabs.internal_function =
276 | Cminor.St_skip -> rtlabs_fun
278 | Cminor.St_assign (x, e) ->
279 translate_expr rtlabs_fun lenv (find_local lenv x) e
281 | Cminor.St_store (chunk, e1, e2) ->
282 let (rtlabs_fun, addr) = choose_destination rtlabs_fun lenv e1 in
283 let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e2 in
284 let old_entry = rtlabs_fun.RTLabs.f_entry in
285 let stmt = RTLabs.St_store (chunk, addr, r, old_entry) in
286 let rtlabs_fun = generate rtlabs_fun stmt in
287 translate_exprs rtlabs_fun lenv [addr ; r] [e1 ; e2]
289 | Cminor.St_call (oret,
290 Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f), _),
292 let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in
293 let oretr = find_olocal lenv oret in
294 let old_entry = rtlabs_fun.RTLabs.f_entry in
295 let stmt = RTLabs.St_call_id (f, regs, oretr, sg, old_entry) in
296 let rtlabs_fun = generate rtlabs_fun stmt in
297 translate_exprs rtlabs_fun lenv regs args
299 | Cminor.St_call (oret, f, args, sg) ->
300 let (rtlabs_fun, fr) = choose_destination rtlabs_fun lenv f in
301 let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in
302 let oretr = find_olocal lenv oret in
303 let old_entry = rtlabs_fun.RTLabs.f_entry in
304 let stmt = RTLabs.St_call_ptr (fr, regs, oretr, sg, old_entry) in
305 let rtlabs_fun = generate rtlabs_fun stmt in
306 translate_exprs rtlabs_fun lenv (fr :: regs) (f :: args)
308 | Cminor.St_tailcall (Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f), _),
310 let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in
311 let stmt = RTLabs.St_tailcall_id (f, regs, sg) in
312 let rtlabs_fun = generate rtlabs_fun stmt in
313 translate_exprs rtlabs_fun lenv regs args
315 | Cminor.St_tailcall (f, args, sg) ->
316 let (rtlabs_fun, fr) = choose_destination rtlabs_fun lenv f in
317 let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in
318 let stmt = RTLabs.St_tailcall_ptr (fr, regs, sg) in
319 let rtlabs_fun = generate rtlabs_fun stmt in
320 translate_exprs rtlabs_fun lenv (fr :: regs) (f :: args)
322 | Cminor.St_seq (s1, s2) ->
323 let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s2 in
324 translate_stmt rtlabs_fun lenv exits s1
326 | Cminor.St_ifthenelse (e, s1, s2) ->
327 let old_entry = rtlabs_fun.RTLabs.f_entry in
328 let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s2 in
329 let lbl_false = rtlabs_fun.RTLabs.f_entry in
330 let rtlabs_fun = change_entry rtlabs_fun old_entry in
331 let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s1 in
332 let lbl_true = rtlabs_fun.RTLabs.f_entry in
333 translate_branch rtlabs_fun lenv e lbl_true lbl_false
335 | Cminor.St_loop s ->
336 let loop_start = fresh_label rtlabs_fun in
337 let rtlabs_fun = change_entry rtlabs_fun loop_start in
338 let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in
339 let old_entry = rtlabs_fun.RTLabs.f_entry in
340 add_graph rtlabs_fun loop_start (RTLabs.St_skip old_entry)
342 | Cminor.St_block s ->
343 let old_entry = rtlabs_fun.RTLabs.f_entry in
344 translate_stmt rtlabs_fun lenv (old_entry :: exits) s
346 | Cminor.St_exit n ->
347 change_entry rtlabs_fun (List.nth exits n)
349 | Cminor.St_return eopt ->
350 let rtlabs_fun = change_entry rtlabs_fun rtlabs_fun.RTLabs.f_exit in
351 (match eopt, rtlabs_fun.RTLabs.f_result with
352 | None, None -> rtlabs_fun
353 | Some e, Some (retr, _) -> translate_expr rtlabs_fun lenv retr e
354 | _ -> assert false (* should be impossible *))
356 | Cminor.St_switch (e, cases, dfl) ->
357 assert false (* should have been simplified before *)
359 let stmt = transform_switch e cases dfl in
360 translate_stmt rtlabs_fun lenv exits stmt
363 | Cminor.St_label (lbl, s) ->
364 let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in
365 let old_entry = rtlabs_fun.RTLabs.f_entry in
366 add_graph rtlabs_fun lbl (RTLabs.St_skip old_entry)
368 | Cminor.St_cost (lbl, s) ->
369 let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in
370 let old_entry = rtlabs_fun.RTLabs.f_entry in
371 generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry))
373 | Cminor.St_goto lbl ->
374 change_entry rtlabs_fun lbl
377 (* Translating function definitions *)
379 (* The translation consists in the following:
380 - Create a universe of pseudo-register names
381 - Create a universe of label names
382 - Create a local environment; that is, a mapping from local
383 variables to pseudo-registers
384 - Extract the registers representing the formal variables
385 - Extract the registers representing the local variables
386 - Allocate a fresh register to hold the result of the function
387 - Allocate a fresh label representing the exit point
388 - Initialize the graph with a return instruction at the end
389 - Complete the graph according to the function's body.
390 Instructions will be added from end to start following the flow of the
393 let translate_internal lbl_prefix f_def =
396 let runiverse = Register.new_universe "%" in
398 (* Labels of statements *)
399 let luniverse = Label.Gen.new_universe lbl_prefix in
401 (* Local environment *)
402 let add_local lenv (x, _) =
403 StringTools.Map.add x (Register.fresh runiverse) lenv in
404 let lenv = StringTools.Map.empty in
405 let lenv = List.fold_left add_local lenv f_def.Cminor.f_params in
406 let lenv = List.fold_left add_local lenv f_def.Cminor.f_vars in
409 let f l (x, t) = l @ [(find_local lenv x, t)] in
410 List.fold_left f [] vars in
412 (* Parameter registers *)
413 let params = extract f_def.Cminor.f_params in
415 (* Local registers *)
416 let locals = extract f_def.Cminor.f_vars in
418 (* [result] is the result of the body, if any. *)
419 let result = match f_def.Cminor.f_return with
420 | AST.Type_void -> None
421 | AST.Type_ret t -> Some (Register.fresh runiverse, t) in
424 locals @ (match result with None -> [] | Some (r, t) -> [(r, t)]) in
426 (* Exit label of the graph *)
427 let exit = Label.Gen.fresh luniverse in
429 (* The control flow graph: for now, it is only a return instruction at the
431 let return = match result with
433 | Some (retr, _) -> Some retr in
434 let graph = Label.Map.add exit (RTLabs.St_return return) Label.Map.empty in
437 { RTLabs.f_luniverse = luniverse ;
438 RTLabs.f_runiverse = runiverse ;
439 RTLabs.f_result = result ;
440 RTLabs.f_params = params ;
441 RTLabs.f_locals = locals ;
442 RTLabs.f_stacksize = f_def.Cminor.f_stacksize ;
443 RTLabs.f_graph = graph ;
444 RTLabs.f_entry = exit ;
445 RTLabs.f_exit = exit } in
447 (* Complete the graph *)
448 translate_stmt rtlabs_fun lenv [] f_def.Cminor.f_body
451 let translate_functions lbls (f_id, f_def) = match f_def with
452 | Cminor.F_int int_def ->
453 let lbl_prefix = StringTools.Gen.fresh_prefix lbls f_id in
454 let def = translate_internal lbl_prefix int_def in
455 (f_id, RTLabs.F_int def)
456 | Cminor.F_ext def -> (f_id, RTLabs.F_ext def)
459 (* Initialization of globals *)
464 Cminor.Expr (Cminor.Cst (AST.Cst_offset off), AST.Sig_offset) in
465 Cminor.Expr (Cminor.Op2 (AST.Op_add, res, cst_off), AST.Sig_offset) in
466 List.fold_left f (Cminor.Expr (Cminor.Cst (AST.Cst_int 0), AST.Sig_offset))
468 let quantity_sig_of_data data =
469 let i = match data with
470 | AST.Data_int8 _ -> 1
471 | AST.Data_int16 _ -> 2
472 | AST.Data_int32 _ -> 4
473 | _ -> assert false (* do not use on these arguments *) in
474 (AST.QInt i, AST.Sig_int (i, AST.Unsigned))
476 let assign_data x stmt (offsets, data) =
477 let off = sum_offsets offsets in
478 let addr = Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol x), AST.Sig_ptr) in
479 let e = Cminor.Expr (Cminor.Op2 (AST.Op_addp, addr, off), AST.Sig_ptr) in
480 let stmt' = match data with
482 | AST.Data_reserve _ -> Cminor.St_skip
484 | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i ->
485 let (quantity, etype) = quantity_sig_of_data data in
486 let cst = Cminor.Expr (Cminor.Cst (AST.Cst_int i), etype) in
487 Cminor.St_store (quantity, e, cst)
488 | AST.Data_float32 f | AST.Data_float64 f -> error_float () in
489 Cminor.St_seq (stmt, stmt')
491 let add_global_initializations_body vars body =
492 let f stmt (x, size, datas_opt) = match datas_opt with
493 | None -> Cminor.St_skip
495 let offsets = Memory.all_offsets size in
496 if List.length offsets <> List.length datas then
497 error "bad global initialization style."
499 let offs_datas = List.combine offsets datas in
500 List.fold_left (assign_data x) stmt offs_datas in
501 Cminor.St_seq (List.fold_left f Cminor.St_skip vars, body)
503 let add_global_initializations_funct vars = function
504 | Cminor.F_int def ->
505 let f_body = add_global_initializations_body vars def.Cminor.f_body in
506 Cminor.F_int { def with Cminor.f_body = f_body }
509 (* [add_global_initializations p] moves the initializations of the globals of
510 [p] to the beginning of the main function, if any. *)
512 let add_global_initializations p = match p.Cminor.main with
513 | None -> p.Cminor.functs
515 let main_def = List.assoc main p.Cminor.functs in
516 let main_def = add_global_initializations_funct p.Cminor.vars main_def in
517 MiscPottier.update_list_assoc main main_def p.Cminor.functs
520 (* Translation of a Cminor program to a RTLabs program. *)
524 (* Fetch the labels already used in the program to create new ones. *)
525 let lbls = CminorAnnotator.all_labels p in
527 (* The initialization of globals are moved at the beginning of the main. *)
528 let functs = p.Cminor.functs (* add_global_initializations p *) in
531 (* The globals are associated their size. *)
532 let f (id, size, _) = (id, size) in
535 (* Put all this together and translate each function. *)
536 { RTLabs.vars = p.Cminor.vars ;
537 RTLabs.functs = List.map (translate_functions lbls) functs ;
538 RTLabs.main = p.Cminor.main }