ddcc added inline comments.
================
Comment at: cmake/modules/FindZ3.cmake:3
+# in the find_path() and find_library() calls
+find_package(PkgConfig QUIET)
+PKG_CHECK_MODULES(PC_Z3 QUIET libz3)
----------------
delcypher wrote:
> @ddcc Seeing as you don't want to use the new upstream Z3 CMake package
> config files I'll try to review this.
>
> Upstream Z3 does not come with pkg-config files for the native library so I'm
> wondering where you expect this to work. Does a Linux distro add their own
> `.pc` files?
>
> It looks like you only use these paths as hints so this so this looks like
> it'll work even without the pkg-config files.
See below.
================
Comment at: cmake/modules/FindZ3.cmake:5
+PKG_CHECK_MODULES(PC_Z3 QUIET libz3)
+set(Z3_DEFINITIONS ${PC_LIBZ3_CFLAGS_OTHER})
+
----------------
delcypher wrote:
> @ddcc This CMake variable is set but never used. Also based on the name it
> suggests that they are compiler definitions rather than other compiler flags.
> Does `_CFLAGS_OTHER` have those semantics? It's unclear from
> https://cmake.org/cmake/help/v3.7/module/FindPkgConfig.html#command:pkg_check_modules
> what they are supposed to be.
>
> To consume these flags you could add `target_compile_definitions()` and
> `target_compile_options()` to all users of Z3. A more elegant way of doing
> this is to create an imported library target (e.g. `z3::libz3`) and set
> compile definitions, compile options and include directories on this imported
> target with `INTERFACE` visibility so that these usage requirements
> implicitly propagate to all users of `z3::libz3`.
I'm not very familiar with CMake, so I based it off of the FindLibXml2.cmake
from the upstream CMake repository. The `pkg-config` part isn't used currently,
but I left it in case z3 does get a proper package.
================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:619
+
+ llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), true);
+ Z3Expr Z3Int = Z3Expr::fromAPSInt(Int);
----------------
delcypher wrote:
> @ddcc Why use APSInt here? Why not APInt, we are looking at raw bits and
> don't want to interpret the most significant bit in a special way.
Since the rest of the code already handles `APSInt`, I just reused that instead
of implementing another method for `APInt`. The overhead is one additional bool
used to store the sign, which doesn't make much difference, since it needs to
be specified anyway with `APInt::toString*()`.
================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:668
+ default:
+ llvm_unreachable("Unsupported sort to integer!");
+ case Z3_BV_SORT: {
----------------
delcypher wrote:
> Is `Z3_FLOATING_POINT_SORT` possible in your implementation?
I don't think so. Things change around a bit with D28954, but by the time this
method is called, the casting should have already been handled elsewhere.
================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:674
+ // are the same size.
+ Z3_get_numeral_uint64(Z3Context::ZC, AST,
+ reinterpret_cast<__uint64 *>(&Value));
----------------
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.
https://reviews.llvm.org/D28952
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
