From 7a5ce519012d726c93817a716946a36dac653b6c Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 12 Nov 2019 08:05:25 -0800 Subject: [PATCH] [inferbo] Revise band semantics Summary: It returns non-top value when one of the parameters of band is positive, i.e., `x & 255` returns `[0, 255]` instead of top. Reviewed By: ezgicicek Differential Revision: D18448614 fbshipit-source-id: aaa298a66 --- infer/src/bufferoverrun/itv.ml | 2 ++ infer/tests/codetoanalyze/java/performance/Cost_test.java | 4 ++++ infer/tests/codetoanalyze/java/performance/issues.exp | 1 + 3 files changed, 7 insertions(+) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 02b71e0e0..6eceb8ec9 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -323,6 +323,8 @@ module ItvPure = struct | _, _ -> if is_ge_zero x && is_ge_zero y then (Bound.zero, Bound.overapprox_min (ub x) (ub y)) else if is_le_zero x && is_le_zero y then (Bound.minf, Bound.overapprox_min (ub x) (ub y)) + else if is_ge_zero x then (Bound.zero, ub x) + else if is_ge_zero y then (Bound.zero, ub y) else top diff --git a/infer/tests/codetoanalyze/java/performance/Cost_test.java b/infer/tests/codetoanalyze/java/performance/Cost_test.java index 2fdd634e4..ade1db464 100644 --- a/infer/tests/codetoanalyze/java/performance/Cost_test.java +++ b/infer/tests/codetoanalyze/java/performance/Cost_test.java @@ -202,6 +202,10 @@ public class Cost_test { void loop_on_unknown_global_linear() { for (int i = 0; i < get_global(); i++) {} } + + void band_constant(int x) { + for (int i = 0; i < (int) (x & 0xff); i++) {} + } } class CloneTest { diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 852aab56d..0c884d552 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -91,6 +91,7 @@ codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performanc codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7963049, O(1), degree = 0] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ k, O(k), degree = 1,{k},Loop at line 92] +codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.band_constant(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 1277, O(1), degree = 0] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.call_inputstream_read_linear(java.io.InputStream):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 27304, O(1), degree = 0] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.ignore_boolean_symbols_linear(boolean,int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ n + 2 ⋅ (1+max(0, n)), O(n), degree = 1,{1+max(0, n)},Loop at line 135,{n},Loop at line 135] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop0_bad():int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 1202, O(1), degree = 0]