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 Extracted.AST
  20 open Extracted.Csyntax
  21 open Extracted.Glue
  22
  23 let freshNameCounter = ref 0
  24 let nameof id =
  25   try
  26     Hashtbl.find ClightFromC.symTable id
  27   with Not_found ->
  28     freshNameCounter := !freshNameCounter + 1;
  29     let name = "_cerco" ^ string_of_int (!freshNameCounter) in
  30     Hashtbl.add ClightFromC.symTable id name;
  31     name
  32
  33 let rec mListIter f l =
  34 match l with
  35 | Extracted.List.Nil -> ()
  36 | Extracted.List.Cons (h,t) -> f h; mListIter f t
  37
  38 let rec mlist l =
  39 match l with
  40 | Extracted.List.Nil -> []
  41 | Extracted.List.Cons (h,t) -> h::(mlist t)
  42
  43 let stack_cost_for scm id =
  44   let check ids =
  45     let id' = Extracted.Types.fst ids in
  46     match Extracted.Identifiers.eq_identifier Extracted.PreIdentifiers.SymbolTag id id' with
  47     | Extracted.Bool.True -> Extracted.Types.Some (Extracted.Types.snd ids)
  48     | _ -> Extracted.Types.None
  49   in
  50   match Extracted.List.find check scm with
  51   | Extracted.Types.None -> 0
  52   | Extracted.Types.Some n -> int_of_matitanat n
  53
  54
  55 let rec flist l =
  56 match l with
  57 | Fnil -> []
  58 | Fcons (id, ty, tl) -> (nameof id,ty)::(flist tl)
  59
  60 type cost_style =
  61 | Cost_plain
  62 | Cost_numbered of Extracted.Label.clight_cost_map * Extracted.CostLabel.costlabel * Extracted.Joint.stack_cost_model * Extracted.Nat.nat
  63 | Cost_instrumented of Extracted.Label.clight_cost_map * Extracted.CostLabel.costlabel * Extracted.Joint.stack_cost_model * Extracted.Nat.nat
  64
  65 (* Not ideal, but convenient for now *)
  66 let style = ref Cost_plain
  67
  68 let namecost l =
  69   "_cost" ^ string_of_int (int_of_matitapos l)
  70
  71 let name_unop = function
  72   | Onotbool -> "!"
  73   | Onotint  -> "~"
  74   | Oneg     -> "-"
  75
  76
  77 let name_binop = function
  78   | Oadd -> "+"
  79   | Osub -> "-"
  80   | Omul -> "*"
  81   | Odiv -> "/"
  82   | Omod -> "%"
  83   | Oand -> "&"
  84   | Oor  -> "|"
  85   | Oxor -> "^"
  86   | Oshl -> "<<"
  87   | Oshr -> ">>"
  88   | Oeq  -> "=="
  89   | One  -> "!="
  90   | Olt  -> "<"
  91   | Ogt  -> ">"
  92   | Ole  -> "<="
  93   | Oge  -> ">="
  94
  95 let name_inttype sz sg =
  96   match sz, sg with
  97   | I8, Signed -> "signed char"
  98   | I8, Unsigned -> "unsigned char"
  99   | I16, Signed -> "short"
 100   | I16, Unsigned -> "unsigned short"
 101   | I32, Signed -> "int"
 102   | I32, Unsigned -> "unsigned int"
 103
 104 (*
 105 let name_floattype sz =
 106   match sz with
 107   | F32 -> "float"
 108   | F64 -> "double"
 109 *)
 110
 111 (* Collecting the names and fields of structs and unions *)
 112
 113 module StructUnionSet = Set.Make(struct
 114   type t = string * fieldlist
 115   let compare (n1, _ : t) (n2, _ : t) = compare n1 n2
 116 end)
 117
 118 let struct_unions = ref StructUnionSet.empty
 119
 120 let register_struct_union id fld =
 121   struct_unions := StructUnionSet.add (id, fld) !struct_unions
 122
 123 (* Declarator (identifier + type) *)
 124
 125 let name_optid id =
 126   if id = "" then "" else " " ^ id
 127
 128 let parenthesize_if_pointer id =
 129   if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
 130
 131 let rec name_cdecl id ty =
 132   match ty with
 133   | Tvoid ->
 134       "void" ^ name_optid id
 135   | Tint(sz, sg) ->
 136       name_inttype sz sg ^ name_optid id
 137   (*| Tfloat sz ->
 138       name_floattype sz ^ name_optid id*)
 139   | Tpointer t ->
 140       name_cdecl ("*" ^ id) t
 141   | Tarray(t, n) ->
 142       name_cdecl
 143         (sprintf "%s[%ld]" (parenthesize_if_pointer id) (Int32.of_int (int_of_matitanat n)))
 144         t
 145   | Tfunction(args, res) ->
 146       let b = Buffer.create 20 in
 147       if id = ""
 148       then Buffer.add_string b "(*)"
 149       else Buffer.add_string b (parenthesize_if_pointer id);
 150       Buffer.add_char b '(';
 151       begin match args with
 152       | Tnil ->
 153           Buffer.add_string b "void"
 154       | _ ->
 155           let rec add_args first = function
 156           | Tnil -> ()
 157           | Tcons (t1, tl) ->
 158               if not first then Buffer.add_string b ", ";
 159               Buffer.add_string b (name_cdecl "" t1);
 160               add_args false tl in
 161           add_args true args
 162       end;
 163       Buffer.add_char b ')';
 164       name_cdecl (Buffer.contents b) res
 165   | Tstruct(name, fld) ->
 166       (nameof name) ^ name_optid id
 167   | Tunion(name, fld) ->
 168       (nameof name) ^ name_optid id
 169   | Tcomp_ptr name ->
 170       (nameof name) ^ " *" ^ id
 171
 172 (* Type *)
 173
 174 let name_type ty = name_cdecl "" ty
 175
 176 (* Expressions *)
 177
 178 let parenthesis_level (Expr (e, ty)) =
 179   match e with
 180   | Econst_int _ -> 0
 181   (*| Econst_float _ -> 0*)
 182   | Evar _ -> 0
 183   | Eunop(_, _) -> 30
 184   | Ederef _ -> 20
 185   | Eaddrof _ -> 30
 186   | Ebinop(op, _, _) ->
 187       begin match op with
 188       | Oand | Oor | Oxor -> 75
 189       | Oeq | One | Olt | Ogt | Ole | Oge -> 70
 190       | Oadd | Osub | Oshl | Oshr -> 60
 191       | Omul | Odiv | Omod -> 40
 192       end
 193   | Ecast _ -> 30
 194   | Econdition(_, _, _) -> 80
 195   | Eandbool(_, _) -> 80
 196   | Eorbool(_, _) -> 80
 197   | Esizeof _ -> 20
 198   | Efield _ -> 20
 199   | Ecost (_,_) -> 20
 200   (*| Ecall (_,_,_) -> 20*)
 201
 202 let rec print_expr p (Expr (eb, ty) as e) =
 203   let level = parenthesis_level e in
 204   match eb with
 205   | Econst_int (_,n) ->
 206       fprintf p "%ld" (Int32.of_int (int_of_bitvector n))
 207   (*| Econst_float f ->
 208       fprintf p "%F" f*)
 209   | Evar id ->
 210       fprintf p "%s" (nameof id)
 211   | Eunop(op, e1) ->
 212       fprintf p "%s%a" (name_unop op) print_expr_prec (level, e1)
 213   | Ederef (Expr (Ebinop(Oadd, e1, e2), _)) ->
 214       fprintf p "@[<hov 2>%a@,[%a]@]"
 215                 print_expr_prec (level, e1)
 216                 print_expr_prec (level, e2)
 217   | Ederef (Expr (Efield(e1, id), _)) ->
 218       fprintf p "%a->%s" print_expr_prec (level, e1) (nameof id)
 219   | Ederef e ->
 220       fprintf p "*%a" print_expr_prec (level, e)
 221   | Eaddrof e ->
 222       fprintf p "&%a" print_expr_prec (level, e)
 223   | Ebinop(op, e1, e2) ->
 224       fprintf p "@[<hov 0>%a@ %s %a@]"
 225                 print_expr_prec (level, e1)
 226                 (name_binop op)
 227                 print_expr_prec (level, e2)
 228   | Ecast(ty, e1) ->
 229       fprintf p "@[<hov 2>(%s)@,%a@]"
 230                 (name_type ty)
 231                 print_expr_prec (level, e1)
 232   | Econdition(e1, e2, e3) ->
 233       fprintf p "@[<hov 0>%a@ ? %a@ : %a@]"
 234                 print_expr_prec (level, e1)
 235                 print_expr_prec (level, e2)
 236                 print_expr_prec (level, e3)
 237   | Eandbool(e1, e2) ->
 238       fprintf p "@[<hov 0>%a@ && %a@]"
 239                 print_expr_prec (level, e1)
 240                 print_expr_prec (level, e2)
 241   | Eorbool(e1, e2) ->
 242       fprintf p "@[<hov 0>%a@ || %a@]"
 243                 print_expr_prec (level, e1)
 244                 print_expr_prec (level, e2)
 245   | Esizeof ty ->
 246       fprintf p "sizeof(%s)" (name_type ty)
 247   | Efield(e1, id) ->
 248       fprintf p "%a.%s" print_expr_prec (level, e1) (nameof id)
 249   | Ecost (lbl,e1) ->
 250       match !style with
 251       | Cost_plain ->
 252         fprintf p "(/* %s */ %a)" (namecost lbl) print_expr e1
 253       | Cost_numbered (cm,_,_,_) ->
 254         fprintf p "(/* %s = %d */ %a)" (namecost lbl) (int_of_matitanat (cm lbl)) print_expr e1
 255       | Cost_instrumented (cm,_,_,_) ->
 256         fprintf p "(__cost_incr(%d), %a)" (int_of_matitanat (cm lbl)) print_expr e1
 257   (*| Ecall (f, arg, e) ->
 258       fprintf p "(%s(%a), %a)" f print_expr arg print_expr e*)
 259
 260 and print_expr_prec p (context_prec, e) =
 261   let this_prec = parenthesis_level e in
 262   if this_prec >= context_prec
 263   then fprintf p "(%a)" print_expr e
 264   else print_expr p e
 265
 266 let rec print_expr_list p (first, el) =
 267   match el with
 268   | Extracted.List.Nil -> ()
 269   | Extracted.List.Cons (e1, et) ->
 270       if not first then fprintf p ",@ ";
 271       print_expr p e1;
 272       print_expr_list p (false, et)
 273
 274 (* Another quick hack :( *)
 275 let return_cost = ref None
 276 let print_return_cost p =
 277   match !return_cost with
 278   | None -> ()
 279   | Some s -> fprintf p "@ __stack_size_incr(-%d);@ " s
 280
 281 let rec print_stmt p s =
 282   match s with
 283   | Sskip ->
 284       fprintf p "/*skip*/;"
 285   | Sassign(e1, e2) ->
 286       fprintf p "@[<hv 2>%a =@ %a;@]" print_expr e1 print_expr e2
 287   | Scall(Extracted.Types.None, e1, el) ->
 288       fprintf p "@[<hv 2>%a@,(@[<hov 0>%a@]);@]"
 289                 print_expr e1
 290                 print_expr_list (true, el)
 291   | Scall(Extracted.Types.Some lhs, e1, el) ->
 292       fprintf p "@[<hv 2>%a =@ %a@,(@[<hov 0>%a@]);@]"
 293                 print_expr lhs
 294                 print_expr e1
 295                 print_expr_list (true, el)
 296   | Ssequence(s1, s2) ->
 297       fprintf p "%a@ %a" print_stmt s1 print_stmt s2
 298   | Sifthenelse(e, s1, Sskip) ->
 299       fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>}@]"
 300               print_expr e
 301               print_stmt s1
 302   | Sifthenelse(e, s1, s2) ->
 303       fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]"
 304               print_expr e
 305               print_stmt s1
 306               print_stmt s2
 307   | Swhile(e, s) ->
 308       fprintf p "@[<v 2>while (%a) {@ %a@;<0 -2>}@]"
 309               print_expr e
 310               print_stmt s
 311   | Sdowhile(e, s) ->
 312       fprintf p "@[<v 2>do {@ %a@;<0 -2>} while(%a);@]"
 313               print_stmt s
 314               print_expr e
 315   | Sfor(s_init, e, s_iter, s_body) ->
 316       fprintf p "@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]"
 317               print_stmt_for s_init
 318               print_expr e
 319               print_stmt_for s_iter
 320               print_stmt s_body
 321   | Sbreak ->
 322       fprintf p "break;"
 323   | Scontinue ->
 324       fprintf p "continue;"
 325   | Sswitch(e, cases) ->
 326       fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]"
 327               print_expr e
 328               print_cases cases
 329   | Sreturn Extracted.Types.None ->
 330       print_return_cost p;
 331       fprintf p "return;"
 332   | Sreturn (Extracted.Types.Some e) ->
 333       print_return_cost p;
 334       fprintf p "return %a;" print_expr e
 335   | Slabel(lbl, s1) ->
 336       fprintf p "%s:@ %a" (nameof lbl) print_stmt s1
 337   | Sgoto lbl ->
 338       fprintf p "goto %s;" (nameof lbl)
 339  | Scost (lbl,s1) ->
 340       match !style with
 341       | Cost_plain ->
 342         fprintf p "%s:@ %a" (namecost lbl) print_stmt s1
 343       | Cost_numbered (cm,_,_,_) ->
 344         fprintf p "/* %s = %d */@ %a" (namecost lbl) (int_of_matitanat (cm lbl)) print_stmt s1
 345       | Cost_instrumented (cm,_,_,_) ->
 346         fprintf p "__cost_incr(%d);@ %a" (int_of_matitanat (cm lbl)) print_stmt s1
 347
 348 and print_cases p cases =
 349   match cases with
 350   | LSdefault Sskip ->
 351       ()
 352   | LSdefault s ->
 353       fprintf p "@[<v 2>default:@ %a@]" print_stmt s
 354   | LScase(_, lbl, Sskip, rem) ->
 355       fprintf p "case %ld:@ %a"
 356         (Int32.of_int (int_of_bitvector lbl))
 357         print_cases rem
 358   | LScase(_, lbl, s, rem) ->
 359       fprintf p "@[<v 2>case %ld:@ %a@]@ %a"
 360               (Int32.of_int (int_of_bitvector lbl))
 361               print_stmt s
 362               print_cases rem
 363
 364 and print_stmt_for p s =
 365   match s with
 366   | Sskip ->
 367       fprintf p "/*nothing*/"
 368   | Sassign(e1, e2) ->
 369       fprintf p "%a = %a" print_expr e1 print_expr e2
 370   | Ssequence(s1, s2) ->
 371       fprintf p "%a, %a" print_stmt_for s1 print_stmt_for s2
 372   | Scall(Extracted.Types.None, e1, el) ->
 373       fprintf p "@[<hv 2>%a@,(@[<hov 0>%a@])@]"
 374                 print_expr e1
 375                 print_expr_list (true, el)
 376   | Scall(Extracted.Types.Some lhs, e1, el) ->
 377       fprintf p "@[<hv 2>%a =@ %a@,(@[<hov 0>%a@])@]"
 378                 print_expr lhs
 379                 print_expr e1
 380                 print_expr_list (true, el)
 381   | _ ->
 382       fprintf p "({ %a })" print_stmt s
 383
 384 let name_function_parameters fun_name params =
 385   let b = Buffer.create 20 in
 386   Buffer.add_string b fun_name;
 387   Buffer.add_char b '(';
 388   begin match params with
 389   | Extracted.List.Nil ->
 390       Buffer.add_string b "void"
 391   | _ ->
 392       let rec add_params first = function
 393       | Extracted.List.Nil -> ()
 394       | Extracted.List.Cons ({Extracted.Types.fst = id; Extracted.Types.snd = ty}, rem) ->
 395           if not first then Buffer.add_string b ", ";
 396           Buffer.add_string b (name_cdecl (nameof id) ty);
 397           add_params false rem in
 398       add_params true params
 399   end;
 400   Buffer.add_char b ')';
 401   Buffer.contents b
 402
 403 let print_function p id f =
 404   fprintf p "%s@ "
 405             (name_cdecl (name_function_parameters (nameof id) f.fn_params)
 406                         f.fn_return);
 407   fprintf p "@[<v 2>{@ ";
 408   mListIter
 409     (fun ({Extracted.Types.fst = id; Extracted.Types.snd = ty}) ->
 410       fprintf p "%s;@ " (name_cdecl (nameof id) ty))
 411     f.fn_vars;
 412   (match !style with
 413   | Cost_plain -> return_cost := None
 414   | Cost_numbered (_,_,scm,_) ->
 415     let cost = stack_cost_for scm id in
 416     fprintf p "/* stack cost %d */@ " cost;
 417     return_cost := None (* No need to tell us the stack size again *)
 418   | Cost_instrumented (_,_,scm,_) ->
 419     let cost = stack_cost_for scm id in
 420     fprintf p "__stack_size_incr(%d);@ " cost;
 421     return_cost := Some cost
 422   );
 423   print_stmt p f.fn_body;
 424   (* We don't always need this (e.g., when it ends with a return), but
 425      better safe than sorry... *)
 426   print_return_cost p;
 427   fprintf p "@;<0 -2>}@]@ @ "
 428
 429 let print_fundef p {Extracted.Types.fst = id; Extracted.Types.snd = fd} =
 430   match fd with
 431   | CL_External(_, args, res) ->
 432       fprintf p "extern %s;@ @ "
 433                 (name_cdecl (nameof id) (Tfunction(args, res)))
 434   | CL_Internal f ->
 435       print_function p id f
 436
 437 let string_of_init id =
 438   let b = Buffer.create (List.length id) in
 439   let add_init = function
 440   | Init_int8 n ->
 441       let n = int_of_bitvector n in
 442       if n >= 32 && n <= 126 && n <> Char.code '\"' && n <> Char.code '\\'
 443       then Buffer.add_char b (Char.chr n)
 444       else Buffer.add_string b (Printf.sprintf "\\%03o" n)
 445   | _ ->
 446       assert false
 447   in List.iter add_init id; Buffer.contents b
 448
 449 let eight = matitanat_of_int 8
 450 let zero8 = Extracted.BitVector.zero eight
 451
 452 let chop_last_nul id =
 453   match List.rev id with
 454   | Init_int8 n :: tl when Extracted.BitVector.eq_bv eight n zero8 = Extracted.Bool.True -> List.rev tl
 455   | _ -> id
 456
 457 let print_init p = function
 458   | Init_int8 n -> fprintf p "%ld,@ " (Int32.of_int (int_of_bitvector n))
 459   | Init_int16 n -> fprintf p "%ld,@ " (Int32.of_int (int_of_bitvector n))
 460   | Init_int32 n -> fprintf p "%ld,@ " (Int32.of_int (int_of_bitvector n))
 461   (*| Init_float32 n -> fprintf p "%F,@ " n
 462   | Init_float64 n -> fprintf p "%F,@ " n*)
 463   | Init_space n -> fprintf p "/* skip %ld, */@ " (Int32.of_int (int_of_matitanat n))
 464   | Init_null  -> fprintf p "0,@ "
 465   | Init_addrof(symb, ofs) ->
 466       let symb = nameof symb in
 467       let ofs = Int32.of_int (int_of_matitanat ofs) in
 468       if ofs = Int32.zero
 469       then fprintf p "&%s,@ " symb
 470       else fprintf p "(void *)((char *)&%s + %ld),@ " symb ofs
 471
 472 let print_init1 p = function
 473   | Init_int8 n -> fprintf p "%ld" (Int32.of_int (int_of_bitvector n))
 474   | Init_int16 n -> fprintf p "%ld" (Int32.of_int (int_of_bitvector n))
 475   | Init_int32 n -> fprintf p "%ld" (Int32.of_int (int_of_bitvector n))
 476   (*| Init_float32 n -> fprintf p "%F" n
 477   | Init_float64 n -> fprintf p "%F" n*)
 478   | Init_space n -> fprintf p "/* skip %ld */" (Int32.of_int (int_of_matitanat n))
 479   | Init_null  -> fprintf p "0"
 480   | Init_addrof(symb, ofs) ->
 481       let symb = nameof symb in
 482       let ofs = Int32.of_int (int_of_matitanat ofs) in
 483       if ofs = Int32.zero
 484       then fprintf p "&%s" symb
 485       else fprintf p "(void *)((char *)&%s + %ld)" symb ofs
 486
 487 (* XXX From Misc.LexingExt *)
 488   let lex_num s pos =
 489     let rec num i =
 490         if s.[i] >= '0' && s.[i] <= '9' then
 491           num (i + 1)
 492         else
 493           i
 494     in
 495     let pos' = num pos in
 496     if pos = pos' then
 497       None
 498     else
 499       Some (pos, pos', int_of_string (String.sub s pos (pos' - pos)))
 500
 501
 502 let match_string_literal s pos =
 503   let s_len = String.length s - 1 in
 504   let prefix = "__stringlit_" in
 505   let len_prefix = String.length prefix in
 506   s_len >= len_prefix
 507   && String.sub s 0 len_prefix = prefix  &&
 508       match lex_num s len_prefix with
 509         | None -> false
 510         | Some (pos, pos', v) -> pos' = String.length s - 1
 511
 512 let print_globvar p ({Extracted.Types.fst =
 513                        {Extracted.Types.fst = id; Extracted.Types.snd = region};
 514                       Extracted.Types.snd =
 515                        {Extracted.Types.fst = init; Extracted.Types.snd = ty};
 516                      }) =
 517   let id = nameof id in
 518   let init = mlist init in
 519   match init with
 520   | [] ->
 521       fprintf p "extern %s;@ @ "
 522               (name_cdecl id ty)
 523   | [Init_space _] ->
 524       fprintf p "%s;@ @ "
 525               (name_cdecl id ty)
 526   | [init] ->
 527       fprintf p "@[<hov 2>%s = %a;@]@ @ "
 528               (name_cdecl id ty) print_init1 init
 529   | _ ->
 530       fprintf p "@[<hov 2>%s = "
 531               (name_cdecl id ty);
 532       if match_string_literal id 0
 533       && List.for_all (function Init_int8 _ -> true | _ -> false) init
 534       then
 535         fprintf p "\"%s\"" (string_of_init (chop_last_nul init))
 536       else begin
 537         fprintf p "{@ ";
 538         List.iter (print_init p) init;
 539         fprintf p "}"
 540       end;
 541       fprintf p ";@]@ @ "
 542
 543 (* Collect struct and union types *)
 544
 545 let rec collect_type = function
 546   | Tvoid -> ()
 547   | Tint(sz, sg) -> ()
 548   (*| Tfloat sz -> ()*)
 549   | Tpointer t -> collect_type t
 550   | Tarray(t, n) -> collect_type t
 551   | Tfunction(args, res) -> collect_type_list args; collect_type res
 552   | Tstruct(id, fld) -> register_struct_union (nameof id) fld; collect_fields fld
 553   | Tunion(id, fld) -> register_struct_union (nameof id) fld; collect_fields fld
 554   | Tcomp_ptr _ -> ()
 555
 556 and collect_type_list = function
 557   | Tnil -> ()
 558   | Tcons (hd,tl) -> collect_type hd; collect_type_list tl
 559
 560 and collect_fields = function
 561   | Fnil -> ()
 562   | Fcons (id, hd, tl) -> collect_type hd; collect_fields tl
 563
 564 let rec collect_expr (Expr(ed, ty)) =
 565   match ed with
 566   | Econst_int _ -> ()
 567   (*| Econst_float f -> ()*)
 568   | Evar id -> ()
 569   | Eunop(op, e1) -> collect_expr e1
 570   | Ederef e -> collect_expr e
 571   | Eaddrof e -> collect_expr e
 572   | Ebinop(op, e1, e2) -> collect_expr e1; collect_expr e2
 573   | Ecast(ty, e1) -> collect_type ty; collect_expr e1
 574   | Econdition(e1, e2, e3) -> collect_expr e1; collect_expr e2; collect_expr e3
 575   | Eandbool(e1, e2) -> collect_expr e1; collect_expr e2
 576   | Eorbool(e1, e2) -> collect_expr e1; collect_expr e2
 577   | Esizeof ty -> collect_type ty
 578   | Efield(e1, id) -> collect_expr e1
 579   | Ecost(_, e) -> collect_expr e
 580   (*| Ecall(_, arg, e) -> collect_expr arg; collect_expr e*)
 581
 582 let rec collect_expr_list = function
 583   | Extracted.List.Nil -> ()
 584   | Extracted.List.Cons (hd, tl) -> collect_expr hd; collect_expr_list tl
 585
 586 let rec collect_stmt = function
 587   | Sskip -> ()
 588   | Sassign(e1, e2) -> collect_expr e1; collect_expr e2
 589   | Scall(Extracted.Types.None, e1, el) -> collect_expr e1; collect_expr_list el
 590   | Scall(Extracted.Types.Some lhs, e1, el) -> collect_expr lhs; collect_expr e1; collect_expr_list el
 591   | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
 592   | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
 593   | Swhile(e, s) -> collect_expr e; collect_stmt s
 594   | Sdowhile(e, s) -> collect_stmt s; collect_expr e
 595   | Sfor(s_init, e, s_iter, s_body) ->
 596       collect_stmt s_init; collect_expr e;
 597       collect_stmt s_iter; collect_stmt s_body
 598   | Sbreak -> ()
 599   | Scontinue -> ()
 600   | Sswitch(e, cases) -> collect_expr e; collect_cases cases
 601   | Sreturn Extracted.Types.None -> ()
 602   | Sreturn (Extracted.Types.Some e) -> collect_expr e
 603   | Slabel(lbl, s) -> collect_stmt s
 604   | Sgoto lbl -> ()
 605   | Scost (_,s1) -> collect_stmt s1
 606
 607 and collect_cases = function
 608   | LSdefault s -> collect_stmt s
 609   | LScase(_, lbl, s, rem) -> collect_stmt s; collect_cases rem
 610
 611 let collect_function f =
 612   collect_type f.fn_return;
 613   mListIter (fun ({Extracted.Types.fst = id; Extracted.Types.snd = ty}) -> collect_type ty) f.fn_params;
 614   mListIter (fun ({Extracted.Types.fst = id; Extracted.Types.snd = ty}) -> collect_type ty) f.fn_vars;
 615   collect_stmt f.fn_body
 616
 617 let collect_fundef ({Extracted.Types.fst = id; Extracted.Types.snd = fd}) =
 618   match fd with
 619   | CL_External(_, args, res) -> collect_type_list args; collect_type res
 620   | CL_Internal f -> collect_function f
 621
 622 let collect_globvar v =
 623   collect_type (Extracted.Types.snd (Extracted.Types.snd v))
 624
 625 let collect_program p =
 626   mListIter collect_globvar p.prog_vars;
 627   mListIter collect_fundef p.prog_funct
 628
 629 let declare_struct_or_union p (name, fld) =
 630   fprintf p "%s;@ @ " name
 631
 632 let print_struct_or_union p (name, fld) =
 633   fprintf p "@[<v 2>%s {" name;
 634   let rec print_fields = function
 635   | Fnil -> ()
 636   | Fcons (id, ty, rem) ->
 637       fprintf p "@ %s;" (name_cdecl (nameof id) ty);
 638       print_fields rem in
 639   print_fields fld;
 640   fprintf p "@;<0 -2>};@]@ "
 641
 642 let print_program_2 p prog =
 643   struct_unions := StructUnionSet.empty;
 644   collect_program prog;
 645   fprintf p "@[<v 0>";
 646   StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
 647   StructUnionSet.iter (print_struct_or_union p) !struct_unions;
 648   mListIter (print_globvar p) prog.prog_vars;
 649   mListIter (print_fundef p) prog.prog_funct;
 650   fprintf p "@]@."
 651
 652 let print_program cs prog =
 653   style := cs;
 654   (match cs with
 655   | Cost_instrumented (cm,initc,_,sinit) ->
 656      let cinit = int_of_matitanat (cm initc) in
 657      let sinit = int_of_float (2.0 ** 16.) - int_of_matitanat sinit in
 658       fprintf str_formatter "int __cost = %d;@\n@\n" cinit;
 659       fprintf str_formatter "int __stack_size = %d, __stack_size_max = %d;@\n@\n" sinit sinit;
 660       fprintf str_formatter "void __cost_incr(int incr) {@\n";
 661       fprintf str_formatter "  __cost = __cost + incr;@\n}@\n@\n";
 662       fprintf str_formatter "void __stack_size_incr(int incr) {@\n";
 663       fprintf str_formatter "  __stack_size = __stack_size + incr;@\n";
 664       fprintf str_formatter "  __stack_size_max = __stack_size_max < __stack_size ? __stack_size : __stack_size_max;@\n}@\n@\n"
 665   | _ -> ());
 666   print_program_2 str_formatter prog;
 667   flush_str_formatter ()
 668
 669 let string_of_ctype = name_type
 670
 671 let print_expression cs e =
 672   style := cs;
 673   print_expr str_formatter e;
 674   flush_str_formatter ()
 675
 676 let print_statement cs s =
 677   style := cs;
 678   print_stmt str_formatter s;
 679   flush_str_formatter ()
 680
 681 let print_ctype_prot = name_type
 682
 683 let print_ctype_def = function
 684   | Tstruct (name, fld) | Tunion (name, fld) ->
 685     let f_fld s (id, t) = s ^ "  " ^ (print_ctype_prot t) ^ " " ^ id ^ ";\n" in
 686     let s_fld = List.fold_left f_fld "" in
 687     nameof name ^ " {\n" ^ (s_fld (flist fld)) ^ "};\n"
 688   | _ -> "" (* no definition associated to the other types *)
 689
 690 let string_of_unop = name_unop
 691
 692 let string_of_binop = name_binop