[cost] Add model of File.listFiles

Summary:
This diff adds a model of `File.listFiles` as returning an array with
a symbolic length.

Reviewed By: ezgicicek

Differential Revision: D22332258

fbshipit-source-id: 6ca593b8b

infer/src/bufferoverrun/bufferOverrunField.ml

@@ -37,6 +37,8 @@ let java_linked_list_length = mk "java.linked_list_length" Typ.(int)
 
 let java_linked_list_next typ = mk "java.linked_list_next" typ
 
+let java_list_files_length = mk "java.list_files_length" Typ.(int)
+
 let is_java_collection_internal_array fn = Fieldname.equal fn java_collection_internal_array
 
 let c_strlen () =

infer/src/bufferoverrun/bufferOverrunField.mli

@@ -38,6 +38,9 @@ val java_linked_list_length : Fieldname.t
 val java_linked_list_next : Typ.t -> Fieldname.t
 (** Virtual field for next of Java's linked list *)
 
+val java_list_files_length : Fieldname.t
+(** Virtual field for length of Java's files list in a directory *)
+
 val is_cpp_vector_elem : Fieldname.t -> bool
 (** Check if the field is for C++ vector's elements *)
 

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -1340,6 +1340,23 @@ module InputStream = struct
     {exec; check= no_check}
 end
 
+module File = struct
+  let list_files exp =
+    let exec ({integer_type_widths} as model_env) ~ret mem =
+      let locs = Sem.eval integer_type_widths exp mem |> Dom.Val.get_pow_loc in
+      match PowLoc.is_singleton_or_more locs with
+      | Singleton loc ->
+          Loc.append_field loc BufferOverrunField.java_list_files_length
+          |> Loc.get_path
+          |> Option.value_map ~default:mem ~f:(fun path ->
+                 let length = Itv.of_normal_path ~unsigned:true path in
+                 JavaClass.decl_array model_env ~ret length mem )
+      | Empty | More ->
+          mem
+    in
+    {exec; check= no_check}
+end
+
 module FileChannel = struct
   (* https://docs.oracle.com/javase/7/docs/api/java/io/InputStream.html#read(byte[],%20int,%20int) *)
   let read buf_exp =
@@ -1575,6 +1592,7 @@ module Call = struct
       ; +PatternMatch.implements_infer_annotation "Assertions"
         &:: "nullsafeFIXME" <>$ capt_exp $+...$--> id
       ; +PatternMatch.implements_infer_annotation "Assertions" &::.*--> no_model
+      ; +PatternMatch.implements_io "File" &:: "listFiles" <>$ capt_exp $--> File.list_files
       ; +PatternMatch.implements_io "InputStream"
         &:: "read" <>$ any_arg $+ any_arg $+ any_arg $+ capt_exp $--> InputStream.read
       ; +PatternMatch.implements_iterator &:: "hasNext" <>$ capt_exp $!--> Collection.hasNext

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

@@ -5,6 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  */
 import com.google.common.base.Objects;
+import java.io.File;
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.Iterator;
@@ -122,4 +123,9 @@ class ListTest {
     }
     for (int i = 0; i < o.my_size; i++) {}
   }
+
+  void call_list_files_linear(File dir) {
+    File[] files = dir.listFiles();
+    for (File f : files) {}
+  }
 }

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

@@ -247,17 +247,18 @@ codetoanalyze/java/performance/LambdaTest.java, LambdaTest.call_lambda(int):void
 codetoanalyze/java/performance/ListTest.java, ListTest$MyOwnObj.<init>(ListTest), 8,  OnUIThread:false, []
 codetoanalyze/java/performance/ListTest.java, ListTest$MyOwnObj.my_put():void, 5,  OnUIThread:false, []
 codetoanalyze/java/performance/ListTest.java, ListTest.<init>(), 3,  OnUIThread:false, []
-codetoanalyze/java/performance/ListTest.java, ListTest.asList_linear(java.lang.String[]):void, 9 + 8 ⋅ array.length + 3 ⋅ (array.length + 1),  OnUIThread:false, [{array.length + 1},Loop at line 42,{array.length},Loop at line 42]
+codetoanalyze/java/performance/ListTest.java, ListTest.asList_linear(java.lang.String[]):void, 9 + 8 ⋅ array.length + 3 ⋅ (array.length + 1),  OnUIThread:false, [{array.length + 1},Loop at line 43,{array.length},Loop at line 43]
-codetoanalyze/java/performance/ListTest.java, ListTest.call_iterate_elements_linear(java.util.List,java.util.List):void, 26 + 5 ⋅ (l2.length + l1.length) + 3 ⋅ (l2.length + l1.length + 1),  OnUIThread:false, [{l2.length + l1.length + 1},call to void ListTest.iterate_elements_linear(List),Loop at line 59,{l2.length + l1.length},call to void ListTest.iterate_elements_linear(List),Loop at line 59]
+codetoanalyze/java/performance/ListTest.java, ListTest.call_iterate_elements_linear(java.util.List,java.util.List):void, 26 + 5 ⋅ (l2.length + l1.length) + 3 ⋅ (l2.length + l1.length + 1),  OnUIThread:false, [{l2.length + l1.length + 1},call to void ListTest.iterate_elements_linear(List),Loop at line 60,{l2.length + l1.length},call to void ListTest.iterate_elements_linear(List),Loop at line 60]
-codetoanalyze/java/performance/ListTest.java, ListTest.indexOfImpl_linear(java.util.List,java.lang.Object):int, 14 + 11 ⋅ list.length + 3 ⋅ (list.length + 1),  OnUIThread:false, [{list.length + 1},Loop at line 18,{list.length},Loop at line 18]
+codetoanalyze/java/performance/ListTest.java, ListTest.call_list_files_linear(java.io.File):void, 13 + 9 ⋅ dir.list_files_length,  OnUIThread:false, [{dir.list_files_length},Loop at line 129]
-codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list1_linear(java.util.List,java.util.List):void, 19 + 12 ⋅ (l2.length + l1.length) + 3 ⋅ (l2.length + l1.length + 1),  OnUIThread:false, [{l2.length + l1.length + 1},Loop at line 76,{l2.length + l1.length},Loop at line 76]
+codetoanalyze/java/performance/ListTest.java, ListTest.indexOfImpl_linear(java.util.List,java.lang.Object):int, 14 + 11 ⋅ list.length + 3 ⋅ (list.length + 1),  OnUIThread:false, [{list.length + 1},Loop at line 19,{list.length},Loop at line 19]
-codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list2_linear(java.util.List,java.util.List):void, 16 + 8 ⋅ (l2.length + l1.length) + 3 ⋅ (l2.length + l1.length + 1),  OnUIThread:false, [{l2.length + l1.length + 1},Loop at line 88,{l2.length + l1.length},Loop at line 88]
+codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list1_linear(java.util.List,java.util.List):void, 19 + 12 ⋅ (l2.length + l1.length) + 3 ⋅ (l2.length + l1.length + 1),  OnUIThread:false, [{l2.length + l1.length + 1},Loop at line 77,{l2.length + l1.length},Loop at line 77]
-codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list3_linear(java.util.List,java.util.List,java.util.List):void, 20 + 8 ⋅ (l2.length + l1.length + a.length) + 3 ⋅ (l2.length + l1.length + a.length + 1),  OnUIThread:false, [{l2.length + l1.length + a.length + 1},Loop at line 99,{l2.length + l1.length + a.length},Loop at line 99]
+codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list2_linear(java.util.List,java.util.List):void, 16 + 8 ⋅ (l2.length + l1.length) + 3 ⋅ (l2.length + l1.length + 1),  OnUIThread:false, [{l2.length + l1.length + 1},Loop at line 89,{l2.length + l1.length},Loop at line 89]
-codetoanalyze/java/performance/ListTest.java, ListTest.iter_my_own_obj(java.util.List):void, 22 + 14 ⋅ a.length + 6 ⋅ a.length + 3 ⋅ (a.length + 1),  OnUIThread:false, [{a.length + 1},Loop at line 120,{a.length},Loop at line 123,{a.length},Loop at line 120]
+codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list3_linear(java.util.List,java.util.List,java.util.List):void, 20 + 8 ⋅ (l2.length + l1.length + a.length) + 3 ⋅ (l2.length + l1.length + a.length + 1),  OnUIThread:false, [{l2.length + l1.length + a.length + 1},Loop at line 100,{l2.length + l1.length + a.length},Loop at line 100]
-codetoanalyze/java/performance/ListTest.java, ListTest.iter_relation_with_var(java.util.List):void, 11 + 10 ⋅ a.length + 5 ⋅ a.length + 3 ⋅ (a.length + 1),  OnUIThread:false, [{a.length + 1},Loop at line 104,{a.length},Loop at line 107,{a.length},Loop at line 104]
+codetoanalyze/java/performance/ListTest.java, ListTest.iter_my_own_obj(java.util.List):void, 22 + 14 ⋅ a.length + 6 ⋅ a.length + 3 ⋅ (a.length + 1),  OnUIThread:false, [{a.length + 1},Loop at line 121,{a.length},Loop at line 124,{a.length},Loop at line 121]
-codetoanalyze/java/performance/ListTest.java, ListTest.iterate_elements_linear(java.util.List):void, 6 + 5 ⋅ l.length + 3 ⋅ (l.length + 1),  OnUIThread:false, [{l.length + 1},Loop at line 59,{l.length},Loop at line 59]
+codetoanalyze/java/performance/ListTest.java, ListTest.iter_relation_with_var(java.util.List):void, 11 + 10 ⋅ a.length + 5 ⋅ a.length + 3 ⋅ (a.length + 1),  OnUIThread:false, [{a.length + 1},Loop at line 105,{a.length},Loop at line 108,{a.length},Loop at line 105]
+codetoanalyze/java/performance/ListTest.java, ListTest.iterate_elements_linear(java.util.List):void, 6 + 5 ⋅ l.length + 3 ⋅ (l.length + 1),  OnUIThread:false, [{l.length + 1},Loop at line 60,{l.length},Loop at line 60]
 codetoanalyze/java/performance/ListTest.java, ListTest.sort_comparator_nlogn(java.util.List):void, 8 + people.length × log(people.length),  OnUIThread:false, [{people.length},Modeled call to List.sort,{people.length},Modeled call to List.sort]
-codetoanalyze/java/performance/ListTest.java, ListTest.sublist(java.util.List):void, 13 + 8 ⋅ (filesList.length - 1) + 3 ⋅ filesList.length,  OnUIThread:false, [{filesList.length},Loop at line 32,{filesList.length - 1},Loop at line 32]
+codetoanalyze/java/performance/ListTest.java, ListTest.sublist(java.util.List):void, 13 + 8 ⋅ (filesList.length - 1) + 3 ⋅ filesList.length,  OnUIThread:false, [{filesList.length},Loop at line 33,{filesList.length - 1},Loop at line 33]
 codetoanalyze/java/performance/ListTest.java, ListTest.sublist_constant(java.util.List):void, 34,  OnUIThread:false, []
 codetoanalyze/java/performance/ListTest.java, ListTest.two_lists(java.util.List,java.util.List):java.util.List, 13,  OnUIThread:false, []
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops$C.<init>(), 3,  OnUIThread:false, []