[analyzer] Improved cmake configuration for Z3

[esteffin]

Summary

Enhanced support for Z3 in the cmake configuration of clang; now it is possible to specify any arbitrary Z3 install prefix (CLANG_ANALYZER_Z3_PREFIX) to cmake with lib (or bin) and include folders. Before the patch only in cmake default locations
were searched (https://cmake.org/cmake/help/v3.4/command/find_path.html).

Specifying any CLANG_ANALYZER_Z3_PREFIX will force also CLANG_ANALYZER_BUILD_Z3 to ON.

Removed also Z3 4.5 version requirement since it was not checked, and now Clang works with Z3 4.7

[george.karpenkov]

CMakeLists.txt

402

I don't understand the semantics of this flag. Clang CMake is not building Z3, so why do we have a flag called BUILD_Z3? And the description seems incorrect as well.

407

I think we need to version lock, since we don't know whether new versions would have the same API.

cmake/modules/FindZ3.cmake

9

I'm pretty sure we shouldn't search in global directories. That can cause a lot of unexpected issues.

[ddcc]

CMakeLists.txt

402

The naming is a bit inaccurate, CLANG_ANALYZER_BUILD_Z3 indicates that the static analyzer should be built with support for the Z3 constraint manager.

406–407

Why is this changed? Doesn't the above force the CLANG_ANALYZER_BUILD_Z3 variable already if CLANG_ANALYZER_Z3_PREFIX is set?

407

Yeah, although the C API is considered to be fairly stable, it looks like a bunch of types have changed around recently. As of Z3 4.8.0, they've moved to stdbool.h and stdint.h, so I believe there's a couple of reinterpret_cast that can be removed from the code now. It looks like Z3_bool is also now typedef'd to a bool instead of an int. The configuration options can also be bit unstable, and my impression is that they've changed around over time.

FYI @mikhail.ramalho @george.karpenkov It looks like Z3 4.8.0 has added support for parallel solving (parallel.enable=true), among other changes and improvements. Might be worth testing to see if using Z3 for refutation/constraint solving is faster, and if not, report any regressions upstream.

cmake/modules/FindZ3.cmake

9

Yeah. It also looks like Z3 4.8.0 has finally integrated a CMake-based build system, so it'd be best to integrate with that.

[esteffin]

CMakeLists.txt

407

For the version we can either choose to have at minimum required version (4.5 before), or to lock it to a specific one.
In any case I suggest to use a stable release as reference (version <= 4.7.1).

Unfortunately in cmake 3.4.3 I did not find a standard way to require a maximum version, nor it is possible specify an ordering on possible version like closest to or latest (No attempt is made to choose a highest or closest version number), so specifying a range of versions will be pretty hard and dangerous.

In conclusion I think that locking it would be the best available solution for now.

[mikhail.ramalho]

Yeah, although the C API is considered to be fairly stable, it looks like a bunch of types have changed around recently. As of Z3 4.8.0, they've moved to stdbool.h and stdint.h, so I believe there's a couple of reinterpret_cast that can be removed from the code now. It looks like Z3_bool is also now typedef'd to a bool instead of an int. The configuration options can also be bit unstable, and my impression is that they've changed around over time.

Although I'm always in favor of supporting the latest changes, I think we should wait for a proper release before updating the code (specially because Z3 seems to be released only once a year and a lot of things can change between releases).

Yeah. It also looks like Z3 4.8.0 has finally integrated a CMake-based build system, so it'd be best to integrate with that.

This seems to be part of the release 4.7.1 as well. @esteffin, can we use that instead?

FYI @mikhail.ramalho @george.karpenkov It looks like Z3 4.8.0 has added support for parallel solving (parallel.enable=true), among other changes and improvements. Might be worth testing to see if using Z3 for refutation/constraint solving is faster, and if not, report any regressions upstream.

That's interesting! I'll run some experiments with that.

[esteffin]

CMakeLists.txt

402

I was really tempted to completely remove the CLANG_ANALYZER_BUILD_Z3 flag and build the support for Z3 only if a valid CLANG_ANALYZER_Z3_PREFIX was given. This will be similar to the autotools way of configuring optional dependencies (--with-dependency).

However I decided to limit the changes to the bare minimum.

Removing the CLANG_ANALYZER_BUILD_Z3 flag will simplify the FindZ3.cmake script since we do not need to look for different locations than the prefix one.

cmake/modules/FindZ3.cmake

9

Using the auto-generated Z3Config.cmake, Z3Targets.cmake and Z3Targets-<configuration>.cmake will solve many problems such as the automatic addition of extra compiler flags required when linking against static libz3.a (-fopenmp and -lpthread).
However I really think that using it is not a good idea since:

• At the moment (version 4.7.1) Z3 does not export its version,
• even if Z3 is auto-exported at build time since version 4.6, Z3Config.cmake, Z3Target.cmake and Z3Target-<configuration>.cmake have never been added to any pre-built release,
• the 3 exported files should be registered in cmake user/system wide configuration to work automatically. This is usually done at install time, but if we get only the binary release there is no registration requiring to provide the prefix,
• Z3 export only one library: z3::libz3. If Z3 is compiled statically the exported target will point to libz3.a, while if it is shared to libz3.so.4.*. If both are present only one library will be found (the last to be installed), forcing only static/shared linkage. (This is a more general cmake limitation)

For the aforementioned reasons I suggest not to change to the way find_package(Z3) works to the new auto-exported one.

[delcypher]

CMakeLists.txt

399

Nit. Rename this something like CLANG_ANALYZER_Z3_INSTALL_PREFIX. The description is also not very accurate

• Again this is an install prefix, just saying prefix is too vague.
• Z3 is a constraint solver, not a constraint manager.
• builds the static analyzer? I presume you mean this option being on implies the static analyzer is built? Maybe say Implies CLANG_ANALYZER_BUILD_Z3?

402

I'm not a big fan of this. My preferred style in CMake of handling optional dependencies is to do something like

find_package(Z3)
# Assume for this example that this sets Z3_AVAILABLE

set(CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT "${Z3_AVAILABLE}")
option(CLANG_ANALYZER_ENABLE_Z3_SOLVER
  "Enable Support for the Z3 constraint solver in the Clang Static Analyzer"
  ${CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT}
)

if (CLANG_ANALYZER_ENABLE_Z3_SOLVER)
  if (NOT Z3_AVAILABLE)
    message(FATAL_ERROR "CLANG_ANALYZER_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available")
  endif()
  # Do stuff to enable Z3 use in the build...
endif()

The advantages of the sketch above is that

• On first configure if Z3 is available we'll use it if it's available. If it's not available on first configure the feature is not enabled.
• The code to detect Z3 is always run which means we'll know if it's broken.
• The user can switch support for Z3 on/off using the CLANG_ANALYZER_ENABLE_Z3_SOLVER option on first configure or in later configures and the request will be respected.

cmake/modules/FindZ3.cmake

9

@esteffin Author of the Z3 CMake build system here.

If you'd like to see example of how to use Z3's CMake Config package take a look at.

https://github.com/Z3Prover/z3/blob/master/examples/c%2B%2B/CMakeLists.txt

At the moment (version 4.7.1) Z3 does not export its version,

Yep. There's a TODO about this at

https://github.com/Z3Prover/z3/blob/12f9336fec018b092af57ef4db330842b7394f24/CMakeLists.txt#L653

I never implemented that because I was always using Z3's bleeding edge master branch. I'm sure the Z3 dev's would happily take a patch if you want to implement this.

even if Z3 is auto-exported at build time since version 4.6, Z3Config.cmake, Z3Target.cmake and Z3Target-<configuration>.cmake have never been added to any pre-built release,

This is because those doing the releases still insist on using the old build system. The main missing piece preventing everyone from switching to the CMake build system is the lack of support for generating OCaml bindings. Someone started this https://github.com/Z3Prover/z3/pull/1666 but it isn't really finished.

the 3 exported files should be registered in cmake user/system wide configuration to work automatically. This is usually done at install time, but if we get only the binary release there is no registration requiring to provide the prefix,

For that particular case what you have to do is pass -DZ3_DIR=<path_to_dir_containing_Z3Config.cmake> when CMake. This is very similar your to CLANG_ANALYZER_Z3_PREFIX but is much more standard because it's using standard CMake mechanisms.

Z3 export only one library: z3::libz3. If Z3 is compiled statically the exported target will point to libz3.a, while if it is shared to libz3.so.4.*. If both are present only one library will be found (the last to be installed), forcing only static/shared linkage. (This is a more general cmake limitation)

This is certainly true. Z3's current CMake build system can't do a shared and static build at the same time. Technically it would be possible to change things so the library gets built twice but I'm not convinced its worth the effort.

For the aforementioned reasons I suggest not to change to the way find_package(Z3) works to the new auto-exported one.

I would like to see people use the Z3 CMake config package I wrote but I understand that if your goal is broadest compatibility then we have to use the existing approach because that works with Z3 built with either build system.

[mikhail.ramalho]

Nit. Rename this something like CLANG_ANALYZER_Z3_INSTALL_PREFIX. The

description is also not very accurate

• Again this is an install prefix, just saying prefix is too vague.
• Z3 is a constraint solver, not a constraint manager.
• builds the static analyzer? I presume you mean this option being on

implies the static analyzer is built? Maybe say `Implies
CLANG_ANALYZER_BUILD_Z3`?

Prefix is the location where Z3 is installed on the machine. You can see
it's used in FindZ3.cmake:

${CLANG_ANALYZER_Z3_PREFIX}/include
${CLANG_ANALYZER_Z3_PREFIX}/lib

But I can see how it's confusing. How about CLANG_ANALYZER_Z3_DIR?

I would like to see people use the Z3 CMake config package I wrote but I
understand that if your goal is broadest compatibility then we have to use
the existing approach because that works with Z3 built with either build
system.

Indeed, the reason we are trying to improve the cmake script is that it'll
be used for the other SMT solver implementations we'll submit for review
soon.

[george.karpenkov]

@delcypher @ddcc @mikhail.ramalho Actually, I was thinking about another way of configuring Z3 without CMake entirely, and I would like to hear thoughts on how crazy that is.
What if we

• Remove all CMake checks
• Define the headers we need in the analyzer
• When initializing Z3 objects (done when Z3-visitor or Z3-solver is enabled), we would try to open the dylib, check it's version, and fail if the dylib is not found or the version does not match.

This is less clean, but would give us a humongous advantage of just being able to drop Z3 dylib into a resource directory (or modifying the Clang rpath) in order to enable Z3,
with no recompilation needed.
This would be a huge benefit for those who don't recompile the compiler regularly.

[ddcc]

In D50818#1206202, @george.karpenkov wrote:

@delcypher @ddcc @mikhail.ramalho Actually, I was thinking about another way of configuring Z3 without CMake entirely, and I would like to hear thoughts on how crazy that is.
What if we

• Remove all CMake checks
• Define the headers we need in the analyzer
• When initializing Z3 objects (done when Z3-visitor or Z3-solver is enabled), we would try to open the dylib, check it's version, and fail if the dylib is not found or the version does not match.

Sounds good to me, it'd make it a lot easier for end-users to test SMT solving functionality. Only caveat is that it'd need some careful testing; I'm not sure how amenable Z3 is to being dynamically loaded, whether there are any conflicting symbol names, etc.

[delcypher]

In D50818#1206202, @george.karpenkov wrote:

@delcypher @ddcc @mikhail.ramalho Actually, I was thinking about another way of configuring Z3 without CMake entirely, and I would like to hear thoughts on how crazy that is.
What if we

• Remove all CMake checks
• Define the headers we need in the analyzer
• When initializing Z3 objects (done when Z3-visitor or Z3-solver is enabled), we would try to open the dylib, check it's version, and fail if the dylib is not found or the version does not match.

This is less clean, but would give us a humongous advantage of just being able to drop Z3 dylib into a resource directory (or modifying the Clang rpath) in order to enable Z3,
with no recompilation needed.
This would be a huge benefit for those who don't recompile the compiler regularly.

I'm not opposed to supporting dynamically loading Z3 as a shared library but I think

• We have to be version locked due to Z3 sometimes changing its API/ABI. When we dlopen the library the first thing we should do is call the functions that give the version and reject a Z3 library that isn't the version we're locked against.
• We should still support building directly against Z3. This would be useful for developers when experimenting with migrating from one Z3 version to another. This means keeping the CMake code around for this use case. Given that the use case if only for developers I'd advocate switching to the find_package(Z3 CONFIG) approach which requires that Z3 was built with CMake. This will make the CMake side of supporting this configuration in the analyzer as simple as possible.
• We need to have very clear documentation on how to use Z3 library with the analyzer, i.e. how to obtain Z3, how to set up the environment so that the analyzer can use it, and how to know if Z3 is being used for analysis.
• We will have to incorporate Z3's public API headers into the analyzer's code base in order to work with Is that okay from a licensing perspective?
• What mechanism do you want to use for calling Z3 functions? If we mark the Z3 functions as weak in our headers and call them directly we still have to pass all the symbol names to the darwin linker (-U<symbol_name>) in order for it to be happy.

cmake/modules/FindZ3.cmake

9

@esteffin

At the moment (version 4.7.1) Z3 does not export its version,

Oops. Actually the version information is exported (e.g. Z3_VERSION_MAJOR, Z3_VERSION_MINOR, Z3_VERSION_STRING)

See.

https://github.com/Z3Prover/z3/blob/master/cmake/Z3Config.cmake.in

The thing I was referring to was the CMake code that automatically decides if a requested Z3 version is compatible with a found version.

[esteffin]

In D50818#1206202, @george.karpenkov wrote:

@delcypher @ddcc @mikhail.ramalho Actually, I was thinking about another way of configuring Z3 without CMake entirely, and I would like to hear thoughts on how crazy that is.
What if we

• Remove all CMake checks
• Define the headers we need in the analyzer
• When initializing Z3 objects (done when Z3-visitor or Z3-solver is enabled), we would try to open the dylib, check it's version, and fail if the dylib is not found or the version does not match.

This is less clean, but would give us a humongous advantage of just being able to drop Z3 dylib into a resource directory (or modifying the Clang rpath) in order to enable Z3,
with no recompilation needed.
This would be a huge benefit for those who don't recompile the compiler regularly.

I think this is an interesting idea, especially for removing the dependency to Z3 and I agree it will allow usage of it to many user not recompiling it often (and allowing the binaries to enable it).

However this is far beyond the aim of this patch. Indeed as stated before by @mikhail.ramalho

Indeed, the reason we are trying to improve the cmake script is that it'll be used for the other SMT solver implementations we'll submit for review soon.

this patch is to improve the current cmake script when Z3 is used, and to be used for other SMT solver implementations. For this reason I propose to postpone the suggested approach to a separate patch.

CMakeLists.txt

402

Definitely agree that this will be the way. Adding to new patch.

407

Fixing to version 4.7.1 (latest stable)

cmake/modules/FindZ3.cmake

9

As stated before I think that using the cmake-generated config script for Z3 will give us many benefits such as automatic addition of Z3 dependencies (such as GMP when used) and management of extra compilation flags.

However I strongly suggest not to use it until it will be shipped to the binary release of Z3. Asking people to compile Z3 (when the binaries are released online) will reduce the number of people using such feature.

When Z3Config.cmake will be added to the binary release it will definitely be the case to migrate to it.

[esteffin]

Improved and changed the proposed patch accordingly to the comment.

Version 4.7.1 is now checked

Z3 is searched in CLANG_ANALYZER_Z3_INSTALL_DIR first and then in the default paths.

Error are raised if Z3 is required and not found, or if it is specified an invalid installation directory.

[esteffin]

Ping...

[esteffin]

Final patch ready to be applied

CMakeLists.txt

 add_definitions( -D_GNU_SOURCE )
 
 option(CLANG_BUILD_TOOLS
   "Build the Clang tools. If OFF, just generate build targets." ON)
 
 option(CLANG_ENABLE_ARCMT "Build ARCMT." ON)
 option(CLANG_ENABLE_STATIC_ANALYZER "Build static analyzer." ON)
 
-option(CLANG_ANALYZER_BUILD_Z3
-  "Build the static analyzer with the Z3 constraint manager." OFF)
+set(CLANG_ANALYZER_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 solver.")
 
-option(CLANG_ENABLE_PROTO_FUZZER "Build Clang protobuf fuzzer." OFF)
+find_package(Z3 4.7.1 EXACT)
 
-if(NOT CLANG_ENABLE_STATIC_ANALYZER AND (CLANG_ENABLE_ARCMT OR CLANG_ANALYZER_BUILD_Z3))
-  message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT or Z3")
+if (CLANG_ANALYZER_Z3_INSTALL_DIR)
+  if (NOT Z3_FOUND)
+    message(FATAL_ERROR "Z3 4.7.1 has not been found in CLANG_ANALYZER_Z3_INSTALL_DIR: ${CLANG_ANALYZER_Z3_INSTALL_DIR}.")
+  endif()
+endif()
+
+set(CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}")
+
+option(CLANG_ANALYZER_ENABLE_Z3_SOLVER
+  "Enable Support for the Z3 constraint solver in the Clang Static Analyzer."
+  ${CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT}
+)
+
+if (CLANG_ANALYZER_ENABLE_Z3_SOLVER)
+  if (NOT Z3_FOUND)
+    message(FATAL_ERROR "CLANG_ANALYZER_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.")
   endif()
 
-if(CLANG_ANALYZER_BUILD_Z3)
-  find_package(Z3 4.5)
-  if(Z3_FOUND)
-    set(CLANG_ANALYZER_WITH_Z3 1)
-  else()
-    message(FATAL_ERROR "Cannot find Z3 header file or shared library")
-  endif()
+
+option(CLANG_ENABLE_PROTO_FUZZER "Build Clang protobuf fuzzer." OFF)
+
+if(NOT CLANG_ENABLE_STATIC_ANALYZER AND (CLANG_ENABLE_ARCMT OR CLANG_ANALYZER_ENABLE_Z3_SOLVER))
+  message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT or Z3")
 endif()
 
 if(CLANG_ENABLE_ARCMT)
   set(CLANG_ENABLE_OBJC_REWRITER ON)
 endif()
 
 # Clang version information
 set(CLANG_EXECUTABLE_VERSION

cmake/modules/FindZ3.cmake

+# Looking for Z3 in CLANG_ANALYZER_Z3_INSTALL_DIR
 find_path(Z3_INCLUDE_DIR NAMES z3.h
+   NO_DEFAULT_PATH
+   PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}/include
    PATH_SUFFIXES libz3 z3
    )
 
 find_library(Z3_LIBRARIES NAMES z3 libz3
+   NO_DEFAULT_PATH
+   PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}
+   PATH_SUFFIXES lib bin
    )
 
-find_program(Z3_EXECUTABLE z3)
+find_program(Z3_EXECUTABLE z3
+   NO_DEFAULT_PATH
+   PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}
+   PATH_SUFFIXES bin
+   )
+
+# If Z3 has not been found in CLANG_ANALYZER_Z3_INSTALL_DIR look in the default directories
+find_path(Z3_INCLUDE_DIR NAMES z3.h
+   PATH_SUFFIXES libz3 z3
+   )
+
+find_library(Z3_LIBRARIES NAMES z3 libz3
+   PATH_SUFFIXES lib bin
+   )
+
+find_program(Z3_EXECUTABLE z3
+   PATH_SUFFIXES bin
+   )
 
-if(Z3_INCLUDE_DIR AND Z3_EXECUTABLE)
+if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE)
     execute_process (COMMAND ${Z3_EXECUTABLE} -version
       OUTPUT_VARIABLE libz3_version_str
       ERROR_QUIET
       OUTPUT_STRIP_TRAILING_WHITESPACE)
 
     string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1"
            Z3_VERSION_STRING "${libz3_version_str}")
     unset(libz3_version_str)

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

 
 #endif
 
 SMTSolverRef clang::ento::CreateZ3Solver() {
 #if CLANG_ANALYZER_WITH_Z3
   return llvm::make_unique<Z3Solver>();
 #else
   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
-                           "with -DCLANG_ANALYZER_BUILD_Z3=ON",
+                           "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
                            false);
   return nullptr;
 #endif
 }
 
 std::unique_ptr<ConstraintManager>
 ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
 #if CLANG_ANALYZER_WITH_Z3
   return llvm::make_unique<Z3ConstraintManager>(Eng, StMgr.getSValBuilder());
 #else
   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
-                           "with -DCLANG_ANALYZER_BUILD_Z3=ON",
+                           "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
                            false);
   return nullptr;
 #endif
 }