[inferbo] Add Java String constructor models

Summary: This diff adds models of Java String. In order to keep the precision of cost checker, I fixed cost models for String in this diff too.

Reviewed By: ngorogiannis

Differential Revision: D17203309

fbshipit-source-id: 8cc2814fc

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -201,6 +201,23 @@ module TransferFunctions = struct
     | Load {id; e= exp; typ} ->
         let represents_multiple_values = is_array_access_exp exp in
         BoUtils.Exec.load_locs ~represents_multiple_values id typ (Sem.eval_locs exp mem) mem
+    | Store {e1= tgt_exp; e2= Const (Const.Cstr _) as src; loc= location}
+      when Language.curr_language_is Java ->
+        let pname = Summary.get_proc_name summary in
+        let node_hash = CFG.Node.hash node in
+        let model_env =
+          BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths
+        in
+        let tgt_locs = Sem.eval_locs tgt_exp mem in
+        let tgt_deref =
+          let allocsite =
+            Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None
+              ~represents_multiple_values:false
+          in
+          PowLoc.singleton (Loc.of_allocsite allocsite)
+        in
+        Dom.Mem.update_mem tgt_locs (Dom.Val.of_pow_loc ~traces:Dom.TraceSet.bottom tgt_deref) mem
+        |> Models.JavaString.constructor_from_char_ptr model_env tgt_deref src
     | Store {e1= exp1; e2= Const (Const.Cstr s); loc= location} ->
         let locs = Sem.eval_locs exp1 mem in
         let model_env =

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -564,6 +564,40 @@ module ArrObjCommon = struct
     let arr_locs = deref_of model_env exp ~fn mem in
     let mem = Dom.Mem.add_stack (Loc.of_id id) (eval_array_locs_length arr_locs mem) mem in
     load_size_alias id arr_locs mem
+
+
+  let at arr_exp ~fn index_exp =
+    let exec ({pname; location} as model_env) ~ret:(id, _) mem =
+      let array_v =
+        let locs = deref_of model_env arr_exp ~fn mem in
+        if PowLoc.is_bot locs then Dom.Val.unknown_from ~callee_pname:(Some pname) ~location
+        else Dom.Mem.find_set locs mem
+      in
+      Dom.Mem.add_stack (Loc.of_id id) array_v mem
+    and check ({location; integer_type_widths} as model_env) mem cond_set =
+      let idx = Sem.eval integer_type_widths index_exp mem in
+      let arr = Dom.Mem.find_set (deref_of model_env arr_exp ~fn mem) mem in
+      let relation = Dom.Mem.get_relation mem in
+      let latest_prune = Dom.Mem.get_latest_prune mem in
+      BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp:None ~relation ~is_plus:true
+        ~last_included:false ~latest_prune location cond_set
+    in
+    {exec; check}
+
+
+  let copy_constructor model_env deref_of_tgt ~fn src_exp mem =
+    let deref_of_src = deref_of model_env src_exp ~fn mem in
+    Dom.Mem.update_mem deref_of_tgt (Dom.Mem.find_set deref_of_src mem) mem
+
+
+  let constructor_from_char_ptr ({integer_type_widths} as model_env) tgt_deref ~fn src mem =
+    let elem_locs = PowLoc.append_field tgt_deref ~fn in
+    match src with
+    | Exp.Const (Const.Cstr s) ->
+        BoUtils.Exec.decl_string model_env ~do_alloc:true elem_locs s mem
+    | _ ->
+        let v = Sem.eval integer_type_widths src mem in
+        Dom.Mem.update_mem elem_locs v mem
 end
 
 module StdVector = struct
@@ -614,31 +648,16 @@ module StdVector = struct
         (Dom.Val.get_all_locs v, Dom.Val.get_traces v)
       in
       let deref_of_vec = append_fields vec_locs ~vec_typ ~elt_typ in
-      let deref_of_src = deref_of model_env elt_typ (src_exp, vec_typ) mem in
+      let fn = BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ in
       mem
       |> Dom.Mem.update_mem vec_locs (Dom.Val.of_pow_loc ~traces deref_of_vec)
