[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend
Devin Coughlin via Phabricator via cfe-commits
cfe-commits at lists.llvm.org
Fri Feb 24 14:56:14 PST 2017
dcoughlin accepted this revision.
dcoughlin added a comment.
This revision is now accepted and ready to land.
Dominic, this (https://reviews.llvm.org/D28952) and https://reviews.llvm.org/D26061 look get to me! Let's get these two committed! We'd like to get to a place where in-tree incremental development can be done on the Z3 constraint manager.
On my machine total Analysis test time increases from 25s to 90s when the Z3 tests are enabled using a static Z3 library. Testing time when Z3 is not enabled does not change measurably.
Here's how I suggest staging these in. Please give the bots time to settle after each commit.
1. Apply the refactoring changes from https://reviews.llvm.org/D26061. This is NFC (no functional change).
2. Split out the test changes from https://reviews.llvm.org/D28952. This would change the tests to use 'clang_analyze_cc1' and change the lit.cfg to add a normal substitution for it. (But not call the analyzer twice). This is also NFC.
3. Add the new constraint solver and the lit/CMake changes for for the rest of https://reviews.llvm.org/D28952.
This will separate the stuff that is unlikely to break from the build system changes, which might need to be reverted quickly.
Once this is done, we (I) will add a bot that automatically runs the Z3 tests to make sure we catch regressions that affect the Z3 solver.
With the bot in place we will review https://reviews.llvm.org/D28953, https://reviews.llvm.org/D28954, and https://reviews.llvm.org/D28955 separately.
Does that sound good to you?
https://reviews.llvm.org/D28952
More information about the cfe-commits
mailing list