Cost: simplify range of parameters

Reviewed By: ddino

Differential Revision: D8379528

fbshipit-source-id: cf7da17

infer/src/bufferoverrun/itv.ml

@@ -97,6 +97,8 @@ module Symbol = struct
 
   let equal = [%compare.equal : t]
 
+  let paths_equal s1 s2 = phys_equal s1.path s2.path
+
   let make : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> BoundEnd.t -> int -> t =
    fun ~unsigned pname path bound_end id -> {id; pname; unsigned; path; bound_end}
 
@@ -165,6 +167,10 @@ module NonZeroInt : sig
   val plus : t -> t -> t option
 
   val exact_div_exn : t -> t -> t
+
+  val max : t -> t -> t
+
+  val min : t -> t -> t
 end = struct
   type t = int [@@deriving compare]
 
@@ -197,6 +203,11 @@ end = struct
   let exact_div_exn num den =
     if not (is_multiple num den) then raise DivisionNotExact ;
     num / den
+
+
+  let max = Int.max
+
+  let min = Int.min
 end
 
 module Ints : sig
@@ -419,6 +430,28 @@ module SymLinear = struct
   let int_lb x = if is_ge_zero x then Some 0 else None
 
   let int_ub x = if is_le_zero x then Some 0 else None
+
+  (** When two following symbols are from the same path, simplify what would lead to a zero sum. E.g. 2 * x.lb - x.ub = x.lb *)
+  let simplify_bound_ends_from_paths : t -> t =
+   fun x ->
+    let f (prev_opt, to_add) symb coeff =
+      match prev_opt with
+      | Some (prev_coeff, prev_symb)
+        when Symbol.paths_equal prev_symb symb
+             && NonZeroInt.is_positive coeff <> NonZeroInt.is_positive prev_coeff ->
+          let add_coeff =
+            (if NonZeroInt.is_positive coeff then NonZeroInt.max else NonZeroInt.min)
+              prev_coeff (NonZeroInt.( ~- ) coeff)
+          in
+          let to_add =
+            to_add |> M.add symb add_coeff |> M.add prev_symb (NonZeroInt.( ~- ) add_coeff)
+          in
+          (None, to_add)
+      | _ ->
+          (Some (coeff, symb), to_add)
+    in
+    let _, to_add = fold x ~init:(None, zero) ~f in
+    plus x to_add
 end
 
 module Bound = struct
@@ -1030,6 +1063,14 @@ module Bound = struct
   let subst_lb_exn x map = subst_exn ~subst_pos:BoundEnd.LowerBound x map
 
   let subst_ub_exn x map = subst_exn ~subst_pos:BoundEnd.UpperBound x map
+
+  let simplify_bound_ends_from_paths x =
+    match x with
+    | MInf | PInf | MinMax _ ->
+        x
+    | Linear (c, se) ->
+        let se' = SymLinear.simplify_bound_ends_from_paths se in
+        if phys_equal se se' then x else Linear (c, se')
 end
 
 type ('c, 's) valclass = Constant of 'c | Symbolic of 's | ValTop
@@ -1393,7 +1434,8 @@ module ItvRange = struct
 
   let of_bounds : lb:Bound.t -> ub:Bound.t -> t =
    fun ~lb ~ub ->
-    Bound.plus_u ub Bound.one |> Bound.plus_u (Bound.neg lb) |> NonNegativeBound.of_bound
+    Bound.plus_u ub Bound.one |> Bound.plus_u (Bound.neg lb)
+    |> Bound.simplify_bound_ends_from_paths |> NonNegativeBound.of_bound
 
 
   let to_top_lifted_polynomial : t -> NonNegativePolynomial.astate =

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

@@ -42,9 +42,6 @@ codetoanalyze/c/performance/cost_test.c, loop1_bad, 6, EXPENSIVE_EXECUTION_TIME_
 codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 11 * k.ub]
 codetoanalyze/c/performance/cost_test.c, loop2_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 11 * k.ub]
 codetoanalyze/c/performance/cost_test.c, loop2_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 11 * k.ub]
-codetoanalyze/c/performance/cost_test.c, loop3_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 11 * (-k.lb + k.ub + 15)]
-codetoanalyze/c/performance/cost_test.c, loop3_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 11 * (-k.lb + k.ub + 15)]
-codetoanalyze/c/performance/cost_test.c, loop3_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 11 * (-k.lb + k.ub + 15)]
 codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 211]
 codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 5 * (-m.lb + 20)]
 codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 5 * (-m.lb + 20)]

infer/tests/codetoanalyze/java/performance/Cost_test.java

@@ -93,11 +93,10 @@ private static  int FN_loop2(int k) {
     return 0;
   }
 
-// Expected: constant, but the bound is a polynomial since we can't
+  // Expected: constant
-// currently map variables to polynomial symbols
+  private static int loop3(int k) {
-private static  int FN_loop3(int k) {
 
-  for (int i = k; i < k + 15; i++) {
+    for (int i = k; i < k + 18; i++) {
       alias2_OK();
     }
     return 0;
@@ -117,6 +116,4 @@ private static int main_bad() {
     k4 = bar_OK() + foo_OK() + cond_OK(19) * 3;
     return 0;
   }
-
-
 }

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

@@ -20,12 +20,12 @@ codetoanalyze/java/performance/Compound_loop.java, void Compound_loop.while_and_
 codetoanalyze/java/performance/Continue.java, int Continue.continue_outer_loop_FN(), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop2(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 * k.ub]
 codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop2(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 12 * k.ub]
-codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop3(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 12 * (-k.lb + k.ub + 15)]
-codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop3(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 * (-k.lb + k.ub + 15)]
 codetoanalyze/java/performance/Cost_test.java, int Cost_test.loop0_bad(), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1101]
 codetoanalyze/java/performance/Cost_test.java, int Cost_test.loop0_bad(), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1102]
 codetoanalyze/java/performance/Cost_test.java, int Cost_test.loop1_bad(), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1203]
 codetoanalyze/java/performance/Cost_test.java, int Cost_test.loop1_bad(), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1202]
+codetoanalyze/java/performance/Cost_test.java, int Cost_test.loop3(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 219]
+codetoanalyze/java/performance/Cost_test.java, int Cost_test.loop3(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 218]
 codetoanalyze/java/performance/Cost_test.java, int Cost_test.main_bad(), 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 237]
 codetoanalyze/java/performance/Cost_test.java, int Cost_test.main_bad(), 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 205]
 codetoanalyze/java/performance/Cost_test.java, int Cost_test.main_bad(), 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 243]