C library: additional floating-point functions and cleanup #9612
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 CBMC | |
on: | |
push: | |
branches: [ develop ] | |
pull_request: | |
branches: [ develop ] | |
env: | |
cvc5-version: "1.0.0" | |
jobs: | |
# This job takes approximately 21 to 40 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++ maven jq flex bison libxml2-utils ccache cmake z3 | |
- name: Confirm z3 solver is available and log the version installed | |
run: z3 --version | |
- name: Download cvc-5 from the releases page and make sure it can be deployed | |
run: | | |
wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux | |
chmod u+x cvc5 | |
mv cvc5 /usr/local/bin | |
cvc5 --version | |
- name: Prepare ccache | |
uses: actions/cache@v4 | |
with: | |
save-always: true | |
path: .ccache | |
key: ${{ runner.os }}-20.04-make-${{ github.ref }}-${{ github.sha }}-PR | |
restore-keys: | | |
${{ runner.os }}-20.04-make-${{ github.ref }} | |
${{ runner.os }}-20.04-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: Build with make | |
run: | | |
git clone https://github.com/conp-solutions/riss riss.git | |
cmake -Hriss.git -Briss.git/release -DCMAKE_BUILD_TYPE=Release | |
make -C riss.git/release riss-coprocessor-lib-static -j2 | |
make -C src -j2 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss | |
make -C jbmc/src -j2 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss | |
make -C unit -j2 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss | |
make -C jbmc/unit -j2 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss | |
- name: Print ccache stats | |
run: ccache -s | |
- name: Checking completeness of help output | |
run: scripts/check_help.sh g++ | |
- name: Run unit tests | |
run: | | |
make -C unit test IPASIR=$PWD/riss.git/riss | |
make -C jbmc/unit test IPASIR=$PWD/riss.git/riss | |
echo "Running expected failure tests" | |
make TAGS="[!shouldfail]" -C unit test IPASIR=$PWD/riss.git/riss | |
make TAGS="[!shouldfail]" -C jbmc/unit test IPASIR=$PWD/riss.git/riss | |
- name: Run regression tests | |
run: | | |
make -C regression test-parallel JOBS=2 LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss | |
make -C regression/cbmc test-paths-lifo | |
env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 | |
make -C jbmc/regression test-parallel JOBS=2 | |
- name: Check cleanup | |
run: | | |
make -C src clean IPASIR=$PWD/riss.git/riss | |
make -C jbmc/src clean IPASIR=$PWD/riss.git/riss | |
rm -r riss.git | |
rm src/goto-cc/goto-ld | |
make -C unit clean | |
make -C regression clean | |
make -C jbmc/unit clean | |
make -C jbmc/regression clean | |
if [[ $(git status --ignored --porcelain | grep -v .ccache/) ]] ; then | |
git status --ignored | |
exit 1 | |
fi | |
# This job takes approximately 25 to 34 minutes | |
check-ubuntu-20_04-make-clang: | |
runs-on: ubuntu-20.04 | |
env: | |
CC: "ccache /usr/bin/clang" | |
CXX: "ccache /usr/bin/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 maven jq flex bison libxml2-utils cpanminus ccache z3 | |
make -C src minisat2-download cadical-download | |
cpanm Thread::Pool::Simple | |
- name: Confirm z3 solver is available and log the version installed | |
run: z3 --version | |
- name: Download cvc-5 from the releases page and make sure it can be deployed | |
run: | | |
wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux | |
chmod u+x cvc5 | |
mv cvc5 /usr/local/bin | |
cvc5 --version | |
- name: Prepare ccache | |
uses: actions/cache@v4 | |
with: | |
save-always: true | |
path: .ccache | |
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: Build with make | |
run: | | |
make -C src -j2 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical | |
make -C unit -j2 | |
make -C jbmc/src -j2 | |
make -C jbmc/unit -j2 | |
- name: Print ccache stats | |
run: ccache -s | |
- name: Run unit tests | |
run: | | |
make -C unit test | |
make -C jbmc/unit test | |
make TAGS="[z3]" -C unit test | |
- name: Run expected failure unit tests | |
run: | | |
make TAGS="[!shouldfail]" -C unit test | |
make TAGS="[!shouldfail]" -C jbmc/unit test | |
- name: Run regression tests | |
run: | | |
make -C regression test-parallel JOBS=2 | |
make -C regression/cbmc test-paths-lifo | |
env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 | |
make -C jbmc/regression test-parallel JOBS=2 | |
# This job has been copied from the one above it, and modified to only build CBMC | |
# and run the `regression/cbmc/` regression tests against Z3. The rest of the tests | |
# (unit/regression) have been stripped based on the rationale that they are going | |
# to be run by the job above, which is basically the same, but more comprehensive. | |
# The reason we opted for a new job is that adding a `test-z3` step to the current | |
# jobs increases the job runtime to unacceptable levels (over 2hrs). | |
# This job takes approximately 5 to 18 minutes | |
check-ubuntu-20_04-make-clang-smt-z3: | |
runs-on: ubuntu-20.04 | |
env: | |
CC: "ccache /usr/bin/clang" | |
CXX: "ccache /usr/bin/clang++" | |
steps: | |
- uses: actions/checkout@v4 | |
with: | |
submodules: recursive | |
- name: Fetch dependencies | |
env: | |
DEBIAN_FRONTEND: noninteractive | |
run: | | |
sudo apt-get update | |
sudo apt-get install --no-install-recommends -yq clang-10 clang++-10 gdb maven jq flex bison libxml2-utils cpanminus ccache z3 | |
make -C src minisat2-download | |
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: | |
save-always: true | |
path: .ccache | |
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: Build with make | |
run: make -C src -j2 | |
- name: Print ccache stats | |
run: ccache -s | |
- name: Run regression/cbmc tests with z3 as the backend | |
run: make -C regression/cbmc test-z3 | |
# This job takes approximately 29 to 42 minutes | |
check-ubuntu-20_04-cmake-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 cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3 | |
- name: Confirm z3 solver is available and log the version installed | |
run: z3 --version | |
- name: Download cvc-5 from the releases page and make sure it can be deployed | |
run: | | |
wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux | |
chmod u+x cvc5 | |
mv cvc5 /usr/local/bin | |
cvc5 --version | |
- name: Prepare ccache | |
uses: actions/cache@v4 | |
with: | |
save-always: true | |
path: .ccache | |
key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR | |
restore-keys: | | |
${{ runner.os }}-20.04-Release-${{ github.ref }} | |
${{ runner.os }}-20.04-Release | |
- name: ccache environment | |
run: | | |
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV | |
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV | |
- name: Configure using CMake | |
run: cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical" | |
- name: Check that doc task works | |
run: ninja -C build doc | |
- name: Zero ccache stats and limit in size | |
run: ccache -z --max-size=500M | |
- name: Build with Ninja | |
run: ninja -C build -j2 | |
- name: Print ccache stats | |
run: ccache -s | |
- name: Checking completeness of help output | |
run: scripts/check_help.sh /usr/bin/g++ build/bin | |
- name: Check if package building works | |
run: | | |
cd build | |
ninja package | |
ls *.deb | |
- name: Run tests | |
run: cd build; ctest . -V -L CORE -j2 | |
- name: Check cleanup | |
run: | | |
rm -r build | |
rm scripts/bash-autocomplete/cbmc.sh | |
make -C unit clean | |
make -C regression clean | |
make -C jbmc/regression clean | |
if [[ $(git status --ignored --porcelain | grep -v .ccache/) ]] ; then | |
git status --ignored | |
exit 1 | |
fi | |
# This job takes approximately 34 to 38 minutes | |
check-ubuntu-22_04-make-clang: | |
runs-on: ubuntu-22.04 | |
env: | |
CC: "ccache /usr/bin/clang" | |
CXX: "ccache /usr/bin/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 clang-14 gdb maven jq flex bison libxml2-utils cpanminus ccache z3 | |
make -C src minisat2-download cadical-download | |
cpanm Thread::Pool::Simple | |
- name: Confirm z3 solver is available and log the version installed | |
run: z3 --version | |
- name: Download cvc-5 from the releases page and make sure it can be deployed | |
run: | | |
wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux | |
chmod u+x cvc5 | |
mv cvc5 /usr/local/bin | |
cvc5 --version | |
- name: Prepare ccache | |
uses: actions/cache@v4 | |
with: | |
save-always: true | |
path: .ccache | |
key: ${{ runner.os }}-22.04-make-clang-${{ github.ref }}-${{ github.sha }}-PR | |
restore-keys: | | |
${{ runner.os }}-22.04-make-clang-${{ github.ref }} | |
${{ runner.os }}-22.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: Perform C/C++ library syntax check | |
run: | | |
make -C src/ansi-c library_check | |
make -C src/cpp library_check | |
- name: Build with make | |
run: | | |
make -C src -j2 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical | |
make -C unit -j2 | |
make -C jbmc/src -j2 | |
make -C jbmc/unit -j2 | |
- name: Print ccache stats | |
run: ccache -s | |
- name: Run unit tests | |
run: | | |
make -C unit test | |
make -C jbmc/unit test | |
make TAGS="[z3]" -C unit test | |
- name: Run expected failure unit tests | |
run: | | |
make TAGS="[!shouldfail]" -C unit test | |
make TAGS="[!shouldfail]" -C jbmc/unit test | |
- name: Run regression tests | |
run: | | |
make -C regression test-parallel JOBS=2 | |
make -C regression/cbmc test-paths-lifo | |
env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 | |
make -C jbmc/regression test-parallel JOBS=2 | |
# This job takes approximately 22 to 41 minutes | |
check-ubuntu-22_04-cmake-gcc: | |
runs-on: ubuntu-22.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 cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3 | |
- name: Confirm z3 solver is available and log the version installed | |
run: z3 --version | |
- name: Download cvc-5 from the releases page and make sure it can be deployed | |
run: | | |
wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux | |
chmod u+x cvc5 | |
mv cvc5 /usr/local/bin | |
cvc5 --version | |
- name: Prepare ccache | |
uses: actions/cache@v4 | |
with: | |
save-always: true | |
path: .ccache | |
key: ${{ runner.os }}-22.04-Release-${{ github.ref }}-${{ github.sha }}-PR | |
restore-keys: | | |
${{ runner.os }}-22.04-Release-${{ github.ref }} | |
${{ runner.os }}-22.04-Release | |
- name: ccache environment | |
run: | | |
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV | |
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV | |
- name: Configure using CMake | |
run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical" | |
- name: Check that doc task works | |
run: ninja -C build doc | |
- name: Zero ccache stats and limit in size | |
run: ccache -z --max-size=500M | |
- name: Build with Ninja | |
run: ninja -C build -j2 | |
- name: Print ccache stats | |
run: ccache -s | |
- name: Check if package building works | |
run: | | |
cd build | |
ninja package | |
ls *.deb | |
- name: Run tests | |
run: cd build; ctest . -V -L CORE -j2 | |
# This job takes approximately 26 to 46 minutes | |
check-ubuntu-22_04-cmake-gcc-13: | |
runs-on: ubuntu-22.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 cmake ninja-build gcc-13 gdb g++-13 maven flex bison libxml2-utils dpkg-dev ccache doxygen z3 | |
# Update symlinks so that any use of gcc (including our regression | |
# tests) will use GCC 13. | |
sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-13 110 \ | |
--slave /usr/bin/g++ g++ /usr/bin/g++-13 \ | |
--slave /usr/bin/gcov gcov /usr/bin/gcov-13 | |
sudo ln -sf cpp-13 /usr/bin/cpp | |
- name: Confirm z3 solver is available and log the version installed | |
run: z3 --version | |
- name: Download cvc-5 from the releases page and make sure it can be deployed | |
run: | | |
wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux | |
chmod u+x cvc5 | |
mv cvc5 /usr/local/bin | |
cvc5 --version | |
- name: Prepare ccache | |
uses: actions/cache@v4 | |
with: | |
save-always: true | |
path: .ccache | |
key: ${{ runner.os }}-22.04-Release-gcc-13-${{ github.ref }}-${{ github.sha }}-PR | |
restore-keys: | | |
${{ runner.os }}-22.04-Release-gcc-13-${{ github.ref }} | |
${{ runner.os }}-22.04-Release-gcc-13 | |
- name: ccache environment | |
run: | | |
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV | |
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV | |
- name: Configure using CMake | |
run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_FLAGS=-Wp,-D_GLIBCXX_ASSERTIONS | |
- name: Zero ccache stats and limit in size | |
run: ccache -z --max-size=500M | |
- name: Build with Ninja | |
run: ninja -C build -j2 | |
- name: Print ccache stats | |
run: ccache -s | |
- name: Run tests | |
run: cd build; ctest . -V -L CORE -j2 | |
# This job takes approximately 30 to 60 minutes | |
check-ubuntu-22_04-cmake-gcc-32bit: | |
runs-on: ubuntu-22.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 cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils ccache doxygen z3 g++-multilib | |
- name: Confirm z3 solver is available and log the version installed | |
run: z3 --version | |
- name: Download cvc-5 from the releases page and make sure it can be deployed | |
run: | | |
wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux | |
chmod u+x cvc5 | |
mv cvc5 /usr/local/bin | |
cvc5 --version | |
- name: Prepare ccache | |
uses: actions/cache@v4 | |
with: | |
save-always: true | |
path: .ccache | |
key: ${{ runner.os }}-22.04-Release-32-${{ github.ref }}-${{ github.sha }}-PR | |
restore-keys: | | |
${{ runner.os }}-22.04-Release-32-${{ github.ref }} | |
${{ runner.os }}-22.04-Release-32 | |
- name: ccache environment | |
run: | | |
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV | |
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV | |
- name: Configure using CMake | |
run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical" -DCMAKE_CXX_FLAGS=-m32 | |
- name: Zero ccache stats and limit in size | |
run: ccache -z --max-size=500M | |
- name: Build with Ninja | |
run: ninja -C build -j2 | |
- name: Print ccache stats | |
run: ccache -s | |
- name: Run tests | |
run: cd build; ctest . -V -L CORE -j2 | |
# This job takes approximately 5 to 24 minutes | |
check-ubuntu-20_04-cmake-gcc-KNOWNBUG: | |
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 cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3 | |
- name: Prepare ccache | |
uses: actions/cache@v4 | |
with: | |
save-always: true | |
path: .ccache | |
key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR | |
restore-keys: | | |
${{ runner.os }}-20.04-Release-${{ github.ref }} | |
${{ runner.os }}-20.04-Release | |
- name: ccache environment | |
run: | | |
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV | |
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV | |
- name: Configure using CMake | |
run: cmake -H. -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ | |
- name: Zero ccache stats and limit in size | |
run: ccache -z --max-size=500M | |
- name: Build with Ninja | |
run: ninja -C build -j2 | |
- name: Print ccache stats | |
run: ccache -s | |
- name: Run tests | |
run: | | |
cd build | |
ctest . -V -L KNOWNBUG -j2 | |
export PATH=$PWD/bin:$PATH | |
cd ../regression/cbmc | |
sed -i '1s/^CORE\(.*\)broken-smt-backend/KNOWNBUG\1broken-smt-backend/' */*.desc | |
# the following tests fail on Windows only | |
git checkout -- memory_allocation1 printf1 union12 va_list3 | |
../test.pl -c "cbmc --cprover-smt2" -I broken-smt-backend -K | |
# This job takes approximately 8 to 30 minutes | |
check-ubuntu-20_04-cmake-gcc-THOROUGH: | |
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 cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3 | |
- name: Prepare ccache | |
uses: actions/cache@v4 | |
with: | |
save-always: true | |
path: .ccache | |
key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR | |
restore-keys: | | |
${{ runner.os }}-20.04-Release-${{ github.ref }} | |
${{ runner.os }}-20.04-Release | |
- name: ccache environment | |
run: | | |
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV | |
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV | |
- name: Configure using CMake | |
run: cmake -H. -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical" | |
- name: Zero ccache stats and limit in size | |
run: ccache -z --max-size=500M | |
- name: Build with Ninja | |
run: ninja -C build -j2 | |
- name: Print ccache stats | |
run: ccache -s | |
- name: Run tests | |
run: cd build; ctest . -V -L THOROUGH -j2 | |
# This job takes approximately 39 to 69 minutes | |
check-macos-11-make-clang: | |
runs-on: macos-11 | |
steps: | |
- uses: actions/checkout@v4 | |
with: | |
submodules: recursive | |
- name: Fetch dependencies | |
run: brew install maven flex bison parallel ccache z3 | |
- name: Confirm z3 solver is available and log the version installed | |
run: z3 --version | |
- name: Download cvc5 binary and make sure it can be deployed | |
run: | | |
curl -L https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-macOS --output cvc5 | |
chmod u+x cvc5 | |
mv cvc5 /usr/local/bin | |
cvc5 --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: Build using Make | |
run: | | |
make -C src minisat2-download cadical-download | |
make -C src -j3 CXX="ccache clang++" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical | |
make -C jbmc/src -j3 CXX="ccache clang++" | |
make -C unit "CXX=ccache clang++" | |
make -C jbmc/unit "CXX=ccache clang++" | |
- name: Print ccache stats | |
run: ccache -s | |
- name: Run unit tests | |
run: | | |
cd unit; ./unit_tests | |
./unit_tests "[z3]" | |
- name: Run JBMC unit tests | |
run: cd jbmc/unit; ./unit_tests | |
- name: Run regression tests | |
run: make -C regression test-parallel JOBS=3 | |
- name: Run JBMC regression tests | |
run: make -C jbmc/regression test-parallel JOBS=3 | |
# This job takes approximately 66 to 85 minutes | |
check-macos-12-cmake-clang: | |
runs-on: macos-12 | |
steps: | |
- uses: actions/checkout@v4 | |
with: | |
submodules: recursive | |
- name: Fetch dependencies | |
run: brew install cmake ninja maven flex bison ccache z3 | |
- name: Confirm z3 solver is available and log the version installed | |
run: z3 --version | |
- name: Download cvc5 binary and make sure it can be deployed | |
run: | | |
curl -L https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-macOS --output cvc5 | |
chmod u+x cvc5 | |
mv cvc5 /usr/local/bin | |
cvc5 --version | |
- name: Prepare ccache | |
uses: actions/cache@v4 | |
with: | |
save-always: true | |
path: .ccache | |
key: ${{ runner.os }}-Release-Glucose-${{ github.ref }}-${{ github.sha }}-PR | |
restore-keys: | | |
${{ runner.os }}-Release-Glucose-${{ github.ref }} | |
${{ runner.os }}-Release-Glucose | |
- 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: Configure using CMake | |
run: | | |
mkdir build | |
cd build | |
cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=$(brew --prefix llvm@15)/bin/clang -DCMAKE_CXX_COMPILER=$(brew --prefix llvm@15)/bin/clang++ -Dsat_impl=glucose | |
- name: Build with Ninja | |
run: cd build; ninja -j3 | |
- name: Print ccache stats | |
run: ccache -s | |
- name: Run CTest | |
run: cd build; ctest -V -L CORE . -j3 | |
# This job takes approximately 49 to 70 minutes | |
check-vs-2019-cmake-build-and-test: | |
runs-on: windows-2019 | |
env: | |
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
steps: | |
- uses: actions/checkout@v4 | |
with: | |
submodules: recursive | |
- name: Setup Visual Studio environment | |
uses: microsoft/setup-msbuild@v2 | |
- name: Fetch dependencies | |
run: | | |
choco install winflexbison3 | |
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 | |
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\cvc5" | |
Invoke-WebRequest -Uri https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Win64.exe -OutFile c:\tools\cvc5\cvc5.exe | |
echo "c:\tools\cvc5;" >> $env:GITHUB_PATH | |
- name: Confirm z3 solver is available and log the version installed | |
run: z3 --version | |
- name: Confirm cvc5 solver is available and log the version installed | |
run: cvc5 --version | |
- name: Prepare ccache | |
uses: actions/cache@v4 | |
with: | |
save-always: true | |
path: .ccache | |
key: ${{ runner.os }}-msbuild-${{ github.ref }}-${{ github.sha }}-PR | |
restore-keys: | | |
${{ runner.os }}-msbuild-${{ github.ref }} | |
${{ runner.os }}-msbuild | |
- name: ccache environment | |
run: | | |
echo "CLCACHE_BASEDIR=$((Get-Item -Path '.\').FullName)" >> $env:GITHUB_ENV | |
echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV | |
- name: Configure with cmake | |
run: cmake -S . -B build | |
- name: Build Release | |
run: cmake --build build --config Release -- /p:UseMultiToolTask=true /p:CLToolExe=clcache | |
- name: Print ccache stats | |
run: clcache -s | |
- uses: ilammy/msvc-dev-cmd@v1 | |
- name: Test cbmc | |
run: | | |
Set-Location build | |
ctest -V -L CORE -C Release . -j2 | |
# This job takes approximately 65 to 84 minutes | |
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 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\cvc5" | |
wget.exe -O c:\tools\cvc5\cvc5.exe https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Win64.exe | |
echo "c:\tools\cvc5;" >> $env:GITHUB_PATH | |
- name: Confirm z3 solver is available and log the version installed | |
run: z3 --version | |
- name: Confirm cvc5 solver is available and log the version installed | |
run: cvc5 --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: Download minisat with make | |
run: make -C src minisat2-download | |
- name: Build CBMC with make | |
run: make CXX=clcache BUILD_ENV=MSVC -j2 -C src | |
- name: Build unit tests with make | |
run: make CXX=clcache BUILD_ENV=MSVC -j2 -C unit all | |
- name: Build jbmc with make | |
run: | | |
make CXX=clcache -j2 -C jbmc/src setup-submodules | |
make CXX=clcache BUILD_ENV=MSVC -j2 -C jbmc/src | |
- name: Build JBMC unit tests | |
run: make CXX=clcache BUILD_ENV=MSVC -j2 -C jbmc/unit all | |
- name: Print ccache stats | |
run: clcache -s | |
- name: Run CBMC and JBMC unit tests | |
run: | | |
make CXX=clcache BUILD_ENV=MSVC -C unit test | |
make CXX=clcache BUILD_ENV=MSVC -C unit test TAGS="[z3]" | |
make CXX=clcache BUILD_ENV=MSVC -C jbmc/unit test | |
- name: Run CBMC regression tests | |
run: make CXX=clcache BUILD_ENV=MSVC -C regression test | |
# This job takes approximately 7 to 32 minutes | |
windows-msi-package: | |
runs-on: windows-2019 | |
env: | |
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
steps: | |
- uses: actions/checkout@v4 | |
with: | |
submodules: recursive | |
- name: Setup Visual Studio environment | |
uses: microsoft/setup-msbuild@v2 | |
- name: Fetch dependencies | |
run: | | |
choco install winflexbison3 | |
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 | |
- name: Prepare ccache | |
uses: actions/cache@v4 | |
with: | |
save-always: true | |
path: .ccache | |
key: ${{ runner.os }}-msbuild-${{ github.ref }}-${{ github.sha }}-PKG | |
restore-keys: | | |
${{ runner.os }}-msbuild-${{ github.ref }} | |
${{ runner.os }}-msbuild | |
- name: ccache environment | |
run: | | |
echo "CLCACHE_BASEDIR=$((Get-Item -Path '.\').FullName)" >> $env:GITHUB_ENV | |
echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV | |
- name: Configure with cmake | |
run: cmake -S . -B build | |
- name: Build Release | |
run: cmake --build build --config Release -- /p:UseMultiToolTask=true /p:CLToolExe=clcache | |
- name: Print ccache stats | |
run: clcache -s | |
- name: Create packages | |
id: create_packages | |
# We need to get the path to cpack because fascinatingly, | |
# chocolatey also includes a command called "cpack" which takes precedence | |
run: | | |
Set-Location build | |
$cpack = "$(Split-Path -Parent (Get-Command cmake).Source)\cpack.exe" | |
& $cpack . -C Release | |
$msi_name = (Get-ChildItem -name *.msi).Name | |
echo "msi_installer=build/$msi_name" >> $env:GITHUB_OUTPUT | |
echo "msi_name=$msi_name" >> $env:GITHUB_OUTPUT | |
# This job takes approximately 2 to 3 minutes | |
check-string-table: | |
runs-on: ubuntu-20.04 | |
steps: | |
- uses: actions/checkout@v4 | |
- name: Check for unused irep ids | |
run: ./scripts/string_table_check.sh | |
# This job takes approximately 23 to 29 minutes | |
check-docker-image: | |
runs-on: ubuntu-20.04 | |
steps: | |
- uses: actions/checkout@v4 | |
with: | |
submodules: recursive | |
- name: Download test dependencies | |
run: | | |
sudo apt update | |
sudo apt install openjdk-11-jdk-headless | |
- name: Build docker image | |
run: docker build -t cbmc . | |
- name: Smoke test goto-cc | |
run: docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc goto-cc -o /mnt/smoke/test.goto /mnt/smoke/test.c | |
- name: Smoke test cbmc | |
run: docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc cbmc /mnt/smoke/test.goto | |
- name: Smoke test jbmc | |
run: | | |
javac .github/workflows/smoke_test_assets/Test.java | |
docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc jbmc --classpath /mnt/smoke Test | |
- name: Smoke test goto-analyzer | |
run: docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc goto-analyzer /mnt/smoke/test.goto --unreachable-functions | |
# This job takes approximately 39 to 41 minutes | |
include-what-you-use: | |
runs-on: ubuntu-22.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 cmake ninja-build gcc gdb g++ maven flex bison iwyu | |
- name: Configure using CMake | |
run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ | |
- name: Run include-what-you-use | |
run: | | |
iwyu_tool -p build/compile_commands.json -j2 | tee includes.txt | |
if sed '/minisat2-src/,/^--$/d' includes.txt | grep '^- ' -B1 ; then | |
echo "Unnecessary includes found. Use '// IWYU pragma: keep' to override this." | |
exit 1 | |
fi | |
# This job takes approximately 45 to 75 minutes | |
codecov-coverage-report: | |
runs-on: ubuntu-20.04 | |
steps: | |
- name: Clone repository | |
uses: actions/checkout@v4 | |
with: | |
submodules: recursive | |
- name: Remove unnecessary software to free up disk space | |
run: | | |
# inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml | |
df -h | |
sudo rm -rf /usr/share/dotnet /usr/local/lib/* /opt/* | |
df -h | |
- name: Download testing and coverage 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 -y g++ gcc gdb binutils flex bison cmake maven jq libxml2-utils openjdk-11-jdk-headless lcov ccache z3 | |
- name: Confirm z3 solver is available and log the version installed | |
run: z3 --version | |
- name: Download cvc-5 from the releases page and make sure it can be deployed | |
run: | | |
wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux | |
chmod u+x cvc5 | |
mv cvc5 /usr/local/bin | |
cvc5 --version | |
- name: Prepare ccache | |
uses: actions/cache@v4 | |
with: | |
save-always: true | |
path: .ccache | |
key: ${{ runner.os }}-20.04-Coverage-${{ github.ref }}-${{ github.sha }}-PR | |
restore-keys: | | |
${{ runner.os }}-20.04-Coverage-${{ github.ref }} | |
${{ runner.os }}-20.04-Coverage | |
- name: ccache environment | |
run: | | |
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV | |
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV | |
- name: Configure CMake CBMC build with coverage instrumentation parameters | |
run: cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=2 -DCMAKE_CXX_COMPILER=/usr/bin/g++ | |
- name: Zero ccache stats and limit in size | |
run: ccache -z --max-size=7G | |
- name: Execute CMake CBMC build | |
run: cmake --build build -- -j2 | |
- name: Print ccache stats | |
run: ccache -s | |
- name: Run CTest and collect coverage statistics | |
run: | | |
echo "lcov_excl_line = UNREACHABLE" > ~/.lcovrc | |
cmake --build build --target coverage -- -j2 | |
- name: Upload coverage statistics to Codecov | |
uses: codecov/codecov-action@v3 | |
with: | |
token: ${{ secrets.CODECOV_TOKEN }} | |
files: build/html/coverage.info | |
fail_ci_if_error: true | |
verbose: true |