Skip to content

Commit ae53fb0

Browse files
sim642sim642
authored
Merge pull request #1816 from goblint/interval32
Simplify exclusion bit range module and type
2 parents 09f63d4 + 297343d commit ae53fb0

File tree

9 files changed

+153
-174
lines changed

9 files changed

+153
-174
lines changed

‎src/cdomain/value/cdomains/int/bitfieldDomain.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -660,7 +660,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
660660

661661
let refine_with_bitfield ik x y = meet ik x y
662662

663-
let refine_with_excl_list ik t (excl : (int_t list * (int64 * int64)) option) : t = norm ik t
663+
let refine_with_excl_list ik t (excl : (int_t list * (int * int)) option) : t = norm ik t
664664

665665
let refine_with_incl_list ik t (incl : (int_t list) option) : t =
666666
let joined =match incl with

‎src/cdomain/value/cdomains/int/defExcDomain.ml‎

Lines changed: 62 additions & 77 deletions
Original file line numberDiff line numberDiff line change
@@ -6,17 +6,20 @@ open GoblintCil
66
module BISet = struct
77
include SetDomain.Make (IntOps.BigIntOps)
88
let is_singleton s = cardinal s = 1
9+
10+
let reduce f s =
11+
BatOption.get_exn (fold (fun x acc -> Option.map (f x) acc) s None) (Invalid_argument "BISet.reduce: empty set")
912
end
1013

1114
(* The module [Exclusion] constains common functionality about handling of exclusion sets between [DefExc] and [Enums] *)
1215
module Exclusion =
1316
struct
14-
module R = Interval32
17+
module R = IntervalArith (IntOps.NIntOps)
1518
(* We use these types for the functions in this module to make the intended meaning more explicit *)
16-
type t = Exc of BISet.t * Interval32.t
19+
type t = Exc of BISet.t * R.t
1720
type inc = Inc of BISet.t [@@unboxed]
18-
let max_of_range r = Size.max_from_bit_range (Option.get (R.maximal r))
19-
let min_of_range r = Size.min_from_bit_range (Option.get (R.minimal r))
21+
let max_of_range r = Size.max_from_bit_range (R.maximal r)
22+
let min_of_range r = Size.min_from_bit_range (R.minimal r)
2023
let cardinality_of_range r = Z.succ (Z.add (Z.neg (min_of_range r)) (max_of_range r))
2124

2225
let cardinality_BISet s =
@@ -65,11 +68,11 @@ end
6568
module DefExc : S with type int_t = Z.t = (* definite or set of excluded values *)
6669
struct
6770
module S = BISet
68-
module R = Interval32 (* range for exclusion *)
71+
module R = Exclusion.R (* range for exclusion *)
6972

7073
(* Ikind used for intervals representing the domain *)
7174
let range_ikind = Cil.IInt
72-
let size t = R.of_interval range_ikind (let a,b = Size.bits_i64 t in Int64.neg a,b)
75+
let size t = let a,b = Size.bits t in -a,b
7376

7477

