source: Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightPrinter.ml @ 489

Last change on this file since 489 was 489, checked in by campbell, 8 years ago

Pointer fixes for the temporary version of the compiler that can output matita
terms.

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