mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

[CMake] Implement support for building the .NET bindings.

Browse source 
When using Mono support for installing/uninstalling the bindings
is also implemented. For Windows install/uninstall is not implemented
because the python build system does not implement it and Microsoft's
documentation (https://msdn.microsoft.com/en-us/library/dkkx7f79.aspx)
says that the gacutil should only be used for development and not for
production.

For now a warning is just emitted if ``INSTALL_DOTNET_BINDINGS``
is enabled and the .NET toolchain is native Windows. Someone with
better knowledge of how to correctly install assemblies under Windows
should implement this or remove this message.

A notable difference from the Python build system is the
``/linkresource:`` flag is not passed to the C# compiler. This means
a user of the .NET bindings will have to copy the Z3 library (i.e.
``libz3.dll``) to their application directory manually. The reason
for this difference is that using this flag requires the working
directory to be the directory containing the Z3 library (i.e.
``libz3.dll``) but setting this up with multi-configuration generators
doesn't currently seem possible.
This commit is contained in:
Dan Liew 2016-03-24 23:54:44 +00:00
parent 6a2a8e06d7
commit 20d3bf4d0c
8 changed files with 390 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.gitignore vendored
View file

@ -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

7
CMakeLists.txt
View file

@ -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

5
README-CMake.md
View file

@ -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.

53
contrib/cmake/cmake/modules/FindDotNetToolchain.cmake Normal file
View file

@ -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
)

12
contrib/cmake/src/CMakeLists.txt
View file

@ -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

273
contrib/cmake/src/api/dotnet/CMakeLists.txt Normal file
View file

@ -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:$<TARGET_FILE_NAME:libz3>")
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
"$<$<CONFIG:Debug>:/debug+>"
"$<$<CONFIG:Debug>:/debug:full>"
"$<$<CONFIG:Debug>:/optimize->"
# This has to be quoted otherwise the ``;`` is interpreted as a command separator
"$<$<CONFIG:Debug>:\"/define:DEBUG$<SEMICOLON>TRACE\">"
# Release flags, expands to nothing if we are doing a debug build
"$<$<NOT:$<CONFIG:Debug>>:/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 ``$<TARGET_FILE_DIR:libz3>`` 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()

18
contrib/cmake/src/api/dotnet/cmake_install_gac.cmake.in Normal file
View file

@ -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()

20
contrib/cmake/src/api/dotnet/cmake_uninstall_gac.cmake.in Normal file
View file

@ -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()