7578
type t = [
@@ -81,17 +84,17 @@ struct
8184
let name () = "def_exc"
8285

8386

84-
let overflow_range = R.of_interval range_ikind (-999L, 999L) (* Since there is no top ikind we use a range that includes both IInt128 [-127,127] and IUInt128 [0,128]. Only needed for intermediate range computation on longs. Correct range is set by cast. *)
87+
let overflow_range = (-999, 999) (* Since there is no top ikind we use a range that includes both IInt128 [-127,127] and IUInt128 [0,128]. Only needed for intermediate range computation on longs. Correct range is set by cast. *)
8588
let top_overflow () = `Excluded (S.empty (), overflow_range)
8689
let bot () = `Bot
8790
let top_of ?bitfield ik =
8891
match bitfield with
8992
| Some b when b <= Z.numbits (Size.range ik |> snd) ->
9093
let range =
9194
if Cil.isSigned ik then
92-
R.of_interval range_ikind (Int64.of_int @@ -(b - 1), Int64.of_int b)
95+
(-(b - 1), b)
9396
else
94-
R.of_interval range_ikind (Int64.zero, Int64.of_int b)
97+
(0, b)
9598
in
9699
`Excluded (S.empty (), range)
97100
| _ -> `Excluded (S.empty (), size ik)
@@ -236,14 +239,14 @@ struct
236239
(* Unless one of them is zero, we can exclude it: *)
237240
else
238241
let a,b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in
239-
let r = R.join (R.of_interval range_ikind a) (R.of_interval range_ikind b) in
242+
let r = R.join a b in
240243
`Excluded ((if Z.equal x Z.zero || Z.equal y Z.zero then S.empty () else S.singleton Z.zero), r)
241244
(* A known value and an exclusion set... the definite value should no
242245
* longer be excluded: *)
243246
| `Excluded (s,r), `Definite x
244247
| `Definite x, `Excluded (s,r) ->
245248
if not (in_range r x) then
246-
let a = R.of_interval range_ikind (Size.min_range_sign_agnostic x) in
249+
let a = Size.min_range_sign_agnostic x in
247250
`Excluded (S.remove x s, R.join a r)
248251
else
249252
`Excluded (S.remove x s, r)
@@ -276,9 +279,11 @@ struct
276279
(* The greatest lower bound of two exclusion sets is their union, this is
277280
* just DeMorgans Law *)
278281
| `Excluded (x,r1), `Excluded (y,r2) ->
279-
let r' = R.meet r1 r2 in
280-
let s' = S.union x y |> S.filter (in_range r') in
281-
`Excluded (s', r')
282+
match R.meet r1 r2 with
283+
| None -> `Bot
284+
| Some r' ->
285+
let s' = S.union x y |> S.filter (in_range r') in
286+
`Excluded (s', r')
282287

283288
let narrow ik x y = x
284289

@@ -296,14 +301,14 @@ struct
296301
| `Definite x -> Some (IntOps.BigIntOps.to_bool x)
297302
| `Excluded (s,r) when S.mem Z.zero s -> Some true
298303
| _ -> None
299-
let top_bool = `Excluded (S.empty (), R.of_interval range_ikind (0L, 1L))
304+
let top_bool = `Excluded (S.empty (), (0, 1))
300305

301306
let of_interval ik (x,y) =
302307
if Z.compare x y = 0 then
303308
of_int ik x
304309
else
305310
let a, b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in
306-
let r = R.join (R.of_interval range_ikind a) (R.of_interval range_ikind b) in
311+
let r = R.join a b in
307312
let ex = if Z.gt x Z.zero || Z.lt y Z.zero then S.singleton Z.zero else S.empty () in
308313
norm ik @@ (`Excluded (ex, r))
309314

@@ -333,7 +338,7 @@ struct
333338
let is_excl_list l = match l with `Excluded _ -> true | _ -> false
334339
let to_excl_list (x:t) = match x with
335340
| `Definite _ -> None
336-
| `Excluded (s,r) -> Some (S.elements s, (Option.get (R.minimal r), Option.get (R.maximal r)))
341+
| `Excluded (s,r) -> Some (S.elements s, r)
337342
| `Bot -> None
338343

339344
let to_incl_list x = match x with
@@ -458,47 +463,40 @@ struct
458463
let ge ik x y = le ik y x
459464

460465
let lognot ik x = norm ik @@ match x with
461-
| `Excluded (s, r) ->
466+
| `Excluded (s, ((min, max) as r)) ->
462467
let s' = S.map Z.lognot s in
463-
let r' = match R.minimal r, R.maximal r with
464-
| Some min, Some max when Int64.compare (Int64.neg max) Int64.zero <= 0 && Int64.compare (Int64.neg min) Int64.zero > 0 ->
465-
R.of_interval range_ikind (Int64.neg max, Int64.neg min)
466-
| _, _ -> apply_range Z.lognot r
468+
let r' =
469+
if -max <= 0 && -min > 0 then
470+
(-max, -min)
471+
else
472+
apply_range Z.lognot r
467473
in
468474
`Excluded (s', r')
469475
| `Definite x -> `Definite (Z.lognot x)
470476
| `Bot -> `Bot
471477

472478
let logand ik x y = norm ik (match x,y with
473-
| `Excluded (_, r), `Definite i
474-
| `Definite i, `Excluded (_, r) ->
479+
| `Excluded (_, (r1, r2)), `Definite i
480+
| `Definite i, `Excluded (_, (r1, r2)) ->
475481
if Z.equal i Z.zero then
476482
`Definite Z.zero
477483
else if Z.equal i Z.one then
478484
of_interval IBool (Z.zero, Z.one)
479485
else (
480-
match R.minimal r, R.maximal r with
481-
| None, _
482-
| _, None -> top_of ik
483-
| Some r1, Some r2 ->
484-
match Z.compare i Z.zero >= 0, Int64.compare r1 Int64.zero >= 0 with
485-
| true, true -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, Int64.min r2 (Int64.of_int @@ Z.numbits i)))
486-
| true, _ -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i))
487-
| _, true -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, r2))
488-
| _, _ ->
489-
let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
490-
`Excluded (S.empty (), R.of_interval range_ikind (Int64.neg b, b))
486+
match Z.compare i Z.zero >= 0, r1 >= 0 with
487+
| true, true -> `Excluded (S.empty (), (0, Int.min r2 (Z.numbits i)))
488+
| true, _ -> `Excluded (S.empty (), (0, Z.numbits i))
489+
| _, true -> `Excluded (S.empty (), (0, r2))
490+
| _, _ ->
491+
let b = Int.max (Z.numbits i) (Int.max (Int.abs r1) (Int.abs r2)) in
492+
`Excluded (S.empty (), (-b, b))
491493
)
492-
| `Excluded (_, p), `Excluded (_, r) ->
493-
begin match R.minimal p, R.maximal p, R.minimal r, R.maximal r with
494-
| Some p1, Some p2, Some r1, Some r2 ->
495-
begin match Int64.compare p1 Int64.zero >= 0, Int64.compare r1 Int64.zero >= 0 with
496-
| true, true -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, Int64.min p2 r2))
497-
| true, _ -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, p2))
498-
| _, true -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, r2))
499-
| _, _ -> `Excluded (S.empty (), R.join p r)
500-
end
501-
| _ -> top_of ik
494+
| `Excluded (_, ((p1, p2) as p)), `Excluded (_, ((r1, r2) as r)) ->
495+
begin match p1 >= 0, r1 >= 0 with
496+
| true, true -> `Excluded (S.empty (), (0, Int.min p2 r2))
497+
| true, _ -> `Excluded (S.empty (), (0, p2))
498+
| _, true -> `Excluded (S.empty (), (0, r2))
499+
| _, _ -> `Excluded (S.empty (), R.join p r)
502500
end
503501
(* The good case: *)
504502
| `Definite x, `Definite y ->
@@ -509,17 +507,13 @@ struct
509507
raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
510508

