Source file excluded.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
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
(** Finite sets of possibly included or definitely excluded integer constants *)
open Mopsa
open Sig.Abstraction.Simplified_value
open Ast
open Common
module SimplifiedValue =
struct
(** {2 Types} *)
(** ********* *)
module Set = SetExt.Make(
struct
type t = Z.t
let compare = Z.compare
let print = unformat Z.pp_print
end
)
type t =
| In of Set.t
| NotIn of Set.t
let print printer a =
let print_set prefix s =
if Set.is_empty s then pp_string printer (prefix^"∅")
else
pp_set
(unformat Z.pp_print)
printer
(Set.to_poly_set s)
~sopen:(prefix ^ "{") ~ssep:"," ~sclose:"}" in
match a with
| In s -> print_set "∈ " s
| NotIn s -> print_set "∉ " s
(** {2 Header of the abstraction} *)
(** ***************************** *)
include GenValueId(
struct
type nonrec t = t
let name = "universal.numeric.values.powersets.excluded"
let display = "excluded"
end)
let accept_type = function
| T_int | T_bool -> true
| _ -> false
let bottom = In Set.empty
let top = NotIn Set.empty
let is_bottom a =
match a with
| In s -> Set.is_empty s
| NotIn _ -> false
let is_top a =
match a with
| In _ -> false
| NotIn s -> Set.is_empty s
(** {2 Options} *)
(** *********** *)
let opt_max_intset = ref 10
let () =
register_domain_option name {
key = "-max-excluded-set-size";
category = "Numeric";
doc = " maximum size of integer sets for the excluded powerset";
spec = Set_int (opt_max_intset,ArgExt.empty);
default = string_of_int !opt_max_intset;
}
(** {2 Utilities} *)
(** ************* *)
let zero = In (Set.singleton Z.zero)
let one = In (Set.singleton Z.one)
(** [bound a] is [a] if the number of elements in [a] is lesser or equal to
the maximum number of elements allowed, otherwise it is [top]. Does not
bound the size of [NotIn], as there are no infinite ascending chains for
[NotIn]. *)
let bound_size (a:t) : t =
match a with
| NotIn _ -> a
| In s -> if Set.cardinal s <= !opt_max_intset then a else top
(** [of_bounds l r] is [{l, l+1, ..., r}] if this set has size up to the
maximum number of elements, otherwise it is [NotIn {l-1, r+1}].
This is a precision optimization compared to simply return top, as we
already know that [l - 1] and [r + 1] will not be in the set of elements.
Due to this optimization, top is often represented as
[∉{MININT - 1, MAXINT + 1}] in C programs. *)
let of_bounds (l:Z.t) (h:Z.t) : t =
let rec doit acc i =
if Z.gt i h then In acc
else doit (Set.add i acc) (Z.succ i)
in
if Z.sub h l >= Z.of_int !opt_max_intset
then NotIn (Set.of_list [Z.pred l; Z.succ h])
else doit Set.empty l
let is_zero = function
| In s -> Set.equal s (Set.singleton Z.zero)
| NotIn _ -> false
let contains_zero = function
| In s -> Set.mem Z.zero s
| NotIn s -> Set.mem Z.zero s |> not
let contains_non_zero = function
| In s -> Set.remove Z.zero s |> Set.is_empty |> not
| NotIn s -> true
let remove_zero = function
| In s -> In (Set.remove Z.zero s)
| NotIn s -> NotIn (Set.add Z.zero s)
(** [of_bool t f] is:
- [∅] if [t = false] and [f = false]
- [{0}] if [t = false] and [f = true]
- [{1}] if [t = true] and [f = false]
- [{0,1}] if [t = true] and [f = true] *)
let of_bool t f = match t,f with
| false, false -> bottom
| true, false -> In (Set.singleton Z.one)
| false, true -> In (Set.singleton Z.zero)
| true, true -> In (Set.of_list [Z.zero; Z.one]) |> bound_size
let to_itv (a:t) : int_itv =
if is_top a then Nb I.minf_inf else
if is_bottom a then BOT else
match a with
| In s -> Nb (I.of_z (Set.min_elt s) (Set.max_elt s))
| NotIn _ -> Nb I.minf_inf
let map f = function
| In s -> In (Set.map f s)
| NotIn s -> NotIn (Set.map f s)
(** [combine combiner s1 s2] is [{combiner x1 x2 | x1 ∈ s1, x2 ∈ s2}]. *)
let combine combiner (s1:Set.t) (s2:Set.t) =
Set.fold
(fun n1 acc ->
Set.fold (fun n2 -> Set.add (combiner n1 n2)) s2 acc
) s1 Set.empty
let combine_opt combiner (s1:Set.t) (s2:Set.t) =
Set.fold
(fun n1 acc ->
Set.fold (fun n2 acc ->
match combiner n1 n2 with
| None -> acc
| Some r -> Set.add r acc) s2 acc
) s1 Set.empty
(** {2 Lattice operators} *)
(** ********************* *)
let subset (a1:t) (a2:t) : bool =
match a1,a2 with
| In s1, In s2 -> Set.subset s1 s2
| NotIn s1, NotIn s2 -> Set.subset s2 s1
| In s1, NotIn s2 -> Set.inter s1 s2 |> Set.is_empty
| NotIn s1, In s2 -> false
let join (a1:t) (a2:t) : t =
match a1,a2 with
| In s1, In s2 -> In (Set.union s1 s2)
| NotIn s1, NotIn s2 -> NotIn (Set.inter s1 s2)
| In s1, NotIn s2 -> NotIn (Set.diff s2 s1)
| NotIn s1, In s2 -> NotIn (Set.diff s1 s2)
let meet (a1:t) (a2:t) : t =
match a1,a2 with
| In s1, In s2 -> In (Set.inter s1 s2)
| NotIn s1, NotIn s2 -> NotIn (Set.union s1 s2)
| In s1, NotIn s2 -> In (Set.diff s1 s2)
| NotIn s1, In s2 -> In (Set.diff s2 s1)
let widen ctx (a1:t) (a2:t) : t =
match a1,a2 with
| NotIn _, _ | _, NotIn _ ->
join a1 a2
| In s1, In s2 ->
if Set.cardinal s1 + Set.cardinal s2 <= !opt_max_intset
then In (Set.union s1 s2)
else top
(** {2 Forward semantics} *)
(** ********************* *)
let constant (c: constant) (t: typ) : t =
match c with
| C_bool true -> In (Set.singleton Z.one)
| C_bool false -> In (Set.singleton Z.zero)
| C_top T_bool -> In (Set.of_list [Z.zero; Z.one]) |> bound_size
| C_top T_int -> top
| C_int n -> In (Set.singleton n)
| C_int_interval (Finite i1, Finite i2) -> of_bounds i1 i2
| _ -> top
let unop (op: operator) (t: typ) (a: t) (type_return: typ) =
match op with
| O_plus -> a
| O_minus -> map Z.neg a
| O_log_not -> of_bool (contains_zero a) (contains_non_zero a)
| _ -> top
(** [combine_with combiner a1 a2] combines the elements of [a1] and [a2] with
[combiner]. If [a1] and [a2] are finite sets, it applies [combiner] to the
cartesian product of the two. If [a1] and [a2] are both exclued powersets,
returns [top]. If one of the two is a finite set of size exactly one (and
therefore, it is a definite value), returns an excluded set where the
constant is combined with the excluded powerset. Otherwise, returns [top].
*)
let combine_with combine combiner a1 a2 =
match a1,a2 with
| In s1, In s2 -> In (combine combiner s1 s2) |> bound_size
| NotIn s1, NotIn s2 -> top
| NotIn notin_set, In in_set ->
begin match Set.cardinal in_set with
| 0 -> bottom
| 1 -> NotIn (combine combiner notin_set in_set)
| _ -> top
end
| In in_set, NotIn notin_set ->
begin match Set.cardinal in_set with
| 0 -> bottom
| 1 -> NotIn (combine combiner in_set notin_set)
| _ -> top
end
let binop (op:operator) (t1:typ) (a1:t) (t2:typ) (a2:t) (type_return:typ) =
if is_bottom a1 || is_bottom a2 then bottom else
if is_top a1 || is_top a2 then top else
let with_int f a b = f a (Z.to_int b) in
try match op with
| O_plus -> combine_with combine Z.add a1 a2
| O_minus -> combine_with combine Z.sub a1 a2
| O_mult -> if is_zero a1 || is_zero a2 then zero else combine_with combine Z.mul a1 a2
| O_div ->
let () = debug "%a O_div %a@." (format print) a1 (format print) a2 in
if is_zero a1 then a1 else
let a2 = match a2 with
| In s2 -> In (Set.remove Z.zero s2)
| NotIn s2 -> NotIn (Set.remove Z.zero s2)
in
combine_with combine_opt (fun x y ->
if Z.(x mod y = zero) then Some (Z.div x y)
else None) a1 a2
| O_pow ->
begin match a1,a2 with
| In s1, In s2 -> combine_with combine (with_int Z.pow) a1 a2
| _ -> top
end
| O_bit_and ->
begin match a1,a2 with
| In s1, In s2 -> combine_with combine Z.logand a1 a2
| _ -> top
end
| O_bit_or ->
begin match a1,a2 with
| In s1, In s2 -> combine_with combine Z.logor a1 a2
| _ -> top
end
| O_bit_xor ->
begin match a1,a2 with
| In s1, In s2 -> combine_with combine Z.logxor a1 a2
| _ -> top
end
| O_bit_lshift ->
if is_zero a1 then a1 else
begin match a1,a2 with
| In s1, In s2 -> combine_with combine (with_int Z.shift_left) a1 a2
| _ -> top
end
| O_bit_rshift ->
if is_zero a1 then a1 else
begin match a1,a2 with
| In s1, In s2 -> combine_with combine (with_int Z.shift_right) a1 a2
| _ -> top
end
| O_mod ->
begin match a1,a2 with
| In s1, In s2 -> if is_zero a1 then a1 else combine_with combine Z.rem a1 (remove_zero a2)
| _ -> top
end
| O_log_or ->
of_bool
(contains_non_zero a1 || contains_non_zero a2)
(contains_zero a1 && contains_zero a2)
| O_log_and ->
of_bool
(contains_non_zero a1 && contains_non_zero a2)
(contains_zero a1 || contains_zero a2)
| O_log_xor ->
of_bool
((contains_non_zero a1 && contains_zero a2) ||
(contains_zero a1 && contains_non_zero a2))
((contains_zero a1 && contains_zero a2) ||
(contains_non_zero a1 && contains_non_zero a2))
| _ -> top
with Z.Overflow -> top
include DefaultValueFunctions
let avalue : type r. r avalue_kind -> t -> r option =
fun aval a ->
match aval with
| Common.V_int_interval -> Some (to_itv a)
| Common.V_int_interval_fast -> Some (to_itv a)
| Common.V_int_congr_interval -> Some (to_itv a, Bot.Nb Common.C.minf_inf)
| _ -> None
let rec compare (op:operator) (b:bool) (t1:typ) (a1:t) (t2:typ) (a2:t) : (t*t) =
if is_bottom a1 || is_bottom a2 then (bottom, bottom) else
let op = if b then op else negate_comparison_op op in
match op with
| O_eq ->
begin match a1,a2 with
| In s1, In s2 -> let a = In (Set.inter s1 s2) in a,a
| NotIn s1, NotIn s2 -> let a = NotIn (Set.union s1 s2) in a,a
| In in_set, NotIn notin_set -> In (Set.diff in_set notin_set), a2
| NotIn notin_set, In in_set -> a1, In (Set.diff in_set notin_set)
end
| O_ne ->
begin match a1,a2 with
| In s1, In s2 ->
let s1 = if Set.cardinal s2 = 1 then Set.diff s1 s2 else s1 in
let s2 = if Set.cardinal s1 = 1 then Set.diff s2 s1 else s2 in
In s1, In s2
| NotIn notin_set, In in_set ->
if Set.cardinal in_set = 1 then
let notin_set' = Set.union notin_set in_set in
let in_set' = in_set in
NotIn notin_set', In in_set'
else
a1,a2
| In in_set, NotIn notin_set ->
if Set.cardinal in_set = 1 then
let notin_set' = Set.union notin_set in_set in
let in_set' = in_set in
In in_set', NotIn notin_set'
else
a1,a2
| NotIn _, NotIn _ -> a1, a2
end
| O_le ->
begin match a1,a2 with
| In s1, In s2 ->
let min_s1 = Set.min_elt s1 in
let max_s2 = Set.max_elt s2 in
In (Set.filter (fun n -> Z.leq n max_s2) s1),
In (Set.filter (fun n -> Z.geq n min_s1) s2)
| In s1, NotIn s2 ->
a1, NotIn (Set.add (Set.min_elt s1 |> Z.pred) s2)
| NotIn s1, In s2 ->
NotIn (Set.add (Set.max_elt s2 |> Z.succ) s1), a2
| NotIn _, NotIn _ -> a1, a2
end
| O_ge ->
begin match a1,a2 with
| In s1, In s2 ->
let max_s1 = Set.max_elt s1 in
let min_s2 = Set.min_elt s2 in
In (Set.filter (fun n -> Z.geq n min_s2) s1),
In (Set.filter (fun n -> Z.leq n max_s1) s2)
| In s1, NotIn s2 ->
a1, NotIn (Set.add (Set.max_elt s1 |> Z.succ) s2)
| NotIn s1, In s2 ->
NotIn (Set.add (Set.min_elt s2 |> Z.pred) s1), a2
| NotIn _, NotIn _ -> a1, a2
end
| O_lt ->
begin match a1,a2 with
| In s1, In s2 ->
let min_s1 = Set.min_elt s1 in
let max_s2 = Set.max_elt s2 in
In (Set.filter (fun n -> Z.lt n max_s2) s1),
In (Set.filter (fun n -> Z.gt n min_s1) s2)
| In s1, NotIn s2 ->
a1, NotIn (Set.add (Set.min_elt s1) s2)
| NotIn s1, In s2 ->
NotIn (Set.add (Set.max_elt s2) s1), a2
| NotIn _, NotIn _ -> a1, a2
end
| O_gt ->
begin match a1,a2 with
| In s1, In s2 ->
let max_s1 = Set.max_elt s1 in
let min_s2 = Set.min_elt s2 in
In (Set.filter (fun n -> Z.gt n min_s2) s1),
In (Set.filter (fun n -> Z.lt n max_s1) s2)
| In s1, NotIn s2 ->
a1, NotIn (Set.add (Set.max_elt s1) s2)
| NotIn s1, In s2 ->
NotIn (Set.add (Set.min_elt s2) s1), a2
| NotIn _, NotIn _ -> a1, a2
end
| _ -> default_compare op b t1 a1 t2 a2
end
let () =
register_simplified_value_abstraction (module SimplifiedValue)