source: Deliverables/D2.3/8051/cparser/Cprint.ml @ 453

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

Import of the Paris's sources.

File size: 16.0 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 C abstract syntax *)
17
18open Format
19open C
20
21let print_idents_in_full = ref false
22
23let print_line_numbers = ref false
24
25let location pp (file, lineno) =
26  if !print_line_numbers && lineno >= 0 then
27    fprintf pp "# %d \"%s\"@ " lineno file
28
29let ident pp i =
30  if !print_idents_in_full
31  then fprintf pp "%s$%d" i.name i.stamp
32  else fprintf pp "%s" i.name
33
34let attribute pp = function
35  | AConst -> fprintf pp "const"
36  | AVolatile -> fprintf pp "volatile"
37  | ARestrict -> fprintf pp "restrict"
38
39let attributes pp = function
40  | [] -> ()
41  | al -> List.iter (fun a -> fprintf pp " %a" attribute a) al
42
43let name_of_ikind = function
44  | IBool -> "_Bool"
45  | IChar -> "char"
46  | ISChar -> "signed char"
47  | IUChar -> "unsigned char"
48  | IInt -> "int"
49  | IUInt -> "unsigned int"
50  | IShort -> "short"
51  | IUShort -> "unsigned short"
52  | ILong -> "long"
53  | IULong -> "unsigned long"
54  | ILongLong -> "long long"
55  | IULongLong -> "unsigned long long"
56
57let name_of_fkind = function
58  | FFloat -> "float"
59  | FDouble -> "double"
60  | FLongDouble -> "long double"
61
62let rec dcl pp ty n =
63  match ty with
64  | TVoid a ->
65      fprintf pp "void%a%t" attributes a n
66  | TInt(k, a) ->
67      fprintf pp "%s%a%t" (name_of_ikind k) attributes a n
68  | TFloat(k, a) ->
69      fprintf pp "%s%a%t" (name_of_fkind k) attributes a n
70  | TPtr(t, a) ->
71      let n' pp =
72        match t with
73        | TFun _ | TArray _ -> fprintf pp " (*%a%t)" attributes a n
74        | _ -> fprintf pp " *%a%t" attributes a n in
75      dcl pp t n'
76  | TArray(t, sz, a) ->
77      let n' pp =
78        begin match a with
79        | [] -> n pp
80        | _  -> fprintf pp " (%a%t)" attributes a n
81        end;
82        begin match sz with
83        | None -> fprintf pp "[]"
84        | Some i -> fprintf pp "[%Ld]" i
85        end in
86      dcl pp t n'
87  | TFun(tres, args, vararg, a) ->
88      let param (id, ty) =
89        dcl pp ty
90          (fun pp -> fprintf pp " %a" ident id) in
91      let n' pp =
92        begin match a with
93        | [] -> n pp
94        | _  -> fprintf pp " (%a%t)" attributes a n
95        end;
96        fprintf pp "(@[<hov 0>";
97        begin match args with
98        | None -> ()
99        | Some [] -> if vararg then fprintf pp "..." else fprintf pp "void"
100        | Some (a1 :: al) ->
101            param a1;
102            List.iter (fun a -> fprintf pp ",@ "; param a) al;
103            if vararg then fprintf pp ",@ ..."
104        end;
105        fprintf pp "@])" in
106      dcl pp tres n'
107  | TNamed(id, a) ->
108      fprintf pp "%a%a%t" ident id attributes a n
109  | TStruct(id, a) ->
110      fprintf pp "struct %a%a%t" ident id attributes a n
111  | TUnion(id, a) ->
112      fprintf pp "union %a%a%t" ident id attributes a n
113
114let typ pp ty =
115  dcl pp ty (fun _ -> ())
116
117let const pp = function
118  | CInt(v, ik, s) ->
119      if s <> "" then
120        fprintf pp "%s" s
121      else begin
122        fprintf pp "%Ld" v;
123        match ik with
124        | IULongLong -> fprintf pp "ULL"
125        | ILongLong -> fprintf pp "LL"
126        | IULong -> fprintf pp "UL"
127        | ILong -> fprintf pp "L"
128        | IUInt -> fprintf pp "U"
129        | _ -> ()
130      end
131  | CFloat(v, fk, s) ->
132      if s <> "" then
133        fprintf pp "%s" s
134      else begin
135        fprintf pp "%.18g" v;
136        match fk with
137        | FFloat -> fprintf pp "F"
138        | FLongDouble -> fprintf pp "L"
139        | _ -> ()
140      end
141  | CStr s ->
142      fprintf pp "\"";
143      for i = 0 to String.length s - 1 do
144        match s.[i] with
145        | '\009' -> fprintf pp "\\t"
146        | '\010' -> fprintf pp "\\n"
147        | '\013' -> fprintf pp "\\r"
148        | '\"'   -> fprintf pp "\\\""
149        | '\\'   -> fprintf pp "\\\\"
150        | c ->
151            if c >= ' ' && c <= '~'
152            then fprintf pp "%c" c
153            else fprintf pp "\\%03o" (Char.code c)
154      done;
155      fprintf pp "\""
156  | CWStr l ->
157      fprintf pp "L\"";
158      List.iter
159        (fun c ->
160          if c >= 32L && c <= 126L && c <> 34L && c <>92L
161          then fprintf pp "%c" (Char.chr (Int64.to_int c))
162          else fprintf pp "\" \"\\x%02Lx\" \"" c)
163        l;     
164      fprintf pp "\""
165  | CEnum(id, v) ->
166      ident pp id
167
168type associativity = LtoR | RtoL | NA
169
170let precedence = function               (* H&S section 7.2 *)
171  | EConst _ -> (16, NA)
172  | ESizeof _ -> (15, RtoL)
173  | EVar _ -> (16, NA)
174  | EBinop(Oindex, _, _, _) -> (16, LtoR)
175  | ECall _ -> (16, LtoR)
176  | EUnop((Odot _|Oarrow _), _) -> (16, LtoR)
177  | EUnop((Opostincr|Opostdecr), _) -> (16, LtoR)
178  | EUnop((Opreincr|Opredecr|Onot|Olognot|Ominus|Oplus|Oaddrof|Oderef), _) -> (15, RtoL)
179  | ECast _ -> (14, RtoL)
180  | EBinop((Omul|Odiv|Omod), _, _, _) -> (13, LtoR)
181  | EBinop((Oadd|Osub), _, _, _) -> (12, LtoR)
182  | EBinop((Oshl|Oshr), _, _, _) -> (11, LtoR)
183  | EBinop((Olt|Ogt|Ole|Oge), _, _, _) -> (10, LtoR)
184  | EBinop((Oeq|One), _, _, _) -> (9, LtoR)
185  | EBinop(Oand, _, _, _) -> (8, LtoR)
186  | EBinop(Oxor, _, _, _) -> (7, LtoR)
187  | EBinop(Oor, _, _, _) -> (6, LtoR)
188  | EBinop(Ologand, _, _, _) -> (5, LtoR)
189  | EBinop(Ologor, _, _, _) -> (4, LtoR)
190  | EConditional _ -> (3, RtoL)
191  | EBinop((Oassign|Oadd_assign|Osub_assign|Omul_assign|Odiv_assign|Omod_assign|Oand_assign|Oor_assign|Oxor_assign|Oshl_assign|Oshr_assign), _, _, _) -> (2, RtoL)
192  | EBinop(Ocomma, _, _, _) -> (1, LtoR)
193
194let rec exp pp (prec, a) =
195  let (prec', assoc) = precedence a.edesc in
196  let (prec1, prec2) =
197    if assoc = LtoR
198    then (prec', prec' + 1)
199    else (prec' + 1, prec') in
200  if prec' < prec
201  then fprintf pp "@[<hov 2>("
202  else fprintf pp "@[<hov 2>";
203  begin match a.edesc with
204  | EConst cst -> const pp cst
205  | EVar id -> ident pp id
206  | ESizeof ty -> fprintf pp "sizeof(%a)" typ ty
207  | EUnop(Ominus, a1) ->
208      fprintf pp "-%a" exp (prec', a1)
209  | EUnop(Oplus, a1) ->
210      fprintf pp "+%a" exp (prec', a1)
211  | EUnop(Olognot, a1) ->
212      fprintf pp "!%a" exp (prec', a1)
213  | EUnop(Onot, a1) ->
214      fprintf pp "~%a" exp (prec', a1)
215  | EUnop(Oderef, a1) ->
216      fprintf pp "*%a" exp (prec', a1)
217  | EUnop(Oaddrof, a1) ->
218      fprintf pp "&%a" exp (prec', a1)
219  | EUnop(Opreincr, a1) ->
220      fprintf pp "++%a" exp (prec', a1)
221  | EUnop(Opredecr, a1) ->
222      fprintf pp "--%a" exp (prec', a1)
223  | EUnop(Opostincr, a1) ->
224      fprintf pp "%a++" exp (prec', a1)
225  | EUnop(Opostdecr, a1) ->
226      fprintf pp "%a--" exp (prec', a1)
227  | EUnop(Odot s, a1) ->
228      fprintf pp "%a.%s" exp (prec', a1)s
229  | EUnop(Oarrow s, a1) ->
230      fprintf pp "%a->%s" exp (prec', a1)s
231  | EBinop(Oadd, a1, a2, _) ->
232      fprintf pp "%a@ + %a" exp (prec1, a1) exp (prec2, a2)
233  | EBinop(Osub, a1, a2, _) ->
234      fprintf pp "%a@ - %a" exp (prec1, a1) exp (prec2, a2)
235  | EBinop(Omul, a1, a2, _) ->
236      fprintf pp "%a@ * %a" exp (prec1, a1) exp (prec2, a2)
237  | EBinop(Odiv, a1, a2, _) ->
238      fprintf pp "%a@ / %a" exp (prec1, a1) exp (prec2, a2)
239  | EBinop(Omod, a1, a2, _) ->
240      fprintf pp "%a@ %% %a" exp (prec1, a1) exp (prec2, a2)
241  | EBinop(Oand, a1, a2, _) ->
242      fprintf pp "%a@ & %a" exp (prec1, a1) exp (prec2, a2)
243  | EBinop(Oor, a1, a2, _) ->
244      fprintf pp "%a@ | %a" exp (prec1, a1) exp (prec2, a2)
245  | EBinop(Oxor, a1, a2, _) ->
246      fprintf pp "%a@ ^ %a" exp (prec1, a1) exp (prec2, a2)
247  | EBinop(Oshl, a1, a2, _) ->
248      fprintf pp "%a@ << %a" exp (prec1, a1) exp (prec2, a2)
249  | EBinop(Oshr, a1, a2, _) ->
250      fprintf pp "%a@ >> %a" exp (prec1, a1) exp (prec2, a2)
251  | EBinop(Oeq, a1, a2, _) ->
252      fprintf pp "%a@ == %a" exp (prec1, a1) exp (prec2, a2)
253  | EBinop(One, a1, a2, _) ->
254      fprintf pp "%a@ != %a" exp (prec1, a1) exp (prec2, a2)
255  | EBinop(Olt, a1, a2, _) ->
256      fprintf pp "%a@ < %a" exp (prec1, a1) exp (prec2, a2)
257  | EBinop(Ogt, a1, a2, _) ->
258      fprintf pp "%a@ > %a" exp (prec1, a1) exp (prec2, a2)
259  | EBinop(Ole, a1, a2, _) ->
260      fprintf pp "%a@ <= %a" exp (prec1, a1) exp (prec2, a2)
261  | EBinop(Oge, a1, a2, _) ->
262      fprintf pp "%a@ >= %a" exp (prec1, a1) exp (prec2, a2)
263  | EBinop(Oindex, a1, a2, _) ->
264      fprintf pp "%a[%a]" exp (prec1, a1) exp (0, a2)
265  | EBinop(Oassign, a1, a2, _) ->
266      fprintf pp "%a =@ %a" exp (prec1, a1) exp (prec2, a2)
267  | EBinop(Oadd_assign, a1, a2, _) ->
268      fprintf pp "%a +=@ %a" exp (prec1, a1) exp (prec2, a2)
269  | EBinop(Osub_assign, a1, a2, _) ->
270      fprintf pp "%a -=@ %a" exp (prec1, a1) exp (prec2, a2)
271  | EBinop(Omul_assign, a1, a2, _) ->
272      fprintf pp "%a *=@ %a" exp (prec1, a1) exp (prec2, a2)
273  | EBinop(Odiv_assign, a1, a2, _) ->
274      fprintf pp "%a /=@ %a" exp (prec1, a1) exp (prec2, a2)
275  | EBinop(Omod_assign, a1, a2, _) ->
276      fprintf pp "%a %%=@ %a" exp (prec1, a1) exp (prec2, a2)
277  | EBinop(Oand_assign, a1, a2, _) ->
278      fprintf pp "%a &=@ %a" exp (prec1, a1) exp (prec2, a2)
279  | EBinop(Oor_assign, a1, a2, _) ->
280      fprintf pp "%a |=@ %a" exp (prec1, a1) exp (prec2, a2)
281  | EBinop(Oxor_assign, a1, a2, _) ->
282      fprintf pp "%a ^=@ %a" exp (prec1, a1) exp (prec2, a2)
283  | EBinop(Oshl_assign, a1, a2, _) ->
284      fprintf pp "%a <<=@ %a" exp (prec1, a1) exp (prec2, a2)
285  | EBinop(Oshr_assign, a1, a2, _) ->
286      fprintf pp "%a >>=@ %a" exp (prec1, a1) exp (prec2, a2)
287  | EBinop(Ocomma, a1, a2, _) ->
288      fprintf pp "%a,@ %a" exp (prec1, a1) exp (prec2, a2)
289  | EBinop(Ologand, a1, a2, _) ->
290      fprintf pp "%a@ && %a" exp (prec1, a1) exp (prec2, a2)
291  | EBinop(Ologor, a1, a2, _) ->
292      fprintf pp "%a@ || %a" exp (prec1, a1) exp (prec2, a2)
293  | EConditional(a1, a2, a3) ->
294      fprintf pp "%a@ ? %a@ : %a" exp (4, a1) exp (4, a2) exp (4, a3)
295  | ECast(ty, a1) ->
296      fprintf pp "(%a) %a" typ ty exp (prec', a1)
297  | ECall({edesc = EVar {name = "__builtin_va_start"}},
298          [a1; {edesc = EUnop(Oaddrof, a2)}]) ->
299      fprintf pp "__builtin_va_start@[<hov 1>(%a,@ %a)@]"
300              exp (2, a1) exp (2, a2)
301  | ECall({edesc = EVar {name = "__builtin_va_arg"}},
302          [a1; {edesc = ESizeof ty}]) ->
303      fprintf pp "__builtin_va_arg@[<hov 1>(%a,@ %a)@]"
304              exp (2, a1) typ ty
305  | ECall(a1, al) ->
306      fprintf pp "%a@[<hov 1>(" exp (prec', a1);
307      begin match al with
308      | [] -> ()
309      | a1 :: al ->
310          fprintf pp "%a" exp (2, a1); 
311          List.iter (fun a -> fprintf pp ",@ %a" exp (2, a)) al
312      end;
313      fprintf pp ")@]"
314  end;
315  if prec' < prec then fprintf pp ")@]" else fprintf pp "@]"
316
317let rec init pp = function
318  | Init_single e ->
319      exp pp (2, e)
320  | Init_array il ->
321      fprintf pp "@[<hov 1>{";
322      List.iter (fun i -> fprintf pp "%a,@ " init i) il;
323      fprintf pp "}@]"
324  | Init_struct(id, il) ->
325      fprintf pp "@[<hov 1>{";
326      List.iter (fun (fld, i) -> fprintf pp "%a,@ " init i) il;
327      fprintf pp "}@]"
328  | Init_union(id, fld, i) ->
329      fprintf pp "@[<hov 1>{%a}@]" init i
330
331let simple_decl pp (id, ty) =
332  dcl pp ty (fun pp -> fprintf pp " %a" ident id)
333
334let storage pp = function
335  | Storage_default -> ()
336  | Storage_extern -> fprintf pp "extern "
337  | Storage_static -> fprintf pp "static "
338  | Storage_register -> fprintf pp "register "
339
340let full_decl pp (sto, id, ty, int) =
341  fprintf pp "@[<hov 2>%a" storage sto;
342  dcl pp ty (fun pp -> fprintf pp " %a" ident id);
343  begin match int with
344  | None -> ()
345  | Some i -> fprintf pp " =@ %a" init i
346  end;
347  fprintf pp ";@]"
348
349exception Not_expr
350
351let rec exp_of_stmt s =
352  match s.sdesc with
353  | Sdo e -> e
354  | Sseq(s1, s2) -> 
355      {edesc = EBinop(Ocomma, exp_of_stmt s1, exp_of_stmt s2, TVoid []);
356       etyp = TVoid []}
357  | Sif(e, s1, s2) ->
358      {edesc = EConditional(e, exp_of_stmt s1, exp_of_stmt s2);
359       etyp = TVoid []}
360  | _ ->
361      raise Not_expr
362
363let rec stmt pp s =
364  location pp s.sloc;
365  match s.sdesc with
366  | Sskip ->
367      fprintf pp "/*skip*/;"
368  | Sdo e ->
369      fprintf pp "%a;" exp (0, e)
370  | Sseq(s1, s2) ->
371      fprintf pp "%a@ %a" stmt s1 stmt s2
372  | Sif(e, s1, {sdesc = Sskip}) ->
373      fprintf pp "@[<v 2>if (%a) {@ %a@;<0 -2>}@]"
374              exp (0, e) stmt_block s1
375  | Sif(e, {sdesc = Sskip}, s2) ->
376      let not_e = {edesc = EUnop(Olognot, e); etyp = TInt(IInt, [])} in
377      fprintf pp "@[<v 2>if (%a) {@ %a@;<0 -2>}@]"
378              exp (0, not_e) stmt_block s2
379  | Sif(e, s1, s2) ->
380      fprintf pp  "@[<v 2>if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]"
381              exp (0, e) stmt_block s1 stmt_block s2
382  | Swhile(e, s1) ->
383      fprintf pp "@[<v 2>while (%a) {@ %a@;<0 -2>}@]"
384              exp (0, e) stmt_block s1
385  | Sdowhile(s1, e) ->
386      fprintf pp "@[<v 2>do {@ %a@;<0 -2>} while(%a);@]"
387              stmt_block s1 exp (0, e)
388  | Sfor(e1, e2, e3, s1) ->
389      fprintf pp "@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]"
390              opt_exp e1
391              exp (0, e2)
392              opt_exp e3
393              stmt_block s1
394  | Sbreak ->
395      fprintf pp "break;"
396  | Scontinue ->
397      fprintf pp "continue;"
398  | Sswitch(e, s1) ->
399      fprintf pp "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]"
400              exp (0, e)
401              stmt_block s1
402  | Slabeled(lbl, s1) ->
403      fprintf pp "%a:@ %a" slabel lbl stmt s1
404  | Sgoto lbl ->
405      fprintf pp "goto %s;" lbl
406  | Sreturn None ->
407      fprintf pp "return;"
408  | Sreturn (Some e) ->
409      fprintf pp "return %a;" exp (0, e)
410  | Sblock sl ->
411      fprintf pp "@[<v 2>{@ %a@;<0 -2>}@]" stmt_block s
412  | Sdecl d ->
413      full_decl pp d
414
415and slabel pp = function
416  | Slabel s ->
417      fprintf pp "%s" s
418  | Scase e ->
419      fprintf pp "case %a" exp (0, e)
420  | Sdefault ->
421      fprintf pp "default"
422
423and stmt_block pp s =
424  match s.sdesc with
425  | Sblock [] -> ()
426  | Sblock (s1 :: sl) ->
427      stmt pp s1;
428      List.iter (fun s -> fprintf pp "@ %a" stmt s) sl
429  | _ ->
430      stmt pp s
431
432and opt_exp pp s =
433  if s.sdesc = Sskip then fprintf pp "/*nothing*/" else
434    try
435      exp pp (0, exp_of_stmt s)
436    with Not_expr ->
437      fprintf pp "@[<v 3>({ %a })@]" stmt s
438
439let fundef pp f =
440  fprintf pp "@[<hov 2>%s%a"
441    (if f.fd_inline then "inline " else "")
442    storage f.fd_storage;
443  simple_decl pp (f.fd_name, TFun(f.fd_ret, Some f.fd_params, f.fd_vararg, []));
444  fprintf pp "@]@ @[<v 2>{@ ";
445  List.iter (fun d -> fprintf pp "%a@ " full_decl d) f.fd_locals;
446  stmt_block pp f.fd_body;
447  fprintf pp "@;<0 -2>}@]@ @ "
448
449let field pp f =
450  simple_decl pp ({name = f.fld_name; stamp = 0}, f.fld_typ);
451  match f.fld_bitfield with
452  | None -> ()
453  | Some n -> fprintf pp " : %d" n
454
455let globdecl pp g =
456  location pp g.gloc;
457  match g.gdesc with
458  | Gdecl d ->
459      fprintf pp "%a@ @ " full_decl d
460  | Gfundef f ->
461      fundef pp f
462  | Gcompositedecl(kind, id) ->
463      fprintf pp "%s %a;@ @ "
464        (match kind with Struct -> "struct" | Union -> "union")
465        ident id
466  | Gcompositedef(kind, id, flds) ->
467      fprintf pp "@[<v 2>%s %a {"
468        (match kind with Struct -> "struct" | Union -> "union")
469        ident id;
470      List.iter (fun fld -> fprintf pp "@ %a;" field fld) flds;
471      fprintf pp "@;<0 -2>};@]@ @ "
472  | Gtypedef(id, ty) ->
473      fprintf pp "@[<hov 2>typedef %a;@]@ @ " simple_decl (id, ty)
474  | Genumdef(id, fields) ->
475      fprintf pp "@[<v 2>enum %a {" ident id;
476      List.iter
477        (fun (name, opt_e) ->
478           fprintf pp "@ %a" ident name;
479           begin match opt_e with
480           | None -> ()
481           | Some e -> fprintf pp " = %a" exp (0, e)
482           end;
483           fprintf pp ",")
484         fields;
485       fprintf pp "@;<0 -2>};@]@ @ "
486  | Gpragma s ->
487       fprintf pp "#pragma %s@ @ " s
488
489let program pp prog =
490  fprintf pp "@[<v 0>";
491  List.iter (globdecl pp) prog;
492  fprintf pp "@]@."
Note: See TracBrowser for help on using the repository browser.