[inferbo] Add naive models for Java's Buffer

Summary: First iteration for naive Buffer models.

Reviewed By: skcho

Differential Revision: D22844558

fbshipit-source-id: 4619255a9

infer/src/absint/ProcnameDispatcher.ml

@@ -253,6 +253,10 @@ module type Common = sig
   val ( ~+ ) : ('context -> string -> bool) -> ('context, 'f, 'f, 'arg_payload) name_matcher
   (** Starts a path with a matching name that satisfies the given function *)
 
+  val startsWith : string -> 'context -> string -> bool
+
+  val endsWith : string -> 'context -> string -> bool
+
   val ( &+ ) :
        ('context, 'f_in, 'f_interm, accept_more, 'arg_payload) templ_matcher
     -> ('f_interm, 'f_out, 'lc) template_arg
@@ -353,6 +357,10 @@ module Common = struct
 
   let ( ~+ ) f_name = name_cons_f empty f_name
 
+  let startsWith prefix _ s = String.is_prefix ~prefix s
+
+  let endsWith suffix _ s = String.is_suffix ~suffix s
+
   let ( &+ ) templ_matcher template_arg = templ_cons templ_matcher template_arg
 
   let ( &+...>! ) templ_matcher () = templ_matcher &+ any_template_args >! ()

infer/src/absint/ProcnameDispatcher.mli

@@ -64,6 +64,10 @@ module type Common = sig
   val ( ~+ ) : ('context -> string -> bool) -> ('context, 'f, 'f, 'arg_payload) name_matcher
   (** Starts a path with a matching name that satisfies the given function *)
 
+  val startsWith : string -> 'context -> string -> bool
+
+  val endsWith : string -> 'context -> string -> bool
+
   val ( &+ ) :
        ('context, 'f_in, 'f_interm, accept_more, 'arg_payload) templ_matcher
     -> ('f_interm, 'f_out, 'lc) template_arg

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -881,6 +881,14 @@ module Collection = struct
     {exec; check= no_check}
 
 
+  let allocate size_exp =
+    let exec ({integer_type_widths} as env) ~ret mem =
+      let length = Sem.eval integer_type_widths size_exp mem |> Dom.Val.get_itv in
+      create_collection env ~ret mem ~length
+    in
+    {exec; check= no_check}
+
+
   let eval_collection_internal_array_locs coll_exp mem =
     Sem.eval_locs coll_exp mem
     |> PowLoc.append_field ~fn:BufferOverrunField.java_collection_internal_array
@@ -1487,8 +1495,8 @@ module FileChannel = struct
     {exec; check= no_check}
 end
 
-module ByteBuffer = struct
+module Buffer = struct
-  let get_int buf_exp =
+  let get buf_exp =
     let exec _ ~ret:(ret_id, _) mem =
       let range = Dom.Mem.find_set (Sem.eval_locs buf_exp mem) mem |> Dom.Val.get_modeled_range in
       let v = Dom.Val.of_itv Itv.nat |> Dom.Val.set_modeled_range range in
@@ -1750,6 +1758,11 @@ module Call = struct
       ; +PatternMatch.Java.implements_io "InputStream"
         &:: "read" <>$ any_arg $+ any_arg $+ any_arg $+ capt_exp $--> InputStream.read
       ; +PatternMatch.Java.implements_iterator &:: "hasNext" <>$ capt_exp $!--> Collection.hasNext
+      ; +PatternMatch.Java.implements_nio "Buffer" &:: "wrap" <>$ capt_exp $--> create_copy_array
+      ; +PatternMatch.Java.implements_nio "Buffer"
+        &:: "allocate" <>$ capt_exp $--> Collection.allocate
+      ; +PatternMatch.Java.implements_nio "Buffer"
+        &:: "hasRemaining" <>$ capt_exp $!--> Collection.hasNext
       ; +PatternMatch.Java.implements_iterator &:: "next" <>$ capt_exp $!--> Collection.next
       ; +PatternMatch.Java.implements_lang "CharSequence"
         &:: "<init>" <>$ capt_exp $+ capt_exp $--> JavaString.copy_constructor
@@ -1824,14 +1837,9 @@ module Call = struct
         $--> Collection.putAll
       ; +PatternMatch.Java.implements_map &:: "size" <>$ capt_exp $!--> Collection.size
       ; +PatternMatch.Java.implements_map &:: "values" <>$ capt_exp $!--> Collection.iterator
-      ; +PatternMatch.Java.implements_nio "ByteBuffer"
+      ; +PatternMatch.Java.implements_nio "Buffer"
-        &:: "get" <>$ capt_exp $--> ByteBuffer.get_int
+        &::+ startsWith "get" <>$ capt_exp $+...$--> Buffer.get
-      ; +PatternMatch.Java.implements_nio "ByteBuffer"
+      ; +PatternMatch.Java.implements_nio "Buffer" &:: "duplicate" <>$ capt_exp $+...$--> id
-        &:: "getInt" <>$ capt_exp $--> ByteBuffer.get_int
-      ; +PatternMatch.Java.implements_nio "ByteBuffer"
-        &:: "getLong" <>$ capt_exp $--> ByteBuffer.get_int
-      ; +PatternMatch.Java.implements_nio "ByteBuffer"
-        &:: "getShort" <>$ capt_exp $--> ByteBuffer.get_int
       ; +PatternMatch.Java.implements_nio "channels.FileChannel"
         &:: "read" <>$ any_arg $+ capt_exp $+ any_arg $--> FileChannel.read
       ; +PatternMatch.Java.implements_org_json "JSONArray"

infer/src/bufferoverrun/bufferOverrunTypModels.ml

@@ -39,5 +39,6 @@ let dispatch : (Tenv.t, typ_model, unit) ProcnameDispatcher.TypName.dispatcher =
     ; +PatternMatch.Java.implements_iterator &::.*--> Java.collection
     ; +PatternMatch.Java.implements_map &::.*--> Java.collection
     ; +PatternMatch.Java.implements_pseudo_collection &::.*--> Java.collection
+    ; +PatternMatch.Java.implements_nio "Buffer" &::.*--> Java.collection
     ; +PatternMatch.Java.implements_lang "Integer" &::.*--> Java.integer
     ; +PatternMatch.Java.implements_org_json "JSONArray" &::.*--> Java.collection ]

infer/src/checkers/purityModels.ml

@@ -31,12 +31,11 @@ let modifies_third = PurityDomain.impure_params (PurityDomain.ModifiedParamIndic
 
 let pure_builtins _ s = BuiltinPureMethods.mem s pure_builtins
 
-let endsWith suffix _ s = String.is_suffix ~suffix s
-
-let startsWith prefix _ s = String.is_prefix ~prefix s
-
 (* matches get*Value *)
-let getStarValue tenv s = startsWith "get" tenv s && endsWith "Value" tenv s
+let getStarValue tenv s =
+  let open ProcnameDispatcher.ProcName in
+  startsWith "get" tenv s && endsWith "Value" tenv s
+
 
 module ProcName = struct
   let dispatch : (Tenv.t, PurityDomain.t, unit) ProcnameDispatcher.ProcName.dispatcher =
@@ -77,6 +76,8 @@ module ProcName = struct
       ; +PatternMatch.Java.implements_collection &:: "isEmpty" <>--> PurityDomain.pure
       ; +PatternMatch.Java.implements_collection &:: "get" <>--> PurityDomain.pure
       ; +PatternMatch.Java.implements_collection &:: "set" <>--> modifies_first
+      ; +PatternMatch.Java.implements_nio "Buffer" &::+ startsWith "get" <>--> modifies_first
+      ; +PatternMatch.Java.implements_nio "Buffer" &::+ startsWith "put" <>--> modifies_first
       ; +PatternMatch.Java.implements_list &:: "contains" <>--> PurityDomain.pure
       ; +PatternMatch.Java.implements_collection &:: "contains" <>--> PurityDomain.pure
       ; +PatternMatch.Java.implements_enumeration &:: "hasMoreElements" <>--> PurityDomain.pure

infer/tests/codetoanalyze/java/performance/BufferTest.java

@@ -0,0 +1,52 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * 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.*;
+import java.nio.*;
+import java.util.*;
+
+class BufferTest {
+  private ByteBuffer data;
+
+  void drainBuffer_linear(ByteBuffer buffer) {
+    while (buffer.hasRemaining()) {
+      Byte b = buffer.get();
+    }
+  }
+
+  void fillBuffer_linear(CharBuffer buffer, int capacity, String string) {
+    for (int i = 0; i < capacity; i++) {
+      buffer.put(string.charAt(i));
+    }
+  }
+
+  void wrapBuffer_linear(byte[] arr) {
+    ByteBuffer buffer = ByteBuffer.wrap(arr);
+    while (buffer.hasRemaining()) {
+      Byte b = buffer.get();
+    }
+  }
+
+  void allocateBuffer_constant(byte[] arr) {
+    ByteBuffer buffer = ByteBuffer.allocate(10);
+    while (buffer.hasRemaining()) {
+      Byte b = buffer.get();
+    }
+  }
+
+  public void writeTo_linear(OutputStream out) throws IOException {
+    byte[] buffer = new byte[8192];
+    ByteBuffer data = this.data.duplicate();
+    data.clear();
+    while (data.hasRemaining()) {
+      int count = Math.min(buffer.length, data.remaining());
+      data.get(buffer, 0, count);
+      out.write(buffer, 0, count);
+    }
+  }
+}

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

@@ -116,7 +116,7 @@ public class Loops {
     for (int i = 0; i < seq.length(); i++) {}
   }
 
-  void modeled_range_linear(FileChannel fc, ByteBuffer bb) throws IOException {
+  void modeled_range_linear_FP(FileChannel fc, ByteBuffer bb) throws IOException {
     int i;
     int offset = 0;
     do {

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

@@ -82,6 +82,12 @@ codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.
 codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant_FP(int):int, 13 + 7 ⋅ p,  OnUIThread:false, [{p},Call to int Break.break_loop(int,int),Loop]
 codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 8 + 7 ⋅ p,  OnUIThread:false, [{p},Loop]
 codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 8 + 4 ⋅ maxI + 3 ⋅ maxI × (min(12, maxJ)) + 5 ⋅ maxI × (12-max(0, maxJ)) + 5 ⋅ (min(11, maxI)) × (min(11, maxJ)),  OnUIThread:false, [{min(11, maxJ)},Loop,{min(11, maxI)},Loop,{12-max(0, maxJ)},Loop,{min(12, maxJ)},Loop,{maxI},Loop]
+codetoanalyze/java/performance/BufferTest.java, codetoanalyze.java.performance.BufferTest.<init>(), 3,  OnUIThread:false, []
+codetoanalyze/java/performance/BufferTest.java, codetoanalyze.java.performance.BufferTest.allocateBuffer_constant(byte[]):void, 118,  OnUIThread:false, []
+codetoanalyze/java/performance/BufferTest.java, codetoanalyze.java.performance.BufferTest.drainBuffer_linear(java.nio.ByteBuffer):void, 3 + 8 ⋅ buffer.length + 3 ⋅ (buffer.length + 1),  OnUIThread:false, [{buffer.length + 1},Loop,{buffer.length},Loop]
+codetoanalyze/java/performance/BufferTest.java, codetoanalyze.java.performance.BufferTest.fillBuffer_linear(java.nio.CharBuffer,int,java.lang.String):void, 5 + 13 ⋅ capacity,  OnUIThread:false, [{capacity},Loop]
+codetoanalyze/java/performance/BufferTest.java, codetoanalyze.java.performance.BufferTest.wrapBuffer_linear(byte[]):void, 6 + 8 ⋅ arr.length + 3 ⋅ (arr.length + 1),  OnUIThread:false, [{arr.length + 1},Loop,{arr.length},Loop]
+codetoanalyze/java/performance/BufferTest.java, codetoanalyze.java.performance.BufferTest.writeTo_linear(java.io.OutputStream):void, 12 + 19 ⋅ this.data.length + 3 ⋅ (this.data.length + 1),  OnUIThread:false, [{this.data.length + 1},Loop,{this.data.length},Loop]
 codetoanalyze/java/performance/CantHandle.java, CantHandle.<init>(), 3,  OnUIThread:false, []
 codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_FP(int):void, ⊤,  OnUIThread:false, [Unbounded loop,Loop]
 codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_variant_FP(int):void, ⊤,  OnUIThread:false, [Unbounded loop,Loop]
@@ -277,7 +283,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.modeled_range_linear(java.nio.channels.FileChannel,java.nio.ByteBuffer):void, 6 + 14 ⋅ FileChannel.read(...).modeled,  OnUIThread:false, [{FileChannel.read(...).modeled},Modeled call to read(...)]
+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]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.string_concat_linear(java.lang.String,java.lang.String):void, 11 + 5 ⋅ (p.length + s.length) + 3 ⋅ (p.length + s.length + 1),  OnUIThread:false, [{p.length + s.length + 1},Loop,{p.length + s.length},Loop]

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

@@ -66,7 +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.modeled_range_linear(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.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]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol_FP():void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded value x,Call to void Loops.loop_linear(int),Loop]