[PATCH] D112296: [Analyzer][solver] Handle adjustments in constraint assignor remainder

[Gabor Marton via Phabricator via cfe-commits]

martong updated this revision to Diff 382362.
martong added a comment.

- Handle adjustment in `assumeSym` for non-comparison ops.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D112296

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  clang/test/Analysis/constraint-assignor.c


Index: clang/test/Analysis/constraint-assignor.c
===================================================================
--- clang/test/Analysis/constraint-assignor.c
+++ 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();
 
 void rem_constant_rhs_ne_zero(int x, int y) {
   if (x % 3 == 0) // x % 3 != 0 -> x != 0
@@ -67,3 +66,11 @@
   if (d % 2 != 0)
     return;
 }
+
+void remainder_with_adjustment(int x, int y) {
+  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.
+}
Index: clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -41,7 +41,15 @@
       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());
+    if (Assumption) {
+      return assumeSymRel(State, SIE, BO_NE, Zero);
+    }
+    return assumeSymRel(State, SIE, BO_EQ, Zero);
+  }
+
+  if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
     BinaryOperator::Opcode Op = SSE->getOpcode();
     assert(BinaryOperator::isComparisonOp(Op));
 
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1615,14 +1615,14 @@
   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;
   }
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
@@ -342,7 +342,6 @@
   ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
                                        bool Assumption) override;
 
-protected:
   /// Assume a constraint between a symbolic expression and a concrete integer.
   virtual ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym,
                                        BinaryOperator::Opcode op,


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D112296.382362.patch
Type: text/x-patch
Size: 3417 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20211026/8f5e388c/attachment.bin>