[inferbo] Add InputStream.read model

Summary: This diff adds a model of a `InputStream.read` function.

Reviewed By: jvillard

Differential Revision: D17422745

fbshipit-source-id: 861d6798d

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -1107,6 +1107,18 @@ let unmodifiable _ s =
   && List.exists ~f:(fun suffix -> String.is_suffix ~suffix s) ["Set"; "Collection"; "Map"; "List"]
 
 
+module InputStream = struct
+  (* https://docs.oracle.com/javase/7/docs/api/java/io/InputStream.html#read(byte[],%20int,%20int) *)
+  let read exp =
+    let exec {integer_type_widths} ~ret:(ret_id, _) mem =
+      let max = Sem.eval integer_type_widths exp mem in
+      let traces = Dom.Val.get_traces max in
+      let v = Dom.Val.of_itv ~traces (Itv.set_lb Itv.Bound.mone (Dom.Val.get_itv max)) in
+      model_by_value v ret_id mem
+    in
+    {exec; check= no_check}
+end
+
 module Call = struct
   let dispatch : (Tenv.t, model) ProcnameDispatcher.Call.dispatcher =
     let open ProcnameDispatcher.Call in
@@ -1337,5 +1349,6 @@ module Call = struct
       ; +PatternMatch.implements_lang "Integer"
         &:: "intValue" <>$ capt_exp $--> JavaInteger.intValue
       ; +PatternMatch.implements_lang "Integer" &:: "valueOf" <>$ capt_exp $--> JavaInteger.valueOf
-      ]
+      ; +PatternMatch.implements_io "InputStream"
+        &:: "read" <>$ any_arg $+ any_arg $+ any_arg $+ capt_exp $--> InputStream.read ]
 end

infer/src/bufferoverrun/itv.ml

@@ -131,7 +131,9 @@ module ItvPure = struct
 
   let pos = (Bound.one, Bound.pinf)
 
-  let set_lb_zero (_, ub) = (Bound.zero, ub)
+  let set_lb lb (_, ub) = (lb, ub)
+
+  let set_lb_zero = set_lb Bound.zero
 
   let top = (Bound.minf, Bound.pinf)
 
@@ -594,6 +596,8 @@ let incr = plus one
 
 let decr x = minus x one
 
+let set_lb lb = lift1 (ItvPure.set_lb lb)
+
 let set_lb_zero = lift1 ItvPure.set_lb_zero
 
 let get_iterator_itv : t -> t = lift1 ItvPure.get_iterator_itv

infer/src/bufferoverrun/itv.mli

@@ -161,6 +161,8 @@ val decr : t -> t
 
 val incr : t -> t
 
+val set_lb : Bound.t -> t -> t
+
 val set_lb_zero : t -> t
 
 val neg : t -> t

infer/tests/codetoanalyze/java/performance/Cost_test.java

@@ -4,9 +4,11 @@
  * This source code is licensed under the MIT license found in the
  * LICENSE file in the root directory of this source tree.
  */
-
 package codetoanalyze.java.performance;
 
+import java.io.IOException;
+import java.io.InputStream;
+
 public class Cost_test {
 
   // Cost: 5
@@ -179,4 +181,13 @@ public class Cost_test {
       }
     }
   }
+
+  void call_inputstream_read_linear(InputStream is) throws IOException {
+    int total = 0;
+    int r;
+    byte[] buf = new byte[20];
+    while (total < 100 && (r = is.read(buf, 0, 20)) != -1) {
+      total += r;
+    }
+  }
 }

infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java

@@ -34,7 +34,7 @@ class UnknownCallsTest {
     return 0;
   }
 
-  // Expected: Max(Math,min(...), InputStream.read(....)) but we get T
+  // Expected: linear to maxBytesToRead (= Math.min(...))
   public int read_max_cost(
       InputStream in, byte[] buffer, int byteOffset, int byteCount, ArrayList<Integer> list)
       throws IOException {

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

@@ -87,8 +87,9 @@ 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, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 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 90]
+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.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 133,{n},Loop at line 133]
+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 28604, 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]
 codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop1_bad():int, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 1303, O(1), degree = 0]
 codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop3(int):int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 237, O(1), degree = 0]
@@ -178,7 +179,6 @@ codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switc
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 14 + 12 ⋅ String.toCharArray().length.ub, O(String.toCharArray().length.ub), degree = 1,{String.toCharArray().length.ub},call to void UnknownCallsTest.loop_over_charArray(StringBuilder,String),Loop at line 52]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_linear(org.json.JSONArray):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ jsonArray.length, O(jsonArray.length), degree = 1,{jsonArray.length},Loop at line 18]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ String.toCharArray().length.ub, O(String.toCharArray().length.ub), degree = 1,{String.toCharArray().length.ub},Loop at line 52]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 47]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 9, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 21 + 5 ⋅ (Math.min(...).ub + 1), O(Math.min(...).ub), degree = 1,{Math.min(...).ub + 1},Loop at line 47]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 15 + 6 ⋅ 2⋅Math.min(...).ub, O(2⋅Math.min(...).ub), degree = 1,{2⋅Math.min(...).ub},Loop at line 33]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 15 + 6 ⋅ (Math.min(...).ub + InputStream.read(...).ub), O((Math.min(...).ub + InputStream.read(...).ub)), degree = 1,{Math.min(...).ub + InputStream.read(...).ub},Loop at line 33]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 62,{list.length},Loop at line 62]