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

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

This is a fairly large patch, but the core of it is the actual implementation of the Z3 constraint solver backend. In its current form, the backend is implemented as a Clang plugin,  but I also have a git commit that has it inside the static analyzer. The non-plugin approach makes testing easier, by avoiding the introduction of new `%z3` and %z3_cc1` variables in `lit.cfg` and modifying all the testcases to load in the Z3 constraint manager plugin.

1. The testcase `Analysis/unsupported-types.c` currently fails, because when using the constraint manager as a Clang plugin, somehow a copy of `llvm::APFloat` is getting compiled into the shared library. Thus, comparisons of `&TI.getLongDoubleFormat()` against `&llvm::APFloat::x87DoubleExtended()` or `&llvm::APFloat::PPCDoubleDouble()` are always failing, which causes a subsequent assertion error. When testing the non-plugin implementation, it works fine.
2. The testcase `Analysis/reference.cpp` currently fails, because the `RangeConstraintManager` has an internal optimization that assumes references are known to be non-zero (see RangeConstraintManager.cpp:422). This optimization is probably in the wrong place, and should be moved into the analyzer and out of the constraint solver.
3. The testcase `Analysis/ptr-arith.c` currently fails, because handling of `ptrdiff_t` is somewhat tricky. This constraint manager interface maps `ptrdiff_t` to a signed bitvector in Z3, and pointers to unsigned bitvectors in Z3. However, since this testcase compares the pointer values both directly and indirectly via `ptrdiff_t`, if `a < b` is true using a signed comparison, the same is not necessarily true using an unsigned comparison.
4. Because of the divergence in capabilities between this and the existing constraint manager, the follow-up child patches that add support for additional features will probably cause problems for the existing constraint manager. I haven't fully tested that, but there is an issue of how to update the testsuite results without duplicating most of the existing testcases for each constraint manager backend.
5. Since this constraint manager uses Z3, the plugin links against the Z3 shared library. I believe this should be fine since Z3 is under a MIT license, but I'm not really familiar with any licensing issues.
6. This plugin requires Z3 4.5.0 or later. I'm not sure if this is available in any distribution package repositories, so it may be necessary to build from source.


https://reviews.llvm.org/D28952