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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
|
(* *********************************************************************)
(* *)
(* 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-printer for LTLin code *)
open Format
open Camlcoq
open Datatypes
open Maps
open AST
open Integers
open Locations
open Machregsaux
open LTLin
open PrintOp
let name_of_chunk = function
| Mint8signed -> "int8signed"
| Mint8unsigned -> "int8unsigned"
| Mint16signed -> "int16signed"
| Mint16unsigned -> "int16unsigned"
| Mint32 -> "int32"
| Mfloat32 -> "float32"
| Mfloat64 -> "float64"
let name_of_type = function
| Tint -> "int"
| Tfloat -> "float"
let reg pp loc =
match loc with
| R r ->
begin match name_of_register r with
| Some s -> fprintf pp "%s" s
| None -> fprintf pp "<unknown reg>"
end
| S (Local(ofs, ty)) ->
fprintf pp "local(%s,%ld)" (name_of_type ty) (camlint_of_coqint ofs)
| S (Incoming(ofs, ty)) ->
fprintf pp "incoming(%s,%ld)" (name_of_type ty) (camlint_of_coqint ofs)
| S (Outgoing(ofs, ty)) ->
fprintf pp "outgoing(%s,%ld)" (name_of_type ty) (camlint_of_coqint ofs)
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_instruction pp i =
match i with
| Lop(op, args, res) ->
fprintf pp "%a = %a@ "
reg res (PrintOp.print_operation reg) (op, args)
| Lload(chunk, addr, args, dst) ->
fprintf pp "%a = %s[%a]@ "
reg dst (name_of_chunk chunk)
(PrintOp.print_addressing reg) (addr, args)
| Lstore(chunk, addr, args, src) ->
fprintf pp "%s[%a] = %a@ "
(name_of_chunk chunk)
(PrintOp.print_addressing reg) (addr, args)
reg src
| Lcall(sg, fn, args, res) ->
fprintf pp "%a = %a(%a)@ "
reg res ros fn regs args
| Ltailcall(sg, fn, args) ->
fprintf pp "tailcall %a(%a)@ "
ros fn regs args
| Lbuiltin(ef, args, res) ->
fprintf pp "%a = builtin \"%s\"(%a)@ "
reg res (extern_atom ef.ef_id) regs args
| Llabel lbl ->
fprintf pp "%ld:@ " (camlint_of_positive lbl)
| Lgoto lbl ->
fprintf pp "goto %ld@ " (camlint_of_positive lbl)
| Lcond(cond, args, lbl) ->
fprintf pp "if (%a) goto %ld@ "
(PrintOp.print_condition reg) (cond, args)
(camlint_of_positive lbl)
| Ljumptable(arg, tbl) ->
let tbl = Array.of_list tbl in
fprintf pp "@[<v 2>jumptable (%a)" reg arg;
for i = 0 to Array.length tbl - 1 do
fprintf pp "@ case %d: goto %ld" i (camlint_of_positive tbl.(i))
done;
fprintf pp "@]@ "
| Lreturn None ->
fprintf pp "return@ "
| Lreturn (Some arg) ->
fprintf pp "return %a@ " reg arg
let print_function pp f =
fprintf pp "@[<v 2>f(%a) {@ " regs f.fn_params;
List.iter (print_instruction pp) f.fn_code;
fprintf pp "@;<0 -2>}@]@."
let print_fundef pp fd =
match fd with
| Internal f -> print_function pp f
| External _ -> ()
let destination : string option ref = ref None
let currpp : formatter option ref = ref None
let print_if fd =
match !destination with
| None -> ()
| Some f ->
let pp =
match !currpp with
| Some pp -> pp
| None ->
let oc = open_out f in
let pp = formatter_of_out_channel oc in
currpp := Some pp;
pp
in print_fundef pp fd
|
