[Analyzer][solver] Handle adjustments in constraint assignor remainder

We can reuse the "adjustment" handling logic in the higher level
of the solver by calling `State->assume`.

Differential Revision: https://reviews.llvm.org/D112296

3 files changed, 29 insertions, 9 deletions

diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index 77f97da4322b..6e4ee6e337ce 100644
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1614,14 +1614,14 @@ public:
   bool handleRemainderOp(const SymT *Sym, RangeSet Constraint) {
     if (Sym->getOpcode() != BO_Rem)
       return true;
-    const SymbolRef LHS = Sym->getLHS();
-    const llvm::APSInt &Zero =
-        Builder.getBasicValueFactory().getValue(0, Sym->getType());
     // a % b != 0 implies that a != 0.
     if (!Constraint.containsZero()) {
-      State = RCM.assumeSymNE(State, LHS, Zero, Zero);
-      if (!State)
-        return false;
+      SVal SymSVal = Builder.makeSymbolVal(Sym->getLHS());
+      if (auto NonLocSymSVal = SymSVal.getAs<nonloc::SymbolVal>()) {
+        State = State->assume(*NonLocSymSVal, true);
+        if (!State)
+          return false;
+      }
     }
     return true;
   }
diff --git a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
index 80f3054a5a37..892d64ea4e4e 100644
--- a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -41,7 +41,12 @@ ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
       return assumeSymRel(State, SIE->getLHS(), op, SIE->getRHS());
     }
 
-  } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
+    // Handle adjustment with non-comparison ops.
+    const llvm::APSInt &Zero = getBasicVals().getValue(0, SIE->getType());
+    return assumeSymRel(State, SIE, (Assumption ? BO_NE : BO_EQ), Zero);
+  }
+
+  if (const auto *SSE = dyn_cast<SymSymExpr>(Sym)) {
     BinaryOperator::Opcode Op = SSE->getOpcode();
     assert(BinaryOperator::isComparisonOp(Op));
 
diff --git a/clang/test/Analysis/constraint-assignor.c b/clang/test/Analysis/constraint-assignor.c
index 1c041e3e0ce4..1b9e40e6bf64 100644
--- a/clang/test/Analysis/constraint-assignor.c
+++ b/clang/test/Analysis/constraint-assignor.c
@@ -3,9 +3,8 @@
 // RUN:   -analyzer-checker=debug.ExprInspection \
 // RUN:   -verify
 
-// expected-no-diagnostics
-
 void clang_analyzer_warnIfReached();
+void clang_analyzer_eval(int);
 
 void rem_constant_rhs_ne_zero(int x, int y) {
   if (x % 3 == 0) // x % 3 != 0 -> x != 0
@@ -67,3 +66,19 @@ void internal_unsigned_signed_mismatch(unsigned a) {
   if (d % 2 != 0)
     return;
 }
+
+void remainder_with_adjustment(int x) {
+  if ((x + 1) % 3 == 0) // (x + 1) % 3 != 0 -> x + 1 != 0 -> x != -1
+    return;
+  clang_analyzer_eval(x + 1 != 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(x != -1);    // expected-warning{{TRUE}}
+  (void)x; // keep the constraints alive.
+}
+
+void remainder_with_adjustment_of_composit_lhs(int x, int y) {
+  if ((x + y + 1) % 3 == 0) // (x + 1) % 3 != 0 -> x + 1 != 0 -> x != -1
+    return;
+  clang_analyzer_eval(x + y + 1 != 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(x + y != -1);    // expected-warning{{TRUE}}
+  (void)(x * y); // keep the constraints alive.
+}