Skip to content

Commit 17780e3

Browse files
sim642sim642
authored
Merge pull request #1739 from H-Innos/bit-operation-additions
Improve int domain bitwise operators, support struct bitfields
2 parents aeb8b2c + f76ae66 commit 17780e3

File tree

17 files changed

+1315
-63
lines changed

17 files changed

+1315
-63
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -193,7 +193,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
193193
(* bot = all bits are invalid *)
194194
let bot () = (BArith.zero_mask, BArith.zero_mask)
195195

196-
let top_of ik =
196+
let top_of ?bitfield ik = (* TODO: use bitfield *)
197197
if GoblintCil.isSigned ik then top ()
198198
else (BArith.one_mask, Ints_t.of_bigint (snd (Size.range ik)))
199199

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ struct
4444
let range ik = Size.range ik
4545

4646
let top () = Some (Z.zero, Z.one)
47-
let top_of ik = Some (Z.zero, Z.one)
47+
let top_of ?bitfield ik = Some (Z.zero, Z.one)
4848
let bot () = None
4949
let bot_of ik = bot ()
5050

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

Lines changed: 99 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,17 @@ struct
8484
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. *)
8585
let top_overflow () = `Excluded (S.empty (), overflow_range)
8686
let bot () = `Bot
87-
let top_of ik = `Excluded (S.empty (), size ik)
87+
let top_of ?bitfield ik =
88+
match bitfield with
89+
| Some b when b <= Z.numbits (Size.range ik |> snd) ->
90+
let range =
91+
if Cil.isSigned ik then
92+
R.of_interval range_ikind (Int64.of_int @@ -(b - 1), Int64.of_int b)
93+
else
94+
R.of_interval range_ikind (Int64.zero, Int64.of_int b)
95+
in
96+
`Excluded (S.empty (), range)
97+
| _ -> `Excluded (S.empty (), size ik)
8898
let bot_of ik = bot ()
8999

90100
let show x =
@@ -447,20 +457,49 @@ struct
447457

448458
let ge ik x y = le ik y x
449459

450-
let lognot = lift1 Z.lognot
460+
let lognot ik x = norm ik @@ match x with
461+
| `Excluded (s, r) ->
462+
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
467+
in
468+
`Excluded (s', r')
469+
| `Definite x -> `Definite (Z.lognot x)
470+
| `Bot -> `Bot
451471

452472
let logand ik x y = norm ik (match x,y with
453-
(* We don't bother with exclusion sets: *)
454-
| `Excluded _, `Definite i ->
455-
(* Except in two special cases *)
473+
| `Excluded (_, r), `Definite i
474+
| `Definite i, `Excluded (_, r) ->
456475
if Z.equal i Z.zero then
457476
`Definite Z.zero
458477
else if Z.equal i Z.one then
459478
of_interval IBool (Z.zero, Z.one)
460-
else
461-
top_of ik
462-
| `Definite _, `Excluded _
463-
| `Excluded _, `Excluded _ -> top_of ik
479+
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))
491+
)
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
502+
end
464503
(* The good case: *)
465504
| `Definite x, `Definite y ->
466505
(try `Definite (Z.logand x y) with | Division_by_zero -> top_of ik)
@@ -469,9 +508,58 @@ struct
469508
(* If only one of them is bottom, we raise an exception that eval_rv will catch *)
470509
raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
471510

511+
let logor ik x y = norm ik (match x,y with
512+
| `Excluded (_, r), `Definite i
513+
| `Definite i, `Excluded (_, r) ->
514+
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)))
516+
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))
523+
)
524+
| `Excluded (_, r1), `Excluded (_, r2) -> `Excluded (S.empty (), R.join r1 r2)
525+
| `Definite x, `Definite y ->
526+
(try `Definite (Z.logor x y) with | Division_by_zero -> top_of ik)
527+
| `Bot, `Bot -> `Bot
528+
| _ ->
529+
(* If only one of them is bottom, we raise an exception that eval_rv will catch *)
530+
raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
472531

473-
let logor = lift2 Z.logor
474-
let logxor = lift2 Z.logxor
532+
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
556+
(* The good case: *)
557+
| `Definite x, `Definite y ->
558+
(try `Definite (Z.logxor x y) with | Division_by_zero -> top_of ik)
559+
| `Bot, `Bot -> `Bot
560+
| _ ->
561+
(* If only one of them is bottom, we raise an exception that eval_rv will catch *)
562+
raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
475563

476564
let shift (shift_op: int_t -> int -> int_t) (ik: Cil.ikind) (x: t) (y: t) =
477565
(* BigInt only accepts int as second argument for shifts; perform conversion here *)

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

Lines changed: 121 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -21,10 +21,21 @@ module Enums : S with type int_t = Z.t = struct
2121
let bot () = failwith "bot () not implemented for Enums"
2222
let bot_of ik = Inc (BISet.empty ())
2323
let top_bool = Inc (BISet.of_list [Z.zero; Z.one])
24-
let top_of ik =
24+
25+
let top_of ?bitfield ik =
2526
match ik with
2627
| IBool -> top_bool
27-
| _ -> Exc (BISet.empty (), size ik)
28+
| _ ->
29+
match bitfield with
30+
| Some b when b <= Z.numbits (Size.range ik |> snd) ->
31+
let range =
32+
if Cil.isSigned ik then
33+
R.of_interval range_ikind (Int64.of_int @@ -(b - 1), Int64.of_int b)
34+
else
35+
R.of_interval range_ikind (Int64.of_int 0, Int64.of_int b)
36+
in
37+
Exc (BISet.empty (), range)
38+
| _ -> Exc (BISet.empty (), size ik)
2839

2940
let range ik = Size.range ik
3041

@@ -209,10 +220,114 @@ module Enums : S with type int_t = Z.t = struct
209220

210221
let rem = lift2 Z.rem
211222

212-
let lognot = lift1 Z.lognot
213-
let logand = lift2 Z.logand
214-
let logor = lift2 Z.logor
215-
let logxor = lift2 Z.logxor
223+
let apply_range f r = (* apply f to the min/max of the old range r to get a new range *)
224+
let rf m = (size % Size.min_for % f) (m r) in
225+
let r1, r2 = rf Exclusion.min_of_range, rf Exclusion.max_of_range in
226+
R.join r1 r2
227+
228+
let lognot ikind v = norm ikind @@ match v with
229+
| Inc x when BISet.is_empty x -> v
230+
| Inc x when BISet.is_singleton x -> Inc (BISet.singleton (Z.lognot (BISet.choose x)))
231+
| Inc x -> Inc (BISet.map Z.lognot x) (* TODO: don't operate on Inc? *)
232+
| Exc (s, r) ->
233+
let s' = BISet.map Z.lognot s in
234+
let r' = match R.minimal r, R.maximal r with
235+
| Some min, Some max -> R.of_interval range_ikind (Int64.neg max, Int64.neg min) (* TODO: why missing conditions compared to DefExc lognot? *)
236+
| _, _ -> apply_range Z.lognot r
237+
in
238+
Exc (s', r')
239+
240+
let logand ikind u v = handle_bot u v (fun () ->
241+
norm ikind @@ match u, v with
242+
| Inc x, Inc y when BISet.is_singleton x && BISet.is_singleton y ->
243+
Inc (BISet.singleton (Z.logand (BISet.choose x) (BISet.choose y)))
244+
| Inc x, Exc (s, r)
245+
| Exc (s, r), Inc x ->
246+
let f i =
247+
match R.minimal r, R.maximal r with
248+
| None, _
249+
| _, None -> R.top_of ikind
250+
| Some r1, Some r2 ->
251+
match Z.compare i Z.zero >= 0, Int64.compare r1 Int64.zero >= 0 with
252+
| true, true -> R.of_interval range_ikind (Int64.zero, Int64.min r2 (Int64.of_int @@ Z.numbits i))
253+
| true, _ -> R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i)
254+
| _, true -> R.of_interval range_ikind (Int64.zero, r2)
255+
| _, _ ->
256+
let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
257+
R.of_interval range_ikind (Int64.neg b, b)
258+
in
259+
let r' = BISet.fold (fun i acc -> R.join (f i) acc) x (R.bot ()) in
260+
Exc (BISet.empty (), r')
261+
| Exc (_, p), Exc (_, r) ->
262+
begin match R.minimal p, R.maximal p, R.minimal r, R.maximal r with
263+
| Some p1, Some p2, Some r1, Some r2 ->
264+
begin match Int64.compare p1 Int64.zero >= 0, Int64.compare r1 Int64.zero >= 0 with
265+
| true, true -> Exc (BISet.empty (), R.of_interval range_ikind (Int64.zero, Int64.min p2 r2))
266+
| true, _ -> Exc (BISet.empty (), R.of_interval range_ikind (Int64.zero, p2))
267+
| _, true -> Exc (BISet.empty (), R.of_interval range_ikind (Int64.zero, r2))
268+
| _, _ -> Exc (BISet.empty (), R.join p r)
269+
end
270+
| _ -> top_of ikind
271+
end
272+
| _, _ -> top_of ikind
273+
)
274+
275+
let logor ikind u v = handle_bot u v (fun () ->
276+
norm ikind @@ match u, v with
277+
| Inc x, Inc y when BISet.is_singleton x && BISet.is_singleton y ->
278+
Inc (BISet.singleton (Z.logor (BISet.choose x) (BISet.choose y)))
279+
| Inc x, Exc (_, r)
280+
| Exc (_, r), Inc x ->
281+
let f i =
282+
if Z.compare i Z.zero >= 0 then
283+
R.join r (R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i))
284+
else (
285+
match R.minimal r, R.maximal r with
286+
| None, _
287+
| _, None -> R.top_of ikind
288+
| Some r1, Some r2 ->
289+
let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
290+
R.of_interval range_ikind (Int64.neg b, b)
291+
)
292+
in
293+
let r' = BISet.fold (fun i acc -> R.join (f i) acc) x (R.bot ()) in
294+
Exc (BISet.empty (), r')
295+
| Exc (_, r1), Exc (_, r2) -> Exc (BISet.empty (), R.join r1 r2)
296+
| _ -> top_of ikind
297+
)
298+
299+
let logxor ikind u v = handle_bot u v (fun () ->
300+
norm ikind @@ match u, v with
301+
| Inc x, Inc y when BISet.is_singleton x && BISet.is_singleton y ->
302+
Inc (BISet.singleton (Z.logxor (BISet.choose x) (BISet.choose y)))
303+
| Inc x, Exc (_, r)
304+
| Exc (_, r), Inc x ->
305+
let f i =
306+
match R.minimal r, R.maximal r with
307+
| None, _
308+
| _, None -> R.top_of ikind
309+
| Some r1, Some r2 ->
310+
let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
311+
if Int64.compare r1 Int64.zero >= 0 && Z.compare i Z.zero >= 0 then
312+
R.of_interval range_ikind (Int64.zero, b)
313+
else
314+
R.of_interval range_ikind (Int64.neg b, b)
315+
in
316+
let r' = BISet.fold (fun i acc -> R.join (f i) acc) x (R.bot ()) in
317+
Exc (BISet.empty (), r')
318+
| Exc (_, p), Exc (_, r) ->
319+
begin match R.minimal p, R.maximal p, R.minimal r, R.maximal r with
320+
| Some p1, Some p2, Some r1, Some r2 ->
321+
if Int64.compare p1 Int64.zero >= 0 && Int64.compare r1 Int64.zero >= 0 then
322+
Exc (BISet.empty (), R.of_interval range_ikind (Int64.zero, Int64.max p2 r2))
323+
else (
324+
let b = List.fold_left Int64.max Int64.zero (List.map Int64.abs [p1; p2; r1; r2]) in
325+
Exc (BISet.empty (), R.of_interval range_ikind (Int64.neg b, b))
326+
)
327+
| _, _, _, _ -> top_of ikind
328+
end
329+
| _ -> top_of ikind
330+
)
216331

217332
let shift (shift_op: int_t -> int -> int_t) (ik: Cil.ikind) (x: t) (y: t) =
218333
handle_bot x y (fun () ->

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,7 @@ module IntDomTupleImpl = struct
115115

116116
(* f0: constructors *)
117117
let bot () = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.bot } ()
118-
let top_of = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.top_of }
118+
let top_of ?bitfield = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.top_of ?bitfield }
119119
let bot_of = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.bot_of }
120120
let of_bool ik = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.of_bool ik }
121121
let of_excl_list ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_excl_list ik}

0 commit comments

Comments
 (0)