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 -j2 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: 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 -j2
      - 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: Print ccache stats
        run: ccache -s

  # 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 -j2
      - 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: Print ccache stats
        run: ccache -s