[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

[Gabor Marton via Phabricator via cfe-commits]

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

We should track non-equivalency (disequality) in case of greater-then or
less-then assumptions.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D88019

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


Index: clang/test/Analysis/equality_tracking.c
===================================================================
--- clang/test/Analysis/equality_tracking.c
+++ clang/test/Analysis/equality_tracking.c
@@ -185,3 +185,37 @@
     }
   }
 }
+
+void avoidInfeasibleConstraintforGT(int a, int b) {
+  int c = b - a;
+  if (c <= 0)
+    return;
+  // c > 0
+  // b - a > 0
+  // b > a
+  if (a != b) {
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+    return;
+  }
+  clang_analyzer_warnIfReached(); // no warning
+  // a == b
+  if (c < 0)
+    ;
+}
+
+void avoidInfeasibleConstraintforLT(int a, int b) {
+  int c = b - a;
+  if (c >= 0)
+    return;
+  // c < 0
+  // b - a < 0
+  // b < a
+  if (a != b) {
+    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+    return;
+  }
+  clang_analyzer_warnIfReached(); // no warning
+  // a == b
+  if (c < 0)
+    ;
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -2104,7 +2104,12 @@
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {
   RangeSet New = getSymLTRange(St, Sym, Int, Adjustment);
-  return New.isEmpty() ? nullptr : setConstraint(St, Sym, New);
+  if (New.isEmpty())
+    // this is infeasible assumption
+    return nullptr;
+
+  ProgramStateRef NewState = setConstraint(St, Sym, New);
+  return trackNE(NewState, Sym, Int, Adjustment);
 }
 
 RangeSet RangeConstraintManager::getSymGTRange(ProgramStateRef St,
@@ -2140,7 +2145,12 @@
                                     const llvm::APSInt &Int,
                                     const llvm::APSInt &Adjustment) {
   RangeSet New = getSymGTRange(St, Sym, Int, Adjustment);
-  return New.isEmpty() ? nullptr : setConstraint(St, Sym, New);
+  if (New.isEmpty())
+    // this is infeasible assumption
+    return nullptr;
+
+  ProgramStateRef NewState = setConstraint(St, Sym, New);
+  return trackNE(NewState, Sym, Int, Adjustment);
 }
 
 RangeSet RangeConstraintManager::getSymGERange(ProgramStateRef St,


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D88019.293142.patch
Type: text/x-patch
Size: 2249 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20200921/eaba719f/attachment.bin>