Refactor ANTLR3 dependency (#6202)

This PR refactors our first, and arguably most fragile, dependency.
Right now all dependencies need to be manually installed (by calling the appropriate contrib/get-X script). For optional dependencies, we additionally need to enable them when calling the configure script (or via ccmake).
This PR is the first step in refactoring all dependencies to be automatically build (if required) as an external project.

Note that this not only eliminates the need to call contrib scripts, but also simplifies cross compilation: as all dependencies are now built within the build folders, every build folder has its own copy which may use different toolchains.

4 files changed, 278 insertions, 39 deletions

diff --git a/cmake/FindANTLR.cmake b/cmake/FindANTLR.cmake
deleted file mode 100644
index 5fdba3f3b..000000000
--- a/cmake/FindANTLR.cmake
+++ /dev/null
@@ -1,39 +0,0 @@
-#####################
-## FindANTLR.cmake
-## Top contributors (to current version):
-##   Mathias Preiner, Aina Niemetz
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
-## in the top-level source directory and their institutional affiliations.
-## All rights reserved.  See the file COPYING in the top-level source
-## directory for licensing information.
-##
-# Find ANTLR
-# ANTLR_FOUND - system has ANTLR lib
-# ANTLR_BINARY - the ANTLR binary
-# ANTLR_INCLUDE_DIR - the ANTLR include directory
-# ANTLR_LIBRARIES - Libraries needed to use ANTLR
-
-find_program(ANTLR_BINARY NAMES antlr3)
-find_path(ANTLR_INCLUDE_DIR NAMES antlr3.h)
-find_library(ANTLR_LIBRARIES NAMES antlr3c antlr3c-static)
-
-# Check if antlr3FileStreamNew is available. If not we have to
-# define CVC4_ANTLR3_OLD_INPUT_STREAM (src/parser/CMakeLists.txt).
-if(ANTLR_INCLUDE_DIR)
-  include(CheckSymbolExists)
-  set(CMAKE_REQUIRED_INCLUDES ${ANTLR_INCLUDE_DIR})
-  set(CMAKE_REQUIRED_LIBRARIES ${ANTLR_LIBRARIES})
-  check_symbol_exists(
-    antlr3FileStreamNew "antlr3defs.h" HAVE_ANTLR3_FILE_STREAM_NEW)
-endif()
-
-include(FindPackageHandleStandardArgs)
-find_package_handle_standard_args(
-  ANTLR DEFAULT_MSG ANTLR_BINARY ANTLR_INCLUDE_DIR ANTLR_LIBRARIES)
-
-mark_as_advanced(ANTLR_BINARY ANTLR_INCLUDE_DIR ANTLR_LIBRARIES
-                 HAVE_ANTLR3_FILE_STREAM_NEW)
-if(ANTLR_LIBRARIES)
-  message(STATUS "Found ANTLR libs: ${ANTLR_LIBRARIES}")
-endif()
diff --git a/cmake/FindANTLR3.cmake b/cmake/FindANTLR3.cmake
new file mode 100644
index 000000000..2ca66ff0b
--- /dev/null
+++ b/cmake/FindANTLR3.cmake
@@ -0,0 +1,128 @@
+#####################
+## FindANTLR3.cmake
+## Top contributors (to current version):
+##   Gereon Kremer, Mathias Preiner, Aina Niemetz
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.
+##
+# Find ANTLR3
+# ANTLR3_FOUND - should always be true
+# ANTLR3 - target for the ANTLR3 runtime
+# ANTLR3_COMMAND - command line to run ANTLR3
+
+include(deps-helper)
+
+find_program(ANTLR3_BINARY NAMES antlr3)
+find_path(ANTLR3_INCLUDE_DIR NAMES antlr3.h)
+find_library(ANTLR3_RUNTIME NAMES antlr3c)
+
+set(ANTLR3_FOUND_SYSTEM FALSE)
+if(ANTLR3_BINARY AND ANTLR3_INCLUDE_DIR AND ANTLR3_RUNTIME)
+    set(ANTLR3_FOUND_SYSTEM TRUE)
+
+    # Parse ANTLR3 version
+    file(STRINGS "${ANTLR3_INCLUDE_DIR}/antlr3config.h" ANTLR3_VERSION REGEX "^#define VERSION \"[0-9.]+\"")
+    string(REGEX MATCH "[0-9.]+" ANTLR3_VERSION "${ANTLR3_VERSION}")
+
+    check_system_version("ANTLR3")
+endif()
+
+if(NOT ANTLR3_FOUND_SYSTEM)
+    include(ExternalProject)
+
+    set(ANTLR3_VERSION "3.4")
+
+    # Download antlr generator jar
+    ExternalProject_Add(
+        ANTLR3-EP-jar
+        PREFIX ${DEPS_PREFIX}
+        URL https://www.antlr3.org/download/antlr-${ANTLR3_VERSION}-complete.jar
+        URL_HASH SHA1=5cab59d859caa6598e28131d30dd2e89806db57f
+        DOWNLOAD_NO_EXTRACT ON
+        CONFIGURE_COMMAND ""
+        BUILD_COMMAND ""
+        INSTALL_COMMAND ${CMAKE_COMMAND} -E copy
+            <SOURCE_DIR>/../antlr-3.4-complete.jar
+            <INSTALL_DIR>/share/java/antlr-3.4-complete.jar
+        BUILD_BYPRODUCTS <INSTALL_DIR>/share/java/antlr-3.4-complete.jar
+    )
+
+    # Download config guess
+    ExternalProject_Add(
+        ANTLR3-EP-config.guess
+        PREFIX ${DEPS_PREFIX}
+        URL "http://git.savannah.gnu.org/gitweb/?p=config.git\\\;a=blob_plain\\\;f=config.guess\\\;hb=HEAD"
+        DOWNLOAD_NAME config.guess
+        DOWNLOAD_NO_EXTRACT ON
+        CONFIGURE_COMMAND ""
+        BUILD_COMMAND ""
+        INSTALL_COMMAND ${CMAKE_COMMAND} -E copy <SOURCE_DIR>/../config.guess <INSTALL_DIR>/share/config.guess
+        BUILD_BYPRODUCTS <INSTALL_DIR>/share/config.guess
+    )
+
+    if(CMAKE_SYSTEM_PROCESSOR MATCHES ".*64$")
+        set(64bit "--enable-64bit")
+    else()
+        unset(64bit)
+    endif()
+
+    # Download, build and install antlr3 runtime
+    ExternalProject_Add(
+        ANTLR3-EP-runtime
+        DEPENDS ANTLR3-EP-config.guess
+        PREFIX ${DEPS_PREFIX}
+        URL https://www.antlr3.org/download/C/libantlr3c-3.4.tar.gz
+        URL_HASH SHA1=faa9ab43ab4d3774f015471c3f011cc247df6a18
+        CONFIGURE_COMMAND ${CMAKE_COMMAND} -E copy 
+            <SOURCE_DIR>/../config.guess <SOURCE_DIR>/config.guess
+        COMMAND sed "s/avr32 \\\\/avr32 | aarch64 \\\\/"
+            <SOURCE_DIR>/config.sub > <SOURCE_DIR>/config.sub.new
+        COMMAND ${CMAKE_COMMAND} -E copy
+            <SOURCE_DIR>/config.sub.new <SOURCE_DIR>/config.sub
+        COMMAND ${CMAKE_COMMAND} -E copy_directory <SOURCE_DIR>/include include/
+        COMMAND <SOURCE_DIR>/configure
+            --with-pic
+            --disable-antlrdebug
+            --prefix=<INSTALL_DIR>
+            --srcdir=<SOURCE_DIR>
+            --disable-shared
+            --enable-static
+            ${64bit}
+            --host=${TOOLCHAIN_PREFIX}
+        BUILD_BYPRODUCTS <INSTALL_DIR>/lib/libantlr3c.a
+    )
+
+    find_package(Java REQUIRED)
+    set(ANTLR3_BINARY ${Java_JAVA_EXECUTABLE}
+        -cp "${DEPS_BASE}/share/java/antlr-3.4-complete.jar" org.antlr.Tool)
+    set(ANTLR3_INCLUDE_DIR "${DEPS_BASE}/include/")
+    set(ANTLR3_RUNTIME "${DEPS_BASE}/lib/libantlr3c.a")
+endif()
+
+set(ANTLR3_FOUND TRUE)
+# This may not be a single binary: the EP has a whole commandline
+# We thus do not make this an executable target.
+# Just call ${ANTLR3_COMMAND} instead.
+set(ANTLR3_COMMAND ${ANTLR3_BINARY} CACHE STRING "run ANTLR3" FORCE)
+
+add_library(ANTLR3 STATIC IMPORTED GLOBAL)
+set_target_properties(ANTLR3 PROPERTIES IMPORTED_LOCATION "${ANTLR3_RUNTIME}")
+set_target_properties(ANTLR3 PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${ANTLR3_INCLUDE_DIR}")
+
+mark_as_advanced(ANTLR3_BINARY)
+mark_as_advanced(ANTLR3_COMMAND)
+mark_as_advanced(ANTLR3_FOUND)
+mark_as_advanced(ANTLR3_FOUND_SYSTEM)
+mark_as_advanced(ANTLR3_INCLUDE_DIR)
+mark_as_advanced(ANTLR3_JAR)
+mark_as_advanced(ANTLR3_RUNTIME)
+
+if(ANTLR3_FOUND_SYSTEM)
+    message(STATUS "Found ANTLR3 runtime: ${ANTLR3_RUNTIME}")
+else()
+    message(STATUS "Building ANTLR3 runtime: ${ANTLR3_RUNTIME}")
+    add_dependencies(ANTLR3 ANTLR3-EP-runtime ANTLR3-EP-jar)
+endif()
diff --git a/cmake/FindDummy.cmake.template b/cmake/FindDummy.cmake.template
new file mode 100644
index 000000000..ecb7f672b
--- /dev/null
+++ b/cmake/FindDummy.cmake.template
@@ -0,0 +1,100 @@
+#####################
+## FindDummy.cmake
+## Top contributors (to current version):
+##   Gereon Kremer
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.
+##
+# This file serves as a template for how the FindX.cmake scripts should
+# work.
+#
+# Find Dummy library
+# Exported variables:
+#   Dummy_FOUND - we have the Dummy lib, always true
+#   Dummy_FOUND_SYSTEM - we use the system version
+# Exported targets:
+#   Dummy - an imported library target
+
+# provides some utility definitions
+include(deps-helper)
+
+# initial setup, for example load Java, Python, ...
+
+# first look for the library using the standard procedures
+find_path(Dummy_INCLUDE_DIR NAMES dummy/dummy.h)
+find_library(Dummy_LIBRARIES NAMES dummy)
+
+# check whether we found something
+set(Dummy_FOUND_SYSTEM FALSE)
+if(Dummy_INCLUDE_DIR AND Dummy_LIBRARIES)
+    # was installed system wide
+    set(Dummy_FOUND_SYSTEM TRUE)
+
+    # parse the version
+    file(STRINGS ${Dummy_INCLUDE_DIR}/dummy/dummy.h Dummy_VERSION REGEX "^#define DUMMY_VERSION .*")
+	  string(REGEX MATCH "[0-9]+\\.[0-9]+\\.[0-9]+" Dummy_VERSION "${Dummy_VERSION}")
+
+    # check whether the version satisfies the version requirement
+    # this may reset the Dummy_FOUND_SYSTEM variable
+    check_system_version("Dummy")
+endif()
+
+# not found or version too old
+if(NOT Dummy_FOUND_SYSTEM)
+    # we install the library with an external project
+    include(ExternalProject)
+
+    # check for cases where the external project is known to fail
+    # it might make sense to specify a reason
+    fail_if_cross_compiling("Windows" "" "Dummy" "some reason")
+    fail_if_cross_compiling("" "arm" "Dummy" "some reason")
+
+    # declare some release, version, tag, commit
+    set(Dummy_VERSION "1.2.3")
+    # do whatever is necessary
+    # - set the proper install prefix
+    # - prefer URL to GIT (to avoid rebuilds)
+    # - only build / install static versions if possible
+    # - pass ${TOOLCHAIN_PREFIX}
+    ExternalProject_Add(
+        Dummy-EP
+        PREFIX ${DEPS_PREFIX}
+        URL https://dummy.org/download/dummy-${Dummy_VERSION}.tar.bz2
+        URL_HASH SHA1=abc123
+        CMAKE_ARGS
+          -DCMAKE_INSTALL_PREFIX=<INSTALL_DIR>
+          -DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE}
+    )
+    # we may have dependencies on some other library
+    add_dependencies(Dummy-EP Foo)
+
+    # set the variables like the find_* commands at the top
+    set(Dummy_INCLUDE_DIR "${DEPS_BASE}/include/")
+    set(Dummy_LIBRARIES "${DEPS_BASE}/lib/libdummy.a")
+endif()
+
+# just set this to true
+set(Dummy_FOUND TRUE)
+
+# now create a target for the library
+add_library(Dummy STATIC IMPORTED GLOBAL)
+set_target_properties(Dummy PROPERTIES IMPORTED_LOCATION "${Dummy_LIBRARIES}")
+set_target_properties(Dummy PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${Dummy_INCLUDE_DIR}")
+
+# mark all variables as advanced
+mark_as_advanced(Dummy_FOUND)
+mark_as_advanced(Dummy_FOUND_SYSTEM)
+mark_as_advanced(Dummy_INCLUDE_DIR)
+mark_as_advanced(Dummy_LIBRARIES)
+
+# print an appropriate message
+if(Dummy_FOUND_SYSTEM)
+    message(STATUS "Found Dummy ${Dummy_VERSION}: ${Dummy_LIBRARIES}")
+else()
+    message(STATUS "Building Dummy ${Dummy_VERSION}: ${Dummy_LIBRARIES}")
+    # make sure the external project is actually build
+    add_dependencies(Dummy Dummy-EP)
+endif()
diff --git a/cmake/deps-helper.cmake b/cmake/deps-helper.cmake
new file mode 100644
index 000000000..bdc3e5de1
--- /dev/null
+++ b/cmake/deps-helper.cmake
@@ -0,0 +1,50 @@
+# where to build dependencies
+set(DEPS_PREFIX "${CMAKE_BINARY_DIR}/deps")
+# base path to installed dependencies
+set(DEPS_BASE "${CMAKE_BINARY_DIR}/deps")
+# CMake wants directories specified via INTERFACE_INCLUDE_DIRECTORIES
+# (and similar) to exist when target property is set.
+file(MAKE_DIRECTORY "${DEPS_BASE}/include/")
+
+macro(check_system_version name)
+    # find_package sets this variable when called with a version
+    # https://cmake.org/cmake/help/latest/command/find_package.html#version-selection
+    # we ignore the EXACT option and version ranges here
+    if (${name}_FIND_VERSION)
+        if(${name}_VERSION VERSION_LESS ${name}_FIND_VERSION)
+            message(VERBOSE "System version for ${name} has incompatible \
+version: required ${${name}_FIND_VERSION} but found ${${name}_VERSION}")
+            set(${name}_FOUND_SYSTEM FALSE)
+        endif()
+    endif()
+endmacro(check_system_version)
+
+# fail if we are cross compiling as indicated by name and processor
+# we are cross compiling if
+# - CMAKE_SYSTEM_NAME has been changed to ${name}
+# - CMAKE_SYSTEM_PROCESSOR has been changed to ${processor}
+function(fail_if_cross_compiling name processor target error)
+    set(FAIL FALSE)
+    if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "${CMAKE_HOST_SYSTEM_NAME}")
+        if(NOT "${name}" STREQUAL "")
+            if("${CMAKE_SYSTEM_NAME}" STREQUAL "${name}")
+                set(FAIL TRUE)
+            endif()
+        endif()
+    endif()
+    if(NOT "${CMAKE_SYSTEM_PROCESSOR}" STREQUAL "${CMAKE_HOST_SYSTEM_PROCESSOR}")
+        if(NOT "${processor}" STREQUAL "")
+            if("${CMAKE_SYSTEM_PROCESSOR}" STREQUAL "${processor}")
+                set(FAIL TRUE)
+            endif()
+        endif()
+    endif()
+    if(FAIL)
+        message(SEND_ERROR
+            "We are cross compiling from \
+${CMAKE_HOST_SYSTEM_NAME}-${CMAKE_HOST_SYSTEM_PROCESSOR} to \
+${CMAKE_SYSTEM_NAME}-${CMAKE_SYSTEM_PROCESSOR}.\n"
+            "This is not supported by ${target}:\n"
+            "${error}")
+    endif()
+endfunction(fail_if_cross_compiling)