Merge pull request #1804 from goblint/issue-1803

Fix interval division

Author: sim642

src/cdomain/value/cdomains/int/intervalDomain.ml

@@ -64,10 +64,12 @@ struct
     | Some _, None -> false
     | Some (x1,x2), Some (y1,y2) -> Ints_t.compare x1 y1 >= 0 && Ints_t.compare x2 y2 <= 0
 
-  let join ik (x:t) y =
+  let join_no_norm ik (x:t) y =
     match x, y with
     | None, z | z, None -> z
-    | Some (x1,x2), Some (y1,y2) -> norm ik @@ Some (Ints_t.min x1 y1, Ints_t.max x2 y2) |> fst
+    | Some (x1,x2), Some (y1,y2) -> Some (Ints_t.min x1 y1, Ints_t.max x2 y2)
+
+  let join ik (x:t) y = norm ik @@ join_no_norm ik x y |> fst
 
   let meet ik (x:t) y =
     match x, y with
@@ -292,16 +294,13 @@ struct
     match x, y with
     | None, None -> (bot (),{underflow=false; overflow=false})
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
-    | (Some (x1,x2) as x), (Some (y1,y2) as y) ->
-      begin
-        let is_zero v = Ints_t.compare v Ints_t.zero = 0 in
-        match y1, y2 with
-        | l, u when is_zero l && is_zero u -> (top_of ik,{underflow=false; overflow=false})
-        | l, _ when is_zero l              -> div ik (Some (x1,x2)) (Some (Ints_t.one,y2))
-        | _, u when is_zero u              -> div ik (Some (x1,x2)) (Some (y1, Ints_t.(neg one)))
-        | _ when leq (of_int ik (Ints_t.zero) |> fst) (Some (y1,y2)) -> (top_of ik,{underflow=false; overflow=false})
-        | _ -> binary_op_with_norm IArith.div ik x y
-      end
+    | Some x, Some y ->
+      let (neg, pos) = IArith.div x y in
+      let (r, ov) = norm ik (join_no_norm ik neg pos) in (* normal join drops overflow info *)
+      if leq (of_int ik Ints_t.zero |> fst) (Some y) then
+        (top_of ik, ov)
+      else
+        (r, ov)
 
   let ne ik x y =
     match x, y with

src/cdomain/value/cdomains/int/intervalSetDomain.ml

@@ -173,7 +173,12 @@ struct
   let binary_op_with_norm op (ik:ikind) (x: t) (y: t) : t*overflow_info = match x, y with
     | [], _ -> ([],{overflow=false; underflow=false})
     | _, [] -> ([],{overflow=false; underflow=false})
-    | _, _ -> norm_intvs ik @@ List.concat_map (fun (x,y) -> [op x y]) (BatList.cartesian_product x y)
+    | _, _ -> norm_intvs ik @@ List.map (fun (x,y) -> op x y) (BatList.cartesian_product x y)
+
+  let binary_op_concat_with_norm op (ik:ikind) (x: t) (y: t) : t*overflow_info = match x, y with
+    | [], _ -> ([],{overflow=false; underflow=false})
+    | _, [] -> ([],{overflow=false; underflow=false})
+    | _, _ -> norm_intvs ik @@ List.concat_map (fun (x,y) -> op x y) (BatList.cartesian_product x y)
 
   let binary_op_with_ovc (x: t) (y: t) op : t*overflow_info = match x, y with
     | [], _ -> ([],{overflow=false; underflow=false})
@@ -187,7 +192,7 @@ struct
 
   let unary_op_with_norm op (ik:ikind) (x: t) = match x with
     | [] -> ([],{overflow=false; underflow=false})
-    | _ -> norm_intvs ik @@ List.concat_map (fun x -> [op x]) x
+    | _ -> norm_intvs ik @@ List.map op x
 
   let rec leq (xs: t) (ys: t) =
     let leq_interval (al, au) (bl, bu) = al >=. bl && au <=. bu in
@@ -358,17 +363,15 @@ struct
   let neg ?no_ov = unary_op_with_norm IArith.neg
 
   let div ?no_ov ik x y =
