diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 500376372..8c3c2a3c2 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -198,6 +198,8 @@ module Bound = struct let eval_big_int x i1 i2 = match x with Plus -> Z.(i1 + i2) | Minus -> Z.(i1 - i2) + let eval_neg_if_minus x i = match x with Plus -> i | Minus -> Z.neg i + let pp ~need_plus : F.formatter -> t -> unit = fun fmt -> function | Plus -> @@ -306,10 +308,10 @@ module Bound = struct let big_int_ub_of_minmax = function | MinMax (c, Plus, Min, d, _) -> Some Z.(c + d) - | MinMax (c, Minus, Max, d, s) when Symb.Symbol.is_unsigned s -> - Some Z.(min c (c - d)) | MinMax (c, Minus, Max, d, _) -> Some Z.(c - d) + | MinMax (c, Minus, Min, _, s) when Symb.Symbol.is_unsigned s -> + Some c | MinMax _ -> None | MInf | PInf | Linear _ -> @@ -317,12 +319,12 @@ module Bound = struct let big_int_lb_of_minmax = function - | MinMax (c, Plus, Max, d, s) when Symb.Symbol.is_unsigned s -> - Some Z.(max c (c + d)) | MinMax (c, Plus, Max, d, _) -> Some Z.(c + d) | MinMax (c, Minus, Min, d, _) -> Some Z.(c - d) + | MinMax (c, Plus, Min, _, s) when Symb.Symbol.is_unsigned s -> + Some c | MinMax _ -> None | MInf | PInf | Linear _ -> @@ -446,23 +448,30 @@ module Bound = struct let xcompare = PartialOrder.of_le ~le - let remove_max_int : t -> t = - fun x -> - match x with - | MinMax (c, Plus, Max, _, s) -> - Linear (c, SymLinear.singleton_one s) - | MinMax (c, Minus, Min, _, s) -> - Linear (c, SymLinear.singleton_minus_one s) + let is_const : t -> bool = function + | Linear (_, se) when SymLinear.is_zero se -> + true | _ -> - x + false - let rec lb : default:t -> t -> t -> t = - fun ~default x y -> - if le x y then x - else if le y x then y + let neg : t -> t = function + | MInf -> + PInf + | PInf -> + MInf + | Linear (c, x) -> + Linear (Z.neg c, SymLinear.neg x) + | MinMax (c, sign, min_max, d, x) -> + mk_MinMax (Z.neg c, Sign.neg sign, min_max, d, x) + + + let exact_min : otherwise:(t -> t -> t) -> t -> t -> t = + fun ~otherwise b1 b2 -> + if le b1 b2 then b1 + else if le b2 b1 then b2 else - match (x, y) with + match (b1, b2) with | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2 -> mk_MinMax (c2, Plus, Min, Z.(c1 - c2), SymLinear.get_one_symbol x2) | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_one_symbol x1 && SymLinear.is_zero x2 -> @@ -473,70 +482,168 @@ module Bound = struct | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_mone_symbol x1 && SymLinear.is_zero x2 -> mk_MinMax (c1, Minus, Max, Z.(c1 - c2), SymLinear.get_mone_symbol x1) - | MinMax (c1, Plus, Min, d1, s), Linear (c2, se) - | Linear (c2, se), MinMax (c1, Plus, Min, d1, s) - when SymLinear.is_zero se -> - mk_MinMax (c1, Plus, Min, Z.(min d1 (c2 - c1)), s) - | MinMax (c1, Plus, Max, _, s), Linear (c2, se) - | Linear (c2, se), MinMax (c1, Plus, Max, _, s) + | MinMax (c1, (Plus as sign), (Min as minmax), _, s), Linear (c2, se) + | Linear (c2, se), MinMax (c1, (Plus as sign), (Min as minmax), _, s) + | MinMax (c1, (Minus as sign), (Max as minmax), _, s), Linear (c2, se) + | Linear (c2, se), MinMax (c1, (Minus as sign), (Max as minmax), _, s) when SymLinear.is_zero se -> - mk_MinMax (c1, Plus, Min, Z.(c2 - c1), s) - | MinMax (c1, Minus, Min, _, s), Linear (c2, se) - | Linear (c2, se), MinMax (c1, Minus, Min, _, s) - when SymLinear.is_zero se -> - mk_MinMax (c1, Minus, Max, Z.(c1 - c2), s) - | MinMax (c1, Minus, Max, d1, s), Linear (c2, se) - | Linear (c2, se), MinMax (c1, Minus, Max, d1, s) - when SymLinear.is_zero se -> - mk_MinMax (c1, Minus, Max, Z.(max d1 (c1 - c2)), s) - | MinMax (_, Plus, Min, _, _), MinMax (_, Plus, Max, _, _) - | MinMax (_, Plus, Min, _, _), MinMax (_, Minus, Min, _, _) - | MinMax (_, Minus, Max, _, _), MinMax (_, Plus, Max, _, _) - | MinMax (_, Minus, Max, _, _), MinMax (_, Minus, Min, _, _) -> - lb ~default x (remove_max_int y) - | MinMax (_, Plus, Max, _, _), MinMax (_, Plus, Min, _, _) - | MinMax (_, Minus, Min, _, _), MinMax (_, Plus, Min, _, _) - | MinMax (_, Plus, Max, _, _), MinMax (_, Minus, Max, _, _) - | MinMax (_, Minus, Min, _, _), MinMax (_, Minus, Max, _, _) -> - lb ~default (remove_max_int x) y - | MinMax (c1, Plus, Max, d1, _), MinMax (c2, Plus, Max, d2, _) -> - Linear (Z.(min (c1 + d1) (c2 + d2)), SymLinear.zero) - | _, _ -> - default - - - (** underapproximation of min b1 b2 *) - let min_l b1 b2 = lb ~default:MInf b1 b2 - - (** overapproximation of min b1 b2 *) - let min_u b1 b2 = - lb - ~default: - (* When the result is not representable, our best effort is to return the first argument. Any other deterministic heuristics would work too. *) - b1 b1 b2 - - - let ub : default:t -> t -> t -> t = - fun ~default x y -> - if le x y then y - else if le y x then x - else - match (x, y) with - | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2 -> - mk_MinMax (c2, Plus, Max, Z.(c1 - c2), SymLinear.get_one_symbol x2) - | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_one_symbol x1 && SymLinear.is_zero x2 -> - mk_MinMax (c1, Plus, Max, Z.(c2 - c1), SymLinear.get_one_symbol x1) - | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_mone_symbol x2 - -> - mk_MinMax (c2, Minus, Min, Z.(c2 - c1), SymLinear.get_mone_symbol x2) - | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_mone_symbol x1 && SymLinear.is_zero x2 - -> - mk_MinMax (c1, Minus, Min, Z.(c1 - c2), SymLinear.get_mone_symbol x1) - | _, _ -> - default + let d = Sign.eval_neg_if_minus sign Z.(c2 - c1) in + mk_MinMax (c1, sign, minmax, d, s) + | MinMax (c1, (Minus as sign), (Max as minmax), d1, s1), MinMax (c2, Minus, Max, d2, s2) + | MinMax (c1, (Plus as sign), (Min as minmax), d1, s1), MinMax (c2, Plus, Min, d2, s2) + when Symb.Symbol.equal s1 s2 -> + let v1 = Sign.eval_big_int sign c1 d1 in + let v2 = Sign.eval_big_int sign c2 d2 in + let c = Z.min c1 c2 in + let v = MinMax.eval_big_int minmax v1 v2 in + let d = Sign.eval_neg_if_minus sign Z.(v - c) in + mk_MinMax (c, sign, minmax, d, s1) + | b1, b2 -> + otherwise b1 b2 + + + let rec underapprox_min b1 b2 = + exact_min b1 b2 ~otherwise:(fun b1 b2 -> + match (b1, b2) with + | MinMax (c1, sign, _, d1, _s), Linear (_c2, se) + | Linear (_c2, se), MinMax (c1, sign, _, d1, _s) + when SymLinear.is_zero se -> + Linear (Sign.eval_big_int sign c1 d1, SymLinear.zero) + (* + There is no best abstraction, we could also use: + For Plus, Max: mk_MinMax (c1, Plus, Min, Z.(c2 - c1), s) + For Minus, Min: mk_MinMax (c1, Minus, Max, Z.(c1 - c2), s) + *) + | MinMax (_, Minus, Max, _, _), MinMax (_, Plus, Min, _, _) + | MinMax (_, Plus, Min, _, _), MinMax (_, Minus, Max, _, _) -> + fallback_underapprox_min b1 b2 + | MinMax (c1, (Plus as sign1), Max, d1, _), MinMax (c2, (Minus as sign2), Min, d2, _) + | MinMax (c1, (Minus as sign1), Min, d1, _), MinMax (c2, (Plus as sign2), Max, d2, _) -> + let v1 = Sign.eval_big_int sign1 c1 d1 in + let v2 = Sign.eval_big_int sign2 c2 d2 in + Linear (Z.min v1 v2, SymLinear.zero) + | MinMax (c1, (Plus as sign), (Max as minmax), d1, s1), MinMax (c2, Plus, Max, d2, s2) + | MinMax (c1, (Minus as sign), (Min as minmax), d1, s1), MinMax (c2, Minus, Min, d2, s2) + when Symb.Symbol.equal s1 s2 -> + let v1 = Sign.eval_big_int sign c1 d1 in + let v2 = Sign.eval_big_int sign c2 d2 in + let v = Z.min v1 v2 in + let c = Z.min c1 c2 in + let d = Sign.eval_neg_if_minus sign Z.(v - c) in + mk_MinMax (c, sign, minmax, d, s1) + | ( MinMax (c1, (Plus as sign1), (Min as minmax1), d1, s1) + , MinMax (c2, (Plus as sign2), Max, d2, s2) ) + | ( MinMax (c2, (Plus as sign2), Max, d2, s2) + , MinMax (c1, (Plus as sign1), (Min as minmax1), d1, s1) ) + | ( MinMax (c1, (Minus as sign1), (Max as minmax1), d1, s1) + , MinMax (c2, (Minus as sign2), Min, d2, s2) ) + | ( MinMax (c2, (Minus as sign2), Min, d2, s2) + , MinMax (c1, (Minus as sign1), (Max as minmax1), d1, s1) ) + | ( MinMax (c1, (Minus as sign1), (Max as minmax1), d1, s1) + , MinMax (c2, (Plus as sign2), Max, d2, s2) ) + | ( MinMax (c2, (Plus as sign2), (Max as minmax1), d2, s2) + , MinMax (c1, (Minus as sign1), Max, d1, s1) ) + | ( MinMax (c1, (Plus as sign1), (Min as minmax1), d1, s1) + , MinMax (c2, (Minus as sign2), Min, d2, s2) ) + | ( MinMax (c2, (Minus as sign2), (Min as minmax1), d2, s2) + , MinMax (c1, (Plus as sign1), Min, d1, s1) ) + when Symb.Symbol.equal s1 s2 -> + let v1 = Sign.eval_big_int sign1 c1 d1 in + let v2 = Sign.eval_big_int sign2 c2 d2 in + let v = Z.min v1 v2 in + let d = Sign.eval_neg_if_minus sign1 Z.(v - c1) in + mk_MinMax (c1, sign1, minmax1, d, s1) + | b1, b2 -> + fallback_underapprox_min b1 b2 ) + + + and fallback_underapprox_min b1 b2 = + match big_int_lb b2 with + | Some v2 when not (is_const b2) -> + underapprox_min b1 (Linear (v2, SymLinear.zero)) + | _ -> ( + match big_int_lb b1 with + | Some v1 when not (is_const b1) -> + underapprox_min (Linear (v1, SymLinear.zero)) b2 + | _ -> + MInf ) + + + let overapprox_min original_b1 b2 = + let rec overapprox_min b1 b2 = + exact_min b1 b2 ~otherwise:(fun b1 b2 -> + match (b1, b2) with + | ( MinMax (c1, (Minus as sign1), (Max as minmax1), d1, s1) + , MinMax (c2, (Plus as sign2), Min, d2, s2) ) + | ( MinMax (c1, (Plus as sign1), (Min as minmax1), d1, s1) + , MinMax (c2, (Minus as sign2), Max, d2, s2) ) + when Symb.Symbol.equal s1 s2 -> + let v1 = Sign.eval_big_int sign1 c1 d1 in + let v2 = Sign.eval_big_int sign2 c2 d2 in + let vmeet = Z.(shift_right (c1 + c2 + one) 1) in + let v = Z.(min vmeet (min v1 v2)) in + let d = Sign.eval_neg_if_minus sign1 Z.(v - c1) in + mk_MinMax (c1, sign1, minmax1, d, s1) + | MinMax (c1, (Minus as sign1), Max, d1, s1), MinMax (c2, (Plus as sign2), Min, d2, s2) + | MinMax (c1, (Minus as sign1), Min, d1, s1), MinMax (c2, (Plus as sign2), Max, d2, s2) + | MinMax (c1, (Plus as sign1), Min, d1, s1), MinMax (c2, (Minus as sign2), Max, d2, s2) + | MinMax (c1, (Plus as sign1), Max, d1, s1), MinMax (c2, (Minus as sign2), Min, d2, s2) + when Symb.Symbol.equal s1 s2 -> + let v1 = Sign.eval_big_int sign1 c1 d1 in + let v2 = Sign.eval_big_int sign2 c2 d2 in + let vmeet = Z.(shift_right (c1 + c2 + one) 1) in + Linear (Z.(max vmeet (max v1 v2)), SymLinear.zero) + | (MinMax (_, Plus, Min, _, s1) as b), MinMax (_, Plus, Max, _, s2) + | MinMax (_, Plus, Max, _, s2), (MinMax (_, Plus, Min, _, s1) as b) + | (MinMax (_, Minus, Min, _, s1) as b), MinMax (_, Minus, Max, _, s2) + | MinMax (_, Minus, Max, _, s2), (MinMax (_, Minus, Min, _, s1) as b) + when Symb.Symbol.equal s1 s2 -> + b + | MinMax (c1, Plus, Max, _, s1), MinMax (c2, Plus, Max, _, s2) + | MinMax (c1, Minus, Min, _, s1), MinMax (c2, Minus, Min, _, s2) + when Symb.Symbol.equal s1 s2 -> + if Z.leq c1 c2 then b1 else b2 + | ( MinMax (c1, (Minus as sign1), (Max as minmax1), d1, s1) + , MinMax (c2, (Plus as sign2), Max, d2, s2) ) + | ( MinMax (c2, (Plus as sign2), (Max as minmax1), d2, s2) + , MinMax (c1, (Minus as sign1), Max, d1, s1) ) + | ( MinMax (c1, (Plus as sign1), (Min as minmax1), d1, s1) + , MinMax (c2, (Minus as sign2), Min, d2, s2) ) + | ( MinMax (c2, (Minus as sign2), (Min as minmax1), d2, s2) + , MinMax (c1, (Plus as sign1), Min, d1, s1) ) + when Symb.Symbol.equal s1 s2 -> + let v1 = Sign.eval_big_int sign1 c1 d1 in + let v2 = Sign.eval_big_int sign2 c2 d2 in + let vmin, vmax = if Z.leq v1 v2 then (v1, v2) else (v2, v1) in + let vmeet = Z.(shift_right (c1 + c2 + one) 1) in + let v = if Z.leq vmin vmeet && Z.leq vmeet vmax then vmeet else vmax in + let d = Sign.eval_neg_if_minus sign1 Z.(v - c1) in + mk_MinMax (c1, sign1, minmax1, d, s1) + | _ -> ( + match big_int_ub b2 with + | Some v2 when not (is_const b2) -> + overapprox_min b1 (Linear (v2, SymLinear.zero)) + | _ -> ( + match big_int_ub b1 with + | Some v1 when not (is_const b1) -> + overapprox_min (Linear (v1, SymLinear.zero)) b2 + | _ -> + (* When the result is not representable, our best effort is to return the first original argument. Any other deterministic heuristics would work too. *) + original_b1 ) ) ) + in + overapprox_min original_b1 b2 + + + let underapprox_max b1 b2 = neg (overapprox_min (neg b1) (neg b2)) + let overapprox_max b1 b2 = neg (underapprox_min (neg b1) (neg b2)) + + let approx_max = function + | Symb.BoundEnd.LowerBound -> + underapprox_max + | Symb.BoundEnd.UpperBound -> + overapprox_max - let max_u : t -> t -> t = ub ~default:PInf let widen_l : t -> t -> t = fun x y -> @@ -656,17 +763,6 @@ module Bound = struct let mult_const_u = mult_const Symb.BoundEnd.UpperBound - let neg : t -> t = function - | MInf -> - PInf - | PInf -> - MInf - | Linear (c, x) -> - Linear (Z.neg c, SymLinear.neg x) - | MinMax (c, sign, min_max, d, x) -> - mk_MinMax (Z.neg c, Sign.neg sign, min_max, d, x) - - let div_const : t -> NonZeroInt.t -> t option = fun x n -> match x with @@ -727,7 +823,7 @@ module Bound = struct let get s = match eval_sym s with | NonBottom x when Symb.Symbol.is_unsigned s -> - NonBottom (ub ~default:x zero x) + NonBottom (approx_max subst_pos x zero) | x -> x in @@ -745,7 +841,8 @@ module Bound = struct Bottom ) | NonBottom x -> let x = mult_const subst_pos coeff x in - if Symb.Symbol.is_unsigned s then NonBottom (ub ~default:x zero x) else NonBottom x + if Symb.Symbol.is_unsigned s then NonBottom (approx_max subst_pos x zero) + else NonBottom x in match x with | MInf | PInf -> diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index 4638f449f..3552de9d1 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -81,11 +81,11 @@ module Bound : sig val xcompare : t PartialOrder.xcompare - val min_l : t -> t -> t + val underapprox_min : t -> t -> t - val min_u : t -> t -> t + val overapprox_min : t -> t -> t - val max_u : t -> t -> t + val overapprox_max : t -> t -> t val widen_l : t -> t -> t diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 1a8cd63cf..0080e5e51 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -501,7 +501,9 @@ module ItvPure = struct `RightSubsumesLeft - let join : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.min_l l1 l2, Bound.max_u u1 u2) + let join : t -> t -> t = + fun (l1, u1) (l2, u2) -> (Bound.underapprox_min l1 l2, Bound.overapprox_max u1 u2) + let widen : prev:t -> next:t -> num_iters:int -> t = fun ~prev:(l1, u1) ~next:(l2, u2) ~num_iters:_ -> (Bound.widen_l l1 l2, Bound.widen_u u1 u2) @@ -729,7 +731,9 @@ module ItvPure = struct else Boolean.Top - let min_sem : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.min_l l1 l2, Bound.min_u u1 u2) + let min_sem : t -> t -> t = + fun (l1, u1) (l2, u2) -> (Bound.underapprox_min l1 l2, Bound.overapprox_min u1 u2) + let is_invalid : t -> bool = function | Bound.PInf, _ | _, Bound.MInf -> diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 14bd77f19..fc9c0f4b5 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -105,6 +105,9 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVE codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Offset: [n.lb, +oo] Size: n] codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Offset: [n.lb, +oo] Size: n] codetoanalyze/c/bufferoverrun/issue_kinds.c, zero_to_infty, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] +codetoanalyze/c/bufferoverrun/minmax.c, exact_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] +codetoanalyze/c/bufferoverrun/minmax.c, exact_min_plus_min_plus_min_UNDERRUN, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: x,Call,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [-19+min(0, x.lb), -1] Size: 1] +codetoanalyze/c/bufferoverrun/minmax.c, underapprox_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, no_bucket, ERROR, [] codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 255] Size: 255] codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 256] Size: 256] @@ -153,9 +156,8 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 7, CONDITION_AL codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 11, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] -codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,Assignment,ArrayAccess: Offset: [0, +oo] Size: 17] -codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Return,Assignment,Binop: ([-1, +oo] + 1):signed32] -codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex_200_Good_FP, 4, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,Assignment,ArrayAccess: Offset: [0, +oo] Size: 16] +codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,Assignment,ArrayAccess: Offset: [-28, 16] Size: 17] +codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_sym_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,Assignment,ArrayAccess: Offset: [-28, 16] Size: 17] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_false_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 1 Size: 1] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/minmax.c b/infer/tests/codetoanalyze/c/bufferoverrun/minmax.c new file mode 100644 index 000000000..cd6fa6407 --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/minmax.c @@ -0,0 +1,40 @@ +/* + * Copyright (c) 2018-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +int exact_min_minus_min_linear_CAF(int x) { + int size1[1]; + int y = 28; + if (x < 5) + y = x + 10; + // y = [10 + min(18, x), 28] + if (y > 28) { + size1[-1] = 0; + } + return y; +} + +int underapprox_min_minus_min_linear_CAF(int x) { + int size1[1]; + int y = 10; + if (x < 5) + y = x + 20; + // y = [20 + min(-10, x), 24] + if (y > 24) { + size1[-1] = 0; + } + return y; +} + +void exact_min_plus_min_plus_min_UNDERRUN(int x, int b) { + int size1[1]; + int y = exact_min_minus_min_linear_CAF(x); + if (b) + y = underapprox_min_minus_min_linear_CAF(x); + y -= 29; + // [-19 + min(0, x), -1] + size1[y] = 0; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c index f55d19497..0888fcffc 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c @@ -61,7 +61,7 @@ void call_fromHex_sym_Good(char c) { } } -void call_fromHex_200_Good_FP() { +void call_fromHex_200_Good() { char arr[16]; int idx = fromHex(200); if (idx >= 0) { @@ -69,7 +69,7 @@ void call_fromHex_200_Good_FP() { } } -void call_fromHex2_sym_Good(char c) { +void call_fromHex2_sym_Good_FP(char c) { char arr[17]; int idx = fromHex(c); arr[idx + 1] = 'H';