diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 8c0c7fb3e..eae1e0ef8 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -163,9 +163,9 @@ module SymLinear = struct is_one_symbol_of_common get_mone_symbol_opt - let is_signed_one_symbol_of : weak:bool -> Sign.t -> Symb.Symbol.t -> t -> bool = - fun ~weak sign s x -> - match sign with Plus -> is_one_symbol_of ~weak s x | Minus -> is_mone_symbol_of ~weak s x + let is_signed_one_symbol_of : ?weak:bool -> Sign.t -> Symb.Symbol.t -> t -> bool = + fun ?weak sign s x -> + match sign with Plus -> is_one_symbol_of ?weak s x | Minus -> is_mone_symbol_of ?weak s x let get_symbols : t -> Symb.SymbolSet.t = @@ -770,6 +770,14 @@ module Bound = struct | MinMax (n1, Minus, Min, _, s1), Linear (n2, s2) when Z.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 -> y + | Linear (n1, s1), MinMax (n2, (Plus as sign1), Min, n3, _) + | Linear (n1, s1), MinMax (n2, (Minus as sign1), Max, n3, _) + when Z.equal n1 (Sign.eval_big_int sign1 n2 n3) && SymLinear.is_empty s1 -> + y + | Linear (n1, s1), MinMax (n2, (Plus as sign1), Min, _, s2) + | Linear (n1, s1), MinMax (n2, (Minus as sign1), Max, _, s2) + when Z.equal n1 n2 && SymLinear.is_signed_one_symbol_of sign1 s2 s1 -> + y | _ -> if le x y then x else @@ -790,6 +798,14 @@ module Bound = struct | MinMax (n1, Minus, Max, _, s1), Linear (n2, s2) when Z.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 -> y + | Linear (n1, s1), MinMax (n2, (Plus as sign1), Max, n3, _) + | Linear (n1, s1), MinMax (n2, (Minus as sign1), Min, n3, _) + when Z.equal n1 (Sign.eval_big_int sign1 n2 n3) && SymLinear.is_empty s1 -> + y + | Linear (n1, s1), MinMax (n2, (Plus as sign1), Max, _, s2) + | Linear (n1, s1), MinMax (n2, (Minus as sign1), Min, _, s2) + when Z.equal n1 n2 && SymLinear.is_signed_one_symbol_of sign1 s2 s1 -> + y | _ -> if le y x then x else diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 6a69693d7..230af7a0d 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -311,6 +311,6 @@ codetoanalyze/c/bufferoverrun/unrolling.c, call_do_two_times2_Good_FP, 0, BUFFER codetoanalyze/c/bufferoverrun/unrolling.c, call_do_two_times_Good_FP, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,,Parameter `n`,,Array declaration,Array access: Offset: [0, 4] Size: 1 by call to `do_two_times_Good` ] codetoanalyze/c/bufferoverrun/while_loop.c, diverge_on_narrowing, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([-oo, +oo] + 1):signed32] -codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `y`,,Parameter `y`,Binary operation: (x + [-oo, +oo]):signed32] +codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `y`,,Parameter `y`,Binary operation: (x + [min(0, y), max(0, y)]):signed32] codetoanalyze/c/bufferoverrun/while_loop.c, join_minmax_with_sum_signed_Good_FP, 12, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Parameter `y`,,Assignment,Array declaration,Array access: Offset: [0, +oo] Size: [0, +oo]] codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: [0, 10] Size: 10] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c b/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c index d03101b87..4cf3f8525 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/while_loop.c @@ -58,3 +58,14 @@ void join_minmax_with_sum_signed_Good_FP(int x, int y) { } a[i] = 2; } + +void preciser_widen_Good(int x) { + int idx = 0; + int arr[10]; + while (idx < 10) { + arr[idx] = 0; + if (unknown()) { + idx = x; + } + } +} diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index c54accd1e..99bfa9c6d 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -21,7 +21,7 @@ codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 3, INTEGER_OVER codetoanalyze/c/performance/cost_test.c, alias_OK, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binary operation: ([-oo, +oo] + 1):signed32] codetoanalyze/c/performance/cost_test.c, call_infinite, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Call to infinite,Unbounded loop,Loop at line 146, column 3] codetoanalyze/c/performance/cost_test.c, call_while_upto20_minus100_bad, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 606, O(1), degree = 0] -codetoanalyze/c/performance/cost_test.c, ignore_character_symbols_constant_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 155, column 3] +codetoanalyze/c/performance/cost_test.c, ignore_character_symbols_constant_FP, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 4 ⋅ (122-min(97, c)), O((-c + 122)), degree = 1,{122-min(97, c)},Loop at line 155, column 3] codetoanalyze/c/performance/cost_test.c, infinite, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 146, column 3] codetoanalyze/c/performance/cost_test.c, infinite, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: ([-oo, +oo] + [0, +oo]):signed32] codetoanalyze/c/performance/cost_test.c, infinite_FN, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: ([-oo, +oo] + [0, +oo]):signed32] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index a4a8bbada..fcf0ba879 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -114,7 +114,7 @@ codetoanalyze/java/performance/IntTest.java, IntTest.static_Integer_top():void, codetoanalyze/java/performance/IntTest.java, IntTest.valueOf_linear(int):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ p + 3 ⋅ (1+max(0, p)), O(p), degree = 1,{1+max(0, p)},Loop at line 20,{p},Loop at line 20] codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 3 ⋅ (k - 1) + 4 ⋅ (max(1, k)), O(k), degree = 1,{max(1, k)},Loop at line 58,{k - 1},Loop at line 58] codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 31] -codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `x`,,Parameter `x`,Binary operation: (size + [-oo, +oo]):signed32] +codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `x`,,Parameter `x`,Binary operation: (size + [min(0, x), max(0, x)]):signed32] codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `x`,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ items.length + 3 ⋅ (items.length + 1), O(items.length), degree = 1,{items.length + 1},Loop at line 66,{items.length},Loop at line 66] codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + 12 ⋅ (size + 5) + 7 ⋅ (size + 5) × (5+min(1, size)) + 4 ⋅ (5+min(0, size)), O(size²), degree = 2,{5+min(0, size)},Loop at line 46,{5+min(1, size)},Loop at line 46,{size + 5},Loop at line 46]