[inferbo,cost] Add models for java.util.Arrays and java.util.List

Reviewed By: jvillard

Differential Revision: D15577408

fbshipit-source-id: f9e94dc35

infer/src/absint/PatternMatch.ml

@@ -54,6 +54,8 @@ let implements interface tenv typename =
   supertype_exists tenv is_interface (Typ.Name.Java.from_string typename)
 
 
+let implements_arrays = implements "java.util.Arrays"
+
 let implements_iterator = implements "java.util.Iterator"
 
 let implements_collection = implements "java.util.Collection"

infer/src/absint/PatternMatch.mli

@@ -30,6 +30,9 @@ val is_subtype : Tenv.t -> Typ.Name.t -> Typ.Name.t -> bool
 val is_subtype_of_str : Tenv.t -> Typ.Name.t -> string -> bool
 (** Resolve [typ_str] in [tenv], then check [typ] <: [typ_str] *)
 
+val implements_arrays : Tenv.t -> string -> bool
+(** Check whether class implements Java's Arrays *)
+
 val implements_iterator : Tenv.t -> string -> bool
 (** Check whether class implements Java's Iterator *)
 

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -328,12 +328,17 @@ let inferbo_min e1 e2 =
   {exec; check= no_check}
 
 
-let inferbo_set_size e1 e2 =
-  let exec {integer_type_widths; location} ~ret:_ mem =
-    let locs = Sem.eval integer_type_widths e1 mem |> Dom.Val.get_pow_loc in
-    let length = Sem.eval integer_type_widths e2 mem in
+let set_size {integer_type_widths; location} array_v size_exp mem =
+  let locs = Dom.Val.get_pow_loc array_v in
+  let length = Sem.eval integer_type_widths size_exp mem in
   Dom.Mem.transform_mem ~f:(Dom.Val.set_array_length location ~length) locs mem
-  and check = check_alloc_size ~can_be_zero:true e2 in
+
+
+let inferbo_set_size src_exp size_exp =
+  let exec ({integer_type_widths} as model) ~ret:_ mem =
+    let src_v = Sem.eval integer_type_widths src_exp mem in
+    set_size model src_v size_exp mem
+  and check = check_alloc_size ~can_be_zero:true size_exp in
   {exec; check}
 
 
@@ -422,6 +427,20 @@ let snprintf = by_risky_value_from Trace.snprintf Dom.Val.Itv.nat
 
 let vsnprintf = by_risky_value_from Trace.vsnprintf Dom.Val.Itv.nat
 
+let copy array_v ret_id mem =
+  let dest_loc = Loc.of_id ret_id |> PowLoc.singleton in
+  Dom.Mem.update_mem dest_loc array_v mem
+
+
+(** Creates a new array with the values from the given array.*)
+let create_copy_array src_exp =
+  let exec {integer_type_widths} ~ret:(id, _) mem =
+    let array_v = Sem.eval integer_type_widths src_exp mem in
+    copy array_v id mem
+  in
+  {exec; check= no_check}
+
+
 module CFArray = struct
   (** Creates a new array from the given array by copying the first X
      elements. *)
@@ -440,16 +459,6 @@ module CFArray = struct
     {exec; check}
 
 
-  (** Creates a new array with the values from the given array.*)
-  let create_copy_array src_exp =
-    let exec {integer_type_widths} ~ret:(id, _) mem =
-      let dest_loc = Loc.of_id id |> PowLoc.singleton in
-      let v = Sem.eval integer_type_widths src_exp mem in
-      Dom.Mem.update_mem dest_loc v mem
-    in
-    {exec; check= no_check}
-
-
   let at (array_exp, _) (index_exp, _) = at ?size:None array_exp index_exp
 end
 
@@ -612,8 +621,7 @@ end
 - each time we add an element, we increase the length of the array
 - each time we delete an element, we decrease the length of the array *)
 module Collection = struct
-  let new_collection _ =
-    let exec {pname; node_hash; location} ~ret:(id, _) mem =
+  let create_collection {pname; node_hash; location} ~ret:(id, _) mem ~length =
     let represents_multiple_values = true in
     let traces = Trace.(Set.singleton location ArrayDeclaration) in
     let coll_allocsite =
@@ -625,7 +633,7 @@ module Collection = struct
         Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None
           ~represents_multiple_values
       in
-        Dom.Val.of_java_array_alloc allocsite ~length:Itv.zero ~traces
+      Dom.Val.of_java_array_alloc allocsite ~length ~traces
     in
     let coll_loc = Loc.of_allocsite coll_allocsite in
     let internal_array_loc =
@@ -633,12 +641,23 @@ module Collection = struct
     in
     mem
     |> Dom.Mem.add_heap internal_array_loc internal_array
-      |> Dom.Mem.add_stack (Loc.of_id id)
-           (coll_loc |> PowLoc.singleton |> Dom.Val.of_pow_loc ~traces)
+    |> Dom.Mem.add_stack (Loc.of_id id) (coll_loc |> PowLoc.singleton |> Dom.Val.of_pow_loc ~traces)
+
+
+  (** Returns a fixed-size list with a given length backed by the specified array. *)
+  let copyOf array_exp length_exp =
+    let exec ({integer_type_widths} as model) ~ret:(id, _) mem =
+      let array_v = Sem.eval integer_type_widths array_exp mem in
+      copy array_v id mem |> set_size model array_v length_exp
     in
     {exec; check= no_check}
 
 
+  let new_collection _ =
+    let exec = create_collection ~length:Itv.zero 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
@@ -722,6 +741,19 @@ module Collection = struct
     {exec; check= no_check}
 
 
+  (** Returns a view of the portion of this list between the specified
+     fromIndex, inclusive, and toIndex, exclusive. Simply model it as
+     creating a new list with length toIndex - fromIndex.  *)
+  let subList from_exp to_exp =
+    let exec ({integer_type_widths} as model) ~ret mem =
+      let from_idx = Sem.eval integer_type_widths from_exp mem in
+      let to_idx = Sem.eval integer_type_widths to_exp mem in
+      let length = Itv.minus (Dom.Val.get_itv to_idx) (Dom.Val.get_itv from_idx) in
+      create_collection model ~ret mem ~length
+    in
+    {exec; check= no_check}
+
+
   (** increase the size by [0, |collection_to_add|] because put replaces the value
      rather than add a new one when the key is found in the map *)
   let putAll coll_id coll_to_add =
@@ -785,7 +817,7 @@ module Call = struct
       ; -"__inferbo_set_size" <>$ capt_exp $+ capt_exp $!--> inferbo_set_size
       ; -"__exit" <>--> bottom
       ; -"CFArrayCreate" <>$ any_arg $+ capt_exp $+ capt_exp $+...$--> CFArray.create_array
-      ; -"CFArrayCreateCopy" <>$ any_arg $+ capt_exp $!--> CFArray.create_copy_array
+      ; -"CFArrayCreateCopy" <>$ any_arg $+ capt_exp $!--> create_copy_array
       ; -"MCFArrayGetCount" <>$ capt_exp $!--> StdBasicString.length
       ; -"CFDictionaryGetCount" <>$ capt_exp $!--> StdBasicString.length
       ; -"CFArrayGetCount" <>$ capt_exp $!--> StdBasicString.length
@@ -808,6 +840,9 @@ module Call = struct
         $+...$--> Collection.new_collection
       ; -"__new" <>$ capt_exp $+...$--> malloc ~can_be_zero:true
       ; -"__new_array" <>$ capt_exp $+...$--> malloc ~can_be_zero:true
+      ; +PatternMatch.implements_arrays &:: "asList" <>$ capt_exp $!--> create_copy_array
+      ; +PatternMatch.implements_arrays &:: "copyOf" <>$ capt_exp $+ capt_exp
+        $+...$--> Collection.copyOf
       ; -"__placement_new" <>$ capt_exp $+ capt_arg $+? capt_arg $!--> placement_new
       ; -"realloc" <>$ capt_exp $+ capt_exp $+...$--> realloc
       ; -"__get_array_length" <>$ capt_exp $!--> get_array_length
@@ -910,6 +945,7 @@ module Call = struct
         &:: "add" <>$ capt_var_exn $+ capt_exp $+ any_arg $!--> Collection.add_at_index
       ; +PatternMatch.implements_lang "Iterable"
         &:: "iterator" <>$ capt_exp $!--> Collection.iterator
+      ; +PatternMatch.implements_list &:: "listIterator" <>$ capt_exp $+...$--> Collection.iterator
       ; +PatternMatch.implements_map &:: "entrySet" <>$ capt_exp $!--> Collection.iterator
       ; +PatternMatch.implements_map &:: "keySet" <>$ capt_exp $!--> Collection.iterator
       ; +PatternMatch.implements_map &:: "values" <>$ capt_exp $!--> Collection.iterator
@@ -918,6 +954,8 @@ module Call = struct
       ; +PatternMatch.implements_map &:: "putAll" <>$ capt_var_exn $+ capt_exp
         $--> Collection.putAll
       ; +PatternMatch.implements_iterator &:: "hasNext" <>$ capt_exp $!--> Collection.hasNext
+      ; +PatternMatch.implements_list &:: "subList" <>$ any_arg $+ capt_exp $+ capt_exp
+        $--> Collection.subList
       ; +PatternMatch.implements_collection
         &:: "addAll" <>$ capt_var_exn $+ capt_exp $--> Collection.addAll
       ; +PatternMatch.implements_collection

infer/src/checkers/costModels.ml

@@ -39,6 +39,18 @@ module Collections = struct
     |> BasicCost.of_non_negative_bound ~degree_kind
 
 
+  let copyOf size_exp {integer_type_widths; location} ~ret:_ inferbo_mem =
+    let upper_bound =
+      let itv =
+        BufferOverrunSemantics.eval integer_type_widths size_exp inferbo_mem
+        |> BufferOverrunDomain.Val.get_itv
+      in
+      match itv with Bottom -> Bounds.Bound.pinf | NonBottom itv_pure -> Itv.ItvPure.ub itv_pure
+    in
+    Bounds.NonNegativeBound.of_modeled_function "Arrays.copyOf" location upper_bound
+    |> BasicCost.of_non_negative_bound ~degree_kind:Polynomials.DegreeKind.Linear
+
+
   let linear = of_length_bound ~degree_kind:Polynomials.DegreeKind.Linear
 
   let logarithmic = of_length_bound ~degree_kind:Polynomials.DegreeKind.Log
@@ -89,17 +101,24 @@ module Call = struct
     let open ProcnameDispatcher.Call in
     make_dispatcher
       [ +PatternMatch.implements_collections &:: "sort" $ capt_exp $+...$--> Collections.sort
+      ; +PatternMatch.implements_list &:: "sort" $ capt_exp $+...$--> Collections.sort
       ; +PatternMatch.implements_list &:: "contains" <>$ capt_exp
         $+...$--> Collections.linear ~of_function:"List.contains"
       ; +PatternMatch.implements_collections
         &:: "binarySearch" <>$ capt_exp
         $+...$--> Collections.logarithmic ~of_function:"Collections.binarySearch"
+      ; +PatternMatch.implements_arrays &:: "binarySearch" <>$ capt_exp
+        $+...$--> Collections.logarithmic ~of_function:"Arrays.binarySearch"
+      ; +PatternMatch.implements_arrays &:: "copyOf" <>$ any_arg $+ capt_exp
+        $+...$--> Collections.copyOf
       ; +PatternMatch.implements_collections
         &:: "copy" <>$ capt_exp
         $+...$--> Collections.linear ~of_function:"Collections.copy"
       ; +PatternMatch.implements_collections
         &:: "fill" <>$ capt_exp
         $+...$--> Collections.linear ~of_function:"Collections.fill"
+      ; +PatternMatch.implements_arrays &:: "fill" <>$ capt_exp
+        $+...$--> Collections.linear ~of_function:"Arrays.fill"
       ; +PatternMatch.implements_collections
         &:: "reverse" <>$ capt_exp
         $+...$--> Collections.linear ~of_function:"Collections.reverse"

infer/src/checkers/purityModels.ml

@@ -56,7 +56,9 @@ module ProcName = struct
         &::+ startsWith "get" <>--> PurityDomain.pure
       ; +PatternMatch.implements_android "content.res.Resources"
         &::+ startsWith "get" <>--> PurityDomain.pure
+      ; +PatternMatch.implements_arrays &:: "asList" <>--> PurityDomain.pure
       ; +PatternMatch.implements_lang "Iterable" &:: "iterator" <>--> PurityDomain.pure
+      ; +PatternMatch.implements_list &:: "listIterator" <>--> PurityDomain.pure
       ; +PatternMatch.implements_collection &:: "iterator" <>--> PurityDomain.pure
       ; +PatternMatch.implements_iterator &:: "hasNext" <>--> PurityDomain.pure
       ; +PatternMatch.implements_iterator &:: "next" <>--> modifies_first
@@ -136,5 +138,7 @@ module ProcName = struct
       ; +PatternMatch.implements_queue &:: "poll" <>--> modifies_first
       ; +PatternMatch.implements_queue &:: "add" <>--> modifies_first
       ; +PatternMatch.implements_queue &:: "remove" <>--> modifies_first
-      ; +PatternMatch.implements_queue &:: "peek" <>--> PurityDomain.pure ]
+      ; +PatternMatch.implements_queue &:: "peek" <>--> PurityDomain.pure
+      ; +PatternMatch.implements_list &:: "subList" <>--> PurityDomain.pure
+      ; +PatternMatch.implements_arrays &:: "binarySearch" <>--> PurityDomain.pure ]
 end

