src/clight/clightPrinter.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 Csyntax *)
  17
  18 open Format
  19 open AST
  20 open Clight
  21
  22 let name_unop = function
  23   | Onotbool -> "!"
  24   | Onotint  -> "~"
  25   | Oneg     -> "-"
  26
  27
  28 let 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
  46 let 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
  55 let 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
  62 module StructUnionSet = Set.Make(struct
  63   type t = string * (ident*ctype) list
  64   let compare (n1, _ : t) (n2, _ : t) = compare n1 n2
  65 end)
  66
  67 let struct_unions = ref StructUnionSet.empty
  68
  69 let register_struct_union id fld =
  70   struct_unions := StructUnionSet.add (id, fld) !struct_unions
  71
  72 (* Declarator (identifier + type) *)
  73
  74 let name_optid id =
  75   if id = "" then "" else " " ^ id
  76
  77 let parenthesize_if_pointer id =
  78   if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
  79
  80 let 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
 123 let name_type ty = name_cdecl "" ty
 124
 125 (* Expressions *)
 126
 127 let 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
 151 let 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       fprintf p "(/* %s */ %a)" lbl print_expr e1
 200   | Ecall (f, arg, e) ->
 201       fprintf p "(%s(%a), %a)" f print_expr arg print_expr e
 202
 203 and print_expr_prec p (context_prec, e) =
 204   let this_prec = parenthesis_level e in
 205   if this_prec >= context_prec
 206   then fprintf p "(%a)" print_expr e
 207   else print_expr p e
 208
 209 let rec print_expr_list p (first, el) =
 210   match el with
 211   | [] -> ()
 212   | e1 :: et ->
 213       if not first then fprintf p ",@ ";
 214       print_expr p e1;
 215       print_expr_list p (false, et)
 216
 217 let rec print_stmt p s =
 218   match s with
 219   | Sskip ->
 220       fprintf p "/*skip*/;"
 221   | Sassign(e1, e2) ->
 222       fprintf p "@[<hv 2>%a =@ %a;@]" print_expr e1 print_expr e2
 223   | Scall(None, e1, el) ->
 224       fprintf p "@[<hv 2>%a@,(@[<hov 0>%a@]);@]"
 225                 print_expr e1
 226                 print_expr_list (true, el)
 227   | Scall(Some lhs, e1, el) ->
 228       fprintf p "@[<hv 2>%a =@ %a@,(@[<hov 0>%a@]);@]"
 229                 print_expr lhs
 230                 print_expr e1
 231                 print_expr_list (true, el)
 232   | Ssequence(s1, s2) ->
 233       fprintf p "%a@ %a" print_stmt s1 print_stmt s2
 234   | Sifthenelse(e, s1, Sskip) ->
 235       fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>}@]"
 236               print_expr e
 237               print_stmt s1
 238   | Sifthenelse(e, s1, s2) ->
 239       fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]"
 240               print_expr e
 241               print_stmt s1
 242               print_stmt s2
 243   | Swhile(e, s) ->
 244       fprintf p "@[<v 2>while (%a) {@ %a@;<0 -2>}@]"
 245               print_expr e
 246               print_stmt s
 247   | Sdowhile(e, s) ->
 248       fprintf p "@[<v 2>do {@ %a@;<0 -2>} while(%a);@]"
 249               print_stmt s
 250               print_expr e
 251   | Sfor(s_init, e, s_iter, s_body) ->
 252       fprintf p "@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]"
 253               print_stmt_for s_init
 254               print_expr e
 255               print_stmt_for s_iter
 256               print_stmt s_body
 257   | Sbreak ->
 258       fprintf p "break;"
 259   | Scontinue ->
 260       fprintf p "continue;"
 261   | Sswitch(e, cases) ->
 262       fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]"
 263               print_expr e
 264               print_cases cases
 265   | Sreturn None ->
 266       fprintf p "return;"
 267   | Sreturn (Some e) ->
 268       fprintf p "return %a;" print_expr e
 269   | Slabel(lbl, s1) ->
 270       fprintf p "%s:@ %a" lbl print_stmt s1
 271   | Sgoto lbl ->
 272       fprintf p "goto %s;" lbl
 273  | Scost (lbl,s1) ->
 274      fprintf p "%s:@ %a" lbl print_stmt s1
 275
 276 and print_cases p cases =
 277   match cases with
 278   | LSdefault Sskip ->
 279       ()
 280   | LSdefault s ->
 281       fprintf p "@[<v 2>default:@ %a@]" print_stmt s
 282   | LScase(lbl, Sskip, rem) ->
 283       fprintf p "case %ld:@ %a"
 284         (Int32.of_int lbl)
 285         print_cases rem
 286   | LScase(lbl, s, rem) ->
 287       fprintf p "@[<v 2>case %ld:@ %a@]@ %a"
 288               (Int32.of_int lbl)
 289               print_stmt s
 290               print_cases rem
 291
 292 and print_stmt_for p s =
 293   match s with
 294   | Sskip ->
 295       fprintf p "/*nothing*/"
 296   | Sassign(e1, e2) ->
 297       fprintf p "%a = %a" print_expr e1 print_expr e2
 298   | Ssequence(s1, s2) ->
 299       fprintf p "%a, %a" print_stmt_for s1 print_stmt_for s2
 300   | Scall(None, e1, el) ->
 301       fprintf p "@[<hv 2>%a@,(@[<hov 0>%a@])@]"
 302                 print_expr e1
 303                 print_expr_list (true, el)
 304   | Scall(Some lhs, e1, el) ->
 305       fprintf p "@[<hv 2>%a =@ %a@,(@[<hov 0>%a@])@]"
 306                 print_expr lhs
 307                 print_expr e1
 308                 print_expr_list (true, el)
 309   | _ ->
 310       fprintf p "({ %a })" print_stmt s
 311
 312 let name_function_parameters fun_name params =
 313   let b = Buffer.create 20 in
 314   Buffer.add_string b fun_name;
 315   Buffer.add_char b '(';
 316   begin match params with
 317   | [] ->
 318       Buffer.add_string b "void"
 319   | _ ->
 320       let rec add_params first = function
 321       | [] -> ()
 322       | (id, ty) :: rem ->
 323           if not first then Buffer.add_string b ", ";
 324           Buffer.add_string b (name_cdecl id ty);
 325           add_params false rem in
 326       add_params true params
 327   end;
 328   Buffer.add_char b ')';
 329   Buffer.contents b
 330
 331 let print_function p id f =
 332   fprintf p "%s@ "
 333             (name_cdecl (name_function_parameters id f.fn_params)
 334                         f.fn_return);
 335   fprintf p "@[<v 2>{@ ";
 336   List.iter
 337     (fun ((id, ty)) ->
 338       fprintf p "%s;@ " (name_cdecl id ty))
 339     f.fn_vars;
 340   print_stmt p f.fn_body;
 341   fprintf p "@;<0 -2>}@]@ @ "
 342
 343 let print_fundef p (id, fd) =
 344   match fd with
 345   | External(_, args, res) ->
 346       fprintf p "extern %s;@ @ "
 347                 (name_cdecl id (Tfunction(args, res)))
 348   | Internal f ->
 349       print_function p id f
 350
 351 let string_of_init id =
 352   let b = Buffer.create (List.length id) in
 353   let add_init = function
 354   | Init_int8 n ->
 355       if n >= 32 && n <= 126 && n <> Char.code '\"' && n <> Char.code '\\'
 356       then Buffer.add_char b (Char.chr n)
 357       else Buffer.add_string b (Printf.sprintf "\\%03o" n)
 358   | _ ->
 359       assert false
 360   in List.iter add_init id; Buffer.contents b
 361
 362 let chop_last_nul id =
 363   match List.rev id with
 364   | Init_int8 0 :: tl -> List.rev tl
 365   | _ -> id
 366
 367 let print_init p = function
 368   | Init_int8 n -> fprintf p "%ld,@ " (Int32.of_int n)
 369   | Init_int16 n -> fprintf p "%ld,@ " (Int32.of_int n)
 370   | Init_int32 n -> fprintf p "%ld,@ " (Int32.of_int n)
 371   | Init_float32 n -> fprintf p "%F,@ " n
 372   | Init_float64 n -> fprintf p "%F,@ " n
 373   | Init_space n -> fprintf p "/* skip %ld, */@ " (Int32.of_int n)
 374   | Init_addrof(symb, ofs) ->
 375       let ofs = Int32.of_int ofs in
 376       if ofs = Int32.zero
 377       then fprintf p "&%s,@ " symb
 378       else fprintf p "(void *)((char *)&%s + %ld),@ " symb ofs
 379
 380 let print_init1 p = function
 381   | Init_int8 n -> fprintf p "%ld" (Int32.of_int n)
 382   | Init_int16 n -> fprintf p "%ld" (Int32.of_int n)
 383   | Init_int32 n -> fprintf p "%ld" (Int32.of_int n)
 384   | Init_float32 n -> fprintf p "%F" n
 385   | Init_float64 n -> fprintf p "%F" n
 386   | Init_space n -> fprintf p "/* skip %ld */" (Int32.of_int n)
 387   | Init_addrof(symb, ofs) ->
 388       let ofs = Int32.of_int ofs in
 389       if ofs = Int32.zero
 390       then fprintf p "&%s" symb
 391       else fprintf p "(void *)((char *)&%s + %ld)" symb ofs
 392
 393 let match_string_literal s pos =
 394   let s_len = String.length s - 1 in
 395   let prefix = "__stringlit_" in
 396   let len_prefix = String.length prefix in
 397   s_len >= len_prefix
 398   && String.sub s 0 len_prefix = prefix  &&
 399       match Misc.LexingExt.lex_num s len_prefix with
 400         | None -> false
 401         | Some (pos, pos', v) -> pos' = String.length s - 1
 402
 403 let print_globvar p (((id, init), ty)) =
 404   match init with
 405   | [] ->
 406       fprintf p "extern %s;@ @ "
 407               (name_cdecl id ty)
 408   | [Init_space _] ->
 409       fprintf p "%s;@ @ "
 410               (name_cdecl id ty)
 411   | [init] ->
 412       fprintf p "@[<hov 2>%s = %a;@]@ @ "
 413               (name_cdecl id ty) print_init1 init
 414   | _ ->
 415       fprintf p "@[<hov 2>%s = "
 416               (name_cdecl id ty);
 417       if match_string_literal id 0
 418       && List.for_all (function Init_int8 _ -> true | _ -> false) init
 419       then
 420         fprintf p "\"%s\"" (string_of_init (chop_last_nul init))
 421       else begin
 422         fprintf p "{@ ";
 423         List.iter (print_init p) init;
 424         fprintf p "}"
 425       end;
 426       fprintf p ";@]@ @ "
 427
 428 (* Collect struct and union types *)
 429
 430 let rec collect_type = function
 431   | Tvoid -> ()
 432   | Tint(sz, sg) -> ()
 433   | Tfloat sz -> ()
 434   | Tpointer t -> collect_type t
 435   | Tarray(t, n) -> collect_type t
 436   | Tfunction(args, res) -> collect_type_list args; collect_type res
 437   | Tstruct(id, fld) -> register_struct_union id fld; collect_fields fld
 438   | Tunion(id, fld) -> register_struct_union id fld; collect_fields fld
 439   | Tcomp_ptr _ -> ()
 440
 441 and collect_type_list = function
 442   | [] -> ()
 443   | hd::tl -> collect_type hd; collect_type_list tl
 444
 445 and collect_fields = function
 446   | [] -> ()
 447   | (id, hd)::tl -> collect_type hd; collect_fields tl
 448
 449 let rec collect_expr (Expr(ed, ty)) =
 450   match ed with
 451   | Econst_int n -> ()
 452   | Econst_float f -> ()
 453   | Evar id -> ()
 454   | Eunop(op, e1) -> collect_expr e1
 455   | Ederef e -> collect_expr e
 456   | Eaddrof e -> collect_expr e
 457   | Ebinop(op, e1, e2) -> collect_expr e1; collect_expr e2
 458   | Ecast(ty, e1) -> collect_type ty; collect_expr e1
 459   | Econdition(e1, e2, e3) -> collect_expr e1; collect_expr e2; collect_expr e3
 460   | Eandbool(e1, e2) -> collect_expr e1; collect_expr e2
 461   | Eorbool(e1, e2) -> collect_expr e1; collect_expr e2
 462   | Esizeof ty -> collect_type ty
 463   | Efield(e1, id) -> collect_expr e1
 464   | Ecost(_, e) -> collect_expr e
 465   | Ecall(_, arg, e) -> collect_expr arg; collect_expr e
 466
 467 let rec collect_expr_list = function
 468   | [] -> ()
 469   | hd :: tl -> collect_expr hd; collect_expr_list tl
 470
 471 let rec collect_stmt = function
 472   | Sskip -> ()
 473   | Sassign(e1, e2) -> collect_expr e1; collect_expr e2
 474   | Scall(None, e1, el) -> collect_expr e1; collect_expr_list el
 475   | Scall(Some lhs, e1, el) -> collect_expr lhs; collect_expr e1; collect_expr_list el
 476   | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
 477   | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
 478   | Swhile(e, s) -> collect_expr e; collect_stmt s
 479   | Sdowhile(e, s) -> collect_stmt s; collect_expr e
 480   | Sfor(s_init, e, s_iter, s_body) ->
 481       collect_stmt s_init; collect_expr e;
 482       collect_stmt s_iter; collect_stmt s_body
 483   | Sbreak -> ()
 484   | Scontinue -> ()
 485   | Sswitch(e, cases) -> collect_expr e; collect_cases cases
 486   | Sreturn None -> ()
 487   | Sreturn (Some e) -> collect_expr e
 488   | Slabel(lbl, s) -> collect_stmt s
 489   | Sgoto lbl -> ()
 490   | Scost (_,s1) -> collect_stmt s1
 491
 492 and collect_cases = function
 493   | LSdefault s -> collect_stmt s
 494   | LScase(lbl, s, rem) -> collect_stmt s; collect_cases rem
 495
 496 let collect_function f =
 497   collect_type f.fn_return;
 498   List.iter (fun ((id, ty)) -> collect_type ty) f.fn_params;
 499   List.iter (fun ((id, ty)) -> collect_type ty) f.fn_vars;
 500   collect_stmt f.fn_body
 501
 502 let collect_fundef ((id, fd)) =
 503   match fd with
 504   | External(_, args, res) -> collect_type_list args; collect_type res
 505   | Internal f -> collect_function f
 506
 507 let collect_globvar (((id, init), ty)) =
 508   collect_type ty
 509
 510 let collect_program p =
 511   List.iter collect_globvar p.prog_vars;
 512   List.iter collect_fundef p.prog_funct
 513
 514 let declare_struct_or_union p (name, fld) =
 515   fprintf p "%s;@ @ " name
 516
 517 let print_struct_or_union p (name, fld) =
 518   fprintf p "@[<v 2>%s {" name;
 519   let rec print_fields = function
 520   | [] -> ()
 521   | (id, ty)::rem ->
 522       fprintf p "@ %s;" (name_cdecl id ty);
 523       print_fields rem in
 524   print_fields fld;
 525   fprintf p "@;<0 -2>};@]@ "
 526
 527 let print_program_2 p prog =
 528   struct_unions := StructUnionSet.empty;
 529   collect_program prog;
 530   fprintf p "@[<v 0>";
 531   StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
 532   StructUnionSet.iter (print_struct_or_union p) !struct_unions;
 533   List.iter (print_globvar p) prog.prog_vars;
 534   List.iter (print_fundef p) prog.prog_funct;
 535   fprintf p "@]@."
 536
 537 let print_program prog =
 538   print_program_2 str_formatter prog;
 539   flush_str_formatter ()
 540
 541 let string_of_ctype = name_type
 542
 543 let print_expression e =
 544   print_expr str_formatter e;
 545   flush_str_formatter ()
 546
 547 let print_statement s =
 548   print_stmt str_formatter s;
 549   flush_str_formatter ()
 550
 551 let print_ctype_prot = name_type
 552
 553 let print_ctype_def = function
 554   | Tstruct (name, fld) | Tunion (name, fld) ->
 555     let f_fld s (id, t) = s ^ "  " ^ (print_ctype_prot t) ^ " " ^ id ^ ";\n" in
 556     let s_fld = List.fold_left f_fld "" in
 557     name ^ " {\n" ^ (s_fld fld) ^ "};\n"
 558   | _ -> "" (* no definition associated to the other types *)
 559
 560 let string_of_unop = name_unop
 561
 562 let string_of_binop = name_binop