-    let rec interval_div x (y1, y2) = begin
-      let top_of ik = top_of ik |> List.hd in
-      let is_zero v = v =. Ints_t.zero in
-      match y1, y2 with
-      | l, u when is_zero l && is_zero u -> top_of ik
-      | l, _ when is_zero l              -> interval_div x (Ints_t.one,y2)
-      | _, u when is_zero u              -> interval_div x (y1, Ints_t.(neg one))
-      | _ when leq (of_int ik (Ints_t.zero) |> fst) ([(y1,y2)]) -> top_of ik
-      | _ -> IArith.div x (y1, y2)
-    end
-    in binary_op_with_norm interval_div ik x y
+    let rec interval_div x y =
+      let (neg, pos) = IArith.div x y in
+      let r = List.filter_map Fun.id [neg; pos] in
+      if leq (of_int ik Ints_t.zero |> fst) [y] then
+        top_of ik @ r (* keep r because they might overflow, but top doesn't *)
+      else
+        r (* should always be singleton, because if there's a negative and a positive side, then it must've included zero, which is already handled by previous case *)
+    in
+    binary_op_concat_with_norm interval_div ik x y
 
   let rem ik x y =
     let interval_rem (x, y) =

src/cdomain/value/cdomains/intDomain0.ml

@@ -361,16 +361,28 @@ module IntervalArith (Ints_t : IntOps.IntOps) = struct
     let y2p = Ints_t.shift_left Ints_t.one y2 in
     mul (x1, x2) (y1p, y2p)
 
-  let div (x1, x2) (y1, y2) =
-    let x1y1n = (Ints_t.div x1 y1) in
-    let x1y2n = (Ints_t.div x1 y2) in
-    let x2y1n = (Ints_t.div x2 y1) in
-    let x2y2n = (Ints_t.div x2 y2) in
-    let x1y1p = (Ints_t.div x1 y1) in
-    let x1y2p = (Ints_t.div x1 y2) in
-    let x2y1p = (Ints_t.div x2 y1) in
-    let x2y2p = (Ints_t.div x2 y2) in
-    (min4 x1y1n x1y2n x2y1n x2y2n, max4 x1y1p x1y2p x2y1p x2y2p)
+  (** Divide mathematical intervals.
+      Excludes 0 from denominator - must be handled as desired by caller.
+
+      @return negative and positive denominator cases separately, if they exist.
+
+      @see <https://mine.perso.lip6.fr/publi/article-mine-FTiPL17.pdf> Miné, A. Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation. Figure 4.6. *)
+  let div (a, b) (c, d) =
+    let pos =
+      if Ints_t.(compare one d) <= 0 then
+        let c = Ints_t.(max one c) in
+        Some (Ints_t.(min (div a c) (div a d), max (div b c) (div b d)))
+      else
+        None
+    in
+    let neg =
+      if Ints_t.(compare c zero) < 0 then
+        let d = Ints_t.(min d (neg one)) in
+        Some (Ints_t.(min (div b c) (div b d), max (div a c) (div a d)))
+      else
+        None
+    in
+    (neg, pos)
 
   let add (x1, x2) (y1, y2) = (Ints_t.add x1 y1, Ints_t.add x2 y2)
   let sub (x1, x2) (y1, y2) = (Ints_t.sub x1 y2, Ints_t.sub x2 y1)

tests/regression/39-signed-overflows/15-div-minus-1.c

@@ -0,0 +1,12 @@
+// PARAM: --enable ana.int.interval
+#include <limits.h>
+
+int main() {
+    int bad = INT_MIN / -1; // WARN (overflow)
+    int x, y;
+    bad = x / y; // WARN (div by zero and overflow, distinguished in cram test)
+    if (y != 0) {
+        bad = x / y; // WARN (overflow)
+    }
+    return 0;
+}

tests/regression/39-signed-overflows/15-div-minus-1.t

@@ -0,0 +1,20 @@
+  $ goblint --enable warn.deterministic --enable ana.int.interval 15-div-minus-1.c
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (15-div-minus-1.c:5:9-5:26)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (15-div-minus-1.c:7:5-7:16)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (15-div-minus-1.c:9:9-9:20)
+  [Warning][Integer > DivByZero][CWE-369] Second argument of division might be zero (15-div-minus-1.c:7:5-7:16)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 6
+    dead: 0
+    total lines: 6
+
+  $ goblint --enable warn.deterministic --enable ana.int.interval_set 15-div-minus-1.c
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (15-div-minus-1.c:5:9-5:26)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (15-div-minus-1.c:7:5-7:16)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (15-div-minus-1.c:9:9-9:20)
+  [Warning][Integer > DivByZero][CWE-369] Second argument of division might be zero (15-div-minus-1.c:7:5-7:16)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 6
+    dead: 0
+    total lines: 6
+

tests/regression/39-signed-overflows/dune

@@ -0,0 +1,2 @@
+(cram
+ (deps (glob_files *.c)))