[inferbo] Prune linear bound by minmax

Summary:
Before this diff, it gave up pruning of linear bound by minmax bound.
For example, `overapprox_min (x+c1, c2+min(d1,y))` was `x+c1`.

However, we can get a bit more preciser value as follows.

```
overapprox_min (x+c1, c2+min(d1,y))
<= min (x+c1, c2+d1)
= c1+min(c2+d1-c1, x)
```

Reviewed By: ezgicicek

Differential Revision: D16543837

fbshipit-source-id: 8fdbce097

infer/src/bufferoverrun/bounds.ml

@@ -655,6 +655,16 @@ module Bound = struct
               let v = if Z.leq vmin vmeet && Z.leq vmeet vmax then vmeet else vmax in
               let d = Sign.eval_neg_if_minus sign1 Z.(v - c1) in
               mk_MinMax (c1, sign1, minmax1, d, s1)
+          | Linear (c1, x1), MinMax (c2, (Minus as sign), Max, d2, _)
+          | Linear (c1, x1), MinMax (c2, (Plus as sign), Min, d2, _)
+            when SymLinear.is_one_symbol x1 ->
+              let d = Sign.eval_big_int sign c2 d2 in
+              mk_MinMax (c1, Plus, Min, Z.(d - c1), SymLinear.get_one_symbol x1)
+          | Linear (c1, x1), MinMax (c2, (Minus as sign), Max, d2, _)
+          | Linear (c1, x1), MinMax (c2, (Plus as sign), Min, d2, _)
+            when SymLinear.is_mone_symbol x1 ->
+              let d = Sign.eval_big_int sign c2 d2 in
+              mk_MinMax (c1, Minus, Max, Z.(c1 - d), SymLinear.get_mone_symbol x1)
           | _ ->
               (* When the result is not representable, our best effort is to return the first original argument. Any other deterministic heuristics would work too. *)
               original_b1 )

infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c

@@ -365,3 +365,15 @@ void unknown_alias_Bad() {
     a[10] = 0;
   }
 }
+
+void prune_linear_by_minmax(size_t s, size_t t) {
+  if (s > 0 && s < 1000) {
+    if (t >= s + 1) {
+      size_t u = t - 2;
+    }
+  }
+}
+
+void call_prune_linear_by_minmax_Good() {
+  prune_linear_by_minmax(unknown_function(), unknown_function());
+}