source: driver/clightPrinter.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
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  | One  -> "!="
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 | One | 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.