martong marked 2 inline comments 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)
----------------
steakhal wrote:
> ASDenysPetrov wrote:
> > martong wrote:
> > > martong wrote:
> > > > 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`.
> > > BTW, if D103317 was merged, then I'd have to find another test case that
> > > fails here, but I think I could find one. Anyway, the point is that we
> > > need a function here, that handles the adjustments.
> > > 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.
> > Wow, I've just seen a possible solution in the game of words. If
> > `assumeSym(LHS)` leads to //assumeSym**Unsupported**//, then we just need
> > to support it, namely, make it go to `assumeSymRel`. IMO it's worth to
> > investigate such a chance.
> +1, Thank you for pushing this @ASDenysPetrov
> > 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.
> Wow, I've just seen a possible solution in the game of words. If
> `assumeSym(LHS)` leads to //assumeSym**Unsupported**//, then we just need to
> support it, namely, make it go to `assumeSymRel`. IMO it's worth to
> investigate such a chance.
Okay, that could be a good alternative, good idea!
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
