mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

add main remaining updates from #1815

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-20 12:43:05 -08:00
parent 5cdbb1f7be
commit 785fe2f6f7
7 changed files with 76 additions and 158 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile
View file

@ -32,7 +32,6 @@ RUN apt-get update && \
libomp-dev \ libomp-dev \
llvm-3.9 \ llvm-3.9 \
make \ make \
mono-devel \
ninja-build \ ninja-build \
python3 \ python3 \
python3-setuptools \ python3-setuptools \
@ -48,5 +47,6 @@ RUN useradd -m user && \
echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
USER user USER user
WORKDIR /home/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 ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer DOTNET_BINDINGS=0

12
contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile
View file

@ -2,9 +2,10 @@ FROM ubuntu:14.04
RUN apt-get update && \ RUN apt-get update && \
apt-get -y --no-install-recommends install \ apt-get -y --no-install-recommends install \
apt-transport-https \
binutils \ binutils \
clang-3.9 \ clang-3.9 \
cmake \ curl \
doxygen \ doxygen \
default-jdk \ default-jdk \
gcc-multilib \ gcc-multilib \
@ -18,13 +19,20 @@ RUN apt-get update && \
lib32gomp1 \ lib32gomp1 \
llvm-3.9 \ llvm-3.9 \
make \ make \
mono-devel \
ninja-build \ ninja-build \
python3 \ python3 \
python3-setuptools \ python3-setuptools \
python2.7 \ python2.7 \
python-setuptools 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 # Create `user` user for container with password `user`. and give it
# password-less sudo access # password-less sudo access
RUN useradd -m user && \ RUN useradd -m user && \

8
contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile
View file

@ -2,10 +2,12 @@ FROM ubuntu:16.04
RUN apt-get update && \ RUN apt-get update && \
apt-get -y --no-install-recommends install \ apt-get -y --no-install-recommends install \
apt-transport-https \
binutils \ binutils \
clang \ clang \
clang-3.9 \ clang-3.9 \
cmake \ cmake \
curl \
doxygen \ doxygen \
default-jdk \ default-jdk \
gcc-multilib \ gcc-multilib \
@ -20,7 +22,6 @@ RUN apt-get update && \
libomp-dev \ libomp-dev \
llvm-3.9 \ llvm-3.9 \
make \ make \
mono-devel \
ninja-build \ ninja-build \
python3 \ python3 \
python3-setuptools \ python3-setuptools \
@ -28,6 +29,11 @@ RUN apt-get update && \
python-setuptools \ python-setuptools \
sudo 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 # Create `user` user for container with password `user`. and give it
# password-less sudo access # password-less sudo access
RUN useradd -m user && \ RUN useradd -m user && \

11
contrib/ci/scripts/test_z3_examples_cmake.sh
View file

@ -88,11 +88,14 @@ if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
fi fi
if [ "X${DOTNET_BINDINGS}" = "X1" ]; then 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 .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 fi
if [ "X${JAVA_BINDINGS}" = "X1" ]; then if [ "X${JAVA_BINDINGS}" = "X1" ]; then

6
examples/CMakeLists.txt
View file

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

3
examples/dotnet/README
View file

@ -1,7 +1,6 @@
Small example using the .Net bindings. Small example using the .Net bindings.
This example is only built if you have Visual Studio.
To build the example execute To build the example execute
make examples make examples
in the build directory. in the build directory.
It will create the executable dotnet_example.exe It will create a .net core 2.0 app.

190
src/api/dotnet/CMakeLists.txt
View file

