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

Last change on this file since 3673 was 1542, checked in by tranquil, 8 years ago

merge of indexed labels branch

File size: 16.9 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(** Pretty-printer for Csyntax *)
17
18open Format
19open AST
20open Clight
21
22let name_unop = function
23  | Onotbool -> "!"
24  | Onotint  -> "~"
25  | Oneg     -> "-"
26
27
28let name_binop = function
29  | Oadd -> "+"
30  | Osub -> "-"
31  | Omul -> "*"
32  | Odiv -> "/"
33  | Omod -> "%"
34  | Oand -> "&"
35  | Oor  -> "|"
36  | Oxor -> "^"
37  | Oshl -> "<<"
38  | Oshr -> ">>"
39  | Oeq  -> "=="
40  | One  -> "!="
41  | Olt  -> "<"
42  | Ogt  -> ">"
43  | Ole  -> "<="
44  | Oge  -> ">="
45
46let name_inttype sz sg =
47  match sz, sg with
48  | I8, Signed -> "signed char"
49  | I8, Unsigned -> "unsigned char"
50  | I16, Signed -> "short"
51  | I16, Unsigned -> "unsigned short"
52  | I32, Signed -> "int"
53  | I32, Unsigned -> "unsigned int"
54
55let name_floattype sz =
56  match sz with
57  | F32 -> "float"
58  | F64 -> "double"
59
60(* Collecting the names and fields of structs and unions *)
61
62module StructUnionSet = Set.Make(struct
63  type t = string * (ident*ctype) list
64  let compare (n1, _ : t) (n2, _ : t) = compare n1 n2
65end)
66
67let struct_unions = ref StructUnionSet.empty
68
69let register_struct_union id fld =
70  struct_unions := StructUnionSet.add (id, fld) !struct_unions
71
72(* Declarator (identifier + type) *)
73
74let name_optid id =
75  if id = "" then "" else " " ^ id
76
77let parenthesize_if_pointer id =
78  if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
79
80let rec name_cdecl id ty =
81  match ty with
82  | Tvoid ->
83      "void" ^ name_optid id
84  | Tint(sz, sg) ->
85      name_inttype sz sg ^ name_optid id
86  | Tfloat sz ->
87      name_floattype sz ^ name_optid id
88  | Tpointer t ->
89      name_cdecl ("*" ^ id) t
90  | Tarray(t, n) ->
91      name_cdecl
92        (sprintf "%s[%ld]" (parenthesize_if_pointer id) (Int32.of_int n))
93        t
94  | Tfunction(args, res) ->
95      let b = Buffer.create 20 in
96      if id = ""
97      then Buffer.add_string b "(*)"
98      else Buffer.add_string b (parenthesize_if_pointer id);
99      Buffer.add_char b '(';
100      begin match args with
101      | [] ->
102          Buffer.add_string b "void"
103      | _ ->
104          let rec add_args first = function
105          | [] -> ()
106          | t1::tl ->
107              if not first then Buffer.add_string b ", ";
108              Buffer.add_string b (name_cdecl "" t1);
109              add_args false tl in
110          add_args true args
111      end;
112      Buffer.add_char b ')';
113      name_cdecl (Buffer.contents b) res
114  | Tstruct(name, fld) ->
115      name ^ name_optid id
116  | Tunion(name, fld) ->
117      name ^ name_optid id
118  | Tcomp_ptr name ->
119      name ^ " *" ^ id
120
121(* Type *)
122
123let name_type ty = name_cdecl "" ty
124
125(* Expressions *)
126
127let parenthesis_level (Expr (e, ty)) =
128  match e with
129  | Econst_int _ -> 0
130  | Econst_float _ -> 0
131  | Evar _ -> 0
132  | Eunop(_, _) -> 30
133  | Ederef _ -> 20
134  | Eaddrof _ -> 30
135  | Ebinop(op, _, _) ->
136      begin match op with
137      | Oand | Oor | Oxor -> 75
138      | Oeq | One | Olt | Ogt | Ole | Oge -> 70
139      | Oadd | Osub | Oshl | Oshr -> 60
140      | Omul | Odiv | Omod -> 40
141      end
142  | Ecast _ -> 30
143  | Econdition(_, _, _) -> 80
144  | Eandbool(_, _) -> 80
145  | Eorbool(_, _) -> 80
146  | Esizeof _ -> 20
147  | Efield _ -> 20
148  | Ecost (_,_) -> 20 
149  | Ecall (_,_,_) -> 20
150
151let rec print_expr p (Expr (eb, ty) as e) =
152  let level = parenthesis_level e in
153  match eb with
154  | Econst_int n ->
155      fprintf p "%ld" (Int32.of_int n)
156  | Econst_float f ->
157      fprintf p "%F" f
158  | Evar id ->
159      fprintf p "%s" id
160  | Eunop(op, e1) ->
161      fprintf p "%s%a" (name_unop op) print_expr_prec (level, e1)
162  | Ederef (Expr (Ebinop(Oadd, e1, e2), _)) ->
163      fprintf p "@[<hov 2>%a@,[%a]@]"
164                print_expr_prec (level, e1)
165                print_expr_prec (level, e2)
166  | Ederef (Expr (Efield(e1, id), _)) ->
167      fprintf p "%a->%s" print_expr_prec (level, e1) id
168  | Ederef e ->
169      fprintf p "*%a" print_expr_prec (level, e)
170  | Eaddrof e ->
171      fprintf p "&%a" print_expr_prec (level, e)
172  | Ebinop(op, e1, e2) ->
173      fprintf p "@[<hov 0>%a@ %s %a@]"
174                print_expr_prec (level, e1)
175                (name_binop op)
176                print_expr_prec (level, e2)
177  | Ecast(ty, e1) ->
178      fprintf p "@[<hov 2>(%s)@,%a@]"
179                (name_type ty)
180                print_expr_prec (level, e1)
181  | Econdition(e1, e2, e3) ->
182      fprintf p "@[<hov 0>%a@ ? %a@ : %a@]"
183                print_expr_prec (level, e1)
184                print_expr_prec (level, e2)
185                print_expr_prec (level, e3)
186  | Eandbool(e1, e2) ->
187      fprintf p "@[<hov 0>%a@ && %a@]"
188                print_expr_prec (level, e1)
189                print_expr_prec (level, e2)
190  | Eorbool(e1, e2) ->
191      fprintf p "@[<hov 0>%a@ || %a@]"
192                print_expr_prec (level, e1)
193                print_expr_prec (level, e2)
194  | Esizeof ty ->
195      fprintf p "sizeof(%s)" (name_type ty)
196  | Efield(e1, id) ->
197      fprintf p "%a.%s" print_expr_prec (level, e1) id
198  | Ecost(lbl, e1) ->
199    (* printing label uglily even if in comment for consistence *)
200    let lbl = CostLabel.string_of_cost_label lbl in
201    fprintf p "(/* %s */ %a)" lbl print_expr e1
202  | Ecall(f, arg, e) ->
203      fprintf p "(%s(%a), %a)" f print_expr arg print_expr e
204
205and print_expr_prec p (context_prec, e) =
206  let this_prec = parenthesis_level e in
207  if this_prec >= context_prec
208  then fprintf p "(%a)" print_expr e
209  else print_expr p e
210
211let rec print_expr_list p (first, el) =
212  match el with
213  | [] -> ()
214  | e1 :: et ->
215      if not first then fprintf p ",@ ";
216      print_expr p e1;
217      print_expr_list p (false, et)
218
219let print_loop_depth p = function
220  | None -> fprintf p ""
221  | Some x -> fprintf p "/* single entry loop depth: %d */@," x
222
223let rec print_stmt p s =
224  match s with
225  | Sskip ->
226      fprintf p "/*skip*/;"
227  | Sassign(e1, e2) ->
228      fprintf p "@[<hv 2>%a =@ %a;@]" print_expr e1 print_expr e2
229  | Scall(None, e1, el) ->
230      fprintf p "@[<hv 2>%a@,(@[<hov 0>%a@]);@]"
231                print_expr e1
232                print_expr_list (true, el)
233  | Scall(Some lhs, e1, el) ->
234      fprintf p "@[<hv 2>%a =@ %a@,(@[<hov 0>%a@]);@]"
235                print_expr lhs
236                print_expr e1
237                print_expr_list (true, el)
238  | Ssequence(s1, s2) ->
239      fprintf p "%a@ %a" print_stmt s1 print_stmt s2
240  | Sifthenelse(e, s1, Sskip) ->
241      fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>}@]"
242              print_expr e
243              print_stmt s1
244  | Sifthenelse(e, s1, s2) ->
245      fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]"
246              print_expr e
247              print_stmt s1
248              print_stmt s2
249  | Swhile(i, e, s) ->
250    fprintf p "@[<v 0>%a@[<v 2>while (%a) {@ %a@;<0 -2>}@]@]"
251      print_loop_depth i
252      print_expr e
253      print_stmt s
254  | Sdowhile(i, e, s) ->
255    fprintf p "@[<v 0>%a@[<v 2>do {@ %a@;<0 -2>} while(%a);@]@]"
256      print_loop_depth i
257      print_stmt s
258      print_expr e
259  | Sfor(i, s_init, e, s_iter, s_body) ->
260    fprintf p "@[<v 0>%a@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]@]"
261      print_loop_depth i
262      print_stmt_for s_init
263      print_expr e
264      print_stmt_for s_iter
265      print_stmt s_body
266  | Sbreak ->
267    fprintf p "break;"
268  | Scontinue ->
269    fprintf p "continue;"
270  | Sswitch(e, cases) ->
271    fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]"
272      print_expr e
273      print_cases cases
274  | Sreturn None ->
275    fprintf p "return;"
276  | Sreturn (Some e) ->
277    fprintf p "return %a;" print_expr e
278  | Slabel(lbl, s1) ->
279    fprintf p "%s:@ %a" lbl print_stmt s1
280  | Sgoto lbl ->
281    fprintf p "goto %s;" lbl
282  | Scost (lbl,s1) ->
283    let lbl = CostLabel.string_of_cost_label lbl in
284     fprintf p "%s:@ %a" lbl print_stmt s1
285
286and print_cases p cases =
287  match cases with
288  | LSdefault Sskip ->
289      ()
290  | LSdefault s ->
291      fprintf p "@[<v 2>default:@ %a@]" print_stmt s
292  | LScase(lbl, Sskip, rem) ->
293      fprintf p "case %ld:@ %a"
294        (Int32.of_int lbl)
295        print_cases rem
296  | LScase(lbl, s, rem) ->
297      fprintf p "@[<v 2>case %ld:@ %a@]@ %a"
298              (Int32.of_int lbl)
299              print_stmt s
300              print_cases rem
301
302and print_stmt_for p s =
303  match s with
304  | Sskip ->
305      fprintf p "/*nothing*/"
306  | Sassign(e1, e2) ->
307      fprintf p "%a = %a" print_expr e1 print_expr e2
308  | Ssequence(s1, s2) ->
309      fprintf p "%a, %a" print_stmt_for s1 print_stmt_for s2
310  | Scall(None, e1, el) ->
311      fprintf p "@[<hv 2>%a@,(@[<hov 0>%a@])@]"
312                print_expr e1
313                print_expr_list (true, el)
314  | Scall(Some lhs, e1, el) ->
315      fprintf p "@[<hv 2>%a =@ %a@,(@[<hov 0>%a@])@]"
316                print_expr lhs
317                print_expr e1
318                print_expr_list (true, el)
319  | _ ->
320      fprintf p "({ %a })" print_stmt s
321
322let name_function_parameters fun_name params =
323  let b = Buffer.create 20 in
324  Buffer.add_string b fun_name;
325  Buffer.add_char b '(';
326  begin match params with
327  | [] ->
328      Buffer.add_string b "void"
329  | _ ->
330      let rec add_params first = function
331      | [] -> ()
332      | (id, ty) :: rem ->
333          if not first then Buffer.add_string b ", ";
334          Buffer.add_string b (name_cdecl id ty);
335          add_params false rem in
336      add_params true params
337  end;
338  Buffer.add_char b ')';
339  Buffer.contents b
340
341let print_function p id f =
342  fprintf p "%s@ "
343            (name_cdecl (name_function_parameters id f.fn_params)
344                        f.fn_return);
345  fprintf p "@[<v 2>{@ ";
346  List.iter
347    (fun ((id, ty)) ->
348      fprintf p "%s;@ " (name_cdecl id ty))
349    f.fn_vars;
350  print_stmt p f.fn_body;
351  fprintf p "@;<0 -2>}@]@ @ "
352
353let print_fundef p (id, fd) =
354  match fd with
355  | External(_, args, res) ->
356      fprintf p "extern %s;@ @ "
357                (name_cdecl id (Tfunction(args, res)))
358  | Internal f ->
359      print_function p id f
360
361let string_of_init id =
362  let b = Buffer.create (List.length id) in
363  let add_init = function
364  | Init_int8 n ->
365      if n >= 32 && n <= 126 && n <> Char.code '\"' && n <> Char.code '\\'
366      then Buffer.add_char b (Char.chr n)
367      else Buffer.add_string b (Printf.sprintf "\\%03o" n)
368  | _ ->
369      assert false
370  in List.iter add_init id; Buffer.contents b
371
372let chop_last_nul id =
373  match List.rev id with
374  | Init_int8 0 :: tl -> List.rev tl
375  | _ -> id
376
377let print_init p = function
378  | Init_int8 n -> fprintf p "%ld,@ " (Int32.of_int n)
379  | Init_int16 n -> fprintf p "%ld,@ " (Int32.of_int n)
380  | Init_int32 n -> fprintf p "%ld,@ " (Int32.of_int n)
381  | Init_float32 n -> fprintf p "%F,@ " n
382  | Init_float64 n -> fprintf p "%F,@ " n
383  | Init_space n -> fprintf p "/* skip %ld, */@ " (Int32.of_int n)
384  | Init_addrof(symb, ofs) ->
385      let ofs = Int32.of_int ofs in
386      if ofs = Int32.zero
387      then fprintf p "&%s,@ " symb
388      else fprintf p "(void *)((char *)&%s + %ld),@ " symb ofs
389
390let print_init1 p = function
391  | Init_int8 n -> fprintf p "%ld" (Int32.of_int n)
392  | Init_int16 n -> fprintf p "%ld" (Int32.of_int n)
393  | Init_int32 n -> fprintf p "%ld" (Int32.of_int n)
394  | Init_float32 n -> fprintf p "%F" n
395  | Init_float64 n -> fprintf p "%F" n
396  | Init_space n -> fprintf p "/* skip %ld */" (Int32.of_int n)
397  | Init_addrof(symb, ofs) ->
398      let ofs = Int32.of_int ofs in
399      if ofs = Int32.zero
400      then fprintf p "&%s" symb
401      else fprintf p "(void *)((char *)&%s + %ld)" symb ofs
402
403let re_string_literal = Str.regexp "__stringlit_[0-9]+"
404
405let print_globvar p (((id, init), ty)) =
406  match init with
407  | [] ->
408      fprintf p "extern %s;@ @ "
409              (name_cdecl id ty)
410  | [Init_space _] ->
411      fprintf p "%s;@ @ "
412              (name_cdecl id ty)
413  | [init] ->
414      fprintf p "@[<hov 2>%s = %a;@]@ @ "
415              (name_cdecl id ty) print_init1 init
416  | _ ->
417      fprintf p "@[<hov 2>%s = "
418              (name_cdecl id ty);
419      if Str.string_match re_string_literal id 0
420      && List.for_all (function Init_int8 _ -> true | _ -> false) init
421      then
422        fprintf p "\"%s\"" (string_of_init (chop_last_nul init))
423      else begin
424        fprintf p "{@ ";
425        List.iter (print_init p) init;
426        fprintf p "}"
427      end;
428      fprintf p ";@]@ @ "
429
430(* Collect struct and union types *)
431
432let rec collect_type = function
433  | Tvoid -> ()
434  | Tint(sz, sg) -> ()
435  | Tfloat sz -> ()
436  | Tpointer t -> collect_type t
437  | Tarray(t, n) -> collect_type t
438  | Tfunction(args, res) -> collect_type_list args; collect_type res
439  | Tstruct(id, fld) -> register_struct_union id fld; collect_fields fld
440  | Tunion(id, fld) -> register_struct_union id fld; collect_fields fld
441  | Tcomp_ptr _ -> ()
442
443and collect_type_list = function
444  | [] -> ()
445  | hd::tl -> collect_type hd; collect_type_list tl
446
447and collect_fields = function
448  | [] -> ()
449  | (id, hd)::tl -> collect_type hd; collect_fields tl
450
451let rec collect_expr (Expr(ed, ty)) =
452  match ed with
453  | Econst_int n -> ()
454  | Econst_float f -> ()
455  | Evar id -> ()
456  | Eunop(op, e1) -> collect_expr e1
457  | Ederef e -> collect_expr e
458  | Eaddrof e -> collect_expr e
459  | Ebinop(op, e1, e2) -> collect_expr e1; collect_expr e2
460  | Ecast(ty, e1) -> collect_type ty; collect_expr e1
461  | Econdition(e1, e2, e3) -> collect_expr e1; collect_expr e2; collect_expr e3
462  | Eandbool(e1, e2) -> collect_expr e1; collect_expr e2
463  | Eorbool(e1, e2) -> collect_expr e1; collect_expr e2
464  | Esizeof ty -> collect_type ty
465  | Efield(e1, id) -> collect_expr e1
466  | Ecost(_, e) -> collect_expr e
467  | Ecall(_, arg, e) -> collect_expr arg; collect_expr e
468
469let rec collect_expr_list = function
470  | [] -> ()
471  | hd :: tl -> collect_expr hd; collect_expr_list tl
472
473let rec collect_stmt = function
474  | Sskip -> ()
475  | Sassign(e1, e2) -> collect_expr e1; collect_expr e2
476  | Scall(None, e1, el) -> collect_expr e1; collect_expr_list el
477  | Scall(Some lhs, e1, el) -> collect_expr lhs; collect_expr e1; collect_expr_list el
478  | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
479  | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
480  | Swhile(_, e, s) -> collect_expr e; collect_stmt s
481  | Sdowhile(_, e, s) -> collect_stmt s; collect_expr e
482  | Sfor(_, s_init, e, s_iter, s_body) ->
483    collect_stmt s_init; collect_expr e;
484    collect_stmt s_iter; collect_stmt s_body
485  | Sbreak -> ()
486  | Scontinue -> ()
487  | Sswitch(e, cases) -> collect_expr e; collect_cases cases
488  | Sreturn None -> ()
489  | Sreturn (Some e) -> collect_expr e
490  | Slabel(lbl, s) -> collect_stmt s
491  | Sgoto lbl -> ()
492  | Scost (_,s1) -> collect_stmt s1
493
494and collect_cases = function
495  | LSdefault s -> collect_stmt s
496  | LScase(lbl, s, rem) -> collect_stmt s; collect_cases rem
497
498let collect_function f =
499  collect_type f.fn_return;
500  List.iter (fun ((id, ty)) -> collect_type ty) f.fn_params;
501  List.iter (fun ((id, ty)) -> collect_type ty) f.fn_vars;
502  collect_stmt f.fn_body
503
504let collect_fundef ((id, fd)) =
505  match fd with
506  | External(_, args, res) -> collect_type_list args; collect_type res
507  | Internal f -> collect_function f
508
509let collect_globvar (((id, init), ty)) =
510  collect_type ty
511
512let collect_program p =
513  List.iter collect_globvar p.prog_vars;
514  List.iter collect_fundef p.prog_funct
515
516let declare_struct_or_union p (name, fld) =
517  fprintf p "%s;@ @ " name
518
519let print_struct_or_union p (name, fld) =
520  fprintf p "@[<v 2>%s {" name;
521  let rec print_fields = function
522  | [] -> ()
523  | (id, ty)::rem ->
524      fprintf p "@ %s;" (name_cdecl id ty);
525      print_fields rem in
526  print_fields fld;
527  fprintf p "@;<0 -2>};@]@ "
528
529let print_program_2 p prog =
530  struct_unions := StructUnionSet.empty;
531  collect_program prog;
532  fprintf p "@[<v 0>";
533  StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
534  StructUnionSet.iter (print_struct_or_union p) !struct_unions;
535  List.iter (print_globvar p) prog.prog_vars;
536  List.iter (print_fundef p) prog.prog_funct;
537  fprintf p "@]@."
538
539let print_program prog =
540  print_program_2 str_formatter prog;
541  flush_str_formatter ()
542
543let string_of_ctype = name_type
544
545let print_expression e = 
546  print_expr str_formatter e;
547  flush_str_formatter ()
548
549let print_statement s = 
550  print_stmt str_formatter s;
551  flush_str_formatter ()
552
553let print_ctype_prot = name_type
554
555let print_ctype_def = function
556  | Tstruct (name, fld) | Tunion (name, fld) ->
557    let f_fld s (id, t) = s ^ "  " ^ (print_ctype_prot t) ^ " " ^ id ^ ";\n" in
558    let s_fld = List.fold_left f_fld "" in
559    name ^ " {\n" ^ (s_fld fld) ^ "};\n"
560  | _ -> "" (* no definition associated to the other types *)
Note: See TracBrowser for help on using the repository browser.