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:
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;
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
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
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
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
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
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
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
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
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:
>
> >
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`
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
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
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
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
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
NoQ added inline comments.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:265-276
+ const llvm::APSInt = i->From(), = i->To();
+ const llvm::APSInt = (to.isMinSignedValue() ?
+ BV.getMaxValue(to) :
+
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
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
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
baloghadamsoftware added inline comments.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:265-276
+ const llvm::APSInt = i->From(), = i->To();
+ const llvm::APSInt = (to.isMinSignedValue() ?
+ BV.getMaxValue(to) :
+
NoQ added inline comments.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:265-276
+ const llvm::APSInt = i->From(), = i->To();
+ const llvm::APSInt = (to.isMinSignedValue() ?
+ BV.getMaxValue(to) :
+
baloghadamsoftware added inline comments.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:265-276
+ const llvm::APSInt = i->From(), = i->To();
+ const llvm::APSInt = (to.isMinSignedValue() ?
+ BV.getMaxValue(to) :
+
NoQ added inline comments.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:265-276
+ const llvm::APSInt = i->From(), = i->To();
+ const llvm::APSInt = (to.isMinSignedValue() ?
+ BV.getMaxValue(to) :
+
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
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
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
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
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
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
>
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
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
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
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.
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
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.
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 added inline comments.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:511
+ SSE->getLHS()->getType()->isSignedIntegerOrEnumerationType() ||
+ SSE->getLHS()->getType()->isPointerType()) {
+ return negV->Negate(BV,
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 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
baloghadamsoftware added inline comments.
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:511
+ SSE->getLHS()->getType()->isSignedIntegerOrEnumerationType() ||
+ SSE->getLHS()->getType()->isPointerType()) {
+ return negV->Negate(BV,
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
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 =
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
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:
46 matches
Mail list logo
