-
Notifications
You must be signed in to change notification settings - Fork 5
/
ott.ml
154 lines (147 loc) · 5.89 KB
/
ott.ml
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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
open Instr
let no_line_number buf pc = ()
let line_number buf pc = Printf.bprintf buf "% 6d |" pc
let pr = Printf.bprintf
let rec dump_comma_separated how buf what =
match what with
| [] -> ()
| [e] -> how buf e
| e::t -> pr buf "%a, %a" how e (dump_comma_separated how) t
let disassemble_instrs buf (instrs : instructions) =
let rec dump_instr buf pc line needs_label =
if pc >= Array.length instrs then ()
else begin
let dump_next_instr () = dump_instr buf (pc+1) (line+1) true in
let simple buf = function
| Var v -> pr buf "%s" v
| Constant c -> pr buf "%s" (IO.string_of_literal c)
in
let dump_expr buf exp =
match exp with
| Simple e -> simple buf e
| Unop (Neg, a) -> pr buf "(-%a)" simple a
| Unop (Not, a) -> pr buf "(!%a)" simple a
| Binop (Plus, a, b) -> pr buf "(%a + %a)" simple a simple b
| Binop (Sub, a, b) -> pr buf "(%a - %a)" simple a simple b
| Binop (Mult, a, b) -> pr buf "(%a * %a)" simple a simple b
| Binop (Div, a, b) -> pr buf "(%a / %a)" simple a simple b
| Binop (Mod, a, b) -> pr buf "(%a %% %a)" simple a simple b
| Binop (Eq, a, b) -> pr buf "(%a == %a)" simple a simple b
| Binop (Neq, a, b) -> pr buf "(%a != %a)" simple a simple b
| Binop (Lt, a, b) -> pr buf "(%a < %a)" simple a simple b
| Binop (Lte, a, b) -> pr buf "(%a <= %a)" simple a simple b
| Binop (Gt, a, b) -> pr buf "(%a > %a)" simple a simple b
| Binop (Gte, a, b) -> pr buf "(%a >= %a)" simple a simple b
| Binop (And, a, b) -> pr buf "(%a && %a)" simple a simple b
| Binop (Or, a, b) -> pr buf "(%a || %a)" simple a simple b
| Array_index (a, i) -> pr buf "%s[%a]" a simple i
| Array_length e -> pr buf "length(%a)" simple e
in
let dump_arg buf arg = dump_expr buf arg in
let print_default_label () = pr buf "%d : " line in
let print_label label =
let label = if String.length label = 1 then "l"^label else label in
pr buf "%s : " label in
begin match[@warning "-4"] instrs.(pc) with
| Label _ | Call _ | Assume _ | Comment _ ->
()
| _ ->
if needs_label then print_default_label ()
end;
begin match instrs.(pc) with
| Call (l, var, f, args) ->
pr buf "%s : call %s = " l var;
dump_expr buf f;
pr buf " (%a)\n" (dump_comma_separated dump_arg) args;
dump_next_instr ()
| Stop exp ->
pr buf " stop %a\n" dump_expr exp;
dump_next_instr ()
| Return exp ->
pr buf " return %a\n" dump_expr exp;
dump_next_instr ()
| Decl_var (var, exp) ->
pr buf " var %s = %a\n" var dump_expr exp;
dump_next_instr ()
| Decl_array (var, Length exp) ->
pr buf " array %s[%a]\n" var dump_expr exp;
dump_next_instr ()
| Decl_array (var, List li) ->
pr buf " array %s = [%a]\n" var (dump_comma_separated dump_expr) li;
dump_next_instr ()
| Drop var ->
pr buf " drop %s\n" var;
dump_next_instr ()
| Assign (var, exp) ->
pr buf " %s <- %a\n" var dump_expr exp;
dump_next_instr ()
| Array_assign (var, index, exp) ->
pr buf " %s[%a] <- %a\n" var dump_expr index dump_expr exp;
dump_next_instr ()
| Branch (exp, l1, l2) ->
pr buf " branch %a %s %s\n" dump_expr exp l1 l2;
dump_next_instr ()
| Label (MergeLabel l | BranchLabel l | BailoutLabel l) ->
print_label l;
dump_instr buf (pc+1) line false
| Goto label ->
pr buf " goto %s\n" label;
dump_next_instr ()
| Print exp ->
pr buf " print %a\n" dump_expr exp;
dump_next_instr ()
| Assert exp ->
pr buf " assert %a\n" dump_expr exp;
dump_next_instr ()
| Read var ->
pr buf " read %s\n" var;
dump_next_instr ()
| Assume {label; guards; target={func; version; pos}; varmap; extra_frames} ->
print_label label;
let dump_var buf = function
| x, e -> pr buf "%s = %a" x dump_expr e
in
let dump_frame buf {cont_pos={func; version; pos}; cont_res; varmap} =
pr buf "(%s, %s, %s) [%s = $, %a]"
func version pos
cont_res
(dump_comma_separated dump_var) varmap
in
pr buf "assume %a else (%s, %s, %s) [%a], %a\n"
(dump_comma_separated dump_expr) guards
func version pos
(dump_comma_separated dump_var) varmap
(dump_comma_separated dump_frame) extra_frames;
dump_next_instr ()
| Guard_hint _
| Comment _ ->
dump_instr buf (pc+1) line needs_label
end;
end
in
dump_instr buf 0 1 true
let disassemble buf (prog : Instr.program) =
let dump_func buf {name; formals; body} =
let print_formal buf (Param x) = pr buf "%s " x in
let print_formals buf = (dump_comma_separated print_formal) buf formals in
Printf.bprintf buf "%s -> ( %t ) ( " name print_formals;
let dump_vers buf version =
pr buf "%s -> (\n" version.label;
disassemble_instrs buf version.instrs;
pr buf ") "
in
List.iter (dump_vers buf) body;
Printf.bprintf buf " ) ";
in
Printf.bprintf buf "P( ";
(dump_comma_separated dump_func) buf (prog.main :: prog.functions);
Printf.bprintf buf ")\n"
let disassemble_s (prog : Instr.program) =
let b = Buffer.create 1024 in
disassemble b prog;
Buffer.to_bytes b
let disassemble_o outchan (prog : Instr.program) =
let b = Buffer.create 1024 in
disassemble b prog;
Buffer.output_buffer outchan b;
flush outchan