martong marked an inline comment as done.
martong added inline comments.
================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:1623
if (!Constraint.containsZero()) {
- State = RCM.assumeSymNE(State, LHS, Zero, Zero);
+ State = RCM.assumeSymRel(State, LHS, BO_NE, Zero);
if (!State)
----------------
ASDenysPetrov wrote:
> martong wrote:
> > ASDenysPetrov wrote:
> > > What I see, you're still trying to avoid using `State->assume`, which I
> > > recommend in a parent revision, but coming closer using its guts.
> > So, it would look like this:
> > ```
> > State =
> > State->assume(Builder.makeSymbolVal(LHS).castAs<nonloc::SymbolVal>(), true);
> > ```
> > The main reason why we cannot use `State->assume` is that it boils down to
> > `RangedConstraintManager::assumeSym` that has a specific logic for the
> > `boolean` assumption. I.e. the operator is being negated in a case:
> > ```
> > if (BinaryOperator::isComparisonOp(op) && op != BO_Cmp) {
> > if (!Assumption)
> > op = BinaryOperator::negateComparisonOp(op);
> >
> > return assumeSymRel(State, SIE->getLHS(), op, SIE->getRHS());
> > }
> > ```
> > You can try it for yourself, and see that the test case added in this patch
> > will not pass if we were to use `State->assume`. Essentially, we have to
> > evade the special "bool" logic, and the closest we can get is using
> > `assumeSymRel`.
> >
> > Besides that, by using `State->assume` we would have a superfluous
> > conversion chain `Symbol->SVal->Symbol` until we reach `assumeSymRel`.
> >You can try it for yourself, and see that the test case added in this patch
> >will not pass if we were to use `State->assume.`
> I can't confirm. Your test case passed when I replaced with `State =
> State->assume(Builder.makeSymbolVal(LHS).castAs<nonloc::SymbolVal>(), true);`.
> > specific logic for the boolean assumption. I.e. the operator is being
> > negated in a case:
> That just simplifies the expression, say, you want to find whether `x > 5 is
> false`, than the Solver finds for you whether
> `x <= 5 is true`, which is an equivalent.
> > Essentially, we have to evade the special "bool" logic
> There is no problem with //bool// logic. It's an equivalent of `SVal != 0`
> when //true//, and `SVal == 0` when //false//. Nothing more.
>
> All in all I see the problem to use `assume`. Not because of this function
> itself, but because you do it incorrect by getting an `SVal` from `LHS` with
> `makeSymbolVal`. We should get it with `State->getSVal` which needs
> `LocationContext` as a second parameter. And that's the challenge, to pass
> `LocationContext` here, since `RangedConstraintManager` doesn't use it, at
> least for now.
> I can't confirm. Your test case passed when I replaced with `State =
> State->assume(Builder.makeSymbolVal(LHS).castAs<nonloc::SymbolVal>(), true);`.
Actually, since the last time I tried with `State->assume` we merged D110913.
If you revert the changes of that patch you'll see that this test case indeed
fails. However, here is a slightly modified case that fails even on the current
llvm/main branch with `State->assume` but passes with `assumeSymRel`:
```
void rem_constant_adj(int x, int y) {
if ((x + y + 1) % 3 == 0) // (x + y + 1) % 3 != 0 -> x + y + 1 != 0 -> x != -1
return;
clang_analyzer_eval(x + y + 1 != 0); // expected-warning{{TRUE}}
clang_analyzer_eval(x + y != -1); // expected-warning{{TRUE}}
(void)(x * y); // keep the constraints alive.
}
```
The only change is that we have `x + y` instead of `x`.
Now, the explanation for the original test case when we have `(x + 1) % 3`:
When we ask the value of `x != -1` then `assumeDual` evaluates the TRUE case
which is feasible and then it tries to evaluate the FALSE case, so it queries
`x == -1` is true. However, this kicks in the simplification, which simplifies
the previous constraint of `x+1, [not 0]` to `-1 + 1, [not 0]` which is a
contradiction, thus an infeasible state is returned.
When we have `x + y` in the test case, then simplification cannot simplify `x +
y + 1`, thus the situation is different.
So, the main problem with `State->assume` is that it does not compute the
adjustment. I.e. when we have `x + 1` as LHS then `assumeSym(LHS)` calls into
`assumeSymUnsupported` and that does not compute the adjustment. The only
functions that compute the adjustment are `assumeSymRel` and
`assumeSymInclusiveRange`.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D112296/new/
https://reviews.llvm.org/D112296
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
