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

[Gabor Marton via Phabricator via cfe-commits]

martong marked 2 inline comments as done.
martong added a comment.

> 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.

Yes, good point(s). I am trying to avoid turning into a fixed point algorithm by directly iterating over the equivalence classes instead of reusing the existing track mechanism. On the other hand, perhaps with some budge the fixpoint algo would be worth to experiment with.



================
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);
+
----------------
vsavchenko wrote:
> 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`?
Don't be puzzled by this. This indeed bifurcates. The interesting path is where `b0 == 2` is true.

I am going to update this line with `if (b0 ==2) {` to achieve a similar effect. (I was using creduce and tried to simplify even more after that, but i missed this.)


================
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) {
----------------
vsavchenko wrote:
> 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?
When we evaluate `e2 > 0` then we will set `e1` as disequal to `b1`. However, at this point because of the eager constant folding `e1` is `e0 - 2` (on the path where `b0 == 2` is true). 

So, when we evaluate `b1 == e1` then this is the diseq info we have in the State (I used `dumpDisEq` from D103967):
```
reg_$2<int b1>
DisequalTo:
(reg_$0<int e0>) - 2

(reg_$0<int e0>) - 2
DisequalTo:
reg_$2<int b1>
```

And indeed we ask directly whether the LHS (`reg_$2<int b1>`) is equal to RHS`(reg_$0<int e0>) - (reg_$1<int b0>)`.  This is because the `DeclRefExpr` of `e1` is still bound to SVal which originates from the time before we constrained b0 to 2. With other words: the `Environment` is not changed by introducing a new constraint.

BTW, this test fails even in llvm/main.





Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D103314/new/

https://reviews.llvm.org/D103314