From b3713e7496eb3a32a7109a5f3b2007b190344644 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 6 Apr 2016 22:47:28 +0100 Subject: [PATCH 1/9] 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 2/9] 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 3/9] [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 4/9] [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 5/9] [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 6/9] [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 7/9] [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 8/9] [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 9/9] [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