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

[Anna Zaks via Phabricator via cfe-commits]

zaks.anna added a comment.

Thanks for working on this Dominic!!!

Can you talk a bit about your motivation for working on this project and what your goals are?

Have you compared the performance when using Z3 vs the current builtin solver? I saw that you mention performance issues on large codebases, but could you give some specific numbers of the tradeoffs between performance, code coverage, and the quality of reported bugs. (One very rough idea to use a stronger solver while still keeping the analyzer performant would be to only use it for false positive refutation.)

> I looked around for a generic smt-lib interface earlier, but couldn't find much available, and since I wanted floating-point arithmetic support, I ended up just directly using the Z3 C interface (the C++ interface uses exceptions, which causes problems). As far as I know, CVC4 doesn't have built-in floating-point support. But longer term, I'd  agree that this backend should be made more generic.

Ok. Though I'd love to see an interface that supports CVC4!

> Another issue is that some testcases will have different results depending on the constraint manager in use, but I don't believe it's possible to change the expected  testcase output based on the presence of a feature flag. Unless this changes, there'll need to be (mostly) duplicate testcases for each constraint manager.

How different the results are? Is it the case that you get more warnings with Z3 in most cases? Would it be possible to divide the tests into the ones that work similarly with both solvers and the ones that are only expected to report warnings with Z3? I know this won't work in general, but might be much cleaner than polluting every test with a ton of #ifdefs.

> Furthermore, this and the child patches will cause the static analyzer to generate more complex constraints at runtime. But, I'm not sure if just having RangeConstraintManager ignore unsupported constraints will be sufficient, from a performance and correctness perspective.

This is probably the most important question to answer. Maintaining the performance and correctness of the analyzer mode that is using RangeConstraintManager is very important as this is the mode most users will use at least for a while.

> My personal preference would be to directly merge in this constraint manager without using the plugin approach, because it would simplify some of the testing and changes to the build system (e.g. the APFloat linking issue). But I'm not sure if this would be ok?

Most likely that would be possible.

I'd also like to second Ryan's suggestion to look at his patch to add support for STP. It was very close to landing other than some build system integration issues.


https://reviews.llvm.org/D28952