Remove Autoconf/Makefile build system and adjust the TravisCI

configuration, TravisCI scripts and Dockerfile build appropriately.

There are a bunch of clean ups this enables but this commit doesn't
attempt them. We can do that in future commits.

2 files changed, 68 insertions, 167 deletions

diff --git a/.travis/klee.sh b/.travis/klee.sh
index 119fbb47..33299780 100755
--- a/.travis/klee.sh
+++ b/.travis/klee.sh
@@ -3,9 +3,6 @@
 set -e
 : ${SOLVERS?"Solvers must be specified"}
 
-# Calculate LLVM branch name to retrieve missing files from
-SVN_BRANCH="release_$( echo ${LLVM_VERSION} | sed 's/\.//g')"
-
 ###############################################################################
 # Select the compiler to use to generate LLVM bitcode
 ###############################################################################
@@ -28,18 +25,10 @@ if [ "${KLEE_UCLIBC}" != "0" ]; then
     cd klee-uclibc
     ./configure --make-llvm-lib --with-cc "${KLEE_CC}" --with-llvm-config /usr/bin/llvm-config-${LLVM_VERSION}
     make
-    if [ "X${USE_CMAKE}" == "X1" ]; then
-      KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=TRUE -DKLEE_UCLIBC_PATH=$(pwd) -DENABLE_POSIX_RUNTIME=TRUE"
-    else
-      KLEE_UCLIBC_CONFIGURE_OPTION="--with-uclibc=$(pwd) --enable-posix-runtime"
-    fi
+    KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=TRUE -DKLEE_UCLIBC_PATH=$(pwd) -DENABLE_POSIX_RUNTIME=TRUE"
     cd ../
 else
-    if [ "X${USE_CMAKE}" == "X1" ]; then
-      KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=FALSE -DENABLE_POSIX_RUNTIME=FALSE"
-    else
-      KLEE_UCLIBC_CONFIGURE_OPTION=""
-    fi
+    KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=FALSE -DENABLE_POSIX_RUNTIME=FALSE"
 fi
 
 COVERAGE_FLAGS=""
@@ -53,60 +42,37 @@ fi
 ###############################################################################
 SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /')
 
-if [ "X${USE_CMAKE}" == "X1" ]; then
-  # Set CMake configure options
-  KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=OFF"
-  KLEE_STP_CONFIGURE_OPTION="-DENABLE_SOLVER_STP=OFF"
-  KLEE_METASMT_CONFIGURE_OPTION="-DENABLE_SOLVER_METASMT=OFF"
-  for solver in ${SOLVER_LIST}; do
-    echo "Setting CMake configuration option for ${solver}"
-    case ${solver} in
-    STP)
-      KLEE_STP_CONFIGURE_OPTION="-DENABLE_SOLVER_STP=TRUE -DSTP_DIR=${BUILD_DIR}/stp/build"
-      ;;
-    Z3)
-      echo "Z3"
-      KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=TRUE"
-      ;;
-    metaSMT)
-      echo "metaSMT"
-      if [ "X${METASMT_DEFAULT}" == "X" ]; then
-        METASMT_DEFAULT=STP
-      fi
-      KLEE_METASMT_CONFIGURE_OPTION="-DENABLE_SOLVER_METASMT=TRUE -DmetaSMT_DIR=${BUILD_DIR}/metaSMT/build -DMETASMT_DEFAULT_BACKEND=${METASMT_DEFAULT}"
-      ;;
-    *)
-      echo "Unknown solver ${solver}"
-      exit 1
-    esac
-  done
-  TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "-DENABLE_TCMALLOC=TRUE" || echo "-DENABLE_TCMALLOC=FALSE")
-else
-  KLEE_Z3_CONFIGURE_OPTION=""
-  KLEE_STP_CONFIGURE_OPTION=""
-  KLEE_METASMT_CONFIGURE_OPTION=""
-  for solver in ${SOLVER_LIST}; do
-    echo "Setting configuration option for ${solver}"
-    case ${solver} in
-    STP)
-      KLEE_STP_CONFIGURE_OPTION="--with-stp=${BUILD_DIR}/stp/build"
-      ;;
-    Z3)
-      echo "Z3"
-      KLEE_Z3_CONFIGURE_OPTION="--with-z3=/usr"
-      ;;
-    metaSMT)
-      echo "metaSMT"
-      KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root --with-metasmt-default-backend=${METASMT_DEFAULT}"
-      ;;
-    *)
-      echo "Unknown solver ${solver}"
-      exit 1
-    esac
-  done
+# Set CMake configure options
+KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=OFF"
+KLEE_STP_CONFIGURE_OPTION="-DENABLE_SOLVER_STP=OFF"
+KLEE_METASMT_CONFIGURE_OPTION="-DENABLE_SOLVER_METASMT=OFF"
+for solver in ${SOLVER_LIST}; do
+  echo "Setting CMake configuration option for ${solver}"
+  case ${solver} in
+  STP)
+    KLEE_STP_CONFIGURE_OPTION="-DENABLE_SOLVER_STP=TRUE -DSTP_DIR=${BUILD_DIR}/stp/build"
+    ;;
+  Z3)
+    echo "Z3"
+    KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=TRUE"
+    ;;
+  metaSMT)
+    echo "metaSMT"
+    if [ "X${METASMT_DEFAULT}" == "X" ]; then
+      METASMT_DEFAULT=STP
+    fi
+    KLEE_METASMT_CONFIGURE_OPTION="-DENABLE_SOLVER_METASMT=TRUE -DmetaSMT_DIR=${BUILD_DIR}/metaSMT/build -DMETASMT_DEFAULT_BACKEND=${METASMT_DEFAULT}"
+    ;;
+  *)
+    echo "Unknown solver ${solver}"
+    exit 1
+  esac
+done
 
