From d3f87e44a2481ca3301d2317f4b177199f4ab7b7 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 26 Mar 2016 13:39:10 +0000 Subject: [PATCH 1/7] Refactor ``mk_z3consts_dotnet()`` code into ``mk_z3consts_dotnet_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 | 10 ++++ scripts/mk_genfile_common.py | 92 ++++++++++++++++++++++++++++++++++++ scripts/mk_util.py | 87 ++-------------------------------- 3 files changed, 106 insertions(+), 83 deletions(-) diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py index 2c017bd2c..482b13c94 100755 --- a/scripts/mk_consts_files.py +++ b/scripts/mk_consts_files.py @@ -16,6 +16,7 @@ def main(args): parser = argparse.ArgumentParser(description=__doc__) 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) pargs = parser.parse_args(args) if not mk_genfile_common.check_files_exist(pargs.api_files): @@ -31,6 +32,15 @@ def main(args): logging.info('Generated "{}"'.format(output)) count += 1 + if pargs.dotnet_output_dir: + if not mk_genfile_common.check_dir_exists(pargs.dotnet_output_dir): + return 1 + output = mk_genfile_common.mk_z3consts_dotnet_internal( + pargs.api_files, + pargs.dotnet_output_dir) + logging.info('Generated "{}"'.format(output)) + 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 38d173108..9c6431248 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -163,6 +163,98 @@ def mk_z3consts_py_internal(api_files, output_dir): z3consts.close() return z3consts_output_path +def mk_z3consts_dotnet_internal(api_files, output_dir): + """ + Generate ``Enumerations.cs`` from the list of API header files + in ``api_files`` and write the output file into + the ``output_dir`` directory + + Returns the path to the generated file. + """ + assert os.path.isdir(output_dir) + assert isinstance(api_files, list) + blank_pat = re.compile("^ *\r?$") + 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' ] + z3consts = open(os.path.join(output_dir, 'Enumerations.cs'), 'w') + z3consts_output_path = z3consts.name + z3consts.write('// Automatically generated file\n\n') + z3consts.write('using System;\n\n' + '#pragma warning disable 1591\n\n' + 'namespace Microsoft.Z3\n' + '{\n') + + 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: + z3consts.write(' /// %s\n' % name) + z3consts.write(' public enum %s {\n' % name) + z3consts.write + for k in decls: + i = decls[k] + z3consts.write(' %s = %s,\n' % (k, i)) + z3consts.write(' }\n\n') + mode = SEARCHING + elif len(words) <= 2: + assert False, "Invalid %s, line: %s" % (api_file, linenum) + 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() + z3consts.write('}\n'); + z3consts.close() + return z3consts_output_path + ############################################################################### # Functions for generating a "module definition file" for MSVC ############################################################################### diff --git a/scripts/mk_util.py b/scripts/mk_util.py index e6de3e8ea..dc85c2b76 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2738,96 +2738,17 @@ def mk_z3consts_py(api_files): if VERBOSE: print("Generated '{}".format(generated_file)) - # Extract enumeration types from z3_api.h, and add .Net definitions def mk_z3consts_dotnet(api_files): - blank_pat = re.compile("^ *\r?$") - comment_pat = re.compile("^ *//.*$") - typedef_pat = re.compile("typedef enum *") - typedef2_pat = re.compile("typedef enum { *") - openbrace_pat = re.compile("{ *") - closebrace_pat = re.compile("}.*;") - dotnet = get_component(DOTNET_COMPONENT) - - DeprecatedEnums = [ 'Z3_search_failure' ] - z3consts = open(os.path.join(dotnet.src_dir, 'Enumerations.cs'), 'w') - z3consts.write('// Automatically generated file\n\n') - z3consts.write('using System;\n\n' - '#pragma warning disable 1591\n\n' - 'namespace Microsoft.Z3\n' - '{\n') - + full_path_api_files = [] for api_file in api_files: api_file_c = dotnet.find_file(api_file, dotnet.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: - z3consts.write(' /// %s\n' % name) - z3consts.write(' public enum %s {\n' % name) - z3consts.write - for k in decls: - i = decls[k] - z3consts.write(' %s = %s,\n' % (k, i)) - z3consts.write(' }\n\n') - mode = SEARCHING - elif len(words) <= 2: - assert False, "Invalid %s, line: %s" % (api_file, linenum) - 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() - z3consts.write('}\n'); - z3consts.close() + full_path_api_files.append(api_file) + generated_file = mk_genfile_common.mk_z3consts_dotnet_internal(full_path_api_files, dotnet.src_dir) if VERBOSE: - print("Generated '%s'" % os.path.join(dotnet.src_dir, 'Enumerations.cs')) - + print("Generated '{}".format(generated_file)) # Extract enumeration types from z3_api.h, and add Java definitions def mk_z3consts_java(api_files): From 23ac66ef42b408e8bea92cdd15600c3681994af9 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 26 Mar 2016 13:49:37 +0000 Subject: [PATCH 2/7] Fix inconsistent emission of ``Enumerations.cs``. 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 9c6431248..0734d52b0 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -234,9 +234,9 @@ def mk_z3consts_dotnet_internal(api_files, output_dir): z3consts.write(' /// %s\n' % name) z3consts.write(' public enum %s {\n' % name) z3consts.write - for k in decls: - i = decls[k] - z3consts.write(' %s = %s,\n' % (k, i)) + # Iterate over key-value pairs ordered by value + for k, v in sorted(decls.items(), key=lambda pair: pair[1]): + z3consts.write(' %s = %s,\n' % (k, v)) z3consts.write(' }\n\n') mode = SEARCHING elif len(words) <= 2: From 6a2a8e06d71556beafe0bdaefba75c38970d7505 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 26 Mar 2016 17:08:24 +0000 Subject: [PATCH 3/7] [CMake] Declare uninstall rule before the components so that they can add dependencies to the rule for their own custom uninstall logic. --- CMakeLists.txt | 35 +++++++++++++++++++---------------- 1 file changed, 19 insertions(+), 16 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index df6d528b0..a3ba4968e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -327,6 +327,25 @@ message(STATUS "CMAKE_INSTALL_LIBDIR: \"${CMAKE_INSTALL_LIBDIR}\"") message(STATUS "CMAKE_INSTALL_BINDIR: \"${CMAKE_INSTALL_BINDIR}\"") message(STATUS "CMAKE_INSTALL_INCLUDEDIR: \"${CMAKE_INSTALL_INCLUDEDIR}\"") +################################################################################ +# Uninstall rule +################################################################################ +configure_file( + "${CMAKE_SOURCE_DIR}/cmake/cmake_uninstall.cmake.in" + "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake" + @ONLY +) + +# Target needs to be declared before the components so that they can add +# dependencies to this target so they can run their own custom uninstall rules. +add_custom_target(uninstall + COMMAND + "${CMAKE_COMMAND}" -P "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake" + COMMENT "Uninstalling..." + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + VERBATIM +) + ################################################################################ # CMake build file locations ################################################################################ @@ -362,19 +381,3 @@ if (ENABLE_EXAMPLE_TARGETS) add_subdirectory(examples) endif() -################################################################################ -# Uninstall rule -################################################################################ -configure_file( - "${CMAKE_SOURCE_DIR}/cmake/cmake_uninstall.cmake.in" - "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake" - @ONLY -) - -add_custom_target(uninstall - COMMAND - "${CMAKE_COMMAND}" -P "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake" - COMMENT "Uninstalling..." - ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} - VERBATIM -) From 20d3bf4d0ccbd4e510b04be1d0672f431448e1ae Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 24 Mar 2016 23:54:44 +0000 Subject: [PATCH 4/7] [CMake] Implement support for building the .NET bindings. 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. --- .gitignore | 2 + CMakeLists.txt | 7 + README-CMake.md | 5 + .../cmake/modules/FindDotNetToolchain.cmake | 53 ++++ contrib/cmake/src/CMakeLists.txt | 12 + contrib/cmake/src/api/dotnet/CMakeLists.txt | 273 ++++++++++++++++++ .../src/api/dotnet/cmake_install_gac.cmake.in | 18 ++ .../api/dotnet/cmake_uninstall_gac.cmake.in | 20 ++ 8 files changed, 390 insertions(+) create mode 100644 contrib/cmake/cmake/modules/FindDotNetToolchain.cmake create mode 100644 contrib/cmake/src/api/dotnet/CMakeLists.txt create mode 100644 contrib/cmake/src/api/dotnet/cmake_install_gac.cmake.in create mode 100644 contrib/cmake/src/api/dotnet/cmake_uninstall_gac.cmake.in 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() From c52c999393b6dbd79afb7acba9d4e671b46fcec5 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 27 Mar 2016 12:28:37 +0100 Subject: [PATCH 5/7] [CMake] Document the ``PYTHON_EXECUTABLE`` CMake cache variable. User's can use this to pick a different version of Python to use for the build. --- README-CMake.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README-CMake.md b/README-CMake.md index 965a405e3..2cec1653a 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -272,6 +272,7 @@ The following useful options can be passed to CMake whilst configuring. * ``ENABLE_EXAMPLE_TARGETS`` - BOOL. If set to ``TRUE`` add the build targets for building the API examples. * ``USE_OPENMP`` - BOOL. If set to ``TRUE`` and OpenMP support is detected build with OpenMP support. * ``USE_LIB_GMP`` - BOOL. If set to ``TRUE`` use the GNU multiple precision library. If set to ``FALSE`` use an internal implementation. +* ``PYTHON_EXECUTABLE`` - STRING. The python executable to use during the build. * ``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. From 28f9c61d76644d6b755323453553692ab03d8b0b Mon Sep 17 00:00:00 2001 From: martin-neuhaeusser Date: Mon, 28 Mar 2016 17:08:22 +0200 Subject: [PATCH 6/7] Include *.cmx files during installation of OCaml bindings. The *.cmx files are now installed using ocamlfind. They contain information from the compiler that can be used during optimization (the upcoming OCaml 4.03.0 issues warning 58 if those files are missing from a package). --- scripts/mk_util.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index e6de3e8ea..e8b7fd9f0 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1913,6 +1913,7 @@ class MLComponent(Component): for m in self.modules: out.write(' ' + os.path.join(self.to_src_dir, m) + '.mli') out.write(' ' + os.path.join(self.sub_dir, m) + '.cmi') + out.write(' ' + os.path.join(self.sub_dir, m) + '.cmx') out.write(' %s' % ((os.path.join(self.sub_dir, 'libz3ml$(LIB_EXT)')))) out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml$(LIB_EXT)')))) out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cma')))) @@ -2013,7 +2014,7 @@ class DotNetExampleComponent(ExampleComponent): if VS_X64: out.write(' /platform:x64') elif VS_ARM: - out.write(' /platform:arm') + out.write(' /platform:arm') else: out.write(' /platform:x86') for csfile in get_cs_files(self.ex_dir): @@ -2206,7 +2207,7 @@ def mk_config(): static_opt = static_opt + 'd' config.write( 'AR_FLAGS=/nologo\n' - 'LINK_FLAGS=/nologo %s\n' + 'LINK_FLAGS=/nologo %s\n' 'SLINK_FLAGS=/nologo /LDd\n' % static_opt) if VS_X64: config.write( @@ -2249,7 +2250,7 @@ def mk_config(): 'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n' % (LTCG, LTCG)) - + # End of Windows VS config.mk if is_verbose(): @@ -2483,7 +2484,7 @@ def mk_makefile(): print("To build Z3, open a [Visual Studio x64 Command Prompt], then") elif VS_ARM: print(" platform: ARM\n") - print("To build Z3, open a [Visual Studio ARM Command Prompt], then") + print("To build Z3, open a [Visual Studio ARM Command Prompt], then") else: print(" platform: x86") print("To build Z3, open a [Visual Studio Command Prompt], then") @@ -3388,7 +3389,7 @@ class MakeRuleCmd(object): cls.write_cmd(out, "mkdir -p {install_root}{dir}".format( install_root=install_root, dir=dir)) - + @classmethod def _is_path_prefix_of(cls, temp_path, target_as_abs): """ @@ -3517,4 +3518,3 @@ def configure_file(template_file_path, output_file_path, substitutions): if __name__ == '__main__': import doctest doctest.testmod() - From cc12b1ebce229f1ca21052580d594a8df78a987f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 28 Mar 2016 23:10:23 +0100 Subject: [PATCH 7/7] [CMake] The bug in mono that causes the ``gacutil`` utility to crash if the assembly was compiled with ``/platform:x64`` has now been reported so update the comments to reflect this. --- contrib/cmake/src/api/dotnet/CMakeLists.txt | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/contrib/cmake/src/api/dotnet/CMakeLists.txt b/contrib/cmake/src/api/dotnet/CMakeLists.txt index a087c3a72..f077b57ce 100644 --- a/contrib/cmake/src/api/dotnet/CMakeLists.txt +++ b/contrib/cmake/src/api/dotnet/CMakeLists.txt @@ -188,9 +188,12 @@ list(APPEND CSC_FLAGS "$<$>:/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. +# Mono's gacutil crashes when trying to install an assembly if we set the +# platform in some cases, so only set it on Windows. This bug has been +# reported at https://bugzilla.xamarin.com/show_bug.cgi?id=39955 . However mono +# ignores the platform of an assembly when running it ( +# http://lists.ximian.com/pipermail/mono-devel-list/2015-November/043370.html ) +# so this shouldn't matter in practice. if (DOTNET_TOOLCHAIN_IS_WINDOWS) # Set platform for assembly if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")