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

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

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

> 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

I like the second approach, i.e. to have a debug checker. But I don't see, how would this checker validate all constraints at the moment when they are added to the State. And if we don't check all constraints then we might end up checking a state that is invalid for a while (i.e. that might became invalid previously and not because of the lastly added constraint.) So, essentially, my gut feeling is that both approaches should be validating all newly added constraints against Z3. And that might be too slow, it would have the same speed as using z3 instead of the range based solver.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D88019