[inferbo] Add models for Math.min and Math.max

Reviewed By: skcho

Differential Revision: D18350518

fbshipit-source-id: 39c6b12f0

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -47,6 +47,16 @@ let at ?(size = Int64.zero) array_exp index_exp =
   {exec; check}
 
 
+let eval_binop ~f e1 e2 =
+  let exec {integer_type_widths} ~ret:(id, _) mem =
+    let i1 = Sem.eval integer_type_widths e1 mem |> Dom.Val.get_itv in
+    let i2 = Sem.eval integer_type_widths e2 mem |> Dom.Val.get_itv in
+    let v = f i1 i2 |> Dom.Val.of_itv in
+    Dom.Mem.add_stack (Loc.of_id id) v mem
+  in
+  {exec; check= no_check}
+
+
 (* It returns a tuple of:
      - type of array element
      - stride of the type
@@ -1405,5 +1415,9 @@ module Call = struct
       ; +PatternMatch.implements_nio "ByteBuffer" &:: "getInt" <>$ capt_exp $--> ByteBuffer.get_int
       ; +PatternMatch.implements_nio "ByteBuffer"
         &:: "getLong" <>$ capt_exp $--> ByteBuffer.get_int
-      ; -"java.lang.Object" &:: "clone" <>$ capt_exp $--> Object.clone ]
+      ; -"java.lang.Object" &:: "clone" <>$ capt_exp $--> Object.clone
+      ; +PatternMatch.implements_lang "Math"
+        &:: "max" <>$ capt_exp $+ capt_exp $--> eval_binop ~f:Itv.max_sem
+      ; +PatternMatch.implements_lang "Math"
+        &:: "min" <>$ capt_exp $+ capt_exp $--> eval_binop ~f:Itv.min_sem ]
 end

infer/src/bufferoverrun/itv.ml

@@ -362,6 +362,10 @@ module ItvPure = struct
    fun (l1, u1) (l2, u2) -> (Bound.underapprox_min l1 l2, Bound.overapprox_min u1 u2)
 
 
+  let max_sem : t -> t -> t =
+   fun (l1, u1) (l2, u2) -> (Bound.underapprox_max l1 l2, Bound.overapprox_max u1 u2)
+
+
   let is_invalid : t -> bool = fun (l, u) -> Bound.is_pinf l || Bound.is_minf u || Bound.lt u l
 
   let normalize : t -> t bottom_lifted = fun x -> if is_invalid x then Bottom else NonBottom x
@@ -670,6 +674,8 @@ let lor_sem : t -> t -> Boolean.t = bind2b ItvPure.lor_sem
 
 let min_sem : t -> t -> t = lift2 ItvPure.min_sem
 
+let max_sem : t -> t -> t = lift2 ItvPure.max_sem
+
 let prune_eq_zero : t -> t = bind1 ItvPure.prune_eq_zero
 
 let prune_ne_zero : t -> t = bind1 ItvPure.prune_ne_zero

infer/src/bufferoverrun/itv.mli

@@ -215,6 +215,8 @@ val lt_sem : t -> t -> Boolean.t
 
 val min_sem : t -> t -> t
 
+val max_sem : t -> t -> t
+
 val mod_sem : t -> t -> t
 
 val ne_sem : t -> t -> Boolean.t

infer/tests/codetoanalyze/java/performance/MathTest.java

@@ -0,0 +1,30 @@
+/*
+ * 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.
+ */
+package codetoanalyze.java.performance;
+
+class MathTest {
+
+  void min_constant(int arr[]) {
+    for (int i = 0; i < Math.min(3, arr.length); i++) {}
+  }
+
+  void max_symbolic(int arr[]) {
+    for (int i = 0; i < Math.max(0, arr.length); i++) {}
+  }
+
+  void linear(int p) {
+    for (int count = 0; count < p; count++) {}
+  }
+
+  void call_with_min_constant() {
+    linear(Math.min(3, 10));
+  }
+
+  void call_with_max_linear(int x) {
+    linear(Math.max(1, x));
+  }
+}

infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java

@@ -34,13 +34,12 @@ class UnknownCallsTest {
     return 0;
   }
 
