Modify LDFLAGS to support shared libraries for Win (#1280)

* Use uintptr_t for pointer casts in Swig files

CVC4's Swig interface files were casting pointers to longs in multiple
instances. The problem with that is that on certain platforms *cough*
Windows/MinGW *cough* long is only 32-bit even when compiling a 64-bit
executable (they use the LLP64 data model). This made the compilation of
language bindings fail with MinGW. This commit changes the types to
uintptr_t defined in Swig's stdint.i.

* Modify LDFLAGS to support shared libraries for Win

This commit adds "-no-undefined" to the LDFLAGS of CVC4's library, which
is required for building DLLs (shared libraries on Windows). It also
adds "--export-all-symbols" to the linker flags of the parser to ensure
that there are no unresolved symbols when linking against it (see
comment in the Makefile.am for details).

* Fix for non-Windows builds

* add no-undefined to libcvc4compatjni

6 files changed, 22 insertions, 2 deletions

diff --git a/configure.ac b/configure.ac
index 85660f223..cb36c7a9d 100644
--- a/configure.ac
+++ b/configure.ac
@@ -1305,12 +1305,16 @@ LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 
 # visibility flag not supported for Windows builds
 # also increase default stack size for Windows binaries
+windows_build=no
 case $host_os in
   (*mingw*) FLAG_VISIBILITY_HIDDEN=
             cvc4_LDFLAGS=-Wl,--stack,134217728
             pcvc4_LDFLAGS=-Wl,--stack,134217728
+            windows_build=yes
 esac
 
+AM_CONDITIONAL([CVC4_WINDOWS_BUILD], [test "$windows_build" = "yes"])
+
 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
 AC_SUBST(cvc4_LDFLAGS)
 AC_SUBST(pcvc4_LDFLAGS)
diff --git a/src/Makefile.am b/src/Makefile.am
index 7f9d5a84b..b05a3503c 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -25,7 +25,9 @@ include @top_srcdir@/src/Makefile.theories
 
 lib_LTLIBRARIES = libcvc4.la
 
-libcvc4_la_LDFLAGS = -no-undefined -version-info $(LIBCVC4_VERSION)
+libcvc4_la_LDFLAGS = \
+	-no-undefined \
+	-version-info $(LIBCVC4_VERSION)
 
 # This "tricks" automake into linking us as a C++ library (rather than
 # as a C library, which messes up exception handling support)
diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index e7548bbe1..994054882 100644
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -59,6 +59,7 @@ if CVC4_LANGUAGE_BINDING_JAVA
 javalib_LTLIBRARIES += java/libcvc4jni.la
 javadata_DATA += CVC4.jar
 java_libcvc4jni_la_LDFLAGS = \
+	-no-undefined \
 	-module \
 	-shrext $(CVC4_JAVA_MODULE_EXT) \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
diff --git a/src/bindings/compat/java/Makefile.am b/src/bindings/compat/java/Makefile.am
index 5b052568d..eae498368 100644
--- a/src/bindings/compat/java/Makefile.am
+++ b/src/bindings/compat/java/Makefile.am
@@ -29,6 +29,7 @@ if CVC4_LANGUAGE_BINDING_JAVA
 javalib_LTLIBRARIES += libcvc4compatjni.la
 javadata_DATA += CVC4compat.jar
 libcvc4compatjni_la_LDFLAGS = \
+	-no-undefined \
 	-module \
 	-shrext $(CVC4_JAVA_MODULE_EXT) \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
diff --git a/src/compat/Makefile.am b/src/compat/Makefile.am
index df4603a9a..47c8a6a98 100644
--- a/src/compat/Makefile.am
+++ b/src/compat/Makefile.am
@@ -22,6 +22,7 @@ if CVC4_BUILD_LIBCOMPAT
 lib_LTLIBRARIES = libcvc4compat.la
 
 libcvc4compat_la_LDFLAGS = \
+	-no-undefined \
 	-version-info $(LIBCVC4COMPAT_VERSION)
 
 libcvc4compat_la_LIBADD = \
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index a316019fd..98b98ccaf 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -21,9 +21,20 @@ SUBDIRS = smt1 smt2 cvc tptp
 
 lib_LTLIBRARIES = libcvc4parser.la
 
-libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) \
+libcvc4parser_la_LDFLAGS = \
+	$(ANTLR_LDFLAGS) \
+	-no-undefined \
 	-version-info $(LIBCVC4PARSER_VERSION)
 
+if CVC4_WINDOWS_BUILD
+# -Wl,--export-all-symbols makes sure that all symbols are exported when
+# building a DLL. This option is on by default but gets disabled for the parser
+# library because the generated lexer/parser files define some functions as
+# __declspec(dllexport), which leads to lots of unresolved symbols when linking
+# against libcvc4parser.
+libcvc4parser_la_LDFLAGS += -Wl,--export-all-symbols
+endif
+
 libcvc4parser_la_LIBADD = \
 	@builddir@/smt1/libparsersmt1.la \
 	@builddir@/smt2/libparsersmt2.la \