Add option sem.int.div-by-zero

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

@@ -540,6 +540,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
 
 
   let div ?no_ov ik (z1, o1) (z2, o2) =
+    (* TODO: handle sem.int.div-by-zero option *)
     if o2 = Ints_t.zero then
       (top_of ik, {underflow=false; overflow=false})
     else
@@ -558,6 +559,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
       (norm ~ov:overflow ik res, {underflow=false; overflow=overflow})
 
   let rem ik (z1, o1) (z2, o2) =
+    (* TODO: handle sem.int.div-by-zero option *)
     if o2 = Ints_t.zero then top_of ik else
     if BArith.is_const (z1, o1) && BArith.is_const (z2, o2) then
       let tmp = o1 %: o2 in (!:tmp, tmp)

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

@@ -389,6 +389,7 @@ struct
     | None, None -> bot()
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
     | Some (c1, m1), Some(c2, m2) ->
+      (* TODO: handle sem.int.div-by-zero option *)
       if m2 =: Z.zero then
         if (c2 |: m1) && (c1 %: c2 =: Z.zero || m1 =: Z.zero || not (Cil.isSigned ik)) then
           Some (c1 %: c2, Z.zero)
@@ -405,7 +406,7 @@ struct
     match x,y with
     | None, None -> bot ()
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
-    | _, x when leq zero x -> top ()
+    | _, x when leq zero x -> top () (* TODO: handle sem.int.div-by-zero option *)
     | Some(c1, m1), Some(c2, m2) when not no_ov && m2 =: Z.zero && c2 =: Z.neg Z.one -> top ()
     | Some(c1, m1), Some(c2, m2) when m1 =: Z.zero && m2 =: Z.zero -> Some (c1 /: c2, Z.zero)
     | Some(c1, m1), Some(c2, m2) when m2 =: Z.zero && c2 |: m1 && c2 |: c1 -> Some (c1 /: c2, m1 /: c2)

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

@@ -363,7 +363,7 @@ struct
       | `Excluded _, `Excluded _ -> top_overflow ()
       (* The good case: *)
       | `Definite x, `Definite y ->
-        (try `Definite (f x y) with | Division_by_zero -> top_overflow ())
+        (try `Definite (f x y) with | Division_by_zero -> if GobConfig.get_string "sem.int.div-by-zero" = "assume_none" then `Bot else top_overflow ())
       | `Bot, `Bot -> `Bot
       | _ ->
         (* If only one of them is bottom, we raise an exception that eval_rv will catch *)

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

@@ -202,7 +202,7 @@ module Enums : S with type int_t = Z.t = struct
         | _,_ -> top_of ikind)
 
   let lift2 f ikind a b =
-    try lift2 f ikind a b with Division_by_zero -> top_of ikind
+    try lift2 f ikind a b with Division_by_zero -> if GobConfig.get_string "sem.int.div-by-zero" = "assume_none" then bot () else top_of ikind
 
   let neg ?no_ov = lift1 Z.neg
   let add ?no_ov ikind a b =
@@ -221,8 +221,8 @@ module Enums : S with type int_t = Z.t = struct
 
   let div ?no_ov ikind a b = match a, b with
     | x,Inc one when BISet.is_singleton one && BISet.choose one = Z.one -> x
-    | _,Inc zero when BISet.is_singleton zero && BISet.choose zero = Z.zero -> top_of ikind
-    | Inc zero,_ when BISet.is_singleton zero && BISet.choose zero = Z.zero -> a
+    | _,Inc zero when BISet.is_singleton zero && BISet.choose zero = Z.zero -> if GobConfig.get_string "sem.int.div-by-zero" = "assume_none" then bot () else top_of ikind
+    | Inc zero,_ when BISet.is_singleton zero && BISet.choose zero = Z.zero -> a (* TODO: handle sem.int.div-by-zero option *)
     | x,y -> lift2 Z.div ikind x y
 
   let rem = lift2 Z.rem

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

@@ -348,6 +348,7 @@ struct
          * This range is [0, min xu b] if x is positive, and [max xl -b, min xu b] if x can be negative.
          * The precise bound b is one smaller than the maximum bound. Negative y give the same result as positive. *)
         let pos x = if Ints_t.compare x Ints_t.zero < 0 then Ints_t.neg x else x in
+        (* TODO: handle sem.int.div-by-zero option *)
         let b = Ints_t.sub (Ints_t.max (pos yl) (pos yu)) Ints_t.one in
         let range = if Ints_t.compare xl Ints_t.zero>= 0 then Some (Ints_t.zero, Ints_t.min xu b) else Some (Ints_t.max xl (Ints_t.neg b), Ints_t.min (Ints_t.max (pos xl) (pos xu)) b) in
         meet ik (bit (fun _ik -> Ints_t.rem) ik x y) range
@@ -359,7 +360,7 @@ struct
     | 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
+      if leq (of_int ik Ints_t.zero |> fst) (Some y) && GobConfig.get_string "sem.int.div-by-zero" = "assume_top" then
         (top_of ik, ov)
       else
         (r, ov)

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

@@ -437,10 +437,10 @@ struct
     let 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
+      if leq (of_int ik Ints_t.zero |> fst) [y] && GobConfig.get_string "sem.int.div-by-zero" = "assume_top" 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 *)
+        r (* If sem.int.div-by-zero is assume_top, then 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
 
@@ -452,6 +452,7 @@ struct
         let (xl, xu) = x in let (yl, yu) = y in
         let pos x = if x <. Ints_t.zero then Ints_t.neg x else x in
         let b = (Ints_t.max (pos yl) (pos yu)) -. Ints_t.one in
+        (* TODO: handle sem.int.div-by-zero option *)
         let range = if xl >=. Ints_t.zero then (Ints_t.zero, Ints_t.min xu b) else (Ints_t.max xl (Ints_t.neg b), Ints_t.min (Ints_t.max (pos xl) (pos xu)) b) in
         meet ik (bit Ints_t.rem ik (x, y)) [range]
     in

src/config/options.schema.json

@@ -1633,6 +1633,14 @@
               "type": "string",
               "enum": ["assume_top", "assume_none", "assume_wraparound"],
               "default": "assume_top"
+            },
+            "div-by-zero": {
+              "title": "sem.int.div-by-zero",
+              "description":
+                "How to handle division by zero. Values: 'assume_top' (default): Assume division by zero results in a top value; 'assume_none': Assume program is free of division by zero",
+              "type": "string",
+              "enum": ["assume_top", "assume_none"],
+              "default": "assume_top"
             }
           },
           "additionalProperties": false