NoQ added a comment.
In https://reviews.llvm.org/D35109#969712, @baloghadamsoftware wrote:
> In https://reviews.llvm.org/D35109#969109, @NoQ wrote:
>
> > I guess it'd be an `-analyzer-config` flag. You can add it to the
> > `AnalyzerOptions` object, which has access to these flags and can be
>
baloghadamsoftware added a comment.
In https://reviews.llvm.org/D35109#969109, @NoQ wrote:
> I guess it'd be an `-analyzer-config` flag. You can add it to the
> `AnalyzerOptions` object, which has access to these flags and can be accessed
> from `AnalysisManager`.
OK, I can do that. BUt how
NoQ added a comment.
In https://reviews.llvm.org/D35109#968314, @baloghadamsoftware wrote:
> But how to add a flag for this? Is it a flag enabled by the user or is it
> automatically enabled if the checker is enabled?
I guess it'd be an `-analyzer-config` flag. You can add it to the
baloghadamsoftware added a comment.
In https://reviews.llvm.org/D35109#956075, @NoQ wrote:
> I'm totally fine with assuming the MAX/4 constraint on checker side -
> extension math would still be better than the MAX/4 pattern-matching in core
> because extension math should be more useful on
NoQ added a comment.
Herald added a subscriber: rnkovacs.
In https://reviews.llvm.org/D35109#943558, @baloghadamsoftware wrote:
> In https://reviews.llvm.org/D35109#937763, @NoQ wrote:
>
> > For the type extension approach, somebody simply needs to do the math and
> > prove that it works
baloghadamsoftware added a comment.
In https://reviews.llvm.org/D35109#937763, @NoQ wrote:
> For the type extension approach, somebody simply needs to do the math and
> prove that it works soundly in all cases. Devin has been heroically coming up
> with counter-examples so far, but even if he
george.karpenkov added a comment.
> If the type extension approach is proven to be sound
I lack the full context here, but in my experience Z3 is really great for
proving whether certain operations may or may not overflow, using the built-in
bitvector type.
(I'm not sure though if that is what
NoQ added a comment.
The reason why i don't want to commit the MAX/4 approach now (for `>`/`<` case)
is that it has too little useful effects until the iterator checker is enabled
by default. However, it is a core change that immediately affects all users
with all its negative effects (such as
baloghadamsoftware added a comment.
Let us summarize the possibilities:
1. Type extension approach. I tested it, all tests pass, and also in Devin's
examples we do not infer narrower range than we should. (Wider do not matter.)
I think this is the most complete solution and many checkers could
xazax.hun added a comment.
In https://reviews.llvm.org/D35109#926078, @baloghadamsoftware wrote:
> So still the options are to fix it in the checker or fix it in the engine
> (the max/4 or the type extension solution), but leaving it unfixed is not an
> option. I am open to any solution, but
baloghadamsoftware added a comment.
Thank you for your respone! However, I think you (not you, Artem, but you three
at Apple) do not really understand that I need to compare A+m to B+n not only
because of the iterator range checking, but also in later parts. So your
proposal means that I am
NoQ added a comment.
The unconstrained rearrangements for `+`/`-`/`==`/`!=` are definitely good to
go regardless of anything else.
Within the checker, we propose to manually simplify both `$x - N < $x` and `$x
+ N > $x` to true (where N is positive), because in general this is unsound
(due to
xazax.hun added a comment.
In https://reviews.llvm.org/D35109#916617, @NoQ wrote:
> A breakthrough with credit going to Devin: Note that whenever we're not
> dealing with `>`/`<`/`<=`/`>=` (but only with additive ops and `==` and `!=`,
> and we have everything of the same type) we can
baloghadamsoftware added a comment.
In https://reviews.llvm.org/D35109#916648, @NoQ wrote:
> > How to find the N if we only use == or !=?
>
> Hence the difference between `==` and `is-the-same-symbol-as`. We can find
> `N` by looking at the symbol.
Sorry, if I misunderstand something, but if
NoQ added a comment.
> How to find the N if we only use == or !=?
Hence the difference between `==` and `is-the-same-symbol-as`. We can find `N`
by looking at the symbol.
We'd lose track of cases where, say, `i` and `.end()` were compared to each
other for `>`/`<` before. The question is
baloghadamsoftware added a comment.
Thank you for your comment!
Unfortunately, the iterator checkers depend very much on the >/>=/=C.end(), I cannot imagine this
to be solved just with ==/!=. How to find the N if we only use == or !=?
Furthermore, later parts also add invalidation check where
NoQ added a comment.
A breakthrough with credit going to Devin: Note that whenever we're not dealing
with `>`/`<`/`<=`/`>=` (but only with additive ops and `==` and `!=`, and we
have everything of the same type) we can rearrange regardless of constraints,
simply because Z/nZ is an abelian
baloghadamsoftware added a comment.
Thank you for you work! Probably I did some mistake because my MAX/4solution
did not work when I it earlier. Your solution seems to work. For the iterator
checkers this is surely enough. Should I upload my patch patched with your one?
NoQ added a comment.
In https://reviews.llvm.org/D35109#837723, @NoQ wrote:
> It's something similar to assuming that the string length is within range [0,
> INT_MAX/4] in CStringChecker: we can easily assume that no overflow is
> happening in computations involving string lengths or iterator
baloghadamsoftware added a comment.
Any progress reviewing this? Iterator checkers are pending for more than half a
year because of this.
An alternative solution is to always extend the type and change
`ProgramState::assumeInbound()` so it does not move everything to the bottom of
the range,
baloghadamsoftware added inline comments.
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:595
+
+ if (origWidth < 128) {
+auto newWidth = std::max(2 * origWidth, (uint32_t) 8);
danielmarjamaki wrote:
> I would like that "128" is
danielmarjamaki added a comment.
I like this patch overall.. here are some stylistic nits.
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:610
+} else {
+ if (*lInt >= *rInt) {
+newRhsExt = lInt->getExtValue() -
baloghadamsoftware updated this revision to Diff 119576.
baloghadamsoftware added a comment.
Herald added a subscriber: szepet.
I think it is the final attempt. If Symbols are different, the type is
extended, so we store a correct (but extended) range. However, if the Symbols
are the same, we
baloghadamsoftware added a comment.
I tried to extend the type to avoid overflow scenarios. Unfortunately, this
breaks essential calculations based on the overflow scenarios (e.g.
ProgramSate::assumeInbound()). So I see no other option than to abandon this
patch and return to the local
baloghadamsoftware added a comment.
It seems that Artem's suggestion is not enough (or I misunderstood it). So two
options remain: either we drop this and revert to the local solution in the
Iterator Checkers or we extend the type when rearranging the comparison. Which
way to go?
baloghadamsoftware updated this revision to Diff 116662.
baloghadamsoftware added a comment.
If both sides have concrete integers, they must be in range [min/4..max/4], if
only one, it must be in range [min/2..max/2].
https://reviews.llvm.org/D35109
Files:
baloghadamsoftware added a comment.
Anna, Devin, should I proceed with Artem's suggested way?
https://reviews.llvm.org/D35109
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
NoQ added a comment.
In https://reviews.llvm.org/D35109#837673, @zaks.anna wrote:
> > What do you suggest? Should we widen the type of the difference, or abandon
> > this patch and revert back to the local solution I originally used in the
> > iterator checker?
>
> Does the local solution you
alexshap added inline comments.
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:561
+ // manager to handle these comparisons.
+ if (BinaryOperator::isComparisonOp(op) &&
+ rhs.getSubKind() == nonloc::SymbolValKind) {
some thoughts -
zaks.anna added a comment.
> What do you suggest? Should we widen the type of the difference, or abandon
> this patch and revert back to the local solution I originally used in the
> iterator checker?
Does the local solution you used in the iterator checker not have the same
problem?
baloghadamsoftware added a comment.
What do you suggest? Should we widen the type of the difference, or abandon
this patch and revert back to the local solution I originally used in the
iterator checker?
https://reviews.llvm.org/D35109
___
dcoughlin added a comment.
It still seems like we are inferring invariants that are not sound. Do we need
to restrict the symbolic transformation so that it only applies when A - B,
too, is known to not overflow? Is that sufficient? Is it often the case that
the analyzer knows these
baloghadamsoftware updated this revision to Diff 109117.
baloghadamsoftware added a comment.
Overflow scenarios skipped.
https://reviews.llvm.org/D35109
Files:
lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
test/Analysis/svalbuilder-rearrange-comparisons.c
Index:
dcoughlin requested changes to this revision.
dcoughlin added a comment.
This revision now requires changes to proceed.
Artem, Anna, and I discussed this a bit in person. We think that even though
the benefits look great, it can't be generally applied. Maybe we could apply it
in cases where
dcoughlin added a comment.
I have some concerns about soundness when the rearrangement may overflow.
Here is an example:
void clang_analyzer_eval(int);
void foo(signed char A, signed char B) {
if (A + 0 >= B + 0) {
clang_analyzer_eval(A - 126 == B + 3); // This yields FALSE
baloghadamsoftware updated this revision to Diff 107032.
baloghadamsoftware added a comment.
Rearrangement of unsigned comparison removed (FIXME added). Comment regarding
the types of integer constants added.
https://reviews.llvm.org/D35109
Files:
NoQ added a comment.
I think we'd rather delay the unsigned difference feature (as far as i
understand, you don't rely on it in the iterator checker), than introduce the
artificial cast to signed which may have unexpected consequences, because
that's not how unsigned difference normally
baloghadamsoftware updated this revision to Diff 106626.
baloghadamsoftware added a comment.
Difference of unsigned is converted to signed.
https://reviews.llvm.org/D35109
Files:
include/clang/AST/ASTContext.h
lib/AST/ASTContext.cpp
lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
baloghadamsoftware added a comment.
The other possibility is to make the difference signed.
https://reviews.llvm.org/D35109
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
baloghadamsoftware added a comment.
I think we should exclude unsigned types completely. `A >= B` is converted to
`A - B >= 0`, thus the range of `A - B` is `[0 .. INT_MAX]` which is the full
range for the unsigned type. This implies that upon any conditional statement
`if (A >= B) ...` the
baloghadamsoftware added a comment.
In https://reviews.llvm.org/D35109#806156, @NoQ wrote:
> I think you might also need to convert `APSInt`s to an appropriate type, as
> done above. Type of right-hand-side `APSInt`s do not necessarily coincide
> with the type of the left-hand-side symbol or
NoQ added a comment.
I think you might also need to convert `APSInt`s to an appropriate type, as
done above. Type of right-hand-side `APSInt`s do not necessarily coincide with
the type of the left-hand-side symbol or of the whole expression. `APSInt`
operations crash when signedness doesn't
xazax.hun added a comment.
Are you sure this works as intended when e.g.: `$a+2==$b*3`
So on one of the sides, the ops are not additive?
I would like to see some test cases for that.
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:572
+ lInt = >getRHS();
baloghadamsoftware marked an inline comment as done.
baloghadamsoftware added a comment.
In https://reviews.llvm.org/D35109#801921, @NoQ wrote:
> Because integer promotion rules are tricky, could we, for now, avoid dealing
> with the situation when left-hand side and right-hand side and the
baloghadamsoftware marked an inline comment as done.
baloghadamsoftware added inline comments.
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:583
+newRhs = BasicVals.evalAPSInt(BO_Add, *lInt, *rInt);
+reverse = (lop == BO_Add);
+ }
baloghadamsoftware updated this revision to Diff 105628.
baloghadamsoftware added a comment.
Type check added and restricted to additive operators.
https://reviews.llvm.org/D35109
Files:
lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
test/Analysis/std-c-library-functions.c
NoQ added a comment.
Thanks, this looks great!
Because integer promotion rules are tricky, could we, for now, avoid dealing
with the situation when left-hand side and right-hand side and the result (all
three) are not all of the same type? Or maybe we'd like to support substraction
of
baloghadamsoftware created this revision.
Since the range-based constraint manager (default) is weak in handling
comparisons where symbols are on both sides it is wise to rearrange them to
have symbols only on the left side. Thus e.g. `A + n >= B + m` becomes `A - B
>= m - n` which enables the
48 matches
Mail list logo
