[PATCH] D112296: [Analyzer][solver] Handle adjustments in constraint assignor remainder

[Denys Petrov via Phabricator via cfe-commits]

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