-  TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "--with-tcmalloc" || echo "--without-tcmalloc")
-fi
+###############################################################################
+# Handle additional configure flags
+###############################################################################
+TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "-DENABLE_TCMALLOC=TRUE" || echo "-DENABLE_TCMALLOC=FALSE")
 
 ###############################################################################
 # Handle Sanitizer flags
@@ -133,95 +99,50 @@ fi
 mkdir klee
 cd klee
 
-if [ "X${USE_CMAKE}" == "X1" ]; then
-  GTEST_SRC_DIR="${BUILD_DIR}/test-utils/googletest-release-1.7.0/"
-  if [ "X${DISABLE_ASSERTIONS}" == "X1" ]; then
-    KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=FALSE"
-  else
-    KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=TRUE"
-  fi
+GTEST_SRC_DIR="${BUILD_DIR}/test-utils/googletest-release-1.7.0/"
+if [ "X${DISABLE_ASSERTIONS}" == "X1" ]; then
+  KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=FALSE"
+else
+  KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=TRUE"
+fi
 
-  if [ "X${ENABLE_OPTIMIZED}" == "X1" ]; then
-    CMAKE_BUILD_TYPE="RelWithDebInfo"
-  else
-    CMAKE_BUILD_TYPE="Debug"
-  fi
-  # Compute CMake build type
-  CXXFLAGS="${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}" \
-  CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \
-  cmake \
-    -DLLVM_CONFIG_BINARY="${LLVM_CONFIG}" \
-    -DLLVMCC="${KLEE_CC}" \
-    -DLLVMCXX="${KLEE_CXX}" \
-    ${KLEE_STP_CONFIGURE_OPTION} \
-    ${KLEE_Z3_CONFIGURE_OPTION} \
-    ${KLEE_METASMT_CONFIGURE_OPTION} \
-    ${KLEE_UCLIBC_CONFIGURE_OPTION} \
-    ${TCMALLOC_OPTION} \
-    -DGTEST_SRC_DIR=${GTEST_SRC_DIR} \
-    -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} \
-    ${KLEE_ASSERTS_OPTION} \
-    -DENABLE_UNIT_TESTS=TRUE \
-    -DENABLE_SYSTEM_TESTS=TRUE \
-    -DLIT_ARGS="-v" \
-    ${KLEE_SRC}
-  make
+if [ "X${ENABLE_OPTIMIZED}" == "X1" ]; then
+  CMAKE_BUILD_TYPE="RelWithDebInfo"
 else
