diff --git a/.gitignore b/.gitignore index 80a50ea9f..fcff2132d 100644 --- a/.gitignore +++ b/.gitignore @@ -84,3 +84,5 @@ src/CMakeLists.txt src/*/CMakeLists.txt src/*/*/CMakeLists.txt src/*/*/*/CMakeLists.txt +src/api/dotnet/cmake_install_gac.cmake.in +src/api/dotnet/cmake_uninstall_gac.cmake.in diff --git a/CMakeLists.txt b/CMakeLists.txt index a3ba4968e..ee0810295 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -323,9 +323,16 @@ message(STATUS "Z3_DEPENDENT_EXTRA_C_LINK_FLAGS: ${Z3_DEPENDENT_EXTRA_C_LINK_FLA # Z3 installation locations ################################################################################ include(GNUInstallDirs) +set(CMAKE_INSTALL_PKGCONFIGDIR + "${CMAKE_INSTALL_LIBDIR}/pkgconfig" + CACHE + PATH + "Directory to install pkgconfig files" +) message(STATUS "CMAKE_INSTALL_LIBDIR: \"${CMAKE_INSTALL_LIBDIR}\"") message(STATUS "CMAKE_INSTALL_BINDIR: \"${CMAKE_INSTALL_BINDIR}\"") message(STATUS "CMAKE_INSTALL_INCLUDEDIR: \"${CMAKE_INSTALL_INCLUDEDIR}\"") +message(STATUS "CMAKE_INSTALL_PKGCONFIGDIR: \"${CMAKE_INSTALL_PKGCONFIGDIR}\"") ################################################################################ # Uninstall rule diff --git a/README-CMake.md b/README-CMake.md index 47ec11a7c..965a405e3 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -265,6 +265,7 @@ The following useful options can be passed to CMake whilst configuring. * ``CMAKE_INSTALL_INCLUDEDIR`` - STRING. The path to install z3 include files (relative to ``CMAKE_INSTALL_PREFIX``), e.g. ``include``. * ``CMAKE_INSTALL_LIBDIR`` - STRING. The path to install z3 libraries (relative to ``CMAKE_INSTALL_PREFIX``), e.g. ``lib``. * ``CMAKE_INSTALL_PREFIX`` - STRING. The install prefix to use (e.g. ``/usr/local/``). +* ``CMAKE_INSTALL_PKGCONFIGDIR`` - STRING. The path to install pkgconfig files. * ``CMAKE_INSTALL_PYTHON_PKG_DIR`` - STRING. The path to install the z3 python bindings. This can be relative (to ``CMAKE_INSTALL_PREFIX``) or absolute. * ``ENABLE_TRACING_FOR_NON_DEBUG`` - BOOL. If set to ``TRUE`` enable tracing in non-debug builds, if set to ``FALSE`` disable tracing in non-debug builds. Note in debug builds tracing is always enabled. * ``BUILD_LIBZ3_SHARED`` - BOOL. If set to ``TRUE`` build libz3 as a shared library otherwise build as a static library. @@ -273,6 +274,10 @@ The following useful options can be passed to CMake whilst configuring. * ``USE_LIB_GMP`` - BOOL. If set to ``TRUE`` use the GNU multiple precision library. If set to ``FALSE`` use an internal implementation. * ``BUILD_PYTHON_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's python bindings will be built. * ``INSTALL_PYTHON_BINDINGS`` - BOOL. If set to ``TRUE`` and ``BUILD_PYTHON_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Python bindings. +* ``BUILD_DOTNET_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's .NET bindings will be built. +* ``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``. 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/cmake/modules/FindDotNetToolchain.cmake b/contrib/cmake/cmake/modules/FindDotNetToolchain.cmake new file mode 100644 index 000000000..abc4ff21c --- /dev/null +++ b/contrib/cmake/cmake/modules/FindDotNetToolchain.cmake @@ -0,0 +1,53 @@ +# Tries to find a working .NET tool chain +# +# Once complete this will define +# DOTNET_TOOLCHAIN_FOUND : BOOL : System has a .NET toolchain +# DOTNET_CSC_EXECUTABLE - STRING : Path to C# compiler +# DOTNET_GACUTIL_EXECUTABLE - STRING : Path to gacutil +# DOTNET_TOOLCHAIN_IS_MONO : BOOL : True if detected .NET toolchain is Mono +# DOTNET_TOOLCHAIN_IS_WINDOWS : BOOL : True if detected .NET toolchain is native Windows +include(FindPackageHandleStandardArgs) + +find_program( + DOTNET_CSC_EXECUTABLE + NAMES "csc.exe" "mcs" "dmcs" +) +message(STATUS "DOTNET_CSC_EXECUTABLE: \"${DOTNET_CSC_EXECUTABLE}\"") + +find_program( + DOTNET_GACUTIL_EXECUTABLE + NAMES "gacutil.exe" "gacutil" +) +message(STATUS "DOTNET_GACUTIL_EXECUTABLE: \"${DOTNET_GACUTIL_EXECUTABLE}\"") + +# Try to determine the tool chain vendor +set(DOTNET_DETERMINED_VENDOR FALSE) +if (DOTNET_CSC_EXECUTABLE) + execute_process(COMMAND "${DOTNET_CSC_EXECUTABLE}" "/help" + RESULT_VARIABLE CSC_EXIT_CODE + OUTPUT_VARIABLE CSC_STD_OUT + ) + if (${CSC_EXIT_CODE} EQUAL 0) + if ("${CSC_STD_OUT}" MATCHES "^Mono[ ]+C#") + set(DOTNET_DETERMINED_VENDOR TRUE) + set(DOTNET_TOOLCHAIN_IS_MONO TRUE) + set(DOTNET_TOOLCHAIN_IS_WINDOWS FALSE) + message(STATUS ".NET toolchain is Mono") + elseif ("${CSC_STD_OUT}" MATCHES "^Microsoft.+Visual[ ]+C#") + set(DOTNET_DETERMINED_VENDOR TRUE) + set(DOTNET_TOOLCHAIN_IS_MONO FALSE) + set(DOTNET_TOOLCHAIN_IS_WINDOWS TRUE) + message(STATUS ".NET toolchain is Windows native") + else() + message(STATUS ".NET toolchain is unknown") + endif() + endif() +endif() + +# TODO: Check C# compiler works + +find_package_handle_standard_args(DotNetToolChain DEFAULT_MSG + DOTNET_CSC_EXECUTABLE + DOTNET_GACUTIL_EXECUTABLE + DOTNET_DETERMINED_VENDOR +) diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt index 00dd01627..13403afb1 100644 --- a/contrib/cmake/src/CMakeLists.txt +++ b/contrib/cmake/src/CMakeLists.txt @@ -222,4 +222,16 @@ if (BUILD_PYTHON_BINDINGS) add_subdirectory(api/python) endif() +################################################################################ +# .NET bindings +################################################################################ +option(BUILD_DOTNET_BINDINGS "Build .NET bindings for Z3" OFF) +if (BUILD_DOTNET_BINDINGS) + if (NOT BUILD_LIBZ3_SHARED) + message(FATAL_ERROR "The .NET bindings will not work with a static libz3. " + "You either need to disable BUILD_DOTNET_BINDINGS or enable BUILD_LIBZ3_SHARED") + endif() + add_subdirectory(api/dotnet) +endif() + # TODO: Implement support for other bindigns diff --git a/contrib/cmake/src/api/dotnet/CMakeLists.txt b/contrib/cmake/src/api/dotnet/CMakeLists.txt new file mode 100644 index 000000000..a087c3a72 --- /dev/null +++ b/contrib/cmake/src/api/dotnet/CMakeLists.txt @@ -0,0 +1,273 @@ +find_package(DotNetToolchain REQUIRED) + +# Configure AssemblyInfo.cs +set(VER_MAJOR "${Z3_VERSION_MAJOR}") +set(VER_MINOR "${Z3_VERSION_MINOR}") +set(VER_BUILD "${Z3_VERSION_PATCH}") +set(VER_REVISION "${Z3_VERSION_TWEAK}") +set(Z3_DOTNET_ASSEMBLY_INFO_FILE "${CMAKE_CURRENT_BINARY_DIR}/Properties/AssemblyInfo.cs") +configure_file("Properties/AssemblyInfo.cs.in" "${Z3_DOTNET_ASSEMBLY_INFO_FILE}" @ONLY) + +# Generate Native.cs +set(Z3_DOTNET_NATIVE_FILE "${CMAKE_CURRENT_BINARY_DIR}/Native.cs") +add_custom_command(OUTPUT "${Z3_DOTNET_NATIVE_FILE}" + COMMAND "${PYTHON_EXECUTABLE}" + "${CMAKE_SOURCE_DIR}/scripts/update_api.py" + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "--dotnet-output-dir" + "${CMAKE_CURRENT_BINARY_DIR}" + 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_DOTNET_NATIVE_FILE}" + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} +) + +# Generate Enumerations.cs +set(Z3_DOTNET_CONST_FILE "${CMAKE_CURRENT_BINARY_DIR}/Enumerations.cs") +add_custom_command(OUTPUT "${Z3_DOTNET_CONST_FILE}" + COMMAND "${PYTHON_EXECUTABLE}" + "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py" + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "--dotnet-output-dir" + "${CMAKE_CURRENT_BINARY_DIR}" + 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_DOTNET_CONST_FILE}" + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} +) + +set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE + AlgebraicNum.cs + ApplyResult.cs + ArithExpr.cs + ArithSort.cs + ArrayExpr.cs + ArraySort.cs + AST.cs + ASTMap.cs + ASTVector.cs + BitVecExpr.cs + BitVecNum.cs + BitVecSort.cs + BoolExpr.cs + BoolSort.cs + Constructor.cs + ConstructorList.cs + Context.cs + DatatypeExpr.cs + DatatypeSort.cs + Deprecated.cs + EnumSort.cs + Expr.cs + FiniteDomainExpr.cs + FiniteDomainNum.cs + FiniteDomainSort.cs + Fixedpoint.cs + FPExpr.cs + FPNum.cs + FPRMExpr.cs + FPRMNum.cs + FPRMSort.cs + FPSort.cs + FuncDecl.cs + FuncInterp.cs + Global.cs + Goal.cs + IDecRefQueue.cs + InterpolationContext.cs + IntExpr.cs + IntNum.cs + IntSort.cs + IntSymbol.cs + ListSort.cs + Log.cs + Model.cs + Optimize.cs + ParamDescrs.cs + Params.cs + Pattern.cs + Probe.cs + Quantifier.cs + RatNum.cs + RealExpr.cs + RealSort.cs + ReExpr.cs + RelationSort.cs + ReSort.cs + SeqExpr.cs + SeqSort.cs + SetSort.cs + Solver.cs + Sort.cs + Statistics.cs + Status.cs + StringSymbol.cs + Symbol.cs + Tactic.cs + TupleSort.cs + UninterpretedSort.cs + Version.cs + Z3Exception.cs + Z3Object.cs +) + +set(Z3_DOTNET_ASSEMBLY_SOURCES "") +# Make paths to source files absolute +foreach (csfile ${Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE}) + list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES "${CMAKE_CURRENT_SOURCE_DIR}/${csfile}") +endforeach() + +# Add generated files +list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES + "${Z3_DOTNET_CONST_FILE}" + "${Z3_DOTNET_NATIVE_FILE}" + "${Z3_DOTNET_ASSEMBLY_INFO_FILE}" +) + +# ``csc.exe`` doesn't like UNIX style paths so convert them +# if necessary first to native paths. +set(Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "") +foreach (csfile_path ${Z3_DOTNET_ASSEMBLY_SOURCES}) + file(TO_NATIVE_PATH "${csfile_path}" csfile_path_native) + list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "${csfile_path_native}") +endforeach() + +set(CSC_FLAGS "") +if (DOTNET_TOOLCHAIN_IS_WINDOWS) + # FIXME: Why use these flags? + # Note these flags have been copied from the Python build system. + list(APPEND CSC_FLAGS + "/noconfig" + "/nostdlib+" + "/reference:mscorlib.dll" + ) + # FIXME: This flag only works when the working directory of csc.exe is + # the directory containing the ``libz3`` target. I can't get this to work + # correctly with multi-configuration generators (i.e. Visual Studio) so + # just don't set the flag for now. + #list(APPEND CSC_FLAGS "/linkresource:$") +elseif (DOTNET_TOOLCHAIN_IS_MONO) + # We need to give the assembly a strong name so that it can be installed + # into the GAC. + list(APPEND CSC_FLAGS + "/keyfile:${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.mono.snk" + ) +else() + message(FATAL_ERROR "Unknown .NET toolchain") +endif() + +# Common flags +list(APPEND CSC_FLAGS + "/unsafe+" + "/nowarn:1701,1702" + "/errorreport:prompt" + "/warn:4" + "/reference:System.Core.dll" + "/reference:System.dll" + "/reference:System.Numerics.dll" + "/filealign:512" # Why? + "/target:library" +) + +# Set the build type flags. The build type for the assembly roughly corresponds +# with the native code build type. +list(APPEND CSC_FLAGS + # Debug flags, expands to nothing if we aren't doing a debug build + "$<$:/debug+>" + "$<$:/debug:full>" + "$<$:/optimize->" + # This has to be quoted otherwise the ``;`` is interpreted as a command separator + "$<$:\"/define:DEBUG$TRACE\">" + # Release flags, expands to nothing if we are doing a debug build + "$<$>:/optimize+>" +) + +# FIXME: Mono's gacutil crashes if we set the platform. This bug should +# be reported and fixed. However for Mono the platform flag is ignored +# so it shouldn't matter in practice. +if (DOTNET_TOOLCHAIN_IS_WINDOWS) + # Set platform for assembly + if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") + list(APPEND CSC_FLAGS "/platform:x64") + elseif ("${TARGET_ARCHITECTURE}" STREQUAL "i686") + list(APPEND CSC_FLAGS "/platform:x86") + 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 +# current binary directory. +# 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_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 +file(TO_NATIVE_PATH "${Z3_DOTNET_ASSEMBLY_DLL}" Z3_DOTNET_ASSEMBLY_DLL_NATIVE_PATH) +set(Z3_DOTNET_ASSEMBLY_DLL_DOC "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}/Microsoft.Z3.xml") +file(TO_NATIVE_PATH "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" Z3_DOTNET_ASSEMBLY_DLL_DOC_NATIVE_PATH) +add_custom_command(OUTPUT "${Z3_DOTNET_ASSEMBLY_DLL}" "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" + COMMAND + "${DOTNET_CSC_EXECUTABLE}" + ${CSC_FLAGS} + "/out:${Z3_DOTNET_ASSEMBLY_DLL_NATIVE_PATH}" + "/doc:${Z3_DOTNET_ASSEMBLY_DLL_DOC_NATIVE_PATH}" + ${Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH} + DEPENDS + ${Z3_DOTNET_ASSEMBLY_SOURCES} + libz3 + WORKING_DIRECTORY "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}" + COMMENT "Building \"${Z3_DOTNET_ASSEMBLY_DLL}\"" +) + +# Convenient top-level target +add_custom_target(build_z3_dotnet_bindings + ALL + DEPENDS + "${Z3_DOTNET_ASSEMBLY_DLL}" +) + +############################################################################### +# Install +############################################################################### +option(INSTALL_DOTNET_BINDINGS "Install .NET bindings when invoking install target" ON) +set(GAC_PKG_NAME "Microsoft.Z3.Sharp") +set(PREFIX "${CMAKE_INSTALL_PREFIX}") +set(VERSION "${Z3_VERSION}") +set(Z3_DOTNET_PKGCONFIG_FILE "${CMAKE_CURRENT_BINARY_DIR}/Microsoft.Z3.Sharp.pc") +configure_file("Microsoft.Z3.Sharp.pc.in" "${Z3_DOTNET_PKGCONFIG_FILE}" @ONLY) + +if (DOTNET_TOOLCHAIN_IS_MONO) + message(STATUS "Emitting install rules for .NET bindings") + # Install pkgconfig file for the assembly. This is needed by Monodevelop + # to find the assembly + install(FILES "${Z3_DOTNET_PKGCONFIG_FILE}" DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}") + + # Configure the install and uninstall scripts + configure_file(cmake_install_gac.cmake.in cmake_install_gac.cmake @ONLY) + configure_file(cmake_uninstall_gac.cmake.in cmake_uninstall_gac.cmake @ONLY) + + # Tell CMake to Invoke a script to install assembly to the GAC during install + install(SCRIPT "${CMAKE_CURRENT_BINARY_DIR}/cmake_install_gac.cmake") + + # Add custom target to uninstall the assembly from the GAC + add_custom_target(remove_dotnet_dll_from_gac + COMMAND "${CMAKE_COMMAND}" "-P" "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall_gac.cmake" + COMMENT "Uninstalling ${Z3_DOTNET_ASSEMBLY_NAME} from the GAC" + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + ) + 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") +else() + message(FATAL_ERROR "Unknown .NET toolchain") +endif() diff --git a/contrib/cmake/src/api/dotnet/cmake_install_gac.cmake.in b/contrib/cmake/src/api/dotnet/cmake_install_gac.cmake.in new file mode 100644 index 000000000..d49f985c0 --- /dev/null +++ b/contrib/cmake/src/api/dotnet/cmake_install_gac.cmake.in @@ -0,0 +1,18 @@ +# Install assembly to the GAC +set(GAC_ROOT "$ENV{DESTDIR}@CMAKE_INSTALL_FULL_LIBDIR@") +execute_process(COMMAND + "@DOTNET_GACUTIL_EXECUTABLE@" + "-i" + "@Z3_DOTNET_ASSEMBLY_DLL@" + "-f" + "-package" "@GAC_PKG_NAME@" + "-root" "${GAC_ROOT}" + WORKING_DIRECTORY "@CMAKE_CURRENT_BINARY_DIR@" + RESULT_VARIABLE gacutil_exit_code +) + +if ("${gacutil_exit_code}" EQUAL 0) + message(STATUS "Installed \"@Z3_DOTNET_ASSEMBLY_DLL@\" to the GAC") +else() + message(FATAL_ERROR "Failed to install \"@Z3_DOTNET_ASSEMBLY_DLL@\" to the GAC") +endif() diff --git a/contrib/cmake/src/api/dotnet/cmake_uninstall_gac.cmake.in b/contrib/cmake/src/api/dotnet/cmake_uninstall_gac.cmake.in new file mode 100644 index 000000000..14683e5b8 --- /dev/null +++ b/contrib/cmake/src/api/dotnet/cmake_uninstall_gac.cmake.in @@ -0,0 +1,20 @@ +# Uninstall assembly from the GAC +set(GAC_ROOT "$ENV{DESTDIR}@CMAKE_INSTALL_FULL_LIBDIR@") +execute_process(COMMAND + "@DOTNET_GACUTIL_EXECUTABLE@" + # Note ``-us`` takes assembly file name rather than + # ``-u`` which takes an assembly display name + "-us" + "@Z3_DOTNET_ASSEMBLY_NAME@" + "-f" + "-package" "@GAC_PKG_NAME@" + "-root" "${GAC_ROOT}" + WORKING_DIRECTORY "@CMAKE_CURRENT_BINARY_DIR@" + RESULT_VARIABLE gacutil_exit_code +) + +if ("${gacutil_exit_code}" EQUAL 0) + message(STATUS "Uninstalled \"@Z3_DOTNET_ASSEMBLY_NAME@\" from the GAC") +else() + message(FATAL_ERROR "Failed to uninstall \"@Z3_DOTNET_ASSEMBLY_NAME@\" from the GAC") +endif()