https://github.com/danix800 updated
https://github.com/llvm/llvm-project/pull/65448:
>From 235f39a6a5137e53239105727798d4540e5dd563 Mon Sep 17 00:00:00 2001
From: dingfei <fd...@feysh.com>
Date: Wed, 6 Sep 2023 10:03:21 +0800
Subject: [PATCH 1/2] [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 5de99384449a4c8..9bda29c87f3c0f1 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 8210e576c98bd21..150fe20c9f37a0a 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.
+}
>From d50bf02bb4258acf05f9d7ac3e247f1f8f29c093 Mon Sep 17 00:00:00 2001
From: dingfei <fd...@feysh.com>
Date: Fri, 8 Sep 2023 13:45:03 +0800
Subject: [PATCH 2/2] [analyzer] improve constraint inferring on modulo over
concrete value
---
.../Core/RangeConstraintManager.cpp | 110 ++++++++++++++----
clang/test/Analysis/constraint-assignor.c | 70 +++++++++--
clang/test/Analysis/constraint-infer-mod.c | 62 ++++++++++
3 files changed, 209 insertions(+), 33 deletions(-)
create mode 100644 clang/test/Analysis/constraint-infer-mod.c
diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index 9bda29c87f3c0f1..ebd10e0f553a2ee 100644
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1338,6 +1338,9 @@ class SymbolicRangeInferrer
RangeSet VisitBinaryOperator(RangeSet LHS, BinaryOperator::Opcode Op,
RangeSet RHS, QualType T);
+ RangeSet handleConcreteModulo(Range LHS, llvm::APSInt Modulo, QualType T);
+ RangeSet handleRangeModulo(Range LHS, Range RHS, QualType T);
+
//===----------------------------------------------------------------------===//
// Ranges and operators
//===----------------------------------------------------------------------===//
@@ -1771,6 +1774,14 @@ template <>
RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Rem>(Range LHS,
Range RHS,
QualType T) {
+ if (const llvm::APSInt *ModOrNull = RHS.getConcreteValue()) {
+ return handleConcreteModulo(LHS, *ModOrNull, T);
+ }
+ return handleRangeModulo(LHS, RHS, T);
+}
+
+RangeSet SymbolicRangeInferrer::handleRangeModulo(Range LHS, Range RHS,
+ QualType T) {
llvm::APSInt Zero = ValueFactory.getAPSIntType(T).getZeroValue();
Range ConservativeRange = getSymmetricalRange(RHS, T);
@@ -1824,6 +1835,62 @@ RangeSet
SymbolicRangeInferrer::VisitBinaryOperator<BO_Rem>(Range LHS,
return {RangeFactory, ValueFactory.getValue(Min),
ValueFactory.getValue(Max)};
}
+RangeSet SymbolicRangeInferrer::handleConcreteModulo(Range LHS,
+ llvm::APSInt Modulo,
+ QualType T) {
+ APSIntType ResultType = ValueFactory.getAPSIntType(T);
+ llvm::APSInt Zero = ResultType.getZeroValue();
+ llvm::APSInt One = ResultType.getValue(1);
+
+ if (Modulo == Zero)
+ return RangeFactory.getEmptySet();
+ if (Modulo < 0)
+ Modulo = -Modulo;
+
+ auto ComputeModuloN = [&](llvm::APSInt From, llvm::APSInt To,
+ llvm::APSInt N) -> RangeSet {
+ assert(N > Zero && "Non-positive N!");
+ bool NonNegative = From >= Zero;
+ assert(NonNegative == (To >= Zero) && "Signedness mismatch!");
+
+ if (From > To)
+ return RangeFactory.getEmptySet();
+
+ llvm::APSInt N1 = N - One;
+
+ // spans [0, N - 1] if NonNegative or [-(N - 1), 0] otherwise.
+ if ((To - From) / N > Zero)
+ return {RangeFactory, ValueFactory.getValue(NonNegative ? Zero : -N1),
+ ValueFactory.getValue(NonNegative ? N1 : Zero)};
+
+ llvm::APSInt Min = From % N;
+ llvm::APSInt Max = To % N;
+
+ if (Min < Max) // [Min, Max]
+ return {RangeFactory, ValueFactory.getValue(Min),
+ ValueFactory.getValue(Max)};
+
+ // [0, Max] U [Min, N - 1] if NonNegative, or
+ // [-(N - 1), Max] U [Min, 0] otherwise.
+ const llvm::APSInt &Min1 = ValueFactory.getValue(NonNegative ? Zero : -N1);
+ const llvm::APSInt &Max1 = ValueFactory.getValue(Max);
+ RangeSet RS1{RangeFactory, Min1, Max1};
+
+ const llvm::APSInt &Min2 = ValueFactory.getValue(Min);
+ const llvm::APSInt &Max2 = ValueFactory.getValue(NonNegative ? N1 : Zero);
+ RangeSet RS2{RangeFactory, Min2, Max2};
+
+ return RangeFactory.unite(RS1, RS2);
+ };
+
+ if (!LHS.Includes(Zero))
+ return ComputeModuloN(LHS.From(), LHS.To(), Modulo);
+
+ // split over [From, -1] U [0, To] for easy handling.
+ return RangeFactory.unite(ComputeModuloN(LHS.From(), -One, Modulo),
+ ComputeModuloN(Zero, LHS.To(), Modulo));
+}
+
RangeSet SymbolicRangeInferrer::VisitBinaryOperator(RangeSet LHS,
BinaryOperator::Opcode Op,
RangeSet RHS, QualType T) {
@@ -2088,7 +2155,7 @@ class ConstraintAssignor : public
ConstraintAssignorBase<ConstraintAssignor> {
if (!State)
return false;
}
- } else if (auto *SIE = dyn_cast<SymIntExpr>(Sym);
+ } else if (const 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'
@@ -2105,27 +2172,28 @@ class ConstraintAssignor : public
ConstraintAssignorBase<ConstraintAssignor> {
// (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());
+ BasicValueFactory &ValueFactory = RangeFactory.getValueFactory();
+ APSIntType ResultType = ValueFactory.getAPSIntType(SIE->getType());
+ llvm::APSInt N = SIE->getRHS();
+ if (N < 0)
+ N = -N;
+ N = ResultType.convert(N);
+
+ SymbolRef Sym = SIE->getLHS();
+ RangeSet RS = SymbolicRangeInferrer::inferRange(RangeFactory, State,
Sym);
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;
- }
- }
+ Range R = *RS.begin();
+ llvm::APSInt Distance = ResultType.convert(R.To()).extend(64) -
+ ResultType.convert(R.From()).extend(64);
+ if (Distance < 0) // overflows
+ return true;
+
+ if (Distance < N.extend(64)) {
+ const llvm::APSInt &Point = ValueFactory.getValue(
+ (ResultType.convert(R.To() > 0 ? R.To() : R.From())) / N * N);
+ State = assign(Sym, {RangeFactory, Point, Point});
+ if (!State)
+ return false;
}
}
}
diff --git a/clang/test/Analysis/constraint-assignor.c
b/clang/test/Analysis/constraint-assignor.c
index 150fe20c9f37a0a..2fd0776b829852e 100644
--- a/clang/test/Analysis/constraint-assignor.c
+++ b/clang/test/Analysis/constraint-assignor.c
@@ -84,7 +84,7 @@ void remainder_with_adjustment_of_composit_lhs(int x, int y) {
(void)(x * y); // keep the constraints alive.
}
-void remainder_infeasible(int x, int y) {
+void remainder_infeasible_positive_range(int x) {
if (x <= 2 || x >= 5)
return;
if (x % 5 != 0)
@@ -93,52 +93,98 @@ void remainder_infeasible(int x, int y) {
(void)x; // keep the constraints alive.
}
-void remainder_within_modulo_positive_range_unsigned(unsigned x) {
+void remainder_infeasible_negative_range(int x) {
+ if (x <= -14 || x >= -1)
+ return;
+ if (x % 15 != 0)
+ return;
+ clang_analyzer_warnIfReached(); // no-warning
+ (void)x; // keep the constraints alive.
+}
+
+void remainder_within_modulo_positive_range_unsigned_1(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}}
+ clang_analyzer_dump(x); // expected-warning{{5 S32b}}
+ (void)x; // keep the constraints alive.
+}
+
+void remainder_within_modulo_positive_range_unsigned_2(unsigned char x) {
+ if (x < 252 || x > 254)
+ return;
+ if (x % 5 != 0)
+ return;
+ clang_analyzer_dump(x); // no-warning
+ (void)x; // keep the constraints alive.
+}
+
+void remainder_within_modulo_positive_range_unsigned_3(unsigned x) {
+ if (x < 4294967289 || x > 4294967294)
+ return;
+ if (x % 10 != 0)
+ return;
+ clang_analyzer_eval(x == 4294967290); // expected-warning{{TRUE}}
(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}}
+ 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}}
+ 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}}
+ 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}}
+ clang_analyzer_dump(x); // expected-warning{{5 S32b}}
+ (void)x; // keep the constraints alive.
+}
+
+#define LONG_MIN (-0x7fffffffffffffffL - 1L)
+#define LONG_MAX 0x7fffffffffffffffL
+void remainder_within_modulo_distance_overflow(long x) {
+ if (x < LONG_MIN + 1 || x > LONG_MAX - 1)
+ return;
+
+ if (x % 10 != 0)
+ return;
+ clang_analyzer_dump(x); // expected-warning{{reg_$0<long x>}}
+ (void)x; // keep the constraints alive.
+}
+
+#define CHAR_MIN (-0x7f - 1)
+#define CHAR_MAX 0x7f
+void remainder_within_modulo_not_overflow(char x) {
+ if (x < CHAR_MIN + 1 || x > CHAR_MAX - 1)
+ return;
+
+ if (x % (CHAR_MAX * 2) != 0)
+ return;
+ clang_analyzer_dump(x); // expected-warning{{0 S32b}}
(void)x; // keep the constraints alive.
}
diff --git a/clang/test/Analysis/constraint-infer-mod.c
b/clang/test/Analysis/constraint-infer-mod.c
new file mode 100644
index 000000000000000..eb800da865b1688
--- /dev/null
+++ b/clang/test/Analysis/constraint-infer-mod.c
@@ -0,0 +1,62 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN: -analyzer-checker=core \
+// RUN: -analyzer-checker=debug.ExprInspection \
+// RUN: -verify
+
+void clang_analyzer_warnIfReached(void);
+void clang_analyzer_eval(int);
+void clang_analyzer_dump(int);
+
+void remainder_infer_positive_range(int x) {
+ if (x < 5 || x > 7)
+ return;
+
+ int y = x % 16;
+ clang_analyzer_eval(y >= 5 && y <= 7); // expected-warning{{TRUE}}
+ (void)x; // keep the constraints alive.
+}
+
+void remainder_infer_positive_range_full(int x) {
+ if (x < 9 || x > 51)
+ return;
+
+ int y = x % 10;
+ clang_analyzer_eval(y >= 0 && y <= 9); // expected-warning{{TRUE}}
+ (void)x; // keep the constraints alive.
+}
+
+void remainder_infer_negative_range(int x) {
+ if (x < -7 || x > -5)
+ return;
+
+ int y = x % 16;
+ clang_analyzer_eval(y >= -7 && y <= -5); // expected-warning{{TRUE}}
+ (void)x; // keep the constraints alive.
+}
+
+void remainder_infer_positive_range_wraparound(int x) {
+ if (x < 30 || x > 33)
+ return;
+
+ int y = x % 16;
+ clang_analyzer_eval((y >= 0 && y <= 1) || (y >= 14 && y <= 15)); //
expected-warning{{TRUE}}
+ (void)x; // keep the constraints alive.
+}
+
+void remainder_infer_negative_range_wraparound(int x) {
+ if (x < -33 || x > -30)
+ return;
+
+ int y = x % 16;
+ clang_analyzer_eval((y >= -1 && y <= 0) || (y >= -15 && y <= -14)); //
expected-warning{{TRUE}}
+ (void)x; // keep the constraints alive.
+}
+
+void remainder_infer_range_spans_zero(int x) {
+ if (x < -7 || x > 5)
+ return;
+
+ int y = x % 10;
+ clang_analyzer_eval(y >= -7 && y <= 5); // expected-warning{{TRUE}}
+ (void)x; // keep the constraints alive.
+}
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
