source: driver/clightPrinter.ml @ 2834

Last change on this file since 2834 was 2792, checked in by campbell, 7 years ago

Make instrumented output a little easier to read.

File size: 22.2 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
43let 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
55let rec flist l =
56match l with
57| Fnil -> []
58| Fcons (id, ty, tl) -> (nameof id,ty)::(flist tl)
59
60type cost_style =
61| Cost_plain
62| Cost_numbered of Extracted.Label.clight_cost_map * Extracted.Joint.stack_cost_model
63| Cost_instrumented of Extracted.Label.clight_cost_map * Extracted.Joint.stack_cost_model
64
65(* Not ideal, but convenient for now *)
66let style = ref Cost_plain
67
68let namecost l =
69  "_cost" ^ string_of_int (int_of_matitapos l)
70
71let name_unop = function
72  | Onotbool -> "!"
73  | Onotint  -> "~"
74  | Oneg     -> "-"
75
76
77let 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
95let 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(*
105let 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
113module StructUnionSet = Set.Make(struct
114  type t = string * fieldlist
115  let compare (n1, _ : t) (n2, _ : t) = compare n1 n2
116end)
117
118let struct_unions = ref StructUnionSet.empty
119
120let register_struct_union id fld =
121  struct_unions := StructUnionSet.add (id, fld) !struct_unions
122
123(* Declarator (identifier + type) *)
124
125let name_optid id =
126  if id = "" then "" else " " ^ id
127
128let parenthesize_if_pointer id =
129  if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
130
131let 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
174let name_type ty = name_cdecl "" ty
175
176(* Expressions *)
177
178let 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
202let 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
260and 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
266let 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 :( *)
275let return_cost = ref None
276let print_return_cost p =
277  match !return_cost with
278  | None -> ()
279  | Some s -> fprintf p "@ __stack_size_incr(-%d);@ " s
280
281let 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
348and 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
364and 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
384let 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
403let 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_cost_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
429let 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
437let 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
449let eight = matitanat_of_int 8
450let zero8 = Extracted.BitVector.zero eight
451
452let 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
457let 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
472let 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
502let 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
512let 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
545let 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
556and collect_type_list = function
557  | Tnil -> ()
558  | Tcons (hd,tl) -> collect_type hd; collect_type_list tl
559
560and collect_fields = function
561  | Fnil -> ()
562  | Fcons (id, hd, tl) -> collect_type hd; collect_fields tl
563
564let 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
582let rec collect_expr_list = function
583  | Extracted.List.Nil -> ()
584  | Extracted.List.Cons (hd, tl) -> collect_expr hd; collect_expr_list tl
585
586let 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
607and collect_cases = function
608  | LSdefault s -> collect_stmt s
609  | LScase(_, lbl, s, rem) -> collect_stmt s; collect_cases rem
610
611let 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
617let 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
622let collect_globvar v =
623  collect_type (Extracted.Types.snd (Extracted.Types.snd v))
624
625let collect_program p =
626  mListIter collect_globvar p.prog_vars;
627  mListIter collect_fundef p.prog_funct
628
629let declare_struct_or_union p (name, fld) =
630  fprintf p "%s;@ @ " name
631
632let 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
642let 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
652let print_program cs prog =
653  style := cs;
654  (match cs with
655  | Cost_instrumented _ ->
656      fprintf str_formatter "int __cost = 0;@\n@\n";
657      fprintf str_formatter "void __cost_incr(int incr) {@\n";
658      fprintf str_formatter "  __cost = __cost + incr;@\n}@\n@\n";
659      fprintf str_formatter "int __stack_size = 0, __stack_size_max = 0;@\n@\n";
660      fprintf str_formatter "void __stack_size_incr(int incr) {@\n";
661      fprintf str_formatter "  __stack_size = __stack_size + incr;@\n";
662      fprintf str_formatter "  __stack_size_max = __stack_size_max < __stack_size ? __stack_size : __stack_size_max@\n}@\n@\n"
663  | _ -> ());
664  print_program_2 str_formatter prog;
665  flush_str_formatter ()
666
667let string_of_ctype = name_type
668
669let print_expression cs e = 
670  style := cs;
671  print_expr str_formatter e;
672  flush_str_formatter ()
673
674let print_statement cs s = 
675  style := cs;
676  print_stmt str_formatter s;
677  flush_str_formatter ()
678
679let print_ctype_prot = name_type
680
681let print_ctype_def = function
682  | Tstruct (name, fld) | Tunion (name, fld) ->
683    let f_fld s (id, t) = s ^ "  " ^ (print_ctype_prot t) ^ " " ^ id ^ ";\n" in
684    let s_fld = List.fold_left f_fld "" in
685    nameof name ^ " {\n" ^ (s_fld (flist fld)) ^ "};\n"
686  | _ -> "" (* no definition associated to the other types *)
687
688let string_of_unop = name_unop
689
690let string_of_binop = name_binop
Note: See TracBrowser for help on using the repository browser.