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

[Dan Liew via Phabricator via cfe-commits]

delcypher added inline comments.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:674
+      // are the same size.
+      Z3_get_numeral_uint64(Z3Context::ZC, AST,
+                            reinterpret_cast<__uint64 *>(&Value));
----------------
ddcc wrote:
> The only problem I see now is that if a IEEEquad is fed in, it will generate a 128-bit bitvector, which will be truncated at this point. But the z3 API doesn't support retrieving a rational into anything larger than 64-bit, so perhaps converting it to string is the way to go here.
@ddcc I'm heavily against using the string method due to rounding problems it might introduce. The trick to handling types wider than 64 bits is to construct a new Z3_ast that does an `Z3_mk_extract()` to pull out the bits you want and then call `Z3_get_numeral_uint64()` on that. In the case of IEEE-754 quad you would need to pull out the lower order bits and then the higher order bits, then put these into an array and build an `APInt` from that.


https://reviews.llvm.org/D28952