cparser/Cprint.ml

   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
  18 open Format
  19 open C
  20
  21 let print_idents_in_full = ref false
  22
  23 let print_line_numbers = ref false
  24
  25 let location pp (file, lineno) =
  26   if !print_line_numbers && lineno >= 0 then
  27     fprintf pp "# %d \"%s\"@ " lineno file
  28
  29 let 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
  34 let attribute pp = function
  35   | AConst -> fprintf pp "const"
  36   | AVolatile -> fprintf pp "volatile"
  37   | ARestrict -> fprintf pp "restrict"
  38
  39 let attributes pp = function
  40   | [] -> ()
  41   | al -> List.iter (fun a -> fprintf pp " %a" attribute a) al
  42
  43 let 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
  57 let name_of_fkind = function
  58   | FFloat -> "float"
  59   | FDouble -> "double"
  60   | FLongDouble -> "long double"
  61
  62 let 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
 114 let typ pp ty =
 115   dcl pp ty (fun _ -> ())
 116
 117 let 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
 168 type associativity = LtoR | RtoL | NA
 169
 170 let 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
 194 let 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
 317 let 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
 331 let simple_decl pp (id, ty) =
 332   dcl pp ty (fun pp -> fprintf pp " %a" ident id)
 333
 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 "
 339
 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);
 343   begin match int with
 344   | None -> ()
 345   | Some i -> fprintf pp " =@ %a" init i
 346   end;
 347   fprintf pp ";@]"
 348
 349 exception Not_expr
 350
 351 let 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
 363 let 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
 415 and 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
 423 and 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
 432 and 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
 439 let 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
 449 let 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
 455 let 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
 489 let program pp prog =
 490   fprintf pp "@[<v 0>";
 491   List.iter (globdecl pp) prog;
 492   fprintf pp "@]@."