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

[Gabor Marton via Phabricator via cfe-commits]

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

We can reuse the "adjustment" handling logic in the higher level
of the solver by calling `assumeSymRel`.

(Actually, this shows us that there is no point in separating the
`RangeConstraintManager` from the `RangedConstraintManager`, that
separation is in fact artificial. A follow-up NFC patch might
address this.)


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D112296

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.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/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1620,7 +1620,7 @@
         Builder.getBasicValueFactory().getValue(0, Sym->getType());
     // a % b != 0 implies that a != 0.
     if (!Constraint.containsZero()) {
-      State = RCM.assumeSymNE(State, LHS, Zero, Zero);
+      State = RCM.assumeSymRel(State, LHS, BO_NE, Zero);
       if (!State)
         return false;
     }
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.381476.patch
Type: text/x-patch
Size: 2163 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20211022/53f89dd4/attachment.bin>