From 5fe28785bc3157f356e70c8f5d5642dae0c09008 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Thu, 3 May 2018 05:04:30 -0700 Subject: [PATCH] Cost: fix min Summary: We were wrongly using the underapproximation of `min` rather than the overapproximation Reviewed By: ddino Differential Revision: D7844267 fbshipit-source-id: c9d9247 --- infer/src/bufferoverrun/itv.ml | 25 +++++++++++++------ infer/src/bufferoverrun/itv.mli | 2 +- infer/src/checkers/cost.ml | 2 +- .../codetoanalyze/c/performance/cost_test.c | 5 ++-- .../codetoanalyze/c/performance/issues.exp | 11 +++++--- 5 files changed, 28 insertions(+), 17 deletions(-) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 8a5fac408..45e9754f9 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -622,8 +622,8 @@ module Bound = struct x - let rec lb : ?default:t -> t -> t -> t = - fun ?(default= MInf) x y -> + let rec lb : default:t -> t -> t -> t = + fun ~default x y -> if le x y then x else if le y x then y else @@ -668,6 +668,17 @@ module Bound = struct default + (** underapproximation of min b1 b2 *) + let min_l b1 b2 = lb ~default:MInf b1 b2 + + (** overapproximation of min b1 b2 *) + let min_u b1 b2 = + lb + ~default: + (* When the result is not representable, our best effort is to return the first argument. Any other deterministic heuristics would work too. *) + b1 b1 b2 + + let ub : ?default:t -> t -> t -> t = fun ?(default= PInf) x y -> if le x y then y @@ -688,8 +699,6 @@ module Bound = struct let join : t -> t -> t = ub ~default:PInf - let min : t -> t -> t = lb ~default:MInf - let widen_l : t -> t -> t = fun x y -> match (x, y) with @@ -896,8 +905,8 @@ module ItvPure = struct let has_infty = function Bound.MInf, _ | _, Bound.PInf -> true | _, _ -> false let subst : t -> Bound.t bottom_lifted SymbolMap.t -> t bottom_lifted = - fun x map -> - match (Bound.subst_lb (lb x) map, Bound.subst_ub (ub x) map) with + fun (l, u) map -> + match (Bound.subst_lb l map, Bound.subst_ub u map) with | NonBottom l, NonBottom u -> NonBottom (l, u) | _ -> @@ -938,7 +947,7 @@ module ItvPure = struct `RightSubsumesLeft - let join : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb l1 l2, Bound.ub u1 u2) + let join : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb ~default:MInf l1 l2, Bound.ub u1 u2) let widen : prev:t -> next:t -> num_iters:int -> t = fun ~prev:(l1, u1) ~next:(l2, u2) ~num_iters:_ -> (Bound.widen_l l1 l2, Bound.widen_u u1 u2) @@ -1151,7 +1160,7 @@ module ItvPure = struct else Boolean.Top - let min_sem : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb l1 l2, Bound.lb ~default:u1 u1 u2) + let min_sem : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.min_l l1 l2, Bound.min_u u1 u2) let is_invalid : t -> bool = function | Bound.PInf, _ | _, Bound.MInf -> diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 795f426dd..51c00a18f 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -70,7 +70,7 @@ module Bound : sig val join : t -> t -> t - val min : t -> t -> t + val min_u : t -> t -> t val mult : t -> t -> t diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 96b9fa7ac..0f2f7762d 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -338,7 +338,7 @@ return the addends of the sum x_j1+x_j2+..+x_j_n*) | Leaf (_, c) -> c | Min l -> - evaluate_operator Itv.Bound.min l + evaluate_operator Itv.Bound.min_u l | Plus l -> evaluate_operator Itv.Bound.plus_u l diff --git a/infer/tests/codetoanalyze/c/performance/cost_test.c b/infer/tests/codetoanalyze/c/performance/cost_test.c index 5e49cee3e..9d4969fa1 100644 --- a/infer/tests/codetoanalyze/c/performance/cost_test.c +++ b/infer/tests/codetoanalyze/c/performance/cost_test.c @@ -81,7 +81,7 @@ int loop1_bad() { return 0; } -int FN_loop2(int k) { +int loop2_bad(int k) { for (int i = 0; i < k; i++) { alias2_OK(); @@ -89,8 +89,7 @@ int FN_loop2(int k) { return 0; } -// This is currently evaluated to Top as the analysis is not powerful enough -int FN_loop3(int k) { +int loop3_bad(int k) { for (int i = k; i < k + 15; i++) { alias2_OK(); diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index cd66694e0..5231de6fb 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -1,13 +1,16 @@ -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] codetoanalyze/c/performance/cost_test.c, loop0_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1004] codetoanalyze/c/performance/cost_test.c, loop1_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1104] codetoanalyze/c/performance/cost_test.c, loop1_bad, 4, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1104] codetoanalyze/c/performance/cost_test.c, loop1_bad, 6, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1106] +codetoanalyze/c/performance/cost_test.c, loop2_bad, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, [] +codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 11xs$1 + 3] +codetoanalyze/c/performance/cost_test.c, loop2_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 11xs$1 + 3] +codetoanalyze/c/performance/cost_test.c, loop3_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost (-1)xs$0 + s$1 + 16] +codetoanalyze/c/performance/cost_test.c, loop3_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost (-13)xs$0 + 13xs$1 + 199] +codetoanalyze/c/performance/cost_test.c, loop3_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost (-13)xs$0 + 13xs$1 + 199] +codetoanalyze/c/performance/cost_test.c, loop3_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost (-15)xs$0 + 15xs$1 + 231] codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 211] codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 12, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 201] codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1204]