[PATCH] D103314: [Analyzer][solver] Simplify existing constraints when a new constraint is added

[Valeriy Savchenko via Phabricator via cfe-commits]

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