diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile index 50763e8da..6012bb25f 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile @@ -32,7 +32,6 @@ RUN apt-get update && \ libomp-dev \ llvm-3.9 \ make \ - mono-devel \ ninja-build \ python3 \ python3-setuptools \ @@ -48,5 +47,6 @@ RUN useradd -m user && \ echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers USER user WORKDIR /home/user -# dotnet core doesn't support x86 +# 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 diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile index c963ce255..9c6bdc054 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile @@ -2,9 +2,10 @@ FROM ubuntu:14.04 RUN apt-get update && \ apt-get -y --no-install-recommends install \ + apt-transport-https \ binutils \ clang-3.9 \ - cmake \ + curl \ doxygen \ default-jdk \ gcc-multilib \ @@ -18,13 +19,20 @@ 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 08686e275..f4d9c873a 100644 --- a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile @@ -2,10 +2,12 @@ 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 \ @@ -20,7 +22,6 @@ RUN apt-get update && \ libomp-dev \ llvm-3.9 \ make \ - mono-devel \ ninja-build \ python3 \ python3-setuptools \ @@ -28,6 +29,11 @@ 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 687efebb4..a149a1d83 100755 --- a/contrib/ci/scripts/test_z3_examples_cmake.sh +++ b/contrib/ci/scripts/test_z3_examples_cmake.sh @@ -88,11 +88,14 @@ 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 - run_quiet run_non_native_binding mono ./dotnet_test.exe + 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 fi if [ "X${JAVA_BINDINGS}" = "X1" ]; then diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 17c8e7c3f..5d06029f9 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -116,6 +116,6 @@ endif() ################################################################################ # Build dotnet examples ################################################################################ -#if (BUILD_DOTNET_BINDINGS) -# add_subdirectory(dotnet) -#endif() \ No newline at end of file +if (BUILD_DOTNET_BINDINGS) + add_subdirectory(dotnet) +endif() \ No newline at end of file diff --git a/examples/dotnet/README b/examples/dotnet/README index 3f7e989df..b42156761 100644 --- a/examples/dotnet/README +++ b/examples/dotnet/README @@ -1,7 +1,6 @@ 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 the executable dotnet_example.exe +It will create a .net core 2.0 app. diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 20621e4fc..3ff1a484a 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -1,12 +1,10 @@ -find_package(DotNetToolchain REQUIRED) +find_package(Dotnet 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") @@ -127,160 +125,64 @@ endforeach() 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}") + +# Generate items +set(Z3_DOTNET_COMPILE_ITEMS "") +foreach(csfile ${Z3_DOTNET_ASSEMBLY_SOURCES}) + set(Z3_DOTNET_COMPILE_ITEMS "${Z3_DOTNET_COMPILE_ITEMS}\n ") 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" - ) -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" - ) + +# 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") else() - message(FATAL_ERROR "Unknown .NET toolchain") + set(Z3_DOTNET_PLATFORM "AnyCPU") 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" -) +# TODO conditional for signing. we can then enable the ``Release_delaysign`` configuration -# 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}\"" -) +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) # Convenient top-level target -add_custom_target(build_z3_dotnet_bindings - ALL - DEPENDS - "${Z3_DOTNET_ASSEMBLY_DLL}" -) +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}) ############################################################################### -# Install +# 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. ############################################################################### 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. - # 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") +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}") endif() +