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

Dominic Chen via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Tue Feb 7 14:14:51 PST 2017


ddcc added a comment.

I added support for a callback field in lit's configuration (see https://reviews.llvm.org/D29684), which is used to execute each testcase for each supported constraint solver backends at runtime. I believe this resolves all remaining issues, except for the remaining two testcase failures:

1. 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. Unless anyone objects, I plan to modify this testcase so that this result is fine for the z3 solver backend.
2. 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. Likewise, unless anyone objects, I plan to whitelist this result for the z3 solver backend.


https://reviews.llvm.org/D28952





More information about the cfe-commits mailing list