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

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

Do you want me to replace this version of the patch with one that omits the test case changes? The underlying git commit for just the Z3 constraint manager implementation is https://github.com/ddcc/clang/commit/e1414d300882c1459f461424d3e89d1613ecf03c , and https://github.com/ddcc/clang/commit/fb7d558be6492f11a3793f011f364098ddcc9711 is the commit that converts it to a plugin and modifies all the testcases.

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.

I'm not sure what's the easiest way to maintain backwards support with RangeConstraintManager. Right now, I've modified `lit.cfg` to substitute `%z3` and `%z3_cc1` (for `clang` or `clang -cc1`) with the appropriate argument to load the plugin, if the `z3` feature is available. Otherwise, they are substituted with just the empty string. Another approach would be to do this all in `llvm-lit` without modifying the testcases, but then there'd need to be some sort of path-based matching to determine when the argument to load the plugin should be injected (e.g. only for `test/Analysis`). However, if this constraint manager were built into clang instead of as a plugin, then this issue is moot.

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.

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.


https://reviews.llvm.org/D28952