@ -1,12 +1,10 @@
find_package(DotNetToolchain REQUIRED) find_package(Dotnet REQUIRED)
# Configure AssemblyInfo.cs # Configure AssemblyInfo.cs
set(VER_MAJOR "${Z3_VERSION_MAJOR}") set(VER_MAJOR "${Z3_VERSION_MAJOR}")
set(VER_MINOR "${Z3_VERSION_MINOR}") set(VER_MINOR "${Z3_VERSION_MINOR}")
set(VER_BUILD "${Z3_VERSION_PATCH}") set(VER_BUILD "${Z3_VERSION_PATCH}")
set(VER_REVISION "${Z3_VERSION_TWEAK}") 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 # Generate Native.cs
set(Z3_DOTNET_NATIVE_FILE "${CMAKE_CURRENT_BINARY_DIR}/Native.cs") set(Z3_DOTNET_NATIVE_FILE "${CMAKE_CURRENT_BINARY_DIR}/Native.cs")
@ -127,160 +125,64 @@ endforeach()
list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES
"${Z3_DOTNET_CONST_FILE}" "${Z3_DOTNET_CONST_FILE}"
"${Z3_DOTNET_NATIVE_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. # Generate <Compile Include="files.cs" /> items
set(Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "") set(Z3_DOTNET_COMPILE_ITEMS "")
foreach (csfile_path ${Z3_DOTNET_ASSEMBLY_SOURCES}) foreach(csfile ${Z3_DOTNET_ASSEMBLY_SOURCES})
file(TO_NATIVE_PATH "${csfile_path}" csfile_path_native) set(Z3_DOTNET_COMPILE_ITEMS "${Z3_DOTNET_COMPILE_ITEMS}\n <Compile Include=\"${csfile}\" />")
list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "${csfile_path_native}")
endforeach() endforeach()
set(CSC_FLAGS "")
if (DOTNET_TOOLCHAIN_IS_WINDOWS) # FindDotnet.cmake forwards CMake build type to MSBuild.
# FIXME: Why use these flags? # And thus we can put the conditional properties in the project file.
# Note these flags have been copied from the Python build system. # Note, nuget package file names do not have the ${VER_REV} part.
list(APPEND CSC_FLAGS
"/noconfig" set(Z3_DOTNET_NUPKG_VERSION "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}")
"/nostdlib+" if("${TARGET_ARCHITECTURE}" STREQUAL "i686")
"/reference:mscorlib.dll" set(Z3_DOTNET_PLATFORM "x86")
)
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() else()
message(FATAL_ERROR "Unknown .NET toolchain") set(Z3_DOTNET_PLATFORM "AnyCPU")
endif() endif()
# Common flags # TODO conditional for signing. we can then enable the ``Release_delaysign`` configuration
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 configure_file(${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in ${CMAKE_CURRENT_BINARY_DIR}/build/Microsoft.Z3.csproj)
# with the native code build type. ADD_DOTNET(${CMAKE_CURRENT_BINARY_DIR}/build/Microsoft.Z3.csproj
list(APPEND CSC_FLAGS VERSION ${Z3_DOTNET_NUPKG_VERSION}
# Debug flags, expands to nothing if we aren't doing a debug build PLATFORM ${Z3_DOTNET_PLATFORM}
"$<$<CONFIG:Debug>:/debug+>" SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.csproj.in
"$<$<CONFIG:Debug>:/debug:full>" ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.props
"$<$<CONFIG:Debug>:/optimize->" ${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.targets
# This has to be quoted otherwise the ``;`` is interpreted as a command separator ${Z3_DOTNET_ASSEMBLY_SOURCES}
"$<$<CONFIG:Debug>:\"/define:DEBUG$<SEMICOLON>TRACE\">" PACKAGE Microsoft.Z3
# Release flags, expands to nothing if we are doing a debug build PACK_ARGUMENTS "/p:_DN_CMAKE_CONFIG=$<CONFIG>"
"$<$<NOT:$<CONFIG:Debug>>:/optimize+>" )
) add_dependencies(BUILD_Microsoft.Z3 libz3)
# 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 ``$<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.")
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 # Convenient top-level target
add_custom_target(build_z3_dotnet_bindings add_custom_target(build_z3_dotnet_bindings ALL DEPENDS BUILD_Microsoft.Z3)
ALL
DEPENDS # Register the local nupkg repo
"${Z3_DOTNET_ASSEMBLY_DLL}" 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) 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) if(INSTALL_DOTNET_BINDINGS)
message(STATUS "Emitting install rules for .NET bindings") install(FILES "${CMAKE_BINARY_DIR}/Microsoft.Z3/Microsoft.Z3.${Z3_DOTNET_NUPKG_VERSION}.nupkg" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget")
# Install pkgconfig file for the assembly. This is needed by Monodevelop # move the local repo to the installation directory (cancel the build-time repo)
# to find the assembly 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 "${Z3_DOTNET_PKGCONFIG_FILE}" DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}") install(FILES "${CMAKE_BINARY_DIR}/Microsoft.Z3/Microsoft.Z3.xml" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget")
# TODO GAC?
# Configure the install and uninstall scripts. # set(GAC_PKG_NAME "Microsoft.Z3.Sharp")
# Note: If multi-configuration generator support is ever fixed then these # set(PREFIX "${CMAKE_INSTALL_PREFIX}")
# scripts will be broken. # set(VERSION "${Z3_VERSION}")
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() endif()