[cost][inferbo] Add models for indexOf

Reviewed By: skcho

Differential Revision: D16089480

fbshipit-source-id: 1065a1830

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -357,6 +357,20 @@ let inferbo_set_size src_exp size_exp =
 
 let model_by_value value id mem = Dom.Mem.add_stack (Loc.of_id id) value mem
 
+(** Given a string of length n, return itv [-1, n_u-1]. *)
+let range_itv_mone exp mem =
+  eval_string_len exp mem |> BufferOverrunDomain.Val.get_itv |> Itv.set_lb_zero |> Itv.decr
+
+
+let indexOf exp =
+  let exec _ ~ret:(ret_id, _) mem =
+    (* if not found, indexOf returns -1. *)
+    let v = range_itv_mone exp mem |> Dom.Val.of_itv in
+    model_by_value v ret_id mem
+  in
+  {exec; check= no_check}
+
+
 let cast exp =
   let exec {integer_type_widths} ~ret:(ret_id, _) mem =
     let itv = Sem.eval integer_type_widths exp mem in
@@ -877,6 +891,7 @@ module Call = struct
       ; -"strcat" <>$ capt_exp $+ capt_exp $+...$--> strcat
       ; +PatternMatch.implements_lang "String"
         &:: "concat" <>$ capt_exp $+ capt_exp $+...$--> strcat
+      ; +PatternMatch.implements_lang "String" &:: "indexOf" <>$ capt_exp $+ any_arg $--> indexOf
       ; -"strcpy" <>$ capt_exp $+ capt_exp $+...$--> strcpy
       ; -"strncpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> strncpy
       ; -"snprintf" <>--> snprintf

infer/src/checkers/costModels.ml

@@ -50,6 +50,19 @@ let modeled ~of_function {pname; location} ~ret:(_, ret_typ) _ : BasicCost.t =
   of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function location
 
 
+(** 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
+  Option.value_map from ~default:itv ~f:(fun (start_exp, integer_type_widths) ->
+      let start_itv =
+        BufferOverrunSemantics.eval integer_type_widths start_exp mem
+        |> BufferOverrunDomain.Val.get_itv
+      in
+      Itv.minus itv start_itv )
+  |> Itv.set_lb_zero
+
+
 module BoundsOf (Container : S) = struct
   let of_length exp {location} ~ret:_ mem ~of_function ~degree_kind =
     let itv = Container.length exp mem |> BufferOverrunDomain.Val.get_itv in
@@ -66,7 +79,7 @@ module BoundsOf (Container : S) = struct
     BasicCost.mult n log_n
 end
 
-module String = struct
+module JavaString = struct
   let substring_aux ~begin_idx ~end_v {integer_type_widths; location} inferbo_mem =
     let begin_v = BufferOverrunSemantics.eval integer_type_widths begin_idx inferbo_mem in
     let itv =
@@ -85,6 +98,36 @@ module String = struct
     substring_aux ~begin_idx
       ~end_v:(BufferOverrunSemantics.eval integer_type_widths end_idx inferbo_mem)
       model_env inferbo_mem
+
+
+  (** 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
+    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
+    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 itv =
+      BufferOverrunModels.eval_string_len exp inferbo_mem |> BufferOverrunDomain.Val.get_itv
+    in
+    let index_itv =
+      BufferOverrunModels.eval_string_len index_exp inferbo_mem |> BufferOverrunDomain.Val.get_itv
+    in
+    let n =
+      of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.indexOf" location
+    in
+    let m =
+      of_itv ~itv:index_itv ~degree_kind:Polynomials.DegreeKind.Linear
+        ~of_function:"String.indexOf" location
+    in
+    BasicCost.mult n m
 end
 
 module BoundsOfCollection = BoundsOf (Collection)
@@ -93,6 +136,7 @@ module BoundsOfArray = BoundsOf (Array)
 module Call = struct
   let dispatch : (Tenv.t, model) ProcnameDispatcher.Call.dispatcher =
     let open ProcnameDispatcher.Call in
+    let int_typ = Typ.mk (Typ.Tint Typ.IInt) in
     make_dispatcher
       [ +PatternMatch.implements_collections
         &:: "sort" $ capt_exp
@@ -131,11 +175,20 @@ module Call = struct
         &:: "shuffle" <>$ capt_exp
         $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.shuffle"
       ; +PatternMatch.implements_lang "String"
-        &:: "substring" <>$ capt_exp $+ capt_exp $--> String.substring
+        &:: "substring" <>$ capt_exp $+ capt_exp $--> JavaString.substring
+      ; +PatternMatch.implements_lang "String"
+        &:: "indexOf" <>$ capt_exp
+        $+ capt_exp_of_typ (+PatternMatch.implements_lang "String")
+        $--> JavaString.indexOf_str
+      ; +PatternMatch.implements_lang "String"
+        &:: "indexOf" <>$ capt_exp $+ any_arg_of_prim_typ int_typ $+ capt_exp
+        $--> JavaString.indexOf_char_starting_from
+      ; +PatternMatch.implements_lang "String"
+        &:: "indexOf" <>$ capt_exp $+ any_arg_of_prim_typ int_typ $--> JavaString.indexOf_char
       ; +PatternMatch.implements_lang "String"
         &:: "substring"
         $ any_arg_of_typ (+PatternMatch.implements_lang "String")
-        $+ capt_exp $+ capt_exp $--> String.substring_no_end
+        $+ capt_exp $+ capt_exp $--> JavaString.substring_no_end
       ; +PatternMatch.implements_inject "Provider"
         &:: "get"
         <>--> modeled ~of_function:"Provider.get" ]

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

@@ -0,0 +1,32 @@
+/*
+ * 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 {
+
+  String mId;
+
+  int indexof_linear(String m) {
+    return m.indexOf('_');
+  }
+
+  int indexof_from_linear(String m, int j) {
+    return m.indexOf('_', j);
+  }
+
+  int indexof_quadratic(String m, String n) {
+    return m.indexOf(n);
+  }
+
+  int indexof_constant(String n) {
+    String m = "hi";
+    return m.indexOf('i');
+  }
+
+  public String index_substring_linear() {
+    int index = indexof_linear(mId);
+    return mId.substring(0, index);
+  }
+}

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

@@ -156,6 +156,10 @@ codetoanalyze/java/performance/MapTest.java, MapTest.entrySet_linear(java.util.M
 codetoanalyze/java/performance/MapTest.java, MapTest.keySet_linear(java.util.Map):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 8 ⋅ (map.length - 1) + 3 ⋅ map.length, degree = 1,{map.length},Loop at line 13,{map.length - 1},Loop at line 13]
 codetoanalyze/java/performance/MapTest.java, MapTest.putAll_linear(java.util.Map):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 13 + 8 ⋅ (map.length - 1) + 3 ⋅ map.length, degree = 1,{map.length},Loop at line 28,{map.length - 1},Loop at line 28]
 codetoanalyze/java/performance/MapTest.java, MapTest.values_linear(java.util.Map):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 13 + 8 ⋅ map.length + 3 ⋅ (map.length + 1), degree = 1,{map.length + 1},Loop at line 22,{map.length},Loop at line 22]
+codetoanalyze/java/performance/StringTest.java, StringTest.index_substring_linear():java.lang.String, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 9 + 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, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + (-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, 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, degree = 2,{n.length},Modeled call to String.indexOf,{m.length},Modeled call to String.indexOf]
 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, degree = 0]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.vanilla_switch(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]