[cost] Revise substring's cost model

Summary:
Prevent returning a negative cost bound when calling `substring(begin_index, end_index)` when either is possible
- `begin_index < 0`
- `begin_index > end_index`

Instead, return unit cost since such cases either throw `IndexOutOfBoundsException ` at runtime or correspond to having two symbolic bounds that cannot be semantically compared.

Reviewed By: dulmarod

Differential Revision: D19619410

fbshipit-source-id: cf5e8cb7b

infer/src/cost/costModels.ml

@@ -52,20 +52,28 @@ module JavaString = struct
     let begin_itv = BufferOverrunDomain.Val.get_itv begin_v in
     let end_itv = BufferOverrunDomain.Val.get_itv end_v in
     let itv =
-      if Boolean.is_true (Itv.le_sem begin_itv end_itv) then Itv.minus end_itv begin_itv
+      if
-      else end_itv
+        Boolean.is_true (Itv.le_sem Itv.zero begin_itv)
+        && Boolean.is_true (Itv.le_sem begin_itv end_itv)
+      then Itv.minus end_itv begin_itv
+      else
+        (* in practice, either we have two symbolic bounds that are semantically
+           incomparable at this point or there is an out of bounds exception. In
+           both cases, we don't want to give negative cost so we
+           behave as if there is no model and give unit cost. *)
+        Itv.of_int 1
     in
     CostUtils.of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.substring"
       location
 
 
-  let substring exp begin_idx model_env ~ret:_ inferbo_mem =
+  let substring_no_end exp begin_idx model_env ~ret:_ inferbo_mem =
     substring_aux ~begin_idx
       ~end_v:(BufferOverrunModels.JavaString.get_length model_env exp inferbo_mem)
       model_env inferbo_mem
 
 
-  let substring_no_end begin_idx end_idx ({integer_type_widths} as model_env) ~ret:_ inferbo_mem =
+  let substring begin_idx end_idx ({integer_type_widths} as model_env) ~ret:_ inferbo_mem =
     substring_aux ~begin_idx
       ~end_v:(BufferOverrunSemantics.eval integer_type_widths end_idx inferbo_mem)
       model_env inferbo_mem
@@ -163,7 +171,7 @@ module Call = struct
           &:: "shuffle" <>$ capt_exp
           $+...$--> BoundsOfCollection.linear_length ~of_function:"Collections.shuffle"
         ; +PatternMatch.implements_lang "String"
-          &:: "substring" <>$ capt_exp $+ capt_exp $--> JavaString.substring
+          &:: "substring" <>$ capt_exp $+ capt_exp $--> JavaString.substring_no_end
         ; +PatternMatch.implements_lang "String"
           &:: "indexOf" <>$ capt_exp
           $+ capt_exp_of_typ (+PatternMatch.implements_lang "String")
@@ -176,7 +184,7 @@ module Call = struct
         ; +PatternMatch.implements_lang "String"
           &:: "substring"
           $ any_arg_of_typ (+PatternMatch.implements_lang "String")
-          $+ capt_exp $+ capt_exp $--> JavaString.substring_no_end
+          $+ capt_exp $+ capt_exp $--> JavaString.substring
         ; +PatternMatch.implements_inject "Provider"
           &:: "get"
           <>--> modeled ~of_function:"Provider.get"

infer/tests/codetoanalyze/java/hoistingExpensive/HoistModeled.java

@@ -42,14 +42,16 @@ class HoistModeled {
     }
   }
 
-  void linear_substring_hoist(String s, ArrayList<Integer> list, Integer el) {
+  void linear_substring_hoist_FN(String s, ArrayList<Integer> list, Integer el) {
     String sub;
     int length = s.length();
     for (int i = 0; i < 10; i++) {
-      sub = s.substring(2, length - 1);
+      sub =
+          s.substring(
+              2, length - 1); // can't determine statically that 2 <= length-1. So we give unit cost
     }
     for (int i = 0; i < 10; i++) {
-      sub = s.substring(1);
+      sub = s.substring(1); // ditto
     }
   }
 
@@ -66,4 +68,13 @@ class HoistModeled {
       call_expensive_hoist("ez", list, el);
     }
   }
+
+  void constant_substring_dont_hoist(String s, int x) {
+    String sub;
+    int length = s.length();
+    int y = -1;
+    for (int i = 0; i < 10; i++) {
+      sub = s.substring(x, y);
+    }
+  }
 }

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

