[PATCH] D115149: [analyzer][solver] Fix assertion on (NonLoc, Op, Loc) expressions

[Balázs Benics via Phabricator via cfe-commits]

steakhal marked an inline comment as done.
steakhal added a comment.

Sorry for my late response, I have a bunch of other tasks to do.

---

In D115149#3175068 <https://reviews.llvm.org/D115149#3175068>, @NoQ wrote:

>> It can happen if the `Loc` was perfectly constrained to a concrete
>> value (`nonloc::ConcreteInt`)
>
> This shouldn't happen. It should be `loc::ConcreteInt` which is, well, a `Loc`.

Well, yes.

However, unless we implement `evalBinOpLN()` for all possible arithmetic operators and do the same for the `evalBinOpNL()` (which currently doesn't exist), we cannot calculate this operation accurately.
In the arithmetic operation, we have two integral operands, which is basically modeled by the domain of `NonLocs`. However, the address of a pointer is modeled by `Locs`. There is the reinterpret-cast operation which is capable of crossing these two domains, producing an expression that can participate in arithmetic operations, but on the abstract domain side, we still stick to `Locs`, which breaks the assumption that should only handle the `BO_Add` for mixed domain symbolic computations.

By combining this with the improved simplifier, which substitutes concretized subexpressions we can get to a situation where we have to evaluate other operators besides `BO_Add`.
I had no time to implement `evalBinOpLN()` for all possible arithmetic operators nor implement `evalBinOpNL()` in a similar way. The current implementation in this patch is like a hotfix, doing the best possible thing given that the mentioned functions/behavior is not implemented yet.
IMO since it did not crash too frequently, it is probably not that critical to have this slight inaccuracy in representation - given that zero is zero in both (NonLocs, Locs) domains xD.
Alternatively to this, we could return `Unknown`, but I feel like that approach is even worse than this.



================
Comment at: clang/lib/StaticAnalyzer/Core/SValBuilder.cpp:463
+  if (const Optional<Loc> RV = rhs.getAs<Loc>()) {
+    const auto IsCommutative = [](BinaryOperatorKind Op) {
+      return Op == BO_Mul || Op == BO_Add || Op == BO_And || Op == BO_Xor ||
----------------
ASDenysPetrov wrote:
> IMO it should be in a family of `BinaryOperator::is..` methods.
It isn't as easy as it might seem at first glance. I've considered doing it that way.
In our context, we don't really deal with floating-point numbers, but in the generic implementation, we should have the type in addition to the OpKind. We don't need that complexity, so I sticked to inlining them here.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D115149/new/

https://reviews.llvm.org/D115149