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

[Gabor Marton via Phabricator via cfe-commits]

martong abandoned this revision.
martong added inline comments.



Comment at: clang/test/Analysis/constraint_manager_negate_difference.c:125-130
 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}}
   }
 }

Actually, this test case was correct, because UINT_MID is a special value and 
for that
```
_Static_assert(UINT_MID == -UINT_MID, "");
```
holds.
So, this patch is meaningless.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D125379

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

[Balázs Benics via Phabricator via cfe-commits]

steakhal added a comment.

Seems reasonable.




Comment at: clang/test/Analysis/constraint_manager_negate_difference.c:145-148
+// 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}}

It's not immediately clear what you refer to by the `TRUE` case. The two evals 
the opposite condition, consequently one of them should be `FALSE`. Same for 
the next case.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D125379

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[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  = State->getSymbolManager();


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}}
+