Source file smt_external.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
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
open Smt_options
module Translate = struct
open Dba
let unary e = function
| Unary_op.Not -> Formula.mk_bv_not
| Unary_op.UMinus -> Formula.mk_bv_neg
| Unary_op.Sext n -> Formula.mk_bv_sign_extend (n - Dba.Expr.size_of e)
| Unary_op.Uext n -> Formula.mk_bv_zero_extend (n - Dba.Expr.size_of e)
| Unary_op.Restrict interval -> Formula.mk_bv_extract interval
let as_bv bop e1 e2 = Formula.(mk_bv_ite (bop e1 e2) mk_bv_one mk_bv_zero)
let rotate_right_const n = Formula.mk_bv_rotate_right n
let rotate_left_const n = Formula.mk_bv_rotate_left n
let rotate shift_func rev_shift_func const_rot_func value shift =
let open Formula in
match shift.bv_term_desc with
| BvCst x ->
let op = Bitvector.value_of x |> Z.to_int |> const_rot_func in
op value
| _ ->
let part1 = shift_func value shift
and shift_size = Formula_utils.bv_size shift
and value_size = Formula_utils.bv_size value |> Z.of_int in
let value_size = Bitvector.create value_size shift_size |> mk_bv_cst in
let offset = mk_bv_sub value_size shift in
let part2 = rev_shift_func value offset in
mk_bv_or part1 part2
let rotate_right =
rotate Formula.mk_bv_lshr Formula.mk_bv_shl rotate_right_const
let rotate_left =
rotate Formula.mk_bv_shl Formula.mk_bv_lshr rotate_left_const
let binary op =
let open Binary_op in
match op with
| Plus -> Formula.mk_bv_add
| Minus -> Formula.mk_bv_sub
| Mult -> Formula.mk_bv_mul
| DivU -> Formula.mk_bv_udiv
| DivS -> Formula.mk_bv_sdiv
| ModU -> Formula.mk_bv_urem
| ModS -> Formula.mk_bv_srem
| Eq -> as_bv Formula.mk_bv_equal
| Diff -> as_bv Formula.mk_bv_distinct
| LeqU -> as_bv Formula.mk_bv_ule
| LtU -> as_bv Formula.mk_bv_ult
| GeqU -> as_bv Formula.mk_bv_uge
| GtU -> as_bv Formula.mk_bv_ugt
| LeqS -> as_bv Formula.mk_bv_sle
| LtS -> as_bv Formula.mk_bv_slt
| GeqS -> as_bv Formula.mk_bv_sge
| GtS -> as_bv Formula.mk_bv_sgt
| Xor -> Formula.mk_bv_xor
| And -> Formula.mk_bv_and
| Or -> Formula.mk_bv_or
| Concat -> Formula.mk_bv_concat
| LShift -> Formula.mk_bv_shl
| RShiftU -> Formula.mk_bv_lshr
| RShiftS -> Formula.mk_bv_ashr
| LeftRotate -> rotate_left
| RightRotate -> rotate_right
let rec expr symbolic_state e =
let smt_unary = unary and smt_binary = binary in
let open Dba.Expr in
match e with
| Var { name; size; _ } ->
Smt_symbolic.State.get_bv name (Size.Bit.create size) symbolic_state
| Cst bv -> (Formula.mk_bv_cst bv, symbolic_state)
| Load (bytes, _endianness, e, None) ->
let smt_e, st = expr symbolic_state e in
let mem = Smt_symbolic.State.get_memory st in
(Formula.mk_select bytes mem smt_e, st)
| Load _ -> assert false
| Binary (bop, lop, rop) as e ->
Logger.debug ~level:6 "Translating binary %a"
Dba_printer.Ascii.pp_bl_term e;
let l_smt_e, st = expr symbolic_state lop in
let r_smt_e, st' = expr st rop in
(smt_binary bop l_smt_e r_smt_e, st')
| Unary (uop, e) ->
let v, st = expr symbolic_state e in
(smt_unary e uop v, st)
| Ite (c, then_e, else_e) ->
let cond, st = expr symbolic_state c in
let then_smt, st' = expr st then_e in
let else_smt, st'' = expr st' else_e in
let v =
Formula.(mk_bv_ite (mk_bv_equal cond mk_bv_one) then_smt else_smt)
in
(v, st'')
open Smt_symbolic
let lvalue_with_rval_update symbolic_state logical_rval = function
| LValue.Var { name; size = bitsize; _ } ->
( name,
Formula.bv_sort bitsize,
Formula.mk_bv_term logical_rval,
symbolic_state )
| LValue.Restrict ({ name; size = bitsize; _ }, { Interval.lo; Interval.hi })
->
let size = Size.Bit.create bitsize in
let t = Formula.bv_sort bitsize in
let svar, st = State.get_bv name size symbolic_state in
let concat_lo = lo - 1 and concat_hi = hi + 1 in
let max_bit = bitsize - 1 in
let rval =
let open Formula in
match (concat_lo < 0, concat_hi > max_bit) with
| false, false ->
mk_bv_concat
(mk_bv_extract
{ Interval.lo = concat_hi; Interval.hi = max_bit }
svar)
(mk_bv_concat logical_rval
(mk_bv_extract
{ Interval.lo = 0; Interval.hi = concat_lo }
svar))
| true, false ->
mk_bv_concat
(mk_bv_extract
{ Interval.lo = concat_hi; Interval.hi = max_bit }
svar)
logical_rval
| false, true ->
mk_bv_concat logical_rval
(mk_bv_extract
{ Interval.lo = 0; Interval.hi = concat_lo }
svar)
| true, true -> logical_rval
in
(name, t, Formula.mk_bv_term rval, st)
| LValue.Store (sz, _, e, None) ->
let mem = State.get_memory symbolic_state in
let value = logical_rval in
let index, st = expr symbolic_state e in
let n, s, v = State.memory_term (Formula.mk_store sz mem index value) in
(n, s, v, st)
| LValue.Store _ -> assert false
let assign ?(wild = false) lval rval symstate =
let logical_rval_base, st = expr symstate rval in
let name, var_type, logical_rval, st' =
lvalue_with_rval_update st logical_rval_base lval
in
Smt_symbolic.State.assign ~wild name var_type logical_rval st'
let gen_unknown =
let count = ref 0 in
fun ?naming_hint () ->
match naming_hint with
| None ->
incr count;
"bs_unknown" ^ string_of_int !count
| Some name -> name
let havoc ?naming_hint ?(wild = false) lvalue ss =
let size = LValue.size_of lvalue in
let name = gen_unknown ?naming_hint () in
let symstate =
Smt_symbolic.State.declare ~wild name (Formula.BvSort size) ss
in
let logical_rval_base, st =
Smt_symbolic.State.get_bv name (Size.Bit.create size) symstate
in
let name, var_type, logical_rval, st' =
lvalue_with_rval_update st logical_rval_base lvalue
in
Smt_symbolic.State.assign name var_type logical_rval st'
let assume cond state =
assert (Expr.size_of cond = 1);
let c, state = expr state cond in
Smt_symbolic.State.constrain Formula.(mk_bv_equal c mk_bv_one) state
end
module Utils = struct
let sse_dirname = "binsec_sse"
let mk_file ~dir =
let n = ref 0 in
fun () ->
incr n;
let temp_dir = dir () in
if not (Sys.file_exists temp_dir) then (
Logger.debug ~level:6 "Creating directory %s" temp_dir;
Unix.mkdir temp_dir 0o700);
let filename =
Filename.concat temp_dir @@ Printf.sprintf "sse_%d.smt2" !n
in
Logger.debug ~level:5 "Creating temporary %s" filename;
filename
let temp_file =
let dir () =
let tmpdir = SMT_dir.get () in
Filename.concat tmpdir sse_dirname
in
mk_file ~dir
end
module Solver = struct
let queries = ref 0
type time = { mutable sec : float }
let cumulated_time = { sec = 0. }
let query_stat () = !queries
let time_stat () = cumulated_time.sec
type t = Formula_solver.Session.t * float
let open_session () =
let timeout = Formula_options.Solver.Timeout.get () in
let file =
if SMT_dir.is_set () then (
let filename = Utils.temp_file () in
Logger.debug ~level:3 "@[<h>Using SMT script file %s@]" filename;
Some filename)
else None
in
let solver = Formula_options.Solver.get () in
let t = Unix.gettimeofday () in
(Formula_solver.Session.create ?file ~timeout solver, t)
let put (solver, _) entry = Formula_solver.Session.put_entry solver entry
let check_sat (solver, _) =
incr queries;
try Formula_solver.Session.check_sat solver with
| Failure msg ->
Logger.warning "SMT solver failed on %s" msg;
Formula_solver.Session.destroy solver;
if not (KeepGoing.get ()) then (
Logger.error
"@[<v 0>@[SMT solver failed with message:@].@ @[%s@]@ @[Aborting. \
Use -keep-going to ignore@]@]"
msg;
failwith msg);
Formula.UNKNOWN
| e ->
Formula_solver.Session.destroy solver;
Logger.warning "Destroyed session";
raise e
let value_of_constant cst =
let open Smtlib in
match cst with
| CstHexadecimal s -> Bitvector.of_hexstring ("0x" ^ s)
| CstBinary s -> Bitvector.of_string ("0b" ^ s)
| CstDecimalSize (value, size) ->
Bitvector.create (Z.of_string value) (int_of_string size)
| CstBool b -> Bitvector.of_bool b
| CstNumeral _ | CstString _ | CstDecimal _ ->
Logger.fatal
"Model construction: unexpected constant %a as bitvector value"
Smtlib_pp.pp_spec_constant cst
let terms =
let open Smtlib in
match terms with
| [ (_, { term_desc = TermSpecConstant cst; _ }) ] -> value_of_constant cst
| _ -> assert false
let get_bv_value (solver, _) e =
extract_bv (Formula_solver.Session.get_value solver (Formula.mk_bv_term e))
let get_ax_values (solver, _) e =
let model = Smt_model.create () in
Smt_model.add_memory_term model
(Formula_solver.Session.get_value solver (Formula.mk_ax_term e));
Smt_model.memory_bindings model
let close_session (solver, t) =
Formula_solver.Session.destroy solver;
cumulated_time.sec <- cumulated_time.sec +. Unix.gettimeofday () -. t
let check_sat_and_close solver =
let res = check_sat solver in
close_session solver;
res
end