int_set.ml 16.7 KB
Newer Older
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
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2019                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Abstract_interp
open Bottom.Type

(* Make sure all this is synchronized with the default value of -ilevel *)
let small_cardinal = ref 8
let set_small_cardinal i = small_cardinal := i

let debug_cardinal = false

let emitter = Lattice_messages.register "Int_set";;
let log_imprecision s = Lattice_messages.emit_imprecision emitter s

type set = Int.t array

let bottom = Array.make 0 Int.zero

let small_nums = Array.init 33 (fun i -> [| (Integer.of_int i) |])

let zero = small_nums.(0)
let one = small_nums.(1)
let minus_one = [| Int.minus_one |]
let zero_or_one = [| Int.zero ; Int.one |]

let inject_singleton e =
  if Int.le Int.zero e && Int.le e Int.thirtytwo
  then small_nums.(Int.to_int e)
  else [| e |]

let unsafe_share_array a s =
  let e = a.(0) in
  if s = 1 && Int.le Int.zero e && Int.le e Int.thirtytwo
  then small_nums.(Int.to_int e)
  else if s = 2 && Int.is_zero e && Int.is_one a.(1)
  then zero_or_one
  else a

(* TODO: assert s <> 0 *)
let share_array a s =
  if s = 0 then bottom else unsafe_share_array a s

let share_array_or_bottom a s =
  if s = 0 then `Bottom else `Value (unsafe_share_array a s)

let inject_array = share_array

let project_array t = t

(* ------------------------------- Datatype --------------------------------- *)

let hash s = Array.fold_left (fun acc v -> 1031 * acc + (Int.hash v)) 17 s

let rehash s = share_array s (Array.length s)

exception Unequal of int

let compare s1 s2 =
  if s1 == s2 then 0 else
    let l1 = Array.length s1 in
    let l2 = Array.length s2 in
    if l1 <> l2
    then l1 - l2 (* no overflow here *)
    else
      (try
         for i = 0 to l1 - 1 do
           let r = Int.compare s1.(i) s2.(i) in
           if r <> 0 then raise (Unequal r)
         done;
         0
       with Unequal v -> v)

let equal e1 e2 = compare e1 e2 = 0

let pretty fmt s =
  if Array.length s = 0 then Format.fprintf fmt "BottomMod"
  else begin
    Pretty_utils.pp_iter
      ~pre:"@[<hov 1>{"
      ~suf:"}@]"
      ~sep:";@ "
      Array.iter Int.pretty fmt s
  end

include Datatype.Make_with_collections
    (struct
      type t = set
      let name = "int_set"
      open Structural_descr
      let structural_descr = t_array (Descr.str Int.descr)
      let reprs = [ zero ]
      let equal = equal
      let compare = compare
      let hash = hash
      let pretty = pretty
      let rehash = rehash
      let internal_pretty_code = Datatype.pp_fail
      let mem_project = Datatype.never_any_project
      let copy = Datatype.undefined
      let varname = Datatype.undefined
    end)

(* ---------------------------------- Utils --------------------------------- *)

let cardinal = Array.length

let for_all f (a : Integer.t array) =
  let l = Array.length a in
  let rec c i = i = l || ((f a.(i)) && c (succ i)) in
  c 0

let exists = Extlib.array_exists

let iter = Array.iter
let fold = Array.fold_left

