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