-      |> Dom.Mem.update_mem deref_of_vec (Dom.Mem.find_set deref_of_src mem)
+      |> ArrObjCommon.copy_constructor model_env deref_of_vec ~fn src_exp
     in
     {exec; check= no_check}
 
 
-  let at elt_typ vec_arg index_exp =
-    let exec ({pname; location} as model_env) ~ret:(id, _) mem =
-      let array_v =
-        let locs = deref_of model_env elt_typ vec_arg mem in
-        if PowLoc.is_bot locs then Dom.Val.unknown_from ~callee_pname:(Some pname) ~location
-        else Dom.Mem.find_set locs mem
-      in
-      Dom.Mem.add_stack (Loc.of_id id) array_v mem
-    and check ({location; integer_type_widths} as model_env) mem cond_set =
-      let idx = Sem.eval integer_type_widths index_exp mem in
-      let arr = Dom.Mem.find_set (deref_of model_env elt_typ vec_arg mem) mem in
-      let relation = Dom.Mem.get_relation mem in
-      let latest_prune = Dom.Mem.get_latest_prune mem in
-      BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp:None ~relation ~is_plus:true
-        ~last_included:false ~latest_prune location cond_set
-    in
-    {exec; check}
+  let at elt_typ (vec_exp, vec_typ) index_exp =
+    ArrObjCommon.at vec_exp ~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ) index_exp
 
 
   let set_size {location} locs new_size mem =
@@ -693,8 +712,8 @@ module StdVector = struct
 end
 
 module StdBasicString = struct
