[PATCH] D75698: [analyzer][WIP] Suppress bug reports where a tracked expression's latest value change was a result of an invalidation

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

In D75698#1914102 <https://reviews.llvm.org/D75698#1914102>, @martong wrote:

> > P.S. So, like, we could try to emit the warning only if we covered enough execution paths to prove that there's either dead code or the warning is true. Then we would no longer care about invalidation problems. Unfortunately, i don't have any specific suggestion of how to prove such facts for an arbitrary CFG.
>
> If I understand you correctly, this would mean that we have to reason about all possible execution paths at the same time to do this. Actually, that would be possible only with some kind of a fix-point flow-analysis and clearly the symbolic execution we have in CSA is a completely different beast (it reasons about one path where there is a bug).


Nah, we just need to cover *enough* paths, not *all* paths. Just take all paths on which we've managed to find a particular bug (we keep track of these paths during de-duplicating anyway) and somehow figure out that it's "enough" paths. The point is to prove that there's dead code if all of these paths are infeasible. I.e., it may require an auxiliary CFG-based analysis that'll reason about all possible execution paths, but it doesn't require us to have much interaction between that analysis and our usual symbolic execution. We already have such auxiliary analysis, eg. see how dead symbol elimination is an all-paths problem and `RelaxedLiveVariables` analysis is helping us out with it.

See also my old little essay on this subject <http://lists.llvm.org/pipermail/cfe-dev/2018-October/059863.html>. I was talking about it in the context of path note generation but the problem is roughly the same here.

I know this is vague but i spent some time trying to come up with an actual solution and failed so far, so take it with a grain of salt^^

>> P.P.S. Actually you know what, maybe we should only drop the report if the constraint over the invalidated value contradicts the constraint over the old value. That'll make things a bit more complicated and will require a visitor indeed, though hopefully not as complicated as concrete value tracking, as we're still interested in only one region at a time.
> 
> How would that be different than proving the feasibility of the path with Z3? Could we reuse Mikhail's work here, or that would be overkill for this task?

This problem is fairly orthogonal to constraint solving. It's about providing constraints, not solving them. Like, we have two different values that we previously thought of as separate, now we're telling the solver that they're, emm, maybe slightly less separate, "hey dude, actually, on second thought, can you please take a look at what would have happened if they were actually equal?". We still don't care how exactly does the solver solve this.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D75698