From 038971c029c0835e69e1dce5e54359dad585f9ee Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Jan 2019 10:21:56 -0800 Subject: [PATCH] Revert "api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration." --- .gitignore | 3 - .travis.yml | 3 +- cmake/modules/DotnetImports.props.in | 8 - cmake/modules/FindDotnet.cmake | 471 ------------------ .../z3_base_ubuntu32_16.04.Dockerfile | 5 +- .../z3_base_ubuntu_14.04.Dockerfile | 12 +- .../z3_base_ubuntu_16.04.Dockerfile | 8 +- contrib/ci/scripts/test_z3_examples_cmake.sh | 11 +- examples/CMakeLists.txt | 7 - examples/dotnet/CMakeLists.txt | 34 -- examples/dotnet/README | 3 +- examples/dotnet/dotnet.csproj | 12 - src/api/dotnet/CMakeLists.txt | 190 +++++-- src/api/dotnet/Microsoft.Z3.csproj | 418 ++++++++++++++++ src/api/dotnet/Microsoft.Z3.csproj.in | 95 ---- src/api/dotnet/Microsoft.Z3.props | 23 - src/api/dotnet/Microsoft.Z3.targets | 11 - src/api/dotnet/Properties/AssemblyInfo.cs.in | 38 ++ src/api/dotnet/core/README.txt | 15 + src/api/dotnet/core/core.csproj | 18 + 20 files changed, 645 insertions(+), 740 deletions(-) delete mode 100644 cmake/modules/DotnetImports.props.in delete mode 100644 cmake/modules/FindDotnet.cmake delete mode 100644 examples/dotnet/CMakeLists.txt delete mode 100644 examples/dotnet/dotnet.csproj create mode 100644 src/api/dotnet/Microsoft.Z3.csproj delete mode 100644 src/api/dotnet/Microsoft.Z3.csproj.in delete mode 100644 src/api/dotnet/Microsoft.Z3.props delete mode 100644 src/api/dotnet/Microsoft.Z3.targets create mode 100644 src/api/dotnet/Properties/AssemblyInfo.cs.in create mode 100644 src/api/dotnet/core/README.txt create mode 100644 src/api/dotnet/core/core.csproj diff --git a/.gitignore b/.gitignore index 88ccbb56f..e189a9569 100644 --- a/.gitignore +++ b/.gitignore @@ -76,6 +76,3 @@ src/api/ml/z3.mllib *.bak doc/api doc/code -.vs -examples/**/obj -CMakeSettings.json diff --git a/.travis.yml b/.travis.yml index 12e62ed3d..9ec6132b6 100644 --- a/.travis.yml +++ b/.travis.yml @@ -20,7 +20,7 @@ env: # 64-bit UBSan Debug build - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug UBSAN_BUILD=1 RUN_UNIT_TESTS=SKIP # 64-bit ASan Debug build - - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug ASAN_BUILD=1 RUN_UNIT_TESTS=SKIP ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug ASAN_BUILD=1 RUN_UNIT_TESTS=SKIP ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so # Build for running unit tests under ASan/UBSan # FIXME: We should really be doing a debug build but the unit tests run too # slowly when we do that. @@ -85,7 +85,6 @@ matrix: osx_image: xcode8.3 # Note: Apple Clang does not support OpenMP env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 DOTNET_BINDINGS=0 - script: # Use `travis_wait` when doing LTO builds because this configuration will # have long link times during which it will not show any output which diff --git a/cmake/modules/DotnetImports.props.in b/cmake/modules/DotnetImports.props.in deleted file mode 100644 index 090d46502..000000000 --- a/cmake/modules/DotnetImports.props.in +++ /dev/null @@ -1,8 +0,0 @@ - - - ${_DN_OUTPUT_PATH}/ - ${_DN_XPLAT_LIB_DIR}/ - ${_DN_VERSION} - ${_DN_CUSTOM_BUILDPROPS} - - diff --git a/cmake/modules/FindDotnet.cmake b/cmake/modules/FindDotnet.cmake deleted file mode 100644 index 98c5f2079..000000000 --- a/cmake/modules/FindDotnet.cmake +++ /dev/null @@ -1,471 +0,0 @@ -#.rst -# FindDotnet -# ---------- -# -# Find DotNet executable, and initialize functions for adding dotnet projects. -# -# Results are reported in the following variables:: -# -# DOTNET_FOUND - True if dotnet executable is found -# DOTNET_EXE - Dotnet executable -# DOTNET_VERSION - Dotnet version as reported by dotnet executable -# NUGET_EXE - Nuget executable (WIN32 only) -# NUGET_CACHE_PATH - Nuget package cache path -# -# The following functions are defined to add dotnet/msbuild projects: -# -# ADD_DOTNET -- add a project to be built by dotnet. -# -# ``` -# ADD_DOTNET( [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP] -# [CONFIG configuration] -# [PLATFORM platform] -# [PACKAGE output_nuget_packages... ] -# [VERSION nuget_package_version] -# [DEPENDS depend_nuget_packages... ] -# [OUTPUT_PATH output_path relative to cmake binary output dir] -# [CUSTOM_BUILDPROPS value....] -# [SOURCES additional_file_dependencies... ] -# [ARGUMENTS additional_build_args...] -# [PACK_ARGUMENTS additional_pack_args...]) -# ``` -# -# RUN_DOTNET -- Run a project with `dotnet run`. The `OUTPUT` argument represents artifacts -# produced by running the .NET program, and can be consumed from other build steps. -# -# ``` -# RUN_DOTNET( [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP] -# [ARGUMENTS program_args...] -# [OUTPUT outputs...] -# [CONFIG configuration] -# [PLATFORM platform] -# [DEPENDS depend_nuget_packages... ] -# [OUTPUT_PATH output_path relative to cmake binary output dir] -# [CUSTOM_BUILDPROPS value....] -# [SOURCES additional_file_dependencies... ]) -# ``` -# -# ADD_MSBUILD -- add a project to be built by msbuild. Windows-only. When building in Unix systems, msbuild targets are skipped. -# -# ``` -# ADD_MSBUILD( [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP] -# [CONFIG configuration] -# [PLATFORM platform] -# [PACKAGE output_nuget_packages... ] -# [DEPENDS depend_nuget_packages... ] -# [CUSTOM_BUILDPROPS value....] -# [SOURCES additional_file_dependencies... ] -# [ARGUMENTS additional_build_args...] -# [PACK_ARGUMENTS additional_pack_args...]) -# ``` -# -# SMOKETEST_DOTNET -- add a dotnet smoke test project to the build. The project will be run during a build, -# and if the program fails to build or run, the build fails. Currently only .NET Core App framework is supported. -# Multiple smoke tests will be run one-by-one to avoid global resource conflicts. -# -# SMOKETEST_DOTNET( [RELEASE|DEBUG] [X86|X64|ANYCPU] [NETCOREAPP] -# [ARGUMENTS program_args...] -# [CONFIG configuration] -# [PLATFORM platform] -# [DEPENDS depend_nuget_packages... ] -# [OUTPUT_PATH output_path relative to cmake binary output dir] -# [CUSTOM_BUILDPROPS value....] -# [SOURCES additional_file_dependencies... ]) -# -# For all the above functions, `RELEASE|DEBUG` overrides `CONFIG`, `X86|X64|ANYCPU` overrides PLATFORM. -# For Unix systems, the target framework defaults to `netstandard2.0`, unless `NETCOREAPP` is specified. -# For Windows, the project is built as-is, allowing multi-targeting. -# -# -# DOTNET_REGISTER_LOCAL_REPOSITORY -- register a local NuGet package repository. -# -# ``` -# DOTNET_REGISTER_LOCAL_REPOSITORY(repo_name repo_path) -# ``` -# -# TEST_DOTNET -- add a dotnet test project to ctest. The project will be run with `dotnet test`, -# and trx test reports will be generated in the build directory. For Windows, all target frameworks -# are tested against. For other platforms, only .NET Core App is tested against. -# Test failures will not fail the build. -# Tests are only run with `ctest -C `, not with `cmake --build ...` -# -# ``` -# TEST_DOTNET( -# [ARGUMENTS additional_dotnet_test_args...] -# [OUTPUT_PATH output_path relative to cmake binary output dir]) -# ``` -# -# GEN_DOTNET_PROPS -- Generates a Directory.Build.props file. The created file is populated with MSBuild properties: -# - DOTNET_PACKAGE_VERSION: a version string that can be referenced in the actual project file as $(DOTNET_PACKAGE_VERSION). -# The version string value can be set with PACKAGE_VERSION argument, and defaults to '1.0.0'. -# - XPLAT_LIB_DIR: points to the cmake build root directory. -# - OutputPath: Points to the cmake binary directory (overridden by OUTPUT_PATH, relatively). Therefore, projects built without cmake will consistently output -# to the cmake build directory. -# - Custom properties can be injected with XML_INJECT argument, which injects an arbitrary string into the project XML file. -# -# ``` -# GEN_DOTNET_PROPS( -# [PACKAGE_VERSION version] -# [XML_INJECT xml_injection]) -# ``` -# -# Require 3.5 for batch copy multiple files - -cmake_minimum_required(VERSION 3.5.0) - -IF(DOTNET_FOUND) - RETURN() -ENDIF() - -SET(NUGET_CACHE_PATH "~/.nuget/packages") -FIND_PROGRAM(DOTNET_EXE dotnet) -SET(DOTNET_MODULE_DIR ${CMAKE_CURRENT_LIST_DIR}) - -IF(NOT DOTNET_EXE) - SET(DOTNET_FOUND FALSE) - IF(Dotnet_FIND_REQUIRED) - MESSAGE(SEND_ERROR "Command 'dotnet' is not found.") - ENDIF() - RETURN() -ENDIF() - -EXECUTE_PROCESS( - COMMAND ${DOTNET_EXE} --version - OUTPUT_VARIABLE DOTNET_VERSION - OUTPUT_STRIP_TRAILING_WHITESPACE -) - -IF(WIN32) - FIND_PROGRAM(NUGET_EXE nuget PATHS ${CMAKE_BINARY_DIR}/tools) - IF(NUGET_EXE) - MESSAGE("-- Found nuget: ${NUGET_EXE}") - ELSE() - SET(NUGET_EXE ${CMAKE_BINARY_DIR}/tools/nuget.exe) - MESSAGE("-- Downloading nuget...") - FILE(DOWNLOAD https://dist.nuget.org/win-x86-commandline/latest/nuget.exe ${NUGET_EXE}) - MESSAGE("nuget.exe downloaded and saved to ${NUGET_EXE}") - ENDIF() -ENDIF() - -FUNCTION(DOTNET_REGISTER_LOCAL_REPOSITORY repo_name repo_path) - MESSAGE("-- Registering NuGet local repository '${repo_name}' at '${repo_path}'.") - GET_FILENAME_COMPONENT(repo_path ${repo_path} ABSOLUTE) - IF(WIN32) - STRING(REPLACE "/" "\\" repo_path ${repo_path}) - EXECUTE_PROCESS(COMMAND ${NUGET_EXE} sources list OUTPUT_QUIET) - EXECUTE_PROCESS(COMMAND ${NUGET_EXE} sources Remove -Name "${repo_name}" OUTPUT_QUIET ERROR_QUIET) - EXECUTE_PROCESS(COMMAND ${NUGET_EXE} sources Add -Name "${repo_name}" -Source "${repo_path}") - ELSE() - GET_FILENAME_COMPONENT(nuget_config ~/.nuget/NuGet/NuGet.Config ABSOLUTE) - EXECUTE_PROCESS(COMMAND ${DOTNET_EXE} nuget locals all --list OUTPUT_QUIET) - EXECUTE_PROCESS(COMMAND sed -i "/${repo_name}/d" "${nuget_config}") - EXECUTE_PROCESS(COMMAND sed -i "s## \\n #g" "${nuget_config}") - ENDIF() -ENDFUNCTION() - -FUNCTION(DOTNET_GET_DEPS _DN_PROJECT arguments) - CMAKE_PARSE_ARGUMENTS( - # prefix - _DN - # options (flags) - "RELEASE;DEBUG;X86;X64;ANYCPU;NETCOREAPP" - # oneValueArgs - "CONFIG;PLATFORM;VERSION;OUTPUT_PATH" - # multiValueArgs - "PACKAGE;DEPENDS;ARGUMENTS;PACK_ARGUMENTS;OUTPUT;SOURCES;CUSTOM_BUILDPROPS" - # the input arguments - ${arguments}) - - GET_FILENAME_COMPONENT(_DN_abs_proj "${_DN_PROJECT}" ABSOLUTE) - GET_FILENAME_COMPONENT(_DN_proj_dir "${_DN_abs_proj}" DIRECTORY) - GET_FILENAME_COMPONENT(_DN_projname "${_DN_PROJECT}" NAME) - STRING(REGEX REPLACE "\\.[^.]*$" "" _DN_projname_noext ${_DN_projname}) - - FILE(GLOB_RECURSE DOTNET_deps - ${_DN_proj_dir}/*.cs - ${_DN_proj_dir}/*.fs - ${_DN_proj_dir}/*.vb - ${_DN_proj_dir}/*.xaml - ${_DN_proj_dir}/*.resx - ${_DN_proj_dir}/*.xml - ${_DN_proj_dir}/*.*proj - ${_DN_proj_dir}/*.cs - ${_DN_proj_dir}/*.config) - LIST(APPEND DOTNET_deps ${_DN_SOURCES}) - SET(_DN_deps "") - FOREACH(dep ${DOTNET_deps}) - IF(NOT dep MATCHES /obj/ AND NOT dep MATCHES /bin/) - LIST(APPEND _DN_deps ${dep}) - ENDIF() - ENDFOREACH() - - - IF(_DN_RELEASE) - SET(_DN_CONFIG Release) - ELSEIF(_DN_DEBUG) - SET(_DN_CONFIG Debug) - ENDIF() - - IF(NOT _DN_CONFIG) - SET(_DN_CONFIG "$<$:Debug>$<$>:Release>") - ENDIF() - - # If platform is not specified, do not pass the Platform property. - # dotnet will pick the default Platform. - - IF(_DN_X86) - SET(_DN_PLATFORM x86) - ELSEIF(_DN_X64) - SET(_DN_PLATFORM x64) - ELSEIF(_DN_ANYCPU) - SET(_DN_PLATFORM "AnyCPU") - ENDIF() - - # If package version is not set, first fallback to DOTNET_PACKAGE_VERSION - # If again not set, defaults to 1.0.0 - IF(NOT _DN_VERSION) - SET(_DN_VERSION ${DOTNET_PACKAGE_VERSION}) - ENDIF() - IF(NOT _DN_VERSION) - SET(_DN_VERSION "1.0.0") - ENDIF() - - # Set the output path to the binary directory. - # Build outputs in separated output directories prevent overwriting. - # Later we then copy the outputs to the destination. - - IF(NOT _DN_OUTPUT_PATH) - SET(_DN_OUTPUT_PATH ${_DN_projname_noext}) - ENDIF() - - GET_FILENAME_COMPONENT(_DN_OUTPUT_PATH ${CMAKE_BINARY_DIR}/${_DN_OUTPUT_PATH} ABSOLUTE) - - # In a cmake build, the XPLAT libraries are always copied over. - # Set the proper directory for .NET projects. - SET(_DN_XPLAT_LIB_DIR ${CMAKE_BINARY_DIR}) - - SET(DOTNET_PACKAGES ${_DN_PACKAGE} PARENT_SCOPE) - SET(DOTNET_CONFIG ${_DN_CONFIG} PARENT_SCOPE) - SET(DOTNET_PLATFORM ${_DN_PLATFORM} PARENT_SCOPE) - SET(DOTNET_DEPENDS ${_DN_DEPENDS} PARENT_SCOPE) - SET(DOTNET_PROJNAME ${_DN_projname_noext} PARENT_SCOPE) - SET(DOTNET_PROJPATH ${_DN_abs_proj} PARENT_SCOPE) - SET(DOTNET_PROJDIR ${_DN_proj_dir} PARENT_SCOPE) - SET(DOTNET_ARGUMENTS ${_DN_ARGUMENTS} PARENT_SCOPE) - SET(DOTNET_RUN_OUTPUT ${_DN_OUTPUT} PARENT_SCOPE) - SET(DOTNET_PACKAGE_VERSION ${_DN_VERSION} PARENT_SCOPE) - SET(DOTNET_OUTPUT_PATH ${_DN_OUTPUT_PATH} PARENT_SCOPE) - SET(DOTNET_deps ${_DN_deps} PARENT_SCOPE) - - IF(_DN_PLATFORM) - SET(_DN_PLATFORM_PROP "/p:Platform=${_DN_PLATFORM}") - ENDIF() - - IF(_DN_NETCOREAPP) - SET(_DN_BUILD_OPTIONS -f netcoreapp2.0) - SET(_DN_PACK_OPTIONS /p:TargetFrameworks=netcoreapp2.0) - ELSEIF(UNIX) - # Unix builds default to netstandard2.0 - SET(_DN_BUILD_OPTIONS -f netstandard2.0) - SET(_DN_PACK_OPTIONS /p:TargetFrameworks=netstandard2.0) - ENDIF() - - SET(_DN_IMPORT_PROP ${CMAKE_CURRENT_BINARY_DIR}/${_DN_projname}.imports.props) - CONFIGURE_FILE(${DOTNET_MODULE_DIR}/DotnetImports.props.in ${_DN_IMPORT_PROP}) - SET(_DN_IMPORT_ARGS "/p:DirectoryBuildPropsPath=${_DN_IMPORT_PROP}") - - SET(DOTNET_IMPORT_PROPERTIES ${_DN_IMPORT_ARGS} PARENT_SCOPE) - SET(DOTNET_BUILD_PROPERTIES ${_DN_PLATFORM_PROP} ${_DN_IMPORT_ARGS} PARENT_SCOPE) - SET(DOTNET_BUILD_OPTIONS ${_DN_BUILD_OPTIONS} PARENT_SCOPE) - SET(DOTNET_PACK_OPTIONS --include-symbols ${_DN_PACK_OPTIONS} ${_DN_PACK_ARGUMENTS} PARENT_SCOPE) - -ENDFUNCTION() - -MACRO(ADD_DOTNET_DEPENDENCY_TARGETS tgt) - FOREACH(pkg_dep ${DOTNET_DEPENDS}) - ADD_DEPENDENCIES(${tgt}_${DOTNET_PROJNAME} PKG_${pkg_dep}) - MESSAGE(" ${DOTNET_PROJNAME} <- ${pkg_dep}") - ENDFOREACH() - - FOREACH(pkg ${DOTNET_PACKAGES}) - STRING(TOLOWER ${pkg} pkg_lowercase) - GET_FILENAME_COMPONENT(cache_path ${NUGET_CACHE_PATH}/${pkg_lowercase} ABSOLUTE) - IF(WIN32) - SET(rm_command powershell -NoLogo -NoProfile -NonInteractive -Command "Remove-Item -Recurse -Force -ErrorAction Ignore '${cache_path}'\; exit 0") - ELSE() - SET(rm_command rm -rf ${cache_path}) - ENDIF() - ADD_CUSTOM_TARGET( - DOTNET_PURGE_${pkg} - COMMAND ${CMAKE_COMMAND} -E echo "======= [x] Purging nuget package cache for ${pkg}" - COMMAND ${rm_command} - DEPENDS ${DOTNET_deps} - ) - ADD_DEPENDENCIES(${tgt}_${DOTNET_PROJNAME} DOTNET_PURGE_${pkg}) - # Add a target for the built package -- this can be referenced in - # another project. - ADD_CUSTOM_TARGET(PKG_${pkg}) - ADD_DEPENDENCIES(PKG_${pkg} ${tgt}_${DOTNET_PROJNAME}) - MESSAGE("==== ${DOTNET_PROJNAME} -> ${pkg}") - ENDFOREACH() -ENDMACRO() - -MACRO(DOTNET_BUILD_COMMANDS) - IF(${DOTNET_IS_MSBUILD}) - SET(build_dotnet_cmds - COMMAND ${CMAKE_COMMAND} -E echo "======= Building msbuild project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]" - COMMAND ${NUGET_EXE} restore -Force ${DOTNET_PROJPATH} - COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Clean ${DOTNET_BUILD_PROPERTIES} /p:Configuration="${DOTNET_CONFIG}" - COMMAND ${DOTNET_EXE} msbuild ${DOTNET_PROJPATH} /t:Build ${DOTNET_BUILD_PROPERTIES} /p:Configuration="${DOTNET_CONFIG}" ${DOTNET_ARGUMENTS}) - SET(build_dotnet_type "msbuild") - ELSE() - SET(build_dotnet_cmds - COMMAND ${CMAKE_COMMAND} -E echo "======= Building .NET project ${DOTNET_PROJNAME} [${DOTNET_CONFIG} ${DOTNET_PLATFORM}]" - COMMAND ${DOTNET_EXE} restore ${DOTNET_PROJPATH} ${DOTNET_IMPORT_PROPERTIES} - COMMAND ${DOTNET_EXE} clean ${DOTNET_PROJPATH} ${DOTNET_BUILD_PROPERTIES} - COMMAND ${DOTNET_EXE} build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_BUILD_OPTIONS} ${DOTNET_ARGUMENTS}) - SET(build_dotnet_type "dotnet") - ENDIF() - - # DOTNET_OUTPUTS refer to artifacts produced, that the BUILD_proj_name target depends on. - SET(DOTNET_OUTPUTS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.buildtimestamp) - LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E touch ${DOTNET_OUTPUTS}) - IF(NOT "${DOTNET_PACKAGES}" STREQUAL "") - MESSAGE("-- Adding ${build_dotnet_type} project ${DOTNET_PROJPATH} (version ${DOTNET_PACKAGE_VERSION})") - FOREACH(pkg ${DOTNET_PACKAGES}) - LIST(APPEND DOTNET_OUTPUTS ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.nupkg) - LIST(APPEND DOTNET_OUTPUTS ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.symbols.nupkg) - LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E remove ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.nupkg) - LIST(APPEND build_dotnet_cmds COMMAND ${CMAKE_COMMAND} -E remove ${DOTNET_OUTPUT_PATH}/${pkg}.${DOTNET_PACKAGE_VERSION}.symbols.nupkg) - ENDFOREACH() - LIST(APPEND build_dotnet_cmds COMMAND ${DOTNET_EXE} pack --no-build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_PACK_OPTIONS}) - ELSE() - MESSAGE("-- Adding ${build_dotnet_type} project ${DOTNET_PROJPATH} (no nupkg)") - ENDIF() - - ADD_CUSTOM_COMMAND( - OUTPUT ${DOTNET_OUTPUTS} - DEPENDS ${DOTNET_deps} - ${build_dotnet_cmds} - ) - ADD_CUSTOM_TARGET( - BUILD_${DOTNET_PROJNAME} ALL - DEPENDS ${DOTNET_OUTPUTS}) - -ENDMACRO() - -FUNCTION(ADD_DOTNET DOTNET_PROJECT) - DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}") - SET(DOTNET_IS_MSBUILD FALSE) - DOTNET_BUILD_COMMANDS() - ADD_DOTNET_DEPENDENCY_TARGETS(BUILD) -ENDFUNCTION() - -FUNCTION(ADD_MSBUILD DOTNET_PROJECT) - IF(NOT WIN32) - MESSAGE("-- Building non-Win32, skipping ${DOTNET_PROJECT}") - RETURN() - ENDIF() - - DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}") - SET(DOTNET_IS_MSBUILD TRUE) - DOTNET_BUILD_COMMANDS() - ADD_DOTNET_DEPENDENCY_TARGETS(BUILD) -ENDFUNCTION() - -FUNCTION(RUN_DOTNET DOTNET_PROJECT) - DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN};NETCOREAPP") - MESSAGE("-- Adding dotnet run project ${DOTNET_PROJECT}") - FILE(MAKE_DIRECTORY ${DOTNET_OUTPUT_PATH}) - ADD_CUSTOM_COMMAND( - OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp ${DOTNET_RUN_OUTPUT} - DEPENDS ${DOTNET_deps} - COMMAND ${DOTNET_EXE} restore ${DOTNET_PROJPATH} ${DOTNET_IMPORT_PROPERTIES} - COMMAND ${DOTNET_EXE} clean ${DOTNET_PROJPATH} ${DOTNET_BUILD_PROPERTIES} - COMMAND ${DOTNET_EXE} build --no-restore ${DOTNET_PROJPATH} -c ${DOTNET_CONFIG} ${DOTNET_BUILD_PROPERTIES} ${DOTNET_BUILD_OPTIONS} - # XXX tfm - COMMAND ${DOTNET_EXE} ${DOTNET_OUTPUT_PATH}/netcoreapp2.0/${DOTNET_PROJNAME}.dll ${DOTNET_ARGUMENTS} - COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp - WORKING_DIRECTORY ${DOTNET_OUTPUT_PATH}) - ADD_CUSTOM_TARGET( - RUN_${DOTNET_PROJNAME} - DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp ${DOTNET_RUN_OUTPUT}) - ADD_DOTNET_DEPENDENCY_TARGETS(RUN) -ENDFUNCTION() - -FUNCTION(TEST_DOTNET DOTNET_PROJECT) - DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}") - MESSAGE("-- Adding dotnet test project ${DOTNET_PROJECT}") - IF(WIN32) - SET(test_framework_args "") - ELSE() - SET(test_framework_args -f netcoreapp2.0) - ENDIF() - - ADD_TEST(NAME ${DOTNET_PROJNAME} - COMMAND ${DOTNET_EXE} test ${test_framework_args} --results-directory "${CMAKE_BINARY_DIR}" --logger trx ${DOTNET_ARGUMENTS} - WORKING_DIRECTORY ${DOTNET_OUTPUT_PATH}) - -ENDFUNCTION() - -SET_PROPERTY(GLOBAL PROPERTY DOTNET_LAST_SMOKETEST "") - -FUNCTION(SMOKETEST_DOTNET DOTNET_PROJECT) - MESSAGE("-- Adding dotnet smoke test project ${DOTNET_PROJECT}") - IF(WIN32) - RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}") - ELSE() - RUN_DOTNET(${DOTNET_PROJECT} "${ARGN}") - ENDIF() - - DOTNET_GET_DEPS(${DOTNET_PROJECT} "${ARGN}") - ADD_CUSTOM_TARGET( - SMOKETEST_${DOTNET_PROJNAME} - ALL - DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${DOTNET_PROJNAME}.runtimestamp) - ADD_DOTNET_DEPENDENCY_TARGETS(SMOKETEST) - GET_PROPERTY(_dn_last_smoketest GLOBAL PROPERTY DOTNET_LAST_SMOKETEST) - IF(_dn_last_smoketest) - MESSAGE("${_dn_last_smoketest} -> SMOKETEST_${DOTNET_PROJNAME}") - ADD_DEPENDENCIES(SMOKETEST_${DOTNET_PROJNAME} ${_dn_last_smoketest}) - ENDIF() - # Chain the smoke tests together so they are executed sequentially - SET_PROPERTY(GLOBAL PROPERTY DOTNET_LAST_SMOKETEST SMOKETEST_${DOTNET_PROJNAME}) - -ENDFUNCTION() - -SET(DOTNET_IMPORTS_TEMPLATE ${CMAKE_CURRENT_LIST_DIR}/DotnetImports.props.in) - -FUNCTION(GEN_DOTNET_PROPS target_props_file) - CMAKE_PARSE_ARGUMENTS( - # prefix - _DNP - # options (flags) - "" - # oneValueArgs - "PACKAGE_VERSION;XML_INJECT" - # multiValueArgs - "" - # the input arguments - ${ARGN}) - - IF(NOT _DNP_PACKAGE_VERSION) - SET(_DNP_PACKAGE_VERSION 1.0.0) - ENDIF() - - IF(_DNP_XML_INJECT) - SET(_DN_CUSTOM_BUILDPROPS ${_DNP_XML_INJECT}) - ENDIF() - - SET(_DN_OUTPUT_PATH ${CMAKE_BINARY_DIR}) - SET(_DN_XPLAT_LIB_DIR ${CMAKE_BINARY_DIR}) - SET(_DN_VERSION ${_DNP_PACKAGE_VERSION}) - CONFIGURE_FILE(${DOTNET_IMPORTS_TEMPLATE} ${target_props_file}) - UNSET(_DN_OUTPUT_PATH) - UNSET(_DN_XPLAT_LIB_DIR) - UNSET(_DN_VERSION) -ENDFUNCTION() - - -MESSAGE("-- Found .NET toolchain: ${DOTNET_EXE} (version ${DOTNET_VERSION})") -SET(DOTNET_FOUND TRUE) diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile index 6012bb25f..87e3c8d67 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile @@ -32,6 +32,7 @@ RUN apt-get update && \ libomp-dev \ llvm-3.9 \ make \ + mono-devel \ ninja-build \ python3 \ python3-setuptools \ @@ -47,6 +48,4 @@ RUN useradd -m user && \ echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers USER user WORKDIR /home/user -# TODO .NET core does not support Linux x86 yet, disable it for now. -# see: https://github.com/dotnet/coreclr/issues/9265 -ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer DOTNET_BINDINGS=0 +ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile index 9c6bdc054..c963ce255 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile @@ -2,10 +2,9 @@ FROM ubuntu:14.04 RUN apt-get update && \ apt-get -y --no-install-recommends install \ - apt-transport-https \ binutils \ clang-3.9 \ - curl \ + cmake \ doxygen \ default-jdk \ gcc-multilib \ @@ -19,20 +18,13 @@ RUN apt-get update && \ lib32gomp1 \ llvm-3.9 \ make \ + mono-devel \ ninja-build \ python3 \ python3-setuptools \ python2.7 \ python-setuptools -RUN curl -SL https://packages.microsoft.com/config/ubuntu/14.04/packages-microsoft-prod.deb --output packages-microsoft-prod.deb && \ - dpkg -i packages-microsoft-prod.deb && \ - apt-get update && \ - apt-get -y --no-install-recommends install dotnet-sdk-2.1 - -RUN curl -SL https://cmake.org/files/v3.12/cmake-3.12.0-Linux-x86_64.sh --output cmake-3.12.0-Linux-x86_64.sh && \ - sh cmake-3.12.0-Linux-x86_64.sh --prefix=/usr/local --exclude-subdir - # Create `user` user for container with password `user`. and give it # password-less sudo access RUN useradd -m user && \ diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile index f4d9c873a..08686e275 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile @@ -2,12 +2,10 @@ FROM ubuntu:16.04 RUN apt-get update && \ apt-get -y --no-install-recommends install \ - apt-transport-https \ binutils \ clang \ clang-3.9 \ cmake \ - curl \ doxygen \ default-jdk \ gcc-multilib \ @@ -22,6 +20,7 @@ RUN apt-get update && \ libomp-dev \ llvm-3.9 \ make \ + mono-devel \ ninja-build \ python3 \ python3-setuptools \ @@ -29,11 +28,6 @@ RUN apt-get update && \ python-setuptools \ sudo -RUN curl -SL https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb --output packages-microsoft-prod.deb && \ - dpkg -i packages-microsoft-prod.deb && \ - apt-get update && \ - apt-get -y --no-install-recommends install dotnet-sdk-2.1 - # Create `user` user for container with password `user`. and give it # password-less sudo access RUN useradd -m user && \ diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh index a149a1d83..687efebb4 100755 --- a/contrib/ci/scripts/test_z3_examples_cmake.sh +++ b/contrib/ci/scripts/test_z3_examples_cmake.sh @@ -88,14 +88,11 @@ if [ "X${PYTHON_BINDINGS}" = "X1" ]; then fi if [ "X${DOTNET_BINDINGS}" = "X1" ]; then + # Build .NET example + # FIXME: Move compliation step into CMake target + mcs ${Z3_SRC_DIR}/examples/dotnet/Program.cs /target:exe /out:dotnet_test.exe /reference:Microsoft.Z3.dll /r:System.Numerics.dll # Run .NET example - if [ "X${ASAN_BUILD}" = "X1" ]; then - # The dotnet test get stuck on ASAN - # so don't run it for now. - echo "Skipping .NET example under ASan build" - else - run_quiet run_non_native_binding dotnet ${Z3_BUILD_DIR}/dotnet/netcoreapp2.0/dotnet.dll - fi + run_quiet run_non_native_binding mono ./dotnet_test.exe fi if [ "X${JAVA_BINDINGS}" = "X1" ]; then diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 5d06029f9..6c50320ed 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -112,10 +112,3 @@ set_target_properties(z3_tptp5 PROPERTIES EXCLUDE_FROM_ALL TRUE) if (BUILD_PYTHON_BINDINGS) add_subdirectory(python) endif() - -################################################################################ -# Build dotnet examples -################################################################################ -if (BUILD_DOTNET_BINDINGS) - add_subdirectory(dotnet) -endif() \ No newline at end of file diff --git a/examples/dotnet/CMakeLists.txt b/examples/dotnet/CMakeLists.txt deleted file mode 100644 index 108326f83..000000000 --- a/examples/dotnet/CMakeLists.txt +++ /dev/null @@ -1,34 +0,0 @@ -find_package(Dotnet REQUIRED) - -if("${TARGET_ARCHITECTURE}" STREQUAL "i686") - set(Z3_DOTNET_PLATFORM "x86") -else() - set(Z3_DOTNET_PLATFORM "AnyCPU") -endif() - -configure_file(${CMAKE_CURRENT_SOURCE_DIR}/dotnet.csproj dotnet.csproj COPYONLY) -configure_file(${CMAKE_CURRENT_SOURCE_DIR}/Program.cs Program.cs COPYONLY) - -ADD_DOTNET(${CMAKE_CURRENT_BINARY_DIR}/dotnet.csproj - PLATFORM ${Z3_DOTNET_PLATFORM} - NETCOREAPP - CUSTOM_BUILDPROPS "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}" - DEPENDS Microsoft.Z3) - -if(UNIX AND NOT APPLE) - set(z3_dotnet_native_lib ${CMAKE_BINARY_DIR}/libz3.so) - set(z3_dotnet_test_manual_copy_deps - ${CMAKE_BINARY_DIR}/Microsoft.Z3/netstandard2.0/Microsoft.Z3.dll - ${z3_dotnet_native_lib} - ) - - add_custom_target( - z3_dotnet_test_manual_copy_assembly_hack ALL - COMMAND ${CMAKE_COMMAND} -E copy ${z3_dotnet_test_manual_copy_deps} ${CMAKE_BINARY_DIR}/dotnet/netcoreapp2.0/ - # hack the libz3 entry in deps so it's easy enough for dotnet to reach it... - COMMAND sed \"s/runtimes\\/.*libz3\\.so/libz3.so/\" -i ${CMAKE_BINARY_DIR}/dotnet/netcoreapp2.0/dotnet.deps.json - ) - - add_dependencies(z3_dotnet_test_manual_copy_assembly_hack BUILD_dotnet) -endif() - diff --git a/examples/dotnet/README b/examples/dotnet/README index b42156761..3f7e989df 100644 --- a/examples/dotnet/README +++ b/examples/dotnet/README @@ -1,6 +1,7 @@ Small example using the .Net bindings. +This example is only built if you have Visual Studio. To build the example execute make examples in the build directory. -It will create a .net core 2.0 app. +It will create the executable dotnet_example.exe diff --git a/examples/dotnet/dotnet.csproj b/examples/dotnet/dotnet.csproj deleted file mode 100644 index 7776259ea..000000000 --- a/examples/dotnet/dotnet.csproj +++ /dev/null @@ -1,12 +0,0 @@ - - - - Exe - netcoreapp2.0 - - - - - - - diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 3ff1a484a..20621e4fc 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -1,10 +1,12 @@ -find_package(Dotnet REQUIRED) +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") @@ -125,64 +127,160 @@ endforeach() list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES "${Z3_DOTNET_CONST_FILE}" "${Z3_DOTNET_NATIVE_FILE}" + "${Z3_DOTNET_ASSEMBLY_INFO_FILE}" ) - -# Generate items -set(Z3_DOTNET_COMPILE_ITEMS "") -foreach(csfile ${Z3_DOTNET_ASSEMBLY_SOURCES}) - set(Z3_DOTNET_COMPILE_ITEMS "${Z3_DOTNET_COMPILE_ITEMS}\n ") +# ``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() - -# FindDotnet.cmake forwards CMake build type to MSBuild. -# And thus we can put the conditional properties in the project file. -# Note, nuget package file names do not have the ${VER_REV} part. - -set(Z3_DOTNET_NUPKG_VERSION "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}") -if("${TARGET_ARCHITECTURE}" STREQUAL "i686") - set(Z3_DOTNET_PLATFORM "x86") +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" + ) +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.snk" + ) else() - set(Z3_DOTNET_PLATFORM "AnyCPU") + message(FATAL_ERROR "Unknown .NET toolchain") endif() -# TODO conditional for signing. we can then enable the ``Release_delaysign`` configuration +# 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" +) -configure_file(${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in ${CMAKE_CURRENT_BINARY_DIR}/build/Microsoft.Z3.csproj) -ADD_DOTNET(${CMAKE_CURRENT_BINARY_DIR}/build/Microsoft.Z3.csproj - VERSION ${Z3_DOTNET_NUPKG_VERSION} - PLATFORM ${Z3_DOTNET_PLATFORM} - SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in - ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.props - ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.targets - ${Z3_DOTNET_ASSEMBLY_SOURCES} - PACKAGE Microsoft.Z3 - PACK_ARGUMENTS "/p:_DN_CMAKE_CONFIG=$" - ) -add_dependencies(BUILD_Microsoft.Z3 libz3) +# 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: Ideally we should emit files into a configuration specific directory +# when using multi-configuration generators so that the files generated by each +# configuration don't clobber each other. Unfortunately 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. +# See http://public.kitware.com/pipermail/cmake/2016-March/063101.html +# +# For now just output file to the root binary directory like the Python build +# system does and emit a warning when appropriate. +if (DEFINED CMAKE_CONFIGURATION_TYPES) + # Multi-configuration build (e.g. Visual Studio and Xcode). + message(WARNING "You are using a multi-configuration generator. The build rules for" + " the \".NET\" bindings currently do not emit files per configuration so previously" + " generated files for other configurations will be overwritten.") +endif() + +set(Z3_DOTNET_ASSEMBLY_OUTPUT_DIR "${CMAKE_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 BUILD_Microsoft.Z3) - -# Register the local nupkg repo -set(Z3_DOTNET_LOCALREPO_NAME "Microsoft Z3 Local Repository") -DOTNET_REGISTER_LOCAL_REPOSITORY(${Z3_DOTNET_LOCALREPO_NAME} ${CMAKE_BINARY_DIR}) +add_custom_target(build_z3_dotnet_bindings + ALL + DEPENDS + "${Z3_DOTNET_ASSEMBLY_DLL}" +) ############################################################################### -# Install: register a local nuget repo and install our package. -# the build step depends on the 'purge' target, making sure that -# a user will always restore the freshly-built package. +# 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(INSTALL_DOTNET_BINDINGS) - install(FILES "${CMAKE_BINARY_DIR}/Microsoft.Z3/Microsoft.Z3.${Z3_DOTNET_NUPKG_VERSION}.nupkg" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget") - # move the local repo to the installation directory (cancel the build-time repo) - install(CODE "include(${CMAKE_CURRENT_LIST_DIR}/../../../cmake/modules/FindDotnet.cmake)\n DOTNET_REGISTER_LOCAL_REPOSITORY(\"${Z3_DOTNET_LOCALREPO_NAME}\" ${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR}/z3.nuget)") - install(FILES "${CMAKE_BINARY_DIR}/Microsoft.Z3/Microsoft.Z3.xml" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget") -# TODO GAC? -# set(GAC_PKG_NAME "Microsoft.Z3.Sharp") -# set(PREFIX "${CMAKE_INSTALL_PREFIX}") -# set(VERSION "${Z3_VERSION}") +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. + # Note: If multi-configuration generator support is ever fixed then these + # scripts will be broken. + 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) + # Don't install Z3_DOTNET_ASSEMBLY_DLL into the gac. Instead just copy into + # installation directory. + install(FILES "${Z3_DOTNET_ASSEMBLY_DLL}" DESTINATION "${CMAKE_INSTALL_LIBDIR}") + install(FILES "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" DESTINATION "${CMAKE_INSTALL_LIBDIR}") +else() + message(FATAL_ERROR "Unknown .NET toolchain") endif() - diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj new file mode 100644 index 000000000..045c610dd --- /dev/null +++ b/src/api/dotnet/Microsoft.Z3.csproj @@ -0,0 +1,418 @@ + + + + Debug + AnyCPU + 8.0.30703 + 2.0 + {EC3DB697-B734-42F7-9468-5B62821EEB5A} + Library + Properties + Microsoft.Z3 + Microsoft.Z3 + v4.0 + 512 + Client + 0 + + + true + full + false + ..\Debug\ + DEBUG;TRACE + prompt + 4 + true + ..\Debug\Microsoft.Z3.XML + False + False + True + False + False + True + False + True + True + False + False + False + True + False + False + False + True + False + False + True + True + True + False + False + + + + + + + True + Full + %28none%29 + 2 + + + pdbonly + true + ..\external\ + + + prompt + 4 + true + ..\external\Microsoft.Z3.xml + AnyCPU + + + ..\external\ + true + ..\external\Microsoft.Z3.xml + true + pdbonly + AnyCPU + bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + MinimumRecommendedRules.ruleset + ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + true + ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + true + false + + + true + ..\x64\Debug\ + DEBUG;TRACE + true + full + x64 + ..\Debug\Microsoft.Z3.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + MinimumRecommendedRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + true + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + true + True + False + True + False + False + False + False + False + False + False + False + False + False + False + False + False + True + False + False + True + False + False + False + + + + + + + False + Full + %28none%29 + 0 + ..\x64\Debug\Microsoft.Z3.XML + + + ..\x64\external_64\ + true + ..\x64\external_64\Microsoft.Z3.xml + true + pdbonly + x64 + ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + MinimumRecommendedRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + true + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + True + False + True + False + False + True + True + True + False + False + False + True + True + False + False + False + True + False + False + True + True + False + False + + + + + -repro + + True + Full + %28none%29 + 2 + + + ..\x64\external\ + true + ..\x64\external\Microsoft.Z3.XML + true + pdbonly + x64 + bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + MinimumRecommendedRules.ruleset + ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + true + ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + true + + + false + + + + + + + false + + + ..\Release_delaysign\ + true + ..\Release_delaysign\Microsoft.Z3.XML + true + pdbonly + AnyCPU + ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + MinimumRecommendedRules.ruleset + ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + true + ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + true + DELAYSIGN + + + bin\x64\Release_delaysign\ + true + bin\x64\Release_delaysign\Microsoft.Z3.XML + true + pdbonly + x64 + ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + MinimumRecommendedRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + true + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + true + + + true + ..\x86\Debug\ + DEBUG;TRACE + true + full + x86 + ..\Debug\Microsoft.Z3.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + MinimumRecommendedRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + ..\x86\Debug\Microsoft.Z3.XML + + + bin\x86\Release\ + true + bin\x86\Release\Microsoft.Z3.xml + true + pdbonly + x86 + ..\external\Microsoft.Z3.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + MinimumRecommendedRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + + + bin\x86\external\ + true + bin\x86\external\Microsoft.Z3.XML + true + pdbonly + x86 + bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + MinimumRecommendedRules.ruleset + ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + true + ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + true + + + bin\x86\Release_delaysign\ + DELAYSIGN + true + bin\x86\Release_delaysign\Microsoft.Z3.XML + true + pdbonly + x86 + ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + MinimumRecommendedRules.ruleset + ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + true + ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + true + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in deleted file mode 100644 index fc6d6a978..000000000 --- a/src/api/dotnet/Microsoft.Z3.csproj.in +++ /dev/null @@ -1,95 +0,0 @@ - - - - - - Microsoft.Z3 - Microsoft.Z3 - Microsoft.Z3 - - Z3 .NET Interface - Z3 .NET Interface - - Z3 - - Z3 is a satisfiability modulo theories solver from Microsoft Research. - .NET Interface to the Z3 Theorem Prover - - Copyright (C) 2006-2019 Microsoft Corporation - Copyright (C) 2006-2019 Microsoft Corporation - - Microsoft Corporation - Microsoft Corporation - - @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@ - @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@ - - @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@ - @VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@ - - ${DOTNET_PACKAGE_VERSION} - smt constraint solver theorem prover - - Microsoft - Microsoft - - - - - false - false - - - - DELAYSIGN - true - true - - - - - - netstandard2.0;net45 - library - True - 1701,1702 - 4 - true - $(OutputPath)\Microsoft.Z3.xml - - - - -${Z3_DOTNET_COMPILE_ITEMS} - - - - - - build - - - build - - - - - - - - - runtimes\win-x64\native - - - runtimes\linux-x64\native - - - - - - - runtimes\win-x86\native - - - - diff --git a/src/api/dotnet/Microsoft.Z3.props b/src/api/dotnet/Microsoft.Z3.props deleted file mode 100644 index a5db71359..000000000 --- a/src/api/dotnet/Microsoft.Z3.props +++ /dev/null @@ -1,23 +0,0 @@ - - - - - - true - true - true - - - $(MSBuildThisFileDirectory)..\ - $(Z3_PACKAGE_PATH)runtimes\win-x64\native\libz3.dll - $(Z3_PACKAGE_PATH)runtimes\win-x86\native\libz3.dll - $(Z3_PACKAGE_PATH)runtimes\linux-x64\native\libz3.so - - - - - - false - - - diff --git a/src/api/dotnet/Microsoft.Z3.targets b/src/api/dotnet/Microsoft.Z3.targets deleted file mode 100644 index 38e56b350..000000000 --- a/src/api/dotnet/Microsoft.Z3.targets +++ /dev/null @@ -1,11 +0,0 @@ - - - - - - %(RecursiveDir)%(FileName)%(Extension) - PreserveNewest - - - - diff --git a/src/api/dotnet/Properties/AssemblyInfo.cs.in b/src/api/dotnet/Properties/AssemblyInfo.cs.in new file mode 100644 index 000000000..e5a85f16f --- /dev/null +++ b/src/api/dotnet/Properties/AssemblyInfo.cs.in @@ -0,0 +1,38 @@ +using System; +using System.Reflection; +using System.Runtime.CompilerServices; +using System.Runtime.InteropServices; +using System.Security.Permissions; + +// General Information about an assembly is controlled through the following +// set of attributes. Change these attribute values to modify the information +// associated with an assembly. +[assembly: AssemblyTitle("Z3 .NET Interface")] +[assembly: AssemblyDescription(".NET Interface to the Z3 Theorem Prover")] +[assembly: AssemblyConfiguration("")] +[assembly: AssemblyCompany("Microsoft Corporation")] +[assembly: AssemblyProduct("Z3")] +[assembly: AssemblyCopyright("Copyright (C) 2006-2015 Microsoft Corporation")] +[assembly: AssemblyTrademark("")] +[assembly: AssemblyCulture("")] + +// Setting ComVisible to false makes the types in this assembly not visible +// to COM components. If you need to access a type in this assembly from +// COM, set the ComVisible attribute to true on that type. +[assembly: ComVisible(false)] + +// The following GUID is for the ID of the typelib if this project is exposed to COM +[assembly: Guid("4853ed71-2078-40f4-8117-bc46646bce0e")] + +// Version information for an assembly consists of the following four values: +// +// Major Version +// Minor Version +// Build Number +// Revision +// +// You can specify all the values or you can default the Build and Revision Numbers +// by using the '*' as shown below: +// [assembly: AssemblyVersion("4.2.0.0")] +[assembly: AssemblyVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")] +[assembly: AssemblyFileVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")] diff --git a/src/api/dotnet/core/README.txt b/src/api/dotnet/core/README.txt new file mode 100644 index 000000000..fa274f72b --- /dev/null +++ b/src/api/dotnet/core/README.txt @@ -0,0 +1,15 @@ +Z3 API for .NET Core + +Z3's .NET API uses Code Contracts, which are not included in .NET Core. The +enclosed file called DummyContracts.cs provides stubs for the Code Contracts +functions, so that the API will compile, but not perform any contract +checking. To build this using .NET core, run (in this directory): + +dotnet restore +dotnet build core.csproj -c Release + +If you are building with the cmake system, you should first +copy over files that are produced by the compiler into +this directory. You need to copy over Native.cs and Enumeration.cs + +-- good luck! diff --git a/src/api/dotnet/core/core.csproj b/src/api/dotnet/core/core.csproj new file mode 100644 index 000000000..5fa3275cf --- /dev/null +++ b/src/api/dotnet/core/core.csproj @@ -0,0 +1,18 @@ + + + + netcoreapp1.0 + $(DefineConstants);DOTNET_CORE + portable + Microsoft.Z3 + Library + core + $(PackageTargetFallback);dnxcore50 + 1.0.4 + + + + + + +