511509
let logor ik x y = norm ik (match x,y with
512-
| `Excluded (_, r), `Definite i
513-
| `Definite i, `Excluded (_, r) ->
510+
| `Excluded (_, ((r1, r2) as r)), `Definite i
511+
| `Definite i, `Excluded (_, ((r1, r2) as r)) ->
514512
if Z.compare i Z.zero >= 0 then
515-
`Excluded (S.empty (), R.join r (R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i)))
513+
`Excluded (S.empty (), R.join r (0, Z.numbits i))
516514
else (
517-
match R.minimal r, R.maximal r with
518-
| None, _
519-
| _, None -> top_of ik
520-
| Some r1, Some r2 ->
521-
let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
522-
`Excluded (S.empty (), R.of_interval range_ikind (Int64.neg b, b))
515+
let b = Int.max (Z.numbits i) (Int.max (Int.abs r1) (Int.abs r2)) in
516+
`Excluded (S.empty (), (-b, b))
523517
)
524518
| `Excluded (_, r1), `Excluded (_, r2) -> `Excluded (S.empty (), R.join r1 r2)
525519
| `Definite x, `Definite y ->
@@ -530,29 +524,20 @@ struct
530524
raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
531525

532526
let logxor ik x y = norm ik (match x,y with
533-
| `Definite i, `Excluded (_, r)
534-
| `Excluded (_, r), `Definite i ->
535-
begin match R.minimal r, R.maximal r with
536-
| None, _
537-
| _, None -> top_of ik
538-
| Some r1, Some r2 ->
539-
let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
540-
if Int64.compare r1 Int64.zero >= 0 && Z.compare i Z.zero >= 0 then
541-
`Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, b))
542-
else
543-
`Excluded (S.empty (), R.of_interval range_ikind (Int64.neg b, b))
544-
end
545-
| `Excluded (_, p), `Excluded (_, r) ->
546-
begin match R.minimal p, R.maximal p, R.minimal r, R.maximal r with
547-
| Some p1, Some p2, Some r1, Some r2 ->
548-
if Int64.compare p1 Int64.zero >= 0 && Int64.compare r1 Int64.zero >= 0 then
549-
`Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, Int64.max p2 r2))
550-
else (
551-
let b = List.fold_left Int64.max Int64.zero (List.map Int64.abs [p1; p2; r1; r2]) in
552-
`Excluded (S.empty (), R.of_interval range_ikind (Int64.neg b, b))
553-
)
554-
| _, _, _, _ -> top_of ik
555-
end
527+
| `Definite i, `Excluded (_, (r1, r2))
528+
| `Excluded (_, (r1, r2)), `Definite i ->
529+
let b = Int.max (Z.numbits i) (Int.max (Int.abs r1) (Int.abs r2)) in
530+
if r1 >= 0 && Z.compare i Z.zero >= 0 then
531+
`Excluded (S.empty (), (0, b))
532+
else
533+
`Excluded (S.empty (), (-b, b))
534+
| `Excluded (_, (p1, p2)), `Excluded (_, (r1, r2)) ->
535+
if p1 >= 0 && r1 >= 0 then
536+
`Excluded (S.empty (), (0, Int.max p2 r2))
537+
else (
538+
let b = List.fold_left Int.max 0 (List.map Int.abs [p1; p2; r1; r2]) in
539+
`Excluded (S.empty (), (-b, b))
540+
)
556541
(* The good case: *)
557542
| `Definite x, `Definite y ->
558543
(try `Definite (Z.logxor x y) with | Division_by_zero -> top_of ik)

0 commit comments

Comments
 (0)