[clang] 5f8dca0 - [Analyzer] Extend ConstraintAssignor to handle remainder op

[Gabor Marton via cfe-commits]

Author: Gabor Marton
Date: 2021-10-22T10:47:25+02:00
New Revision: 5f8dca023504ed21490a40ddc3a0241029782910

URL: https://github.com/llvm/llvm-project/commit/5f8dca023504ed21490a40ddc3a0241029782910
DIFF: https://github.com/llvm/llvm-project/commit/5f8dca023504ed21490a40ddc3a0241029782910.diff

LOG: [Analyzer] Extend ConstraintAssignor to handle remainder op

Summary:
`a % b != 0` implies that `a != 0` for any `a` and `b`. This patch
extends the ConstraintAssignor to do just that. In fact, we could do
something similar with division and in case of multiplications we could
have some other inferences, but I'd like to keep these for future
patches.

Fixes https://bugs.llvm.org/show_bug.cgi?id=51940

Reviewers: noq, vsavchenko, steakhal, szelethus, asdenyspetrov

Subscribers:

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

Added: 
    clang/test/Analysis/constraint-assignor.c

Modified: 
    clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
    clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

Removed: 
    


################################################################################
diff  --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
index 599e4ec812a1b..153b8a732166f 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
@@ -282,6 +282,11 @@ class RangeSet {
   ///             where N = size(this)
   bool contains(llvm::APSInt Point) const { return containsImpl(Point); }
 
+  bool containsZero() const {
+    APSIntType T{getMinValue()};
+    return contains(T.getZeroValue());
+  }
+
   void dump(raw_ostream &OS) const;
   void dump() const;
 

diff  --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index 7df9027b373d9..e75a207ee86ab 100644
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1610,7 +1610,28 @@ class ConstraintAssignor : public ConstraintAssignorBase<ConstraintAssignor> {
     return Assignor.assign(CoS, NewConstraint);
   }
 
+  /// Handle expressions like: a % b != 0.
+  template <typename SymT>
+  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;
+    }
+    return true;
+  }
+
   inline bool assignSymExprToConst(const SymExpr *Sym, Const Constraint);
+  inline bool assignSymIntExprToRangeSet(const SymIntExpr *Sym,
+                                         RangeSet Constraint) {
+    return handleRemainderOp(Sym, Constraint);
+  }
   inline bool assignSymSymExprToRangeSet(const SymSymExpr *Sym,
                                          RangeSet Constraint);
 
@@ -1688,9 +1709,7 @@ class ConstraintAssignor : public ConstraintAssignorBase<ConstraintAssignor> {
     if (Constraint.getConcreteValue())
       return !Constraint.getConcreteValue()->isZero();
 
-    APSIntType T{Constraint.getMinValue()};
-    Const Zero = T.getZeroValue();
-    if (!Constraint.contains(Zero))
+    if (!Constraint.containsZero())
       return true;
 
     return llvm::None;
@@ -1734,6 +1753,9 @@ bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym,
 
 bool ConstraintAssignor::assignSymSymExprToRangeSet(const SymSymExpr *Sym,
                                                     RangeSet Constraint) {
+  if (!handleRemainderOp(Sym, Constraint))
+    return false;
+
   Optional<bool> ConstraintAsBool = interpreteAsBool(Constraint);
 
   if (!ConstraintAsBool)

diff  --git a/clang/test/Analysis/constraint-assignor.c b/clang/test/Analysis/constraint-assignor.c
new file mode 100644
index 0000000000000..1c041e3e0ce45
--- /dev/null
+++ b/clang/test/Analysis/constraint-assignor.c
@@ -0,0 +1,69 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -verify
+
+// expected-no-diagnostics
+
+void clang_analyzer_warnIfReached();
+
+void rem_constant_rhs_ne_zero(int x, int y) {
+  if (x % 3 == 0) // x % 3 != 0 -> x != 0
+    return;
+  if (x * y != 0) // x * y == 0
+    return;
+  if (y != 1)     // y == 1     -> x == 0
+    return;
+  clang_analyzer_warnIfReached(); // no-warning
+  (void)x; // keep the constraints alive.
+}
+
+void rem_symbolic_rhs_ne_zero(int x, int y, int z) {
+  if (x % z == 0) // x % z != 0 -> x != 0
+    return;
+  if (x * y != 0) // x * y == 0
+    return;
+  if (y != 1)     // y == 1     -> x == 0
+    return;
+  clang_analyzer_warnIfReached(); // no-warning
+  (void)x; // keep the constraints alive.
+}
+
+void rem_symbolic_rhs_ne_zero_nested(int w, int x, int y, int z) {
+  if (w % x % z == 0) // w % x % z != 0 -> w % x != 0
+    return;
+  if (w % x * y != 0) // w % x * y == 0
+    return;
+  if (y != 1)         // y == 1         -> w % x == 0
+    return;
+  clang_analyzer_warnIfReached(); // no-warning
+  (void)(w * x); // keep the constraints alive.
+}
+
+void rem_constant_rhs_ne_zero_early_contradiction(int x, int y) {
+  if ((x + y) != 0)     // (x + y) == 0
+    return;
+  if ((x + y) % 3 == 0) // (x + y) % 3 != 0 -> (x + y) != 0 -> contradiction
+    return;
+  clang_analyzer_warnIfReached(); // no-warning
+  (void)x; // keep the constraints alive.
+}
+
+void rem_symbolic_rhs_ne_zero_early_contradiction(int x, int y, int z) {
+  if ((x + y) != 0)     // (x + y) == 0
+    return;
+  if ((x + y) % z == 0) // (x + y) % z != 0 -> (x + y) != 0 -> contradiction
+    return;
+  clang_analyzer_warnIfReached(); // no-warning
+  (void)x; // keep the constraints alive.
+}
+
+void internal_unsigned_signed_mismatch(unsigned a) {
+  int d = a;
+  // Implicit casts are not handled, thus the analyzer models `d % 2` as
+  // `(reg_$0<unsigned int a>) % 2`
+  // However, this should not result in internal signedness mismatch error when
+  // we assign new constraints below.
+  if (d % 2 != 0)
+    return;
+}