From 545e6c88028bd52f9d3aee347d4a2b7258c013bb Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 12 Mar 2020 02:19:41 -0700 Subject: [PATCH] [inferbo] Add models of String.lastIndexOf and String.replace Reviewed By: ezgicicek Differential Revision: D20387528 fbshipit-source-id: 2b52f682c --- .../src/bufferoverrun/bufferOverrunModels.ml | 11 ++++++++- .../java/performance/StringTest.java | 23 +++++++++++++++++++ .../codetoanalyze/java/performance/issues.exp | 3 +++ 3 files changed, 36 insertions(+), 1 deletion(-) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 400ca7da0..673cd32bc 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -1194,6 +1194,9 @@ module JavaString = struct mem in {exec; check= no_check} + + + let replace = id end module Preconditions = struct @@ -1265,6 +1268,7 @@ module Call = struct let std_array0 = mk_std_array () in let std_array1 = mk_std_array () in let std_array2 = mk_std_array () in + let int_typ = Typ.mk (Typ.Tint Typ.IInt) in let char_typ = Typ.mk (Typ.Tint Typ.IChar) in let char_ptr = Typ.mk (Typ.Tptr (char_typ, Pk_pointer)) in let char_array = Typ.mk (Typ.Tptr (Typ.mk_array char_typ, Pk_pointer)) in @@ -1326,7 +1330,12 @@ module Call = struct ; +PatternMatch.implements_lang "String" &:: "concat" <>$ capt_exp $+ capt_exp $+...$--> JavaString.concat ; +PatternMatch.implements_lang "String" - &:: "indexOf" <>$ capt_exp $+ any_arg $--> JavaString.indexOf + &:: "indexOf" <>$ capt_exp $+ any_arg $+...$--> JavaString.indexOf + ; +PatternMatch.implements_lang "String" + &:: "lastIndexOf" <>$ capt_exp $+ any_arg $+...$--> JavaString.indexOf + ; +PatternMatch.implements_lang "String" + &:: "replace" <>$ capt_exp $+ any_arg_of_prim_typ int_typ $+ any_arg_of_prim_typ int_typ + $--> JavaString.replace ; +PatternMatch.implements_lang "String" &:: "split" <>$ any_arg $+ any_arg $+ capt_exp $--> JavaString.split_with_limit ; +PatternMatch.implements_lang "String" diff --git a/infer/tests/codetoanalyze/java/performance/StringTest.java b/infer/tests/codetoanalyze/java/performance/StringTest.java index 58463b83d..fc05aec80 100644 --- a/infer/tests/codetoanalyze/java/performance/StringTest.java +++ b/infer/tests/codetoanalyze/java/performance/StringTest.java @@ -85,4 +85,27 @@ class StringTest { String sub = s.substring(x, y); for (int i = 0; i < sub.length(); i++) {} } + + public void replace_linear(String s) { + String r = s.replace('.', '/'); + for (int i = 0; i < r.length(); i++) {} + } + + public void last_index_of_linear(String s) { + int j = s.lastIndexOf('/'); + for (int i = 0; i < j; i++) {} + } + + boolean unknown_bool; + + public void last_index_of_linear_FP(String s) { + int i = s.lastIndexOf('/'); + while (i > 0) { + int j = s.lastIndexOf('/', i - 1); + if (j > 0) { + break; + } + i = j; + } + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 6bbc20e8d..870aad55c 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -189,6 +189,9 @@ codetoanalyze/java/performance/StringTest.java, StringTest.index_substring_linea codetoanalyze/java/performance/StringTest.java, StringTest.indexof_from_linear(java.lang.String,int):int, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + (-j + m.length), O((-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, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + m.length, O(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, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + m.length × n.length, O(m.length × n.length), degree = 2,{n.length},Modeled call to String.indexOf,{m.length},Modeled call to String.indexOf] +codetoanalyze/java/performance/StringTest.java, StringTest.last_index_of_linear(java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ (s.length - 1), O(s.length), degree = 1,{s.length - 1},Loop at line 96] +codetoanalyze/java/performance/StringTest.java, StringTest.last_index_of_linear_FP(java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 6 ⋅ (s.length - 1) × (s.length + 1) + 4 ⋅ (1+min(1, s.length))², O(s.length²), degree = 2,{1+min(1, s.length)},Loop at line 103,{1+min(1, s.length)},Loop at line 103,{s.length + 1},Loop at line 103,{s.length - 1},Loop at line 103] +codetoanalyze/java/performance/StringTest.java, StringTest.replace_linear(java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ s.length + 3 ⋅ (s.length + 1), O(s.length), degree = 1,{s.length + 1},Loop at line 91,{s.length},Loop at line 91] codetoanalyze/java/performance/StringTest.java, StringTest.split_linear(java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ (-1+max(2, s.length)), O(s.length), degree = 1,{-1+max(2, s.length)},Loop at line 40] codetoanalyze/java/performance/StringTest.java, StringTest.split_with_limit_linear(java.lang.String,int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 6 ⋅ (max(1, limit)), O(limit), degree = 1,{max(1, limit)},Loop at line 45] codetoanalyze/java/performance/StringTest.java, StringTest.string_constructor_linear(java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ s.length + 3 ⋅ (s.length + 1), O(s.length), degree = 1,{s.length + 1},Loop at line 71,{s.length},Loop at line 71]