diff --git a/infer/src/absint/ProcnameDispatcher.ml b/infer/src/absint/ProcnameDispatcher.ml index c2137b1ff..4f49b342a 100644 --- a/infer/src/absint/ProcnameDispatcher.ml +++ b/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 >! () diff --git a/infer/src/absint/ProcnameDispatcher.mli b/infer/src/absint/ProcnameDispatcher.mli index 76b2d9dde..6a265a21d 100644 --- a/infer/src/absint/ProcnameDispatcher.mli +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 5c18c0e28..9c99b55c5 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/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 - let get_int buf_exp = +module Buffer = struct + 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" &:: "" <>$ 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" - &:: "get" <>$ capt_exp $--> ByteBuffer.get_int - ; +PatternMatch.Java.implements_nio "ByteBuffer" - &:: "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 "Buffer" + &::+ startsWith "get" <>$ capt_exp $+...$--> Buffer.get + ; +PatternMatch.Java.implements_nio "Buffer" &:: "duplicate" <>$ capt_exp $+...$--> id ; +PatternMatch.Java.implements_nio "channels.FileChannel" &:: "read" <>$ any_arg $+ capt_exp $+ any_arg $--> FileChannel.read ; +PatternMatch.Java.implements_org_json "JSONArray" diff --git a/infer/src/bufferoverrun/bufferOverrunTypModels.ml b/infer/src/bufferoverrun/bufferOverrunTypModels.ml index 7d8432090..a6d759ed4 100644 --- a/infer/src/bufferoverrun/bufferOverrunTypModels.ml +++ b/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 ] diff --git a/infer/src/checkers/purityModels.ml b/infer/src/checkers/purityModels.ml index 354b6da9c..e27d1d1cc 100644 --- a/infer/src/checkers/purityModels.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/java/performance/BufferTest.java b/infer/tests/codetoanalyze/java/performance/BufferTest.java new file mode 100644 index 000000000..9798ded81 --- /dev/null +++ b/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); + } + } +} diff --git a/infer/tests/codetoanalyze/java/performance/Loops.java b/infer/tests/codetoanalyze/java/performance/Loops.java index 95f161677..5d4cf2160 100644 --- a/infer/tests/codetoanalyze/java/performance/Loops.java +++ b/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 { diff --git a/infer/tests/codetoanalyze/java/performance/cost-issues.exp b/infer/tests/codetoanalyze/java/performance/cost-issues.exp index 4ee99a1eb..48b51642c 100644 --- a/infer/tests/codetoanalyze/java/performance/cost-issues.exp +++ b/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.(), 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.(), 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] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 60c713deb..7e05837bf 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/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, [,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,,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, [,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, [,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, [,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]