From 022039535ac36d03cc483cdcc2b5907ca0e574f1 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 16 Apr 2016 03:52:11 -0500 Subject: [PATCH] [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()