Narrowing from widening thresholds

src/cdomain/value/cdomains/intDomain.ml

@@ -572,6 +572,14 @@ 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
+    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 (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 =
@@ -702,9 +710,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 && 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
 
 
@@ -1382,8 +1391,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

tests/regression/03-practical/33-threshold-narrowing-intervals.c

@@ -0,0 +1,13 @@
+// PARAM: --enable ana.int.interval --enable ana.int.interval_threshold_widening --set ana.int.interval_threshold_widening_constants comparisons
+#include <goblint.h>
+
+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);
+
+}

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 <goblint.h>
+
+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);
+
+}

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