Skip to content

Commit d393f28

Browse files
sim642sim642
committed
Remove unnecessary bit range matches in bitwise operations
1 parent fa4d052 commit d393f28

File tree

2 files changed

+73
-100
lines changed

2 files changed

+73
-100
lines changed

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

Lines changed: 38 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -463,44 +463,40 @@ struct
463463
let ge ik x y = le ik y x
464464

465465
let lognot ik x = norm ik @@ match x with
466-
| `Excluded (s, r) ->
466+
| `Excluded (s, ((min, max) as r)) ->
467467
let s' = S.map Z.lognot s in
468-
let r' = match R.minimal r, R.maximal r with (* TODO: remove match *)
469-
| min, max when Int.compare (-max) 0 <= 0 && Int.compare (-min) 0 > 0 ->
468+
let r' =
469+
if Int.compare (-max) 0 <= 0 && Int.compare (-min) 0 > 0 then
470470
(-max, -min)
471-
| _, _ -> apply_range Z.lognot r
471+
else
472+
apply_range Z.lognot r
472473
in
473474
`Excluded (s', r')
474475
| `Definite x -> `Definite (Z.lognot x)
475476
| `Bot -> `Bot
476477

477478
let logand ik x y = norm ik (match x,y with
478-
| `Excluded (_, r), `Definite i
479-
| `Definite i, `Excluded (_, r) ->
479+
| `Excluded (_, (r1, r2)), `Definite i
480+
| `Definite i, `Excluded (_, (r1, r2)) ->
480481
if Z.equal i Z.zero then
481482
`Definite Z.zero
482483
else if Z.equal i Z.one then
483484
of_interval IBool (Z.zero, Z.one)
484485
else (
485-
match R.minimal r, R.maximal r with (* TODO: remove match *)
486-
| r1, r2 ->
487-
match Z.compare i Z.zero >= 0, Int.compare r1 0 >= 0 with
488-
| true, true -> `Excluded (S.empty (), (0, Int.min r2 (Z.numbits i)))
489-
| true, _ -> `Excluded (S.empty (), (0, Z.numbits i))
490-
| _, true -> `Excluded (S.empty (), (0, r2))
491-
| _, _ ->
492-
let b = Int.max (Z.numbits i) (Int.max (Int.abs r1) (Int.abs r2)) in
493-
`Excluded (S.empty (), (-b, b))
486+
match Z.compare i Z.zero >= 0, Int.compare r1 0 >= 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))
494493
)
495-
| `Excluded (_, p), `Excluded (_, r) ->
496-
begin match R.minimal p, R.maximal p, R.minimal r, R.maximal r with (* TODO: remove match *)
497-
| p1, p2, r1, r2 ->
498-
begin match Int.compare p1 0 >= 0, Int.compare r1 0 >= 0 with
499-
| true, true -> `Excluded (S.empty (), (0, Int.min p2 r2))
500-
| true, _ -> `Excluded (S.empty (), (0, p2))
501-
| _, true -> `Excluded (S.empty (), (0, r2))
502-
| _, _ -> `Excluded (S.empty (), R.join p r)
503-
end
494+
| `Excluded (_, ((p1, p2) as p)), `Excluded (_, ((r1, r2) as r)) ->
495+
begin match Int.compare p1 0 >= 0, Int.compare r1 0 >= 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)
504500
end
505501
(* The good case: *)
506502
| `Definite x, `Definite y ->
@@ -511,15 +507,13 @@ struct
511507
raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
512508

