From 6a38121b8a4be68aff653b26d67682a80fbdc5f8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Mon, 3 Feb 2020 07:01:30 -0800 Subject: [PATCH] [inferbo] Add model for String.substring Reviewed By: skcho Differential Revision: D19663254 fbshipit-source-id: 29b711e41 --- .../src/bufferoverrun/bufferOverrunModels.ml | 39 +++++++++++++++++++ .../java/performance/StringTest.java | 10 +++++ .../codetoanalyze/java/performance/issues.exp | 2 + 3 files changed, 51 insertions(+) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 26d601e26..8aafd638f 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -1146,6 +1146,41 @@ module JavaString = struct let empty_constructor tgt_exp = copy_constructor tgt_exp (Exp.Const (Const.Cstr "")) + + let create_with_length {pname; node_hash; location; integer_type_widths} ~ret:(id, _) ~begin_idx + ~end_v mem = + let begin_itv = Sem.eval integer_type_widths begin_idx mem |> Dom.Val.get_itv in + let end_itv = Dom.Val.get_itv end_v in + let length_itv = Itv.minus end_itv begin_itv in + let arr_loc = + Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path:None + ~represents_multiple_values:false + |> Loc.of_allocsite + in + let elem_alloc = + Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None + ~represents_multiple_values:true + in + let traces = Trace.(Set.singleton location ArrayDeclaration) in + Dom.Mem.add_stack (Loc.of_id id) (Dom.Val.of_loc arr_loc) mem + |> Dom.Mem.add_heap (Loc.append_field arr_loc ~fn) + (Dom.Val.of_java_array_alloc elem_alloc ~length:length_itv ~traces) + + + let substring_no_end exp begin_idx = + let exec model_env ~ret mem = + create_with_length model_env ~ret ~begin_idx ~end_v:(get_length model_env exp mem) mem + in + {exec; check= no_check} + + + let substring begin_idx end_idx = + let exec ({integer_type_widths} as model_env) ~ret mem = + create_with_length model_env ~ret ~begin_idx + ~end_v:(Sem.eval integer_type_widths end_idx mem) + mem + in + {exec; check= no_check} end module Preconditions = struct @@ -1282,6 +1317,10 @@ module Call = struct &:: "split" <>$ any_arg $+ any_arg $+ capt_exp $--> JavaString.split_with_limit ; +PatternMatch.implements_lang "String" &:: "split" <>$ capt_exp $+ any_arg $--> JavaString.split + ; +PatternMatch.implements_lang "String" + &:: "substring" <>$ capt_exp $+ capt_exp $--> JavaString.substring_no_end + ; +PatternMatch.implements_lang "CharSequence" + &:: "substring" <>$ any_arg $+ capt_exp $+ capt_exp $--> JavaString.substring ; -"strcpy" <>$ capt_exp $+ capt_exp $+...$--> strcpy ; -"strncpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> strncpy ; -"snprintf" <>--> snprintf diff --git a/infer/tests/codetoanalyze/java/performance/StringTest.java b/infer/tests/codetoanalyze/java/performance/StringTest.java index d1cdcae95..58463b83d 100644 --- a/infer/tests/codetoanalyze/java/performance/StringTest.java +++ b/infer/tests/codetoanalyze/java/performance/StringTest.java @@ -75,4 +75,14 @@ class StringTest { String s = new String(); string_constructor_linear(s); } + + public void substring_no_end_linear(String s, int x) { + String sub = s.substring(x); + for (int i = 0; i < sub.length(); i++) {} + } + + public void substring_linear(String s, int x, int y) { + String sub = s.substring(x, y); + for (int i = 0; i < sub.length(); i++) {} + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 4ef036d0e..20cf4675e 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -204,6 +204,8 @@ codetoanalyze/java/performance/StringTest.java, StringTest.indexof_quadratic(jav 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] +codetoanalyze/java/performance/StringTest.java, StringTest.substring_linear(java.lang.String,int,int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 8 ⋅ (-x + y), O((-x + y)), degree = 1,{-x + y},Loop at line 86] +codetoanalyze/java/performance/StringTest.java, StringTest.substring_no_end_linear(java.lang.String,int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 9 + 8 ⋅ (-x + s.length), O((-x + s.length)), degree = 1,{-x + s.length},Loop at line 81] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 798, O(1), degree = 0] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.vanilla_switch(int):void, 0, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]