[clang] [analyzer][z3] Fix SMTConstraintManager.h removeDeadBindings (PR #215240)

[Donát Nagy via cfe-commits]

NagyDonat wrote:

> > However, note that symbol liveness is used for many things, so this extended lifetime may cause surprising side effects. [...]
> 
> I am not actually extending symbol liveness (as determined by `bool SymReaper::isLive(SymbolRef sym)`) though.

My phrasing was inaccurate, but unfortunately your changes actually influence the leak warnings of checkers like `MallocChecker.cpp` and `StreamChecker.cpp` (in the corner case when your you have constraints about the symbols tracked by those checkers).

> All I am doing here is changing how the constraints are removed by `removeDeadBindings`.

This is slightly inaccurate: you are changing the removal of _symbols_, and not just the removal of constraints. (Of course, when a symbol is removed this way, constraints about it are also removed.) The leak warning checkers register a `check::DeadSymbols` callback to detect the point when a symbol is removed ("marked as dead") and use this opportunity to produce a bug report if the symbol was in an "active/open" state. To preserve the constraints about more symbols, you need to keep those symbols alive, and this means that they will also be alive for the POV of the leak warning checkers.

However, I reiterate that I don't think that this is a blocking issue, because these are rare corner cases and can only produce false negatives (which is always acceptable: the static analyzer is inherently heuristic-based and will always produce many false negatives).

It is probably a good idea to add a comment like "NOTE: This logic keeps more symbols alive than the range-based constraint manager, which may cause false negatives in leak warnings." I think that you shouldn't do more in this commit -- fixing this situation is low priority, and even if you see a good way to do it, it probably belongs in a separate PR.

https://github.com/llvm/llvm-project/pull/215240