Source file printCommon.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
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
open Format
open Utils
open Prog
open Wsize
module E = Expr
let escape = String.map (fun c -> if c = '.' || c = ':' || c = '#' then '_' else c)
let pp_wsize fmt sz = fprintf fmt "%s" (string_of_wsize sz)
let pp_aligned fmt =
function
| Memory_model.Aligned ->
Format.fprintf fmt "#aligned "
| Unaligned -> ()
let pp_unaligned fmt =
function
| Memory_model.Aligned -> ()
| Unaligned ->
Format.fprintf fmt "#unaligned "
let string_of_signess s = if s = Unsigned then "u" else "s"
let string_of_velem s ws ve =
let nws = int_of_ws ws in
let nve = int_of_velem ve in
let s = string_of_signess s in
asprintf "%d%s%d" (nws / nve) s nve
let string_of_cmp_ty = function
| E.Cmp_w (Signed, _) -> "s"
| E.Cmp_w (Unsigned, _) -> "u"
| E.Cmp_int -> ""
let string_of_cmp_kind = function
| E.Cmp_w (sg, sz) -> asprintf " %d%s" (int_of_ws sz) (string_of_signess sg)
| E.Cmp_int -> ""
let string_of_w_cast sz =
asprintf "%du" (int_of_ws sz)
let string_of_op_kind = function
| E.Op_w ws -> string_of_w_cast ws
| E.Op_int -> ""
let string_of_div_kind sg = function
| E.Op_w ws -> asprintf "%d%s" (int_of_ws ws) (string_of_signess sg)
| E.Op_int -> if sg = Signed then (string_of_signess sg) else ""
let string_of_w_ty ws = asprintf "u%d" (int_of_ws ws)
let string_of_wi sg = asprintf "%si" (string_of_signess sg)
let string_of_wi_ty sg ws = asprintf "%si%d" (string_of_signess sg) (int_of_ws ws)
let string_of_int_cast sg =
asprintf "%sint" (string_of_signess sg)
let string_of_wi_cast sg sz =
asprintf "%d%s" (int_of_ws sz) (string_of_wi sg)
let string_of_wiop1 ~debug sg = function
| E.WIwint_of_int sz ->
asprintf "(%s%s)" (string_of_wi_cast sg sz)
(if debug then " /* of int */" else "")
| WIint_of_wint sz ->
asprintf "(%s%s)" (string_of_int_cast sg)
(if debug then " /* of " ^ (string_of_wi_ty sg sz) ^ " */" else "")
| WIword_of_wint sz ->
asprintf "(%s%s)" (string_of_w_cast sz)
(if debug then " /* of " ^ (string_of_wi_ty sg sz) ^ " */" else "")
| WIwint_of_word sz ->
asprintf "(%s%s)" (string_of_wi_cast sg sz)
(if debug then " /* of " ^ (string_of_w_ty sz) ^ " */" else "")
| WIwint_ext(szo, _) ->
asprintf "(%s)" (string_of_wi_cast sg szo)
| WIneg sz ->
asprintf "-%s" (string_of_wi_cast sg sz)
let string_of_op1 ~debug = function
| E.Oint_of_word (s, sz) ->
asprintf "(%s%s)" (string_of_int_cast s)
(if debug then " /* of " ^ (string_of_w_ty sz) ^ " */" else "")
| E.Oword_of_int szo -> asprintf "(%du)" (int_of_ws szo)
| E.Osignext (szo, _) -> asprintf "(%ds)" (int_of_ws szo)
| E.Ozeroext (szo, _) -> asprintf "(%du)" (int_of_ws szo)
| E.Olnot sz ->
asprintf "!%s" (string_of_w_cast sz)
| E.Onot -> "!"
| E.Oneg k -> "-" ^ string_of_op_kind k
| E.Owi1(sg, o) -> string_of_wiop1 ~debug sg o
let string_of_wiop2 sg sz = function
| E.WIadd -> "+" ^ string_of_wi_cast sg sz
| E.WImul -> "*" ^ string_of_wi_cast sg sz
| E.WIsub -> "-" ^ string_of_wi_cast sg sz
| E.WIdiv -> "/" ^ string_of_wi_cast sg sz
| E.WImod -> "%" ^ string_of_wi_cast sg sz
| E.WIshr -> ">>" ^ string_of_wi_cast sg sz
| E.WIshl -> "<<" ^ string_of_wi_cast sg sz
| E.WIeq -> "==" ^ string_of_wi_cast sg sz
| E.WIneq -> "!=" ^ string_of_wi_cast sg sz
| E.WIlt -> "<" ^ string_of_wi_cast sg sz
| E.WIle -> "<=" ^ string_of_wi_cast sg sz
| E.WIgt -> ">" ^ string_of_wi_cast sg sz
| E.WIge -> ">=" ^ string_of_wi_cast sg sz
let string_of_op2 = function
| E.Obeq -> "=="
| E.Oand -> "&&"
| E.Oor -> "||"
| E.Oadd k -> "+" ^ string_of_op_kind k
| E.Omul k -> "*" ^ string_of_op_kind k
| E.Osub k -> "-" ^ string_of_op_kind k
| E.Odiv(s, k) -> "/" ^ string_of_div_kind s k
| E.Omod(s, k) -> "%" ^ string_of_div_kind s k
| E.Oland w -> "&" ^ string_of_w_cast w
| E.Olor w -> "|" ^ string_of_w_cast w
| E.Olxor w -> "^" ^ string_of_w_cast w
| E.Olsr w -> ">>" ^ string_of_w_cast w
| E.Olsl k -> "<<" ^ string_of_op_kind k
| E.Oasr E.Op_int -> ">>s"
| E.Oasr (E.Op_w w) -> asprintf ">>%ds" (int_of_ws w)
| E.Oror w -> ">>r " ^ string_of_w_cast w
| E.Orol w -> "<<r " ^ string_of_w_cast w
| E.Oeq k -> "==" ^ string_of_op_kind k
| E.Oneq k -> "!=" ^ string_of_op_kind k
| E.Olt k -> "<" ^ string_of_cmp_ty k
| E.Ole k -> "<=" ^ string_of_cmp_ty k
| E.Ogt k -> ">" ^ string_of_cmp_ty k
| E.Oge k -> ">=" ^ string_of_cmp_ty k
| Ovadd (ve, ws) -> asprintf "+%s" (string_of_velem Unsigned ws ve)
| Ovsub (ve, ws) -> asprintf "-%s" (string_of_velem Unsigned ws ve)
| Ovmul (ve, ws) -> asprintf "*%s" (string_of_velem Unsigned ws ve)
| Ovlsr (ve, ws) -> asprintf ">>%s" (string_of_velem Unsigned ws ve)
| Ovasr (ve, ws) -> asprintf ">>%s" (string_of_velem Signed ws ve)
| Ovlsl (ve, ws) -> asprintf "<<%s" (string_of_velem Signed ws ve)
| Owi2(sg, ws, o) -> string_of_wiop2 sg ws o
let pp_opn pd asmOp fmt o = pp_string fmt (Sopn.string_of_sopn pd asmOp o)
let pp_syscall (o : 'a Syscall_t.syscall_t) =
match o with Syscall_t.RandomBytes _ -> "#randombytes"
let pp_bool fmt b = if b then fprintf fmt "true" else fprintf fmt "false"
let pp_writable fmt = function
| Constant -> fprintf fmt " const"
| Writable -> fprintf fmt " mut"
let pp_pointer fmt = function
| Direct -> ()
| Pointer w -> fprintf fmt "%a ptr" pp_writable w
let pp_kind fmt = function
| Const -> fprintf fmt "param"
| Stack ptr -> fprintf fmt "stack%a" pp_pointer ptr
| Reg (k, ptr) -> fprintf fmt "reg%a" pp_pointer ptr
| Inline -> fprintf fmt "inline"
| Global -> fprintf fmt "global"
let w_of_signedess = function
| None -> "u"
| Some Wsize.Signed -> "si"
| Some Wsize.Unsigned -> "ui"
let pp_btype ?w fmt = function
| Bool -> fprintf fmt "bool"
| U i -> fprintf fmt "%s%i" (w_of_signedess w) (int_of_ws i)
| Int -> fprintf fmt "int"
let pp_gtype ?w (pp_size : formatter -> 'size -> unit) fmt = function
| Bty ty -> pp_btype ?w fmt ty
| Arr (ws, e) -> fprintf fmt "%a[%a]" (pp_btype ?w:None) (U ws) pp_size e
let non_default_wsize x ws =
if Wsize.wsize_eqb ws (fst (array_kind x.v_ty)) then None
else Some ws
let peel_implicit_cast_to_uint =
function
| Papp1 (Expr.Oint_of_word (Unsigned, _), e)
| e -> e
let pp_access_size fmt = function
| None -> ()
| Some ws -> fprintf fmt ":%a " (pp_btype ?w:None) (U ws)
let pp_mem_access pp_expr fmt al ws e =
fprintf fmt "[%a%a%a]"
pp_aligned al pp_access_size ws pp_expr e
let pp_arr_access pp_gvar pp_expr fmt al aa ws x e =
fprintf fmt "%a%s[%a%a%a]"
pp_gvar x
(if aa = Warray_.AAdirect then "." else "")
pp_unaligned al
pp_access_size ws
pp_expr (peel_implicit_cast_to_uint e)
let pp_arr_slice pp_gvar pp_expr pp_len fmt aa ws x e len =
fprintf fmt "%a%s[%a%a : %a]" pp_gvar x
(if aa = Warray_.AAdirect then "." else "")
pp_access_size ws pp_expr (peel_implicit_cast_to_uint e) pp_len len
let pp_len fmt len = fprintf fmt "%i" len
let pp_ty fmt = pp_gtype pp_len fmt
let pp_datas fmt data =
let pp_w fmt w =
let w = Conv.z_of_int8 w in
fprintf fmt ".byte %s" (Z.to_string w)
in
fprintf fmt "@[<v>%a@]" (pp_list "@ " pp_w) data
let pp_var fmt x =
let y = Conv.var_of_cvar x in
fprintf fmt "%s" y.v_name
let pp_var_i fmt x = pp_var fmt x.E.v_var