[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

Author: Gabor Marton

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;
 

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)

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;
+}