[inferbo] Ignore symbolic values in ranges when upper bound is constant

Summary:
Handle the case of

- computing the range of `[lb, ub]` where `lb` contains length path and `ub` is constant. E.g. `[a.length, 2]` would give `3` range
- simplifying  `c1 +/- min(c2, a.length)` to `c1 +/- min(c2, 0)`

since the length of a collection/array is always nonnegative.

This also removes some existing FPs in tests results.

Facebook

Context: we stumbled upon this issue in ObjC results TV109717121 which is corresponding to the added test case.

Reviewed By: skcho

Differential Revision: D23648807

fbshipit-source-id: 1e89ea246

infer/src/bufferoverrun/bounds.ml

@@ -105,6 +105,12 @@ module SymLinear = struct
 
   let neg : t -> t = fun x -> M.map NonZeroInt.( ~- ) x
 
+  let remove_positive_length_symbol : t -> t =
+    M.filter (fun symb coeff ->
+        let path = Symb.Symbol.path symb in
+        not (NonZeroInt.is_positive coeff && Symb.SymbolPath.is_length path) )
+
+
   let plus : t -> t -> t =
    fun x y ->
     let plus_coeff _ c1 c2 = NonZeroInt.plus c1 c2 in
@@ -614,6 +620,22 @@ module Bound = struct
         mk_MultB (Z.neg c, neg x, y)
 
 
+  let rec remove_positive_length_symbol b =
+    match b with
+    | MInf | PInf ->
+        b
+    | Linear (c, x) ->
+        Linear (c, SymLinear.remove_positive_length_symbol x)
+    | MinMax (c, sign, min_max, d, x) ->
+        if Symb.Symbol.is_length x then
+          Linear (Sign.eval_big_int sign c (MinMax.eval_big_int min_max d Z.zero), SymLinear.empty)
+        else b
+    | MinMaxB (m, x, y) ->
+        mk_MinMaxB (m, remove_positive_length_symbol x, remove_positive_length_symbol y)
+    | MultB (c, x, y) ->
+        mk_MultB (c, remove_positive_length_symbol x, remove_positive_length_symbol y)
+
+
   let exact_min : otherwise:(t -> t -> t) -> t -> t -> t =
    fun ~otherwise b1 b2 ->
     if le b1 b2 then b1
@@ -1227,6 +1249,20 @@ module Bound = struct
         if phys_equal a a' && phys_equal b b' then x else mk_MultB (c, a', b')
 
 
+  let simplify_minimum_length x =
+    match x with
+    | MultB _ | Linear _ | MInf | PInf | MinMaxB _ ->
+        x
+    | MinMax (c1, sign, Min, c2, symb) ->
+        let path = Symb.Symbol.path symb in
+        if Symb.SymbolPath.is_length path then
+          let z = Sign.eval_big_int sign c1 (Z.min c2 Z.zero) in
+          Linear (z, SymLinear.empty)
+        else x
+    | MinMax _ ->
+        x
+
+
   let get_same_one_symbol b1 b2 =
     match (b1, b2) with
     | Linear (n1, se1), Linear (n2, se2) when Z.(equal n1 zero) && Z.(equal n2 zero) ->

infer/src/bufferoverrun/bounds.mli

@@ -126,6 +126,12 @@ module Bound : sig
 
   val simplify_min_one : t -> t
 
+  val simplify_minimum_length : t -> t
+  (** Simplifies c1 +/- min(c2, length) to c1 +- min(0,c2) *)
+
+  val remove_positive_length_symbol : t -> t
+  (** Removes positive symbols that are coming from length paths *)
+
   val get_same_one_symbol : t -> t -> Symb.SymbolPath.t option
   (** It returns a symbol [s] when the two bounds are all linear expressions of the symbol [1⋅s]. *)
 

infer/src/bufferoverrun/itv.ml

@@ -22,9 +22,18 @@ module ItvRange = struct
 
   let of_bounds : loop_head_loc:Location.t -> lb:Bound.t -> ub:Bound.t -> t =
    fun ~loop_head_loc ~lb ~ub ->
+    let lb =
+      (* Handle the case of[s, c] where s contains positive length path and c
+         is constant. E.g [len, 2] would give 3 since len is always
+         nonnegative *)
+      if Bound.is_symbolic lb && not (Bound.is_symbolic ub) then
+        Bound.remove_positive_length_symbol lb
+      else lb
+    in
     Bound.plus_u ~weak:true ub Bound.one
     |> Bound.plus_u ~weak:true (Bound.neg lb)
     |> Bound.simplify_min_one |> Bound.simplify_bound_ends_from_paths
