[clang] [analyzer] Reduce constraint on modulo with small concrete range (PR #65448)

[Ding Fei via cfe-commits]

https://github.com/danix800 updated https://github.com/llvm/llvm-project/pull/65448:

>From 235f39a6a5137e53239105727798d4540e5dd563 Mon Sep 17 00:00:00 2001
From: dingfei <fding at feysh.com>
Date: Wed, 6 Sep 2023 10:03:21 +0800
Subject: [PATCH] [analyzer] Reduce constraint on modulo with small concrete
 range

---
 .../Core/RangeConstraintManager.cpp           | 48 +++++++++++++++
 clang/test/Analysis/constraint-assignor.c     | 60 +++++++++++++++++++
 2 files changed, 108 insertions(+)

diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index 5de99384449a4c..9bda29c87f3c0f 100644
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -2073,6 +2073,14 @@ class ConstraintAssignor : public ConstraintAssignorBase<ConstraintAssignor> {
     if (Sym->getOpcode() != BO_Rem)
       return true;
     // a % b != 0 implies that a != 0.
+    // Z3 verification:
+    //   (declare-const a Int)
+    //   (declare-const m Int)
+    //   (assert (not (= m 0)))
+    //   (assert (not (= (mod a m) 0)))
+    //   (assert (= a 0))
+    //   (check-sat)
+    //   ; unsat
     if (!Constraint.containsZero()) {
       SVal SymSVal = Builder.makeSymbolVal(Sym->getLHS());
       if (auto NonLocSymSVal = SymSVal.getAs<nonloc::SymbolVal>()) {
@@ -2080,6 +2088,46 @@ class ConstraintAssignor : public ConstraintAssignorBase<ConstraintAssignor> {
         if (!State)
           return false;
       }
+    } else if (auto *SIE = dyn_cast<SymIntExpr>(Sym);
+               SIE && Constraint.encodesFalseRange()) {
+      // a % m == 0 && a in [x, y] && y - x < m implies that
+      // a = (y < 0 ? x : y) / m * m which is a 'ConcreteInt'
+      // where x and m are 'ConcreteInt'.
+      //
+      // Z3 verification:
+      //   (declare-const a Int)
+      //   (declare-const m Int)
+      //   (declare-const x Int)
+      //   (declare-const y Int)
+      //   (assert (= (mod a m) 0))
+      //   (assert (< (- y x) m))
+      //   (assert (and (>= a x) (<= a y)))
+      //   (assert (not (= a (* (div y m) m))))
+      //   (check-sat)
+      //   ; unsat
+      llvm::APSInt Modulo = SIE->getRHS();
+      Modulo = llvm::APSInt(Modulo.abs(), Modulo.isUnsigned());
+      RangeSet RS =
+          SymbolicRangeInferrer::inferRange(RangeFactory, State, SIE->getLHS());
+      if (RS.size() == 1) {
+        auto R = RS.begin();
+        if ((R->To() - R->From()).getExtValue() < Modulo.getExtValue()) {
+          SVal SymSVal = Builder.makeSymbolVal(SIE->getLHS());
+          if (auto NonLocSymSVal = SymSVal.getAs<nonloc::SymbolVal>()) {
+            auto NewConstConstraint = Builder.makeIntVal(
+                (R->To() > 0 ? R->To() : R->From()) / Modulo * Modulo);
+            if (auto Cond = Builder
+                                .evalBinOp(State, BO_EQ, *NonLocSymSVal,
+                                           NewConstConstraint,
+                                           Builder.getConditionType())
+                                .template getAs<DefinedOrUnknownSVal>()) {
+              State = State->assume(*Cond, true);
+              if (!State)
+                return false;
+            }
+          }
+        }
+      }
     }
     return true;
   }
diff --git a/clang/test/Analysis/constraint-assignor.c b/clang/test/Analysis/constraint-assignor.c
index 8210e576c98bd2..150fe20c9f37a0 100644
--- a/clang/test/Analysis/constraint-assignor.c
+++ b/clang/test/Analysis/constraint-assignor.c
@@ -5,6 +5,7 @@
 
 void clang_analyzer_warnIfReached(void);
 void clang_analyzer_eval(int);
+void clang_analyzer_dump(int);
 
 void rem_constant_rhs_ne_zero(int x, int y) {
   if (x % 3 == 0) // x % 3 != 0 -> x != 0
@@ -82,3 +83,62 @@ void remainder_with_adjustment_of_composit_lhs(int x, int y) {
   clang_analyzer_eval(x + y != -1);    // expected-warning{{TRUE}}
   (void)(x * y); // keep the constraints alive.
 }
+
+void remainder_infeasible(int x, int y) {
+  if (x <= 2 || x >= 5)
+    return;
+  if (x % 5 != 0)
+    return;
+  clang_analyzer_warnIfReached(); // no-warning
+  (void)x; // keep the constraints alive.
+}
+
+void remainder_within_modulo_positive_range_unsigned(unsigned x) {
+  if (x <= 2 || x > 6)
+    return;
+  clang_analyzer_dump(x); // expected-warning{{reg_$0<unsigned int x>}}
+  if (x % 5 != 0)
+    return;
+  clang_analyzer_dump(x);          // expected-warning{{5 S32b}}
+  (void)x; // keep the constraints alive.
+}
+
+void remainder_within_modulo_positive_range(int x) {
+  if (x <= 2 || x > 6)
+    return;
+  clang_analyzer_dump(x); // expected-warning{{reg_$0<int x>}}
+  if (x % 5 != 0)
+    return;
+  clang_analyzer_dump(x);          // expected-warning{{5 S32b}}
+  (void)x; // keep the constraints alive.
+}
+
+void remainder_within_modulo_range_spans_zero(int x) {
+  if (x <= -2 || x > 2)
+    return;
+  clang_analyzer_dump(x); // expected-warning{{reg_$0<int x>}}
+  if (x % 5 != 0)
+    return;
+  clang_analyzer_dump(x);          // expected-warning{{0 S32b}}
+  (void)x; // keep the constraints alive.
+}
+
+void remainder_within_modulo_negative_range(int x) {
+  if (x <= -7 || x > -2)
+    return;
+  clang_analyzer_dump(x); // expected-warning{{reg_$0<int x>}}
+  if (x % 5 != 0)
+    return;
+  clang_analyzer_dump(x);          // expected-warning{{-5 S32b}}
+  (void)x; // keep the constraints alive.
+}
+
+void remainder_within_modulo_range_neg_mod(int x) {
+  if (x <= 2 || x > 6)
+    return;
+  clang_analyzer_dump(x); // expected-warning{{reg_$0<int x>}}
+  if (x % -5 != 0)
+    return;
+  clang_analyzer_dump(x);          // expected-warning{{5 S32b}}
+  (void)x; // keep the constraints alive.
+}