[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
This revision was automatically updated to reflect the committed changes.
Closed by commit rC335814: [Analyzer] Constraint Manager Negates Difference
(authored by baloghadamsoftware, committed by ).
Repository:
rC Clang
https://reviews.llvm.org/D35110
Files:
include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
test/Analysis/constraint_manager_negate_difference.c
test/Analysis/ptr-arith.c
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -174,6 +174,38 @@
return newRanges;
}
+// Turn all [A, B] ranges to [-B, -A]. Ranges [MIN, B] are turned to range set
+// [MIN, MIN] U [-B, MAX], when MIN and MAX are the minimal and the maximal
+// signed values of the type.
+RangeSet RangeSet::Negate(BasicValueFactory &BV, Factory &F) const {
+ PrimRangeSet newRanges = F.getEmptySet();
+
+ for (iterator i = begin(), e = end(); i != e; ++i) {
+const llvm::APSInt &from = i->From(), &to = i->To();
+const llvm::APSInt &newTo = (from.isMinSignedValue() ?
+ BV.getMaxValue(from) :
+ BV.getValue(- from));
+if (to.isMaxSignedValue() && !newRanges.isEmpty() &&
+newRanges.begin()->From().isMinSignedValue()) {
+ assert(newRanges.begin()->To().isMinSignedValue() &&
+ "Ranges should not overlap");
+ assert(!from.isMinSignedValue() && "Ranges should not overlap");
+ const llvm::APSInt &newFrom = newRanges.begin()->From();
+ newRanges =
+F.add(F.remove(newRanges, *newRanges.begin()), Range(newFrom, newTo));
+} else if (!to.isMinSignedValue()) {
+ const llvm::APSInt &newFrom = BV.getValue(- to);
+ newRanges = F.add(newRanges, Range(newFrom, newTo));
+}
+if (from.isMinSignedValue()) {
+ newRanges = F.add(newRanges, Range(BV.getMinValue(from),
+ BV.getMinValue(from)));
+}
+ }
+
+ return newRanges;
+}
+
void RangeSet::print(raw_ostream &os) const {
bool isFirst = true;
os << "{ ";
@@ -252,6 +284,8 @@
RangeSet::Factory F;
RangeSet getRange(ProgramStateRef State, SymbolRef Sym);
+ const RangeSet* getRangeForMinusSymbol(ProgramStateRef State,
+ SymbolRef Sym);
RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym,
const llvm::APSInt &Int,
@@ -268,6 +302,7 @@
RangeSet getSymGERange(ProgramStateRef St, SymbolRef Sym,
const llvm::APSInt &Int,
const llvm::APSInt &Adjustment);
+
};
} // end anonymous namespace
@@ -423,9 +458,15 @@
if (ConstraintRangeTy::data_type *V = State->get(Sym))
return *V;
+ BasicValueFactory &BV = getBasicVals();
+
+ // If Sym is a difference of symbols A - B, then maybe we have range set
+ // stored for B - A.
+ if (const RangeSet *R = getRangeForMinusSymbol(State, Sym))
+return R->Negate(BV, F);
+
// Lazily generate a new RangeSet representing all possible values for the
// given symbol type.
- BasicValueFactory &BV = getBasicVals();
QualType T = Sym->getType();
RangeSet Result(F, BV.getMinValue(T), BV.getMaxValue(T));
@@ -441,6 +482,32 @@
return Result;
}
+// FIXME: Once SValBuilder supports unary minus, we should use SValBuilder to
+//obtain the negated symbolic expression instead of constructing the
+//symbol manually. This will allow us to support finding ranges of not
+//only negated SymSymExpr-type expressions, but also of other, simpler
+//expressions which we currently do not know how to negate.
+const RangeSet*
+RangeConstraintManager::getRangeForMinusSymbol(ProgramStateRef State,
+ SymbolRef Sym) {
+ if (const SymSymExpr *SSE = dyn_cast(Sym)) {
+if (SSE->getOpcode() == BO_Sub) {
+ QualType T = Sym->getType();
+ SymbolManager &SymMgr = State->getSymbolManager();
+ SymbolRef negSym = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub,
+ SSE->getLHS(), T);
+ if (const RangeSet *negV = State->get(negSym)) {
+// Unsigned range set cannot be negated, unless it is [0, 0].
+if ((negV->getConcreteValue() &&
+ (*negV->getConcreteValue() == 0)) ||
+T->isSignedIntegerOrEnumerationType())
+ return negV;
+ }
+}
+ }
+ return nullptr;
+}
+
//======
// assumeSymX methods: protected interface for RangeConstraintManager.
//======/
Index: include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
==
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
NoQ accepted this revision.
NoQ added a comment.
This revision is now accepted and ready to land.
Thank you!! Please commit.
Comment at: test/Analysis/constraint_manager_negate_difference.c:95
+void negate_mixed(int m, int n) {
+ if (m -n > INT_MIN && m - n <= 0)
+return;
Whitespace (:
https://reviews.llvm.org/D35110
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware updated this revision to Diff 152752.
baloghadamsoftware added a comment.
Comment fixed, assertions inserted, new tests added.
https://reviews.llvm.org/D35110
Files:
include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
test/Analysis/constraint_manager_negate_difference.c
test/Analysis/ptr-arith.c
Index: test/Analysis/ptr-arith.c
===
--- test/Analysis/ptr-arith.c
+++ test/Analysis/ptr-arith.c
@@ -265,49 +265,26 @@
clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{TRUE}}
}
-//---
-// False positives
-//---
-
void zero_implies_reversed_equal(int *lhs, int *rhs) {
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{UNKNOWN}}
if ((rhs - lhs) == 0) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs != lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{FALSE}}
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs != lhs); // expected-warning{{TRUE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
- clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void canonical_equal(int *lhs, int *rhs) {
clang_analyzer_eval(lhs == rhs); // expected-warning{{UNKNOWN}}
if (lhs == rhs) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
-
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void compare_element_region_and_base(int *p) {
Index: test/Analysis/constraint_manager_negate_difference.c
===
--- /dev/null
+++ test/Analysis/constraint_manager_negate_difference.c
@@ -0,0 +1,98 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-relational-comparison-simplification=true -verify %s
+
+void clang_analyzer_eval(int);
+
+void exit(int);
+
+#define UINT_MAX (~0U)
+#define INT_MAX (UINT_MAX & (UINT_MAX >> 1))
+#define INT_MIN (UINT_MAX & ~(UINT_MAX >> 1))
+
+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 assert_in_range(int x) {
+ assert(x <= ((int)INT_MAX / 4));
+ assert(x >= -(((int)INT_MAX) / 4));
+}
+
+void assert_in_wide_range(int x) {
+ assert(x <= ((int)INT_MAX / 2));
+ assert(x >= -(((int)INT_MAX) / 2));
+}
+
+void assert_in_range_2(int m, int n) {
+ assert_in_range(m);
+ assert_in_range(n);
+}
+
+void equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m != n)
+return;
+ assert_in_wide_range(m - n);
+ clang_analyzer_eval(n == m); // expected-warning{{TRUE}}
+}
+
+void non_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m == n)
+return;
+ assert_in_wide_range(m - n);
+ clang_analyzer_eval(n != m); // expected-warning{{TRUE}}
+}
+
+void less_or_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m < n)
+return;
+ assert_in_wide_range(m - n);
+ clang_analyzer_eval(n <= m); // expected-warning{{TRUE}}
+}
+
+void less(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m <= n)
+return;
+ assert_in_wide_range(m - n);
+ clang_analyzer_eval(n < m); // expected-warning{{TRUE}}
+}
+
+void greater_or_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m > n)
+return;
+ assert_in_wide_range(m - n);
+ clang_analyzer_eval(n >= m); // expected-warning{{TRUE}}
+}
+
+void greater(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m >= n)
+return;
+ assert_in_wide_range(m - n);
+ clang_analyzer_eval(n > m); // expected-warning{{TRUE}}
+}
+
+void negate_positive_range(int m, int n) {
+ if (m - n <= 0)
+return;
+ clang_analyzer_eval(n - m < 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(n - m > INT_MIN); // expected-warning{{TRUE}}
+ clang_analyzer_eval(n - m == INT_MIN); // expected-warning{{FALSE}}
+}
+
+void negate_int_min(int m, int n) {
+ if (m - n != INT_MIN)
+return;
+ clang_analyzer_eval(n - m == INT_MIN); // expected-warning{{TRUE}}
+}
+
+void negate_mixed(int m, int n) {
+ if (m -n > INT_MIN && m - n <= 0)
+return;
+ clang
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
NoQ added a comment.
Ok, code makes sense to me now!
I think we still need a few new tests to cover the corner cases.
In https://reviews.llvm.org/D35110#1135306, @baloghadamsoftware wrote:
> I added extra assertion into the test for the difference. Interestingly, it
> also works if I assert `n-m` is in the range instead of `m-n`. However, I
> wonder how can I apply such constraint to the difference of iterator
> positions without decomposing them to symbols and constants.
I don't see how iterator checker is different from the tests. The code of the
program in your tests doesn't decompose `m - n` into symbols and constants, it
simply subtracts an opaque value `n` (whatever it is) from an opaque value `m`
(whatever it is) and makes assumptions on the opaque result of the subtraction
(whatever it is). The checker should do the same, i guess?
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:177-178
+// Turn all [A, B] ranges to [-B, -A]. Turn minimal signed value to maximal
+// signed value.
+RangeSet RangeSet::Negate(BasicValueFactory &BV, Factory &F) const {
I guess the comment needs to be updated.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:189
+newRanges.begin()->From().isMinSignedValue()) {
+ const llvm::APSInt &newFrom = newRanges.begin()->From();
+ newRanges =
I suggest a few sanity checks here (untested):
`assert(newRanges.begin()->To().isMinSignedValue());` because we shouldn't ever
get an overlap.
`assert(!from.isMinSignedValue())` for the same reason; it's good to know
because it tells us what `newTo` is equal to on this path.
https://reviews.llvm.org/D35110
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added a comment. I tested all parts of the Iterator Checkers, all tests passed. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added a comment. I added extra assertion into the test for the difference. Interestingly, it also works if I assert `n-m` is in the range instead of `m-n`. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware updated this revision to Diff 151720.
baloghadamsoftware added a comment.
-(-2^n) == -2^n
https://reviews.llvm.org/D35110
Files:
include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
test/Analysis/constraint_manager_negate_difference.c
test/Analysis/ptr-arith.c
Index: test/Analysis/ptr-arith.c
===
--- test/Analysis/ptr-arith.c
+++ test/Analysis/ptr-arith.c
@@ -265,49 +265,26 @@
clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{TRUE}}
}
-//---
-// False positives
-//---
-
void zero_implies_reversed_equal(int *lhs, int *rhs) {
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{UNKNOWN}}
if ((rhs - lhs) == 0) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs != lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{FALSE}}
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs != lhs); // expected-warning{{TRUE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
- clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void canonical_equal(int *lhs, int *rhs) {
clang_analyzer_eval(lhs == rhs); // expected-warning{{UNKNOWN}}
if (lhs == rhs) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
-
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void compare_element_region_and_base(int *p) {
Index: test/Analysis/constraint_manager_negate_difference.c
===
--- /dev/null
+++ test/Analysis/constraint_manager_negate_difference.c
@@ -0,0 +1,77 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-relational-comparison-simplification=true -verify %s
+
+void clang_analyzer_eval(int);
+
+void exit(int);
+
+#define UINT_MAX (~0U)
+#define INT_MAX (UINT_MAX & (UINT_MAX >> 1))
+
+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 assert_in_range(int x) {
+ assert(x <= ((int)INT_MAX / 4));
+ assert(x >= -(((int)INT_MAX) / 4));
+}
+
+void assert_in_wide_range(int x) {
+ assert(x <= ((int)INT_MAX / 2));
+ assert(x >= -(((int)INT_MAX) / 2));
+}
+
+void assert_in_range_2(int m, int n) {
+ assert_in_range(m);
+ assert_in_range(n);
+}
+
+void equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m != n)
+return;
+ assert_in_wide_range(m - n);
+ clang_analyzer_eval(n == m); // expected-warning{{TRUE}}
+}
+
+void non_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m == n)
+return;
+ assert_in_wide_range(m - n);
+ clang_analyzer_eval(n != m); // expected-warning{{TRUE}}
+}
+
+void less_or_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m < n)
+return;
+ assert_in_wide_range(m - n);
+ clang_analyzer_eval(n <= m); // expected-warning{{TRUE}}
+}
+
+void less(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m <= n)
+return;
+ assert_in_wide_range(m - n);
+ clang_analyzer_eval(n < m); // expected-warning{{TRUE}}
+}
+
+void greater_or_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m > n)
+return;
+ assert_in_wide_range(m - n);
+ clang_analyzer_eval(n >= m); // expected-warning{{TRUE}}
+}
+
+void greater(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m >= n)
+return;
+ assert_in_wide_range(m - n);
+ clang_analyzer_eval(n > m); // expected-warning{{TRUE}}
+}
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -174,6 +174,34 @@
return newRanges;
}
+// Turn all [A, B] ranges to [-B, -A]. Turn minimal signed value to maximal
+// signed value.
+RangeSet RangeSet::Negate(BasicValueFactory &BV, Factory &F) const {
+ PrimRangeSet newRanges = F.getEmptySet();
+
+ for (iterator i = begin(), e = end(); i != e; ++i) {
+const llvm::APSInt &from = i->From(), &to = i->To();
+
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
NoQ added a comment. I still don't think i fully understand your concern? Could you provide an example and point out what exactly goes wrong? https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
NoQ added a comment. > In the iterator checkers we do not know anything about the rearranged > expressions, it has no access to the sum/difference, the whole purpose of > your proposal was to put in into the infrastructure. It wasn't. The purpose was merely to move (de-duplicate) the code that computes the sum/difference away from the checker. The checker can still operate on the result of such calculation if it knows something about that result that the core doesn't. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added a comment. Herald added a subscriber: mikhail.ramalho. Any idea how to proceed? https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added a comment. In https://reviews.llvm.org/D35110#1119496, @NoQ wrote: > Which expressions are constrained? Why does the difference use the whole > range? Is it something that could have been fixed by the "enforce that > separately" part in my old comment: > > > iterator-related symbols are all planned to be within range [-2²⁹, -2²⁹], > > right? So if we subtract one such symbol from another, it's going to be in > > range [-2³⁰, 2³⁰]. Can we currently infer that? Or maybe we should make the > > iterator checker to enforce that separately? > > ? `RangedConstraintManager` currently does not support `Sym+Sym`-type of expressions, only `Sym+Int`-type ones. That is why it cannot calculate that the result is within `[-2³⁰, 2³⁰]`. In the iterator checkers we do not know anything about the rearranged expressions, it has no access to the sum/difference, the whole purpose of your proposal was to put in into the infrastructure. The checker enforces everything it can but it does not help. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
NoQ added a comment. In https://reviews.llvm.org/D35110#1117401, @baloghadamsoftware wrote: > Sorry, Artem, but it does not work this way. Even if the symbolic expressions > are constrained to `[-MAX/4..MAX/4]`, after rearrangement the difference > still uses the whole range, thus `m>n` becomes `m-n>0`, where in the false > branch the range for `m-n` is `[MIN..0]`. Then if we check `n>=m` the range > set is reversed to `[MIN..MIN]U[0..MAX]` which results `UNKNOWN` for `n-m`. > It does not solve any of our problems and there is no remedy on the checker's > side. Which expressions are constrained? Why does the difference use the whole range? Is it something that could have been fixed by the "enforce that separately" part in my old comment: > iterator-related symbols are all planned to be within range [-2²⁹, -2²⁹], > right? So if we subtract one such symbol from another, it's going to be in > range [-2³⁰, 2³⁰]. Can we currently infer that? Or maybe we should make the > iterator checker to enforce that separately? ? https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added a comment. Maybe if we could apply somehow a `[-MAX/2..MAX/2]` constraint to both sides of the rearranged equality in SimpleSValBuilder. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added a comment. Sorry, Artem, but it does not work this way. Even if the symbolic expressions are constrained to `[-MAX/4..MAX/4]`, after rearrangement the difference still uses the whole range, thus `m>n` becomes `m-n>0`, where in the false branch the range for `m-n` is `[MIN..0]`. Then if we check `n>=m` the range set is reversed to `[MIN..MIN]U[0..MAX]` which results `UNKNOWN` for `n-m`. It does not solve any of our problems and there is no remedy on the checker's side. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
NoQ added inline comments.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:192
+if (from.isMinSignedValue()) {
+ F.add(newRanges, Range(BV.getMinValue(from), BV.getMinValue(from)));
+}
NoQ wrote:
> Return value of `add` seems to be accidentally discarded here.
>
> I guess i'll look into adding an `__attribute__((warn_unused_result))` to
> these functions, because it's a super common bug.
Also tests would have saved us.
https://reviews.llvm.org/D35110
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
NoQ added inline comments.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:191
+}
+if (from.isMinSignedValue()) {
+ F.add(newRanges, Range(BV.getMinValue(from), BV.getMinValue(from)));
We'll also need to merge the two adjacent segments if the original range had
both a [MinSingedValue, MinSignedValue] and a [X, MaxSignedValue]:
{F6287707}
Because our immutable sets are sorted, you can conduct the check for the first
and the last segment separately.
I think this code needs comments because even though it's short it's pretty
hard to get right.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:192
+if (from.isMinSignedValue()) {
+ F.add(newRanges, Range(BV.getMinValue(from), BV.getMinValue(from)));
+}
Return value of `add` seems to be accidentally discarded here.
I guess i'll look into adding an `__attribute__((warn_unused_result))` to these
functions, because it's a super common bug.
https://reviews.llvm.org/D35110
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware updated this revision to Diff 148804.
baloghadamsoftware added a comment.
I still disagree, but I want the review to continue so I did the requested
modifications.
https://reviews.llvm.org/D35110
Files:
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
lib/StaticAnalyzer/Core/RangedConstraintManager.h
test/Analysis/constraint_manager_negate_difference.c
test/Analysis/ptr-arith.c
Index: test/Analysis/ptr-arith.c
===
--- test/Analysis/ptr-arith.c
+++ test/Analysis/ptr-arith.c
@@ -265,49 +265,26 @@
clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{TRUE}}
}
-//---
-// False positives
-//---
-
void zero_implies_reversed_equal(int *lhs, int *rhs) {
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{UNKNOWN}}
if ((rhs - lhs) == 0) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs != lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{FALSE}}
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs != lhs); // expected-warning{{TRUE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
- clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void canonical_equal(int *lhs, int *rhs) {
clang_analyzer_eval(lhs == rhs); // expected-warning{{UNKNOWN}}
if (lhs == rhs) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
-
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void compare_element_region_and_base(int *p) {
Index: test/Analysis/constraint_manager_negate_difference.c
===
--- /dev/null
+++ test/Analysis/constraint_manager_negate_difference.c
@@ -0,0 +1,66 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-relational-comparison-simplification=true -verify %s
+
+void clang_analyzer_eval(int);
+
+void exit(int);
+
+#define UINT_MAX (~0U)
+#define INT_MAX (UINT_MAX & (UINT_MAX >> 1))
+
+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 assert_in_range(int x) {
+ assert(x <= ((int)INT_MAX / 4));
+ assert(x >= -(((int)INT_MAX) / 4));
+}
+
+void assert_in_range_2(int m, int n) {
+ assert_in_range(m);
+ assert_in_range(n);
+}
+
+void equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m != n)
+return;
+ clang_analyzer_eval(n == m); // expected-warning{{TRUE}}
+}
+
+void non_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m == n)
+return;
+ clang_analyzer_eval(n != m); // expected-warning{{TRUE}}
+}
+
+void less_or_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m < n)
+return;
+ clang_analyzer_eval(n <= m); // expected-warning{{TRUE}}
+}
+
+void less(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m <= n)
+return;
+ clang_analyzer_eval(n < m); // expected-warning{{TRUE}}
+}
+
+void greater_or_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m > n)
+return;
+ clang_analyzer_eval(n >= m); // expected-warning{{TRUE}}
+}
+
+void greater(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m >= n)
+return;
+ clang_analyzer_eval(n > m); // expected-warning{{TRUE}}
+}
Index: lib/StaticAnalyzer/Core/RangedConstraintManager.h
===
--- lib/StaticAnalyzer/Core/RangedConstraintManager.h
+++ lib/StaticAnalyzer/Core/RangedConstraintManager.h
@@ -115,6 +115,8 @@
RangeSet Intersect(BasicValueFactory &BV, Factory &F, llvm::APSInt Lower,
llvm::APSInt Upper) const;
+ RangeSet Negate(BasicValueFactory &BV, Factory &F) const;
+
void print(raw_ostream &os) const;
bool operator==(const RangeSet &other) const {
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -174,6 +174,28 @@
return newRanges;
}
+// Turn all [A, B] ranges to [-B, -A]. Turn minimal
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
NoQ added inline comments. Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:265-276 + const llvm::APSInt &from = i->From(), &to = i->To(); + const llvm::APSInt &newFrom = (to.isMinSignedValue() ? + BV.getMaxValue(to) : + (to.isMaxSignedValue() ? + BV.getMinValue(to) : + BV.getValue(- to))); + const llvm::APSInt &newTo = (from.isMinSignedValue() ? baloghadamsoftware wrote: > NoQ wrote: > > baloghadamsoftware wrote: > > > NoQ wrote: > > > > Hmm, wait a minute, is this actually correct? > > > > > > > > For the range [-2³¹, -2³¹ + 1] over a 32-bit integer, the negated range > > > > will be [-2³¹, -2³¹] U [2³¹ - 1, 2³¹ - 1]. > > > > > > > > So there must be a place in the code where we take one range and add > > > > two ranges. > > > The two ends of the range of the type usually stands for +/- infinity. If > > > we add the minimum of the type when negating a negative range, then we > > > lose the whole point of this transformation. > > > > > > Example: If `A - B < 0`, then the range of `A - B` is `[-2³¹, -1]`, If we > > > negate this, and keep the `-2³¹` range end, then we get `[-2³¹, -2³¹]U[1, > > > 2³¹-1]`. However, this does not mean `B - A > 0`. If we make assumption > > > about this, we get two states instead of one, in the true state `A - B`'s > > > range is `[1, 2³¹-1]` and in the false state it is `[-2³¹, -2³¹]`. This > > > is surely not what we want. > > Well, we can't turn math into something we want, it is what it is. > > > > Iterator-related symbols are all planned to be within range [-2²⁹, -2²⁹], > > right? So if we subtract one such symbol from another, it's going to be in > > range [-2³⁰, 2³⁰]. Can we currently infer that? Or maybe we should make the > > iterator checker to enforce that separately? Because this range doesn't > > include -2³¹, so we won't have any problems with doing negation correctly. > > > > So as usual i propose to get this code mathematically correct and then see > > if we can ensure correct behavior by enforcing reasonable constraints on > > our symbols. > I agree that the code should do mathematically correct things, but what I > argue here is what math here means. Computer science is based on math, but it > is somewhat different because of finite ranges and overflows. So I initially > regarded the minimal and maximal values as infinity. Maybe that is not > correct. However, I am sure that negating `-2³¹` should never be `-2³¹`. This > is mathematically incorrect, and renders the whole calculation useless, since > the union of a positive range and a negative range is unsuitable for any > reasoning. I see two options here: > > 1. Remove the extension when negating a range which ends at the maximal value > of the type. So the negated range begins at the minimal value plus one. > However, cut the range which begins at the minimal value of the type by one. > So the negated range ends at the maximal value, as in the current version in > the patch. > > 2. Remove the extension as in 1. and disable the whole negation if we have > the range begins at the minimal value. > > Iterator checkers are of course not affected because of the max/4 constraints. > However, I am sure that negating `-2³¹` should never be `-2³¹`. This is > mathematically incorrect, and renders the whole calculation useless, since > the union of a positive range and a negative range is unsuitable for any > reasoning. Well, that's how computers already work. And that's how all sorts of abstract algebra work as well, so this is totally mathematically correct. We promise to support the [[ https://en.wikipedia.org/wiki/Two's_complement | two's complement ]] semantics in the analyzer when it comes to signed integer overflows. Even though it's technically UB, most implementations follow this semantics and a lot of real-world applications explicitly rely on that. Also we cannot simply drop values from our constraint ranges in the general case because the values we drop might be the only valid values, and the assumption that at least one non-dropped value can definitely be taken is generally incorrect. Finding cornercases like this one is one of the strong sides of any static analysis: it is in fact our job to make the user aware of it if he doesn't understand overflow rules. If it cannot be said that the variable on a certain path is non-negative because it might as well be -2³¹, we should totally explore this possibility. If for a certain checker it brings no benefit because such value would be unlikely in certain circumstances, that checker is free to cut off the respective paths, but the core should perform operations precisely. I don't think we have much room for personal preferences here. https://reviews.llvm.org/D35110 ___
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added a comment. Can we continue the discussion here, please? We should involve Devin and/or George as well if we cannot agree ourselves. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware marked 2 inline comments as done. baloghadamsoftware added a comment. I chose option 1 for now. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware updated this revision to Diff 145187.
baloghadamsoftware added a comment.
Fixed according to the comments.
https://reviews.llvm.org/D35110
Files:
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
test/Analysis/constraint_manager_negate_difference.c
test/Analysis/ptr-arith.c
Index: test/Analysis/ptr-arith.c
===
--- test/Analysis/ptr-arith.c
+++ test/Analysis/ptr-arith.c
@@ -265,49 +265,26 @@
clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{TRUE}}
}
-//---
-// False positives
-//---
-
void zero_implies_reversed_equal(int *lhs, int *rhs) {
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{UNKNOWN}}
if ((rhs - lhs) == 0) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs != lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{FALSE}}
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs != lhs); // expected-warning{{TRUE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
- clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void canonical_equal(int *lhs, int *rhs) {
clang_analyzer_eval(lhs == rhs); // expected-warning{{UNKNOWN}}
if (lhs == rhs) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
-
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void compare_element_region_and_base(int *p) {
Index: test/Analysis/constraint_manager_negate_difference.c
===
--- /dev/null
+++ test/Analysis/constraint_manager_negate_difference.c
@@ -0,0 +1,66 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-relational-comparison-simplification=true -verify %s
+
+void clang_analyzer_eval(int);
+
+void exit(int);
+
+#define UINT_MAX (~0U)
+#define INT_MAX (UINT_MAX & (UINT_MAX >> 1))
+
+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 assert_in_range(int x) {
+ assert(x <= ((int)INT_MAX / 4));
+ assert(x >= -(((int)INT_MAX) / 4));
+}
+
+void assert_in_range_2(int m, int n) {
+ assert_in_range(m);
+ assert_in_range(n);
+}
+
+void equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m != n)
+return;
+ clang_analyzer_eval(n == m); // expected-warning{{TRUE}}
+}
+
+void non_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m == n)
+return;
+ clang_analyzer_eval(n != m); // expected-warning{{TRUE}}
+}
+
+void less_or_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m < n)
+return;
+ clang_analyzer_eval(n <= m); // expected-warning{{TRUE}}
+}
+
+void less(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m <= n)
+return;
+ clang_analyzer_eval(n < m); // expected-warning{{TRUE}}
+}
+
+void greater_or_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m > n)
+return;
+ clang_analyzer_eval(n >= m); // expected-warning{{TRUE}}
+}
+
+void greater(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m >= n)
+return;
+ clang_analyzer_eval(n > m); // expected-warning{{TRUE}}
+}
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -256,6 +256,25 @@
return newRanges;
}
+ // Turn all [A, B] ranges to [-B, -A]. Turn minimal signed value to maximal
+ // signed value.
+ RangeSet Negate(BasicValueFactory &BV, Factory &F) const {
+PrimRangeSet newRanges = F.getEmptySet();
+
+for (iterator i = begin(), e = end(); i != e; ++i) {
+ const llvm::APSInt &from = i->From(), &to = i->To();
+ const llvm::APSInt &newFrom = (to.isMinSignedValue() ?
+ BV.getMaxValue(to) :
+ BV.getValue(- to));
+ const llvm::APSInt &newTo = (from.isMinSignedValue() ?
+ BV.getMaxValue(from) :
+ BV.getValue(- from));
+
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added inline comments. Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:265-276 + const llvm::APSInt &from = i->From(), &to = i->To(); + const llvm::APSInt &newFrom = (to.isMinSignedValue() ? + BV.getMaxValue(to) : + (to.isMaxSignedValue() ? + BV.getMinValue(to) : + BV.getValue(- to))); + const llvm::APSInt &newTo = (from.isMinSignedValue() ? NoQ wrote: > baloghadamsoftware wrote: > > NoQ wrote: > > > Hmm, wait a minute, is this actually correct? > > > > > > For the range [-2³¹, -2³¹ + 1] over a 32-bit integer, the negated range > > > will be [-2³¹, -2³¹] U [2³¹ - 1, 2³¹ - 1]. > > > > > > So there must be a place in the code where we take one range and add two > > > ranges. > > The two ends of the range of the type usually stands for +/- infinity. If > > we add the minimum of the type when negating a negative range, then we lose > > the whole point of this transformation. > > > > Example: If `A - B < 0`, then the range of `A - B` is `[-2³¹, -1]`, If we > > negate this, and keep the `-2³¹` range end, then we get `[-2³¹, -2³¹]U[1, > > 2³¹-1]`. However, this does not mean `B - A > 0`. If we make assumption > > about this, we get two states instead of one, in the true state `A - B`'s > > range is `[1, 2³¹-1]` and in the false state it is `[-2³¹, -2³¹]`. This is > > surely not what we want. > Well, we can't turn math into something we want, it is what it is. > > Iterator-related symbols are all planned to be within range [-2²⁹, -2²⁹], > right? So if we subtract one such symbol from another, it's going to be in > range [-2³⁰, 2³⁰]. Can we currently infer that? Or maybe we should make the > iterator checker to enforce that separately? Because this range doesn't > include -2³¹, so we won't have any problems with doing negation correctly. > > So as usual i propose to get this code mathematically correct and then see if > we can ensure correct behavior by enforcing reasonable constraints on our > symbols. I agree that the code should do mathematically correct things, but what I argue here is what math here means. Computer science is based on math, but it is somewhat different because of finite ranges and overflows. So I initially regarded the minimal and maximal values as infinity. Maybe that is not correct. However, I am sure that negating `-2³¹` should never be `-2³¹`. This is mathematically incorrect, and renders the whole calculation useless, since the union of a positive range and a negative range is unsuitable for any reasoning. I see two options here: 1. Remove the extension when negating a range which ends at the maximal value of the type. So the negated range begins at the minimal value plus one. However, cut the range which begins at the minimal value of the type by one. So the negated range ends at the maximal value, as in the current version in the patch. 2. Remove the extension as in 1. and disable the whole negation if we have the range begins at the minimal value. Iterator checkers are of course not affected because of the max/4 constraints. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
NoQ added inline comments. Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:265-276 + const llvm::APSInt &from = i->From(), &to = i->To(); + const llvm::APSInt &newFrom = (to.isMinSignedValue() ? + BV.getMaxValue(to) : + (to.isMaxSignedValue() ? + BV.getMinValue(to) : + BV.getValue(- to))); + const llvm::APSInt &newTo = (from.isMinSignedValue() ? baloghadamsoftware wrote: > NoQ wrote: > > Hmm, wait a minute, is this actually correct? > > > > For the range [-2³¹, -2³¹ + 1] over a 32-bit integer, the negated range > > will be [-2³¹, -2³¹] U [2³¹ - 1, 2³¹ - 1]. > > > > So there must be a place in the code where we take one range and add two > > ranges. > The two ends of the range of the type usually stands for +/- infinity. If we > add the minimum of the type when negating a negative range, then we lose the > whole point of this transformation. > > Example: If `A - B < 0`, then the range of `A - B` is `[-2³¹, -1]`, If we > negate this, and keep the `-2³¹` range end, then we get `[-2³¹, -2³¹]U[1, > 2³¹-1]`. However, this does not mean `B - A > 0`. If we make assumption about > this, we get two states instead of one, in the true state `A - B`'s range is > `[1, 2³¹-1]` and in the false state it is `[-2³¹, -2³¹]`. This is surely not > what we want. Well, we can't turn math into something we want, it is what it is. Iterator-related symbols are all planned to be within range [-2²⁹, -2²⁹], right? So if we subtract one such symbol from another, it's going to be in range [-2³⁰, 2³⁰]. Can we currently infer that? Or maybe we should make the iterator checker to enforce that separately? Because this range doesn't include -2³¹, so we won't have any problems with doing negation correctly. So as usual i propose to get this code mathematically correct and then see if we can ensure correct behavior by enforcing reasonable constraints on our symbols. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added inline comments. Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:265-276 + const llvm::APSInt &from = i->From(), &to = i->To(); + const llvm::APSInt &newFrom = (to.isMinSignedValue() ? + BV.getMaxValue(to) : + (to.isMaxSignedValue() ? + BV.getMinValue(to) : + BV.getValue(- to))); + const llvm::APSInt &newTo = (from.isMinSignedValue() ? NoQ wrote: > Hmm, wait a minute, is this actually correct? > > For the range [-2³¹, -2³¹ + 1] over a 32-bit integer, the negated range will > be [-2³¹, -2³¹] U [2³¹ - 1, 2³¹ - 1]. > > So there must be a place in the code where we take one range and add two > ranges. The two ends of the range of the type usually stands for +/- infinity. If we add the minimum of the type when negating a negative range, then we lose the whole point of this transformation. Example: If `A - B < 0`, then the range of `A - B` is `[-2³¹, -1]`, If we negate this, and keep the `-2³¹` range end, then we get `[-2³¹, -2³¹]U[1, 2³¹-1]`. However, this does not mean `B - A > 0`. If we make assumption about this, we get two states instead of one, in the true state `A - B`'s range is `[1, 2³¹-1]` and in the false state it is `[-2³¹, -2³¹]`. This is surely not what we want. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
NoQ added inline comments. Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:265-276 + const llvm::APSInt &from = i->From(), &to = i->To(); + const llvm::APSInt &newFrom = (to.isMinSignedValue() ? + BV.getMaxValue(to) : + (to.isMaxSignedValue() ? + BV.getMinValue(to) : + BV.getValue(- to))); + const llvm::APSInt &newTo = (from.isMinSignedValue() ? Hmm, wait a minute, is this actually correct? For the range [-2³¹, -2³¹ + 1] over a 32-bit integer, the negated range will be [-2³¹, -2³¹] U [2³¹ - 1, 2³¹ - 1]. So there must be a place in the code where we take one range and add two ranges. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
NoQ added a comment.
LGTM! Minor nitpicking in comments.
Currently there's no such problem, but as `GetRange` becomes more complicated,
we'll really miss the possibility of saying something like "if there's a range
for negated symbol, `return GetRange(the negated symbol)`", so that all other
special cases applied. We could have allowed that by canonicalizing symbols
(i.e. announce that `$A` always goes before `$B` and therefore we will store a
range for `$A - $B` even if we're told to store the range for `$B - $A`) and
then the "if" will become "if the symbol is not canonical, `return GetRange(the
canonicalized symbol)`".
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:546
+ if (const SymSymExpr *SSE = dyn_cast(Sym)) {
+// FIXME: Once SValBuilder supports unary minus, we should use SValBuilder
Can we move the whole `if` into a function?
Eg.,
```
if (RangeSet *R = getRangeForMinusSymbol(Sym))
return R->Negate(BV, F)
```
?
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:557
+ SSE->getLHS(), T);
+ if (ConstraintRangeTy::data_type *negV =
+ State->get(negSym)) {
`ConstraintRangeTy::data_type` ~> `RangeSet` should be easier to read.
https://reviews.llvm.org/D35110
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added a comment. No more pending dependency, so we can continue the review. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware updated this revision to Diff 141955.
baloghadamsoftware added a comment.
Herald added a reviewer: george.karpenkov.
Rebased to the newly committed SValbuilder rearranger patch
https://reviews.llvm.org/D35110
Files:
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
test/Analysis/constraint_manager_negate_difference.c
test/Analysis/ptr-arith.c
Index: test/Analysis/ptr-arith.c
===
--- test/Analysis/ptr-arith.c
+++ test/Analysis/ptr-arith.c
@@ -265,49 +265,26 @@
clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{TRUE}}
}
-//---
-// False positives
-//---
-
void zero_implies_reversed_equal(int *lhs, int *rhs) {
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{UNKNOWN}}
if ((rhs - lhs) == 0) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs != lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{FALSE}}
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs != lhs); // expected-warning{{TRUE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
- clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void canonical_equal(int *lhs, int *rhs) {
clang_analyzer_eval(lhs == rhs); // expected-warning{{UNKNOWN}}
if (lhs == rhs) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
-
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void compare_element_region_and_base(int *p) {
Index: test/Analysis/constraint_manager_negate_difference.c
===
--- /dev/null
+++ test/Analysis/constraint_manager_negate_difference.c
@@ -0,0 +1,66 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-relational-comparison-simplification=true -verify %s
+
+void clang_analyzer_eval(int);
+
+void exit(int);
+
+#define UINT_MAX (~0U)
+#define INT_MAX (UINT_MAX & (UINT_MAX >> 1))
+
+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 assert_in_range(int x) {
+ assert(x <= ((int)INT_MAX / 4));
+ assert(x >= -(((int)INT_MAX) / 4));
+}
+
+void assert_in_range_2(int m, int n) {
+ assert_in_range(m);
+ assert_in_range(n);
+}
+
+void equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m != n)
+return;
+ clang_analyzer_eval(n == m); // expected-warning{{TRUE}}
+}
+
+void non_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m == n)
+return;
+ clang_analyzer_eval(n != m); // expected-warning{{TRUE}}
+}
+
+void less_or_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m < n)
+return;
+ clang_analyzer_eval(n <= m); // expected-warning{{TRUE}}
+}
+
+void less(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m <= n)
+return;
+ clang_analyzer_eval(n < m); // expected-warning{{TRUE}}
+}
+
+void greater_or_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m > n)
+return;
+ clang_analyzer_eval(n >= m); // expected-warning{{TRUE}}
+}
+
+void greater(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m >= n)
+return;
+ clang_analyzer_eval(n > m); // expected-warning{{TRUE}}
+}
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -256,6 +256,29 @@
return newRanges;
}
+ // Turn all [A, B] ranges to [-B, -A]. Turn minimal signed value to maximal
+ // signed value and vice versa.
+ RangeSet Negate(BasicValueFactory &BV, Factory &F) const {
+PrimRangeSet newRanges = F.getEmptySet();
+
+for (iterator i = begin(), e = end(); i != e; ++i) {
+ const llvm::APSInt &from = i->From(), &to = i->To();
+ const llvm::APSInt &newFrom = (to.isMinSignedValue() ?
+ BV.getMaxValue(to) :
+ (to.isMaxSignedValue() ?
+ BV.getMinValue(to) :
+
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware updated this revision to Diff 129441.
baloghadamsoftware added a comment.
Updated to be based upon https://reviews.llvm.org/D41938.
https://reviews.llvm.org/D35110
Files:
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
test/Analysis/constraint_manager_negate_difference.c
test/Analysis/ptr-arith.c
Index: test/Analysis/ptr-arith.c
===
--- test/Analysis/ptr-arith.c
+++ test/Analysis/ptr-arith.c
@@ -265,49 +265,26 @@
clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{TRUE}}
}
-//---
-// False positives
-//---
-
void zero_implies_reversed_equal(int *lhs, int *rhs) {
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{UNKNOWN}}
if ((rhs - lhs) == 0) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs != lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{FALSE}}
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs != lhs); // expected-warning{{TRUE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
- clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void canonical_equal(int *lhs, int *rhs) {
clang_analyzer_eval(lhs == rhs); // expected-warning{{UNKNOWN}}
if (lhs == rhs) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
-
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void compare_element_region_and_base(int *p) {
Index: test/Analysis/constraint_manager_negate_difference.c
===
--- /dev/null
+++ test/Analysis/constraint_manager_negate_difference.c
@@ -0,0 +1,64 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-relational-comparison-simplification=true -verify %s
+
+void clang_analyzer_eval(int);
+
+void exit(int);
+
+#define UINT_MAX (~0U)
+#define INT_MAX (UINT_MAX & (UINT_MAX >> 1))
+
+void assert_in_range(int x) {
+ // Assert that no overflows occur in this test file.
+ // Assuming that concrete integers are also within that range.
+ if (x > ((int)INT_MAX / 4))
+exit(1);
+ if (x < -(((int)INT_MAX) / 4))
+exit(1);
+}
+
+void assert_in_range_2(int m, int n) {
+ assert_in_range(m);
+ assert_in_range(n);
+}
+
+void equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m != n)
+return;
+ clang_analyzer_eval(n == m); // expected-warning{{TRUE}}
+}
+
+void non_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m == n)
+return;
+ clang_analyzer_eval(n != m); // expected-warning{{TRUE}}
+}
+
+void less_or_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m < n)
+return;
+ clang_analyzer_eval(n <= m); // expected-warning{{TRUE}}
+}
+
+void less(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m <= n)
+return;
+ clang_analyzer_eval(n < m); // expected-warning{{TRUE}}
+}
+
+void greater_or_equal(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m > n)
+return;
+ clang_analyzer_eval(n >= m); // expected-warning{{TRUE}}
+}
+
+void greater(int m, int n) {
+ assert_in_range_2(m, n);
+ if (m >= n)
+return;
+ clang_analyzer_eval(n > m); // expected-warning{{TRUE}}
+}
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -256,6 +256,29 @@
return newRanges;
}
+ // Turn all [A, B] ranges to [-B, -A]. Turn minimal signed value to maximal
+ // signed value and vice versa.
+ RangeSet Negate(BasicValueFactory &BV, Factory &F) const {
+PrimRangeSet newRanges = F.getEmptySet();
+
+for (iterator i = begin(), e = end(); i != e; ++i) {
+ const llvm::APSInt &from = i->From(), &to = i->To();
+ const llvm::APSInt &newFrom = (to.isMinSignedValue() ?
+ BV.getMaxValue(to) :
+ (to.isMaxSignedValue() ?
+ BV.getMinValue(to) :
+ BV.getValue(- to)));
+ const llvm::APSInt &newTo = (from.isMinSignedValue() ?
+ BV.getMaxValue(from) :
+
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added a comment. In https://reviews.llvm.org/D35110#972430, @NoQ wrote: > In https://reviews.llvm.org/D35110#969782, @baloghadamsoftware wrote: > > > Strange, but modifying the tests from `m n` to `m - n > > 0` does not help. The statement `if (m - n 0)` does not store a > > range for `m - n` in the constraint manager. With the other patch which > > automatically changes `m n` to `m - n 0` the range is > > stored automatically. > > > I guess we can easily assume how a `SymIntExpr` relates to a number by > storing a range on the opaque left-hand-side symbol, no matter how > complicated it is, but we cannot assume how a symbol relates to a symbol > (there's no obvious range to store). That's just how `assumeSym` currently > works. Actually it happens because `m - n` evaluates to `Unknown`. The code part responsible for this is the beginning of `SValBuilder::makeSymExprValNN()`, which prevents `m - n`-like symbolic expression unless one of `m` or `n` is `Tainted`. Anna added this part 5-6 years ago because some kind of bug, but it seems that it still exists. If I try to remove it then one test executes for days (with loop max count 63 or 64) and two tests fail with an assert. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
NoQ added a comment. In https://reviews.llvm.org/D35110#969782, @baloghadamsoftware wrote: > Strange, but modifying the tests from `m n` to `m - n > 0` does not help. The statement `if (m - n 0)` does not store a > range for `m - n` in the constraint manager. With the other patch which > automatically changes `m n` to `m - n 0` the range is > stored automatically. I guess we can easily assume how a `SymIntExpr` relates to a number by storing a range on the opaque left-hand-side symbol, no matter how complicated it is, but we cannot assume how a symbol relates to a symbol (there's no obvious range to store). That's just how `assumeSym` currently works. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added a comment. Strange, but modifying the tests from `m n` to `m - n 0` does not help. The statement `if (m - n 0)` does not store a range for `m - n` in the constraint manager. With the other patch which automatically changes `m n` to `m - n 0` the range is stored automatically. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added a comment. In https://reviews.llvm.org/D35110#968284, @baloghadamsoftware wrote: > This one is not blocked anymore since I removed the dependency. But I have to modify the test cases... https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added a comment. Herald added subscribers: a.sidorin, rnkovacs, szepet. This one is not blocked anymore since I removed the dependency. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added a comment. In https://reviews.llvm.org/D35110#854334, @zaks.anna wrote: > Is this blocked on the same reasons as what was raised in > https://reviews.llvm.org/D35109? No, it is blocked because https://reviews.llvm.org/D35109 is a prerequisite. https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
zaks.anna added a comment. Is this blocked on the same reasons as what was raised in https://reviews.llvm.org/D35109? https://reviews.llvm.org/D35110 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware updated this revision to Diff 107079.
baloghadamsoftware added a comment.
I think I checked the type of the left side of the difference, not the
difference itself. Thus the difference is not a pointer type, it is a signed
integer type, the tests pass when I remove that line.
https://reviews.llvm.org/D35110
Files:
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
test/Analysis/constraint_manager_negate_difference.c
test/Analysis/ptr-arith.c
Index: test/Analysis/ptr-arith.c
===
--- test/Analysis/ptr-arith.c
+++ test/Analysis/ptr-arith.c
@@ -265,49 +265,26 @@
clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{TRUE}}
}
-//---
-// False positives
-//---
-
void zero_implies_reversed_equal(int *lhs, int *rhs) {
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{UNKNOWN}}
if ((rhs - lhs) == 0) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs != lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{FALSE}}
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs != lhs); // expected-warning{{TRUE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
- clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void canonical_equal(int *lhs, int *rhs) {
clang_analyzer_eval(lhs == rhs); // expected-warning{{UNKNOWN}}
if (lhs == rhs) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
-
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void compare_element_region_and_base(int *p) {
Index: test/Analysis/constraint_manager_negate_difference.c
===
--- /dev/null
+++ test/Analysis/constraint_manager_negate_difference.c
@@ -0,0 +1,39 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection -verify %s
+
+void clang_analyzer_eval(int);
+
+void equal(int m, int n) {
+ if (m != n)
+return;
+ clang_analyzer_eval(n == m); // expected-warning{{TRUE}}
+}
+
+void non_equal(int m, int n) {
+ if (m == n)
+return;
+ clang_analyzer_eval(n != m); // expected-warning{{TRUE}}
+}
+
+void less_or_equal(int m, int n) {
+ if (m < n)
+return;
+ clang_analyzer_eval(n <= m); // expected-warning{{TRUE}}
+}
+
+void less(int m, int n) {
+ if (m <= n)
+return;
+ clang_analyzer_eval(n < m); // expected-warning{{TRUE}}
+}
+
+void greater_or_equal(int m, int n) {
+ if (m > n)
+return;
+ clang_analyzer_eval(n >= m); // expected-warning{{TRUE}}
+}
+
+void greater(int m, int n) {
+ if (m >= n)
+return;
+ clang_analyzer_eval(n > m); // expected-warning{{TRUE}}
+}
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -256,6 +256,29 @@
return newRanges;
}
+ // Turn all [A, B] ranges to [-B, -A]. Turn minimal signed value to maximal
+ // signed value and vice versa.
+ RangeSet Negate(BasicValueFactory &BV, Factory &F) const {
+PrimRangeSet newRanges = F.getEmptySet();
+
+for (iterator i = begin(), e = end(); i != e; ++i) {
+ const llvm::APSInt &from = i->From(), &to = i->To();
+ const llvm::APSInt &newFrom = (to.isMinSignedValue() ?
+ BV.getMaxValue(to) :
+ (to.isMaxSignedValue() ?
+ BV.getMinValue(to) :
+ BV.getValue(- to)));
+ const llvm::APSInt &newTo = (from.isMinSignedValue() ?
+ BV.getMaxValue(from) :
+ (from.isMaxSignedValue() ?
+BV.getMinValue(from) :
+BV.getValue(- from)));
+ newRanges = F.add(newRanges, Range(newFrom, newTo));
+}
+
+return newRanges;
+ }
+
void print(raw_ostream &os) const {
bool isFirst = true;
os << "{ ";
@@ -465,11 +488,37 @@
if (ConstraintRangeTy::data_type *V = State->get(Sym))
return *V;
- // Lazily generate a new RangeSet representing all possible values for the
- // given symbol type.
+ //
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
NoQ added inline comments.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:511
+ SSE->getLHS()->getType()->isSignedIntegerOrEnumerationType() ||
+ SSE->getLHS()->getType()->isPointerType()) {
+ return negV->Negate(BV, F);
baloghadamsoftware wrote:
> NoQ wrote:
> > baloghadamsoftware wrote:
> > > NoQ wrote:
> > > > Pointer types are currently treated as unsigned, so i'm not sure you
> > > > want them here.
> > > For me it seems that pointer differences are still pointer types and they
> > > are signed. (The range becomes negative upon negative assumption. From
> > > test `ptr-arith.c`:
> > >
> > > ```
> > > void use_symbols(int *lhs, int *rhs) {
> > > clang_analyzer_eval(lhs < rhs); // expected-warning{{UNKNOWN}}
> > > if (lhs < rhs)
> > > return;
> > > clang_analyzer_eval(lhs < rhs); // expected-warning{{FALSE}}
> > >
> > > clang_analyzer_eval(lhs - rhs); // expected-warning{{UNKNOWN}}
> > > if ((lhs - rhs) != 5)
> > > return;
> > > clang_analyzer_eval((lhs - rhs) == 5); // expected-warning{{TRUE}}
> > > }
> > > ```
> > >
> > > If I put `clang_analyzer_printState()` into the empty line in the middle,
> > > I get the following range for the difference: `[-9223372036854775808,
> > > 0]`. If I replace `int*` with `unsigned`, this range becomes `[0, 0]`, so
> > > `int*` is handled as a signed type here.
> > Umm, yeah, i was wrong.
> >
> > *looks closer*
> >
> > `T` is the type of the difference, right? I don't think i'd expect pointer
> > type as the type of the difference.
> >
> > Could you add test cases for pointers if you intend to support them (and
> > maybe for unsigned types)?
> I do not know exactly the type, but if I remove the `T->isPointerType()`
> condition the test in `ptr_arith.c` will fail with `UNKNOWN`. So the type of
> the difference is a type that returns `true` from `T->isPointerType()`.
>
> Pointer tests are already there in `ptr_arith.c`. Should I duplicate them?
I don't see any failing tests when i remove `T->isPointerType()`.
Also this shouldn't be system-specific, because the target triple is hardcoded
in `ptr-arith.c` runline.
Could you point out which test is failing and dump the type in question
(`-ast-dump`, or `Type->dump()`, or `llvm::errs() << QualType::getAsString()`,
or whatever)?
https://reviews.llvm.org/D35110
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added inline comments.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:511
+ SSE->getLHS()->getType()->isSignedIntegerOrEnumerationType() ||
+ SSE->getLHS()->getType()->isPointerType()) {
+ return negV->Negate(BV, F);
NoQ wrote:
> baloghadamsoftware wrote:
> > NoQ wrote:
> > > Pointer types are currently treated as unsigned, so i'm not sure you want
> > > them here.
> > For me it seems that pointer differences are still pointer types and they
> > are signed. (The range becomes negative upon negative assumption. From test
> > `ptr-arith.c`:
> >
> > ```
> > void use_symbols(int *lhs, int *rhs) {
> > clang_analyzer_eval(lhs < rhs); // expected-warning{{UNKNOWN}}
> > if (lhs < rhs)
> > return;
> > clang_analyzer_eval(lhs < rhs); // expected-warning{{FALSE}}
> >
> > clang_analyzer_eval(lhs - rhs); // expected-warning{{UNKNOWN}}
> > if ((lhs - rhs) != 5)
> > return;
> > clang_analyzer_eval((lhs - rhs) == 5); // expected-warning{{TRUE}}
> > }
> > ```
> >
> > If I put `clang_analyzer_printState()` into the empty line in the middle, I
> > get the following range for the difference: `[-9223372036854775808, 0]`. If
> > I replace `int*` with `unsigned`, this range becomes `[0, 0]`, so `int*` is
> > handled as a signed type here.
> Umm, yeah, i was wrong.
>
> *looks closer*
>
> `T` is the type of the difference, right? I don't think i'd expect pointer
> type as the type of the difference.
>
> Could you add test cases for pointers if you intend to support them (and
> maybe for unsigned types)?
I do not know exactly the type, but if I remove the `T->isPointerType()`
condition the test in `ptr_arith.c` will fail with `UNKNOWN`. So the type of
the difference is a type that returns `true` from `T->isPointerType()`.
Pointer tests are already there in `ptr_arith.c`. Should I duplicate them?
https://reviews.llvm.org/D35110
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
NoQ added inline comments.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:511
+ SSE->getLHS()->getType()->isSignedIntegerOrEnumerationType() ||
+ SSE->getLHS()->getType()->isPointerType()) {
+ return negV->Negate(BV, F);
baloghadamsoftware wrote:
> NoQ wrote:
> > Pointer types are currently treated as unsigned, so i'm not sure you want
> > them here.
> For me it seems that pointer differences are still pointer types and they are
> signed. (The range becomes negative upon negative assumption. From test
> `ptr-arith.c`:
>
> ```
> void use_symbols(int *lhs, int *rhs) {
> clang_analyzer_eval(lhs < rhs); // expected-warning{{UNKNOWN}}
> if (lhs < rhs)
> return;
> clang_analyzer_eval(lhs < rhs); // expected-warning{{FALSE}}
>
> clang_analyzer_eval(lhs - rhs); // expected-warning{{UNKNOWN}}
> if ((lhs - rhs) != 5)
> return;
> clang_analyzer_eval((lhs - rhs) == 5); // expected-warning{{TRUE}}
> }
> ```
>
> If I put `clang_analyzer_printState()` into the empty line in the middle, I
> get the following range for the difference: `[-9223372036854775808, 0]`. If I
> replace `int*` with `unsigned`, this range becomes `[0, 0]`, so `int*` is
> handled as a signed type here.
Umm, yeah, i was wrong.
*looks closer*
`T` is the type of the difference, right? I don't think i'd expect pointer type
as the type of the difference.
Could you add test cases for pointers if you intend to support them (and maybe
for unsigned types)?
https://reviews.llvm.org/D35110
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware updated this revision to Diff 106627.
baloghadamsoftware added a comment.
Type selection simplified, FIXME added.
https://reviews.llvm.org/D35110
Files:
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
test/Analysis/constraint_manager_negate_difference.c
test/Analysis/ptr-arith.c
Index: test/Analysis/ptr-arith.c
===
--- test/Analysis/ptr-arith.c
+++ test/Analysis/ptr-arith.c
@@ -265,49 +265,26 @@
clang_analyzer_eval((rhs - lhs) > 0); // expected-warning{{TRUE}}
}
-//---
-// False positives
-//---
-
void zero_implies_reversed_equal(int *lhs, int *rhs) {
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{UNKNOWN}}
if ((rhs - lhs) == 0) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs != lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{FALSE}}
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs != lhs); // expected-warning{{TRUE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
- clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void canonical_equal(int *lhs, int *rhs) {
clang_analyzer_eval(lhs == rhs); // expected-warning{{UNKNOWN}}
if (lhs == rhs) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
-
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void compare_element_region_and_base(int *p) {
Index: test/Analysis/constraint_manager_negate_difference.c
===
--- /dev/null
+++ test/Analysis/constraint_manager_negate_difference.c
@@ -0,0 +1,39 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection -verify %s
+
+void clang_analyzer_eval(int);
+
+void equal(int m, int n) {
+ if (m != n)
+return;
+ clang_analyzer_eval(n == m); // expected-warning{{TRUE}}
+}
+
+void non_equal(int m, int n) {
+ if (m == n)
+return;
+ clang_analyzer_eval(n != m); // expected-warning{{TRUE}}
+}
+
+void less_or_equal(int m, int n) {
+ if (m < n)
+return;
+ clang_analyzer_eval(n <= m); // expected-warning{{TRUE}}
+}
+
+void less(int m, int n) {
+ if (m <= n)
+return;
+ clang_analyzer_eval(n < m); // expected-warning{{TRUE}}
+}
+
+void greater_or_equal(int m, int n) {
+ if (m > n)
+return;
+ clang_analyzer_eval(n >= m); // expected-warning{{TRUE}}
+}
+
+void greater(int m, int n) {
+ if (m >= n)
+return;
+ clang_analyzer_eval(n > m); // expected-warning{{TRUE}}
+}
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -256,6 +256,29 @@
return newRanges;
}
+ // Turn all [A, B] ranges to [-B, -A]. Turn minimal signed value to maximal
+ // signed value and vice versa.
+ RangeSet Negate(BasicValueFactory &BV, Factory &F) const {
+PrimRangeSet newRanges = F.getEmptySet();
+
+for (iterator i = begin(), e = end(); i != e; ++i) {
+ const llvm::APSInt &from = i->From(), &to = i->To();
+ const llvm::APSInt &newFrom = (to.isMinSignedValue() ?
+ BV.getMaxValue(to) :
+ (to.isMaxSignedValue() ?
+ BV.getMinValue(to) :
+ BV.getValue(- to)));
+ const llvm::APSInt &newTo = (from.isMinSignedValue() ?
+ BV.getMaxValue(from) :
+ (from.isMaxSignedValue() ?
+BV.getMinValue(from) :
+BV.getValue(- from)));
+ newRanges = F.add(newRanges, Range(newFrom, newTo));
+}
+
+return newRanges;
+ }
+
void print(raw_ostream &os) const {
bool isFirst = true;
os << "{ ";
@@ -465,11 +488,38 @@
if (ConstraintRangeTy::data_type *V = State->get(Sym))
return *V;
- // Lazily generate a new RangeSet representing all possible values for the
- // given symbol type.
+ // If Sym is a difference of symbols A - B, then maybe we have range set
+ // stored for B - A.
BasicValueFactory &BV = getBasicVals();
QualType T = Sym->getTyp
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware added inline comments.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:511
+ SSE->getLHS()->getType()->isSignedIntegerOrEnumerationType() ||
+ SSE->getLHS()->getType()->isPointerType()) {
+ return negV->Negate(BV, F);
NoQ wrote:
> Pointer types are currently treated as unsigned, so i'm not sure you want
> them here.
For me it seems that pointer differences are still pointer types and they are
signed. (The range becomes negative upon negative assumption. From test
`ptr-arith.c`:
```
void use_symbols(int *lhs, int *rhs) {
clang_analyzer_eval(lhs < rhs); // expected-warning{{UNKNOWN}}
if (lhs < rhs)
return;
clang_analyzer_eval(lhs < rhs); // expected-warning{{FALSE}}
clang_analyzer_eval(lhs - rhs); // expected-warning{{UNKNOWN}}
if ((lhs - rhs) != 5)
return;
clang_analyzer_eval((lhs - rhs) == 5); // expected-warning{{TRUE}}
}
```
If I put `clang_analyzer_printState()` into the empty line in the middle, I get
the following range for the difference: `[-9223372036854775808, 0]`. If I
replace `int*` with `unsigned`, this range becomes `[0, 0]`, so `int*` is
handled as a signed type here.
https://reviews.llvm.org/D35110
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
NoQ added inline comments.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:496
+ if (const SymSymExpr *SSE = dyn_cast(Sym)) {
+if (SSE->getOpcode() == BO_Sub) {
With this, it sounds as if we're half-way into finally supporting the unary
minus operator (:
Could you add a FIXME here: "Once SValBuilder supports unary minus, we should
use SValBuilder to obtain the negated symbolic expression instead of
constructing the symbol manually. This will allow us to support finding ranges
of not only negated SymSymExpr-type expressions, but also of other, simpler
expressions which we currently do not know how to negate."
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:499-504
+ // If the type of A - B is the same as the type of A, then use the type
of
+ // B as the type of B - A. Otherwise keep the type of A - B.
+ SymbolRef negSym = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub,
+ SSE->getLHS(),
+ (T == SSE->getLHS()->getType()) ?
+ SSE->getRHS()->getType() : T);
I'm quite sure that types of `A - B` and `B - A` are always equal when it comes
to integer promotion rules.
Also, due to our broken `SymbolCast` (which is often missing where it ideally
should be), the type of the `A - B` symbol may not necessarily be the same as
the type that you obtain by applying integer promotion rules to types of `A`
and `B`.
So i think you should always take the type of `A - B` and expect to find `B -
A` of the same type in the range map, otherwise give up.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:511
+ SSE->getLHS()->getType()->isSignedIntegerOrEnumerationType() ||
+ SSE->getLHS()->getType()->isPointerType()) {
+ return negV->Negate(BV, F);
Pointer types are currently treated as unsigned, so i'm not sure you want them
here.
Comment at: test/Analysis/ptr-arith.c:268-270
//---
// False positives
//---
The tests that are now supported should be moved above this comment.
https://reviews.llvm.org/D35110
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
xazax.hun added inline comments.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:500
+ // If the type of A - B is the same as the type of A, then use the type
of
+ // B as the type of B - A. Otherwise keep the type of A - B.
+ SymbolRef negSym = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub,
Could you give an example why do you need this (probably as a test), or
constrain the transformation when all the types are the same?
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:507
+ State->get(negSym)) {
+// Do not negate an unsigned range set, unless it is [0, 0].
+if((negV->getConcreteValue() &&
I think it would be better to describe why don't we want to do that rather than
describing what the code does.
https://reviews.llvm.org/D35110
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware updated this revision to Diff 105593.
baloghadamsoftware added a comment.
Wrong patch files was uploaded first.
https://reviews.llvm.org/D35110
Files:
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
test/Analysis/ptr-arith.c
Index: test/Analysis/ptr-arith.c
===
--- test/Analysis/ptr-arith.c
+++ test/Analysis/ptr-arith.c
@@ -272,42 +272,23 @@
void zero_implies_reversed_equal(int *lhs, int *rhs) {
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{UNKNOWN}}
if ((rhs - lhs) == 0) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs != lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{FALSE}}
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
clang_analyzer_eval(rhs != lhs); // expected-warning{{TRUE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
- clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void canonical_equal(int *lhs, int *rhs) {
clang_analyzer_eval(lhs == rhs); // expected-warning{{UNKNOWN}}
if (lhs == rhs) {
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{TRUE}}
-#else
-clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
return;
}
clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
-
-#ifdef ANALYZER_CM_Z3
clang_analyzer_eval(rhs == lhs); // expected-warning{{FALSE}}
-#else
- clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
-#endif
}
void compare_element_region_and_base(int *p) {
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -256,6 +256,29 @@
return newRanges;
}
+ // Turn all [A, B] ranges to [-B, -A]. Turn minimal signed value to maximal
+ // signed value and vice versa.
+ RangeSet Negate(BasicValueFactory &BV, Factory &F) const {
+PrimRangeSet newRanges = F.getEmptySet();
+
+for (iterator i = begin(), e = end(); i != e; ++i) {
+ const llvm::APSInt &from = i->From(), &to = i->To();
+ const llvm::APSInt &newFrom = (to.isMinSignedValue() ?
+ BV.getMaxValue(to) :
+ (to.isMaxSignedValue() ?
+ BV.getMinValue(to) :
+ BV.getValue(- to)));
+ const llvm::APSInt &newTo = (from.isMinSignedValue() ?
+ BV.getMaxValue(from) :
+ (from.isMaxSignedValue() ?
+BV.getMinValue(from) :
+BV.getValue(- from)));
+ newRanges = F.add(newRanges, Range(newFrom, newTo));
+}
+
+return newRanges;
+ }
+
void print(raw_ostream &os) const {
bool isFirst = true;
os << "{ ";
@@ -465,11 +488,36 @@
if (ConstraintRangeTy::data_type *V = State->get(Sym))
return *V;
- // Lazily generate a new RangeSet representing all possible values for the
- // given symbol type.
+ // If Sym is a difference of symbols A - B, then maybe we have range set
+ // stored for B - A.
BasicValueFactory &BV = getBasicVals();
QualType T = Sym->getType();
+ if (const SymSymExpr *SSE = dyn_cast(Sym)) {
+if (SSE->getOpcode() == BO_Sub) {
+ SymbolManager &SymMgr = State->getSymbolManager();
+ // If the type of A - B is the same as the type of A, then use the type of
+ // B as the type of B - A. Otherwise keep the type of A - B.
+ SymbolRef negSym = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub,
+ SSE->getLHS(),
+ (T == SSE->getLHS()->getType()) ?
+ SSE->getRHS()->getType() : T);
+ if (ConstraintRangeTy::data_type *negV =
+ State->get(negSym)) {
+// Do not negate an unsigned range set, unless it is [0, 0].
+if((negV->getConcreteValue() &&
+(*negV->getConcreteValue() == 0)) ||
+ SSE->getLHS()->getType()->isSignedIntegerOrEnumerationType() ||
+ SSE->getLHS()->getType()->isPointerType()) {
+ return negV->Negate(BV, F);
+}
+ }
+}
+ }
+
+ // Lazily generate a new RangeSet representing all possible values for the
+ // given symbol type.
+
RangeSet Result(F, BV.getMinValue(T), BV.getMaxValue(T));
// Special case: references are known to be non-zero.
___
[PATCH] D35110: [Analyzer] Constraint Manager Negates Difference
baloghadamsoftware created this revision.
If range `[m .. n]` is stored for symbolic expression `A - B`, then we can
deduce the range for `B - A` which is [-n .. -m]. This is only true for signed
types, unless the range is `[0 .. 0]`.
https://reviews.llvm.org/D35110
Files:
lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
test/Analysis/std-c-library-functions.c
test/Analysis/svalbuilder-rearrange-comparisons.c
Index: test/Analysis/svalbuilder-rearrange-comparisons.c
===
--- /dev/null
+++ test/Analysis/svalbuilder-rearrange-comparisons.c
@@ -0,0 +1,156 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection -verify %s
+
+void clang_analyzer_dump(int x);
+void clang_analyzer_printState();
+
+int f();
+
+void compare_different_symbol() {
+ int x = f(), y = f();
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 0}}
+}
+
+void compare_different_symbol_plus_left_int() {
+ int x = f()+1, y = f();
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_minus_left_int() {
+ int x = f()-1, y = f();
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$5{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 1}}
+}
+
+void compare_different_symbol_plus_right_int() {
+ int x = f(), y = f()+2;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 2}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 2}}
+}
+
+void compare_different_symbol_minus_right_int() {
+ int x = f(), y = f()-2;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 2}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int() {
+ int x = f()+2, y = f()+1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int() {
+ int x = f()+2, y = f()-1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$5{int}) - (conj_$2{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int() {
+ int x = f()-2, y = f()+1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int() {
+ int x = f()-2, y = f()-1;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$5{int}) - 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{((conj_$2{int}) - (conj_$5{int})) == 1}}
+}
+
+void compare_same_symbol() {
+ int x = f(), y = x;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{1 S32b}}
+}
+
+void compare_same_symbol_plus_left_int() {
+ int x = f(), y = x;
+ ++x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_left_int() {
+ int x = f(), y = x;
+ --x;
+ clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_plus_right_int() {
+ int x = f(), y = x+1;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+ clang_analyzer_dump(x == y);
+ // expected-warning@-1{{0 S32b}}
+}
+
+void compare_same_symbol_minus_right_int() {
+ int x = f(), y = x-1;
+ clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+ clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+ clang_analyzer_dump(x == y);
