[inferbo] Revise Java's String constructor models

Summary:
Java's String models were broken for

- initializing a String object with a locally defined constant string (which is an `Object*` in SIL).
- initializing a String object with a `char`/`byte` array

This diff fixes them and also adds models for  `new String ()`.

Reviewed By: skcho

Differential Revision: D19662180

fbshipit-source-id: 23968d0aa

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -1089,10 +1089,14 @@ module JavaString = struct
     ArrObjCommon.constructor_from_char_ptr model_env tgt_deref ~fn src mem
 
 
-  (* https://docs.oracle.com/javase/7/docs/api/java/lang/String.html#String(byte[]) *)
-  let constructor tgt_exp src =
-    let exec model_env ~ret:_ mem =
-      constructor_from_char_ptr model_env (Sem.eval_locs tgt_exp mem) src mem
+  (* https://docs.oracle.com/javase/7/docs/api/java/lang/String.html#String(char[]) *)
+  (* same for byte[]*)
+  let constructor_from_array tgt_exp arr_exp =
+    let exec {integer_type_widths} ~ret:_ mem =
+      let tgt_locs = Sem.eval_locs tgt_exp mem in
+      let deref_of_tgt = PowLoc.append_field tgt_locs ~fn in
+      let src_arr_locs = Dom.Val.get_all_locs (Sem.eval_arr integer_type_widths arr_exp mem) in
+      Dom.Mem.update_mem deref_of_tgt (Dom.Mem.find_set src_arr_locs mem) mem
     in
     {exec; check= no_check}
 
@@ -1128,13 +1132,20 @@ module JavaString = struct
 
 
   (* https://docs.oracle.com/javase/7/docs/api/java/lang/String.html#String(java.lang.String) *)
-  let copy_constructor vec_exp src_exp =
+  let copy_constructor tgt_exp src_exp =
     let exec ({integer_type_widths} as model_env) ~ret:_ mem =
-      let vec_locs = Sem.eval integer_type_widths vec_exp mem |> Dom.Val.get_all_locs in
-      let deref_of_vec = PowLoc.append_field vec_locs ~fn in
-      ArrObjCommon.copy_constructor model_env deref_of_vec ~fn src_exp mem
+      let tgt_deref = Sem.eval integer_type_widths tgt_exp mem |> Dom.Val.get_all_locs in
+      let elem_locs = PowLoc.append_field tgt_deref ~fn in
+      match src_exp with
+      | Exp.Const (Const.Cstr s) ->
+          BoUtils.Exec.decl_string model_env ~do_alloc:true elem_locs s mem
+      | _ ->
+          ArrObjCommon.copy_constructor model_env elem_locs ~fn src_exp mem
     in
     {exec; check= no_check}
+
+
+  let empty_constructor tgt_exp = copy_constructor tgt_exp (Exp.Const (Const.Cstr ""))
 end
 
 module Preconditions = struct
@@ -1206,7 +1217,9 @@ module Call = struct
     let std_array0 = mk_std_array () in
     let std_array1 = mk_std_array () in
     let std_array2 = mk_std_array () in
-    let char_ptr = Typ.mk (Typ.Tptr (Typ.mk (Typ.Tint Typ.IChar), Pk_pointer)) in
+    let char_typ = Typ.mk (Typ.Tint Typ.IChar) in
+    let char_ptr = Typ.mk (Typ.Tptr (char_typ, Pk_pointer)) in
+    let char_array = Typ.mk (Typ.Tptr (Typ.mk_array char_typ, Pk_pointer)) in
     make_dispatcher
       [ -"__exit" <>--> bottom
       ; -"CFArrayCreate" <>$ any_arg $+ capt_exp $+ capt_exp $+...$--> CFArray.create_array
@@ -1255,11 +1268,12 @@ module Call = struct
       ; +PatternMatch.implements_lang "String"
         &:: "charAt" <>$ capt_exp $+ capt_exp $--> JavaString.charAt
       ; +PatternMatch.implements_lang "String"
-        &:: "<init>" <>$ capt_exp
-        $+ capt_exp_of_typ (+PatternMatch.implements_lang "String")
-        $--> JavaString.copy_constructor
+        &:: "<init>" <>$ capt_exp $+ capt_exp_of_prim_typ char_array
+        $--> JavaString.constructor_from_array
+      ; +PatternMatch.implements_lang "String"
+        &:: "<init>" <>$ capt_exp $+ capt_exp $--> JavaString.copy_constructor
       ; +PatternMatch.implements_lang "String"
-        &:: "<init>" <>$ capt_exp $+ capt_exp $--> JavaString.constructor
+        &:: "<init>" <>$ capt_exp $--> JavaString.empty_constructor
       ; +PatternMatch.implements_lang "String"
         &:: "concat" <>$ capt_exp $+ capt_exp $+...$--> JavaString.concat
       ; +PatternMatch.implements_lang "String"

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

@@ -49,4 +49,30 @@ class StringTest {
     String s = new String("hello");
     split_linear(s);
   }
+
+  void byte_array_constructor_linear(byte[] data) {
+    String s = new String(data);
+    for (int i = 0; i < s.length(); i++) {}
+  }
+
+  void call_string_constant() {
+    byte[] data = new byte[10];
+    byte_array_constructor_linear(data);
+  }
+
+  void string_constructor_constant() {
+    String s = "abcd";
+    String str = new String(s);
+    for (int i = 0; i < str.length(); i++) {}
+  }
+
+  void string_constructor_linear(String s) {
+    String str = new String(s);
+    for (int i = 0; i < str.length(); i++) {}
+  }
+
+  void call_string_constructor_constant() {
+    String s = new String();
+    string_constructor_linear(s);
+  }
 }

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

@@ -196,12 +196,14 @@ codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.Mat
 codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.max2_symbolic(int,int):void, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 9 ⋅ (max(x, y)), O((max(x, y))), degree = 1,{max(x, y)},Loop at line 20]
 codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.max_symbolic(int[]):void, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ arr.length + 4 ⋅ (arr.length + 1), O(arr.length), degree = 1,{arr.length + 1},Loop at line 16,{arr.length},Loop at line 16]
 codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.checkNotNull_linear(java.util.ArrayList,java.lang.Object):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 11 + 8 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 37,{list.length},Loop at line 37]
+codetoanalyze/java/performance/StringTest.java, StringTest.byte_array_constructor_linear(byte[]):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ data.length + 3 ⋅ (data.length + 1), O(data.length), degree = 1,{data.length + 1},Loop at line 55,{data.length},Loop at line 55]
 codetoanalyze/java/performance/StringTest.java, StringTest.index_substring_linear():java.lang.String, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 9 + this.mId.length, O(this.mId.length), degree = 1,{this.mId.length},call to int StringTest.indexof_linear(String),Modeled call to String.indexOf]
 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 ⋅ (-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/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]