+    |> Bound.simplify_minimum_length
     |> Bounds.NonNegativeBound.of_loop_bound loop_head_loc
 
 

infer/src/bufferoverrun/symb.ml

@@ -233,6 +233,8 @@ module SymbolPath = struct
         false
 
 
+  let is_length = function Length _ -> true | _ -> false
+
   let is_global = function Normal p | Offset {p} | Length {p} | Modeled {p} -> is_global_partial p
 end
 
@@ -353,6 +355,13 @@ module Symbol = struct
         path
 
 
+  let is_length = function
+    | ForeignVariable _ ->
+        false
+    | OneValue {path} | BoundEnd {path} ->
+        SymbolPath.is_length path
+
+
   (* NOTE: This may not be satisfied in the cost checker for simplifying its results. *)
   let check_bound_end s be =
     if Config.bo_debug >= 3 then

infer/src/bufferoverrun/symb.mli

@@ -80,6 +80,8 @@ module SymbolPath : sig
   val is_cpp_vector_elem : partial -> bool
 
   val is_global_partial : partial -> bool
+
+  val is_length : t -> bool
 end
 
 module Symbol : sig
@@ -95,6 +97,8 @@ module Symbol : sig
 
   val is_global : t -> bool
 
+  val is_length : t -> bool
+
   val pp_mark : markup:bool -> F.formatter -> t -> unit
 
   val equal : t -> t -> bool

infer/tests/codetoanalyze/java/performance/Loops.java

@@ -10,6 +10,7 @@ import android.app.Activity;
 import java.io.IOException;
 import java.nio.ByteBuffer;
 import java.nio.channels.FileChannel;
+import java.util.ArrayList;
 
 public class Loops {
 
@@ -171,4 +172,14 @@ public class Loops {
       }
     }
   }
+
+  int loop_prune_constant(ArrayList<Integer> list) {
+    int k = 0;
+    for (int i = 0; i < 3; ++i) {
+      if (list.size() >= i + 1) {
+        k++;
+      }
+    }
+    return k;
+  }
 }

infer/tests/codetoanalyze/java/performance/StringTest.java

