Merge pull request #7863 from adpaco-aws/issue-7862 #24

Workflow file for this run

.github/workflows/pull-request-checks.yaml at d927b47

	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@v3
	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@v3
	with:
	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
	- 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@v3
	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@v3
	with:
	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@v3
	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@v3
	with:
	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@v3
	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@v3
	with:
	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 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@v3
	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@v3
	with:
	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@v3
	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@v3
	with:
	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@v3
	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@v3
	with:
	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
	- 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@v3
	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@v3
	with:
	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@v3
	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@v3
	with:
	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@v3
	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@v3
	with:
	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@v3
	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@v3
	with:
	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@v3
	with:
	submodules: recursive
	- uses: nuget/setup-nuget@v1
	with:
	nuget-version: '5.8.x'
	- 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: Setup Visual Studio environment
	uses: microsoft/setup-msbuild@v1
	- name: Prepare ccache
	uses: actions/cache@v3
	with:
	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@v3
	with:
	submodules: recursive
	- uses: nuget/setup-nuget@v1
	with:
	nuget-version: '5.8.x'
	- 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:\ProgramData\chocolatey\bin" >> $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: Setup MSBuild
	uses: microsoft/setup-msbuild@v1
	- name: Initialise Developer Command Line
	uses: ilammy/msvc-dev-cmd@v1
	- name: Prepare ccache
	uses: actions/cache@v3
	with:
	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@v3
	with:
	submodules: recursive
	- uses: nuget/setup-nuget@v1
	with:
	nuget-version: '5.8.x'
	- 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: Setup Visual Studio environment
	uses: microsoft/setup-msbuild@v1
	- name: Prepare ccache
	uses: actions/cache@v3
	with:
	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@v3
	- 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@v3
	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@v3
	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@v3
	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@v3
	with:
	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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Merge pull request #7863 from adpaco-aws/issue-7862 #24

Workflow file

Merge pull request #7863 from adpaco-aws/issue-7862 #24

Jobs

Run details

Workflow file for this run