---
name: CI

on:
  pull_request:
    branches: master
  push:
    branches: master

# Defaults for building KLEE
env:
  BASE_IMAGE: ubuntu:jammy-20230126
  REPOSITORY: ghcr.io/klee
  COVERAGE: 0
  DISABLE_ASSERTIONS: 0
  ENABLE_DOXYGEN: 0
  ENABLE_OPTIMIZED: 1
  ENABLE_DEBUG: 1
  GTEST_VERSION: 1.11.0
  KLEE_RUNTIME_BUILD: "Debug+Asserts"
  LLVM_VERSION: 11
  MINISAT_VERSION: "master"
  REQUIRES_RTTI: 0
  SOLVERS: STP:Z3
  STP_VERSION: 2.3.3
  TCMALLOC_VERSION: 2.9.1
  UCLIBC_VERSION: klee_uclibc_v1.4
  USE_TCMALLOC: 1
  USE_LIBCXX: 1
  Z3_VERSION: 4.8.15
  SQLITE_VERSION: 3400100

jobs:
  Linux:
    runs-on: ubuntu-latest
    strategy:
      matrix:
        name: [
          "LLVM 16",
          "LLVM 15",
          "LLVM 14",
          "LLVM 13",
          "LLVM 12",
          "LLVM 11, Doxygen",
          "LLVM 10",
          "LLVM 9",
          "ASan",
          "UBSan",
          "MSan",
          "Z3 only",
          "metaSMT",
          "STP master",
          "Latest klee-uclibc",
          "Asserts disabled",
          "No TCMalloc, optimised runtime",
        ]
        include:
          - name: "LLVM 16"
            env:
              LLVM_VERSION: 16
          - name: "LLVM 15"
            env:
              LLVM_VERSION: 15
          - name: "LLVM 14"
            env:
              LLVM_VERSION: 14
          - name: "LLVM 13"
            env:
              LLVM_VERSION: 13
          - name: "LLVM 12"
            env:
              LLVM_VERSION: 12
          - name: "LLVM 11, Doxygen"
            env:
              LLVM_VERSION: 11
              ENABLE_DOXYGEN: 1
          - name: "LLVM 10"
            env:
              LLVM_VERSION: 10
          - name: "LLVM 9"
            env:
              LLVM_VERSION: 9
          # Sanitizer builds. Do unoptimized build otherwise the optimizer
          # might remove problematic code
          - name: "ASan"
            env:
              SANITIZER_BUILD: address
              ENABLE_OPTIMIZED: 0
              USE_TCMALLOC: 0
              SANITIZER_LLVM_VERSION: 12
          - name: "UBSan"
            env:
              SANITIZER_BUILD: undefined
              ENABLE_OPTIMIZED: 0
              USE_TCMALLOC: 0
              SANITIZER_LLVM_VERSION: 12
          - name: "MSan"
            env:
              SANITIZER_BUILD: memory
              ENABLE_OPTIMIZED: 0
              USE_TCMALLOC: 0
              SOLVERS: STP
              SANITIZER_LLVM_VERSION: 14
          # Test just using Z3 only
          - name: "Z3 only"
            env:
              SOLVERS: Z3
          # Test just using metaSMT
          - name: "metaSMT"
            env:
              METASMT_VERSION: qf_abv
              SOLVERS: metaSMT
              METASMT_DEFAULT: STP
              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 disabled"
            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"
    steps:
      - name: Checkout KLEE source code
        uses: actions/checkout@v3
      - name: Build KLEE
        env: ${{ matrix.env }}
        run: scripts/build/build.sh klee --docker --create-final-image
      - name: Run tests
        run: scripts/build/run-tests.sh --run-docker --debug

  macOS:
    runs-on: macos-latest
    env:
      BASE: /tmp
      SOLVERS: STP
      UCLIBC_VERSION: 0
      USE_TCMALLOC: 0
      USE_LIBCXX: 0
    steps:
      - name: Install newer version of Bash
        run: brew install bash
      - name: Checkout KLEE source code
        uses: actions/checkout@v3
      - name: Build KLEE
        run: scripts/build/build.sh klee --debug --install-system-deps
      - name: Run tests
        run: scripts/build/run-tests.sh /tmp/klee_build* --debug

  Docker:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout KLEE Code
        uses: actions/checkout@v3
      - name: Build Docker image
        run: docker build .

  Coverage:
    runs-on: ubuntu-latest
    strategy:
      matrix:
        name: [
          "STP",
          "Z3",
        ]
        include:
          - name: "STP"
            env:
              SOLVERS: STP:Z3
          - name: "Z3"
            env:
              SOLVERS: Z3
    env:
      ENABLE_OPTIMIZED: 0
      COVERAGE: 1
    steps:
      - name: Checkout KLEE source code
        uses: actions/checkout@v3
        with:
          # Codecov may run into "Issue detecting commit SHA. Please run
          # actions/checkout with fetch-depth > 1 or set to 0" when uploading.
          # See also https://github.com/codecov/codecov-action/issues/190
          fetch-depth: 2
      - name: Build KLEE
        env: ${{ matrix.env }}
        run: scripts/build/build.sh klee --docker --create-final-image
      - name: Run tests
        run: scripts/build/run-tests.sh --coverage --upload-coverage --run-docker --debug