[inferbo] Add model for String.split

Reviewed By: skcho

Differential Revision: D19141055

fbshipit-source-id: a5257b2f8

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

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);
+  }
 }

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]