ebmc: benchmarking in CI #1865
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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: 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: 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 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: 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: Print ccache stats | |
run: ccache -s |