Interval: Do not compute with top.

Arithmetic operations on the current top representation of the interval
domain now return top if any of the operands is top. The reason is that
the top value [-2^31,2^31-1] is too "narrow" to represent some concrete
values. Thus computing with it leads to spurious, unsound results.

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,6 +361,7 @@ struct
         meet (bit Int64.rem x y) range
 
   let mul 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)))
@@ -358,6 +372,7 @@ struct
                     (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)))