From c51f47b05e0036a4bb64ad068e1017c3f0af9115 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Mon, 3 Feb 2020 07:01:26 -0800 Subject: [PATCH] [inferbo] Revise Java's String constructor models Summary: Java's String models were broken for - initializing a String object with a locally defined constant string (which is an `Object*` in SIL). - initializing a String object with a `char`/`byte` array This diff fixes them and also adds models for `new String ()`. Reviewed By: skcho Differential Revision: D19662180 fbshipit-source-id: 23968d0aa --- .../src/bufferoverrun/bufferOverrunModels.ml | 40 +++++++++++++------ .../java/performance/StringTest.java | 26 ++++++++++++ .../codetoanalyze/java/performance/issues.exp | 2 + 3 files changed, 55 insertions(+), 13 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index d16ac4abe..26d601e26 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -1089,10 +1089,14 @@ module JavaString = struct ArrObjCommon.constructor_from_char_ptr model_env tgt_deref ~fn src mem - (* https://docs.oracle.com/javase/7/docs/api/java/lang/String.html#String(byte[]) *) - let constructor tgt_exp src = - let exec model_env ~ret:_ mem = - constructor_from_char_ptr model_env (Sem.eval_locs tgt_exp mem) src mem + (* https://docs.oracle.com/javase/7/docs/api/java/lang/String.html#String(char[]) *) + (* same for byte[]*) + let constructor_from_array tgt_exp arr_exp = + let exec {integer_type_widths} ~ret:_ mem = + let tgt_locs = Sem.eval_locs tgt_exp mem in + let deref_of_tgt = PowLoc.append_field tgt_locs ~fn in + let src_arr_locs = Dom.Val.get_all_locs (Sem.eval_arr integer_type_widths arr_exp mem) in + Dom.Mem.update_mem deref_of_tgt (Dom.Mem.find_set src_arr_locs mem) mem in {exec; check= no_check} @@ -1128,13 +1132,20 @@ module JavaString = struct (* https://docs.oracle.com/javase/7/docs/api/java/lang/String.html#String(java.lang.String) *) - let copy_constructor vec_exp src_exp = + let copy_constructor tgt_exp src_exp = let exec ({integer_type_widths} as model_env) ~ret:_ mem = - let vec_locs = Sem.eval integer_type_widths vec_exp mem |> Dom.Val.get_all_locs in - let deref_of_vec = PowLoc.append_field vec_locs ~fn in - ArrObjCommon.copy_constructor model_env deref_of_vec ~fn src_exp mem + let tgt_deref = Sem.eval integer_type_widths tgt_exp mem |> Dom.Val.get_all_locs in + let elem_locs = PowLoc.append_field tgt_deref ~fn in + match src_exp with + | Exp.Const (Const.Cstr s) -> + BoUtils.Exec.decl_string model_env ~do_alloc:true elem_locs s mem + | _ -> + ArrObjCommon.copy_constructor model_env elem_locs ~fn src_exp mem in {exec; check= no_check} + + + let empty_constructor tgt_exp = copy_constructor tgt_exp (Exp.Const (Const.Cstr "")) end module Preconditions = struct @@ -1206,7 +1217,9 @@ 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 char_ptr = Typ.mk (Typ.Tptr (Typ.mk (Typ.Tint Typ.IChar), Pk_pointer)) 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 make_dispatcher [ -"__exit" <>--> bottom ; -"CFArrayCreate" <>$ any_arg $+ capt_exp $+ capt_exp $+...$--> CFArray.create_array @@ -1255,11 +1268,12 @@ module Call = struct ; +PatternMatch.implements_lang "String" &:: "charAt" <>$ capt_exp $+ capt_exp $--> JavaString.charAt ; +PatternMatch.implements_lang "String" - &:: "" <>$ capt_exp - $+ capt_exp_of_typ (+PatternMatch.implements_lang "String") - $--> JavaString.copy_constructor + &:: "" <>$ capt_exp $+ capt_exp_of_prim_typ char_array + $--> JavaString.constructor_from_array + ; +PatternMatch.implements_lang "String" + &:: "" <>$ capt_exp $+ capt_exp $--> JavaString.copy_constructor ; +PatternMatch.implements_lang "String" - &:: "" <>$ capt_exp $+ capt_exp $--> JavaString.constructor + &:: "" <>$ capt_exp $--> JavaString.empty_constructor ; +PatternMatch.implements_lang "String" &:: "concat" <>$ capt_exp $+ capt_exp $+...$--> JavaString.concat ; +PatternMatch.implements_lang "String" diff --git a/infer/tests/codetoanalyze/java/performance/StringTest.java b/infer/tests/codetoanalyze/java/performance/StringTest.java index 89beda226..d1cdcae95 100644 --- a/infer/tests/codetoanalyze/java/performance/StringTest.java +++ b/infer/tests/codetoanalyze/java/performance/StringTest.java @@ -49,4 +49,30 @@ class StringTest { String s = new String("hello"); split_linear(s); } + + void byte_array_constructor_linear(byte[] data) { + String s = new String(data); + for (int i = 0; i < s.length(); i++) {} + } + + void call_string_constant() { + byte[] data = new byte[10]; + byte_array_constructor_linear(data); + } + + void string_constructor_constant() { + String s = "abcd"; + String str = new String(s); + for (int i = 0; i < str.length(); i++) {} + } + + void string_constructor_linear(String s) { + String str = new String(s); + for (int i = 0; i < str.length(); i++) {} + } + + void call_string_constructor_constant() { + String s = new String(); + string_constructor_linear(s); + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index c3aa3edc7..4ef036d0e 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -196,12 +196,14 @@ codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.Mat codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.max2_symbolic(int,int):void, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 9 ⋅ (max(x, y)), O((max(x, y))), degree = 1,{max(x, y)},Loop at line 20] codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.max_symbolic(int[]):void, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ arr.length + 4 ⋅ (arr.length + 1), O(arr.length), degree = 1,{arr.length + 1},Loop at line 16,{arr.length},Loop at line 16] codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.checkNotNull_linear(java.util.ArrayList,java.lang.Object):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 11 + 8 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 37,{list.length},Loop at line 37] +codetoanalyze/java/performance/StringTest.java, StringTest.byte_array_constructor_linear(byte[]):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ data.length + 3 ⋅ (data.length + 1), O(data.length), degree = 1,{data.length + 1},Loop at line 55,{data.length},Loop at line 55] codetoanalyze/java/performance/StringTest.java, StringTest.index_substring_linear():java.lang.String, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 9 + this.mId.length, O(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, 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.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/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]