#dist: xenial
services:
    - docker
language: cpp
env:
    ###########################################################################
    # Configurations
    #
    # Each line in the "env" section represents a set of environment variables
    # passed to a build. Thus each line represents a different build
    # configuration.
    ###########################################################################

    # Check a subset of the matrix of:
    #   LLVM  : {3.8, 3.9, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0, 10.0}
    #   SOLVERS : {Z3, STP, STP:Z3, metaSMT}
    #   STP_VERSION   : {2.3.3, master}
    #   METASMT_VERSION : {v4.rc1}
    #   METASMT_DEFAULT : {BTOR, CVC4, STP, YICES2, Z3}
    #   METASMT_BOOST_VERSION : {x.y.z} // e.g. 1.60.0, libboost-dev will be used if unspecified
    #   UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled
    #   DISABLE_ASSERTIONS: {0, 1}
    #   ENABLE_OPTIMIZED: {0, 1}
    #   COVERAGE: {0, 1} // when set indicates that coverage data should be uploaded to the service
    #   USE_TCMALLOC: {0, 1}

    # Define default values - they are overwritten by each matrix entry if needed
    global:
    - secure: EF/WAc4BdIRUchF3mjATN3/UwtGWtGaRgb5oIIJHjKhgZFdPsgWsXFgaOB0jaK2hfO/svj/LvlasuRIGxeePVjeaiX8ZlVpuHiX67vdYLY+0kCDRwkusRjm60/GbPU9O/Xjgb/d4aWAEkoq5OnsprVTEvU8iY2JHtAqgwR+wW9I=
    - secure: Hrp1MRSxDUH2GTQg3QR/yUttY/3KmgbFb5e+zyy551dKpHjxJdsNe8bquY9oFoT7KmPQYl0HNNjEv4qWW8RK+HWHOCB55nL1KlGpOG7vAJcUEZg7ScbliGgiovMB6jIQVfeP9FhYngfc13vNZQ5PGlqzfSsHSAbvkwEogBToHVw=
    - secure: DQAEQWJblXvIztN/sgH63OtFncI+Qju6wRy1zIV/iLf5KbAmLs1h3itU7EsE/+3+LgV1MVQ5QNJDBUj17A6VHRKNaQ5qnIllTAcC3o0nPDohQkQoCgDG8HZ+M4wtVfr7q2K6byEPB2UbSH+mEjSMTihJufgBBVfKyyozAfYycjg=

    # Default configuration for all Travis-CI jobs. They are overriden by each job.
    - BASE_IMAGE=ubuntu:bionic-20200112
    - REPOSITORY=klee

    - COVERAGE=0
    - DISABLE_ASSERTIONS=0
    - ENABLE_OPTIMIZED=1
    - ENABLE_DEBUG=1
    - GTEST_VERSION=1.7.0
    - KLEE_RUNTIME_BUILD="Debug+Asserts"
    - LLVM_VERSION=6.0
    - METASMT_VERSION=qf_abv
    - MINISAT_VERSION="master"
    - REQUIRES_RTTI=0
    - SANITIZER_BUILD=
    - SOLVERS=STP:Z3
    - STP_VERSION=2.3.3
    - TCMALLOC_VERSION=2.7
    - UCLIBC_VERSION=klee_uclibc_v1.2
    - USE_TCMALLOC=1
    - USE_LIBCXX=1
    - Z3_VERSION=4.8.4

