vsavchenko added a comment.
OK, we definitely need to know about performance.
Plus, I'm still curious about the crash. I didn't get how simplification
helped/caused that crash.
I have one thought here. If the lack of simplification indeed caused the crash,
we are in trouble with this patch. IMO simplification in just one place should
make it better, but shouldn't produce infeasible states for us. In other
words, any number simplifications is a conservative operation that makes our
lives a bit better. The moment they become a requirement (i.e. simplifications
call for more simplifications or we crash) this solution from this patch has to
become much harder. This is because whenever we do `merge`, we essentially can
create another situation when we find out that some symbolic expression is a
constant. Let's say that we are merging classes `A` and `B` which have
constraints `[INT_MIN, 42]` and `[42, INT_MAX]`. After the merge, we are
positive that all the members of this new class are equal to 42. And if so, we
can further simplify classes and their members. This algorithm turns into a
fixed point algorithm, which has a good chance to sabotage our performance.
This being said, can we re-iterate on that crash and the proposed fix in much
more detail?
================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1789
+ if (DisequalToOther.contains(*this))
+ return nullptr;
if (!DisequalToOther.isEmpty()) {
----------------
very opinionated nit: can you please add extra new line after this?
================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1976-1986
+ Optional<bool> KnownClassEquality =
+ isEqualTo(State, ClassOfSimplifiedSym);
+ if (KnownClassEquality) {
+ // The classes are already equal, there is no need to merge.
+ if (*KnownClassEquality == true)
+ continue;
+ // We are about to add the newly simplified symbol to this equivalence
----------------
Now, since you put this logic into `merge`, you can just merge.
================
Comment at: clang/test/Analysis/find-binop-constraints.cpp:150
+ int e1 = e0 - b0; // e1 is bound to (reg_$0<int e0>) - (reg_$1<int b0>)
+ (void)(b0 == 2);
+
----------------
It's not really connected to your patch, but this confuses me! Why does the
analyzer think that `b0` is guaranteed to be 2 after this statement. Even if
we eagerly assume here, shouldn't it mean that there are still two paths `b0 ==
2` and `b0 != 2`?
================
Comment at: clang/test/Analysis/find-binop-constraints.cpp:155-158
+ // Here, e1 is still bound to (reg_$0<int e0>) - (reg_$1<int b0>) but we
+ // should be able to simplify it to (reg_$0<int e0>) - 2 and thus realize
+ // the contradiction.
+ if (b1 == e1) {
----------------
Hmm, I don't see how simplification helped here.
After the previous `if` statement, we should have had two equivalence classes
known to be disequal: `reg_$2<int b1>` and `(reg_$0<int e0>) - (reg_$1<int
b0>)`.
Further, we directly compare these two symbols. We can figure it out without
any simplifications.
Am I missing something here?
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D103314/new/
https://reviews.llvm.org/D103314
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
