From 80f4b64915e431ad12922ecff96b391f3c75f375 Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Tue, 30 Jul 2019 06:45:45 -0700
Subject: [PATCH] [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                    | 10 ++++++++++
 .../codetoanalyze/c/bufferoverrun/prune_alias.c      | 12 ++++++++++++
 2 files changed, 22 insertions(+)

diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml
index 6bda8e3d8..7102dbc2c 100644
--- a/infer/src/bufferoverrun/bounds.ml
+++ b/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 )
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c
index 247263cb3..bce597fa1 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c
+++ b/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());
+}