[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

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

steakhal added a comment.

In D88019#2291953 <https://reviews.llvm.org/D88019#2291953>, @steakhal wrote:

> What are our options mitigating anything similar happening in the future?
>
> This way any change touching the `SymbolicRangeInferrer` and any related parts of the analyzer seems to be way too fragile.
> Especially, since we might want to add support for comparing SymSyms, just like we try to do in D77792 <https://reviews.llvm.org/D77792>.

What about changing the EXPENSIVE_CHECKS <https://github.com/llvm/llvm-project/blob/d70ec366c91b2a5fc6334e6f6ca9c4d9a6785c5e/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h#L99-L101> in the assume function in the following way:
Convert all range constraints into a Z3 model and check if that is `UNSAT`.
In that case, we would have returned a state with contradictions, so we would prevent this particular bug from lurking around to bite us later.

And another possibility could be to create a debug checker, which registers to the assume callback and does the same conversion and check.
This is more appealing to me in some way, like decouples the Z3 dependency from the `ConstraintManager` header.

Which approach should I prefer? @NoQ @vsavchenko @martong @xazax.hun @Szelethus


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D88019