pull-request-checks.yaml

name: Build and Test HW-CBMC
on:
  push:
    branches: [ main ]
  pull_request:
    branches: [ main ]

jobs:
  # This job takes approximately 15 minutes
  check-ubuntu-20_04-make-gcc:
    runs-on: ubuntu-20.04
    steps:
      - uses: actions/checkout@v4
        with:
          submodules: recursive
      - name: Fetch dependencies
        env:
          # This is needed in addition to -yq to prevent apt-get from asking for
          # user input
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends -yq gcc gdb g++ jq flex bison libxml2-utils ccache cmake z3
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Prepare ccache
        uses: actions/cache@v4
        with:
          path: .ccache
          save-always: true
          key: ${{ runner.os }}-20.04-make-gcc-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-20.04-make-gcc-${{ github.ref }}
            ${{ runner.os }}-20.04-make-gcc
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Get minisat
        run: |
          make -C lib/cbmc/src minisat2-download
      - name: Build with make
        run: make -C src -j4 CXX="ccache g++"
      - name: Run the ebmc tests with SAT
        run: make -C regression/ebmc test
      - name: Run the ebmc tests with Z3
        run: make -C regression/ebmc test-z3
      - name: Run the verilog tests
        run: make -C regression/verilog test
      - name: Run the verilog tests with Z3
        run: make -C regression/verilog test-z3
      - name: Run the smv tests
        run: make -C regression/smv test
      - name: Run the smv tests with Z3
        run: make -C regression/smv test-z3
      - name: Run the vlindex tests
        run: make -C regression/vlindex test
      - name: Print ccache stats
        run: ccache -s

  # This job takes approximately 15 minutes
  check-ubuntu-20_04-make-clang:
    runs-on: ubuntu-20.04
    env:
      CC: "ccache clang"
      CXX: "ccache clang++"
    steps:
      - uses: actions/checkout@v4
        with:
          submodules: recursive
      - name: Fetch dependencies
        env:
          # This is needed in addition to -yq to prevent apt-get from asking for
          # user input
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends -yq clang-10 clang++-10 gdb jq flex bison libxml2-utils cpanminus ccache z3
          cpanm Thread::Pool::Simple
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Prepare ccache
        uses: actions/cache@v4
        with:
          path: .ccache
          save-always: true
          key: ${{ runner.os }}-20.04-make-clang-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-20.04-make-clang-${{ github.ref }}
            ${{ runner.os }}-20.04-make-clang
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Get minisat
        run: |
          make -C lib/cbmc/src minisat2-download
      - name: Build with make
        run: make CXX="ccache clang++" -C src -j4
      - name: Run the ebmc tests with SAT
        run: make -C regression/ebmc test
      - name: Run the ebmc tests with Z3
        run: make -C regression/ebmc test-z3
      - name: Run the verilog tests
        run: make -C regression/verilog test
      - name: Run the verilog tests with Z3
        run: make -C regression/verilog test-z3
      - name: Run the smv tests
        run: make -C regression/smv test
      - name: Run the smv tests with Z3
        run: make -C regression/smv test-z3
      - name: Run the vlindex tests
        run: make -C regression/vlindex test
      - name: Print ccache stats
        run: ccache -s
      - name: Upload the ebmc binary
        uses: actions/upload-artifact@v4
        with:
          name: ebmc-binary
          retention-days: 5
          path: src/ebmc/ebmc

  # This job takes approximately 4 minutes
  benchmarking:
    runs-on: ubuntu-20.04
    needs: check-ubuntu-20_04-make-clang
    steps:
      - uses: actions/checkout@v4
        with:
          submodules: recursive
      - name: Fetch dependencies
        env:
          # This is needed in addition to -yq to prevent apt-get from asking for
          # user input
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends z3
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Get the ebmc binary
        uses: actions/download-artifact@v4
        with:
          name: ebmc-binary
          path: ebmc
      - name: Try the ebmc binary
        run: chmod a+x ./ebmc/ebmc ; ./ebmc/ebmc --version
      - name: HWMCC08 benchmarks
        run: PATH=$PATH:$PWD/ebmc benchmarking/hwmcc08.sh

  # This job takes approximately 1 minute
  examples:
    runs-on: ubuntu-20.04
    needs: check-ubuntu-20_04-make-clang
    steps:
      - uses: actions/checkout@v4
      - name: Get the ebmc binary
        uses: actions/download-artifact@v4
        with:
          name: ebmc-binary
          path: ebmc
      - name: Try the ebmc binary
        run: chmod a+x ./ebmc/ebmc ; ./ebmc/ebmc --version
      - name: Hazard3
        run: PATH=$PATH:$PWD/ebmc examples/Hazard3/Hazard3.sh

  # This job takes approximately 15 minutes
  check-centos8-make-gcc:
    name: CentOS 8
    runs-on: ubuntu-22.04
    container:
      image: centos:8
    steps:
      - name: Install Packages
        run: |
          sed -i -e "s|mirrorlist=|#mirrorlist=|g" -e "s|#baseurl=http://mirror.centos.org|baseurl=http://vault.centos.org|g" /etc/yum.repos.d/CentOS-Linux-*
          yum -y install make gcc-c++ flex bison git rpmdevtools wget
          wget --no-verbose https://github.com/ccache/ccache/releases/download/v4.8.3/ccache-4.8.3-linux-x86_64.tar.xz
          tar xJf ccache-4.8.3-linux-x86_64.tar.xz
          cp ccache-4.8.3-linux-x86_64/ccache /usr/bin/
          # yum install dnf-plugins-core
          # yum config-manager --set-enabled powertools
          # yum install glibc-static libstdc++-static
      - name: cache for ccache
        uses: actions/cache@v4
        with:
          path: /github/home/.cache/ccache
          save-always: true
          key: ${{ runner.os }}-centos8-make-gcc-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: ${{ runner.os }}-centos8-make-gcc-
      - uses: actions/checkout@v4
        with:
          submodules: recursive
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: ccache path
        run: ccache -p | grep cache_dir
      - name: Get minisat
        run: make -C lib/cbmc/src minisat2-download
      - name: Build with make
        run: make CXX="ccache g++ -Wno-class-memaccess" LIBS="-lstdc++fs" -C src -j4
      - name: Run the ebmc tests with SAT
        run: |
          rm regression/ebmc/neural-liveness/counter1.desc
          make -C regression/ebmc test
      - name: Run the verilog tests
        run: make -C regression/verilog test
      - name: Run the smv tests
        run: make -C regression/smv test
      - name: Run the vlindex tests
        run: make -C regression/vlindex test
      - name: Print ccache stats
        run: ccache -s

  # This job takes approximately 20 minutes
  check-macos-14-make-clang:
    runs-on: macos-14
    steps:
      - uses: actions/checkout@v4
        with:
          submodules: recursive
      - name: Fetch dependencies
        run: brew install bison ccache z3
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Prepare ccache
        uses: actions/cache@v4
        with:
          save-always: true
          path: .ccache
          key: ${{ runner.os }}-make-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-make-${{ github.ref }}
            ${{ runner.os }}-make
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Get minisat
        run: make -C lib/cbmc/src minisat2-download
      - name: Build with make
        run: make YACC="/opt/homebrew/opt/bison/bin/bison" CXX="ccache clang++" -C src -j3
      - name: Run the ebmc tests with SAT
        run: make -C regression/ebmc test
      - name: Run the ebmc tests with Z3
        run: make -C regression/ebmc test-z3
      - name: Run the verilog tests
        run: make -C regression/verilog test
      - name: Run the verilog tests with Z3
        run: make -C regression/verilog test-z3
      - name: Run the smv tests
        run: make -C regression/smv test
      - name: Run the smv tests with Z3
        run: make -C regression/smv test-z3
      - name: Run the vlindex tests
        run: make -C regression/vlindex test
      - name: Print ccache stats
        run: ccache -s

  # This job takes approximately 17 minutes
  check-ubuntu-24_04-make-emcc:
    name: Emscripten build
    runs-on: ubuntu-24.04
    steps:
      - uses: actions/checkout@v4
        with:
          submodules: recursive
      - name: Fetch dependencies
        env:
          # This is needed in addition to -yq to prevent apt-get from asking for
          # user input
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends -yq emscripten flex bison libxml2-utils cpanminus ccache
      - name: Prepare ccache
        uses: actions/cache@v4
        with:
          path: .ccache
          save-always: true
          key: ${{ runner.os }}-24.04-make-emcc-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-24.04-make-emcc-${{ github.ref }}
            ${{ runner.os }}-24.04-make-emcc
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Get minisat
        run: make -C lib/cbmc/src minisat2-download
      - name: Build with make
        run: make -C src -j4 CXX="ccache emcc" HOSTCXX="ccache g++" BUILD_ENV=Unix LINKLIB="emar rc \$@ \$^" AR="emar" EXEEXT=".html"
      - name: print version number via node.js
        run: node --no-experimental-fetch src/ebmc/ebmc.js --version
      - name: Print ccache stats
        run: ccache -s

  check-vs-2022-make-build-and-test:
    runs-on: windows-2022
    env:
      GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
    steps:
      - uses: actions/checkout@v4
        with:
          submodules: recursive
      - name: Setup MSBuild
        uses: microsoft/setup-msbuild@v2
      - name: Fetch dependencies
        run: |
          choco install -y --no-progress winflexbison3 strawberryperl wget
          if($LastExitCode -ne 0)
          {
            Write-Output "::error ::Dependency installation via Chocolatey failed."
            exit $LastExitCode
          }
          nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
          echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH
          echo "c:\Strawberry\" >> $env:GITHUB_PATH
          Invoke-WebRequest -Uri https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-win.zip -OutFile .\z3.zip
          Expand-Archive -LiteralPath '.\z3.Zip' -DestinationPath C:\tools
          echo "c:\tools\z3-4.8.10-x64-win\bin;" >> $env:GITHUB_PATH
          New-Item -ItemType directory "C:\tools\parallel"
          wget.exe -O c:\tools\parallel\parallel https://git.savannah.gnu.org/cgit/parallel.git/plain/src/parallel
          echo "c:\tools\parallel" >> $env:GITHUB_PATH
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Initialise Developer Command Line
        uses: ilammy/msvc-dev-cmd@v1
      - name: Prepare ccache
        uses: actions/cache@v4
        with:
          save-always: true
          path: .ccache
          key: ${{ runner.os }}-msbuild-make-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-msbuild-make-${{ github.ref }}
            ${{ runner.os }}-msbuild-make
      - name: ccache environment
        run: |
          echo "CLCACHE_BASEDIR=$((Get-Item -Path '.\').FullName)" >> $env:GITHUB_ENV
          echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV
      - name: Zero ccache stats and limit in size (2 GB)
        run: |
          clcache -z
          clcache -M 2147483648
      - name: Download minisat with make
        run: make -C lib/cbmc/src minisat2-download
      - name: Build EBMC with make
        env:
          # disable MSYS file-name mangling
          MSYS2_ARG_CONV_EXCL: "*"
        run: make CXX=clcache BUILD_ENV=MSVC -j4 -C src
      - name: Print ccache stats
        run: clcache -s