infer/tests/codetoanalyze/java/performance/Array.java

@@ -6,6 +6,8 @@
  */
 package codetoanalyze.java.performance;
 
+import java.util.Arrays;
+
 public class Array {
 
   public void array_access_good() {
@@ -29,4 +31,21 @@ public class Array {
       if (10 < optionNumerators[j] + 1) {}
     }
   }
+
+  int binary_search_log(String[] arr) {
+    return Arrays.binarySearch(arr, "x");
+  }
+
+  void fill_linear(String[] arr) {
+    Arrays.fill(arr, "x");
+  }
+
+  void copyOf_linear(String[] arr) {
+    String[] new_arr = Arrays.copyOf(arr, arr.length);
+    for (String el : new_arr) {}
+  }
+
+  void copyOf_constant(String[] arr) {
+    String[] new_arr = Arrays.copyOf(arr, 10);
+  }
 }

infer/tests/codetoanalyze/java/performance/ListTest.java

@@ -0,0 +1,42 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+import com.google.common.base.Objects;
+import java.util.Arrays;
+import java.util.List;
+import java.util.ListIterator;
+
+class ListTest {
+
+  int indexOfImpl_linear(List<?> list, Object element) {
+    ListIterator<?> listIterator = list.listIterator();
+    while (listIterator.hasNext()) {
+      if (Objects.equal(element, listIterator.next())) {
+        return listIterator.previousIndex();
+      }
+    }
+    return -1;
+  }
+
+  void sort_comparator_nlogn(List<Person> people) {
+    people.sort(new LexicographicComparator());
+  }
+
+  void sublist(List<String> filesList) {
+
+    for (String file : filesList.subList(1, filesList.size())) {}
+  }
+
+  void sublist_constant(List<String> filesList) {
+
+    for (String file : filesList.subList(1, 3)) {}
+  }
+
+  void asList_linear(String[] array) {
+    List<String> list = Arrays.asList(array);
+    for (String el : list) {}
+  }
+}

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

