source: Deliverables/D2.2/8051/src/cminor/cminorToRTLabs.ml @ 818

Last change on this file since 818 was 818, checked in by ayache, 9 years ago

32 and 16 bits operations support in D2.2/8051

File size: 18.5 KB
Line 
1
2(** This module translates a [Cminor] program into a [RTLabs] program. *)
3
4open Driver
5
6
7let error_prefix = "Cminor to RTLabs"
8let error = Error.global_error error_prefix
9let error_float () = error "float not supported."
10
11
12(* Helper functions *)
13
14let 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
22let type_of (Cminor.Expr (_, t)) = t
23
24let 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
30type local_env = Register.t StringTools.Map.t
31
32let 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
36let 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
41let 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
50let 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
60let fresh_label (rtlabs_fun : RTLabs.internal_function) : Label.t =
61  Label.Gen.fresh rtlabs_fun.RTLabs.f_luniverse
62
63let 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 *)
72let 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
82let 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
94let 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
116let 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
162and 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 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]
199
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
206
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
215
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))
220
221and translate_exprs
222    (rtlabs_fun : RTLabs.internal_function)
223    (lenv       : local_env)
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
229
230
231(*
232(* Switch transformation
233
234   switch (e) {
235   case c0: exit i0;
236   case c1: exit i1;
237   ...
238   default: exit idfl; }
239
240   is translated to
241
242   if (e == c0) exit i0;
243   if (e == c1) exit i1;
244   ...
245   exit idfl; *)
246
247let transform_switch
248    (e : Cminor.expression)
249    (cases : (int * int) list)
250    (dfl : int)
251    : Cminor.statement =
252  let rec aux = function
253    | [] -> Cminor.St_skip
254    | (case, exit) :: cases ->
255      let c =
256        Cminor.Op2 (AST.Op_cmp (AST.Cmp_eq, uint),
257                    e, Cminor.Cst (AST.Cst_int case)) in
258      let stmt =
259        Cminor.St_ifthenelse (c, Cminor.St_exit exit, Cminor.St_skip) in
260      Cminor.St_seq (stmt, aux cases)
261  in
262  Cminor.St_seq (aux cases, Cminor.St_exit dfl)
263*)
264
265
266(* Translating statements *)
267
268let rec translate_stmt
269    (rtlabs_fun : RTLabs.internal_function)
270    (lenv       : local_env)
271    (exits      : Label.t list)
272    (stmt       : Cminor.statement)
273    : RTLabs.internal_function =
274  match stmt with
275
276    | Cminor.St_skip -> rtlabs_fun
277
278    | Cminor.St_assign (x, e) ->
279      translate_expr rtlabs_fun lenv (find_local lenv x) e
280
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]
288
289    | Cminor.St_call (oret,
290                      Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f), _),
291                      args, sg) ->
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
298
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)
307
308    | Cminor.St_tailcall (Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f), _),
309                          args, sg) ->
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
314
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)
321
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
325
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
334
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)
341
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
345
346    | Cminor.St_exit n ->
347      change_entry rtlabs_fun (List.nth exits n)
348
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 *))
355
356    | Cminor.St_switch (e, cases, dfl) ->
357      assert false (* should have been simplified before *)
358(*
359      let stmt = transform_switch e cases dfl in
360      translate_stmt rtlabs_fun lenv exits stmt
361*)
362
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)
367
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))
372
373    | Cminor.St_goto lbl ->
374      change_entry rtlabs_fun lbl
375
376
377(* Translating function definitions *)
378
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
391     function. *)
392
393let translate_internal lbl_prefix f_def =
394
395  (* Register names *)
396  let runiverse = Register.new_universe "%" in
397
398  (* Labels of statements *)
399  let luniverse = Label.Gen.new_universe lbl_prefix in
400
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
407
408  let extract vars =
409    let f l (x, t) = l @ [(find_local lenv x, t)] in
410    List.fold_left f [] vars in
411
412  (* Parameter registers *)
413  let params = extract f_def.Cminor.f_params in
414 
415  (* Local registers *)
416  let locals =  extract f_def.Cminor.f_vars in
417
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
422
423  let locals =
424    locals @ (match result with None -> [] | Some (r, t) -> [(r, t)]) in
425
426  (* Exit label of the graph *)
427  let exit = Label.Gen.fresh luniverse in
428
429  (* The control flow graph: for now, it is only a return instruction at the
430     end. *)
431  let return = match result with
432    | None -> None
433    | Some (retr, _) -> Some retr in
434  let graph = Label.Map.add exit (RTLabs.St_return return) Label.Map.empty in
435
436  let rtlabs_fun =
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
446
447  (* Complete the graph *)
448  translate_stmt rtlabs_fun lenv [] f_def.Cminor.f_body
449
450
451let 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)
457
458
459(* Initialization of globals *)
460
461let sum_offsets =
462  let f res off =
463    let cst_off =
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))
467
468let 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))
475
476let 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
481(*
482    | AST.Data_reserve _ -> Cminor.St_skip
483*)
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')
490
491let add_global_initializations_body vars body =
492  let f stmt (x, size, datas_opt) = match datas_opt with
493    | None -> Cminor.St_skip
494    | Some datas ->
495      let offsets = Memory.all_offsets size in
496      if List.length offsets <> List.length datas then
497        error "bad global initialization style."
498      else
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)
502
503let 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 }
507  | def -> def
508
509(* [add_global_initializations p] moves the initializations of the globals of
510   [p] to the beginning of the main function, if any. *)
511
512let add_global_initializations p = match p.Cminor.main with
513  | None -> p.Cminor.functs
514  | Some main ->
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
518
519(* Translation of a Cminor program to a RTLabs program. *)
520
521let translate p =
522
523  (* Fetch the labels already used in the program to create new ones. *)
524  let lbls = CminorAnnotator.all_labels p in
525
526  (* The initialization of globals are moved at the beginning of the main. *)
527  let functs = add_global_initializations p in
528
529  (* The globals are associated their size. *)
530  let f (id, size, _) = (id, size) in
531
532  (* Put all this together and translate each function. *)
533  { RTLabs.vars = List.map f p.Cminor.vars ;
534    RTLabs.functs = List.map (translate_functions lbls) functs ;
535    RTLabs.main = p.Cminor.main }
Note: See TracBrowser for help on using the repository browser.