Merge pull request #134 from goblint/interval_no_compute_on_top

Interval domain: Don't compute on top values

Author: jerhard

src/cdomains/intDomain.ml

@@ -266,7 +266,15 @@ struct
       let ur = if Int64.compare max_int x2 = 0 then y2 else x2 in
       norm @@ Some (lr,ur)
 
+  (* Returns top if one of a, b is top, otherwise return result *)
+  let on_top_return_top_bin a b result =
+    if is_top a || is_top b then top () else result
+
+  let on_top_return_top_un a result =
+    if is_top a then top () else result
+
   let log f i1 i2 =
+    on_top_return_top_bin i1 i2 @@
     match is_bot i1, is_bot i2 with
     | true, true -> bot ()
     | true, _
@@ -280,6 +288,7 @@ struct
   let logand = log (&&)
 
   let log1 f i1 =
+    on_top_return_top_un i1 @@
     if is_bot i1 then
       bot ()
     else
@@ -290,6 +299,7 @@ struct
   let lognot = log1 not
 
   let bit f i1 i2 =
+    on_top_return_top_bin i1 i2 @@
     match is_bot i1, is_bot i2 with
     | true, true -> bot ()
     | true, _
@@ -315,17 +325,20 @@ struct
   let shift_right = bit (fun x y -> Int64.shift_right x (Int64.to_int y))
   let shift_left  = bit (fun x y -> Int64.shift_left  x (Int64.to_int y))
 
-  let neg = function None -> None | Some (x,y) -> norm @@ Some (Int64.neg y, Int64.neg x)
+  let neg x = on_top_return_top_un x @@ match x with None -> None | Some (x,y) -> norm @@ Some (Int64.neg y, Int64.neg x)
 
   let add x y =
+    on_top_return_top_bin x y @@
     match x, y with
     | None, None -> None
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (short 80 x) (short 80 y)))
     | Some (x1,x2), Some (y1,y2) -> norm @@ Some (Int64.add x1 y1, Int64.add x2 y2)
 
   let sub i1 i2 = add i1 (neg i2)
 
-  let rem x y = match x, y with
+  let rem x y =
+    on_top_return_top_bin x y @@
+    match x, y with
     | None, None -> None
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (short 80 x) (short 80 y)))
     | Some (xl, xu), Some (yl, yu) ->
@@ -348,16 +361,21 @@ struct
         meet (bit Int64.rem x y) range
 
   let mul x y =
-    match x, y with
-    | None, None -> bot ()
-    | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (short 80 x) (short 80 y)))
-    | Some (x1,x2), Some (y1,y2) ->
-      let x1y1 = (Int64.mul x1 y1) in let x1y2 = (Int64.mul x1 y2) in
-      let x2y1 = (Int64.mul x2 y1) in let x2y2 = (Int64.mul x2 y2) in
-      norm @@ Some ((min (min x1y1 x1y2) (min x2y1 x2y2)),
-                    (max (max x1y1 x1y2) (max x2y1 x2y2)))
+    if (is_top x || is_top y) && to_int x <> Some 0L && to_int y <> Some 0L then
+      (* if one of the argument is zero, the result must be zero, even if the value is outside the range of Interval32 *)
+      top ()
+    else
+      match x, y with
+      | None, None -> bot ()
+      | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (short 80 x) (short 80 y)))
+      | Some (x1,x2), Some (y1,y2) ->
+        let x1y1 = (Int64.mul x1 y1) in let x1y2 = (Int64.mul x1 y2) in
+        let x2y1 = (Int64.mul x2 y1) in let x2y2 = (Int64.mul x2 y2) in
+        norm @@ Some ((min (min x1y1 x1y2) (min x2y1 x2y2)),
+                      (max (max x1y1 x1y2) (max x2y1 x2y2)))
 
   let rec div x y =
+    on_top_return_top_bin x y @@
     match x, y with
     | None, None -> bot ()
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (short 80 x) (short 80 y)))

tests/regression/01-cpa/43-large-n-div.c

@@ -0,0 +1,18 @@
+//PARAM: --enable ana.int.interval --disable ana.int.def_exc
+#include <assert.h>
+
+int main(){
+    // 2^33
+    long long x = 8589934592l;
+    // 2^31 - 1
+    long long y = 2147483647;
+
+    long long z = x/y;
+
+    if(z == 4){
+        // Should be reachable
+        assert(1);
+    }
+
+    assert(z > 2); //UNKNOWN
+}

tests/regression/01-cpa/44-large-n-div2.c

@@ -0,0 +1,23 @@
+//PARAM: --enable ana.int.interval --enable ana.int.def_exc
+#include <assert.h>
+
+int main(){
+    int top;
+    // 2^33
+    long long x = 8589934592l;
+    // 2^31 - 1
+    long long y = 2147483647;
+
+    if(top) {
+        x = x - 1;
+    }
+
+    long long z = x/y;
+
+    if(z == 4){
+        // Should be reachable
+        assert(1);
+    }
+
+    assert(z > 2); //UNKNOWN
+}

tests/regression/27-inv_invariants/01-ints.c

@@ -21,12 +21,12 @@ int main() {
     assert(x == 2 && y == 4);
   if (x == 3 && y/x == 2) {
     assert(y == 6); // UNKNOWN!
-    assert(RANGE(y, 6, 8));
+    assert(RANGE(y, 6, 8)); // UNKNOWN
   }
   if (y/3 == -2)
-    assert(RANGE(y, -8, -6));
+    assert(RANGE(y, -8, -6)); // UNKNOWN
   if (y/-3 == -2)
-    assert(RANGE(y, 6, 8));
+    assert(RANGE(y, 6, 8)); // UNKNOWN
   if (y/x == 2 && x == 3)
     assert(x == 3); // TO-DO y == [6,8]; this does not work because CIL transforms this into two if-statements
   if (2+(3-x)*4/5 == 6 && 2*y >= x+5)
@@ -113,7 +113,7 @@ int main2() {
   if (x == three && y/x == two) {
     // y could for example also be 7
     assert(y == six);  // UNKNOWN!
-    assert(RANGE(y, 6, 8));
+    assert(RANGE(y, 6, 8)); // UNKNOWN
   }
   if (y/x == two && x == three)
     assert(x == three); // TO-DO y == six
@@ -124,9 +124,9 @@ int main2() {
     assert(x != two); // [two,four] -> [three,four] TO-DO x % two == one
 
   if (y/three == -two)
-    assert(RANGE(y, -8, -6));
+    assert(RANGE(y, -8, -6)); // UNKNOWN
   if (y/-three == -two)
-    assert(RANGE(y, 6, 8));
+    assert(RANGE(y, 6, 8)); // UNKNOWN
   if (y/x == two && x == three)
     assert(x == 3); // TO-DO y == [6,8]; this does not work because CIL transforms this into two if-statements
   if (two+(three-x)*four/five == six && two*y >= x+five)