source: Deliverables/D2.2/8051/src/clight/runtime.ml @ 3673

Last change on this file since 3673 was 1525, checked in by ayache, 8 years ago

D2.2: function pointers using JMP.

File size: 14.8 KB
Line 
1
2(** This module adds runtime functions in a [Clight] program. These functions
3    implement unsupported functions by the target architecture that introduce a
4    branch. We need to define them at the [Clight] level in order to have a
5    correct labelling. *)
6
7
8let error_prefix = "Adding runtime functions"
9let error = Error.global_error error_prefix
10
11
12let add_program p s =
13  let tmp_file = Filename.temp_file "add_runtime" ".c" in
14  let cout = open_out tmp_file in
15  let output = s ^ (ClightPrinter.print_program p) in
16  output_string cout output ;
17  flush cout ;
18  close_out cout ;
19  let p = ClightParser.process tmp_file in
20  Misc.SysExt.safe_remove tmp_file ;
21  p
22
23
24type operation =
25  | Unary of Clight.unary_operation * Clight.ctype
26  | Binary of Clight.binary_operation * Clight.ctype * Clight.ctype
27  | Cast of Clight.ctype (* destination type *) * Clight.ctype (* source type *)
28  | Fun of string (* name of the function *)
29
30type op_replacement =
31    (* operation to be replaced *)
32    operation *
33    (* base name of the replacement function *)
34    string *
35    (* C definition of the replacement function, provided a name for the
36       function *)
37    (string -> string) *
38    (* dependencies *)
39    operation list
40
41module CtypeSet =
42  Set.Make (struct type t = Clight.ctype let compare = Pervasives.compare end)
43
44
45let deps op replacements =
46  let f res (op', _, _, deps) = if op' = op then deps else res in
47  List.fold_left f [] replacements
48
49
50(* Filter used operations only *)
51
52module OperationSet =
53  Set.Make (struct type t = operation let compare = Pervasives.compare end)
54
55let union_list l = List.fold_left OperationSet.union OperationSet.empty l
56
57let f_ctype ctype _ = ctype
58
59let f_expr e _ sub_expr_descrs_res =
60  let res_e = match e with
61    | Clight.Expr (Clight.Evar x, Clight.Tfunction _) ->
62      OperationSet.singleton (Fun x)
63    | _ -> OperationSet.empty in
64  union_list (res_e :: sub_expr_descrs_res)
65
66let f_expr_descr ed _ sub_exprs_res =
67  let res_ed = match ed with
68    | Clight.Eunop (unop, Clight.Expr (_, t)) ->
69      OperationSet.singleton (Unary (unop, t))
70    | Clight.Ebinop (binop, Clight.Expr (_, t1), Clight.Expr (_, t2)) ->
71      OperationSet.singleton (Binary (binop, t1, t2))
72    | Clight.Ecast (t, Clight.Expr (_, t')) ->
73      OperationSet.singleton (Cast (t, t'))
74    | _ -> OperationSet.empty in
75  union_list (res_ed :: sub_exprs_res)
76
77let f_stmt _ sub_exprs_res sub_stmts_res =
78  OperationSet.union (union_list sub_exprs_res) (union_list sub_stmts_res)
79
80let used_ops_stmt = ClightFold.statement f_ctype f_expr f_expr_descr f_stmt
81
82let used_ops_fundef = function
83  | Clight.Internal cfun -> used_ops_stmt cfun.Clight.fn_body
84  | Clight.External _ -> OperationSet.empty
85
86let used_ops p =
87  let f ops (_, fundef) = OperationSet.union ops (used_ops_fundef fundef) in
88  List.fold_left f OperationSet.empty p.Clight.prog_funct
89
90
91let mem_replacements op =
92  let f res (op', _, _, _) = res || (op' = op) in
93  List.fold_left f false
94
95let rec fix equal next x =
96  let y = next x in
97  if equal x y then x
98  else fix equal next y
99
100let needed_replacements used_ops replacements =
101  let f op = mem_replacements op replacements in
102  let reduced_used_ops = OperationSet.filter f used_ops in
103  let next_ops ops =
104    let add ops op = OperationSet.add op ops in
105    let f op next_ops = List.fold_left add next_ops (deps op replacements) in
106    OperationSet.fold f ops ops in
107  let needed_ops = fix OperationSet.equal next_ops reduced_used_ops in
108  let f (op, _, _, _) = OperationSet.mem op needed_ops in
109  List.filter f replacements
110
111
112let map_fresh_name unique map base_name =
113  if StringTools.Map.mem base_name map then
114    (map, StringTools.Map.find base_name map)
115  else
116    let fresh_name = unique base_name in
117    (StringTools.Map.add base_name fresh_name map, fresh_name)
118
119let fresh_replacements unique replacements =
120  let f (map, l) (op, base_name, new_fun, deps) =
121    let (map, fresh_name) = map_fresh_name unique map base_name in
122    (map, l @ [(op, fresh_name, new_fun fresh_name, deps)]) in
123  snd (List.fold_left f (StringTools.Map.empty, []) replacements)
124
125
126let add_replacements replacements p =
127  let f_replacements s (_, _, new_fun, _) = s ^ "\n" ^ new_fun in
128  let added_string = List.fold_left f_replacements "" replacements in
129  add_program p added_string
130
131
132let make_replacement_assoc = List.map (fun (op, name, _, _) -> (op, name))
133
134
135let add p replacements =
136  let used_ops = used_ops p in
137  let needed_replacements = needed_replacements used_ops replacements in
138  let unique = StringTools.make_unique (ClightAnnotator.all_idents p) in
139  let replacements = fresh_replacements unique needed_replacements in
140  let p = add_replacements replacements p in
141  (p, make_replacement_assoc replacements)
142
143
144(* Replacement *)
145
146let seq =
147  List.fold_left
148    (fun stmt1 stmt2 ->
149      if stmt1 = Clight.Sskip then stmt2
150      else
151        if stmt2 = Clight.Sskip then stmt1
152        else Clight.Ssequence (stmt1, stmt2))
153    Clight.Sskip
154
155let f_ctype ctype _ = ctype
156
157let call fresh replaced replacement_assoc args ret_type =
158  let tmp = fresh () in
159  let replacement_fun_name = List.assoc replaced replacement_assoc in
160  let tmpe = Clight.Expr (Clight.Evar tmp, ret_type) in
161  let (args, args_types) = List.split args in
162  let f_type = Clight.Tfunction (args_types, ret_type) in
163  let f = Clight.Expr (Clight.Evar replacement_fun_name, f_type) in
164  let call = Clight.Scall (Some tmpe, f, args) in
165  (tmpe, call, [(tmp, ret_type)])
166
167let replace_ident replacement_assoc x t =
168  let new_name = match t with
169    | Clight.Tfunction _
170        when List.mem_assoc (Fun x) replacement_assoc ->
171      let replacement_fun_name = List.assoc (Fun x) replacement_assoc in
172      replacement_fun_name
173    | _ -> x in
174  (Clight.Expr (Clight.Evar new_name, t), Clight.Sskip, [])
175
176let f_expr fresh replacement_assoc e _ _ =
177
178  let f (Clight.Expr (ed, t) as e) sub_exprs_res =
179    let f_sub_exprs (es, stmt, tmps) (e, stmt', tmps') =
180      (es @ [e], seq [stmt ; stmt'], tmps @ tmps') in
181    let (sub_exprs, stmt1, tmps1) =
182      List.fold_left f_sub_exprs ([], Clight.Sskip, []) sub_exprs_res in
183    let (e, stmt2, tmps2) = match ed, sub_exprs with
184      | Clight.Evar x, _ -> replace_ident replacement_assoc x t
185      | Clight.Eunop (unop, Clight.Expr (_, t')), e' :: _
186          when List.mem_assoc (Unary (unop, t')) replacement_assoc ->
187        call fresh (Unary (unop, t')) replacement_assoc [(e', t')] t
188      | Clight.Ebinop (binop, Clight.Expr (_, t1), Clight.Expr (_, t2)),
189        e1 :: e2 :: _
190          when List.mem_assoc (Binary (binop, t1, t2)) replacement_assoc ->
191        call fresh (Binary (binop, t1, t2)) replacement_assoc
192          [(e1, t1) ; (e2, t2)] t
193      | Clight.Ecast (t, Clight.Expr (_, t')), e' :: _
194          when List.mem_assoc (Cast (t, t')) replacement_assoc ->
195        call fresh (Cast (t, t')) replacement_assoc [(e', t')] t
196      | _ -> (e, Clight.Sskip, []) in
197    (ClightFold.expr_fill_exprs e sub_exprs,
198     seq [stmt1 ; stmt2],
199     tmps1 @ tmps2) in
200
201  ClightFold.expr2 f e
202
203let f_expr_descr ed _ _ _ = ed
204
205let f_stmt stmt sub_exprs_res sub_stmts_res =
206  let f_sub_exprs (es, stmt, tmps) (e, stmt', tmps') =
207    (es @ [e], seq [stmt ; stmt'], tmps @ tmps') in
208  let (sub_exprs, added_stmt, tmps1) =
209    List.fold_left f_sub_exprs ([], Clight.Sskip, []) sub_exprs_res in
210  let f_sub_stmts (stmts, tmps) (stmt, tmps') =
211    (stmts @ [stmt], tmps @ tmps') in
212  let (sub_stmts, tmps2) = List.fold_left f_sub_stmts ([], []) sub_stmts_res in
213  let stmt' = ClightFold.statement_fill_subs stmt sub_exprs sub_stmts in
214  (seq [added_stmt ; stmt'], tmps1 @ tmps2)
215
216let replace_statement fresh replacement_assoc =
217  ClightFold.statement f_ctype (f_expr fresh replacement_assoc)
218    f_expr_descr f_stmt
219
220let replace_internal fresh replacement_assoc def =
221  let (new_body, tmps) =
222    replace_statement fresh replacement_assoc def.Clight.fn_body in
223  { def with
224    Clight.fn_vars = def.Clight.fn_vars @ tmps ; Clight.fn_body = new_body }
225
226let replace_funct fresh replacement_assoc (id, fundef) =
227  let fundef' = match fundef with
228    | Clight.Internal def ->
229      Clight.Internal (replace_internal fresh replacement_assoc def)
230    | _ -> fundef in
231  (id, fundef')
232
233let replace fresh replacement_assoc p =
234  let prog_funct =
235    List.map (replace_funct fresh replacement_assoc) p.Clight.prog_funct in
236  { p with Clight.prog_funct = prog_funct }
237
238
239let save_and_parse p =
240  let tmp_file = Filename.temp_file "clight32toclight8" ".c" in
241  try
242    let oc = open_out tmp_file in
243    output_string oc (ClightPrinter.print_program p) ;
244    close_out oc ;
245    let res = ClightParser.process tmp_file in
246    Misc.SysExt.safe_remove tmp_file ;
247    res
248  with Sys_error _ -> failwith "Error reparsing Clight8 transformation."
249
250let add_replacements p replacements =
251  let p = ClightCasts.simplify p in
252  let (p, replacement_assoc) = add p replacements in
253  let p = ClightCasts.simplify p in
254  let tmp_universe = ClightAnnotator.fresh_universe "_tmp" p in
255  let fresh () = StringTools.Gen.fresh tmp_universe in
256  let p = replace fresh replacement_assoc p in
257  let p = save_and_parse p in
258  ClightCasts.simplify p
259
260
261(* Unsupported operations by the 8051. *)
262
263let cint size sign = Clight.Tint (size, sign)
264
265let cints size = cint size AST.Signed
266let cintu size = cint size AST.Unsigned
267
268let cint8s = cints Clight.I8
269let cint8u = cintu Clight.I8
270let cint16s = cints Clight.I16
271let cint16u = cintu Clight.I16
272let cint32s = cints Clight.I32
273let cint32u = cintu Clight.I32
274
275let byte_size_of_intsize = function
276  | Clight.I8 -> 1
277  | Clight.I16 -> 2
278  | Clight.I32 -> 4
279
280let bit_size_of_intsize size = (byte_size_of_intsize size) * 8
281
282let string_of_intsize size = string_of_int (bit_size_of_intsize size)
283
284let ctype_of_intsize = function
285  | Clight.I8 -> "char"
286  | Clight.I16 -> "short"
287  | Clight.I32 -> "int"
288
289
290(* Unsigned divisions and modulos *)
291
292let divumodu_fun res t s =
293  "unsigned " ^ t ^ " " ^ s ^ " (unsigned " ^ t ^ " x, unsigned " ^ t ^ " y)" ^
294    "{\n" ^
295  "  unsigned " ^ t ^ " quo = 0;\n" ^
296  "  unsigned " ^ t ^ " rem = x;\n" ^
297  "  while (rem >= y) {\n" ^
298  "    rem = rem - y;\n" ^
299  "    quo = quo + 1;\n" ^
300  "  }\n" ^
301  "  return (" ^ res ^ ");\n" ^
302  "}\n\n"
303
304let divumodu op sizes sizec t =
305  let (prefix, res) = match op with
306    | Clight.Odiv -> ("div", "quo")
307    | Clight.Omod -> ("mod", "rem")
308    | _ -> assert false (* do not use on these arguments *) in
309  let cu = cintu sizec in
310  (Binary (op, cu, cu), "_" ^ prefix ^ sizes ^ "u", divumodu_fun res t, [])
311
312let divu = divumodu Clight.Odiv
313let modu = divumodu Clight.Omod
314
315
316(* Unsigned divisions *)
317
318(* 16 bits unsigned division *)
319
320let div16u = divu "16" Clight.I16 "short"
321
322(* 32 bits unsigned division *)
323
324let div32u = divu "32" Clight.I32 "int"
325
326(* Signed divisions *)
327
328let divs_fun t s =
329  "signed " ^ t ^ " " ^ s ^ " (signed " ^ t ^ " x, signed " ^ t ^ " y) {\n" ^
330  "  unsigned " ^ t ^ " x1 = (unsigned " ^ t ^ ") x;\n" ^
331  "  unsigned " ^ t ^ " y1 = (unsigned " ^ t ^ ") y;\n" ^
332  "  signed " ^ t ^ " sign = 1;\n" ^
333  "  if (x < 0) { x1 = (unsigned " ^ t ^ ") (-x); sign = -sign; }\n" ^
334  "  if (y < 0) { y1 = (unsigned " ^ t ^ ") (-y); sign = -sign; }\n" ^
335  "  return (sign * ((signed " ^ t ^ ") (x1/y1)));\n" ^
336  "}\n\n"
337
338let divs sizes sizec t =
339  let cs = cints sizec in
340  let cu = cintu sizec in
341  (Binary (Clight.Odiv, cs, cs), "_div" ^ sizes ^ "s", divs_fun t,
342   [Binary (Clight.Odiv, cu, cu)])
343
344(* 8 bits signed division *)
345
346let div8s = divs "8" Clight.I8 "char"
347
348(* 16 bits signed division *)
349
350let div16s = divs "16" Clight.I16 "short"
351
352(* 32 bits signed division *)
353
354let div32s = divs "32" Clight.I32 "int"
355
356
357(* Unsigned modulos *)
358
359(* 16 bits unsigned modulo *)
360
361let mod16u = modu "16" Clight.I16 "short"
362
363(* 32 bits unsigned modulo *)
364
365let mod32u = modu "32" Clight.I32 "int"
366
367(* Signed modulos *)
368
369let mods_fun t s =
370  "signed " ^ t ^ " " ^ s ^ " (signed " ^ t ^ " x, signed " ^ t ^ " y) {\n" ^
371  "  return (x - (x/y) * y);\n" ^
372  "}\n\n"
373
374let mods size ct t =
375  (Binary (Clight.Omod, ct, ct), "_mod" ^ size ^ "s", mods_fun t,
376   [Binary (Clight.Odiv, ct, ct)])
377
378(* 8 bits signed modulo *)
379
380let mod8s = mods "8" cint8s "char"
381
382(* 16 bits signed modulo *)
383
384let mod16s = mods "16" cint16s "short"
385
386(* 32 bits signed modulo *)
387
388let mod32s = mods "32" cint32s "int"
389
390
391(* Shifts *)
392
393let sh_fun op t s =
394  t ^ " " ^ s ^ " (" ^ t ^ " x, " ^ t ^ " y) {\n" ^
395  "  " ^ t ^ " res = x, i;\n" ^
396  "  for (i = 0 ; i < y ; i++) res = res " ^ op ^ " 2;\n" ^
397  "  return res;\n" ^
398  "}\n\n"
399
400let sh cop sop direction deps size sign =
401  let sizes = string_of_intsize size in
402  let ct = Clight.Tint (size, sign) in
403  let (short_sign, long_sign) = match sign with
404    | AST.Signed -> ("s", "signed ")
405    | AST.Unsigned -> ("u", "unsigned ") in
406  let t = long_sign ^ (ctype_of_intsize size) in
407  (Binary (cop, ct, ct), "_sh" ^ direction ^ sizes ^ short_sign,
408   sh_fun sop t, deps)
409
410
411(* Shift lefts *)
412
413let shl = sh Clight.Oshl "*" "l" []
414
415(* Signed shift lefts *)
416
417(* 8 bits signed shift left *)
418
419let shl8s = shl Clight.I8 AST.Signed
420
421(* 16 bits signed shift left *)
422
423let shl16s = shl Clight.I16 AST.Signed
424
425(* 32 bits signed shift left *)
426
427let shl32s = shl Clight.I32 AST.Signed
428
429(* Unsigned shift lefts *)
430
431(* 8 bits unsigned shift left *)
432
433let shl8u = shl Clight.I8 AST.Unsigned
434
435(* 16 bits unsigned shift left *)
436
437let shl16u = shl Clight.I16 AST.Unsigned
438
439(* 32 bits unsigned shift left *)
440
441let shl32u = shl Clight.I32 AST.Unsigned
442
443
444(* Shift rights *)
445
446(* Signed shift rights *)
447
448let shrs_fun size t s =
449  "signed " ^ t ^ " " ^ s ^ " (signed " ^ t ^ " x, signed " ^ t ^ " y) {\n" ^
450  "  unsigned " ^ t ^ " x1, y1, to_add, res, i;\n" ^
451  "  if (y < 0) return 0;\n" ^
452  "  x1 = x; y1 = y; to_add = 1; res = x1;" ^
453  "  for (i = 0 ; i < " ^ size ^ " ; i++) to_add = to_add * 2;\n" ^
454  "  to_add = to_add & x1;\n" ^
455  "  for (i = 0 ; i < y1 ; i++) res = (res / 2) + to_add;\n" ^
456  "  return ((signed " ^ t ^ ") res);\n" ^
457  "}\n\n"
458
459let shrs size =
460  let sizes = string_of_int (bit_size_of_intsize size) in
461  let op_sizes = string_of_int ((bit_size_of_intsize size) - 1) in
462  let t = ctype_of_intsize size in
463  let ct = Clight.Tint (size, AST.Signed) in
464  let ctdep = Clight.Tint (size, AST.Unsigned) in
465  (Binary (Clight.Oshr, ct, ct), "_shr" ^ sizes ^ "s", shrs_fun op_sizes t,
466   [Binary (Clight.Odiv, ctdep, ctdep)])
467
468(* 8 bits signed shift right *)
469
470let shr8s = shrs Clight.I8
471
472(* 16 bits signed shift right *)
473
474let shr16s = shrs Clight.I16
475
476(* 32 bits signed shift right *)
477
478let shr32s = shrs Clight.I32
479
480(* Unsigned shift rights *)
481
482let shru size =
483  let t_dep = Clight.Tint (size, AST.Unsigned) in
484  sh Clight.Oshr "/" "r" [Binary (Clight.Odiv, t_dep, t_dep)] size AST.Unsigned
485
486(* 8 bits unsigned shift right *)
487
488let shr8u = shru Clight.I8
489
490(* 16 bits unsigned shift right *)
491
492let shr16u = shru Clight.I16
493
494(* 32 bits unsigned shift right *)
495
496let shr32u = shru Clight.I32
497
498
499let unsupported =
500  [div16u ; div32u ; div8s ; div16s ; div32s ;
501   mod16u ; mod32u ; mod8s ; mod16s ; mod32s ;
502   shl8s ; shl16s ; shl32s ; shl8u ; shl16u ; shl32u ;
503   shr8s ; shr16s ; shr32s ; shr8u ; shr16u ; shr32u]
504
505
506let replace_unsupported p = add_replacements p unsupported
Note: See TracBrowser for help on using the repository browser.