[PATCH] D80117: [analyzer] Introduce reasoning about symbolic remainder operator

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

In D80117#2059567 <https://reviews.llvm.org/D80117#2059567>, @NoQ wrote:

> > I believe that as of now we can submit these modifications as is and explore performance optimizations later if needed.
>
> I still encourage you to explore the tests we have from our previous attempts to simplify expressions recursively without memoization (`test/Analysis/hangs.c`). I'm asking because these aren't all that artificial: this kind of code was previously reported by a frustrated user as "the analyzer started hanging on my code". Like, please replace a bunch of `+`es with `&`/`|`/`%` and see if this causes your code to perform exponentially over the size of the program. If so, i'd rather have us hurry up and implement memoization.


Ok, looks like my memories on this subject are heavily messed up. The actual problem that made us hang was solved by D47155 <https://reviews.llvm.org/D47155>. This is a dumb bug that would have been avoided if we had memoization but it doesn't require memoization to be avoided and it doesn't look like this code risks repeating that mistake.

Then, our experience with memoization in D47402 <https://reviews.llvm.org/D47402> wasn't as good as i expected; it turned out that there are other exponential parts of the analysis in such cases that we still couldn't avoid. We should probably still do it (given how difficult it is now to identify these "other parts" that are exponential, i'd rather not add more such parts consciously) but i guess it's not that much of a blocker.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D80117