[inferbo] Add model for String.substring

Reviewed By: skcho

Differential Revision: D19663254

fbshipit-source-id: 29b711e41

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -1146,6 +1146,41 @@ module JavaString = struct
 
 
   let empty_constructor tgt_exp = copy_constructor tgt_exp (Exp.Const (Const.Cstr ""))
+
+  let create_with_length {pname; node_hash; location; integer_type_widths} ~ret:(id, _) ~begin_idx
+      ~end_v mem =
+    let begin_itv = Sem.eval integer_type_widths begin_idx mem |> Dom.Val.get_itv in
+    let end_itv = Dom.Val.get_itv end_v in
+    let length_itv = Itv.minus end_itv begin_itv in
+    let arr_loc =
+      Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path:None
+        ~represents_multiple_values:false
+      |> Loc.of_allocsite
+    in
+    let elem_alloc =
+      Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None
+        ~represents_multiple_values:true
+    in
+    let traces = Trace.(Set.singleton location ArrayDeclaration) in
+    Dom.Mem.add_stack (Loc.of_id id) (Dom.Val.of_loc arr_loc) mem
+    |> Dom.Mem.add_heap (Loc.append_field arr_loc ~fn)
+         (Dom.Val.of_java_array_alloc elem_alloc ~length:length_itv ~traces)
+
+
+  let substring_no_end exp begin_idx =
+    let exec model_env ~ret mem =
+      create_with_length model_env ~ret ~begin_idx ~end_v:(get_length model_env exp mem) mem
+    in
+    {exec; check= no_check}
+
+
+  let substring begin_idx end_idx =
+    let exec ({integer_type_widths} as model_env) ~ret mem =
+      create_with_length model_env ~ret ~begin_idx
+        ~end_v:(Sem.eval integer_type_widths end_idx mem)
+        mem
+    in
+    {exec; check= no_check}
 end
 
 module Preconditions = struct
@@ -1282,6 +1317,10 @@ module Call = struct
         &:: "split" <>$ any_arg $+ any_arg $+ capt_exp $--> JavaString.split_with_limit
       ; +PatternMatch.implements_lang "String"
         &:: "split" <>$ capt_exp $+ any_arg $--> JavaString.split
+      ; +PatternMatch.implements_lang "String"
+        &:: "substring" <>$ capt_exp $+ capt_exp $--> JavaString.substring_no_end
+      ; +PatternMatch.implements_lang "CharSequence"
+        &:: "substring" <>$ any_arg $+ capt_exp $+ capt_exp $--> JavaString.substring
       ; -"strcpy" <>$ capt_exp $+ capt_exp $+...$--> strcpy
       ; -"strncpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> strncpy
       ; -"snprintf" <>--> snprintf

infer/tests/codetoanalyze/java/performance/StringTest.java

@@ -75,4 +75,14 @@ class StringTest {
     String s = new String();
     string_constructor_linear(s);
   }
+
+  public void substring_no_end_linear(String s, int x) {
+    String sub = s.substring(x);
+    for (int i = 0; i < sub.length(); i++) {}
+  }
+
+  public void substring_linear(String s, int x, int y) {
+    String sub = s.substring(x, y);
+    for (int i = 0; i < sub.length(); i++) {}
+  }
 }

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -204,6 +204,8 @@ codetoanalyze/java/performance/StringTest.java, StringTest.indexof_quadratic(jav
 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/StringTest.java, StringTest.substring_linear(java.lang.String,int,int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 8 ⋅ (-x + y), O((-x + y)), degree = 1,{-x + y},Loop at line 86]
+codetoanalyze/java/performance/StringTest.java, StringTest.substring_no_end_linear(java.lang.String,int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 9 + 8 ⋅ (-x + s.length), O((-x + s.length)), degree = 1,{-x + s.length},Loop at line 81]
 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]