diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index fbbfb7674..715d83955 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -592,6 +592,14 @@ struct let is_symbolic : t -> bool = fun (lb, ub) -> Bound.is_symbolic lb || Bound.is_symbolic ub + let is_ge_zero : t -> bool + = fun (lb, _) -> + if lb <> Bound.Bot then Bound.le Bound.zero lb else false + + let is_le_zero : t -> bool + = fun (_, ub) -> + if ub <> Bound.Bot then Bound.le ub Bound.zero else false + let neg : t -> t = fun (l, u) -> let l' = Option.value ~default:Bound.MInf (Bound.neg u) in @@ -653,8 +661,13 @@ struct let mod_sem : t -> t -> t = fun x y -> match is_const x, is_const y with - | Some n, Some m -> if Int.equal m 0 then x else of_int (n mod m) - | _, Some m -> (Bound.of_int (-m), Bound.of_int m) + | _, Some 0 -> x + | Some n, Some m -> of_int (n mod m) + | _, Some m -> + let abs_m = abs m in + if is_ge_zero x then (Bound.zero, Bound.of_int (abs_m - 1)) else + if is_le_zero x then (Bound.of_int (-abs_m + 1), Bound.zero) else + (Bound.of_int (-abs_m + 1), Bound.of_int (abs_m - 1)) | _, None -> top (* x << [-1,-1] does nothing. *) diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index 426dc9f50..f69042a29 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -12,14 +12,26 @@ void modulo_signed_Bad(int i) { arr[i % 5] = 123; } -void modulo_signed_Good_FP(int i) { +void modulo_signed_Good(int i) { char arr[5]; if (i >= 0) { arr[i % 5] = 123; } } -void modulo_signed_Good2_FP(int i) { +void modulo_signed_neg_Bad(int i) { + char arr[5]; + arr[i % -5] = 123; +} + +void modulo_signed_neg_Good(int i) { + char arr[5]; + if (i >= 0) { + arr[i % -5] = 123; + } +} + +void modulo_signed_Good2(int i) { char arr[5]; int j = i % 5; if (j >= 0) { diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index b6b798214..522e4c97e 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -1,7 +1,6 @@ -codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN, [Offset: [-5, 5] Size: [5, 5]] -codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Good2_FP, 4, BUFFER_OVERRUN, [Offset: [0, 5] Size: [5, 5]] -codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Good_FP, 3, BUFFER_OVERRUN, [Offset: [-5, 5] Size: [5, 5]] -codetoanalyze/c/bufferoverrun/arith.c, modulo_unsigned_Good_FP, 2, BUFFER_OVERRUN, [Offset: [-5, 5] Size: [5, 5]] +codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN, [Offset: [-4, 4] Size: [5, 5]] +codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN, [Offset: [-4, 4] Size: [5, 5]] +codetoanalyze/c/bufferoverrun/arith.c, modulo_unsigned_Good_FP, 2, BUFFER_OVERRUN, [Offset: [-4, 4] Size: [5, 5]] codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN, [Offset: [3xs$0 + 1, 3xs$1 + 1] Size: [3xs$0 + 1, 3xs$1 + 1]] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, []