From 63df7c7da1b30e359193b41d3952d39c50b174c6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 21 May 2026 17:38:02 +0300 Subject: [PATCH] Add option sem.int.div-by-zero --- src/cdomain/value/cdomains/int/bitfieldDomain.ml | 2 ++ src/cdomain/value/cdomains/int/congruenceDomain.ml | 3 ++- src/cdomain/value/cdomains/int/defExcDomain.ml | 2 +- src/cdomain/value/cdomains/int/enumsDomain.ml | 6 +++--- src/cdomain/value/cdomains/int/intervalDomain.ml | 3 ++- src/cdomain/value/cdomains/int/intervalSetDomain.ml | 5 +++-- src/config/options.schema.json | 8 ++++++++ 7 files changed, 21 insertions(+), 8 deletions(-) diff --git a/src/cdomain/value/cdomains/int/bitfieldDomain.ml b/src/cdomain/value/cdomains/int/bitfieldDomain.ml index ab20be9b4d..19d36d4245 100644 --- a/src/cdomain/value/cdomains/int/bitfieldDomain.ml +++ b/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) diff --git a/src/cdomain/value/cdomains/int/congruenceDomain.ml b/src/cdomain/value/cdomains/int/congruenceDomain.ml index 0752b765f0..c9f6b78b4f 100644 --- a/src/cdomain/value/cdomains/int/congruenceDomain.ml +++ b/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) diff --git a/src/cdomain/value/cdomains/int/defExcDomain.ml b/src/cdomain/value/cdomains/int/defExcDomain.ml index f6c60c9e62..c958c3c147 100644 --- a/src/cdomain/value/cdomains/int/defExcDomain.ml +++ b/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 *) diff --git a/src/cdomain/value/cdomains/int/enumsDomain.ml b/src/cdomain/value/cdomains/int/enumsDomain.ml index bdf4567611..cd8211e1b4 100644 --- a/src/cdomain/value/cdomains/int/enumsDomain.ml +++ b/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 diff --git a/src/cdomain/value/cdomains/int/intervalDomain.ml b/src/cdomain/value/cdomains/int/intervalDomain.ml index c0fc61db38..3fe2221bce 100644 --- a/src/cdomain/value/cdomains/int/intervalDomain.ml +++ b/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) diff --git a/src/cdomain/value/cdomains/int/intervalSetDomain.ml b/src/cdomain/value/cdomains/int/intervalSetDomain.ml index 08b5c27aa3..ea00f4ccc9 100644 --- a/src/cdomain/value/cdomains/int/intervalSetDomain.ml +++ b/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 diff --git a/src/config/options.schema.json b/src/config/options.schema.json index c002dfa88e..eddec5229e 100644 --- a/src/config/options.schema.json +++ b/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