[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

@@ -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]. *)
+  (** Given a string of length n, return itv [1, max(1, n_u -1)]. *)
-  let range_itv_one_mone v =
+  let range_itv_one_max_one_mone v =
-    BufferOverrunDomain.Val.get_itv v |> Itv.decr |> Itv.set_lb Itv.Bound.one
+    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

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_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.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]