[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#4414771 <https://reviews.llvm.org/D152732#4414771>, @xazax.hun wrote:

> In D152732#4414707 <https://reviews.llvm.org/D152732#4414707>, @ymandel wrote:
>
>> Ultimately what matters for a user is the global limit.
>
> I am not 100% sure about that. While it is true that the user cares about the process not hanging, but global vs local limits can have observable effects on the analysis results. With a global limit, after a query exhausted all the budget, for all intents and purposes we continue the analysis without a solver for the rest of the function and all queries would just time out, even the simple ones. With a local limit, the solver might time out for a couple of queries, but we keep the precision for the simple queries. That being said, it is possible that the scenario where we have a few big queries that blows the solver up but the rest of them are simple just does not happen that much. Also, a local timeout produces less reliable worst case runtime results. This makes me think it might be possible that we want both, but this decision is probably better made when we have some evidence that we actually need both. So, I am ok with committing this as is for now.

Great! Yes, I think you're right that having both is probably the ideal solution. Let's start here, but that will be an easy step if and when we need it.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D152732