@@ -11,17 +11,19 @@ codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symboli
 codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_iterator_hoist(int,java.util.ArrayList):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistExpensive.symbolic_expensive_iterator_hoist(int,ArrayList)]
 codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_iterator_hoist(int,java.util.ArrayList):void, 1, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistExpensive.cheap_iterator_dont_hoist(ArrayList) at line 49 is loop-invariant,with estimated cost 7 + 14 ⋅ list.length + 3 ⋅ (list.length + 1), degree = 1,{list.length + 1},call to void HoistExpensive.cheap_iterator_dont_hoist(ArrayList),Loop at line 41,{list.length},call to void HoistExpensive.cheap_iterator_dont_hoist(ArrayList),Loop at line 41]
 codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.call_expensive_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.call_expensive_hoist(String,ArrayList,Integer)]
-codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.call_expensive_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 1, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistModeled.expensive_get_hoist(int) at line 58 is loop-invariant,with estimated cost 85 + 10 ⋅ Provider.get().modeled.ub, degree = 1,{Provider.get().modeled.ub},call to void HoistModeled.expensive_get_hoist(int),Modeled call to Provider.get]
+codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.call_expensive_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 1, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistModeled.expensive_get_hoist(int) at line 60 is loop-invariant,with estimated cost 85 + 10 ⋅ Provider.get().modeled.ub, degree = 1,{Provider.get().modeled.ub},call to void HoistModeled.expensive_get_hoist(int),Modeled call to Provider.get]
 codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_contains_dont_hoist(java.lang.Integer):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.constant_contains_dont_hoist(Integer)]
 codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_contains_dont_hoist(java.lang.Integer):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to boolean ArrayList.contains(Object) at line 34 is loop-invariant]
 codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_substring_dont_hoist(java.lang.String):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.constant_substring_dont_hoist(String)]
 codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_substring_dont_hoist(java.lang.String):void, 1, INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 41 is loop-invariant]
+codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_substring_dont_hoist(java.lang.String,int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.constant_substring_dont_hoist(String,int)]
+codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.constant_substring_dont_hoist(java.lang.String,int):void, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 77 is loop-invariant]
 codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_hoist(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.expensive_get_hoist(int)]
 codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_hoist(int):void, 1, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to Object Provider.get() at line 16 is loop-invariant,with estimated cost Provider.get().modeled.ub, degree = 1,{Provider.get().modeled.ub},Modeled call to Provider.get]
 codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_hoist_hoist_me(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.expensive_get_hoist_hoist_me(String,ArrayList,Integer)]
-codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_hoist_hoist_me(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistModeled.call_expensive_hoist(String,ArrayList,Integer) at line 66 is loop-invariant,with estimated cost 904 + 100 ⋅ Provider.get().modeled.ub, degree = 1,{Provider.get().modeled.ub},call to void HoistModeled.call_expensive_hoist(String,ArrayList,Integer),call to void HoistModeled.expensive_get_hoist(int),Modeled call to Provider.get]
+codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.expensive_get_hoist_hoist_me(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistModeled.call_expensive_hoist(String,ArrayList,Integer) at line 68 is loop-invariant,with estimated cost 904 + 100 ⋅ Provider.get().modeled.ub, degree = 1,{Provider.get().modeled.ub},call to void HoistModeled.call_expensive_hoist(String,ArrayList,Integer),call to void HoistModeled.expensive_get_hoist(int),Modeled call to Provider.get]
 codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_contains_hoist(java.util.ArrayList,java.lang.Integer):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.linear_contains_hoist(ArrayList,Integer)]
 codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_contains_hoist(java.util.ArrayList,java.lang.Integer):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to boolean ArrayList.contains(Object) at line 23 is loop-invariant,with estimated cost list.length, degree = 1,{list.length},Modeled call to List.contains]
-codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.linear_substring_hoist(String,ArrayList,Integer)]
+codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist_FN(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void HoistModeled.linear_substring_hoist_FN(String,ArrayList,Integer)]
-codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 2, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 49 is loop-invariant,with estimated cost (s.length - 1), degree = 1,{s.length - 1},Modeled call to String.substring]
+codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist_FN(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 50 is loop-invariant]
-codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 5, EXPENSIVE_LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int) at line 52 is loop-invariant,with estimated cost s.length, degree = 1,{s.length},Modeled call to String.substring]
+codetoanalyze/java/hoistingExpensive/HoistModeled.java, HoistModeled.linear_substring_hoist_FN(java.lang.String,java.util.ArrayList,java.lang.Integer):void, 7, INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int) at line 54 is loop-invariant]