Clean up interval div

Author: sim642

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

@@ -294,24 +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 (r, ov) =
-          let (n, p) = IArith.div x y in
-          norm ik (join_no_norm ik n p) (* normal join drops overflow info *)
-        in
-        if leq (of_int ik (Ints_t.zero) |> fst) (Some (y1,y2)) then
-          (top_of ik, ov)
-        else
-          (r, ov)
-        (* 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

@@ -363,25 +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) as y) = begin
-      let top_of ik = top_of ik |> List.hd in
-      let r =
-        let (n, p) = IArith.div x y in
-        List.filter_map Fun.id [n; p]
-      in
-      if leq (of_int ik (Ints_t.zero) |> fst) ([(y1,y2)]) then
-        [top_of ik]
-      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 *)
-      (* 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_concat_with_norm interval_div ik x y
+    let rec interval_div x y =
+      if leq (of_int ik Ints_t.zero |> fst) [y] then
+        top_of ik (* TODO: should somehow handle overflow like normal intervals? *)
+      else (
+        let (neg, pos) = IArith.div x y in
+        List.filter_map Fun.id [neg; pos] (* 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,17 +361,6 @@ 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)
-
   let div (a, b) (c, d) =
     let pos =
       if Ints_t.(compare one d) <= 0 then