From 264a97794d9c97f45d4a317949dbc6cca7b572c1 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Tue, 5 Mar 2019 07:02:56 -0800 Subject: [PATCH] [inferbo] Exact result for (c1 - max(d, x)) + (c2 + x) Reviewed By: skcho Differential Revision: D14185196 fbshipit-source-id: 92d8430a1 --- infer/src/bufferoverrun/bounds.ml | 19 ++++++++++++++----- .../codetoanalyze/c/performance/issues.exp | 4 ++-- 2 files changed, 16 insertions(+), 7 deletions(-) diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 57ce70391..15c1dda5f 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -158,6 +158,10 @@ module SymLinear = struct fun s x -> Option.exists (get_mone_symbol_opt x) ~f:(fun s' -> Symb.Symbol.equal s s') + let is_signed_one_symbol_of : Sign.t -> Symb.Symbol.t -> t -> bool = + fun sign s x -> match sign with Plus -> is_one_symbol_of s x | Minus -> is_mone_symbol_of s x + + let get_symbols : t -> Symb.SymbolSet.t = fun x -> M.fold (fun symbol _coeff acc -> Symb.SymbolSet.add symbol acc) x Symb.SymbolSet.empty @@ -729,8 +733,8 @@ module Bound = struct fun x -> match x with Linear (c, y) when SymLinear.is_zero y -> Some c | _ -> None - let plus_common : f:(t -> t -> t) -> t -> t -> t = - fun ~f x y -> + let plus_exact : otherwise:(t -> t -> t) -> t -> t -> t = + fun ~otherwise x y -> if is_zero x then y else if is_zero y then x else @@ -741,12 +745,17 @@ module Bound = struct | Linear (c2, x2), MinMax (c1, sign, min_max, d1, x1) when SymLinear.is_zero x2 -> mk_MinMax (Z.(c1 + c2), sign, min_max, d1, x1) + | MinMax (c1, sign, min_max, d, x1), Linear (c2, x2) + | Linear (c2, x2), MinMax (c1, sign, min_max, d, x1) + when SymLinear.is_signed_one_symbol_of (Sign.neg sign) x1 x2 -> + let c = Sign.eval_big_int sign Z.(c1 + c2) d in + mk_MinMax (c, Sign.neg sign, MinMax.neg min_max, d, x1) | _ -> - f x y + otherwise x y let plus_l : t -> t -> t = - plus_common ~f:(fun x y -> + plus_exact ~otherwise:(fun x y -> match (x, y) with | MinMax (c1, Plus, Max, d1, _), Linear (c2, x2) | Linear (c2, x2), MinMax (c1, Plus, Max, d1, _) -> @@ -759,7 +768,7 @@ module Bound = struct let plus_u : t -> t -> t = - plus_common ~f:(fun x y -> + plus_exact ~otherwise:(fun x y -> match (x, y) with | MinMax (c1, Plus, Min, d1, _), Linear (c2, x2) | Linear (c2, x2), MinMax (c1, Plus, Min, d1, _) -> diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index adde1d33d..b7382e9fa 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -28,7 +28,7 @@ codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_ codetoanalyze/c/performance/cost_test.c, loop1_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1207, degree = 0] codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 10 ⋅ k + 2 ⋅ (1+max(0, k)), degree = 1,{1+max(0, k)},Loop at line 85, column 3,{k},Loop at line 85, column 3] codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 214, degree = 0] -codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ (-m + 20), degree = 1,{-m + 20},Loop at line 117, column 3] +codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 5 ⋅ (-m + 20) + (21-min(20, m)), degree = 1,{21-min(20, m)},Loop at line 117, column 3,{-m + 20},Loop at line 117, column 3] codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 235, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1307, degree = 0] @@ -68,6 +68,6 @@ codetoanalyze/c/performance/switch_continue.c, test_switch, 3, CONDITION_ALWAYS_ codetoanalyze/c/performance/switch_continue.c, test_switch, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0] codetoanalyze/c/performance/switch_continue.c, unroll_loop, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/switch_continue.c, unroll_loop, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/c/performance/switch_continue.c, unroll_loop, 14, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 25 + 12 ⋅ (n - 1), degree = 1,{n - 1},Loop at line 43, column 11] +codetoanalyze/c/performance/switch_continue.c, unroll_loop, 14, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 14 + (n - 1) + 11 ⋅ (max(1, n)), degree = 1,{max(1, n)},Loop at line 43, column 11,{n - 1},Loop at line 43, column 11] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1,{1+max(0, m)},Loop at line 13, column 3,{m},Loop at line 13, column 3] codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1,{1+max(0, m)},Loop at line 25, column 3,{m},Loop at line 25, column 3]