[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 inline comments.


================
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) {
----------------
martong wrote:
> 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.
> 
> 
> 
>  With other words: the Environment is not changed by introducing a new constraint.

This suggests that another approach could be to do change the `Environment` when we add a new constraint. I am not sure about the pros/cons atm, but might be worth to experiment. What do you think?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103314