SMTChecker: Upgrade CVC4 to cvc5

Instead of compiling `solc` itself with CVC4 support, it is now enough
to have `cvc5` executable on PATH when running the compiler.
Instead of using API of CVC4, we now use SMT-LIB2 interface.
That means we write the queries to temporary SMT-LIB2 files and call
the solver process directly to run on the file.

Author: blishko

CMakeLists.txt

@@ -133,15 +133,15 @@ elseif (${Z3_FOUND})
   message("Z3 SMT solver found. This enables optional SMT checking with Z3.")
 endif()
 
-find_package(CVC4 QUIET)
-if (${CVC4_FOUND})
-  add_definitions(-DHAVE_CVC4)
-  message("CVC4 SMT solver found. This enables optional SMT checking with CVC4.")
+find_program(CVC5_PATH cvc5)
+if (CVC5_PATH)
+  add_compile_definitions(CVC5_PATH=${CVC5_PATH})
+  message("cvc5 SMT solver found. This enables optional SMT checking with cvc5.")
 endif()
 
-if (NOT (${Z3_FOUND} OR ${CVC4_FOUND}))
+if (NOT (${Z3_FOUND} OR CVC5_PATH))
   message("No SMT solver found (or it has been forcefully disabled). Optional SMT checking will not be available.\
-  \nPlease install Z3 or CVC4 or remove the option disabling them (USE_Z3, USE_CVC4).")
+  \nPlease install Z3 or cvc5 or remove the option disabling them (USE_Z3).")
 endif()
 
 add_subdirectory(libsolutil)

cmake/EthCompilerSettings.cmake

@@ -266,7 +266,6 @@ option(USE_Z3 "Allow compiling with Z3 SMT solver integration" ON)
 if(UNIX AND NOT APPLE)
 	option(USE_Z3_DLOPEN "Dynamically load the Z3 SMT solver instead of linking against it." OFF)
 endif()
-option(USE_CVC4 "Allow compiling with CVC4 SMT solver integration" ON)
 
 if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))
 	option(USE_LD_GOLD "Use GNU gold linker" ON)

cmake/FindCVC4.cmake

@@ -333,10 +333,7 @@ The following are dependencies for all builds of Solidity:
 +-----------------------------------+-------------------------------------------------------+
 | `z3`_ (version 4.8.16+, Optional) | For use with SMT checker.                             |
 +-----------------------------------+-------------------------------------------------------+
-| `cvc4`_ (Optional)                | For use with SMT checker.                             |
-+-----------------------------------+-------------------------------------------------------+
 
-.. _cvc4: https://cvc4.cs.stanford.edu/web/
 .. _Git: https://git-scm.com/download
 .. _Boost: https://www.boost.org
 .. _CMake: https://cmake.org/download/
@@ -543,12 +540,6 @@ Inside the build folder you can disable them, since they are enabled by default:
     # disables only Z3 SMT Solver.
     cmake .. -DUSE_Z3=OFF
 
-    # disables only CVC4 SMT Solver.
-    cmake .. -DUSE_CVC4=OFF
-
-    # disables both Z3 and CVC4
-    cmake .. -DUSE_CVC4=OFF -DUSE_Z3=OFF
-
 The Version String in Detail
 ============================
 

docs/installing-solidity.rst

@@ -822,10 +822,10 @@ which is primarily an SMT solver and makes `Spacer
 <https://github.com/uuverifiers/eldarica>`_ which does both.
 
 The user can choose which solvers should be used, if available, via the CLI
-option ``--model-checker-solvers {all,cvc4,eld,smtlib2,z3}`` or the JSON option
+option ``--model-checker-solvers {all,cvc5,eld,smtlib2,z3}`` or the JSON option
 ``settings.modelChecker.solvers=[smtlib2,z3]``, where:
 
-- ``cvc4`` is only available if the ``solc`` binary is compiled with it. Only BMC uses ``cvc4``.
+- ``cvc5`` is used via its binary which must be installed in the system. Only BMC uses ``cvc5``.
 - ``eld`` is used via its binary which must be installed in the system. Only CHC uses ``eld``, and only if ``z3`` is not enabled.
 - ``smtlib2`` outputs SMT/Horn queries in the `smtlib2 <http://smtlib.cs.uiowa.edu/>`_ format.
   These can be used together with the compiler's `callback mechanism <https://github.com/ethereum/solc-js>`_ so that
@@ -849,7 +849,7 @@ concerned about this option. More advanced users might apply this option to try
 alternative solvers on more complex problems.
 
 Please note that certain combinations of chosen engine and solver will lead to
-the SMTChecker doing nothing, for example choosing CHC and ``cvc4``.
+the SMTChecker doing nothing, for example choosing CHC and ``cvc5``.
 
 *******************************
 Abstraction and False Positives

docs/smtchecker.rst

@@ -485,7 +485,7 @@ Input Description
           "showUnsupported": true,
           // Choose which solvers should be used, if available.
           // See the Formal Verification section for the solvers description.
-          "solvers": ["cvc4", "smtlib2", "z3"],
+          "solvers": ["cvc5", "smtlib2", "z3"],
           // Choose which targets should be checked: constantCondition,
           // underflow, overflow, divByZero, balance, assert, popEmptyArray, outOfBounds.
           // If the option is not given all targets are checked by default,

docs/using-the-compiler.rst

@@ -20,12 +20,6 @@ else()
   set(z3_SRCS)
 endif()
 
-if (${CVC4_FOUND})
-  set(cvc4_SRCS CVC4Interface.cpp CVC4Interface.h)
-else()
-  set(cvc4_SRCS)
-endif()
-
 if (${USE_Z3_DLOPEN})
   file(GLOB Z3_HEADERS ${Z3_HEADER_PATH}/z3*.h)
   set(Z3_WRAPPER ${CMAKE_CURRENT_BINARY_DIR}/z3wrapper.cpp)
@@ -38,7 +32,7 @@ if (${USE_Z3_DLOPEN})
   set(z3_SRCS ${z3_SRCS} ${Z3_WRAPPER} Z3Loader.cpp Z3Loader.h)
 endif()
 
-add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS})
+add_library(smtutil ${sources} ${z3_SRCS})
 target_link_libraries(smtutil PUBLIC solutil Boost::boost)
 
 if (${USE_Z3_DLOPEN})
@@ -47,7 +41,3 @@ if (${USE_Z3_DLOPEN})
 elseif (${Z3_FOUND})
   target_link_libraries(smtutil PUBLIC z3::libz3)
 endif()
-
-if (${CVC4_FOUND})
-  target_link_libraries(smtutil PUBLIC CVC4::CVC4)
-endif()