1 (* *********************************************************************)
3 (* The Compcert verified compiler *)
5 (* Xavier Leroy, INRIA Paris-Rocquencourt *)
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. *)
14 (* *********************************************************************)
16 (** Pretty-printer for Csyntax *)
20 open Extracted.Csyntax
23 let freshNameCounter = ref 0
26 Hashtbl.find ClightFromC.symTable id
28 freshNameCounter := !freshNameCounter + 1;
29 let name = "_cerco" ^ string_of_int (!freshNameCounter) in
30 Hashtbl.add ClightFromC.symTable id name;
33 let rec mListIter f l =
35 | Extracted.List.Nil -> ()
36 | Extracted.List.Cons (h,t) -> f h; mListIter f t
40 | Extracted.List.Nil -> []
41 | Extracted.List.Cons (h,t) -> h::(mlist t)
43 let stack_cost_for scm id =
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
50 match Extracted.List.find check scm with
51 | Extracted.Types.None -> 0
52 | Extracted.Types.Some n -> int_of_matitanat n
58 | Fcons (id, ty, tl) -> (nameof id,ty)::(flist tl)
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
65 (* Not ideal, but convenient for now *)
66 let style = ref Cost_plain
69 "_cost" ^ string_of_int (int_of_matitapos l)
71 let name_unop = function
77 let name_binop = function
95 let name_inttype sz sg =
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"
105 let name_floattype sz =
111 (* Collecting the names and fields of structs and unions *)
113 module StructUnionSet = Set.Make(struct
114 type t = string * fieldlist
115 let compare (n1, _ : t) (n2, _ : t) = compare n1 n2
118 let struct_unions = ref StructUnionSet.empty
120 let register_struct_union id fld =
121 struct_unions := StructUnionSet.add (id, fld) !struct_unions
123 (* Declarator (identifier + type) *)
126 if id = "" then "" else " " ^ id
128 let parenthesize_if_pointer id =
129 if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
131 let rec name_cdecl id ty =
134 "void" ^ name_optid id
136 name_inttype sz sg ^ name_optid id
138 name_floattype sz ^ name_optid id*)
140 name_cdecl ("*" ^ id) t
143 (sprintf "%s[%ld]" (parenthesize_if_pointer id) (Int32.of_int (int_of_matitanat n)))
145 | Tfunction(args, res) ->
146 let b = Buffer.create 20 in
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
153 Buffer.add_string b "void"
155 let rec add_args first = function
158 if not first then Buffer.add_string b ", ";
159 Buffer.add_string b (name_cdecl "" t1);
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
170 (nameof name) ^ " *" ^ id
174 let name_type ty = name_cdecl "" ty
178 let parenthesis_level (Expr (e, ty)) =
181 (*| Econst_float _ -> 0*)
186 | Ebinop(op, _, _) ->
188 | Oand | Oor | Oxor -> 75
189 | Oeq | One | Olt | Ogt | Ole | Oge -> 70
190 | Oadd | Osub | Oshl | Oshr -> 60
191 | Omul | Odiv | Omod -> 40
194 | Econdition(_, _, _) -> 80
195 | Eandbool(_, _) -> 80
196 | Eorbool(_, _) -> 80
200 (*| Ecall (_,_,_) -> 20*)
202 let rec print_expr p (Expr (eb, ty) as e) =
203 let level = parenthesis_level e in
205 | Econst_int (_,n) ->
206 fprintf p "%ld" (Int32.of_int (int_of_bitvector n))
207 (*| Econst_float f ->
210 fprintf p "%s" (nameof id)
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)
220 fprintf p "*%a" print_expr_prec (level, 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)
227 print_expr_prec (level, e2)
229 fprintf p "@[<hov 2>(%s)@,%a@]"
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)
242 fprintf p "@[<hov 0>%a@ || %a@]"
243 print_expr_prec (level, e1)
244 print_expr_prec (level, e2)
246 fprintf p "sizeof(%s)" (name_type ty)
248 fprintf p "%a.%s" print_expr_prec (level, e1) (nameof id)
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*)
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
266 let rec print_expr_list p (first, el) =
268 | Extracted.List.Nil -> ()
269 | Extracted.List.Cons (e1, et) ->
270 if not first then fprintf p ",@ ";
272 print_expr_list p (false, et)
274 (* Another quick hack :( *)
275 let return_cost = ref None
276 let print_return_cost p =
277 match !return_cost with
279 | Some s -> fprintf p "@ __stack_size_incr(-%d);@ " s
281 let rec print_stmt p s =
284 fprintf p "/*skip*/;"
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@]);@]"
290 print_expr_list (true, el)
291 | Scall(Extracted.Types.Some lhs, e1, el) ->
292 fprintf p "@[<hv 2>%a =@ %a@,(@[<hov 0>%a@]);@]"
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>}@]"
302 | Sifthenelse(e, s1, s2) ->
303 fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]"
308 fprintf p "@[<v 2>while (%a) {@ %a@;<0 -2>}@]"
312 fprintf p "@[<v 2>do {@ %a@;<0 -2>} while(%a);@]"
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
319 print_stmt_for s_iter
324 fprintf p "continue;"
325 | Sswitch(e, cases) ->
326 fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]"
329 | Sreturn Extracted.Types.None ->
332 | Sreturn (Extracted.Types.Some e) ->
334 fprintf p "return %a;" print_expr e
336 fprintf p "%s:@ %a" (nameof lbl) print_stmt s1
338 fprintf p "goto %s;" (nameof lbl)
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
348 and print_cases p cases =
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))
358 | LScase(_, lbl, s, rem) ->
359 fprintf p "@[<v 2>case %ld:@ %a@]@ %a"
360 (Int32.of_int (int_of_bitvector lbl))
364 and print_stmt_for p s =
367 fprintf p "/*nothing*/"
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@])@]"
375 print_expr_list (true, el)
376 | Scall(Extracted.Types.Some lhs, e1, el) ->
377 fprintf p "@[<hv 2>%a =@ %a@,(@[<hov 0>%a@])@]"
380 print_expr_list (true, el)
382 fprintf p "({ %a })" print_stmt s
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"
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
400 Buffer.add_char b ')';
403 let print_function p id f =
405 (name_cdecl (name_function_parameters (nameof id) f.fn_params)
407 fprintf p "@[<v 2>{@ ";
409 (fun ({Extracted.Types.fst = id; Extracted.Types.snd = ty}) ->
410 fprintf p "%s;@ " (name_cdecl (nameof id) ty))
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
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... *)
427 fprintf p "@;<0 -2>}@]@ @ "
429 let print_fundef p {Extracted.Types.fst = id; Extracted.Types.snd = fd} =
431 | CL_External(_, args, res) ->
432 fprintf p "extern %s;@ @ "
433 (name_cdecl (nameof id) (Tfunction(args, res)))
435 print_function p id f
437 let string_of_init id =
438 let b = Buffer.create (List.length id) in
439 let add_init = function
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)
447 in List.iter add_init id; Buffer.contents b
449 let eight = matitanat_of_int 8
450 let zero8 = Extracted.BitVector.zero eight
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
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
469 then fprintf p "&%s,@ " symb
470 else fprintf p "(void *)((char *)&%s + %ld),@ " symb ofs
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
484 then fprintf p "&%s" symb
485 else fprintf p "(void *)((char *)&%s + %ld)" symb ofs
487 (* XXX From Misc.LexingExt *)
490 if s.[i] >= '0' && s.[i] <= '9' then
495 let pos' = num pos in
499 Some (pos, pos', int_of_string (String.sub s pos (pos' - pos)))
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
507 && String.sub s 0 len_prefix = prefix &&
508 match lex_num s len_prefix with
510 | Some (pos, pos', v) -> pos' = String.length s - 1
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};
517 let id = nameof id in
518 let init = mlist init in
521 fprintf p "extern %s;@ @ "
527 fprintf p "@[<hov 2>%s = %a;@]@ @ "
528 (name_cdecl id ty) print_init1 init
530 fprintf p "@[<hov 2>%s = "
532 if match_string_literal id 0
533 && List.for_all (function Init_int8 _ -> true | _ -> false) init
535 fprintf p "\"%s\"" (string_of_init (chop_last_nul init))
538 List.iter (print_init p) init;
543 (* Collect struct and union types *)
545 let rec collect_type = function
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
556 and collect_type_list = function
558 | Tcons (hd,tl) -> collect_type hd; collect_type_list tl
560 and collect_fields = function
562 | Fcons (id, hd, tl) -> collect_type hd; collect_fields tl
564 let rec collect_expr (Expr(ed, ty)) =
567 (*| Econst_float f -> ()*)
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*)
582 let rec collect_expr_list = function
583 | Extracted.List.Nil -> ()
584 | Extracted.List.Cons (hd, tl) -> collect_expr hd; collect_expr_list tl
586 let rec collect_stmt = function
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
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
605 | Scost (_,s1) -> collect_stmt s1
607 and collect_cases = function
608 | LSdefault s -> collect_stmt s
609 | LScase(_, lbl, s, rem) -> collect_stmt s; collect_cases rem
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
617 let collect_fundef ({Extracted.Types.fst = id; Extracted.Types.snd = fd}) =
619 | CL_External(_, args, res) -> collect_type_list args; collect_type res
620 | CL_Internal f -> collect_function f
622 let collect_globvar v =
623 collect_type (Extracted.Types.snd (Extracted.Types.snd v))
625 let collect_program p =
626 mListIter collect_globvar p.prog_vars;
627 mListIter collect_fundef p.prog_funct
629 let declare_struct_or_union p (name, fld) =
630 fprintf p "%s;@ @ " name
632 let print_struct_or_union p (name, fld) =
633 fprintf p "@[<v 2>%s {" name;
634 let rec print_fields = function
636 | Fcons (id, ty, rem) ->
637 fprintf p "@ %s;" (name_cdecl (nameof id) ty);
640 fprintf p "@;<0 -2>};@]@ "
642 let print_program_2 p prog =
643 struct_unions := StructUnionSet.empty;
644 collect_program prog;
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;
652 let print_program cs prog =
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"
666 print_program_2 str_formatter prog;
667 flush_str_formatter ()
669 let string_of_ctype = name_type
671 let print_expression cs e =
673 print_expr str_formatter e;
674 flush_str_formatter ()
676 let print_statement cs s =
678 print_stmt str_formatter s;
679 flush_str_formatter ()
681 let print_ctype_prot = name_type
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 *)
690 let string_of_unop = name_unop
692 let string_of_binop = name_binop