1 (* *********************************************************************)
3 (* The Compcert verified compiler *)
5 (* Xavier Leroy, INRIA Paris-Rocquencourt *)
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. *)
14 (* *********************************************************************)
16 (* Pretty-printer for C abstract syntax *)
21 let print_idents_in_full = ref false
23 let print_line_numbers = ref false
25 let location pp (file, lineno) =
26 if !print_line_numbers && lineno >= 0 then
27 fprintf pp "# %d \"%s\"@ " lineno file
30 if !print_idents_in_full
31 then fprintf pp "%s$%d" i.name i.stamp
32 else fprintf pp "%s" i.name
34 let attribute pp = function
35 | AConst -> fprintf pp "const"
36 | AVolatile -> fprintf pp "volatile"
37 | ARestrict -> fprintf pp "restrict"
39 let attributes pp = function
41 | al -> List.iter (fun a -> fprintf pp " %a" attribute a) al
43 let name_of_ikind = function
46 | ISChar -> "signed char"
47 | IUChar -> "unsigned char"
49 | IUInt -> "unsigned int"
51 | IUShort -> "unsigned short"
53 | IULong -> "unsigned long"
54 | ILongLong -> "long long"
55 | IULongLong -> "unsigned long long"
57 let name_of_fkind = function
60 | FLongDouble -> "long double"
65 fprintf pp "void%a%t" attributes a n
67 fprintf pp "%s%a%t" (name_of_ikind k) attributes a n
69 fprintf pp "%s%a%t" (name_of_fkind k) attributes a n
73 | TFun _ | TArray _ -> fprintf pp " (*%a%t)" attributes a n
74 | _ -> fprintf pp " *%a%t" attributes a n in
80 | _ -> fprintf pp " (%a%t)" attributes a n
83 | None -> fprintf pp "[]"
84 | Some i -> fprintf pp "[%Ld]" i
87 | TFun(tres, args, vararg, a) ->
90 (fun pp -> fprintf pp " %a" ident id) in
94 | _ -> fprintf pp " (%a%t)" attributes a n
96 fprintf pp "(@[<hov 0>";
99 | Some [] -> if vararg then fprintf pp "..." else fprintf pp "void"
102 List.iter (fun a -> fprintf pp ",@ "; param a) al;
103 if vararg then fprintf pp ",@ ..."
108 fprintf pp "%a%a%t" ident id attributes a n
110 fprintf pp "struct %a%a%t" ident id attributes a n
112 fprintf pp "union %a%a%t" ident id attributes a n
115 dcl pp ty (fun _ -> ())
117 let const pp = function
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"
131 | CFloat(v, fk, s) ->
135 fprintf pp "%.18g" v;
137 | FFloat -> fprintf pp "F"
138 | FLongDouble -> fprintf pp "L"
143 for i = 0 to String.length s - 1 do
145 | '\009' -> fprintf pp "\\t"
146 | '\010' -> fprintf pp "\\n"
147 | '\013' -> fprintf pp "\\r"
148 | '\"' -> fprintf pp "\\\""
149 | '\\' -> fprintf pp "\\\\"
151 if c >= ' ' && c <= '~'
152 then fprintf pp "%c" c
153 else fprintf pp "\\%03o" (Char.code 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)
168 type associativity = LtoR | RtoL | NA
170 let precedence = function (* H&S section 7.2 *)
171 | EConst _ -> (16, NA)
172 | ESizeof _ -> (15, RtoL)
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)
194 let rec exp pp (prec, a) =
195 let (prec', assoc) = precedence a.edesc in
198 then (prec', prec' + 1)
199 else (prec' + 1, prec') in
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)
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)
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)@]"
306 fprintf pp "%a@[<hov 1>(" exp (prec', a1);
310 fprintf pp "%a" exp (2, a1);
311 List.iter (fun a -> fprintf pp ",@ %a" exp (2, a)) al
315 if prec' < prec then fprintf pp ")@]" else fprintf pp "@]"
317 let rec init pp = function
321 fprintf pp "@[<hov 1>{";
322 List.iter (fun i -> fprintf pp "%a,@ " init i) il;
324 | Init_struct(id, il) ->
325 fprintf pp "@[<hov 1>{";
326 List.iter (fun (fld, i) -> fprintf pp "%a,@ " init i) il;
328 | Init_union(id, fld, i) ->
329 fprintf pp "@[<hov 1>{%a}@]" init i
331 let simple_decl pp (id, ty) =
332 dcl pp ty (fun pp -> fprintf pp " %a" ident id)
334 let storage pp = function
335 | Storage_default -> ()
336 | Storage_extern -> fprintf pp "extern "
337 | Storage_static -> fprintf pp "static "
338 | Storage_register -> fprintf pp "register "
340 let 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);
345 | Some i -> fprintf pp " =@ %a" init i
351 let rec exp_of_stmt s =
355 {edesc = EBinop(Ocomma, exp_of_stmt s1, exp_of_stmt s2, TVoid []);
358 {edesc = EConditional(e, exp_of_stmt s1, exp_of_stmt s2);
367 fprintf pp "/*skip*/;"
369 fprintf pp "%a;" exp (0, e)
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
380 fprintf pp "@[<v 2>if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]"
381 exp (0, e) stmt_block s1 stmt_block s2
383 fprintf pp "@[<v 2>while (%a) {@ %a@;<0 -2>}@]"
384 exp (0, e) stmt_block s1
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>}@]"
397 fprintf pp "continue;"
399 fprintf pp "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]"
402 | Slabeled(lbl, s1) ->
403 fprintf pp "%a:@ %a" slabel lbl stmt s1
405 fprintf pp "goto %s;" lbl
408 | Sreturn (Some e) ->
409 fprintf pp "return %a;" exp (0, e)
411 fprintf pp "@[<v 2>{@ %a@;<0 -2>}@]" stmt_block s
415 and slabel pp = function
419 fprintf pp "case %a" exp (0, e)
423 and stmt_block pp s =
426 | Sblock (s1 :: sl) ->
428 List.iter (fun s -> fprintf pp "@ %a" stmt s) sl
433 if s.sdesc = Sskip then fprintf pp "/*nothing*/" else
435 exp pp (0, exp_of_stmt s)
437 fprintf pp "@[<v 3>({ %a })@]" stmt s
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>}@]@ @ "
450 simple_decl pp ({name = f.fld_name; stamp = 0}, f.fld_typ);
451 match f.fld_bitfield with
453 | Some n -> fprintf pp " : %d" n
459 fprintf pp "%a@ @ " full_decl d
462 | Gcompositedecl(kind, id) ->
463 fprintf pp "%s %a;@ @ "
464 (match kind with Struct -> "struct" | Union -> "union")
466 | Gcompositedef(kind, id, flds) ->
467 fprintf pp "@[<v 2>%s %a {"
468 (match kind with Struct -> "struct" | Union -> "union")
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;
477 (fun (name, opt_e) ->
478 fprintf pp "@ %a" ident name;
479 begin match opt_e with
481 | Some e -> fprintf pp " = %a" exp (0, e)
485 fprintf pp "@;<0 -2>};@]@ @ "
487 fprintf pp "#pragma %s@ @ " s
489 let program pp prog =
490 fprintf pp "@[<v 0>";
491 List.iter (globdecl pp) prog;