diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 030c45149..e5bdfd71f 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -733,8 +733,18 @@ module Bound = struct let mult_const_u = mult_const Symb.BoundEnd.UpperBound - let div_const : t -> NonZeroInt.t -> t option = - fun x n -> + let overapprox_minmax_div_const x (n : NonZeroInt.t) = + let c = if NonZeroInt.is_positive n then big_int_ub_of_minmax x else big_int_lb_of_minmax x in + Option.map c ~f:(fun c -> Z.(c / (n :> Z.t))) + + + let underapprox_minmax_div_const x (n : NonZeroInt.t) = + let c = if NonZeroInt.is_positive n then big_int_lb_of_minmax x else big_int_ub_of_minmax x in + Option.map c ~f:(fun c -> Z.(c / (n :> Z.t))) + + + let div_const : Symb.BoundEnd.t -> t -> NonZeroInt.t -> t option = + fun bound_end x n -> match x with | MInf -> Some (if NonZeroInt.is_positive n then MInf else PInf) @@ -746,10 +756,23 @@ module Bound = struct Some (Linear (Z.(c / (n :> Z.t)), x'')) | exception NonZeroInt.DivisionNotExact -> None ) + | MinMax _ -> + let c = + match bound_end with + | Symb.BoundEnd.LowerBound -> + underapprox_minmax_div_const x n + | Symb.BoundEnd.UpperBound -> + overapprox_minmax_div_const x n + in + Option.map c ~f:of_big_int | _ -> None + let div_const_l = div_const Symb.BoundEnd.LowerBound + + let div_const_u = div_const Symb.BoundEnd.UpperBound + let get_symbols : t -> Symb.Symbol.t list = function | MInf | PInf -> [] diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index 9836f16df..497709503 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -99,7 +99,9 @@ module Bound : sig val neg : t -> t - val div_const : t -> Ints.NonZeroInt.t -> t sexp_option + val div_const_l : t -> Ints.NonZeroInt.t -> t sexp_option + + val div_const_u : t -> Ints.NonZeroInt.t -> t sexp_option val get_symbols : t -> Symb.Symbol.t list diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index aed79c446..d738ace87 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -611,12 +611,12 @@ module ItvPure = struct if NonZeroInt.is_one n then itv else if NonZeroInt.is_minus_one n then neg itv else if NonZeroInt.is_positive n then - let l' = Option.value ~default:Bound.MInf (Bound.div_const l n) in - let u' = Option.value ~default:Bound.PInf (Bound.div_const u n) in + let l' = Option.value ~default:Bound.MInf (Bound.div_const_l l n) in + let u' = Option.value ~default:Bound.PInf (Bound.div_const_u u n) in (l', u') else - let l' = Option.value ~default:Bound.MInf (Bound.div_const u n) in - let u' = Option.value ~default:Bound.PInf (Bound.div_const l n) in + let l' = Option.value ~default:Bound.MInf (Bound.div_const_l u n) in + let u' = Option.value ~default:Bound.PInf (Bound.div_const_u l n) in (l', u') diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index c166f294c..64eb9638b 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -292,3 +292,17 @@ void unsigned_prune_gt(unsigned int x, unsigned int y) { } void call_unsigned_prune_gt_Good() { unsigned_prune_gt(0, 3); } + +void minmax_div_const_Good(int n) { + int a[9]; + if (0 < n && n < 65) { + int x = a[n / 8]; + } +} + +void minmax_div_const_Bad(int n) { + int a[7]; + if (0 < n && n < 65) { + int x = a[n / 8]; + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 4dfa06150..651a4d397 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -8,6 +8,7 @@ codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 4 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (-2000000000 - 2000000000):signed32] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] +codetoanalyze/c/bufferoverrun/arith.c, minmax_div_const_Bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [0, 8] Size: 7] codetoanalyze/c/bufferoverrun/arith.c, minus_minimum_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (0 - -9223372036854775808):signed64] codetoanalyze/c/bufferoverrun/arith.c, minus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: unknown_uint,Assignment,Binop: ([0, +oo] - 1):unsigned64] codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [-4, 4] Size: 5]