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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
