source: driver/clightPrinter.ml @ 2759

Last change on this file since 2759 was 2759, checked in by campbell, 8 years ago

Print out costs, with choice of style.
Note small anti-assertion patch to extracted ASMCosts.
No stack space yet.

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