-  // Expected: linear to maxBytesToRead (= Math.min(...))
+  // Expected: linear
   public int read_max_cost(
       InputStream in, byte[] buffer, int byteOffset, int byteCount, ArrayList<Integer> list)
       throws IOException {
     int maxBytesToRead = Math.min(byteCount, mBytesToRead);
     int bytesRead = in.read(buffer, byteOffset, maxBytesToRead);
-    // after the join, we get maxBytesToRead in [0, +oo]. Hence, the loop gets T
     if (bytesRead > 0) {
       maxBytesToRead = bytesRead + 1;
     }

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

@@ -180,6 +180,9 @@ 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 + 3 ⋅ (map.length + 1), O(map.length), degree = 1,{map.length + 1},Loop at line 13,{map.length},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 + 3 ⋅ (map.length + 1), O(map.length), degree = 1,{map.length + 1},Loop at line 28,{map.length},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 + 1) + 3 ⋅ (map.length + 2), O(map.length), degree = 1,{map.length + 2},Loop at line 22,{map.length + 1},Loop at line 22]
+codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.call_with_max_linear(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 11 + 5 ⋅ (max(1, x)), O(x), degree = 1,{max(1, x)},call to void MathTest.linear(int),Loop at line 20]
+codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.linear(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ p, O(p), degree = 1,{p},Loop at line 20]
+codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.max_symbolic(int[]):void, 1, 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/StringTest.java, StringTest.index_substring_linear():java.lang.String, 1, 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, 1, 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, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + m.length, O(m.length), degree = 1,{m.length},Modeled call to String.indexOf]
@@ -187,16 +190,16 @@ codetoanalyze/java/performance/StringTest.java, StringTest.indexof_quadratic(jav
 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, O(1), degree = 0]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.vanilla_switch(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_concrete_func_linear(UnknownCallsTest$AbstractC):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ UnknownCallsTest$AbstractC.abstract_func().length.ub, O(UnknownCallsTest$AbstractC.abstract_func().length.ub), degree = 1,{UnknownCallsTest$AbstractC.abstract_func().length.ub},Loop at line 95]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_concrete_func_linear(UnknownCallsTest$AbstractC):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ UnknownCallsTest$AbstractC.abstract_func().length.ub, O(UnknownCallsTest$AbstractC.abstract_func().length.ub), degree = 1,{UnknownCallsTest$AbstractC.abstract_func().length.ub},Loop at line 94]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 14 + 12 ⋅ String.toCharArray().length.ub, O(String.toCharArray().length.ub), degree = 1,{String.toCharArray().length.ub},call to void UnknownCallsTest.loop_over_charArray(StringBuilder,String),Loop at line 52]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 14 + 12 ⋅ String.toCharArray().length.ub, O(String.toCharArray().length.ub), degree = 1,{String.toCharArray().length.ub},call to void UnknownCallsTest.loop_over_charArray(StringBuilder,String),Loop at line 51]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_may_throw_exception_constant():void, 1, EXPENSIVE_ALLOCATION, no_bucket, ERROR, [with estimated cost 11, O(1), degree = 0]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_may_throw_exception_constant():void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 217, O(1), degree = 0]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_throw_exception_linear():void, 1, EXPENSIVE_ALLOCATION, no_bucket, ERROR, [with estimated cost (1+max(0, UnknownCallsTest.throw_exception().ub)), O(UnknownCallsTest.throw_exception().ub), degree = 1,{1+max(0, UnknownCallsTest.throw_exception().ub)},Loop at line 72]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_throw_exception_linear():void, 1, EXPENSIVE_ALLOCATION, no_bucket, ERROR, [with estimated cost (1+max(0, UnknownCallsTest.throw_exception().ub)), O(UnknownCallsTest.throw_exception().ub), degree = 1,{1+max(0, UnknownCallsTest.throw_exception().ub)},Loop at line 71]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_throw_exception_linear():void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ UnknownCallsTest.throw_exception().ub + 8 ⋅ (1+max(0, UnknownCallsTest.throw_exception().ub)), O(UnknownCallsTest.throw_exception().ub), degree = 1,{1+max(0, UnknownCallsTest.throw_exception().ub)},Loop at line 72,{UnknownCallsTest.throw_exception().ub},Loop at line 72]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_throw_exception_linear():void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ UnknownCallsTest.throw_exception().ub + 8 ⋅ (1+max(0, UnknownCallsTest.throw_exception().ub)), O(UnknownCallsTest.throw_exception().ub), degree = 1,{1+max(0, UnknownCallsTest.throw_exception().ub)},Loop at line 71,{UnknownCallsTest.throw_exception().ub},Loop at line 71]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_linear(org.json.JSONArray):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ jsonArray.length, O(jsonArray.length), degree = 1,{jsonArray.length},Loop at line 18]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ String.toCharArray().length.ub, O(String.toCharArray().length.ub), degree = 1,{String.toCharArray().length.ub},Loop at line 52]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ String.toCharArray().length.ub, O(String.toCharArray().length.ub), degree = 1,{String.toCharArray().length.ub},Loop at line 51]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.may_throw_exception():int, 2, UNREACHABLE_CODE, no_bucket, ERROR, [Here]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 9, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 21 + 5 ⋅ (Math.min(...).ub + 1), O(Math.min(...).ub), degree = 1,{Math.min(...).ub + 1},Loop at line 47]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 21 + 5 ⋅ (byteCount + 1), O(byteCount), degree = 1,{byteCount + 1},Loop at line 46]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 15 + 6 ⋅ 2⋅Math.min(...).ub, O(2⋅Math.min(...).ub), degree = 1,{2⋅Math.min(...).ub},Loop at line 33]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 15 + 6 ⋅ 2⋅byteCount, O(2⋅byteCount), degree = 1,{2⋅byteCount},Loop at line 33]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.throw_exception():int, 1, UNREACHABLE_CODE, no_bucket, ERROR, [Here]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 62,{list.length},Loop at line 62]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 61,{list.length},Loop at line 61]