From 7cb11b587a9b88cb12c383d3fc27f4570b44b66f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Mon, 27 Jan 2020 07:24:47 -0800 Subject: [PATCH] [inferbo] Revise String.split's bounds Summary: `String.split(regexp)` returns an array that is split by the given regexp. If the regexp doesn't match, the original string is returned. Hence, the resulting array's length must be in `[1, max(1, n_u -1)]` where`n_u` is the upper bound of the string's length. Reviewed By: dulmarod Differential Revision: D19578318 fbshipit-source-id: 675af7376 --- infer/src/bufferoverrun/bufferOverrunModels.ml | 12 +++++++----- .../tests/codetoanalyze/java/performance/issues.exp | 4 ++-- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 5dabaf235..d16ac4abe 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -1067,9 +1067,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 + (** Given a string of length n, return itv [1, max(1, n_u -1)]. *) + let range_itv_one_max_one_mone v = + let itv_mone = BufferOverrunDomain.Val.get_itv v |> Itv.decr in + let max_length_mone = Itv.max_sem ~use_minmax_bound:true itv_mone (Itv.of_int 1) in + Itv.set_lb Itv.Bound.one max_length_mone let indexOf exp = @@ -1107,7 +1109,7 @@ module JavaString = struct 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 + ArrObjCommon.eval_size model_env exp ~fn mem |> range_itv_one_max_one_mone |> Dom.Val.of_itv in malloc_and_set_length exp model_env ~ret length mem in @@ -1118,7 +1120,7 @@ module JavaString = struct 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 + Sem.eval integer_type_widths dummy_exp mem |> range_itv_one_max_one_mone |> Dom.Val.of_itv in malloc_and_set_length limit_exp model_env ~ret length mem in diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index c22fea572..c3aa3edc7 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -200,8 +200,8 @@ 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.split_linear(java.lang.String):void, 1, 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, 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.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/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]