-  # Build KLEE
-  # Note: ENABLE_SHARED=0 is required because llvm-2.9 is incorectly packaged
-  # and is missing the shared library that was supposed to be built that the build
-  # system will try to use by default.
-  ${KLEE_SRC}/configure --with-llvmsrc=${LLVM_BUILD_DIR} \
-              --with-llvmobj=${LLVM_BUILD_DIR} \
-              --with-llvmcc=${KLEE_CC} \
-              --with-llvmcxx=${KLEE_CXX} \
-              ${KLEE_STP_CONFIGURE_OPTION} \
-              ${KLEE_Z3_CONFIGURE_OPTION} \
-              ${KLEE_METASMT_CONFIGURE_OPTION} \
-              ${KLEE_UCLIBC_CONFIGURE_OPTION} \
-              ${TCMALLOC_OPTION} \
-              CXXFLAGS="${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}" \
-              CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \
-              LDFLAGS="${SANITIZER_LD_FLAGS}"
-  make  DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \
-        ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \
-        ENABLE_SHARED=0
+  CMAKE_BUILD_TYPE="Debug"
 fi
 
+# TODO: We should support Ninja too
+# Configure KLEE
+CXXFLAGS="${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}" \
+CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \
+cmake \
+  -DLLVM_CONFIG_BINARY="${LLVM_CONFIG}" \
+  -DLLVMCC="${KLEE_CC}" \
+  -DLLVMCXX="${KLEE_CXX}" \
+  ${KLEE_STP_CONFIGURE_OPTION} \
+  ${KLEE_Z3_CONFIGURE_OPTION} \
+  ${KLEE_METASMT_CONFIGURE_OPTION} \
+  ${KLEE_UCLIBC_CONFIGURE_OPTION} \
+  ${TCMALLOC_OPTION} \
+  -DGTEST_SRC_DIR=${GTEST_SRC_DIR} \
+  -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} \
+  ${KLEE_ASSERTS_OPTION} \
+  -DENABLE_UNIT_TESTS=TRUE \
+  -DENABLE_SYSTEM_TESTS=TRUE \
+  -DLIT_ARGS="-v" \
+  ${KLEE_SRC}
+make
+
 ###############################################################################
 # Unit tests
 ###############################################################################
-if [ "X${USE_CMAKE}" == "X1" ]; then
-  make unittests
-else
-  # The unittests makefile doesn't seem to have been packaged so get it from SVN
-  sudo mkdir -p /usr/lib/llvm-${LLVM_VERSION}/build/unittests/
-  svn export  http://llvm.org/svn/llvm-project/llvm/branches/${SVN_BRANCH}/unittests/Makefile.unittest \
-      ../Makefile.unittest
-  sudo mv ../Makefile.unittest /usr/lib/llvm-${LLVM_VERSION}/build/unittests/
-
-  make unittests \
-      DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \
-      ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \
-      ENABLE_SHARED=0
-fi
+make unittests
 
 ###############################################################################
 # lit tests
 ###############################################################################
-if [ "X${USE_CMAKE}" == "X1" ]; then
-  make systemtests
-else
-  # Note can't use ``make check`` because llvm-lit is not available
-  cd test
-  # The build system needs to generate this file before we can run lit
-  make lit.site.cfg \
-      DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \
-      ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \
-      ENABLE_SHARED=0
-  cd ../
-  lit -v test/
-fi
+make systemtests
 
 # If metaSMT is the only solver, then rerun lit tests with non-default metaSMT backends
 if [ "X${SOLVERS}" == "XmetaSMT" ]; then
diff --git a/.travis/testing-utils.sh b/.travis/testing-utils.sh
index 7502b4fc..eefccdd2 100755
--- a/.travis/testing-utils.sh
+++ b/.travis/testing-utils.sh
@@ -2,28 +2,8 @@
 # Make sure we exit if there is a failure
 set -e
 
-if [ "X${USE_CMAKE}" == "X1" ]; then
-    # The New CMake build system just needs the GTest sources regardless
-    # of LLVM version.
-    wget https://github.com/google/googletest/archive/release-1.7.0.zip
-    unzip release-1.7.0.zip
-    exit 0
-fi
-
-# Using LLVM3.4 all we need is vanilla GoogleTest :)
+# The New CMake build system just needs the GTest sources regardless
+# of LLVM version.
 wget https://github.com/google/googletest/archive/release-1.7.0.zip
 unzip release-1.7.0.zip
-cd googletest-release-1.7.0/
-cmake .
-make
-# Normally I wouldn't do something like this but hey we're running on a temporary virtual machine, so who cares?
-if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
-   sudo cp lib* /usr/lib/
-   sudo cp -r include/gtest /usr/include
-elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
-   sudo cp lib* /usr/local/lib/
-   sudo cp -r include/gtest /usr/local/include
-else
-   echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
-   exit 1
-fi
+exit 0