From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 19 Sep 2018 00:20:25 +0000 (-0700)
Subject: cmake: Add support for cross-compiling for Windows.
X-Git-Tag: cvc5-1.0.0~4538
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ed8d326cbdec820d347d8b4b5ee7b23c3367d169;p=cvc5.git

cmake: Add support for cross-compiling for Windows.
---

diff --git a/cmake/ConfigureCVC4.cmake b/cmake/ConfigureCVC4.cmake
index 18061c778..f60e9043e 100644
--- a/cmake/ConfigureCVC4.cmake
+++ b/cmake/ConfigureCVC4.cmake
@@ -43,7 +43,18 @@ endif()
 check_include_file(unistd.h HAVE_UNISTD_H)
 check_include_file_cxx(ext/stdio_filebuf.h HAVE_EXT_STDIO_FILEBUF_H)
 
-check_symbol_exists(clock_gettime "time.h" HAVE_CLOCK_GETTIME)
+# For Windows builds check if clock_gettime is available via -lpthread
+# (pthread_time.h).
+if(CVC4_WINDOWS_BUILD)
+  set(CMAKE_REQUIRED_FLAGS -pthread)
+  check_symbol_exists(clock_gettime "time.h" HAVE_CLOCK_GETTIME)
+  unset(CMAKE_REQUIRED_FLAGS)
+  if(HAVE_CLOCK_GETTIME)
+    add_c_cxx_flag(-pthread)
+  endif()
+else()
+  check_symbol_exists(clock_gettime "time.h" HAVE_CLOCK_GETTIME)
+endif()
 check_symbol_exists(ffs "strings.h" HAVE_FFS)
 check_symbol_exists(optreset "getopt.h" HAVE_DECL_OPTRESET)
 check_symbol_exists(sigaltstack "signal.h" HAVE_SIGALTSTACK)
diff --git a/cmake/Toolchain-mingw64.cmake b/cmake/Toolchain-mingw64.cmake
new file mode 100644
index 000000000..85c0622ed
--- /dev/null
+++ b/cmake/Toolchain-mingw64.cmake
@@ -0,0 +1,23 @@
+# Toolchain file for building for Windows from Ubuntu.
+#
+# Use: cmake .. -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake
+
+SET(CMAKE_SYSTEM_NAME Windows)
+
+set(TOOLCHAIN_PREFIX x86_64-w64-mingw32)
+
+SET(CMAKE_C_COMPILER ${TOOLCHAIN_PREFIX}-gcc)
+SET(CMAKE_CXX_COMPILER ${TOOLCHAIN_PREFIX}-g++)
+SET(CMAKE_RC_COMPILER ${TOOLCHAIN_PREFIX}-windres)
+
+# Set target environment path
+SET(CMAKE_FIND_ROOT_PATH /usr/${TOOLCHAIN_PREFIX})
+
+# Adjust the default behaviour of the find_XXX() commands:
+# search headers and libraries in the target environment, search
+# programs in the host environment
+set(CMAKE_FIND_ROOT_PATH_MODE_PROGRAM NEVER)
+set(CMAKE_FIND_ROOT_PATH_MODE_LIBRARY BOTH)
+set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE BOTH)
+
+set(CVC4_WINDOWS_BUILD TRUE)
diff --git a/configure.sh b/configure.sh
index 8c41f9c7e..52c280a56 100755
--- a/configure.sh
+++ b/configure.sh
@@ -19,6 +19,7 @@ General options;
   --name=STR               use custom build directory name
   --best                   turn on dependences known to give best performance
   --gpl                    permit GPL dependences, if available
+  --win64                  cross-compile for Windows 64 bit
 
 
 Features:
@@ -66,6 +67,7 @@ Optional Path to Optional Packages:
   --cryptominisat-dir=PATH path to top level of cryptominisat source tree
   --cxxtest-dir=DIR        path to CxxTest installation
   --glpk-dir=PATH          path to top level of glpk installation
+  --gmp-dir=PATH           path to top level of GMP installation
   --lfsc-dir=PATH          path to top level of lfsc source tree
   --symfpu-dir=PATH        path to top level of symfpu source tree
 
@@ -112,6 +114,7 @@ debug_symbols=default
 debug_context_mm=default
 dumping=default
 gpl=default
+win64=default
 glpk=default
 lfsc=default
 muzzle=default
@@ -137,6 +140,7 @@ antlr_dir=default
 cadical_dir=default
 cryptominisat_dir=default
 glpk_dir=default
+gmp_dir=default
 lfsc_dir=default
 symfpu_dir=default
 
@@ -201,6 +205,9 @@ do
     --gpl) gpl=ON;;
     --no-gpl) gpl=OFF;;
 
