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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
