Skip to content
Build and Test HW-CBMC

Merge pull request #530 from diffblue/SVA-followed-by #1814

Sign in to view logs

Merge pull request #530 from diffblue/SVA-followed-by

Merge pull request #530 from diffblue/SVA-followed-by #1814

Workflow file for this run

.github/workflows/pull-request-checks.yaml at 2776aab
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
# This job takes approximately 20 minutes
check-macos-12-make-clang:
runs-on: macos-12
steps:
- uses: actions/checkout@v4
with:
submodules: recursive
- name: Fetch dependencies
run: brew install flex 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="/usr/local/opt/bison/bin/bison" 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