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

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

Thanks for the feedback! My main constraint is that the results from the floating-point analysis weren't very interesting (see #652894 <#652894>), so I'm not actively working on further development.

> FYI I've been working on floating point support in KLEE and have extended it to support floating point (note however only the Z3 backend actually supports consuming floating point constraints). I've not yet open sourced what I've done as I'm not entirely happy with the design but if there is interest we could see if we could figure out a way of pulling klee::Expr (and the solver bits) out of KLEE to make a standalone library. Note there is a project called metaSMT that uses template meta programming to give the same interface to multiple solvers. KLEE does support it but I'm not familiar with it.

I agree that it'd be useful to move to a more generic SMT interface, potentially SMT-LIB instead of something specific to a solver, but this is more of a long-term goal at the moment.

> KLEE has a few optimization ideas that you could consider implementing that certainly help in the context of symbolic execution...

Likewise, I think adding a constraint cache and implementing performance optimizations would be the next step to getting this enabled by default, and perhaps deprecating the range constraint manager, but the implementation is a little tricky because there's state also being stored in the `ProgramState` object. Since those are reference counted, there's a little more work involved than just adding an intermediate layer with e.g. an `std::map`. But again, it's not something I have the time for at the moment.



================
Comment at: CMakeLists.txt:188
 
+find_package(Z3 4.5)
+
----------------
delcypher wrote:
> delcypher wrote:
> > @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.
> Sorry that URL should be https://github.com/Z3Prover/z3/pull/926
I think this is useful, and upstream z3 has been in need of better packaging. But until it's used by default over the current python script and the z3 folks actively maintain it, I'm a little hesitant to depend on it.


================
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}
+
----------------
delcypher wrote:
> Do you really want such a specific name? How about `CLANG_ANALYSER_HAS_SMT_SOLVER`?
There's been a bit of back and forth over this name in previous revisions, so I'm a little hesitant to change it. In essence, there are two CMake variables, one for whether z3 is present, and another for whether the user requested to build with z3, which are exported to a single C-level definition that is true iff both CMake variables are true.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:70
+public:
+  static Z3_context ZC;
+
----------------
delcypher wrote:
> @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.
I agree that it is an inherent limitation, but since the static analyzer itself is only single-threaded anyway, the entire analyzer will need significant changes before this becomes a problem.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:81
+
+class Z3Expr {
+  friend class Z3Model;
----------------
delcypher wrote:
> @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.
Originally, my understanding was that reference counting wasn't necessary for `Z3_sort` objects, based on the API documentation, and the lack of `Z3_sort_inc_ref()`/`Z3_sort_dec_ref()` functions. But, taking another look at the z3 source code, it seems that `Z3_sort` is casted directly to `Z3_ast`,  so I think this does need to be fixed.


================
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) {
----------------
delcypher wrote:
> @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.
Yeah, both the `APFloat` and `Sema` API's need some work to be more usable from other areas of Clang. This function wasn't originally present in earlier revisions, but at some point the `fltSemantics` definition was changed to only return references, and then this helper became necessary.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:160
+      return llvm::APFloat::IEEEdouble();
+    case 128:
+      return llvm::APFloat::IEEEquad();
----------------
delcypher wrote:
> 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.
This is a common pitfall, but isn't a problem for this function in particular, because `canReasonAbout()` will exclude non-IEEE 754 types, e.g. PPC and 8087 FPU.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:438
+    // Logical operators
+    case BO_LAnd: {
+      Z3_ast Args[] = {LHS.AST, RHS.AST};
----------------
delcypher wrote:
> @ddcc Isn't this repeating some of the logic in `fromBinOp()`?
The cases for `BO_LAnd` and `BO_LOr` are duplicated, but since the two functions handle exclusively floating-point and non floating-point types, the overlap is fairly small.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:559
+      Float.toString(Chars, 0, 0);
+      AST = Z3_mk_numeral(Z3Context::ZC, Chars.c_str(), Sort);
+      break;
----------------
delcypher wrote:
> @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.
>From the comments inside `APFloat::toString()`, this should be precise enough to round-trip from float to string and back again with no loss of precision. However, the I agree that bitcasting makes more sense, especially given the overhead of string conversion.


================
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) {
----------------
delcypher wrote:
> @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.
See above.


https://reviews.llvm.org/D28952