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 df6d528b0..ee0810295 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -323,9 +323,35 @@ 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 +################################################################################ +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 +388,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 -) diff --git a/README-CMake.md b/README-CMake.md index 47ec11a7c..2cec1653a 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -265,14 +265,20 @@ 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. * ``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. +* ``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..f077b57ce --- /dev/null +++ b/contrib/cmake/src/api/dotnet/CMakeLists.txt @@ -0,0 +1,276 @@ +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+>" +) + +# 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") + 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() 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..0734d52b0 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 + # 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: + 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 e8b7fd9f0..be641ba35 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2739,96 +2739,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):