From 2401f6f6eb12b59cc76fa2d1e62ac775f6b05f93 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 2 Nov 2018 10:32:44 -0700 Subject: [PATCH] [inferbo] Give a widening threshold of zero Reviewed By: mbouaziz Differential Revision: D12898540 fbshipit-source-id: 95bdaf4f0 --- infer/src/bufferoverrun/bounds.ml | 8 ++++---- infer/tests/codetoanalyze/c/bufferoverrun/arith.c | 2 +- infer/tests/codetoanalyze/c/bufferoverrun/issues.exp | 1 - infer/tests/codetoanalyze/c/performance/issues.exp | 2 +- infer/tests/codetoanalyze/java/performance/Invariant.java | 7 ++++--- infer/tests/codetoanalyze/java/performance/issues.exp | 6 ++++-- 6 files changed, 14 insertions(+), 12 deletions(-) diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index aa49f65ae..f90efbdb9 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -615,6 +615,8 @@ module Bound = struct overapprox_max + let zero : t = Linear (Z.zero, SymLinear.zero) + let widen_l : t -> t -> t = fun x y -> match (x, y) with @@ -627,7 +629,7 @@ module Bound = struct when Z.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 -> y | _ -> - if le x y then x else MInf + if le x y then x else if le zero x && le zero y then zero else MInf let widen_u : t -> t -> t = @@ -642,11 +644,9 @@ module Bound = struct when Z.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 -> y | _ -> - if le y x then x else PInf + if le y x then x else if le x zero && le y zero then zero else PInf - let zero : t = Linear (Z.zero, SymLinear.zero) - let one : t = Linear (Z.one, SymLinear.zero) let mone : t = Linear (Z.minus_one, SymLinear.zero) diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index 0b635b609..69f8320b9 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -255,7 +255,7 @@ void unsigned_prune_zero2_Good(unsigned int y) { } } -void call_unsigned_prune_zero2_Good_FP() { unsigned_prune_zero2_Good(0); } +void call_unsigned_prune_zero2_Good() { unsigned_prune_zero2_Good(0); } void unsigned_prune_ge1_Good(unsigned int x, unsigned int y) { if (x >= y) { diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 50a811920..ec7e9f1be 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -1,6 +1,5 @@ codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: s,Binop: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ] codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ] -codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_zero2_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: y,Assignment,Binop: ([-oo, 0] - 1):unsigned32 by call to `unsigned_prune_zero2_Good` ] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (2000000000 + 2000000000):signed32] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_l2_Bad, 7, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Assignment,Binop: ([0, 2000000000] + [0, 2000000000]):signed32] diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index 05cab2777..c8f98b5de 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -55,7 +55,7 @@ codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTIO codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * (-m.lb + 20), degree = 1] codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 5 * (-m.lb + 20), degree = 1] codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201, degree = 0] -codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([-oo, +oo] + 1):signed32] +codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([3, +oo] + 1):signed32] codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1205, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1205, degree = 0] codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1205, degree = 0] diff --git a/infer/tests/codetoanalyze/java/performance/Invariant.java b/infer/tests/codetoanalyze/java/performance/Invariant.java index 09e352d96..e710c7264 100644 --- a/infer/tests/codetoanalyze/java/performance/Invariant.java +++ b/infer/tests/codetoanalyze/java/performance/Invariant.java @@ -22,9 +22,10 @@ class Invariant { } // x shouldn't be invariant since it can have two different values - // depending on whether the inner conditional is executed or not - // Currently, we are getting T because of a problem in InferBo, see - // T32798161 + // depending on whether the inner conditional is executed or not. + // Currently, we are getting a quadratic, rather than a linear, + // because the value of x at the true branch of the if statement is + // precisely analyzed to [0,4+min(1,size.ub)], rather than [0,5]. void formal_not_invariant_FP(int size, int x) { int i = 0; while (i < size + x) { diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 43f61b927..337b41f59 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -79,7 +79,7 @@ codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Co codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad(int):void, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 608, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad(int):void, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 609, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad_loop():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201, degree = 0] -codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad_loop():int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([-oo, +oo] + 1):signed32] +codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad_loop():int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([3, +oo] + 1):signed32] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_despite_inferbo(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1304, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_despite_inferbo(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1303, degree = 0] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_despite_inferbo(int):int, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1303, degree = 0] @@ -110,7 +110,9 @@ codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 * items.length.ub + 4 * (items.length.ub + 1), degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 * items.length.ub + 4 * (items.length.ub + 1), degree = 1] -codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] +codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 36 * (size.ub + 5) + 3 * (size.ub + 5) * (5+min(1, size.ub)) + 4 * (5+min(0, size.ub)), degree = 2] +codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 36 * (size.ub + 5) + 3 * (size.ub + 5) * (5+min(1, size.ub)) + 4 * (5+min(0, size.ub)), degree = 2] +codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 36 * (size.ub + 5) + 3 * (size.ub + 5) * (5+min(1, size.ub)) + 4 * (5+min(0, size.ub)), degree = 2] codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 * (size.ub + 20), degree = 1] codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 * (size.ub + 20), degree = 1] codetoanalyze/java/performance/IteratorTest.java, IteratorTest.appendTo(java.util.Iterator):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 2 * (parts.length.ub + -1) + 4 * parts.length.ub, degree = 1]