[inferbo] Exact result for (c1 - max(d, x)) + (c2 + x)

Reviewed By: skcho

Differential Revision: D14185196

fbshipit-source-id: 92d8430a1

infer/src/bufferoverrun/bounds.ml

@@ -158,6 +158,10 @@ module SymLinear = struct
    fun s x -> Option.exists (get_mone_symbol_opt x) ~f:(fun s' -> Symb.Symbol.equal s s')
 
 
+  let is_signed_one_symbol_of : Sign.t -> Symb.Symbol.t -> t -> bool =
+   fun sign s x -> match sign with Plus -> is_one_symbol_of s x | Minus -> is_mone_symbol_of s x
+
+
   let get_symbols : t -> Symb.SymbolSet.t =
    fun x -> M.fold (fun symbol _coeff acc -> Symb.SymbolSet.add symbol acc) x Symb.SymbolSet.empty
 
@@ -729,8 +733,8 @@ module Bound = struct
    fun x -> match x with Linear (c, y) when SymLinear.is_zero y -> Some c | _ -> None
 
 
-  let plus_common : f:(t -> t -> t) -> t -> t -> t =
-   fun ~f x y ->
+  let plus_exact : otherwise:(t -> t -> t) -> t -> t -> t =
+   fun ~otherwise x y ->
     if is_zero x then y
     else if is_zero y then x
     else
@@ -741,12 +745,17 @@ module Bound = struct
       | Linear (c2, x2), MinMax (c1, sign, min_max, d1, x1)
         when SymLinear.is_zero x2 ->
           mk_MinMax (Z.(c1 + c2), sign, min_max, d1, x1)
+      | MinMax (c1, sign, min_max, d, x1), Linear (c2, x2)
+      | Linear (c2, x2), MinMax (c1, sign, min_max, d, x1)
+        when SymLinear.is_signed_one_symbol_of (Sign.neg sign) x1 x2 ->
+          let c = Sign.eval_big_int sign Z.(c1 + c2) d in
+          mk_MinMax (c, Sign.neg sign, MinMax.neg min_max, d, x1)
       | _ ->
-          f x y
+          otherwise x y
 
 
   let plus_l : t -> t -> t =
-    plus_common ~f:(fun x y ->
+    plus_exact ~otherwise:(fun x y ->
         match (x, y) with
         | MinMax (c1, Plus, Max, d1, _), Linear (c2, x2)
         | Linear (c2, x2), MinMax (c1, Plus, Max, d1, _) ->
@@ -759,7 +768,7 @@ module Bound = struct
 
 
   let plus_u : t -> t -> t =
-    plus_common ~f:(fun x y ->
+    plus_exact ~otherwise:(fun x y ->
         match (x, y) with
         | MinMax (c1, Plus, Min, d1, _), Linear (c2, x2)
         | Linear (c2, x2), MinMax (c1, Plus, Min, d1, _) ->

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

@@ -28,7 +28,7 @@ codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_
 codetoanalyze/c/performance/cost_test.c, loop1_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1207, degree = 0]
 codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 10 ⋅ k + 2 ⋅ (1+max(0, k)), degree = 1,{1+max(0, k)},Loop at line 85, column 3,{k},Loop at line 85, column 3]
 codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 214, degree = 0]
-codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ (-m + 20), degree = 1,{-m + 20},Loop at line 117, column 3]
+codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 5 ⋅ (-m + 20) + (21-min(20, m)), degree = 1,{21-min(20, m)},Loop at line 117, column 3,{-m + 20},Loop at line 117, column 3]
 codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 235, degree = 0]
 codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1307, degree = 0]
@@ -68,6 +68,6 @@ codetoanalyze/c/performance/switch_continue.c, test_switch, 3, CONDITION_ALWAYS_
 codetoanalyze/c/performance/switch_continue.c, test_switch, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0]
 codetoanalyze/c/performance/switch_continue.c, unroll_loop, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/c/performance/switch_continue.c, unroll_loop, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/c/performance/switch_continue.c, unroll_loop, 14, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 25 + 12 ⋅ (n - 1), degree = 1,{n - 1},Loop at line 43, column 11]
+codetoanalyze/c/performance/switch_continue.c, unroll_loop, 14, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 14 + (n - 1) + 11 ⋅ (max(1, n)), degree = 1,{max(1, n)},Loop at line 43, column 11,{n - 1},Loop at line 43, column 11]
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1,{1+max(0, m)},Loop at line 13, column 3,{m},Loop at line 13, column 3]
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1,{1+max(0, m)},Loop at line 25, column 3,{m},Loop at line 25, column 3]