let truncate r i =
  if i = 0
  then `Bottom
  else if i = 1
  then `Value (inject_singleton r.(0))
  else begin
    (Obj.truncate (Obj.repr r) i);
    assert (Array.length r = i);
    `Value r
  end

exception Empty

let map_reduce (f : 'a -> 'b) (g : 'b -> 'b -> 'b) (set : 'a array) : 'b =
  if Array.length set <= 0 then
    raise Empty
  else
    let acc = ref (f set.(0)) in
    for i = 1 to Array.length set - 1 do
      acc := g !acc (f set.(i))
    done;
    !acc

let filter (f : Int.t -> bool) (a : Int.t array) : t or_bottom =
  let l = Array.length a in
  let r = Array.make l Int.zero in
  let j = ref 0 in
  for i = 0 to l  - 1 do
    let x = a.(i) in
    if f x then begin
      r.(!j) <- x;
      incr j;
    end
  done;
  truncate r !j

let mem v a =
  let l = Array.length a in
  let rec c i =
    if i = l then (-1)
    else
      let ae = a.(i) in
      if Int.equal ae v
      then i
      else if Int.gt ae v
      then (-1)
      else c (succ i)
  in
  c 0

(* ------------------------------- Set or top ------------------------------- *)

type set_or_top = [ `Set of t | `Top of Integer.t * Integer.t * Integer.t ]

module O = FCSet.Make (Integer)

type pre_set =
  | Pre_set of O.t * int
  | Pre_top of Int.t * Int.t * Int.t

let empty_ps = Pre_set (O.empty, 0)

(* TODO: share this code with ival2.make_itv_from_set? *)
let make_top_from_set s =
  if debug_cardinal then assert (O.cardinal s >= 2);
  let min = O.min_elt s in
  let max = O.max_elt s in
  let modu = O.fold
      (fun x acc ->
         if Int.equal x min then acc else Int.pgcd (Int.sub x min) acc)
      s Int.zero
  in
  (min, max, modu)

let add_ps ps x =
  match ps with
  | Pre_set (o, s) ->
    if debug_cardinal then assert (O.cardinal o = s);
    if O.mem x o (* TODO: improve *)
    then ps
    else
      let no = O.add x o in
      if s < !small_cardinal
      then begin
        if debug_cardinal then assert (O.cardinal no = succ s);
        Pre_set (no, succ s)
      end
      else
        let min, max, modu =  make_top_from_set no in
        Pre_top (min, max, modu)
  | Pre_top (min, max, modu) ->
    let new_modu =
      if Int.equal x min
      then modu
      else Int.pgcd (Int.sub x min) modu
    in
    let new_min = Int.min min x in
    let new_max = Int.max max x in
    Pre_top (new_min, new_max, new_modu)

let o_zero = O.singleton Int.zero
let o_one = O.singleton Int.one
let o_zero_or_one = O.union o_zero o_one

let share_set o s =
  if s = 0 then bottom
  else if s = 1
  then begin
    let e = O.min_elt o in
    inject_singleton e
  end
  else if O.equal o o_zero_or_one
  then zero_or_one
  else
    let a = Array.make s Int.zero in
    let i = ref 0 in
    O.iter (fun e -> a.(!i) <- e; incr i) o;
    assert (!i = s);
    a

let inject_ps = function
  | Pre_set (o, s) -> `Set (share_set o s)
  | Pre_top (min, max, modu) -> `Top (min, max, modu)

(* Given a set of elements that is an under-approximation, returns an
   ival (while maintaining the ival invariants that the "Set"
   constructor is used only for small sets of elements. *)
let set_to_ival_under set =
  let card = Int.Set.cardinal set in
  if card <= !small_cardinal
  then
    let a = Array.make card Int.zero in
    ignore (Int.Set.fold (fun elt i -> Array.set a i elt; i + 1) set 0);
    `Set (share_array a card)
  else
    (* If by chance the set is contiguous. *)
  if (Int.equal
        (Int.sub (Int.Set.max_elt set) (Int.Set.min_elt set))
        (Int.of_int (card - 1)))
  then `Top (Int.Set.min_elt set, Int.Set.max_elt set, Int.one)
  (* Else: arbitrarily drop some elements of the under approximation. *)
  else
    let a = Array.make !small_cardinal Int.zero in
    log_imprecision "Ival.set_to_ival_under";
    try
      ignore (Int.Set.fold (fun elt i ->
          if i = !small_cardinal then raise Exit;
          Array.set a i elt;
          i + 1) set 0);
      assert false
    with Exit -> `Set a

(* ------------------------------ Apply and map ----------------------------- *)

let apply_bin_1_strict_incr f x (s : Integer.t array) =
  let l = Array.length s in
  let r = Array.make l Int.zero in
  let rec c i =
    if i = l
    then share_array r l
    else
      let v = f x s.(i) in
      r.(i) <- v;
      c (succ i)
  in
  c 0

let apply_bin_1_strict_decr f x (s : Integer.t array) =
  let l = Array.length s in
  let r = Array.make l Int.zero in
  let rec c i =
    if i = l
    then share_array r l
    else
      let v = f x s.(i) in
      r.(l - i - 1) <- v;
      c (succ i)
  in
  c 0

let apply2_n f (s1 : Integer.t array) (s2 : Integer.t array) =
  let ps = ref empty_ps in
  let l1 = Array.length s1 in
  let l2 = Array.length s2 in
  for i1 = 0 to pred l1 do
    let e1 = s1.(i1) in
    for i2 = 0 to pred l2 do
      ps := add_ps !ps (f e1 s2.(i2))
    done
  done;
  inject_ps !ps

