From 1a75fa9ebd45ff9d481e9e6e487bc3c7a542c0dd Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Tue, 21 Aug 2018 01:16:51 -0700
Subject: [PATCH] [inferbo] Propagate INFERBO_ALLOC_MAY_BE_ even when the bound
 is infinity

Reviewed By: skcho

Differential Revision: D9398450

fbshipit-source-id: 7b676615e
---
 .../bufferOverrunProofObligations.ml          |  2 +-
 .../c/bufferoverrun/issue_kinds.c             | 43 ++++++++++++-------
 .../codetoanalyze/c/bufferoverrun/issues.exp  |  1 +
 3 files changed, 29 insertions(+), 17 deletions(-)

diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
index 98c181272..a14cbbaab 100644
--- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
+++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
@@ -82,7 +82,7 @@ module AllocSizeCondition = struct
         | cmp_big ->
             let propagate =
               match (cmp_mone, cmp_big) with
-              | `NotComparable, _ | _, `NotComparable ->
+              | (`NotComparable | `LeftSubsumesRight), _ | _, (`NotComparable | `LeftSubsumesRight) ->
                   true
               | _ ->
                   false
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c
index fe35645f6..44da37b52 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c
@@ -5,6 +5,22 @@
  * LICENSE file in the root directory of this source tree.
  */
 
+int zero_or_ten(int ten) {
+  if (ten) {
+    return 10;
+  } else {
+    return 0;
+  }
+}
+
+int zero_to_infty() {
+  int r = 0;
+  for (int i = 0; i < zero_or_ten(0); i++) {
+    r++;
+  }
+  return r;
+}
+
 void l1_concrete_overrun_Bad() {
   int a[10];
   a[10] = 0;
@@ -29,14 +45,6 @@ void l1_symbolic_underrun_Bad(int i) {
   }
 }
 
-int zero_or_ten(int ten) {
-  if (ten) {
-    return 10;
-  } else {
-    return 0;
-  }
-}
-
 void l2_concrete_overrun_Bad() {
   int a[10];
   a[zero_or_ten(1)] = 0;
@@ -157,6 +165,17 @@ void alloc_may_be_big_Good_FP() {
   malloc(zero_or_ten(1) * 100 * 1000 * 1000 + 1);
 }
 
+/*
+  When the upper bound is infinity and the lower bound unknown,
+  we don't report but still propagate the error.
+*/
+void alloc_may_be_big2_Silenced(int n) { malloc(n + zero_to_infty()); }
+
+// Now that we have a lower bound, we can report it
+void call_to_alloc_may_be_big2_is_big_Bad() {
+  alloc_may_be_big2_Silenced(100 * 1000 * 1000);
+}
+
 void l1_unknown_function_Bad() {
   int a[5];
   int idx = unknown_function() * 10;
@@ -167,14 +186,6 @@ void l1_unknown_function_Bad() {
   }
 }
 
-int zero_to_infty() {
-  int r = 0;
-  for (int i = 0; i < zero_or_ten(0); i++) {
-    r++;
-  }
-  return r;
-}
-
 /* Inferbo raises U5 alarm because
    - the pair of offset:[10,10] and size:[5,+oo] is belong to L3
    - the offset value is from an unknown function
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
index 221cdf902..ca8f69886 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
@@ -34,6 +34,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Bad, 0, INFERBO_AL
 codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Good_FP, 1, INFERBO_ALLOC_MAY_BE_BIG, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [1, 1000000001]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Bad, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [-5, 5]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Good_FP, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [-5, 5]]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Bad, 1, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Call,Parameter: n,Alloc: Length: [100000000, +oo] by call to `alloc_may_be_big2_Silenced` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [max(10, i.lb), i.ub] Size: 10]