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

[Dan Liew via Phabricator via cfe-commits]

delcypher added inline comments.


================
Comment at: CMakeLists.txt:188
 
+find_package(Z3 4.5)
+
----------------
@ddcc It is of course up to you but I recently [[ added support for using `libz3` directly | added support for using `libz3` directly ]] from CMake. via it's own CMake config package. You only get this if Z3 was built with CMake so you might not want this restriction.  This feature has only just landed though and might not be sufficient for your needs.  If you take a look at Z3's example projects they are now built with this mechanism when building with CMake.

If you are interested I'd be more than happy to work with you to get this feature ready for your needs in upstream Z3 so you can use it here.


================
Comment at: include/clang/Config/config.h.cmake:42
+/* Define if we have z3 and want to build it */
+#cmakedefine CLANG_ANALYZER_WITH_Z3 ${CLANG_ANALYZER_WITH_Z3}
+
----------------
Do you really want such a specific name? How about `CLANG_ANALYSER_HAS_SMT_SOLVER`?


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:70
+public:
+  static Z3_context ZC;
+
----------------
@ddc
This decision of having a global context might come back to bite you. Especially if you switch to doing parallel solving in the future. This is why KLEE's `Z3ASTHandle` and `Z3SortHandle` store the context so it's possible to use different context.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:81
+
+class Z3Expr {
+  friend class Z3Model;
----------------
@ddcc 
[[ https://github.com/klee/klee/blob/1f13e9dbf9db2095b6612a47717c2b86e4aaba72/lib/Solver/Z3Builder.h#L20 | In KLEE I have something similar to represent Z3Expr ]] called Z3ASTHandle and Z3SortHandle for doing manual reference counting. You might want to take a look at. I don't see you doing reference counting on sorts here so I think you might be leaking memory.

We also have a handy `dump()` method on `Z3ASTHandle` and `Z3SortHandle` for debugging.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:113
+  // Determine whether two float semantics are equivalent
+  static bool areEquivalent(const llvm::fltSemantics &LHS,
+                            const llvm::fltSemantics &RHS) {
----------------
@ddcc Of course this is fine for now but I think we really need to fix the APFloat API. I use it heavily myself and I've come across problems with it such as this one.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:160
+      return llvm::APFloat::IEEEdouble();
+    case 128:
+      return llvm::APFloat::IEEEquad();
----------------
128 is actually ambiguous. It could also be `ppc_fp128`. I had the same problem in KLEE and for now I just assumed IEEEQuad like you have done but at the very least we should leave a comment here noting that this should be fixed some how.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:438
+    // Logical operators
+    case BO_LAnd: {
+      Z3_ast Args[] = {LHS.AST, RHS.AST};
----------------
@ddcc Isn't this repeating some of the logic in `fromBinOp()`?


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:559
+      Float.toString(Chars, 0, 0);
+      AST = Z3_mk_numeral(Z3Context::ZC, Chars.c_str(), Sort);
+      break;
----------------
@ddcc I'm not convinced this is a good idea. Printing as a decimal string could lead to rounding errors. I think you're better of getting an APInt from the APFloat, constructing a bitvector constant from those bits and then using `Z3_mk_fpa_to_fp_bv()` to get a Z3Expr of the right sort. That was we are being bit-wise accurate.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:581
+  /// Construct an APFloat from a Z3Expr, given the AST representation
+  static bool toAPFloat(const Z3_sort &Sort, const Z3_ast &AST,
+                        llvm::APFloat &Float, bool useSemantics = true) {
----------------
@ddcc Again I don't think the use of strings here is a good idea. You can do this in a bit-precise way by getting the bits, making an APInt from that and then making an APFloat from that.


https://reviews.llvm.org/D28952