let apply2_notzero f (s1 : Integer.t array) s2 =
  inject_ps
    (Array.fold_left
       (fun acc v1 ->
          Array.fold_left
            (fun acc v2 ->
               if Int.is_zero v2
               then acc
               else add_ps acc (f v1 v2))
            acc
            s2)
       empty_ps
       s1)

let map_set_decr f (s : Integer.t array) =
  let l = Array.length s in
  if l = 0
  then `Bottom
  else
    let r = Array.make l Int.zero in
    let rec c srcindex dstindex last =
      if srcindex < 0
      then begin
        r.(dstindex) <- last;
        truncate r (succ dstindex)
      end
      else
        let v = f s.(srcindex) in
        if Int.equal v last
        then
          c (pred srcindex) dstindex last
        else begin
          r.(dstindex) <- last;
          c (pred srcindex) (succ dstindex) v
        end
    in
    c (l-2) 0 (f s.(pred l))

let map_set_strict_decr f (s : Integer.t array) =
  let l = Array.length s in
  let r = Array.make l Int.zero in
  let rec c i =
    if i = l
    then share_array r l
    else
      let v = f s.(i) in
      r.(l - i - 1) <- v;
      c (succ i)
  in
  c 0

let map_set_incr f (s : Integer.t array) =
  let l = Array.length s in
  if l = 0
  then `Bottom
  else
    let r = Array.make l Int.zero in
    let rec c srcindex dstindex last =
      if srcindex = l
      then begin
        r.(dstindex) <- last;
        truncate r (succ dstindex)
      end
      else
        let v = f s.(srcindex) in
        if Int.equal v last
        then
          c (succ srcindex) dstindex last
        else begin
          r.(dstindex) <- last;
          c (succ srcindex) (succ dstindex) v
        end
    in
    c 1 0 (f s.(0))

let map f s =
  let pre_set =
    Array.fold_left (fun acc elt -> add_ps acc (f elt)) empty_ps s
  in
  match pre_set with
  | Pre_set (o, s) -> share_set o s
  | Pre_top _ -> assert false

(* --------------------------------- Lattice -------------------------------- *)

let is_included s1 s2 =
  let l1 = Array.length s1 in
  let l2 = Array.length s2 in
  if l1 > l2 then false
  else
    let rec c i1 i2 =
      if i1 = l1 then true
      else if i2 = l2 then false
      else
        let e1 = s1.(i1) in
        let e2 = s2.(i2) in
        let si2 = succ i2 in
        if Int.equal e1 e2
        then c (succ i1) si2
        else if Int.lt e1 e2
        then false
        else c i1 si2 (* TODO: improve by not reading a1.(i1) all the time *)
    in
    c 0 0

(* Join [s1] of length [l1] and [s2] of length [l2]. *)
let join l1 s1 l2 s2 =
  (* first pass: count unique elements and detect inclusions *)
  let rec first i1 i2 uniq inc1 inc2 =
    if i1 = l1
    then (uniq + l2 - i2), false, inc2
    else if i2 = l2
    then (uniq + l1 - i1), inc1, false
    else
      let e1 = s1.(i1) in
      let e2 = s2.(i2) in
      if Int.lt e2 e1
      then first i1 (succ i2) (succ uniq) false inc2
      else if Int.gt e2 e1
      then first (succ i1) i2 (succ uniq) inc1 false
      else first (succ i1) (succ i2) (succ uniq) inc1 inc2
  in
  let uniq, incl1, incl2 = first 0 0 0 true true in
  if incl1 then `Set s1 else
  if incl2 then `Set s2 else
    (* second pass: make a set or make a top *)
  if uniq > !small_cardinal
  then
    let min = Int.min s1.(0) s2.(0) in
    let accum acc x =
      if Int.equal x min
      then acc
      else Int.pgcd (Int.sub x min) acc
    in
    let modu = ref Int.zero in
    for j = 0 to pred l1 do
      modu := accum !modu s1.(j)
    done;
    for j = 0 to pred l2 do
      modu := accum !modu s2.(j)
    done;
    `Top (min, Int.max s1.(pred l1) s2.(pred l2), !modu)
  else
    let r = Array.make uniq Int.zero in
    let rec c i i1 i2 =
      if i1 = l1
      then begin
        Array.blit s2 i2 r i (l2 - i2);
        share_array r uniq
      end
      else if i2 = l2
      then begin
        Array.blit s1 i1 r i (l1 - i1);
        share_array r uniq
      end
      else
        let si = succ i in
        let e1 = s1.(i1) in
        let e2 = s2.(i2) in
        if Int.lt e2 e1
        then begin
          r.(i) <- e2;
          c si i1 (succ i2)
        end
        else begin
          r.(i) <- e1;
          let si1 = succ i1 in
          if Int.equal e1 e2
          then c si si1 (succ i2)
          else c si si1 i2
        end
    in
    `Set (c 0 0 0)

