From b5bdf56373ac0ffd02728e1e55d7a512241c9562 Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Sun, 2 Jun 2024 18:26:57 +0200 Subject: [PATCH 1/8] int intervals: allow narrowing from widening thresholds --- src/cdomain/value/cdomains/intDomain.ml | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 3bf81b1ba1..f482842ca8 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -572,6 +572,16 @@ module IntervalArith (Ints_t : IntOps.IntOps) = struct let min_ik' = Ints_t.to_bigint min_ik in let t = List.find_opt (fun x -> Z.compare l x >= 0 && Z.compare x min_ik' >= 0) ts in BatOption.map_default Ints_t.of_bigint min_ik t + let is_upper_threshold u = + let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.upper_thresholds () else ResettableLazy.force widening_thresholds in + let u = Ints_t.to_bigint u in + let t = List.find_opt (fun x -> Z.compare u x = 0) ts in + Option.is_some t + let is_lower_threshold l = + let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.lower_thresholds () else ResettableLazy.force widening_thresholds_desc in + let l = Ints_t.to_bigint l in + let t = List.find_opt (fun x -> Z.compare l x = 0) ts in + Option.is_some t end module IntervalFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option = @@ -702,9 +712,10 @@ struct match x, y with | _,None | None, _ -> None | Some (x1,x2), Some (y1,y2) -> + let threshold = get_interval_threshold_widening () in let (min_ik, max_ik) = range ik in - let lr = if Ints_t.compare min_ik x1 = 0 then y1 else x1 in - let ur = if Ints_t.compare max_ik x2 = 0 then y2 else x2 in + let lr = if Ints_t.compare min_ik x1 = 0 || threshold && IArith.is_lower_threshold x1 then y1 else x1 in + let ur = if Ints_t.compare max_ik x2 = 0 || threshold && IArith.is_upper_threshold x2 then y2 else x2 in norm ik @@ Some (lr,ur) |> fst From 87d9a3b5c2b9848105805e08a2e30bb566c40595 Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Tue, 4 Jun 2024 13:03:59 +0200 Subject: [PATCH 2/8] add test for narrowing from thresholds --- tests/regression/03-practical/33-threshold-narrowing.c | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 tests/regression/03-practical/33-threshold-narrowing.c diff --git a/tests/regression/03-practical/33-threshold-narrowing.c b/tests/regression/03-practical/33-threshold-narrowing.c new file mode 100644 index 0000000000..0c713fa273 --- /dev/null +++ b/tests/regression/03-practical/33-threshold-narrowing.c @@ -0,0 +1,8 @@ +// PARAM: --enable ana.int.interval --enable ana.int.interval_threshold_widening --set ana.int.interval_threshold_widening_constants comparisons +#include + +int main() { + int i; + for(i = 0; i < 10 && i < 20; i += 3); + __goblint_check(i <= 12); +} From 11526a831b47d0e408b4d56a2b0015f3e8c29978 Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Tue, 4 Jun 2024 20:23:16 +0200 Subject: [PATCH 3/8] fix: narrow only when interval shrinks --- src/cdomain/value/cdomains/intDomain.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index f482842ca8..b882df732b 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -714,8 +714,8 @@ struct | Some (x1,x2), Some (y1,y2) -> let threshold = get_interval_threshold_widening () in let (min_ik, max_ik) = range ik in - let lr = if Ints_t.compare min_ik x1 = 0 || threshold && IArith.is_lower_threshold x1 then y1 else x1 in - let ur = if Ints_t.compare max_ik x2 = 0 || threshold && IArith.is_upper_threshold x2 then y2 else x2 in + let lr = if Ints_t.compare min_ik x1 = 0 || threshold && Ints_t.compare y1 x1 > 0 && IArith.is_lower_threshold x1 then y1 else x1 in + let ur = if Ints_t.compare max_ik x2 = 0 || threshold && Ints_t.compare y2 x2 < 0 && IArith.is_upper_threshold x2 then y2 else x2 in norm ik @@ Some (lr,ur) |> fst From d6456c87b6a206bc73116a82d385fbfe48431fff Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Tue, 4 Jun 2024 20:32:37 +0200 Subject: [PATCH 4/8] narrow thresholds for int interval sets --- src/cdomain/value/cdomains/intDomain.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index b882df732b..7f91c9d036 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -1393,8 +1393,9 @@ struct let min_ys = minimal ys |> Option.get in let max_ys = maximal ys |> Option.get in let min_range,max_range = range ik in - let min = if min_xs =. min_range then min_ys else min_xs in - let max = if max_xs =. max_range then max_ys else max_xs in + let threshold = get_interval_threshold_widening () in + let min = if min_xs =. min_range || threshold && min_ys <. min_xs && IArith.is_lower_threshold min_xs then min_ys else min_xs in + let max = if max_xs =. max_range || threshold && max_ys <. max_xs && IArith.is_upper_threshold max_xs then max_ys else max_xs in xs |> (function (_, y)::z -> (min, y)::z | _ -> []) |> List.rev From ad73869770c75b3aa7ed144c605079d86026ee36 Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Wed, 5 Jun 2024 13:51:10 +0200 Subject: [PATCH 5/8] integrate comments --- src/cdomain/value/cdomains/intDomain.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 7f91c9d036..a67740e9db 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -575,13 +575,11 @@ module IntervalArith (Ints_t : IntOps.IntOps) = struct let is_upper_threshold u = let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.upper_thresholds () else ResettableLazy.force widening_thresholds in let u = Ints_t.to_bigint u in - let t = List.find_opt (fun x -> Z.compare u x = 0) ts in - Option.is_some t + List.exists (fun x -> Z.compare u x = 0) ts let is_lower_threshold l = let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.lower_thresholds () else ResettableLazy.force widening_thresholds_desc in let l = Ints_t.to_bigint l in - let t = List.find_opt (fun x -> Z.compare l x = 0) ts in - Option.is_some t + List.exists (fun x -> Z.compare l x = 0) ts end module IntervalFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option = @@ -1394,7 +1392,7 @@ struct let max_ys = maximal ys |> Option.get in let min_range,max_range = range ik in let threshold = get_interval_threshold_widening () in - let min = if min_xs =. min_range || threshold && min_ys <. min_xs && IArith.is_lower_threshold min_xs then min_ys else min_xs in + let min = if min_xs =. min_range || threshold && min_ys >. min_xs && IArith.is_lower_threshold min_xs then min_ys else min_xs in let max = if max_xs =. max_range || threshold && max_ys <. max_xs && IArith.is_upper_threshold max_xs then max_ys else max_xs in xs |> (function (_, y)::z -> (min, y)::z | _ -> []) From 94a31d4ef61f6e4227c0329f96342ae1f471eeb5 Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Wed, 5 Jun 2024 14:53:00 +0200 Subject: [PATCH 6/8] test interval-set narrowing and lower bounds --- ...rrowing.c => 33-threshold-narrowing-intervals.c} | 5 +++++ .../34-threshold-narrowing-interval-sets.c | 13 +++++++++++++ 2 files changed, 18 insertions(+) rename tests/regression/03-practical/{33-threshold-narrowing.c => 33-threshold-narrowing-intervals.c} (74%) create mode 100644 tests/regression/03-practical/34-threshold-narrowing-interval-sets.c diff --git a/tests/regression/03-practical/33-threshold-narrowing.c b/tests/regression/03-practical/33-threshold-narrowing-intervals.c similarity index 74% rename from tests/regression/03-practical/33-threshold-narrowing.c rename to tests/regression/03-practical/33-threshold-narrowing-intervals.c index 0c713fa273..ef38c151da 100644 --- a/tests/regression/03-practical/33-threshold-narrowing.c +++ b/tests/regression/03-practical/33-threshold-narrowing-intervals.c @@ -5,4 +5,9 @@ int main() { int i; for(i = 0; i < 10 && i < 20; i += 3); __goblint_check(i <= 12); + + int j; + for(j = 0; j > -10 && j > -20; j-= 3); + __goblint_check(j >= -12); + } diff --git a/tests/regression/03-practical/34-threshold-narrowing-interval-sets.c b/tests/regression/03-practical/34-threshold-narrowing-interval-sets.c new file mode 100644 index 0000000000..c1f11c091e --- /dev/null +++ b/tests/regression/03-practical/34-threshold-narrowing-interval-sets.c @@ -0,0 +1,13 @@ +// PARAM: --enable ana.int.interval_set --enable ana.int.interval_threshold_widening --set ana.int.interval_threshold_widening_constants comparisons +#include + +int main() { + int i; + for(i = 0; i < 10 && i < 20; i += 3); + __goblint_check(i <= 12); + + int j; + for(j = 0; j > -10 && j > -20; j-= 3); + __goblint_check(j >= -12); + +} From 8aa9c4f4f0be045e0ba0363dd12bc72790907a27 Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Wed, 5 Jun 2024 14:54:16 +0200 Subject: [PATCH 7/8] add unit test for interval(-set) narrowing --- tests/unit/cdomains/intDomainTest.ml | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml index e697b022eb..a60b7a6cb1 100644 --- a/tests/unit/cdomains/intDomainTest.ml +++ b/tests/unit/cdomains/intDomainTest.ml @@ -205,6 +205,7 @@ struct let i65536 = I.of_interval ik (Z.zero, of_int 65536) let i65537 = I.of_interval ik (Z.zero, of_int 65537) let imax = I.of_interval ik (Z.zero, of_int 2147483647) + let imin = I.of_interval ik (of_int (-2147483648), Z.zero) let assert_equal x y = assert_equal ~cmp:I.equal ~printer:I.show x y @@ -218,9 +219,34 @@ struct assert_equal imax (I.widen ik i65536 i65537); assert_equal imax (I.widen ik i65536 imax) + let test_interval_narrow _ = + GobConfig.set_bool "ana.int.interval_threshold_widening" true; + GobConfig.set_string "ana.int.interval_threshold_widening_constants" "comparisons"; + let i_zero_one = I.of_interval ik (Z.zero, Z.one) in + let i_zero_five = I.of_interval ik (Z.zero, of_int 5) in + let to_widen = I.of_interval ik (Z.zero, Z.zero) in + (* this should widen to [0, x], where x is the next largest threshold above 5 or the maximal int*) + let widened = I.widen ik to_widen i_zero_five in + (* either way, narrowing from [0, x] to [0, 1] should be possible *) + let narrowed = I.narrow ik widened i_zero_one in + (* however, narrowing should not allow [0, x] to grow *) + let narrowed2 = I.narrow ik widened imax in + assert_equal i_zero_one narrowed; + assert_equal widened narrowed2; + + (* the same tests, but for lower bounds *) + let i_minus_one_zero = I.of_interval ik (Z.minus_one, Z.zero) in + let i_minus_five_zero = I.of_interval ik (of_int (-5), Z.zero) in + let widened = I.widen ik to_widen i_minus_five_zero in + let narrowed = I.narrow ik widened i_minus_one_zero in + let narrowed2 = I.narrow ik widened imin in + assert_equal i_minus_one_zero narrowed; + assert_equal widened narrowed2 + let test () = [ "test_interval_rem" >:: test_interval_rem; "test_interval_widen" >:: test_interval_widen; + "test_interval_narrow" >:: test_interval_narrow; ] end From f0c2c45c4003d222d8f86e6ee703f79f8a15b256 Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Tue, 11 Jun 2024 13:15:36 +0200 Subject: [PATCH 8/8] simplify threshold search for narrowing --- src/cdomain/value/cdomains/intDomain.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index a67740e9db..efbab22b43 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -575,11 +575,11 @@ module IntervalArith (Ints_t : IntOps.IntOps) = struct let is_upper_threshold u = let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.upper_thresholds () else ResettableLazy.force widening_thresholds in let u = Ints_t.to_bigint u in - List.exists (fun x -> Z.compare u x = 0) ts + List.exists (Z.equal u) ts let is_lower_threshold l = let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.lower_thresholds () else ResettableLazy.force widening_thresholds_desc in let l = Ints_t.to_bigint l in - List.exists (fun x -> Z.compare l x = 0) ts + List.exists (Z.equal l) ts end module IntervalFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option =