blob: ab93fa52dd6f15e5b1f08f53199cf3b35283e2b9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** Pretty-printers for RTL code *)
open Printf
open Camlcoq
open Datatypes
open Maps
open AST
open RTLBlockInstr
open RTLPar
open PrintAST
open PrintRTLBlockInstr
(* Printing of RTL code *)
let reg pp r =
fprintf pp "x%d" (P.to_int r)
let rec regs pp = function
| [] -> ()
| [r] -> reg pp r
| r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
let ros pp = function
| Coq_inl r -> reg pp r
| Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
let print_bblock pp (pc, i) =
fprintf pp "%5d:{\n" pc;
List.iter (fun x -> fprintf pp "{\n";
List.iter (fun x -> fprintf pp "( "; List.iter (print_bblock_body pp) x; fprintf pp " )") x;
fprintf pp "}\n") i.bb_body;
print_bblock_exit pp i.bb_exit;
fprintf pp "\t}\n\n"
let print_function pp id f =
fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params;
let instrs =
List.sort
(fun (pc1, _) (pc2, _) -> compare pc2 pc1)
(List.rev_map
(fun (pc, i) -> (P.to_int pc, i))
(PTree.elements f.fn_code)) in
List.iter (print_bblock pp) instrs;
fprintf pp "}\n\n"
let print_globdef pp (id, gd) =
match gd with
| Gfun(Internal f) -> print_function pp id f
| _ -> ()
let print_program pp (prog: program) =
List.iter (print_globdef pp) prog.prog_defs
let destination : string option ref = ref None
let print_if passno prog =
match !destination with
| None -> ()
| Some f ->
let oc = open_out (f ^ "." ^ Z.to_string passno) in
print_program oc prog;
close_out oc
|