513509
let logor ik x y = norm ik (match x,y with
514-
| `Excluded (_, r), `Definite i
515-
| `Definite i, `Excluded (_, r) ->
510+
| `Excluded (_, ((r1, r2) as r)), `Definite i
511+
| `Definite i, `Excluded (_, ((r1, r2) as r)) ->
516512
if Z.compare i Z.zero >= 0 then
517513
`Excluded (S.empty (), R.join r (0, Z.numbits i))
518514
else (
519-
match R.minimal r, R.maximal r with (* TODO: remove match *)
520-
| r1, r2 ->
521-
let b = Int.max (Z.numbits i) (Int.max (Int.abs r1) (Int.abs r2)) in
522-
`Excluded (S.empty (), (-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,26 +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 (* TODO: remove match *)
536-
| r1, r2 ->
537-
let b = Int.max (Z.numbits i) (Int.max (Int.abs r1) (Int.abs r2)) in
538-
if Int.compare r1 0 >= 0 && Z.compare i Z.zero >= 0 then
539-
`Excluded (S.empty (), (0, b))
540-
else
541-
`Excluded (S.empty (), (-b, b))
542-
end
543-
| `Excluded (_, p), `Excluded (_, r) ->
544-
begin match R.minimal p, R.maximal p, R.minimal r, R.maximal r with (* TODO: remove match *)
545-
| p1, p2, r1, r2 ->
546-
if Int.compare p1 0 >= 0 && Int.compare r1 0 >= 0 then
547-
`Excluded (S.empty (), (0, Int.max p2 r2))
548-
else (
549-
let b = List.fold_left Int.max 0 (List.map Int.abs [p1; p2; r1; r2]) in
550-
`Excluded (S.empty (), (-b, b))
551-
)
552-
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 Int.compare r1 0 >= 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 Int.compare p1 0 >= 0 && Int.compare r1 0 >= 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+
)
553541
(* The good case: *)
554542
| `Definite x, `Definite y ->
555543
(try `Definite (Z.logxor x y) with | Division_by_zero -> top_of ik)

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

Lines changed: 35 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -232,42 +232,34 @@ module Enums : S with type int_t = Z.t = struct
232232
| Inc x when BISet.is_empty x -> v
233233
| Inc x when BISet.is_singleton x -> Inc (BISet.singleton (Z.lognot (BISet.choose x)))
234234
| Inc x -> Inc (BISet.map Z.lognot x) (* TODO: don't operate on Inc? *)
235-
| Exc (s, r) ->
235+
| Exc (s, (min, max)) ->
236236
let s' = BISet.map Z.lognot s in
237-
let r' = match R.minimal r, R.maximal r with (* TODO: remove match? *)
238-
| min, max -> (-max, -min) (* TODO: why missing conditions compared to DefExc lognot? *)
239-
(* | _, _ -> apply_range Z.lognot r *)
240-
in
237+
let r' = (-max, -min) in (* TODO: why missing conditions and [apply_range Z.lognot r] compared to DefExc lognot? *)
241238
Exc (s', r')
242239

243240
let logand ikind u v = handle_bot u v (fun () ->
244241
norm ikind @@ match u, v with
245242
| Inc x, Inc y when BISet.is_singleton x && BISet.is_singleton y ->
246243
Inc (BISet.singleton (Z.logand (BISet.choose x) (BISet.choose y)))
247-
| Inc x, Exc (s, r)
248-
| Exc (s, r), Inc x ->
244+
| Inc x, Exc (s, (r1, r2))
245+
| Exc (s, (r1, r2)), Inc x ->
249246
let f i =
250-
match R.minimal r, R.maximal r with (* TODO: remove match *)
251-
| r1, r2 ->
252-
match Z.compare i Z.zero >= 0, Int.compare r1 0 >= 0 with
253-
| true, true -> (0, Int.min r2 (Z.numbits i))
254-
| true, _ -> (0, Z.numbits i)
255-
| _, true -> (0, r2)
256-
| _, _ ->
257-
let b = Int.max (Z.numbits i) (Int.max (Int.abs r1) (Int.abs r2)) in
258-
(-b, b)
247+
match Z.compare i Z.zero >= 0, Int.compare r1 0 >= 0 with
248+
| true, true -> (0, Int.min r2 (Z.numbits i))
249+
| true, _ -> (0, Z.numbits i)
250+
| _, true -> (0, r2)
251+
| _, _ ->
252+
let b = Int.max (Z.numbits i) (Int.max (Int.abs r1) (Int.abs r2)) in
253+
(-b, b)
259254
in
260255
let r' = BISet.reduce (fun i acc -> R.join (f i) acc) x in (* reduce is safe because arguments are not bot here *)
261256
Exc (BISet.empty (), r')
262-
| Exc (_, p), Exc (_, r) ->
263-
begin match R.minimal p, R.maximal p, R.minimal r, R.maximal r with (* TODO: remove match *)
264-
| p1, p2, r1, r2 ->
265-
begin match Int.compare p1 0 >= 0, Int.compare r1 0 >= 0 with
266-
| true, true -> Exc (BISet.empty (), (0, Int.min p2 r2))
267-
| true, _ -> Exc (BISet.empty (), (0, p2))
268-
| _, true -> Exc (BISet.empty (), (0, r2))
269-
| _, _ -> Exc (BISet.empty (), R.join p r)
270-
end
257+
| Exc (_, ((p1, p2) as p)), Exc (_, ((r1, r2) as r)) ->
258+
begin match Int.compare p1 0 >= 0, Int.compare r1 0 >= 0 with
259+
| true, true -> Exc (BISet.empty (), (0, Int.min p2 r2))
260+
| true, _ -> Exc (BISet.empty (), (0, p2))
261+
| _, true -> Exc (BISet.empty (), (0, r2))
262+
| _, _ -> Exc (BISet.empty (), R.join p r)
271263
end
272264
| _, _ -> top_of ikind
273265
)
@@ -276,16 +268,14 @@ module Enums : S with type int_t = Z.t = struct
276268
norm ikind @@ match u, v with
277269
| Inc x, Inc y when BISet.is_singleton x && BISet.is_singleton y ->
278270
Inc (BISet.singleton (Z.logor (BISet.choose x) (BISet.choose y)))
279-
| Inc x, Exc (_, r)
280-
| Exc (_, r), Inc x ->
271+
| Inc x, Exc (_, ((r1, r2) as r))
272+
| Exc (_, ((r1, r2) as r)), Inc x ->
281273
let f i =
282274
if Z.compare i Z.zero >= 0 then
283275
R.join r (0, Z.numbits i)
284276
else (
285-
match R.minimal r, R.maximal r with (* TODO: remove match *)
286-
| r1, r2 ->
287-
let b = Int.max (Z.numbits i) (Int.max (Int.abs r1) (Int.abs r2)) in
288-
(-b, b)
277+
let b = Int.max (Z.numbits i) (Int.max (Int.abs r1) (Int.abs r2)) in
278+
(-b, b)
289279
)
290280
in
291281
let r' = BISet.reduce (fun i acc -> R.join (f i) acc) x in (* reduce is safe because arguments are not bot here *)
@@ -298,29 +288,24 @@ module Enums : S with type int_t = Z.t = struct
298288
norm ikind @@ match u, v with
299289
| Inc x, Inc y when BISet.is_singleton x && BISet.is_singleton y ->
300290
Inc (BISet.singleton (Z.logxor (BISet.choose x) (BISet.choose y)))
301-
| Inc x, Exc (_, r)
302-
| Exc (_, r), Inc x ->
291+
| Inc x, Exc (_, (r1, r2))
292+
| Exc (_, (r1, r2)), Inc x ->
303293
let f i =
304-
match R.minimal r, R.maximal r with (* TODO: remove match *)
305-
| r1, r2 ->
306-
let b = Int.max (Z.numbits i) (Int.max (Int.abs r1) (Int.abs r2)) in
307-
if Int.compare r1 0 >= 0 && Z.compare i Z.zero >= 0 then
308-
(0, b)
309-
else
310-
(-b, b)
294+
let b = Int.max (Z.numbits i) (Int.max (Int.abs r1) (Int.abs r2)) in
295+
if Int.compare r1 0 >= 0 && Z.compare i Z.zero >= 0 then
296+
(0, b)
297+
else
298+
(-b, b)
311299
in
312300
let r' = BISet.reduce (fun i acc -> R.join (f i) acc) x in (* reduce is safe because arguments are not bot here *)
313301
Exc (BISet.empty (), r')
314-
| Exc (_, p), Exc (_, r) ->
315-
begin match R.minimal p, R.maximal p, R.minimal r, R.maximal r with (* TODO: remove match *)
316-
| p1, p2, r1, r2 ->
317-
if Int.compare p1 0 >= 0 && Int.compare r1 0 >= 0 then
318-
Exc (BISet.empty (), (0, Int.max p2 r2))
319-
else (
320-
let b = List.fold_left Int.max 0 (List.map Int.abs [p1; p2; r1; r2]) in
321-
Exc (BISet.empty (), (-b, b))
322-
)
323-
end
302+
| Exc (_, (p1, p2)), Exc (_, (r1, r2)) ->
303+
if Int.compare p1 0 >= 0 && Int.compare r1 0 >= 0 then
304+
Exc (BISet.empty (), (0, Int.max p2 r2))
305+
else (
306+
let b = List.fold_left Int.max 0 (List.map Int.abs [p1; p2; r1; r2]) in
307+
Exc (BISet.empty (), (-b, b))
308+
)
324309
| _ -> top_of ikind
325310
)
326311

0 commit comments

Comments
 (0)