+    --win64) win64=ON;;
+    --no-win64) win64=OFF;;
+
     --glpk) glpk=ON;;
     --no-glpk) glpk=OFF;;
 
@@ -281,6 +288,9 @@ do
     --glpk-dir) die "missing argument to $1 (try -h)" ;;
     --glpk-dir=*) glpk_dir=${1##*=} ;;
 
+    --gmp-dir) die "missing argument to $1 (try -h)" ;;
+    --gmp-dir=*) gmp_dir=${1##*=} ;;
+
     --lfsc-dir) die "missing argument to $1 (try -h)" ;;
     --lfsc-dir=*) lfsc_dir=${1##*=} ;;
 
@@ -305,7 +315,8 @@ done
 
 cmake_opts=""
 
-[ $buildtype != default ] && cmake_opts="$cmake_opts -DCMAKE_BUILD_TYPE=$buildtype"
+[ $buildtype != default ] \
+  && cmake_opts="$cmake_opts -DCMAKE_BUILD_TYPE=$buildtype"
 
 [ $asan != default ] \
   && cmake_opts="$cmake_opts -DENABLE_ASAN=$asan" \
@@ -331,6 +342,9 @@ cmake_opts=""
 [ $gpl != default ] \
   && cmake_opts="$cmake_opts -DENABLE_GPL=$gpl" \
   && [ $gpl = ON ] &&  build_dir="$build_dir-gpl"
+[ $win64 != default ] \
+  && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake" \
+  && [ $win64 = ON ] &&  build_dir="$build_dir-win64"
 [ $muzzle != default ] \
   && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle" \
   && [ $muzzle = ON ] &&  build_dir="$build_dir-muzzle"
@@ -407,6 +421,8 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DCRYPTOMINISAT_DIR=$cryptominisat_dir"
 [ "$glpk_dir" != default ] \
   && cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir"
+[ "$gmp_dir" != default ] \
+  && cmake_opts="$cmake_opts -DGMP_DIR=$gmp_dir"
 [ "$lfsc_dir" != default ] \
   && cmake_opts="$cmake_opts -DLFSC_DIR=$lfsc_dir"
 [ "$symfpu_dir" != default ] \
@@ -420,12 +436,21 @@ if [ -n "$build_name" ]; then
   # If a build name is specified just create directory 'build_name' for the
   # current build.
   build_dir=$build_name
+
+  # The cmake toolchain can't be changed once it is configured in $build_dir.
+  # Thus, remove $build_dir and create an empty directory.
+  [ $win64 = ON ] && [ -e "$build_dir" ] && rm -r "$build_dir"
   mkdir -p "$build_name"
 else
   # If no build name is specified create 'cmake-builds' directory and create
   # the current build directory. Set symlink 'cmake-builds/build/' to current
   # build.
   build_dir="$build_prefix$build_dir"
+
+  # The cmake toolchain can't be changed once it is configured in $build_dir.
+  # Thus, remove $build_dir and create an empty directory.
+  [ $win64 = ON ] && [ -e "cmake-build/$build_dir" ] \
+    && rm -r "cmake-builds/$build_dir"
   mkdir -p "cmake-builds/$build_dir"
   cd cmake-builds || exit 1
   [ -e build ] && rm build
diff --git a/contrib/get-win-dependencies b/contrib/get-win-dependencies
index 5ca969f6b..f3fbd6cf7 100755
--- a/contrib/get-win-dependencies
+++ b/contrib/get-win-dependencies
@@ -24,7 +24,7 @@ while getopts ":s" opt; do
 done
 
 if [ -z "$HOST" ]; then
-  HOST=i686-w64-mingw32
+  HOST=x86_64-w64-mingw32
   echo "WARNING:"
   echo "WARNING: Using default HOST value: $HOST"
   echo "WARNING: You should probably run this script like this:"
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index b18573fe5..6cde56c62 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -95,3 +95,13 @@ target_compile_definitions(cvc4parser PRIVATE -D__BUILDING_CVC4PARSERLIB)
 target_link_libraries(cvc4parser cvc4 ${ANTLR_LIBRARIES})
 target_include_directories(cvc4parser PRIVATE ${ANTLR_INCLUDE_DIR})
 install(TARGETS cvc4parser DESTINATION lib)
+
+# The generated lexer/parser files define some functions as
+# __declspec(dllexport) via the ANTLR3_API macro, which leads to lots of
+# unresolved symbols when linking against libcvc4parser.
+# -Wl,--export-all-symbols makes sure that all symbols are exported when
+# building a DLL.
+if(CVC4_WINDOWS_BUILD)
+  set_target_properties(cvc4parser
+    PROPERTIES LINK_FLAGS "-Wl,--export-all-symbols")
+endif()