[PATCH] D125379: [analyzer][solver] Do not negate unsigned ranges

[Gabor Marton via Phabricator via cfe-commits]

martong created this revision.
martong added reviewers: NoQ, steakhal.
Herald added subscribers: manas, ASDenysPetrov, gamesh411, dkrupp, donat.nagy, Szelethus, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, xazax.hun.
Herald added a reviewer: Szelethus.
Herald added a project: All.
martong requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

This is a bugfix. Simply put, 2u - 1u != 2u - 1u. See the static
assertion in the test file. The fix simply ban the negation of unsigned
expressions. This way the we are getting a little bit more conservatie,
but at least we do not infer wrong values.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D125379

Files:
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/test/Analysis/constraint_manager_negate_difference.c


Index: clang/test/Analysis/constraint_manager_negate_difference.c
===================================================================
--- clang/test/Analysis/constraint_manager_negate_difference.c
+++ clang/test/Analysis/constraint_manager_negate_difference.c
@@ -122,31 +122,37 @@
   }
 }
 
+_Static_assert(12u - 1u != 1u - 12u, "Good modulo arithmetic");
 void negate_unsigned_mid(unsigned m, unsigned n) {
   if (m - n == UINT_MID) {
-    clang_analyzer_eval(n - m == UINT_MID); // expected-warning{{TRUE}}
-    clang_analyzer_eval(n - m != UINT_MID); // expected-warning{{FALSE}}
+    clang_analyzer_eval(n - m == UINT_MID); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+    clang_analyzer_eval(n - m != UINT_MID); // expected-warning{{FALSE}} expected-warning{{TRUE}}
   }
 }
 
 void negate_unsigned_mid2(unsigned m, unsigned n) {
   if (m - n < UINT_MID && m - n > UINT_MIN) {
-    clang_analyzer_eval(n - m > UINT_MID); // expected-warning{{TRUE}}
-    clang_analyzer_eval(n - m < UINT_MID); // expected-warning{{FALSE}}
+    clang_analyzer_eval(n - m > UINT_MID); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+    clang_analyzer_eval(n - m < UINT_MID); // expected-warning{{FALSE}} expected-warning{{TRUE}}
   }
 }
 
+
+_Static_assert(1u - 2u == UINT_MAX, "Good modulo arithmetic");
+_Static_assert(2u - 1u == 1, "Good modulo arithmetic");
 void negate_unsigned_max(unsigned m, unsigned n) {
   if (m - n == UINT_MAX) {
-    clang_analyzer_eval(n - m == 1); // expected-warning{{TRUE}}
-    clang_analyzer_eval(n - m != 1); // expected-warning{{FALSE}}
+    // FIXME only the TRUE case should appear. But it is better to be
+    // conservative than faulty.
+    clang_analyzer_eval(n - m == 1); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+    clang_analyzer_eval(n - m != 1); // expected-warning{{FALSE}} expected-warning{{TRUE}}
   }
 }
-
 void negate_unsigned_one(unsigned m, unsigned n) {
   if (m - n == 1) {
-    clang_analyzer_eval(n - m == UINT_MAX); // expected-warning{{TRUE}}
-    clang_analyzer_eval(n - m < UINT_MAX);  // expected-warning{{FALSE}}
+    // FIXME only the TRUE case should appear.
+    clang_analyzer_eval(n - m == UINT_MAX); // expected-warning{{TRUE}} expected-warning{{FALSE}}
+    clang_analyzer_eval(n - m < UINT_MAX);  // expected-warning{{FALSE}} expected-warning{{TRUE}}
   }
 }
 
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1454,8 +1454,7 @@
         QualType T = Sym->getType();
 
         // Do not negate unsigned ranges
-        if (!T->isUnsignedIntegerOrEnumerationType() &&
-            !T->isSignedIntegerOrEnumerationType())
+        if (T->isUnsignedIntegerOrEnumerationType())
           return llvm::None;
 
         SymbolManager &SymMgr = State->getSymbolManager();


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D125379.428633.patch
Type: text/x-patch
Size: 2968 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20220511/0604914d/attachment.bin>