@@ -98,7 +98,7 @@ class StringTest {
 
   boolean unknown_bool;
 
-  public void last_index_of_linear_FP(String s) {
+  public void last_index_of_linear_FN(String s) {
     int i = s.lastIndexOf('/');
     while (i > 0) {
       int j = s.lastIndexOf('/', i - 1);

infer/tests/codetoanalyze/java/performance/cost-issues.exp

@@ -285,6 +285,7 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_simple_linear(codetoanalyze.java.performance.Loops$MyLinkedList):void, 3 + 10 ⋅ (p.linked_list_length + 1),  OnUIThread:false, [{p.linked_list_length + 1},Loop]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.linked_list_model_linear(android.app.Activity):void, 3 + 7 ⋅ (p.linked_list_length + 1),  OnUIThread:false, [{p.linked_list_length + 1},Loop]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.loop_linear(int):void, 5 + 5 ⋅ x,  OnUIThread:false, [{x},Loop]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.loop_prune_constant(java.util.ArrayList):int, 42,  OnUIThread:false, []
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.modeled_range_linear_FP(java.nio.channels.FileChannel,java.nio.ByteBuffer):void, 6 + 14 ⋅ FileChannel.read(...).modeled²,  OnUIThread:false, [{FileChannel.read(...).modeled},Modeled call to read(...),{FileChannel.read(...).modeled},Modeled call to read(...)]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, ⊤,  OnUIThread:false, [Unbounded loop,Loop]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar_linear(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 47 + 26 ⋅ x.length,  OnUIThread:false, [{x.length},Loop]
@@ -305,13 +306,13 @@ codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.Mat
 codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.linear(int):void, 5 + 5 ⋅ p,  OnUIThread:false, [{p},Loop]
 codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.max2_symbolic(int,int):void, 9 + 9 ⋅ (max(x, y)),  OnUIThread:false, [{max(x, y)},Loop]
 codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.max_symbolic(int[]):void, 5 + 5 ⋅ arr.length + 4 ⋅ (arr.length + 1),  OnUIThread:false, [{arr.length + 1},Loop,{arr.length},Loop]
-codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.min_constant(int[]):void, 5 + 5 ⋅ (min(3, arr.length)) + 4 ⋅ (1+min(3, arr.length)),  OnUIThread:false, [{1+min(3, arr.length)},Loop,{min(3, arr.length)},Loop]
+codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.min_constant(int[]):void, 14,  OnUIThread:false, []
 codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest$Constant.<init>(PreconditionTest), 6,  OnUIThread:false, []
 codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.<init>(), 3,  OnUIThread:false, []
-codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.checkArgument_constant(java.util.ArrayList):void, 16 + 5 ⋅ (min(2, list.length)) + 3 ⋅ (1+min(2, list.length)),  OnUIThread:false, [{1+min(2, list.length)},Loop,{min(2, list.length)},Loop]
+codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.checkArgument_constant(java.util.ArrayList):void, 24,  OnUIThread:false, []
 codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.checkNotNull_linear(java.util.ArrayList,java.lang.Object):void, 13 + 8 ⋅ list.length + 3 ⋅ (list.length + 1),  OnUIThread:false, [{list.length + 1},Loop,{list.length},Loop]
-codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.checkState_constant(java.util.ArrayList):void, 16 + 5 ⋅ (min(2, list.length)) + 3 ⋅ (1+min(2, list.length)),  OnUIThread:false, [{1+min(2, list.length)},Loop,{min(2, list.length)},Loop]
-codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.constant_array(int[]):void, 20 + 17 ⋅ (min(5, a.length)),  OnUIThread:false, [{min(5, a.length)},Loop]
+codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.checkState_constant(java.util.ArrayList):void, 24,  OnUIThread:false, []
+codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.constant_array(int[]):void, 37,  OnUIThread:false, []
 codetoanalyze/java/performance/StringBuilderTest.java, StringBuilderTest.<init>(), 3,  OnUIThread:false, []
 codetoanalyze/java/performance/StringBuilderTest.java, StringBuilderTest.append_linear(java.lang.String):void, 25 + 5 ⋅ (s.length + 2) + 3 ⋅ (s.length + 3),  OnUIThread:false, [{s.length + 3},Call to void StringBuilderTest.new_linear(String),Loop,{s.length + 2},Call to void StringBuilderTest.new_linear(String),Loop]
 codetoanalyze/java/performance/StringBuilderTest.java, StringBuilderTest.new_capacity_constant():void, 24,  OnUIThread:false, []
@@ -329,7 +330,7 @@ codetoanalyze/java/performance/StringTest.java, StringTest.indexof_from_linear(j
 codetoanalyze/java/performance/StringTest.java, StringTest.indexof_linear(java.lang.String):int, 5 + m.length,  OnUIThread:false, [{m.length},Modeled call to String.indexOf]
 codetoanalyze/java/performance/StringTest.java, StringTest.indexof_quadratic(java.lang.String,java.lang.String):int, 6 + m.length × n.length,  OnUIThread:false, [{n.length},Modeled call to String.indexOf,{m.length},Modeled call to String.indexOf]
 codetoanalyze/java/performance/StringTest.java, StringTest.last_index_of_linear(java.lang.String):void, 8 + 5 ⋅ (s.length - 1),  OnUIThread:false, [{s.length - 1},Loop]
-codetoanalyze/java/performance/StringTest.java, StringTest.last_index_of_linear_FP(java.lang.String):void, 8 + 6 ⋅ (s.length - 1) × (s.length + 1) + 4 ⋅ (1+min(1, s.length))²,  OnUIThread:false, [{1+min(1, s.length)},Loop,{1+min(1, s.length)},Loop,{s.length + 1},Loop,{s.length - 1},Loop]
+codetoanalyze/java/performance/StringTest.java, StringTest.last_index_of_linear_FN(java.lang.String):void, 24,  OnUIThread:false, []
 codetoanalyze/java/performance/StringTest.java, StringTest.replace_linear(java.lang.String):void, 8 + 5 ⋅ s.length + 3 ⋅ (s.length + 1),  OnUIThread:false, [{s.length + 1},Loop,{s.length},Loop]
 codetoanalyze/java/performance/StringTest.java, StringTest.split_linear(java.lang.String):void, 9 + 6 ⋅ (-1+max(2, s.length)),  OnUIThread:false, [{-1+max(2, s.length)},Loop]
 codetoanalyze/java/performance/StringTest.java, StringTest.split_with_limit_linear(java.lang.String,int):void, 10 + 6 ⋅ (max(1, limit)),  OnUIThread:false, [{max(1, limit)},Loop]

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -66,6 +66,7 @@ codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.util
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded value x,Call to void Loops.loop_linear(int),Loop]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Call,<LHS trace>,Parameter `x`,Binary operation: ([0, +oo] + 1):signed32 by call to `void Loops.loop_linear(int)` ]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.loop_prune_constant(java.util.ArrayList):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.modeled_range_linear_FP(java.nio.channels.FileChannel,java.nio.ByteBuffer):void, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 8):signed32]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]