Merge pull request #4767 from ethereum/cvc4Build

Add workarounds for building against CVC4 on ArchLinux.

Changelog.md

@@ -80,6 +80,7 @@ Compiler Features:
  * Removed ``pragma experimental "v0.5.0";``.
 
 Bugfixes:
+ * Build System: Support versions of CVC4 linked against CLN instead of GMP. In case of compilation issues due to the experimental SMT solver support, the solvers can be disabled when configuring the project with CMake using ``-DUSE_CVC4=OFF`` or ``-DUSE_Z3=OFF``.
  * Tests: Fix chain parameters to make ipc tests work with newer versions of cpp-ethereum.
  * Code Generator: Fix allocation of byte arrays (zeroed out too much memory).
  * Code Generator: Properly handle negative number literals in ABIEncoderV2.

cmake/FindCLN.cmake

@@ -0,0 +1,3 @@
+find_library(CLN_LIBRARY NAMES cln)
+include(FindPackageHandleStandardArgs)
+find_package_handle_standard_args(CLN DEFAULT_MSG CLN_LIBRARY)

cmake/FindCVC4.cmake

@@ -1,8 +1,26 @@
 if (USE_CVC4)
     find_path(CVC4_INCLUDE_DIR cvc4/cvc4.h)
-    find_library(CVC4_LIBRARY NAMES cvc4 )
+    find_library(CVC4_LIBRARY NAMES cvc4)
     include(FindPackageHandleStandardArgs)
     find_package_handle_standard_args(CVC4 DEFAULT_MSG CVC4_LIBRARY CVC4_INCLUDE_DIR)
+    if(CVC4_FOUND)
+        # CVC4 may depend on either CLN or GMP.
+        # We can assume that the one it requires is present on the system,
+        # so we quietly try to find both and link against them, if they are
+        # present.
+        find_package(CLN QUIET)
+        find_package(GMP QUIET)
+
+        set(CVC4_LIBRARIES ${CVC4_LIBRARY})
+
+        if (CLN_FOUND)
+            set(CVC4_LIBRARIES ${CVC4_LIBRARIES} ${CLN_LIBRARY})
+        endif ()
+
+        if (GMP_FOUND)
+            set(CVC4_LIBRARIES ${CVC4_LIBRARIES} ${GMP_LIBRARY})
+        endif ()
+    endif()
 else()
     set(CVC4_FOUND FALSE)
 endif()

libsolidity/CMakeLists.txt

@@ -11,17 +11,11 @@ else()
   list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/Z3Interface.cpp")
 endif()
 
-find_package(GMP QUIET)
 find_package(CVC4 QUIET)
 if (${CVC4_FOUND})
-  if (${GMP_FOUND})
+  include_directories(${CVC4_INCLUDE_DIR})
-    include_directories(${CVC4_INCLUDE_DIR})
+  add_definitions(-DHAVE_CVC4)
-    add_definitions(-DHAVE_CVC4)
+  message("CVC4 SMT solver found. This enables optional SMT checking with CVC4.")
-    message("CVC4 SMT solver and GMP found. This enables optional SMT checking with CVC4.")
-  else()
-    message("CVC4 SMT solver found but its dependency GMP was NOT found. Optional SMT checking with CVC4 will not be available. Please install GMP if it is desired.")
-    list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/CVC4Interface.cpp")
-  endif()
 else()
   list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/CVC4Interface.cpp")
 endif()
@@ -38,7 +32,6 @@ if (${Z3_FOUND})
   target_link_libraries(solidity PUBLIC ${Z3_LIBRARY})
 endif()
 
-if (${CVC4_FOUND} AND ${GMP_FOUND})
+if (${CVC4_FOUND})
-  target_link_libraries(solidity PUBLIC ${CVC4_LIBRARY})
+  target_link_libraries(solidity PUBLIC ${CVC4_LIBRARIES})
-  target_link_libraries(solidity PUBLIC ${GMP_LIBRARY})
 endif()

libsolidity/formal/CVC4Interface.h

@@ -21,8 +21,19 @@
 
 #include <boost/noncopyable.hpp>
 
+#if defined(__GLIBC__)
+// The CVC4 headers includes the deprecated system headers <ext/hash_map>
+// and <ext/hash_set>. These headers cause a warning that will break the
+// build, unless _GLIBCXX_PERMIT_BACKWARD_HASH is set.
+#define _GLIBCXX_PERMIT_BACKWARD_HASH
+#endif
+
 #include <cvc4/cvc4.h>
 
+#if defined(__GLIBC__)
+#undef _GLIBCXX_PERMIT_BACKWARD_HASH
+#endif
+
 namespace dev
 {
 namespace solidity