-  let constructor_from_char_ptr_common char_typ (tgt_exp, tgt_typ) src ~len_opt =
-    let exec ({pname; node_hash; integer_type_widths} as model_env) ~ret mem =
+  let constructor_from_char_ptr char_typ (tgt_exp, tgt_typ) src ~len_opt =
+    let exec ({pname; node_hash} as model_env) ~ret mem =
       let mem =
         Option.value_map len_opt ~default:mem ~f:(fun len ->
             let {exec= malloc_exec} = malloc ~can_be_zero:true len in
@@ -711,13 +730,8 @@ module StdBasicString = struct
       let mem =
         Dom.Mem.update_mem tgt_locs (Dom.Val.of_pow_loc ~traces:Trace.Set.bottom tgt_deref) mem
       in
-      let elem_locs = StdVector.append_fields ~vec_typ:tgt_typ ~elt_typ:char_typ tgt_deref in
-      match src with
-      | Exp.Const (Const.Cstr s) ->
-          BoUtils.Exec.decl_string model_env ~do_alloc:true elem_locs s mem
-      | _ ->
-          let v = Sem.eval integer_type_widths src mem in
-          Dom.Mem.update_mem elem_locs v mem
+      let fn = BufferOverrunField.cpp_vector_elem ~vec_typ:tgt_typ ~elt_typ:char_typ in
+      ArrObjCommon.constructor_from_char_ptr model_env tgt_deref src ~fn mem
     in
     let check ({location; integer_type_widths} as model_env) mem cond_set =
       Option.value_map len_opt ~default:cond_set ~f:(fun len ->
@@ -730,13 +744,13 @@ module StdBasicString = struct
 
 
   (* The (4) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
-  let constructor_from_char_ptr char_typ (tgt_exp, tgt_typ) src len =
-    constructor_from_char_ptr_common char_typ (tgt_exp, tgt_typ) src ~len_opt:(Some len)
+  let constructor_from_char_ptr_with_len char_typ (tgt_exp, tgt_typ) src len =
+    constructor_from_char_ptr char_typ (tgt_exp, tgt_typ) src ~len_opt:(Some len)
 
 
   (* The (5) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
   let constructor_from_char_ptr_without_len char_typ (tgt_exp, tgt_typ) src =
-    constructor_from_char_ptr_common char_typ (tgt_exp, tgt_typ) src ~len_opt:None
+    constructor_from_char_ptr char_typ (tgt_exp, tgt_typ) src ~len_opt:None
 
 
   (* The (7) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
@@ -1007,6 +1021,8 @@ module JavaString = struct
         (length, elem)
 
 
+  let get_length model_env exp mem = get_length_and_elem model_env exp mem |> fst
+
   let concat exp1 exp2 =
     let exec ({pname; node_hash} as model_env) ~ret:(id, _) mem =
       let length_v, elem =
@@ -1047,6 +1063,30 @@ module JavaString = struct
       model_by_value v ret_id mem
     in
     {exec; check= no_check}
+
+
+  let charAt string_exp idx = ArrObjCommon.at ~fn string_exp idx
+
+  let constructor_from_char_ptr model_env tgt_deref src mem =
+    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
+    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 =
+      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
+    in
+    {exec; check= no_check}
 end
 
 module Preconditions = struct
@@ -1112,6 +1152,14 @@ module Call = struct
       ; -"memmove" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy
       ; -"memset" <>$ capt_exp $+ any_arg $+ capt_exp $!--> memset
       ; -"strcat" <>$ capt_exp $+ capt_exp $+...$--> strcat
+      ; +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
+      ; +PatternMatch.implements_lang "String"
+        &:: "<init>" <>$ capt_exp $+ capt_exp $--> JavaString.constructor
       ; +PatternMatch.implements_lang "String"
         &:: "concat" <>$ capt_exp $+ capt_exp $+...$--> JavaString.concat
       ; +PatternMatch.implements_lang "String"
@@ -1150,7 +1198,7 @@ module Call = struct
         < capt_typ `T
         &+...>:: "basic_string" $ capt_arg $+ capt_exp_of_prim_typ char_ptr
         $+ capt_exp_of_prim_typ (Typ.mk (Typ.Tint Typ.size_t))
-        $--> StdBasicString.constructor_from_char_ptr
+        $--> StdBasicString.constructor_from_char_ptr_with_len
       ; -"std" &:: "basic_string"
         < capt_typ `T
         &+...>:: "empty" $ capt_arg $--> StdBasicString.empty

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -168,14 +168,32 @@ module Exec = struct
         mem
 
 
-  let get_max_char s = String.fold s ~init:0 ~f:(fun acc c -> max acc (Char.to_int c))
+  let get_min_max_char s ~init_char =
+    let init_i = Char.to_int init_char in
+    String.fold s ~init:(init_i, init_i) ~f:(fun (min_acc, max_acc) c ->
+        let i = Char.to_int c in
+        (min min_acc i, max max_acc i) )
+
 
   let decl_string {pname; node_hash; location; integer_type_widths} ~do_alloc locs s mem =
     let stride = Some (Typ.width_of_ikind integer_type_widths IChar / 8) in
     let offset = Itv.zero in
-    let size = Itv.of_int (String.length s + 1) in
+    let size =
+      let s_length =
+        if Language.curr_language_is Java then String.length s else String.length s + 1
+      in
+      Itv.of_int s_length
+    in
     let traces = Trace.Set.singleton location Trace.ArrayDeclaration in
-    let char_itv = Itv.join Itv.zero (Itv.of_int (get_max_char s)) in
+    let char_itv =
+      let itv =
+        if Int.equal (String.length s) 0 then Itv.bot
+        else
+          let min, max = get_min_max_char s ~init_char:s.[0] in
+          Itv.join (Itv.of_int min) (Itv.of_int max)
+      in
+      if Language.curr_language_is Java then itv else Itv.join Itv.zero itv
+    in
     let decl loc mem =
       (* It doesn't allocate if the character pointer is in stack, because they are already
          allocated at the entry of the function. *)

infer/src/checkers/costModels.ml

@@ -52,8 +52,10 @@ let modeled ~of_function {pname; location} ~ret:(_, ret_typ) _ : BasicCost.t =
 
 (** Given a string of length n and an optional starting index i (0 by
    default), return itv [0, n_u-i_l] *)
-let string_len_range_itv exp ~from mem =
-  let itv = BufferOverrunModels.eval_string_len exp mem |> BufferOverrunDomain.Val.get_itv in
+let string_len_range_itv model_env exp ~from mem =
+  let itv =
+    BufferOverrunModels.JavaString.get_length model_env exp mem |> BufferOverrunDomain.Val.get_itv
+  in
   Option.value_map from ~default:itv ~f:(fun (start_exp, integer_type_widths) ->
       let start_itv =
         BufferOverrunSemantics.eval integer_type_widths start_exp mem
@@ -90,7 +92,7 @@ module JavaString = struct
 
   let substring exp begin_idx model_env ~ret:_ inferbo_mem =
     substring_aux ~begin_idx
-      ~end_v:(BufferOverrunModels.eval_string_len exp inferbo_mem)
+      ~end_v:(BufferOverrunModels.JavaString.get_length model_env exp inferbo_mem)
       model_env inferbo_mem
 
 
@@ -101,24 +103,29 @@ module JavaString = struct
 
 
   (** O(|m|) where m is the given string and |.| is the length function *)
-  let indexOf_char exp {location} ~ret:_ inferbo_mem =
-    let itv = string_len_range_itv exp ~from:None inferbo_mem in
+  let indexOf_char exp ({location} as model_env) ~ret:_ inferbo_mem =
+    let itv = string_len_range_itv model_env exp ~from:None inferbo_mem in
     of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.indexOf" location
 
 
   (** O(|m|-|n|) where m is the given string and n is the index to start searching from *)
-  let indexOf_char_starting_from exp start_exp {integer_type_widths; location} ~ret:_ inferbo_mem =
-    let itv = string_len_range_itv exp ~from:(Some (start_exp, integer_type_widths)) inferbo_mem in
+  let indexOf_char_starting_from exp start_exp ({integer_type_widths; location} as model_env)
+      ~ret:_ inferbo_mem =
+    let itv =
+      string_len_range_itv model_env exp ~from:(Some (start_exp, integer_type_widths)) inferbo_mem
+    in
     of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.indexOf" location
 
 
   (** O(|m|.|n|) where m and n are the given strings *)
-  let indexOf_str exp index_exp {location} ~ret:_ inferbo_mem =
+  let indexOf_str exp index_exp ({location} as model_env) ~ret:_ inferbo_mem =
     let itv =
-      BufferOverrunModels.eval_string_len exp inferbo_mem |> BufferOverrunDomain.Val.get_itv
+      BufferOverrunModels.JavaString.get_length model_env exp inferbo_mem
+      |> BufferOverrunDomain.Val.get_itv
     in
     let index_itv =
-      BufferOverrunModels.eval_string_len index_exp inferbo_mem |> BufferOverrunDomain.Val.get_itv
+      BufferOverrunModels.JavaString.get_length model_env index_exp inferbo_mem
+      |> BufferOverrunDomain.Val.get_itv
     in
     let n =
       of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.indexOf" location

infer/tests/codetoanalyze/java/bufferoverrun/StringTest.java

@@ -0,0 +1,39 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+class StringTest {
+  void constant_Good() {
+    String s = "hello";
+    char c = s.charAt(4);
+  }
+
+  void constant_Bad() {
+    String s = "hello";
+    char c = s.charAt(5);
+  }
+
+  void constant_explicit_constructor_Good() {
+    String s = new String("hello");
+    char c = s.charAt(4);
+  }
+
+  void constant_explicit_constructor_Bad() {
+    String s = new String("hello");
+    char c = s.charAt(5);
+  }
+
+  void copy_constructor_Good() {
+    String s = new String("hello");
+    String t = new String(s);
+    char c = t.charAt(4);
+  }
+
+  void copy_constructor_Bad() {
+    String s = new String("hello");
+    String t = new String(s);
+    char c = t.charAt(5);
+  }
+}

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

@@ -10,3 +10,6 @@ codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alloc_is_nega
 codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `this.buf[*]`,Assignment,<Length trace>,Array declaration,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10]
 codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `this.yy`,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32]
 codetoanalyze/java/bufferoverrun/External.java, External.external_function_Bad(external.library.SomeExternalClass):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
+codetoanalyze/java/bufferoverrun/StringTest.java, StringTest.constant_Bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
+codetoanalyze/java/bufferoverrun/StringTest.java, StringTest.constant_explicit_constructor_Bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
+codetoanalyze/java/bufferoverrun/StringTest.java, StringTest.copy_constructor_Bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]