let join s1 s2 =
  let l1 = Array.length s1 in
  if l1 = 0
  then `Set s2
  else
    let l2 = Array.length s2 in
    if l2 = 0
    then `Set s1
    else join l1 s1 l2 s2

let link s1 s2 =
  let s1 = Array.fold_right Int.Set.add s1 Int.Set.empty in
  let s2 = Array.fold_right Int.Set.add s2 s1 in
  set_to_ival_under s2

let meet s1 s2 =
  let l1 = Array.length s1 in
  let l2 = Array.length s2 in
  let lr_max = min l1 l2 in
  let r = Array.make lr_max Int.zero in
  let rec c i i1 i2 =
    if i1 = l1 || i2 = l2
    then truncate r i
    else
      let e1 = s1.(i1) in
      let e2 = s2.(i2) in
      if Int.equal e1 e2
      then begin
        r.(i) <- e1;
        c (succ i) (succ i1) (succ i2)
      end
      else if Int.lt e1 e2
      then c i (succ i1) i2
      else c i i1 (succ i2)
  in
  c 0 0 0

let narrow = meet (* meet is exact. *)

let intersects s1 s2 =
  let l1 = Array.length s1 in
  let l2 = Array.length s2 in
  let rec aux i1 i2 =
    if i1 = l1 || i2 = l2 then false
    else
      let e1 = s1.(i1) in
      let e2 = s2.(i2) in
      if Int.equal e1 e2 then true
      else if Int.lt e1 e2 then aux (succ i1) i2
      else aux i1 (succ i2)
  in
  aux 0 0

let diff_if_one _value _rem = assert false

let remove s v =
  let index = mem v s in
  if index >= 0
  then
    let l = Array.length s in
    let pl = pred l in
    let r = Array.make pl Int.zero in
    Array.blit s 0 r 0 index;
    Array.blit s (succ index) r index (pl-index);
    share_array_or_bottom r pl
  else `Value s

(* ------------------------------ Arithmetics ------------------------------- *)

let add_singleton = apply_bin_1_strict_incr Int.add

let add s1 s2 =
  match s1, s2 with
  | [| x |], s | s, [| x |] -> `Set (apply_bin_1_strict_incr Int.add x s)
  | _, _ -> apply2_n Int.add s1 s2

let add_under s1 s2 =
  match s1, s2 with
  | [| x |], s | s, [| x |] -> `Set (apply_bin_1_strict_incr Int.add x s)
  | _, _ ->
    let set =
      Array.fold_left (fun acc i1 ->
          Array.fold_left (fun acc i2 ->
              Int.Set.add (Int.add i1 i2) acc) acc s2)
        Int.Set.empty s1
    in
    set_to_ival_under set

let neg s = map_set_strict_decr Int.neg s

let scale f s =
  if Int.ge f Int.zero
  then apply_bin_1_strict_incr Int.mul f s
  else apply_bin_1_strict_decr Int.mul f s

let mul s1 s2 =
  match s1, s2 with
  | s, [| x |] | [| x |], s -> `Set (scale x s)
  | _, _ -> apply2_n Int.mul s1 s2

let scale_div ~pos f s =
  let div_f =
    if pos
    then fun a -> Int.e_div a f
    else fun a -> Int.c_div a f
  in
  if Int.lt f Int.zero
  then map_set_decr div_f s
  else map_set_incr div_f s

let scale_rem ~pos f s =
  let f = if Int.lt f Int.zero then Int.neg f else f in
  let rem_f a =
    if pos then Int.e_rem a f else Int.c_rem a f
  in
  let pre_set =
    Array.fold_left
      (fun acc v -> add_ps acc (rem_f v))
      empty_ps
      s
  in
  inject_ps pre_set

let c_rem s1 s2 = apply2_notzero Int.c_rem s1 s2

let bitwise_signed_not = map_set_strict_decr Int.lognot

(* ------------------------------- Subdivide -------------------------------- *)

let subdivide s =
  let len = Array.length s in
  assert (len > 0 );
  if len <= 1 then raise Can_not_subdiv;
  let m = len lsr 1 in
  let lenhi = len - m in
  let lo = Array.sub s 0 m in
  let hi = Array.sub s m lenhi in
  share_array lo m,
  share_array hi lenhi


(* -------------------------------- Export ---------------------------------- *)

let min t = t.(0)
let max t = t.(Array.length t - 1)