From 1745bf9dd01c15db64c706b1e98efbea523404dc Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 1 Jul 2020 08:34:56 -0700 Subject: [PATCH] [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 | 2 ++ .../src/bufferoverrun/bufferOverrunField.mli | 3 +++ .../src/bufferoverrun/bufferOverrunModels.ml | 18 ++++++++++++++++ .../java/performance/ListTest.java | 6 ++++++ .../java/performance/cost-issues.exp | 21 ++++++++++--------- 5 files changed, 40 insertions(+), 10 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunField.ml b/infer/src/bufferoverrun/bufferOverrunField.ml index ca69f4dfd..ff899c6e2 100644 --- a/infer/src/bufferoverrun/bufferOverrunField.ml +++ b/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 () = diff --git a/infer/src/bufferoverrun/bufferOverrunField.mli b/infer/src/bufferoverrun/bufferOverrunField.mli index 477fbde76..01c8ba001 100644 --- a/infer/src/bufferoverrun/bufferOverrunField.mli +++ b/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 *) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index cacae3768..e1ab08f09 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/java/performance/ListTest.java b/infer/tests/codetoanalyze/java/performance/ListTest.java index a95c6aa71..5e8dae8d5 100644 --- a/infer/tests/codetoanalyze/java/performance/ListTest.java +++ b/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) {} + } } diff --git a/infer/tests/codetoanalyze/java/performance/cost-issues.exp b/infer/tests/codetoanalyze/java/performance/cost-issues.exp index 6cae384f1..8b40c713b 100644 --- a/infer/tests/codetoanalyze/java/performance/cost-issues.exp +++ b/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.(ListTest), 8, OnUIThread:false, [] codetoanalyze/java/performance/ListTest.java, ListTest$MyOwnObj.my_put():void, 5, OnUIThread:false, [] codetoanalyze/java/performance/ListTest.java, ListTest.(), 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.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.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.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.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_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_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_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.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.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 60,{l2.length + l1.length},call to void ListTest.iterate_elements_linear(List),Loop at line 60] +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.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_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_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_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_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.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.(), 3, OnUIThread:false, []