[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

> Regarding incremental solving with Z3 (or with most SMT solvers in general), let me just lower the expectations a bit: <snip>

Ok, that is good to know. It seems that the performance benefits of incremental solving are unclear, and would be nontrivial to implement (maybe store the states in a DAG, then pop back to the lowest common ancestor from the previous state, and push down to the new state).

> The improvement here (200s vs. 250s) makes me think that some form of caching/incrementalization could pay off.

I'm optimistic that implementing a SMT query cache would significantly improve performance (for both constraint managers), but the current version of that patch has some memory-safety problems (since ProgramStateRef is a reference-counting pointer), and I currently don't have the time to fix it up.

> We could add a new lit substitution '%clang_cc1_analyze' that expands to '%clang_cc1 -analyze -analyzer-constraints=foo -DANALYZER_HAS_CONSTRAINT_MANAGER_FOO" and change the analyzer tests to use it.

I've updated the current version of this diff to use this approach, though there are still the two remaining testcase failures mentioned earlier that I'm not sure how to handle. I also had to remove the argument `-fsyntax-only` in some testcases, because the argument seems to need to appear before `-analyze` (which isn't possible using the substitution-based approach), though it doesn't seem to affect the outcome of the testcase. However, I haven't been able to figure out how to get llvm-lit to execute the same statement twice with different substitutions. From lit.cfg, it seems that I can only define additional substitutions, and not execute a test multiple times. I'm not familiar with the test infrastructure, do you have any suggestions?


https://reviews.llvm.org/D28952