diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index cade9dbcb..500376372 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -194,8 +194,6 @@ module Bound = struct module Sign = struct type t = sign [@@deriving compare] - let equal = [%compare.equal: t] - let neg = function Plus -> Minus | Minus -> Plus let eval_big_int x i1 i2 = match x with Plus -> Z.(i1 + i2) | Minus -> Z.(i1 - i2) @@ -213,8 +211,6 @@ module Bound = struct module MinMax = struct type t = min_max [@@deriving compare] - let equal = [%compare.equal: t] - let neg = function Min -> Max | Max -> Min let eval_big_int x i1 i2 = match x with Min -> Z.min i1 i2 | Max -> Z.max i1 i2 @@ -405,22 +401,30 @@ module Bound = struct false | Linear (c0, x0), Linear (c1, x1) -> c0 <= c1 && SymLinear.le x0 x1 - | MinMax (c1, sign1, m1, d1, x1), MinMax (c2, sign2, m2, d2, x2) - when Sign.equal sign1 sign2 && MinMax.equal m1 m2 -> - c1 <= c2 && Z.equal d1 d2 && Symb.Symbol.equal x1 x2 | MinMax _, MinMax _ when le_minmax_by_int x y -> true - | MinMax (c1, Plus, Min, _, x1), MinMax (c2, Plus, Max, _, x2) - | MinMax (c1, Minus, Max, _, x1), MinMax (c2, Minus, Min, _, x2) -> - c1 <= c2 && Symb.Symbol.equal x1 x2 + | MinMax (c1, (Plus as sign), Min, d1, s1), MinMax (c2, Plus, Min, d2, s2) + | MinMax (c1, (Minus as sign), Min, d1, s1), MinMax (c2, Minus, Min, d2, s2) + | MinMax (c1, (Plus as sign), Max, d1, s1), MinMax (c2, Plus, Max, d2, s2) + | MinMax (c1, (Minus as sign), Max, d1, s1), MinMax (c2, Minus, Max, d2, s2) + when Symb.Symbol.equal s1 s2 -> + Z.leq c1 c2 + && + let v1 = Sign.eval_big_int sign c1 d1 in + let v2 = Sign.eval_big_int sign c2 d2 in + Z.leq v1 v2 + | MinMax (c1, Plus, Min, _, s1), MinMax (c2, Plus, Max, _, s2) + | MinMax (c1, Minus, Max, _, s1), MinMax (c2, Minus, Min, _, s2) + when Symb.Symbol.equal s1 s2 -> + Z.leq c1 c2 + | MinMax _, MinMax _ -> + false | MinMax _, Linear (c, se) -> (SymLinear.is_ge_zero se && le_opt1 Z.leq (big_int_ub_of_minmax x) c) || le_opt1 le (linear_ub_of_minmax x) y | Linear (c, se), MinMax _ -> (SymLinear.is_le_zero se && le_opt2 Z.leq c (big_int_lb_of_minmax y)) || le_opt2 le x (linear_lb_of_minmax y) - | _, _ -> - false let lt : t -> t -> bool = diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 7c4c48427..8c1421d36 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -147,6 +147,9 @@ 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, 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/prune_constant.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c index 801c92a0d..f55d19497 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c @@ -42,3 +42,41 @@ void prune_constant_not_Bad() { a[x + 1] = 0; } } + +int fromHex(char c) { + if (c < '0' || (c > '9' && (c < 'a' || c > 'f'))) { + return -1; // invalid not 0-9a-f hex char + } + if (c <= '9') { + return c - '0'; + } + return c - 'a' + 10; +} + +void call_fromHex_sym_Good(char c) { + char arr[16]; + int idx = fromHex(c); + if (idx >= 0) { + arr[idx] = 'H'; + } +} + +void call_fromHex_200_Good_FP() { + char arr[16]; + int idx = fromHex(200); + if (idx >= 0) { + arr[idx] = 'H'; + } +} + +void call_fromHex2_sym_Good(char c) { + char arr[17]; + int idx = fromHex(c); + arr[idx + 1] = 'H'; +} + +void call_fromHex2_200_Good_FP() { + char arr[17]; + int idx = fromHex(200); + arr[idx + 1] = 'H'; +}