[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

[Manas Gupta via Phabricator via cfe-commits]

manas updated this revision to Diff 349796.
manas added a comment.

Fix for cases involving residual paths and add case for overflowing range near extremum of a type


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D103440/new/

https://reviews.llvm.org/D103440

Files:
  clang/test/Analysis/constant-folding.c


Index: clang/test/Analysis/constant-folding.c
===================================================================
--- clang/test/Analysis/constant-folding.c
+++ clang/test/Analysis/constant-folding.c
@@ -251,3 +251,83 @@
     clang_analyzer_eval((b % a) < x + 10); // expected-warning{{TRUE}}
   }
 }
+
+void testAdditionRules(unsigned int a, unsigned int b, int c, int d) {
+  if (a == 0) {
+    clang_analyzer_eval((a + 0) == 0); // expected-warning{{TRUE}}
+  }
+
+  // Checks for unsigned operands
+  clang_analyzer_eval((a + b) < 0); // expected-warning{{FALSE}}
+  clang_analyzer_eval((a + b) <= UINT_MAX); // expected-warning{{TRUE}}
+
+  if (a == UINT_MAX && b == UINT_MAX) {
+    clang_analyzer_eval((a + b) == UINT_MAX - 1); // expected-warning{{TRUE}}
+  }
+
+  // Checks for inclusive ranges for unsigned integers
+  if (a >= 0 && a <= 10 && b >= 0 && b <= 20) {
+    clang_analyzer_eval((a + b) >= 0); // expected-warning{{TRUE}}
+    clang_analyzer_eval((a + b) > 30); // expected-warning{{FALSE}}
+  }
+
+  // Checks for negative signed integers
+  if (c < 0 && d < 0) {
+    clang_analyzer_eval((c + d) < 0); // expected-warning{{UNKNOWN}}
+  }
+
+  if (c < 0 && c != INT_MIN && d < 0) {
+    clang_analyzer_eval((c + d) == -1); // expected-warning{{FALSE}}
+    clang_analyzer_eval((c + d) == 0); // expected-warning{{FALSE}}
+    clang_analyzer_eval((c + d) <= -2); // expected-warning{{UNKNOWN}}
+    clang_analyzer_eval((c + d) >= 1); // expected-warning{{UNKNOWN}}
+  }
+
+  if (c == INT_MIN && d == INT_MIN) {
+    clang_analyzer_eval((c + d) == 0); // expected-warning{{TRUE}}
+  }
+
+  if (c == INT_MIN && d < 0 && d != INT_MIN) {
+    clang_analyzer_eval((c + d) > 0); // expected-warning{{TRUE}}
+  }
+
+  if (c < 0 && c >= -20 && d < 0 && d >= -40) {
+    clang_analyzer_eval((c + d) < -1); // expected-warning{{TRUE}}
+    clang_analyzer_eval((c + d) >= -60); // expected-warning{{TRUE}}
+  }
+
+  // Checks for integers with different sign bits
+  if (c < 0 && d > 0) {
+    if (c >= -20 && d <= 10) {
+      clang_analyzer_eval((c + d) > -20); // expected-warning{{TRUE}}
+      clang_analyzer_eval((c + d) < 10); // expected-warning{{TRUE}}
+    }
+  }
+
+  // Checks for overlapping signed integers ranges
+  if (c >= -20 && c <= 20 && d >= -10 && d <= 10) {
+    clang_analyzer_eval((c + d) >= -30); // expected-warning{{TRUE}}
+    clang_analyzer_eval((c + d) <= 30); // expected-warning{{TRUE}}
+  }
+
+  // Checks for positive signed integers
+  if (c > 0 && d > 0) {
+    clang_analyzer_eval((c + d) == 1); // expected-warning{{FALSE}}
+    clang_analyzer_eval((c + d) == 0); // expected-warning{{FALSE}}
+    clang_analyzer_eval((c + d) == -1); // expected-warning{{FALSE}}
+    clang_analyzer_eval((c + d) > 1); // expected-warning{{UNKNOWN}}
+    clang_analyzer_eval((c + d) < -1); // expected-warning{{UNKNOWN}}
+  }
+
+  // Checks producing overflowing range with different signs
+  int HALF_INT_MAX = INT_MAX / 2;
+  if (c >= HALF_INT_MAX - 10 && c <= HALF_INT_MAX + 10 &&
+      d >= HALF_INT_MAX - 10 && d <= HALF_INT_MAX + 10) {
+    // The resulting range for (c + d) will be:
+    //   [INT_MIN, INT_MIN + 18] U [INT_MAX - 21, INT_MAX]
+    clang_analyzer_eval((c + d) <= INT_MIN + 18); // expected-warning{{UNKNOWN}}
+    clang_analyzer_eval((c + d) >= INT_MAX - 21); // expected-warning{{UNKNOWN}}
+    clang_analyzer_eval((c + d) == INT_MIN + 19); // expected-warning{{FALSE}}
+    clang_analyzer_eval((c + d) == INT_MAX - 22); // expected-warning{{FALSE}}
+  }
+}


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D103440.349796.patch
Type: text/x-patch
Size: 3516 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20210604/70de85c1/attachment.bin>