[clang] 73c120a - [analyzer] Introduce reasoning about symbolic remainder operator
Valeriy Savchenko via cfe-commits
cfe-commits at lists.llvm.org
Thu May 28 08:57:25 PDT 2020
Author: Valeriy Savchenko
Date: 2020-05-28T18:56:38+03:00
New Revision: 73c120a9895a7e12e3c29a755d64096c8bd0220f
URL: https://github.com/llvm/llvm-project/commit/73c120a9895a7e12e3c29a755d64096c8bd0220f
DIFF: https://github.com/llvm/llvm-project/commit/73c120a9895a7e12e3c29a755d64096c8bd0220f.diff
LOG: [analyzer] Introduce reasoning about symbolic remainder operator
Summary:
New logic tries to narrow possible result values of the remainder operation
based on its operands and their ranges. It also tries to be conservative
with negative operands because according to the standard the sign of
the result is implementation-defined.
rdar://problem/44978988
Differential Revision: https://reviews.llvm.org/D80117
Added:
clang/test/Analysis/PR35418.cpp
clang/test/Analysis/uninit-bug-first-iteration-init.c
Modified:
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
clang/test/Analysis/constant-folding.c
clang/test/Analysis/hangs.c
Removed:
################################################################################
diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index b73c395d80fa..6f92b965ce5b 100644
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -433,6 +433,8 @@ class SymbolicRangeInferrer
return VisitBinaryOperator<BO_Or>(LHS, RHS, T);
case BO_And:
return VisitBinaryOperator<BO_And>(LHS, RHS, T);
+ case BO_Rem:
+ return VisitBinaryOperator<BO_Rem>(LHS, RHS, T);
default:
return infer(T);
}
@@ -496,6 +498,46 @@ class SymbolicRangeInferrer
return infer(T);
}
+ /// Return a symmetrical range for the given range and type.
+ ///
+ /// If T is signed, return the smallest range [-x..x] that covers the original
+ /// range, or [-min(T), max(T)] if the aforementioned symmetric range doesn't
+ /// exist due to original range covering min(T)).
+ ///
+ /// If T is unsigned, return the smallest range [0..x] that covers the
+ /// original range.
+ Range getSymmetricalRange(Range Origin, QualType T) {
+ APSIntType RangeType = ValueFactory.getAPSIntType(T);
+
+ if (RangeType.isUnsigned()) {
+ return Range(ValueFactory.getMinValue(RangeType), Origin.To());
+ }
+
+ if (Origin.From().isMinSignedValue()) {
+ // If mini is a minimal signed value, absolute value of it is greater
+ // than the maximal signed value. In order to avoid these
+ // complications, we simply return the whole range.
+ return {ValueFactory.getMinValue(RangeType),
+ ValueFactory.getMaxValue(RangeType)};
+ }
+
+ // At this point, we are sure that the type is signed and we can safely
+ // use unary - operator.
+ //
+ // While calculating absolute maximum, we can use the following formula
+ // because of these reasons:
+ // * If From >= 0 then To >= From and To >= -From.
+ // AbsMax == To == max(To, -From)
+ // * If To <= 0 then -From >= -To and -From >= From.
+ // AbsMax == -From == max(-From, To)
+ // * Otherwise, From <= 0, To >= 0, and
+ // AbsMax == max(abs(From), abs(To))
+ llvm::APSInt AbsMax = std::max(-Origin.From(), Origin.To());
+
+ // Intersection is guaranteed to be non-empty.
+ return {ValueFactory.getValue(-AbsMax), ValueFactory.getValue(AbsMax)};
+ }
+
/// Return a range set subtracting zero from \p Domain.
RangeSet assumeNonZero(RangeSet Domain, QualType T) {
APSIntType IntType = ValueFactory.getAPSIntType(T);
@@ -635,6 +677,63 @@ RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_And>(Range LHS,
return infer(T);
}
+template <>
+RangeSet SymbolicRangeInferrer::VisitBinaryOperator<BO_Rem>(Range LHS,
+ Range RHS,
+ QualType T) {
+ llvm::APSInt Zero = ValueFactory.getAPSIntType(T).getZeroValue();
+
+ Range ConservativeRange = getSymmetricalRange(RHS, T);
+
+ llvm::APSInt Max = ConservativeRange.To();
+ llvm::APSInt Min = ConservativeRange.From();
+
+ if (Max == Zero) {
+ // It's an undefined behaviour to divide by 0 and it seems like we know
+ // for sure that RHS is 0. Let's say that the resulting range is
+ // simply infeasible for that matter.
+ return RangeFactory.getEmptySet();
+ }
+
+ // At this point, our conservative range is closed. The result, however,
+ // couldn't be greater than the RHS' maximal absolute value. Because of
+ // this reason, we turn the range into open (or half-open in case of
+ // unsigned integers).
+ //
+ // While we operate on integer values, an open interval (a, b) can be easily
+ // represented by the closed interval [a + 1, b - 1]. And this is exactly
+ // what we do next.
+ //
+ // If we are dealing with unsigned case, we shouldn't move the lower bound.
+ if (Min.isSigned()) {
+ ++Min;
+ }
+ --Max;
+
+ bool IsLHSPositiveOrZero = LHS.From() >= Zero;
+ bool IsRHSPositiveOrZero = RHS.From() >= Zero;
+
+ // Remainder operator results with negative operands is implementation
+ // defined. Positive cases are much easier to reason about though.
+ if (IsLHSPositiveOrZero && IsRHSPositiveOrZero) {
+ // If maximal value of LHS is less than maximal value of RHS,
+ // the result won't get greater than LHS.To().
+ Max = std::min(LHS.To(), Max);
+ // We want to check if it is a situation similar to the following:
+ //
+ // <------------|---[ LHS ]--------[ RHS ]----->
+ // -INF 0 +INF
+ //
+ // In this situation, we can conclude that (LHS / RHS) == 0 and
+ // (LHS % RHS) == LHS.
+ Min = LHS.To() < RHS.From() ? LHS.From() : Zero;
+ }
+
+ // Nevertheless, the symmetrical range for RHS is a conservative estimate
+ // for any sign of either LHS, or RHS.
+ return {RangeFactory, ValueFactory.getValue(Min), ValueFactory.getValue(Max)};
+}
+
class RangeConstraintManager : public RangedConstraintManager {
public:
RangeConstraintManager(ExprEngine *EE, SValBuilder &SVB)
diff --git a/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp b/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
index d9fe3af3c000..2e269f6a596e 100644
--- a/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ b/clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -652,6 +652,11 @@ SVal SimpleSValBuilder::evalBinOpNN(ProgramStateRef state,
if (LHSValue == 0)
return evalCastFromNonLoc(lhs, resultTy);
return makeSymExprValNN(op, InputLHS, InputRHS, resultTy);
+ case BO_Rem:
+ // 0 % x == 0
+ if (LHSValue == 0)
+ return makeZeroVal(resultTy);
+ LLVM_FALLTHROUGH;
default:
return makeSymExprValNN(op, InputLHS, InputRHS, resultTy);
}
diff --git a/clang/test/Analysis/PR35418.cpp b/clang/test/Analysis/PR35418.cpp
new file mode 100644
index 000000000000..658da72f1462
--- /dev/null
+++ b/clang/test/Analysis/PR35418.cpp
@@ -0,0 +1,28 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core -verify %s
+
+// expected-no-diagnostics
+
+void halt() __attribute__((__noreturn__));
+void assert(int b) {
+ if (!b)
+ halt();
+}
+
+void decode(unsigned width) {
+ assert(width > 0);
+
+ int base;
+ bool inited = false;
+
+ int i = 0;
+
+ if (i % width == 0) {
+ base = 512;
+ inited = true;
+ }
+
+ base += 1; // no-warning
+
+ if (base >> 10)
+ assert(false);
+}
diff --git a/clang/test/Analysis/constant-folding.c b/clang/test/Analysis/constant-folding.c
index b3320cc53636..08a7accfba64 100644
--- a/clang/test/Analysis/constant-folding.c
+++ b/clang/test/Analysis/constant-folding.c
@@ -1,5 +1,9 @@
// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify -analyzer-config eagerly-assume=false %s
+#define UINT_MAX (~0U)
+#define INT_MAX (int)(UINT_MAX & (UINT_MAX >> 1))
+#define INT_MIN (int)(UINT_MAX & ~(UINT_MAX >> 1))
+
void clang_analyzer_eval(int);
// There should be no warnings unless otherwise indicated.
@@ -174,3 +178,76 @@ void testBitwiseRules(unsigned int a, int b, int c) {
clang_analyzer_eval((a & 1) <= 1); // expected-warning{{TRUE}}
}
}
+
+void testRemainderRules(unsigned int a, unsigned int b, int c, int d) {
+ // Check that we know that remainder of zero divided by any number is still 0.
+ clang_analyzer_eval((0 % c) == 0); // expected-warning{{TRUE}}
+
+ clang_analyzer_eval((10 % a) <= 10); // expected-warning{{TRUE}}
+
+ if (a <= 30 && b <= 50) {
+ clang_analyzer_eval((40 % a) < 30); // expected-warning{{TRUE}}
+ clang_analyzer_eval((a % b) < 50); // expected-warning{{TRUE}}
+ clang_analyzer_eval((b % a) < 30); // expected-warning{{TRUE}}
+
+ if (a >= 10) {
+ // Even though it seems like a valid assumption, it is not.
+ // Check that we are not making this mistake.
+ clang_analyzer_eval((a % b) >= 10); // expected-warning{{UNKNOWN}}
+
+ // Check that we can we can infer when remainder is equal
+ // to the dividend.
+ clang_analyzer_eval((4 % a) == 4); // expected-warning{{TRUE}}
+ if (b < 7) {
+ clang_analyzer_eval((b % a) < 7); // expected-warning{{TRUE}}
+ }
+ }
+ }
+
+ if (c > -10) {
+ clang_analyzer_eval((d % c) < INT_MAX); // expected-warning{{TRUE}}
+ clang_analyzer_eval((d % c) > INT_MIN + 1); // expected-warning{{TRUE}}
+ }
+
+ // Check that we can reason about signed integers when they are
+ // known to be positive.
+ if (c >= 10 && c <= 30 && d >= 20 && d <= 50) {
+ clang_analyzer_eval((5 % c) == 5); // expected-warning{{TRUE}}
+ clang_analyzer_eval((c % d) <= 30); // expected-warning{{TRUE}}
+ clang_analyzer_eval((c % d) >= 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval((d % c) < 30); // expected-warning{{TRUE}}
+ clang_analyzer_eval((d % c) >= 0); // expected-warning{{TRUE}}
+ }
+
+ if (c >= -30 && c <= -10 && d >= -20 && d <= 50) {
+ // Test positive LHS with negative RHS.
+ clang_analyzer_eval((40 % c) < 30); // expected-warning{{TRUE}}
+ clang_analyzer_eval((40 % c) > -30); // expected-warning{{TRUE}}
+
+ // Test negative LHS with possibly negative RHS.
+ clang_analyzer_eval((-10 % d) < 50); // expected-warning{{TRUE}}
+ clang_analyzer_eval((-20 % d) > -50); // expected-warning{{TRUE}}
+
+ // Check that we don't make wrong assumptions
+ clang_analyzer_eval((-20 % d) > -20); // expected-warning{{UNKNOWN}}
+
+ // Check that we can reason about negative ranges...
+ clang_analyzer_eval((c % d) < 50); // expected-warning{{TRUE}}
+ /// ...both ways
+ clang_analyzer_eval((d % c) < 30); // expected-warning{{TRUE}}
+
+ if (a <= 10) {
+ // Result is unsigned. This means that 'c' is casted to unsigned.
+ // We don't want to reason about ranges changing boundaries with
+ // conversions.
+ clang_analyzer_eval((a % c) < 30); // expected-warning{{UNKNOWN}}
+ }
+ }
+
+ // Check that we work correctly when minimal unsigned value from a range is
+ // equal to the signed minimum for the same bit width.
+ unsigned int x = INT_MIN;
+ if (a >= x && a <= x + 10) {
+ clang_analyzer_eval((b % a) < x + 10); // expected-warning{{TRUE}}
+ }
+}
diff --git a/clang/test/Analysis/hangs.c b/clang/test/Analysis/hangs.c
index b109bcb52fdb..ce719a16d6c4 100644
--- a/clang/test/Analysis/hangs.c
+++ b/clang/test/Analysis/hangs.c
@@ -1,9 +1,16 @@
-// RUN: %clang_analyze_cc1 -analyzer-checker core -verify %s
-
-// expected-no-diagnostics
+// RUN: %clang_analyze_cc1 -verify %s \
+// RUN: -analyzer-checker core,debug.ExprInspection
// Stuff that used to hang.
+extern void __assert_fail(__const char *__assertion, __const char *__file,
+ unsigned int __line, __const char *__function)
+ __attribute__((__noreturn__));
+#define assert(expr) \
+ ((expr) ? (void)(0) : __assert_fail(#expr, __FILE__, __LINE__, __func__))
+
+void clang_analyzer_eval(int);
+
int g();
int f(int y) {
@@ -28,3 +35,186 @@ void produce_an_exponentially_exploding_symbol(int x, int y) {
x += y; y += x + g();
x += y; y += x + g();
}
+
+void produce_an_exponentially_exploding_symbol_2(int x, int y) {
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ if (x > 1) {
+ if (x > 2) {
+ if (x > 3) {
+ if (x > 4) {
+ if (x > 5) {
+ if (x > 6) {
+ if (x > 7) {
+ if (x > 8) {
+ if (x > 9) {
+ if (x > 10) {
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+}
+
+void produce_an_exponentially_exploding_symbol_3(int x, int y) {
+ assert(0 < x && x < 10);
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ x &= y;
+ y &= x & g();
+ clang_analyzer_eval(0 < x && x < 10); // expected-warning{{TRUE}}
+ // expected-warning at -1{{FALSE}}
+}
diff --git a/clang/test/Analysis/uninit-bug-first-iteration-init.c b/clang/test/Analysis/uninit-bug-first-iteration-init.c
new file mode 100644
index 000000000000..a0fae2950fed
--- /dev/null
+++ b/clang/test/Analysis/uninit-bug-first-iteration-init.c
@@ -0,0 +1,27 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core -verify %s
+
+// rdar://problem/44978988
+// expected-no-diagnostics
+
+int foo();
+
+int gTotal;
+
+double bar(int start, int end) {
+ int i, cnt, processed, size;
+ double result, inc;
+
+ result = 0;
+ processed = start;
+ size = gTotal * 2;
+ cnt = (end - start + 1) * size;
+
+ for (i = 0; i < cnt; i += 2) {
+ if ((i % size) == 0) {
+ inc = foo();
+ processed++;
+ }
+ result += inc * inc; // no-warning
+ }
+ return result;
+}
More information about the cfe-commits
mailing list