add main remaining updates from Z3Prover#1815

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

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

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 && \

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,14 +22,18 @@ RUN apt-get update && \
         libomp-dev \
         llvm-3.9 \
         make \
-        mono-devel \
         ninja-build \
         python3 \
         python3-setuptools \
         python2.7 \
         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 && \

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

examples/CMakeLists.txt

@@ -116,6 +116,6 @@ endif()
 ################################################################################
 # Build dotnet examples
 ################################################################################
-#if (BUILD_DOTNET_BINDINGS)
-#    add_subdirectory(dotnet)
-#endif()
+if (BUILD_DOTNET_BINDINGS)
+    add_subdirectory(dotnet)
+endif()

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.

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}")
-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"
-  )
-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"
-)
+# Generate <Compile Include="files.cs" /> items
+set(Z3_DOTNET_COMPILE_ITEMS "")
+foreach(csfile ${Z3_DOTNET_ASSEMBLY_SOURCES})
+    set(Z3_DOTNET_COMPILE_ITEMS "${Z3_DOTNET_COMPILE_ITEMS}\n    <Compile Include=\"${csfile}\" />")
+endforeach()
 
-# Set the build type flags. The build type for the assembly roughly corresponds
-# with the native code build type.
-list(APPEND CSC_FLAGS
-  # Debug flags, expands to nothing if we aren't doing a debug build
-  "$<$<CONFIG:Debug>:/debug+>"
-  "$<$<CONFIG:Debug>:/debug:full>"
-  "$<$<CONFIG:Debug>:/optimize->"
-  # This has to be quoted otherwise the ``;`` is interpreted as a command separator
-  "$<$<CONFIG:Debug>:\"/define:DEBUG$<SEMICOLON>TRACE\">"
-  # Release flags, expands to nothing if we are doing a debug build
-  "$<$<NOT:$<CONFIG:Debug>>:/optimize+>"
-)
 
-# 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()
+# 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.
 
-# 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 ``$<TARGET_FILE_DIR:libz3>`` 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.")
+set(Z3_DOTNET_NUPKG_VERSION "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}")
+if("${TARGET_ARCHITECTURE}" STREQUAL "i686")
+    set(Z3_DOTNET_PLATFORM "x86")
+else()
+    set(Z3_DOTNET_PLATFORM "AnyCPU")
 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}\""
-)
+# TODO conditional for signing. we can then enable the ``Release_delaysign`` configuration
+
+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=$<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()
+