[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

@@ -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
 
 

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 {

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, [<LHS trace>,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]