diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 445e6181e..eb0c1389f 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -366,6 +366,16 @@ module SymLinear = struct fun x -> match get_mone_symbol_opt x with Some _ -> true | None -> false + let is_one_symbol_of : Symbol.t -> t -> bool = + fun s x -> + Option.value_map (get_one_symbol_opt x) ~default:false ~f:(fun s' -> Symbol.equal s s') + + + let is_mone_symbol_of : Symbol.t -> t -> bool = + fun s x -> + Option.value_map (get_mone_symbol_opt x) ~default:false ~f:(fun s' -> Symbol.equal s s') + + let get_symbols : t -> Symbol.t list = fun x -> M.fold (fun symbol _coeff acc -> symbol :: acc) x [] end @@ -793,6 +803,12 @@ module Bound = struct match (x, y) with | PInf, _ | _, PInf -> L.(die InternalError) "Lower bound cannot be +oo." + | MinMax (n1, Plus, Max, _, s1), Linear (n2, s2) + when Int.equal n1 n2 && SymLinear.is_one_symbol_of s1 s2 -> + y + | MinMax (n1, Minus, Min, _, s1), Linear (n2, s2) + when Int.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 -> + y | _ -> if le x y then x else MInf @@ -802,6 +818,12 @@ module Bound = struct match (x, y) with | MInf, _ | _, MInf -> L.(die InternalError) "Upper bound cannot be -oo." + | MinMax (n1, Plus, Min, _, s1), Linear (n2, s2) + when Int.equal n1 n2 && SymLinear.is_one_symbol_of s1 s2 -> + y + | MinMax (n1, Minus, Max, _, s1), Linear (n2, s2) + when Int.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 -> + y | _ -> if le y x then x else PInf diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c b/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c index 1077c9d71..b802167cf 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c @@ -38,3 +38,27 @@ void for_loop() { a[i] = 'a'; /* BUG */ } } + +void nop() { int k = 0; } + +int two_loops(int m) { + for (int i = 0; i < m; i++) { + nop(); + } + for (int j = 0; j < m; j++) { + nop(); + } + return m; +} + +void call_two_loops_Good() { + int a[10]; + int m = 5; + a[two_loops(m)] = 1; +} + +void call_two_loops_Bad() { + int a[10]; + int m = 15; + a[two_loops(m)] = 1; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 3f8459490..b205463b5 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -17,6 +17,7 @@ codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRU codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [1, 1] Size: [1, 1] by call to `two_symbolic_accesses()` ] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_U5, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/for_loop.c, call_two_loops_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: m,Assignment,Return,ArrayAccess: Offset: [15, 15] Size: [10, 10]] codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, ERROR, [Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [0, 9] Size: [5, 10]] codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] codetoanalyze/c/bufferoverrun/function_call.c, call_by_ptr_bad, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index 8ac0d8dc0..6d0c625ed 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -49,10 +49,12 @@ codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TI codetoanalyze/c/performance/instantiate.c, do_n_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 3 + 6 * s$1] codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 5 + 5 * s$1^2] codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 5 + 5 * s$1^2] -codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, [] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 4 + 6 * s$1] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 4, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 4 + 6 * s$1] +codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 8 + 12 * s$1] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 6 + 6 * s$1] +codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 7, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 8 + 12 * s$1] +codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 9, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 10 + 12 * s$1] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 4 + 6 * s$1] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 4 + 6 * s$1] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 6 + 6 * s$1] diff --git a/infer/tests/codetoanalyze/c/performance/two_loops_symbolic.c b/infer/tests/codetoanalyze/c/performance/two_loops_symbolic.c index 81584c22b..bd3a3795d 100644 --- a/infer/tests/codetoanalyze/c/performance/two_loops_symbolic.c +++ b/infer/tests/codetoanalyze/c/performance/two_loops_symbolic.c @@ -8,8 +8,6 @@ */ void nop() { int k = 0; } -/* we report infinity after the first loop, due to the problem in prune node. - * Instead, we should obtain the appropriate bounds for the two loops */ int two_loops_symb(int m) { int p = 10; @@ -22,8 +20,6 @@ int two_loops_symb(int m) { return p; } -/* we report the appropriate bounds for the two loops if the loops are over two - * different arguments */ int two_loops_symb_diff(int m, int k) { int p = 10; for (int i = 0; i < m; i++) {