[PATCH] D152732: [clang][dataflow] Support limits on the SAT solver to force timeouts.

[Yitzhak Mandelbaum via Phabricator via cfe-commits]

ymandel added a comment.

In D152732#4414661 <https://reviews.llvm.org/D152732#4414661>, @xazax.hun wrote:

> Huge +1, I think most solvers need to have some resource limits in place as the runtime can explode. I am just not 100% what is the best approach here, putting a global limit on the solver instance vs having a limit per query. Any thoughts on that?

Excellent question. Ultimately what matters for a user is the global limit. So, in that sense, a global limit makes sense. But, it also makes it harder (in principle) to pinpoint the problem, because you could have it timeout on a small query right after a large query that was actually responsible for consuming the resources. That said, I'm guessing in practice it's binary, because of the exponential: either a single call exhausts all resources or it barely uses them. I suspect we'll ~never hit the case I described. So, I'm inclined to start global (to keep it simple) and then refine if necessary. As you probably noticed, this patch actually has both -- the user specifies the global limit, but the implementation is local. So, changing this would be easy.

That said, I should note that it's not global for a TU - just for a function, at least given the way we currently implement our clang-tidy checks. So, that seems a reasonable compromise.

WDYT?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D152732