From 0682ccc1e90656a847b86808787921a0d8225bd4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Thu, 18 Jul 2019 06:06:42 -0700 Subject: [PATCH] [cost][inferbo] Add models for indexOf Reviewed By: skcho Differential Revision: D16089480 fbshipit-source-id: 1065a1830 --- .../src/bufferoverrun/bufferOverrunModels.ml | 15 +++++ infer/src/checkers/costModels.ml | 59 ++++++++++++++++++- .../java/performance/StringTest.java | 32 ++++++++++ .../codetoanalyze/java/performance/issues.exp | 4 ++ 4 files changed, 107 insertions(+), 3 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/performance/StringTest.java diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 045bfa36a..213eeb88a 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -357,6 +357,20 @@ let inferbo_set_size src_exp size_exp = let model_by_value value id mem = Dom.Mem.add_stack (Loc.of_id id) value mem +(** Given a string of length n, return itv [-1, n_u-1]. *) +let range_itv_mone exp mem = + eval_string_len exp mem |> BufferOverrunDomain.Val.get_itv |> Itv.set_lb_zero |> Itv.decr + + +let indexOf exp = + let exec _ ~ret:(ret_id, _) mem = + (* if not found, indexOf returns -1. *) + let v = range_itv_mone exp mem |> Dom.Val.of_itv in + model_by_value v ret_id mem + in + {exec; check= no_check} + + let cast exp = let exec {integer_type_widths} ~ret:(ret_id, _) mem = let itv = Sem.eval integer_type_widths exp mem in @@ -877,6 +891,7 @@ module Call = struct ; -"strcat" <>$ capt_exp $+ capt_exp $+...$--> strcat ; +PatternMatch.implements_lang "String" &:: "concat" <>$ capt_exp $+ capt_exp $+...$--> strcat + ; +PatternMatch.implements_lang "String" &:: "indexOf" <>$ capt_exp $+ any_arg $--> indexOf ; -"strcpy" <>$ capt_exp $+ capt_exp $+...$--> strcpy ; -"strncpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> strncpy ; -"snprintf" <>--> snprintf diff --git a/infer/src/checkers/costModels.ml b/infer/src/checkers/costModels.ml index 688a152ba..cccd38312 100644 --- a/infer/src/checkers/costModels.ml +++ b/infer/src/checkers/costModels.ml @@ -50,6 +50,19 @@ let modeled ~of_function {pname; location} ~ret:(_, ret_typ) _ : BasicCost.t = of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function location +(** Given a string of length n and an optional starting index i (0 by + default), return itv [0, n_u-i_l] *) +let string_len_range_itv exp ~from mem = + let itv = BufferOverrunModels.eval_string_len exp mem |> BufferOverrunDomain.Val.get_itv in + Option.value_map from ~default:itv ~f:(fun (start_exp, integer_type_widths) -> + let start_itv = + BufferOverrunSemantics.eval integer_type_widths start_exp mem + |> BufferOverrunDomain.Val.get_itv + in + Itv.minus itv start_itv ) + |> Itv.set_lb_zero + + module BoundsOf (Container : S) = struct let of_length exp {location} ~ret:_ mem ~of_function ~degree_kind = let itv = Container.length exp mem |> BufferOverrunDomain.Val.get_itv in @@ -66,7 +79,7 @@ module BoundsOf (Container : S) = struct BasicCost.mult n log_n end -module String = struct +module JavaString = struct let substring_aux ~begin_idx ~end_v {integer_type_widths; location} inferbo_mem = let begin_v = BufferOverrunSemantics.eval integer_type_widths begin_idx inferbo_mem in let itv = @@ -85,6 +98,36 @@ module String = struct substring_aux ~begin_idx ~end_v:(BufferOverrunSemantics.eval integer_type_widths end_idx inferbo_mem) model_env inferbo_mem + + + (** O(|m|) where m is the given string and |.| is the length function *) + let indexOf_char exp {location} ~ret:_ inferbo_mem = + let itv = string_len_range_itv exp ~from:None inferbo_mem in + of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.indexOf" location + + + (** O(|m|-|n|) where m is the given string and n is the index to start searching from *) + let indexOf_char_starting_from exp start_exp {integer_type_widths; location} ~ret:_ inferbo_mem = + let itv = string_len_range_itv exp ~from:(Some (start_exp, integer_type_widths)) inferbo_mem in + of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.indexOf" location + + + (** O(|m|.|n|) where m and n are the given strings *) + let indexOf_str exp index_exp {location} ~ret:_ inferbo_mem = + let itv = + BufferOverrunModels.eval_string_len exp inferbo_mem |> BufferOverrunDomain.Val.get_itv + in + let index_itv = + BufferOverrunModels.eval_string_len index_exp inferbo_mem |> BufferOverrunDomain.Val.get_itv + in + let n = + of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.indexOf" location + in + let m = + of_itv ~itv:index_itv ~degree_kind:Polynomials.DegreeKind.Linear + ~of_function:"String.indexOf" location + in + BasicCost.mult n m end module BoundsOfCollection = BoundsOf (Collection) @@ -93,6 +136,7 @@ module BoundsOfArray = BoundsOf (Array) module Call = struct let dispatch : (Tenv.t, model) ProcnameDispatcher.Call.dispatcher = let open ProcnameDispatcher.Call in + let int_typ = Typ.mk (Typ.Tint Typ.IInt) in make_dispatcher [ +PatternMatch.implements_collections &:: "sort" $ capt_exp @@ -131,11 +175,20 @@ module Call = struct &:: "shuffle" <>$ capt_exp $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.shuffle" ; +PatternMatch.implements_lang "String" - &:: "substring" <>$ capt_exp $+ capt_exp $--> String.substring + &:: "substring" <>$ capt_exp $+ capt_exp $--> JavaString.substring + ; +PatternMatch.implements_lang "String" + &:: "indexOf" <>$ capt_exp + $+ capt_exp_of_typ (+PatternMatch.implements_lang "String") + $--> JavaString.indexOf_str + ; +PatternMatch.implements_lang "String" + &:: "indexOf" <>$ capt_exp $+ any_arg_of_prim_typ int_typ $+ capt_exp + $--> JavaString.indexOf_char_starting_from + ; +PatternMatch.implements_lang "String" + &:: "indexOf" <>$ capt_exp $+ any_arg_of_prim_typ int_typ $--> JavaString.indexOf_char ; +PatternMatch.implements_lang "String" &:: "substring" $ any_arg_of_typ (+PatternMatch.implements_lang "String") - $+ capt_exp $+ capt_exp $--> String.substring_no_end + $+ capt_exp $+ capt_exp $--> JavaString.substring_no_end ; +PatternMatch.implements_inject "Provider" &:: "get" <>--> modeled ~of_function:"Provider.get" ] diff --git a/infer/tests/codetoanalyze/java/performance/StringTest.java b/infer/tests/codetoanalyze/java/performance/StringTest.java new file mode 100644 index 000000000..e41d5c660 --- /dev/null +++ b/infer/tests/codetoanalyze/java/performance/StringTest.java @@ -0,0 +1,32 @@ +/* + * 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. + */ +class StringTest { + + String mId; + + int indexof_linear(String m) { + return m.indexOf('_'); + } + + int indexof_from_linear(String m, int j) { + return m.indexOf('_', j); + } + + int indexof_quadratic(String m, String n) { + return m.indexOf(n); + } + + int indexof_constant(String n) { + String m = "hi"; + return m.indexOf('i'); + } + + public String index_substring_linear() { + int index = indexof_linear(mId); + return mId.substring(0, index); + } +} diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index ff8db5cd0..037327381 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -156,6 +156,10 @@ codetoanalyze/java/performance/MapTest.java, MapTest.entrySet_linear(java.util.M codetoanalyze/java/performance/MapTest.java, MapTest.keySet_linear(java.util.Map):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 8 ⋅ (map.length - 1) + 3 ⋅ map.length, degree = 1,{map.length},Loop at line 13,{map.length - 1},Loop at line 13] codetoanalyze/java/performance/MapTest.java, MapTest.putAll_linear(java.util.Map):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 13 + 8 ⋅ (map.length - 1) + 3 ⋅ map.length, degree = 1,{map.length},Loop at line 28,{map.length - 1},Loop at line 28] codetoanalyze/java/performance/MapTest.java, MapTest.values_linear(java.util.Map):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 13 + 8 ⋅ map.length + 3 ⋅ (map.length + 1), degree = 1,{map.length + 1},Loop at line 22,{map.length},Loop at line 22] +codetoanalyze/java/performance/StringTest.java, StringTest.index_substring_linear():java.lang.String, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 9 + this.mId.length, degree = 1,{this.mId.length},call to int StringTest.indexof_linear(String),Modeled call to String.indexOf] +codetoanalyze/java/performance/StringTest.java, StringTest.indexof_from_linear(java.lang.String,int):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + (-j + m.length), degree = 1,{-j + m.length},Modeled call to String.indexOf] +codetoanalyze/java/performance/StringTest.java, StringTest.indexof_linear(java.lang.String):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + m.length, degree = 1,{m.length},Modeled call to String.indexOf] +codetoanalyze/java/performance/StringTest.java, StringTest.indexof_quadratic(java.lang.String,java.lang.String):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + m.length × n.length, degree = 2,{n.length},Modeled call to String.indexOf,{m.length},Modeled call to String.indexOf] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 798, degree = 0] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.vanilla_switch(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]