diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 36f602848..fb128d582 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -1059,6 +1059,11 @@ module JavaString = struct |> BufferOverrunDomain.Val.get_itv |> Itv.set_lb_zero |> Itv.decr + (** Given a string of length n, return itv [1, n_u -1]. *) + let range_itv_one_mone v = + BufferOverrunDomain.Val.get_itv v |> Itv.decr |> Itv.set_lb Itv.Bound.one + + let indexOf exp = let exec model_env ~ret:(ret_id, _) mem = (* if not found, indexOf returns -1. *) @@ -1082,6 +1087,36 @@ module JavaString = struct {exec; check= no_check} + let malloc_and_set_length exp ({location} as model_env) ~ret:((id, _) as ret) length mem = + let {exec} = malloc ~can_be_zero:false exp in + let mem = exec model_env ~ret mem in + let underlying_arr_loc = Dom.Mem.find_stack (Loc.of_id id) mem |> Dom.Val.get_pow_loc in + Dom.Mem.transform_mem ~f:(Dom.Val.set_array_length location ~length) underlying_arr_loc mem + + + (** If the expression does not match any part of the input then the resulting array has just one + element. *) + let split exp = + let exec model_env ~ret mem = + let length = + ArrObjCommon.eval_size model_env exp ~fn mem |> range_itv_one_mone |> Dom.Val.of_itv + in + malloc_and_set_length exp model_env ~ret length mem + in + {exec; check= no_check} + + + let split_with_limit limit_exp = + let exec ({integer_type_widths} as model_env) ~ret mem = + let dummy_exp = Exp.zero in + let length = + Sem.eval integer_type_widths dummy_exp mem |> range_itv_one_mone |> Dom.Val.of_itv + in + malloc_and_set_length limit_exp model_env ~ret length mem + in + {exec; check= no_check} + + (* https://docs.oracle.com/javase/7/docs/api/java/lang/String.html#String(java.lang.String) *) let copy_constructor vec_exp src_exp = let exec ({integer_type_widths} as model_env) ~ret:_ mem = @@ -1219,6 +1254,10 @@ module Call = struct &:: "concat" <>$ capt_exp $+ capt_exp $+...$--> JavaString.concat ; +PatternMatch.implements_lang "String" &:: "indexOf" <>$ capt_exp $+ any_arg $--> JavaString.indexOf + ; +PatternMatch.implements_lang "String" + &:: "split" <>$ any_arg $+ any_arg $+ capt_exp $--> JavaString.split_with_limit + ; +PatternMatch.implements_lang "String" + &:: "split" <>$ capt_exp $+ any_arg $--> JavaString.split ; -"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 c6654fd9e..89beda226 100644 --- a/infer/tests/codetoanalyze/java/performance/StringTest.java +++ b/infer/tests/codetoanalyze/java/performance/StringTest.java @@ -34,4 +34,19 @@ class StringTest { String s = ""; return s.startsWith(",") ? s.substring(1) : s; } + + void split_linear(String s) { + String[] list = s.split(","); + for (int i = 0; i < list.length; i++) {} + } + + void split_with_limit_linear(String s, int limit) { + String[] list = s.split(",", limit); + for (int i = 0; i < list.length; i++) {} + } + + void call_split_constant() { + String s = new String("hello"); + split_linear(s); + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 83a429c22..d06cc9c65 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -197,6 +197,8 @@ codetoanalyze/java/performance/StringTest.java, StringTest.index_substring_linea 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), 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, 1, 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, 1, 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, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ (s.length - 1), O(s.length), degree = 1,{s.length - 1},Loop at line 40] +codetoanalyze/java/performance/StringTest.java, StringTest.split_with_limit_linear(java.lang.String,int):void, 2, 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/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, O(1), degree = 0] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.vanilla_switch(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]