@@ -1,7 +1,10 @@
 codetoanalyze/java/performance/A.java, B$BArray.error():void, 4, EXPENSIVE_ALLOCATION_CALL, no_bucket, ERROR, [with estimated cost 4, degree = 0]
 codetoanalyze/java/performance/A.java, B.error():void, 4, EXPENSIVE_ALLOCATION_CALL, no_bucket, ERROR, [with estimated cost 4, degree = 0]
 codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_overrun_bad():void, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: [2, 8] Size: 8]
-codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ length, degree = 1,{length},Loop at line 28]
+codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ length, degree = 1,{length},Loop at line 30]
+codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.binary_search_log(java.lang.String[]):int, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 2 + log(arr.length), degree = 0 + 1⋅log,{arr.length},Modeled call to Arrays.binarySearch]
+codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.copyOf_linear(java.lang.String[]):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 4 + arr.length, degree = 1,{arr.length},Modeled call to Arrays.copyOf]
+codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.fill_linear(java.lang.String[]):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 2 + arr.length, degree = 1,{arr.length},Modeled call to Arrays.fill]
 codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void, 5, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ mag.length, degree = 1,{mag.length},Loop at line 15]
 codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 4, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 883, degree = 0]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add3_overrun_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Through,Through,Array access: Offset added: 4 Size: 3]