jobs:
    include:
    # Check supported LLVM versions
    - name: "LLVM 10"
      env: LLVM_VERSION=10.0

    - name: "LLVM 9"
      env: LLVM_VERSION=9.0

    - name: "LLVM 8"
      env: LLVM_VERSION=8.0

    - name: "LLVM 7"
      env: LLVM_VERSION=7.0

    - name: "LLVM 6"
      env: LLVM_VERSION=6.0

    - name: "LLVM 5"
      env: LLVM_VERSION=5.0

    - name: "LLVM 4"
      env: LLVM_VERSION=4.0

    - name: "LLVM 3.9"
      env: LLVM_VERSION=3.9

    - name: "LLVM 3.8"
      env: LLVM_VERSION=3.8

    # Sanitizer builds. Do unoptimized build otherwise the optimizer might remove problematic code
    - name: "ASan"
      env: SANITIZER_BUILD=address ENABLE_OPTIMIZED=0 USE_TCMALLOC=0

    - name: "UBSan"
      env: SANITIZER_BUILD=undefined ENABLE_OPTIMIZED=0 USE_TCMALLOC=0
    
    # Use without libcxx as it is too slow to finish before travis time-out
    - name: "MSan"
      env: SANITIZER_BUILD=memory ENABLE_OPTIMIZED=0 USE_TCMALLOC=0 SOLVERS=STP USE_LIBCXX=0

    # Test just using Z3 only
    - name: "Z3 only"
      env: SOLVERS=Z3

    # Test just using metaSMT
    - name: "metaSMT STP"
      env: SOLVERS=metaSMT METASMT_DEFAULT=STP REQUIRES_RTTI=1

    - name: "metaSMT Boolector"
      env: SOLVERS=metaSMT METASMT_DEFAULT=BTOR REQUIRES_RTTI=1

    # Test we can build against STP master
    - name: "STP master"
      env: SOLVERS=STP STP_VERSION=master

    # Check we can build latest klee-uclibc branch
    - name: "Latest klee-uclibc"
      env: UCLIBC_VERSION=klee_0_9_29

    # Check at least one build with Asserts disabled.
    - name: "Asserts enabled"
      env: SOLVERS=STP DISABLE_ASSERTIONS=1

    # Check without TCMALLOC and with an optimised runtime library
    - name: "No TCMalloc, optimised runtime"
      env: USE_TCMALLOC=0 KLEE_RUNTIME_BUILD="Release+Debug+Asserts"

    # Coverage build
    - name: "Coverage"
      env: ENABLE_OPTIMIZED=0 COVERAGE=1

    # macOS
    - name: "macOS"
      os: osx
      env: SOLVERS=STP UCLIBC_VERSION=0 USE_TCMALLOC=0 USE_LIBCXX=0

    # Docker
    - name: "Docker"
      env: BUILD_DOCKER=1

    # TODO: Add Doxygen build
addons:
  apt:
    packages:
      - docker-ce
cache:
  ccache: true
  apt: true
  directories:
    - $HOME/Library/Caches/Homebrew
before_install:
   - if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then export HOMEBREW_NO_INSTALL_CLEANUP=1 && brew update && brew install --verbose --debug bash; fi

script:
    # Build KLEE and run tests
    - if [[ "${BUILD_DOCKER}" != "1" && "$TRAVIS_OS_NAME" == "osx" ]]; then export BASE=/tmp && export PATH="/usr/local/opt/ccache/libexec:/usr/local/bin:$PATH"; scripts/build/build.sh klee --debug --install-system-deps; export DYLD_LIBRARY_PATH=="$(cd ${BASE}/metaSMT-*-deps/stp-git-basic/lib/ && pwd)"; scripts/build/run-tests.sh /tmp/klee_build* --debug; fi
    - if [[ "${BUILD_DOCKER}" != "1" && "$TRAVIS_OS_NAME" == "linux" ]]; then scripts/build/build.sh klee --docker --debug --push-docker-deps --create-final-image; fi
    - if [[ "${BUILD_DOCKER}" != "1" && "$COVERAGE" == "1" && "$TRAVIS_OS_NAME" == "linux" ]]; then scripts/build/run-tests.sh --coverage --upload-coverage --run-docker --debug; fi
    - if [[ "${BUILD_DOCKER}" != "1" && "$COVERAGE" == "0" && "$TRAVIS_OS_NAME" == "linux" ]]; then scripts/build/run-tests.sh --run-docker --debug; fi
    - if [[ "${BUILD_DOCKER}" -eq 1 ]]; then docker build .; fi