From 9c14e9d384c4dfba158d48585231616df66f43e2 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Wed, 2 May 2018 03:24:26 -0700 Subject: [PATCH] [Cost] Fix multiplication by 1 Reviewed By: ddino Differential Revision: D7782184 fbshipit-source-id: dd3c4f1 --- infer/src/bufferoverrun/itv.ml | 44 ++++++++++--------- .../codetoanalyze/c/performance/cost_test.c | 1 - .../codetoanalyze/c/performance/issues.exp | 2 + 3 files changed, 25 insertions(+), 22 deletions(-) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index ce82095ff..8a5fac408 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -806,18 +806,31 @@ module Bound = struct None + let neg : t -> t = function + | MInf -> + PInf + | PInf -> + MInf + | Linear (c, x) -> + Linear (-c, SymLinear.neg x) + | MinMax (c, sign, min_max, d, x) -> + mk_MinMax (-c, Sign.neg sign, min_max, d, x) + + let mult : t -> t -> t = fun x y -> - let res_opt = - match (is_const x, is_const y) with - | _, Some n -> ( - match NonZeroInt.of_int n with Some n' -> mult_const x n' | _ -> Some zero ) - | Some n, _ -> ( - match NonZeroInt.of_int n with Some n' -> mult_const y n' | _ -> Some zero ) - | _, _ -> - None - in - Option.value res_opt ~default:PInf + let default = PInf in + match (x, is_const x, y, is_const y) with + | x, _, _, Some n | _, Some n, x, _ -> ( + match NonZeroInt.of_int n with + | Some n -> + if NonZeroInt.is_one n then x + else if NonZeroInt.is_minus_one n then neg x + else mult_const x n |> Option.value ~default + | None -> + zero ) + | _ -> + default let div_const : t -> NonZeroInt.t -> t option = @@ -837,17 +850,6 @@ module Bound = struct None - let neg : t -> t = function - | MInf -> - PInf - | PInf -> - MInf - | Linear (c, x) -> - Linear (-c, SymLinear.neg x) - | MinMax (c, sign, min_max, d, x) -> - mk_MinMax (-c, Sign.neg sign, min_max, d, x) - - let get_symbols : t -> Symbol.t list = function | MInf | PInf -> [] diff --git a/infer/tests/codetoanalyze/c/performance/cost_test.c b/infer/tests/codetoanalyze/c/performance/cost_test.c index b5d006b26..5e49cee3e 100644 --- a/infer/tests/codetoanalyze/c/performance/cost_test.c +++ b/infer/tests/codetoanalyze/c/performance/cost_test.c @@ -81,7 +81,6 @@ int loop1_bad() { return 0; } -// This is currently evaluated to Top as the analysis is not powerful enough int FN_loop2(int k) { for (int i = 0; i < k; i++) { diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index 6c71389b6..236b8f2f5 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -1,4 +1,6 @@ codetoanalyze/c/performance/cost_test.c, FN_loop2, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, [] +codetoanalyze/c/performance/cost_test.c, FN_loop2, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 11xs$1 + 3] +codetoanalyze/c/performance/cost_test.c, FN_loop2, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 11xs$1 + 3] codetoanalyze/c/performance/cost_test.c, FN_loop3, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, [] codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1002] codetoanalyze/c/performance/cost_test.c, loop0_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1002]