@@ -122,6 +125,10 @@ codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.util
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.String):java.lang.StringBuilder, 2, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 33 + 65 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void JsonUtils.serialize(StringBuilder,String),call to void JsonUtils.escape(StringBuilder,String),Loop at line 13]
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.StringBuilder,java.lang.String):void, 5, EXPENSIVE_ALLOCATION_CALL, no_bucket, ERROR, [with estimated cost String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void JsonUtils.escape(StringBuilder,String),Loop at line 13]
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.StringBuilder,java.lang.String):void, 5, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 24 + 65 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void JsonUtils.escape(StringBuilder,String),Loop at line 13]
+codetoanalyze/java/performance/ListTest.java, ListTest.asList_linear(java.lang.String[]):void, 2, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 7 + 8 ⋅ (array.length - 1) + 3 ⋅ array.length, degree = 1,{array.length},Loop at line 40,{array.length - 1},Loop at line 40]
+codetoanalyze/java/performance/ListTest.java, ListTest.indexOfImpl_linear(java.util.List,java.lang.Object):int, 2, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 4 + 11 ⋅ (list.length - 1) + 3 ⋅ list.length, degree = 1,{list.length},Loop at line 16,{list.length - 1},Loop at line 16]
+codetoanalyze/java/performance/ListTest.java, ListTest.sort_comparator_nlogn(java.util.List):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 8 + people.length × log(people.length), degree = 1 + 1⋅log,{people.length},Modeled call to List.length,{people.length},Modeled call to List.length]
+codetoanalyze/java/performance/ListTest.java, ListTest.sublist(java.util.List):void, 2, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 11 + 8 ⋅ (filesList.length - 2) + 3 ⋅ (filesList.length - 1), degree = 1,{filesList.length - 1},Loop at line 30,{filesList.length - 2},Loop at line 30]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.charsequence_length_linear(java.lang.CharSequence):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ seq.length + 3 ⋅ (seq.length + 1), degree = 1,{seq.length + 1},Loop at line 111,{seq.length},Loop at line 111]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 3, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 2 + 25 ⋅ (length - 1), degree = 1,{length - 1},Loop at line 40]