From b3713e7496eb3a32a7109a5f3b2007b190344644 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 6 Apr 2016 22:47:28 +0100 Subject: [PATCH 01/13] Refactor ``mk_z3consts_java()`` code into ``mk_z3consts_java_internal()`` and move that into ``mk_genfile_common.py``. Then adapt ``mk_util.py`` and ``mk_consts_files.py`` to call into the code at its new location. The purpose of this change is to have Python code common to the Python and CMake build systems separate from Python code that is only used for the Python build system. --- scripts/mk_consts_files.py | 19 ++++++ scripts/mk_genfile_common.py | 110 +++++++++++++++++++++++++++++++++++ scripts/mk_util.py | 106 +++------------------------------ 3 files changed, 137 insertions(+), 98 deletions(-) diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py index 482b13c94..e582d8468 100755 --- a/scripts/mk_consts_files.py +++ b/scripts/mk_consts_files.py @@ -17,6 +17,11 @@ def main(args): parser.add_argument("api_files", nargs="+") parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None) parser.add_argument("--dotnet-output-dir", dest="dotnet_output_dir", default=None) + parser.add_argument("--java-output-dir", dest="java_output_dir", default=None) + parser.add_argument("--java-package-name", + dest="java_package_name", + default=None, + help="Name to give the Java package (e.g. ``com.microsoft.z3``).") pargs = parser.parse_args(args) if not mk_genfile_common.check_files_exist(pargs.api_files): @@ -41,6 +46,20 @@ def main(args): logging.info('Generated "{}"'.format(output)) count += 1 + if pargs.java_output_dir: + if pargs.java_package_name == None: + logging.error('Java package name must be specified') + return 1 + if not mk_genfile_common.check_dir_exists(pargs.java_output_dir): + return 1 + outputs = mk_genfile_common.mk_z3consts_java_internal( + pargs.api_files, + pargs.java_package_name, + pargs.java_output_dir) + for generated_file in outputs: + logging.info('Generated "{}"'.format(generated_file)) + count += 1 + if count == 0: logging.info('No files generated. You need to specific an output directory' ' for the relevant langauge bindings') diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 0734d52b0..d747baee8 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -255,6 +255,116 @@ def mk_z3consts_dotnet_internal(api_files, output_dir): z3consts.close() return z3consts_output_path + +def mk_z3consts_java_internal(api_files, package_name, output_dir): + """ + Generate "com.microsoft.z3.enumerations" package from the list of API + header files in ``api_files`` and write the package directory into + the ``output_dir`` directory + + Returns a list of the generated java source files. + """ + blank_pat = re.compile("^ *$") + comment_pat = re.compile("^ *//.*$") + typedef_pat = re.compile("typedef enum *") + typedef2_pat = re.compile("typedef enum { *") + openbrace_pat = re.compile("{ *") + closebrace_pat = re.compile("}.*;") + + DeprecatedEnums = [ 'Z3_search_failure' ] + gendir = os.path.join(output_dir, "enumerations") + if not os.path.exists(gendir): + os.mkdir(gendir) + + generated_enumeration_files = [] + for api_file in api_files: + api = open(api_file, 'r') + + SEARCHING = 0 + FOUND_ENUM = 1 + IN_ENUM = 2 + + mode = SEARCHING + decls = {} + idx = 0 + + linenum = 1 + for line in api: + m1 = blank_pat.match(line) + m2 = comment_pat.match(line) + if m1 or m2: + # skip blank lines and comments + linenum = linenum + 1 + elif mode == SEARCHING: + m = typedef_pat.match(line) + if m: + mode = FOUND_ENUM + m = typedef2_pat.match(line) + if m: + mode = IN_ENUM + decls = {} + idx = 0 + elif mode == FOUND_ENUM: + m = openbrace_pat.match(line) + if m: + mode = IN_ENUM + decls = {} + idx = 0 + else: + assert False, "Invalid %s, line: %s" % (api_file, linenum) + else: + assert mode == IN_ENUM + words = re.split('[^\-a-zA-Z0-9_]+', line) + m = closebrace_pat.match(line) + if m: + name = words[1] + if name not in DeprecatedEnums: + efile = open('%s.java' % os.path.join(gendir, name), 'w') + generated_enumeration_files.append(efile.name) + efile.write('/**\n * Automatically generated file\n **/\n\n') + efile.write('package %s.enumerations;\n\n' % package_name) + + efile.write('/**\n') + efile.write(' * %s\n' % name) + efile.write(' **/\n') + efile.write('public enum %s {\n' % name) + efile.write + first = True + for k in decls: + i = decls[k] + if first: + first = False + else: + efile.write(',\n') + efile.write(' %s (%s)' % (k, i)) + efile.write(";\n") + efile.write('\n private final int intValue;\n\n') + efile.write(' %s(int v) {\n' % name) + efile.write(' this.intValue = v;\n') + efile.write(' }\n\n') + efile.write(' public static final %s fromInt(int v) {\n' % name) + efile.write(' for (%s k: values()) \n' % name) + efile.write(' if (k.intValue == v) return k;\n') + efile.write(' return values()[0];\n') + efile.write(' }\n\n') + efile.write(' public final int toInt() { return this.intValue; }\n') + # efile.write(';\n %s(int v) {}\n' % name) + efile.write('}\n\n') + efile.close() + mode = SEARCHING + else: + if words[2] != '': + if len(words[2]) > 1 and words[2][1] == 'x': + idx = int(words[2], 16) + else: + idx = int(words[2]) + decls[words[1]] = idx + idx = idx + 1 + linenum = linenum + 1 + api.close() + return generated_enumeration_files + + ############################################################################### # Functions for generating a "module definition file" for MSVC ############################################################################### diff --git a/scripts/mk_util.py b/scripts/mk_util.py index be641ba35..38bf2a854 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2753,109 +2753,19 @@ def mk_z3consts_dotnet(api_files): # Extract enumeration types from z3_api.h, and add Java definitions def mk_z3consts_java(api_files): - blank_pat = re.compile("^ *$") - comment_pat = re.compile("^ *//.*$") - typedef_pat = re.compile("typedef enum *") - typedef2_pat = re.compile("typedef enum { *") - openbrace_pat = re.compile("{ *") - closebrace_pat = re.compile("}.*;") - java = get_component(JAVA_COMPONENT) - - DeprecatedEnums = [ 'Z3_search_failure' ] - gendir = os.path.join(java.src_dir, "enumerations") - if not os.path.exists(gendir): - os.mkdir(gendir) - + full_path_api_files = [] for api_file in api_files: api_file_c = java.find_file(api_file, java.name) api_file = os.path.join(api_file_c.src_dir, api_file) - - api = open(api_file, 'r') - - SEARCHING = 0 - FOUND_ENUM = 1 - IN_ENUM = 2 - - mode = SEARCHING - decls = {} - idx = 0 - - linenum = 1 - for line in api: - m1 = blank_pat.match(line) - m2 = comment_pat.match(line) - if m1 or m2: - # skip blank lines and comments - linenum = linenum + 1 - elif mode == SEARCHING: - m = typedef_pat.match(line) - if m: - mode = FOUND_ENUM - m = typedef2_pat.match(line) - if m: - mode = IN_ENUM - decls = {} - idx = 0 - elif mode == FOUND_ENUM: - m = openbrace_pat.match(line) - if m: - mode = IN_ENUM - decls = {} - idx = 0 - else: - assert False, "Invalid %s, line: %s" % (api_file, linenum) - else: - assert mode == IN_ENUM - words = re.split('[^\-a-zA-Z0-9_]+', line) - m = closebrace_pat.match(line) - if m: - name = words[1] - if name not in DeprecatedEnums: - efile = open('%s.java' % os.path.join(gendir, name), 'w') - efile.write('/**\n * Automatically generated file\n **/\n\n') - efile.write('package %s.enumerations;\n\n' % java.package_name) - - efile.write('/**\n') - efile.write(' * %s\n' % name) - efile.write(' **/\n') - efile.write('public enum %s {\n' % name) - efile.write - first = True - for k in decls: - i = decls[k] - if first: - first = False - else: - efile.write(',\n') - efile.write(' %s (%s)' % (k, i)) - efile.write(";\n") - efile.write('\n private final int intValue;\n\n') - efile.write(' %s(int v) {\n' % name) - efile.write(' this.intValue = v;\n') - efile.write(' }\n\n') - efile.write(' public static final %s fromInt(int v) {\n' % name) - efile.write(' for (%s k: values()) \n' % name) - efile.write(' if (k.intValue == v) return k;\n') - efile.write(' return values()[0];\n') - efile.write(' }\n\n') - efile.write(' public final int toInt() { return this.intValue; }\n') - # efile.write(';\n %s(int v) {}\n' % name) - efile.write('}\n\n') - efile.close() - mode = SEARCHING - else: - if words[2] != '': - if len(words[2]) > 1 and words[2][1] == 'x': - idx = int(words[2], 16) - else: - idx = int(words[2]) - decls[words[1]] = idx - idx = idx + 1 - linenum = linenum + 1 - api.close() + full_path_api_files.append(api_file) + generated_files = mk_genfile_common.mk_z3consts_java_internal( + full_path_api_files, + java.package_name, + java.src_dir) if VERBOSE: - print("Generated '%s'" % ('%s' % gendir)) + for generated_file in generated_files: + print("Generated '{}'".format(generated_file)) # Extract enumeration types from z3_api.h, and add ML definitions def mk_z3consts_ml(api_files): From 3042f0f9649e8595e8f317ea1844decf971305f1 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 6 Apr 2016 22:53:07 +0100 Subject: [PATCH 02/13] Fix inconsistent emission of Java enumeration files. The ordering of emitted enum values is not consistent between python 2 or 3. The root cause of the problem was a dictionary's keys being iterated over which has no defined order. This has been fixed by iterating over the dictionary's items and ordering by values. We could order by key rather than the values but seeing as these represent an enum, ordering by value makes more sense. --- scripts/mk_genfile_common.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index d747baee8..b8d6ac5e1 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -330,13 +330,13 @@ def mk_z3consts_java_internal(api_files, package_name, output_dir): efile.write('public enum %s {\n' % name) efile.write first = True - for k in decls: - i = decls[k] + # Iterate over key-value pairs ordered by value + for k, v in sorted(decls.items(), key=lambda pair: pair[1]): if first: first = False else: efile.write(',\n') - efile.write(' %s (%s)' % (k, i)) + efile.write(' %s (%s)' % (k, v)) efile.write(";\n") efile.write('\n private final int intValue;\n\n') efile.write(' %s(int v) {\n' % name) From 022039535ac36d03cc483cdcc2b5907ca0e574f1 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 16 Apr 2016 03:52:11 -0500 Subject: [PATCH 03/13] [CMake] Implement support for building and installing the Java bindings. I'm not entirely happy with some parts of the implementation * The default locations for installing ``com.microsoft.z3.jar`` and ``libz3java.so`` aren't correct. CMake cache variables have been provided that allow the user to change where these get installed. * The name of ``libz3java.so``. It doesn't conform to the Debian packaging guidelines (https://www.debian.org/doc/packaging-manuals/java-policy/x126.html) and I have not provided an option to change this. * The fact that ``SONAME`` and ``VERSION`` are not set on ``libz3java.so``. These issues should be addressed once we know the correct way to handle installation. --- README-CMake.md | 4 + contrib/cmake/src/CMakeLists.txt | 12 ++ contrib/cmake/src/api/java/CMakeLists.txt | 235 ++++++++++++++++++++++ 3 files changed, 251 insertions(+) create mode 100644 contrib/cmake/src/api/java/CMakeLists.txt diff --git a/README-CMake.md b/README-CMake.md index 2cec1653a..dd50c05fa 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -279,6 +279,10 @@ The following useful options can be passed to CMake whilst configuring. * ``INSTALL_DOTNET_BINDINGS`` - BOOL. If set to ``TRUE`` and ``BUILD_DOTNET_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's .NET bindings. * ``DOTNET_CSC_EXECUTABLE`` - STRING. The path to the C# compiler to use. Only relevant if ``BUILD_DOTNET_BINDINGS`` is set to ``TRUE``. * ``DOTNET_GACUTIL_EXECUTABLE`` - STRING. The path to the gacutil program to use. Only relevant if ``BUILD_DOTNET_BINDINGS`` is set to ``TRUE``. +* ``BUILD_JAVA_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's Java bindings will be built. +* ``INSTALL_JAVA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``BUILD_JAVA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Java bindings. +* ``Z3_JAVA_JAR_INSTALLDIR`` - STRING. The path to directory to install the Z3 Java ``.jar`` file. This path should be relative to ``CMAKE_INSTALL_PREFIX``. +* ``Z3_JAVA_JNI_LIB_INSTALLDIRR`` - STRING. The path to directory to install the Z3 Java JNI bridge library. This path should be relative to ``CMAKE_INSTALL_PREFIX``. On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface. diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt index 13403afb1..574dd1089 100644 --- a/contrib/cmake/src/CMakeLists.txt +++ b/contrib/cmake/src/CMakeLists.txt @@ -234,4 +234,16 @@ if (BUILD_DOTNET_BINDINGS) add_subdirectory(api/dotnet) endif() +################################################################################ +# Java bindings +################################################################################ +option(BUILD_JAVA_BINDINGS "Build Java bindings for Z3" OFF) +if (BUILD_JAVA_BINDINGS) + if (NOT BUILD_LIBZ3_SHARED) + message(FATAL_ERROR "The Java bindings will not work with a static libz3. " + "You either need to disable BUILD_JAVA_BINDINGS or enable BUILD_LIBZ3_SHARED") + endif() + add_subdirectory(api/java) +endif() + # TODO: Implement support for other bindigns diff --git a/contrib/cmake/src/api/java/CMakeLists.txt b/contrib/cmake/src/api/java/CMakeLists.txt new file mode 100644 index 000000000..e41fa5ed0 --- /dev/null +++ b/contrib/cmake/src/api/java/CMakeLists.txt @@ -0,0 +1,235 @@ +find_package(Java REQUIRED) +find_package(JNI REQUIRED) +include(UseJava) + +# Sanity check for dirty source tree +foreach (file_name "enumerations" "Native.cpp" "Native.java") + if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${file_name}") + message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${file_name}\"" + ${z3_polluted_tree_msg}) + endif() +endforeach() + +set(Z3_JAVA_PACKAGE_NAME "com.microsoft.z3") + +# Rule to generate ``Native.java`` and ``Native.cpp`` +set(Z3_JAVA_NATIVE_JAVA "${CMAKE_CURRENT_BINARY_DIR}/Native.java") +set(Z3_JAVA_NATIVE_CPP "${CMAKE_CURRENT_BINARY_DIR}/Native.cpp") +add_custom_command(OUTPUT "${Z3_JAVA_NATIVE_JAVA}" "${Z3_JAVA_NATIVE_CPP}" + COMMAND "${PYTHON_EXECUTABLE}" + "${CMAKE_SOURCE_DIR}/scripts/update_api.py" + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "--java-output-dir" + "${CMAKE_CURRENT_BINARY_DIR}" + "--java-package-name" + ${Z3_JAVA_PACKAGE_NAME} + DEPENDS + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "${CMAKE_SOURCE_DIR}/scripts/update_api.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} + # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency + "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + COMMENT "Generating \"${Z3_JAVA_NATIVE_JAVA}\" and \"${Z3_JAVA_NATIVE_CPP}\"" + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} +) + +# Add rule to build native code that provides a bridge between +# ``Native.java`` and libz3's interfac3. +add_library(z3java SHARED ${Z3_JAVA_NATIVE_CPP}) +target_link_libraries(z3java PRIVATE libz3) +# FIXME: +# Not sure if using all the flags used by the Z3 components is really necessary +# here. At the bare minimum setting _AMD64_ depending on the target is +# necessary but seeing as the Python build system uses all the flags used for building +# Z3's components to build ``Native.cpp`` lets do the same for now. +target_compile_options(z3java PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) +target_compile_definitions(z3java PRIVATE ${Z3_COMPONENT_CXX_DEFINES}) +z3_append_linker_flag_list_to_target(z3java ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) +target_include_directories(z3java PRIVATE + "${CMAKE_SOURCE_DIR}/src/api" + "${CMAKE_BINARY_DIR}/src/api" + ${JNI_INCLUDE_DIRS} +) +# FIXME: Should this library have SONAME and VERSION set? + +# This prevents CMake from automatically defining ``z3java_EXPORTS`` +set_property(TARGET z3java PROPERTY DEFINE_SYMBOL "") + +# Rule to generate the ``com.microsoft.z3.enumerations`` package +# FIXME: This list of files is fragile +set(Z3_JAVA_ENUMERATION_PACKAGE_FILES + Z3_ast_kind.java + Z3_ast_print_mode.java + Z3_decl_kind.java + Z3_error_code.java + Z3_goal_prec.java + Z3_lbool.java + Z3_param_kind.java + Z3_parameter_kind.java + Z3_sort_kind.java + Z3_symbol_kind.java +) +set(Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH "") +foreach (enum_file ${Z3_JAVA_ENUMERATION_PACKAGE_FILES}) + list(APPEND Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH + "${CMAKE_CURRENT_BINARY_DIR}/enumerations/${enum_file}" + ) +endforeach() +add_custom_command(OUTPUT ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH} + COMMAND "${PYTHON_EXECUTABLE}" + "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py" + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "--java-output-dir" + "${CMAKE_CURRENT_BINARY_DIR}" + "--java-package-name" + ${Z3_JAVA_PACKAGE_NAME} + DEPENDS + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} + COMMENT "Generating ${Z3_JAVA_PACKAGE_NAME}.enumerations package" + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} +) + +set(Z3_JAVA_JAR_SOURCE_FILES + AlgebraicNum.java + ApplyResultDecRefQueue.java + ApplyResult.java + ArithExpr.java + ArithSort.java + ArrayExpr.java + ArraySort.java + ASTDecRefQueue.java + AST.java + AstMapDecRefQueue.java + ASTMap.java + AstVectorDecRefQueue.java + ASTVector.java + BitVecExpr.java + BitVecNum.java + BitVecSort.java + BoolExpr.java + BoolSort.java + Constructor.java + ConstructorList.java + Context.java + DatatypeExpr.java + DatatypeSort.java + EnumSort.java + Expr.java + FiniteDomainExpr.java + FiniteDomainNum.java + FiniteDomainSort.java + FixedpointDecRefQueue.java + Fixedpoint.java + FPExpr.java + FPNum.java + FPRMExpr.java + FPRMNum.java + FPRMSort.java + FPSort.java + FuncDecl.java + FuncInterpDecRefQueue.java + FuncInterpEntryDecRefQueue.java + FuncInterp.java + Global.java + GoalDecRefQueue.java + Goal.java + IDecRefQueue.java + IDisposable.java + InterpolationContext.java + IntExpr.java + IntNum.java + IntSort.java + IntSymbol.java + ListSort.java + Log.java + ModelDecRefQueue.java + Model.java + OptimizeDecRefQueue.java + Optimize.java + ParamDescrsDecRefQueue.java + ParamDescrs.java + ParamsDecRefQueue.java + Params.java + Pattern.java + ProbeDecRefQueue.java + Probe.java + Quantifier.java + RatNum.java + RealExpr.java + RealSort.java + ReExpr.java + RelationSort.java + ReSort.java + SeqExpr.java + SeqSort.java + SetSort.java + SolverDecRefQueue.java + Solver.java + Sort.java + StatisticsDecRefQueue.java + Statistics.java + Status.java + StringSymbol.java + Symbol.java + TacticDecRefQueue.java + Tactic.java + TupleSort.java + UninterpretedSort.java + Version.java + Z3Exception.java + Z3Object.java +) +set(Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "") +foreach (java_src_file ${Z3_JAVA_JAR_SOURCE_FILES}) + list(APPEND Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "${CMAKE_CURRENT_SOURCE_DIR}/${java_src_file}") +endforeach() +# Add generated files to list +list(APPEND Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH + ${Z3_JAVA_NATIVE_JAVA} + ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH} +) + +# Convenient top-level target +add_custom_target(build_z3_java_bindings + ALL + DEPENDS + z3java + z3JavaJar +) + +# Rule to build ``com.microsoft.z3.jar`` +# TODO: Add version +# TODO: Should we set ``CMAKE_JNI_TARGET`` to ``TRUE``? +add_jar(z3JavaJar + SOURCES ${Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH} + OUTPUT_NAME ${Z3_JAVA_PACKAGE_NAME} + OUTPUT_DIR "${CMAKE_BINARY_DIR}" +) + +############################################################################### +# Install +############################################################################### +option(INSTALL_JAVA_BINDINGS "Install Java bindings when invoking install target" ON) +if (INSTALL_JAVA_BINDINGS) + # Provide cache variables for the install locations that the user can change. + # FIXME: I don't think these defaults install locations conform to the Debian + # packaging guidelines or any packaging guidelines for that matter... + set(Z3_JAVA_JAR_INSTALLDIR + "${CMAKE_INSTALL_LIBDIR}" + CACHE + PATH + "Directory to install Z3 Java jar file relative to install prefix" + ) + set(Z3_JAVA_JNI_LIB_INSTALLDIR + "${CMAKE_INSTALL_LIBDIR}" + CACHE + PATH + "Directory to install Z3 Java JNI bridge library relative to install prefix" + ) + install(TARGETS z3java + LIBRARY DESTINATION "${Z3_JAVA_JNI_LIB_INSTALLDIR}" + ) + install_jar(z3JavaJar DESTINATION "${Z3_JAVA_JAR_INSTALLDIR}") +endif() From 48550732bf122aac1bb35af3f8db8691f697ebcc Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 18 Apr 2016 11:18:47 +0100 Subject: [PATCH 04/13] [CMake] Add a few notes on finding the Java installation. --- README-CMake.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/README-CMake.md b/README-CMake.md index dd50c05fa..ca3ded9fb 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -290,6 +290,23 @@ Example ``` cmake -DCMAKE_BUILD_TYPE=Release -DENABLE_TRACING=FALSE ../ + +``` + +## Z3 API Bindings + +Z3 exposes various language bindings for its API. Below are some notes on building +and/or installing these bindings when building Z3 with CMake. + +### Java bindings + +The CMake build uses the ``FindJava`` and ``FindJNI`` cmake modules to detect the +installation of Java. If CMake fails to find your installation of Java set the +``JAVA_HOME`` environment variable when invoking CMake so that it points at the +correct location. For example + +``` +JAVA_HOME=/usr/lib/jvm/default cmake -DBUILD_JAVA_BINDINGS=ON ../ ``` ## Developer/packager notes From 8f697287036901b824d792a1cda02935f25f4320 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 18 Apr 2016 11:28:23 +0100 Subject: [PATCH 05/13] [CMake] Change default install location for ``com.microsoft.z3.jar``. It seems ``.jar`` files are typically installed into ``/usr/share/java``. --- contrib/cmake/src/api/java/CMakeLists.txt | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/contrib/cmake/src/api/java/CMakeLists.txt b/contrib/cmake/src/api/java/CMakeLists.txt index e41fa5ed0..b0ac2bedb 100644 --- a/contrib/cmake/src/api/java/CMakeLists.txt +++ b/contrib/cmake/src/api/java/CMakeLists.txt @@ -214,14 +214,15 @@ add_jar(z3JavaJar option(INSTALL_JAVA_BINDINGS "Install Java bindings when invoking install target" ON) if (INSTALL_JAVA_BINDINGS) # Provide cache variables for the install locations that the user can change. - # FIXME: I don't think these defaults install locations conform to the Debian - # packaging guidelines or any packaging guidelines for that matter... + # This defaults to ``/usr/local/java`` which seems to be the location for ``.jar`` + # files on Linux distributions set(Z3_JAVA_JAR_INSTALLDIR - "${CMAKE_INSTALL_LIBDIR}" + "${CMAKE_INSTALL_DATAROOTDIR}/java" CACHE PATH "Directory to install Z3 Java jar file relative to install prefix" ) + # FIXME: I don't think this the right installation location set(Z3_JAVA_JNI_LIB_INSTALLDIR "${CMAKE_INSTALL_LIBDIR}" CACHE From a1e831184494da6b69bd95be022fe0518b2c632d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 18 Apr 2016 11:31:09 +0100 Subject: [PATCH 06/13] [CMake] Add version to ``com.microsoft.z3.jar``. On Linux systems the ``.jar`` file is created as ``com.microsoft.z3-4.4.2.0.jar`` and a symlink named ``com.microsoft.z3.jar`` is created which points to it in the build and install directory. --- contrib/cmake/src/api/java/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/contrib/cmake/src/api/java/CMakeLists.txt b/contrib/cmake/src/api/java/CMakeLists.txt index b0ac2bedb..3663422f0 100644 --- a/contrib/cmake/src/api/java/CMakeLists.txt +++ b/contrib/cmake/src/api/java/CMakeLists.txt @@ -200,12 +200,12 @@ add_custom_target(build_z3_java_bindings ) # Rule to build ``com.microsoft.z3.jar`` -# TODO: Add version # TODO: Should we set ``CMAKE_JNI_TARGET`` to ``TRUE``? add_jar(z3JavaJar SOURCES ${Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH} OUTPUT_NAME ${Z3_JAVA_PACKAGE_NAME} OUTPUT_DIR "${CMAKE_BINARY_DIR}" + VERSION "${Z3_VERSION}" ) ############################################################################### From a56a53e72db9a885fc50ea5007c342e64bf4cb9f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 18 Apr 2016 12:07:18 +0100 Subject: [PATCH 07/13] [CMake] Fix installation location of ``com.microsoft.z3.jar`` when using CMake 2.8.12.2. It seems ``install_jar()`` in the version of ``UseJava.cmake`` shipped with that version of CMake doesn't handle the ``DESTINATION`` argument correctly and treats that as the installation location so CMake would install to ``/usr/local/DESTINATION`` rather than ``/usr/locale/share``. --- contrib/cmake/src/api/java/CMakeLists.txt | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/contrib/cmake/src/api/java/CMakeLists.txt b/contrib/cmake/src/api/java/CMakeLists.txt index 3663422f0..49d4a8841 100644 --- a/contrib/cmake/src/api/java/CMakeLists.txt +++ b/contrib/cmake/src/api/java/CMakeLists.txt @@ -232,5 +232,7 @@ if (INSTALL_JAVA_BINDINGS) install(TARGETS z3java LIBRARY DESTINATION "${Z3_JAVA_JNI_LIB_INSTALLDIR}" ) - install_jar(z3JavaJar DESTINATION "${Z3_JAVA_JAR_INSTALLDIR}") + # Note: Don't use ``DESTINATION`` here as the version of ``UseJava.cmake`` shipped + # with CMake 2.8.12.2 handles that incorrectly. + install_jar(z3JavaJar "${Z3_JAVA_JAR_INSTALLDIR}") endif() From c6965d5cb2f8868a8a05c9b0fef5833e065e9378 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 18 Apr 2016 14:07:09 +0100 Subject: [PATCH 08/13] [CMake] Try to fix the Windows build when building the Java bindings. On Windows the ``z3java`` target is not a ``LIBRARY`` target so just drop the ``LIBRARY`` keyword here. --- contrib/cmake/src/api/java/CMakeLists.txt | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/contrib/cmake/src/api/java/CMakeLists.txt b/contrib/cmake/src/api/java/CMakeLists.txt index 49d4a8841..6e16ddb74 100644 --- a/contrib/cmake/src/api/java/CMakeLists.txt +++ b/contrib/cmake/src/api/java/CMakeLists.txt @@ -229,9 +229,7 @@ if (INSTALL_JAVA_BINDINGS) PATH "Directory to install Z3 Java JNI bridge library relative to install prefix" ) - install(TARGETS z3java - LIBRARY DESTINATION "${Z3_JAVA_JNI_LIB_INSTALLDIR}" - ) + install(TARGETS z3java DESTINATION "${Z3_JAVA_JNI_LIB_INSTALLDIR}") # Note: Don't use ``DESTINATION`` here as the version of ``UseJava.cmake`` shipped # with CMake 2.8.12.2 handles that incorrectly. install_jar(z3JavaJar "${Z3_JAVA_JAR_INSTALLDIR}") From 49c92e4bd7c69d198974d6ec1616342fd28ea6c1 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 18 Apr 2016 15:33:19 +0100 Subject: [PATCH 09/13] [CMake] Add a note about the name of the Z3 Java ``.jar`` file. --- README-CMake.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/README-CMake.md b/README-CMake.md index ca3ded9fb..0943e7a7d 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -308,6 +308,10 @@ correct location. For example ``` JAVA_HOME=/usr/lib/jvm/default cmake -DBUILD_JAVA_BINDINGS=ON ../ ``` +Note that the built ``.jar`` file is named ``com.microsoft.z3-VERSION.jar`` +where ``VERSION`` is the Z3 version. Under non Windows systems a +symbolic link named ``com.microsoft.z3.jar`` is provided. This symbolic +link is not created when building under Windows. ## Developer/packager notes From 7cedf79b38ddfec21e8be0786cf2b558f0684d5f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 26 Apr 2016 00:06:36 +0100 Subject: [PATCH 10/13] [CMake] When building the ".NET" bindings emit ``Microsoft.Z3.dll`` and ``Microsoft.Z3.xml`` to the root build directory rather than ``/src/api/dotnet``. This fixes #573 which makes the behaviour consistent with the Python build system. --- contrib/cmake/src/api/dotnet/CMakeLists.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/contrib/cmake/src/api/dotnet/CMakeLists.txt b/contrib/cmake/src/api/dotnet/CMakeLists.txt index f077b57ce..fdde298a0 100644 --- a/contrib/cmake/src/api/dotnet/CMakeLists.txt +++ b/contrib/cmake/src/api/dotnet/CMakeLists.txt @@ -206,9 +206,9 @@ endif() # FIXME: The get_property() command only works correctly for single configuration generators # so we can't use it. We also can't use ``$`` because the ``OUTPUT`` # argument to ``add_custom_commands()`` won't accept it. For now just output file to the -# current binary directory. +# root binary directory like the Python build system does. # get_property(Z3_DOTNET_ASSEMBLY_OUTPUT_DIR TARGET libz3 PROPERTY LIBRARY_OUTPUT_DIRECTORY) -set(Z3_DOTNET_ASSEMBLY_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}") +set(Z3_DOTNET_ASSEMBLY_OUTPUT_DIR "${CMAKE_BINARY_DIR}") set(Z3_DOTNET_ASSEMBLY_NAME "Microsoft.Z3.dll") set(Z3_DOTNET_ASSEMBLY_DLL "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}/${Z3_DOTNET_ASSEMBLY_NAME}") # csc.exe doesn't work with UNIX style paths so convert to native path From 7213280d9b5544bf82888a8266699d70d55e28f7 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 26 Apr 2016 00:22:39 +0100 Subject: [PATCH 11/13] [CMake] Emit a warning when configuring to build the ``.NET`` bindings under a multi-configuration generator (e.g. Visual Studio). The warning concerns different generated files clobbering each other. Unfortunately there isn't a clean way to fix this right now. See http://public.kitware.com/pipermail/cmake/2016-March/063101.html --- contrib/cmake/src/api/dotnet/CMakeLists.txt | 26 ++++++++++++++++----- 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/contrib/cmake/src/api/dotnet/CMakeLists.txt b/contrib/cmake/src/api/dotnet/CMakeLists.txt index fdde298a0..e8fa12292 100644 --- a/contrib/cmake/src/api/dotnet/CMakeLists.txt +++ b/contrib/cmake/src/api/dotnet/CMakeLists.txt @@ -203,11 +203,23 @@ if (DOTNET_TOOLCHAIN_IS_WINDOWS) endif() endif() -# FIXME: The get_property() command only works correctly for single configuration generators -# so we can't use it. We also can't use ``$`` because the ``OUTPUT`` -# argument to ``add_custom_commands()`` won't accept it. For now just output file to the -# root binary directory like the Python build system does. -# get_property(Z3_DOTNET_ASSEMBLY_OUTPUT_DIR TARGET libz3 PROPERTY LIBRARY_OUTPUT_DIRECTORY) +# FIXME: Ideally we should emit files into a configuration specific directory +# when using multi-configuration generators so that the files generated by each +# configuration don't clobber each other. Unfortunately the ``get_property()`` +# command only works correctly for single configuration generators so we can't +# use it. We also can't use ``$`` because the ``OUTPUT`` +# argument to ``add_custom_commands()`` won't accept it. +# See http://public.kitware.com/pipermail/cmake/2016-March/063101.html +# +# For now just output file to the root binary directory like the Python build +# system does and emit a warning when appropriate. +if (DEFINED CMAKE_CONFIGURATION_TYPES) + # Multi-configuration build (e.g. Visual Studio and Xcode). + message(WARNING "You are using a multi-configuration generator. The build rules for" + " the \".NET\" bindings currently do not emit files per configuration so previously" + " generated files for other configurations will be overwritten.") +endif() + set(Z3_DOTNET_ASSEMBLY_OUTPUT_DIR "${CMAKE_BINARY_DIR}") set(Z3_DOTNET_ASSEMBLY_NAME "Microsoft.Z3.dll") set(Z3_DOTNET_ASSEMBLY_DLL "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}/${Z3_DOTNET_ASSEMBLY_NAME}") @@ -252,7 +264,9 @@ if (DOTNET_TOOLCHAIN_IS_MONO) # to find the assembly install(FILES "${Z3_DOTNET_PKGCONFIG_FILE}" DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}") - # Configure the install and uninstall scripts + # Configure the install and uninstall scripts. + # Note: If multi-configuration generator support is ever fixed then these + # scripts will be broken. configure_file(cmake_install_gac.cmake.in cmake_install_gac.cmake @ONLY) configure_file(cmake_uninstall_gac.cmake.in cmake_uninstall_gac.cmake @ONLY) From 626e0736d23df44b591c08edc7c77268292c3b0e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 26 Apr 2016 08:47:52 +0100 Subject: [PATCH 12/13] [CMake] Implement installation of ".NET" bindings on Windows. We don't install Z3_DOTNET_ASSEMBLY_DLL into the gac. Instead we just copy into installation directory. There are several reasons for this: * We can't install the Z3_DOTNET_ASSEMBLY_DLL into the gac in a portable way like we can with mono (i.e. the ``-root`` flag). * It isn't best practice to use ``gacutil.exe`` on Windows to install into the GAC, see https://msdn.microsoft.com/en-us/library/yf1d93sz(v=vs.110).aspx . Taking this approach should be sufficient because we can now do something like this ``` mkdir build cmake -G Ninja -DCMAKE_INSTALL_PREFIX= ../ ninja mkdir ninja install ``` and then put the contents of into a zip file which creates a redistributable zip file for Windows. --- contrib/cmake/src/api/dotnet/CMakeLists.txt | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/contrib/cmake/src/api/dotnet/CMakeLists.txt b/contrib/cmake/src/api/dotnet/CMakeLists.txt index e8fa12292..7440f021b 100644 --- a/contrib/cmake/src/api/dotnet/CMakeLists.txt +++ b/contrib/cmake/src/api/dotnet/CMakeLists.txt @@ -282,9 +282,10 @@ if (DOTNET_TOOLCHAIN_IS_MONO) add_dependencies(uninstall remove_dotnet_dll_from_gac) elseif(DOTNET_TOOLCHAIN_IS_WINDOWS) - # FIXME: This isn't implemented because I'm not sure how/if the assembly should - # be installed to the GAC. - message(WARNING "Install of .NET bindings is not implemented for Windows") + # Don't install Z3_DOTNET_ASSEMBLY_DLL into the gac. Instead just copy into + # installation directory. + install(FILES "${Z3_DOTNET_ASSEMBLY_DLL}" DESTINATION "${CMAKE_INSTALL_LIBDIR}") + install(FILES "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" DESTINATION "${CMAKE_INSTALL_LIBDIR}") else() message(FATAL_ERROR "Unknown .NET toolchain") endif() From fd7b8fe1ab8130e483a7c598302858f00a461cad Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 26 Apr 2016 11:49:46 +0100 Subject: [PATCH 13/13] [CMake] On Windows fix the ``install`` target so that it installs ``libz3.dll``. I've left a comment about the installation of ``libz3.lib``. I'm not sure if we want that installed or not. --- contrib/cmake/src/CMakeLists.txt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt index 13403afb1..1ce1a76cd 100644 --- a/contrib/cmake/src/CMakeLists.txt +++ b/contrib/cmake/src/CMakeLists.txt @@ -166,7 +166,8 @@ endforeach() install(TARGETS libz3 LIBRARY DESTINATION "${CMAKE_INSTALL_LIBDIR}" - ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}" + ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}" # On Windows this installs ``libz3.lib`` which CMake calls the "corresponding import library". Do we want this installed? + RUNTIME DESTINATION "${CMAKE_INSTALL_LIBDIR}" # For Windows. DLLs are runtime targets for CMake PUBLIC_HEADER DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}" )