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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
