diff --git a/.github/workflows/README.md b/.github/workflows/README.md deleted file mode 100644 index 49898733076..00000000000 --- a/.github/workflows/README.md +++ /dev/null @@ -1,47 +0,0 @@ -# CBMC CI infrastructure - -This folder contains implementation and configuration files for -our CI infrastructure on top of Github Actions. Aside from CI, -it also contains packaging and automated release scripts. - -The files in this folder correspond to: - -* `build-and-test-Xen.yaml` -> Build Xen using CBMC tools. -* `csmith.yaml` -> Run 10 randomly generated CSmith tests per Pull Request. -* `doxygen-check.yaml` -> Build project doxygen documentation per Pull Request. -* `pull-request-check-cpplint.sh` -> Script that's called per Pull Request to execute - `cpplint` over changes. -* `pull-request-check-clang-format.sh` -> Script that's called per Pull Request - to execute `clang-format` over changes. -* `pull-request-checks.yaml` -> Configuration file for the Github Actions CI jobs - for the various platforms. -* `regular-release.yaml` -> Configuration file for performing an automated release - every time a tag of a specific form (`cbmc-x.y.z`) is pushed. -* `release-packages.yaml` -> Configuration file for performing building of build - artifacts that are attached to release when it's being made. Invoked when a - regular release is performed. - -## CI Platforms - -We are currently building and testing CBMC under the following configurations: - -* `make` * `gcc` * `linux` (ubuntu 20.04) -* `make` * `clang` * `linux` (ubuntu 20.04) -* `cmake` * `gcc` * `linux` (ubuntu 20.04) -* `make` * `clang` * `macos` (10.15) -* `cmake` * `clang` * `macos` (10.15) -* `cmake` * `vs` * `windows` (vs2019) - -Aside from the main platform builds for testing, we are also performing -some auxiliary builds that test packaging support to be up-to-date. We -do that for: - -* a `docker` image -* an `ubuntu-20.04` package -* a `windows-msi` installer package - -Last but not least, we are also performing a coverage statistics collection -job, which builds CBMC with coverage information on, and then runs the tests, -finally uploading the results to [Codecov](https://about.codecov.io) which -then updates pull request with coverage statistics after the job has finished -running. diff --git a/.github/workflows/bsd.yaml b/.github/workflows/bsd.yaml deleted file mode 100644 index 797b8f2b416..00000000000 --- a/.github/workflows/bsd.yaml +++ /dev/null @@ -1,193 +0,0 @@ -name: Build and Test on *BSD -on: - push: - branches: [ develop ] - pull_request: - branches: [ develop ] - -jobs: - # This job takes approximately 6 to 26 minutes - FreeBSD: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: Prepare ccache - uses: actions/cache@v3 - with: - path: .ccache - key: freebsd-13.2-gmake-${{ github.ref }}-${{ github.sha }}-PR - restore-keys: | - freebsd-13.2-gmake-${{ github.ref }} - freebsd-13.2-gmake - - name: ccache environment - run: | - echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV - echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV - - name: Build and Test - uses: vmactions/freebsd-vm@v1 - with: - release: 13.2 - usesh: true - run: | - # apparently fail-on-error isn't the default here - set -e -x - echo "Fetch dependencies" - pkg install -y bash gmake git www/p5-libwww python python3 patch flex bison ccache parallel cvc5 z3 - echo "Fetch JBMC dependencies" - pkg install -y openjdk8 wget maven - echo "Zero ccache stats and limit in size" - export CCACHE_BASEDIR=$PWD - export CCACHE_DIR=$PWD/.ccache - ccache -z --max-size=500M - ccache -p - echo "Build with gmake" - # don't do JBMC as to keep the overall time in check - gmake -C src minisat2-download - gmake -C src -j2 CXX="ccache clang++" - # gmake -C jbmc/src setup-submodules - # gmake -C jbmc/src -j2 CXX="ccache clang++" - gmake -C unit "CXX=ccache clang++" - # gmake -C jbmc/unit "CXX=ccache clang++" - echo "Print ccache stats" - ccache -s - echo "Checking completeness of help output" - scripts/check_help.sh clang++ - echo "Run unit tests" - gmake -C unit test - # gmake -C jbmc/unit test - echo "Running expected failure tests" - gmake TAGS='[!shouldfail]' -C unit test - # gmake TAGS='[!shouldfail]' -C jbmc/unit test - echo "Run regression tests" - gmake -C regression/cbmc test - # gmake -C regression test-parallel JOBS=2 - # gmake -C regression/cbmc test-paths-lifo - # env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2 - # # gmake -C jbmc/regression test-parallel JOBS=2 - - # This job takes approximately 7 to 34 minutes - OpenBSD: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: Prepare ccache - uses: actions/cache@v3 - with: - path: .ccache - key: openbsd-7.4-gmake-${{ github.ref }}-${{ github.sha }}-PR - restore-keys: | - openbsd-7.4-gmake-${{ github.ref }} - openbsd-7.4-gmake - - name: ccache environment - run: | - echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV - echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV - - name: Build and Test - uses: vmactions/openbsd-vm@v1 - with: - release: 7.4 - run: | - # apparently fail-on-error isn't the default here - set -e -x - echo "Fetch dependencies" - pkg_add -v bash gmake llvm%16 git python3 bison ccache parallel z3 - ln -s $(which llvm-ar-16) /usr/local/bin/llvm-ar - echo "Fetch JBMC dependencies" - pkg_add -v jdk%1.8 wget maven - echo "Zero ccache stats and limit in size" - export CCACHE_BASEDIR=$PWD - export CCACHE_DIR=$PWD/.ccache - ccache -z --max-size=500M - ccache -p - echo "Build with gmake" - # don't do JBMC so as to keep the overall time in check - gmake -C src minisat2-download - gmake -C src -j2 CXX="ccache clang++" - # gmake -C jbmc/src setup-submodules - # gmake -C jbmc/src -j2 CXX="ccache clang++" - gmake -C unit "CXX=ccache clang++" - # gmake -C jbmc/unit "CXX=ccache clang++" - echo "Print ccache stats" - ccache -s - echo "Checking completeness of help output" - scripts/check_help.sh clang++ - echo "Run unit tests" - gmake -C unit test - # gmake -C jbmc/unit test - echo "Running expected failure tests" - gmake TAGS='[!shouldfail]' -C unit test - # gmake TAGS='[!shouldfail]' -C jbmc/unit test - echo "Run regression tests" - gmake -C regression/cbmc test - # gmake -C regression test-parallel JOBS=2 - # gmake -C regression/cbmc test-paths-lifo - # env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2 - # # gmake -C jbmc/regression test-parallel JOBS=2 - - # This job takes approximately 6 to 29 minutes - NetBSD: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: Prepare ccache - uses: actions/cache@v3 - with: - path: .ccache - key: netbsd-9.3-gmake-${{ github.ref }}-${{ github.sha }}-PR - restore-keys: | - netbsd-9.3-gmake-${{ github.ref }} - netbsd-9.3-gmake - - name: ccache environment - run: | - echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV - echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV - - name: Build and Test - uses: vmactions/netbsd-vm@v1 - with: - release: 9.3 - run: | - # apparently fail-on-error isn't the default here - set -e -x - echo "Fetch dependencies" - pkg_add -v bash gmake git python311 patch flex bison ccache parallel z3 gcc10 - ln -s $(which python3.11) /usr/pkg/bin/python3 - export PATH=/usr/pkg/gcc10/bin:$PATH - echo "Fetch JBMC dependencies" - pkg_add -v openjdk8 wget apache-maven - echo "Zero ccache stats and limit in size" - export CCACHE_BASEDIR=$PWD - export CCACHE_DIR=$PWD/.ccache - ccache -z --max-size=500M - ccache -p - echo "Build with gmake" - # don't do JBMC so as to keep the overall time in check - gmake -C src minisat2-download - gmake -C src -j2 CXX="ccache g++" - # gmake -C jbmc/src setup-submodules - # gmake -C jbmc/src -j2 CXX="ccache g++" - gmake -C unit "CXX=ccache g++" - # gmake -C jbmc/unit "CXX=ccache g++" - echo "Print ccache stats" - ccache -s - echo "Checking completeness of help output" - scripts/check_help.sh g++ - echo "Run unit tests" - # TODO: unit tests are failing, requires debugging - gmake -C unit test || true - # gmake -C jbmc/unit test - echo "Running expected failure tests" - gmake TAGS='[!shouldfail]' -C unit test - # gmake TAGS='[!shouldfail]' -C jbmc/unit test - echo "Run regression tests" - # TODO: we need to model some more library functions - gmake -C regression/cbmc test || true - # gmake -C regression test-parallel JOBS=2 - # gmake -C regression/cbmc test-paths-lifo - # env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2 - # # gmake -C jbmc/regression test-parallel JOBS=2 diff --git a/.github/workflows/build-and-test-Linux.yaml b/.github/workflows/build-and-test-Linux.yaml deleted file mode 100644 index 2ab7e0a4dfd..00000000000 --- a/.github/workflows/build-and-test-Linux.yaml +++ /dev/null @@ -1,54 +0,0 @@ -name: Build Linux partially with CPROVER tools - -on: - pull_request: - branches: - - '**' - -jobs: - # This job takes approximately 18 minutes - CompileLinux: - runs-on: ubuntu-20.04 - steps: - - uses: actions/checkout@v4 - with: - submodules: true - - name: Install Packages - 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 clang-10 clang++-10 flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache - sudo apt-get install --no-install-recommends -y libssl-dev libelf-dev libudev-dev libpci-dev libiberty-dev autoconf - sudo apt-get install --no-install-recommends -y gawk jq - - - name: Prepare ccache - uses: actions/cache@v3 - with: - path: .ccache - key: ${{ runner.os }}-20.04-make-clang-${{ github.ref }}-${{ github.sha }}-KERNEL - 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 CBMC tools - run: | - make -C src minisat2-download - make -C src CXX='ccache /usr/bin/clang++' cbmc.dir goto-cc.dir goto-diff.dir -j2 - - name: Print ccache stats - run: ccache -s - - - name: Run (Docker Based) Linux Build test - run: integration/linux/compile_linux.sh - - - uses: actions/upload-artifact@v4 - with: - name: CPROVER-faultyInput - path: CPROVER/faultyInput/* diff --git a/.github/workflows/build-and-test-Xen.yaml b/.github/workflows/build-and-test-Xen.yaml index 66779668fcc..283c0e083a7 100644 --- a/.github/workflows/build-and-test-Xen.yaml +++ b/.github/workflows/build-and-test-Xen.yaml @@ -61,3 +61,9 @@ jobs: - name: Check for goto-cc section in xen-syms binary run: objdump -h xen_4_13/xen/xen-syms | grep "goto-cc" + + - name: Show goto-cc properties + run: $(pwd)/src/cbmc/cbmc --show-properties xen_4_13/xen/xen-syms + + - name: Show some goto-cc functions + run: $(pwd)/src/cbmc/cbmc --list-goto-functions xen_4_13/xen/xen-syms | grep "arch" diff --git a/.github/workflows/codeql-analysis.yml b/.github/workflows/codeql-analysis.yml deleted file mode 100644 index e8c6a919338..00000000000 --- a/.github/workflows/codeql-analysis.yml +++ /dev/null @@ -1,54 +0,0 @@ -name: "CodeQL" - -on: - push: - branches: [ develop ] - pull_request: - branches: [ develop ] - -jobs: - # This job takes approximately 82 minutes - analyze: - name: Analyze - runs-on: ubuntu-latest - permissions: - actions: read - contents: read - security-events: write - - strategy: - fail-fast: false - matrix: - language: [ 'cpp', 'java', 'javascript', 'python' ] - - steps: - - name: Checkout repository - uses: actions/checkout@v4 - with: - submodules: recursive - - # Initializes the CodeQL tools for scanning. - - name: Initialize CodeQL - uses: github/codeql-action/init@v3 - with: - languages: ${{ matrix.language }} - # If you wish to specify custom queries, you can do so here or in a config file. - # By default, queries listed here will override any specified in a config file. - # Prefix the list here with "+" to use these queries and those in the config file. - # queries: ./path/to/local/query, your-org/your-repo/queries@main - - - name: Install dependencies - run: | - sudo apt-get update - sudo apt-get install --no-install-recommends -yq maven flex bison - - - name: Build - run: | - make -C src minisat2-download - make -C src -j2 - make -C unit -j2 - make -C jbmc/src -j2 - make -C jbmc/unit -j2 - - - name: Perform CodeQL Analysis - uses: github/codeql-action/analyze@v3 diff --git a/.github/workflows/csmith.yaml b/.github/workflows/csmith.yaml deleted file mode 100644 index a5e144ac055..00000000000 --- a/.github/workflows/csmith.yaml +++ /dev/null @@ -1,47 +0,0 @@ -name: Run CSmith - -on: - pull_request: - branches: [ develop ] - -jobs: - # This job takes approximately 18 minutes - run-10-random-tests: - 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 -y build-essential flex bison maven ccache clang-10 clang++-10 - sudo apt-get install --no-install-recommends -y csmith libcsmith-dev - make -C src minisat2-download - - name: Prepare ccache - uses: actions/cache@v3 - with: - path: .ccache - key: ${{ runner.os }}-20.04-make-clang-${{ github.ref }}-${{ github.sha }}-CSMITH - 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 CXX='ccache /usr/bin/clang++' cbmc.dir goto-cc.dir goto-instrument.dir -j2 - - name: Print ccache stats - run: ccache -s - - name: Run 10 randomly-generated CSmith tests - run: | - export PATH=$PWD/src/cbmc:$PWD/src/goto-cc:$PWD/src/goto-instrument:$PATH - scripts/csmith.sh 10 diff --git a/.github/workflows/doxygen-check.yaml b/.github/workflows/doxygen-check.yaml deleted file mode 100644 index 07d28bd3654..00000000000 --- a/.github/workflows/doxygen-check.yaml +++ /dev/null @@ -1,23 +0,0 @@ -name: Build Doxygen Documentation -on: - pull_request: - branches: [ develop ] - -jobs: - # This job takes approximately 2 minutes - check-doxygen: - # Note that the versions used for this `check-doxygen` job should be kept in - # sync with the `publish` job. - runs-on: ubuntu-22.04 - steps: - - uses: actions/checkout@v4 - - 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 doxygen graphviz - - name: Run Doxygen - run: ./scripts/run_doxygen.sh diff --git a/.github/workflows/publish.yaml b/.github/workflows/publish.yaml deleted file mode 100644 index 562fd038bc7..00000000000 --- a/.github/workflows/publish.yaml +++ /dev/null @@ -1,40 +0,0 @@ -name: Publish CBMC documentation -on: [push, pull_request] - -jobs: - # This job takes approximately 3 minutes - publish: - # Note that the versions used for this `publish` job should be kept in sync - # with the `check-doxygen` job. - runs-on: ubuntu-22.04 - steps: - - name: Checkout repository - uses: actions/checkout@v4 - - - name: Install doxygen - run: | - sudo apt update - sudo apt install doxygen graphviz pandoc npm - - - name: Install python modules - run: sudo python3 -m pip install gitpython pandocfilters - - - name: Install mermaid diagram filter - run: | - git clone https://github.com/raghur/mermaid-filter/ - cd mermaid-filter - sed -i '1s/{/{ "overrides": { "puppeteer": "^21" },/' package.json - sed -i '1s/^\/\/ //' index.js - npm install --loglevel verbose - sudo npm link --loglevel verbose - cd .. - - - name: Build documentation - run: cd doc/doxygen-root && make && touch html/.nojekyll - - - name: Publish documentation - if: ${{ github.event_name == 'push' && startsWith('refs/heads/develop', github.ref) }} - uses: JamesIves/github-pages-deploy-action@v4 - with: - branch: gh-pages - folder: doc/doxygen-root/html diff --git a/.github/workflows/pull-request-check-clang-format.sh b/.github/workflows/pull-request-check-clang-format.sh deleted file mode 100755 index ec19cd05ade..00000000000 --- a/.github/workflows/pull-request-check-clang-format.sh +++ /dev/null @@ -1,38 +0,0 @@ -#!/usr/bin/env bash - -# Stop on errors -set -e - -# Log information about the run of this check. -echo "Pull request's base branch is: ${BASE_BRANCH}" -echo "Pull request's merge branch is: ${MERGE_BRANCH}" -echo "Pull request's source branch is: ${GITHUB_HEAD_REF}" -clang-format-11 --version - -# The checkout action leaves us in detatched head state. The following line -# names the checked out commit, for simpler reference later. -git checkout -b ${MERGE_BRANCH} - -# Build list of files to ignore -while read file ; do EXCLUDES+="':(top,exclude)$file' " ; done < .clang-format-ignore - -# Make sure we can refer to ${BASE_BRANCH} by name -git checkout ${BASE_BRANCH} -git checkout ${MERGE_BRANCH} - -# Find the commit on which the PR is based. -MERGE_BASE=$(git merge-base ${BASE_BRANCH} ${MERGE_BRANCH}) -echo "Checking for formatting errors introduced since $MERGE_BASE" - -# Do the checking. "eval" is used so that quotes (as inserted into $EXCLUDES -# above) are not interpreted as parts of file names. -eval git-clang-format-11 --binary clang-format-11 $MERGE_BASE -- $EXCLUDES -git diff > formatted.diff -if [[ -s formatted.diff ]] ; then - echo 'Formatting error! The following diff shows the required changes' - echo 'Use the raw log to get a version of the diff that preserves spacing' - cat formatted.diff - exit 1 -fi -echo 'No formatting errors found' -exit 0 diff --git a/.github/workflows/pull-request-check-cpplint.sh b/.github/workflows/pull-request-check-cpplint.sh deleted file mode 100755 index 3c3a251ab62..00000000000 --- a/.github/workflows/pull-request-check-cpplint.sh +++ /dev/null @@ -1,24 +0,0 @@ -#!/usr/bin/env bash - -# Stop on errors -set -e - -# Log information about the run of this check. -echo "Pull request's base branch is: ${BASE_BRANCH}" -echo "Pull request's merge branch is: ${MERGE_BRANCH}" -echo "Pull request's source branch is: ${GITHUB_HEAD_REF}" - -# The checkout action leaves us in detatched head state. The following line -# names the checked out commit, for simpler reference later. -git checkout -b ${MERGE_BRANCH} - -# Make sure we can refer to ${BASE_BRANCH} by name -git checkout ${BASE_BRANCH} -git checkout ${MERGE_BRANCH} - -# Find the commit on which the PR is based. -MERGE_BASE=$(git merge-base ${BASE_BRANCH} ${MERGE_BRANCH}) -echo "Checking standards of code touched since $MERGE_BASE" - -# Do the checking. -./scripts/run_diff.sh CPPLINT $MERGE_BASE diff --git a/.github/workflows/pull-request-check-rust-api.yaml b/.github/workflows/pull-request-check-rust-api.yaml deleted file mode 100644 index 8a48bcfa98f..00000000000 --- a/.github/workflows/pull-request-check-rust-api.yaml +++ /dev/null @@ -1,109 +0,0 @@ -name: Build and Test the Rust API -on: - push: - branches: [ develop ] - pull_request: - branches: [ develop ] -env: - default_build_dir: "build/" - default_solver: "minisat2" - default_include_dir: "src/libcprover-cpp/" - -# For now, we support two jobs: A Linux and a MacOS based one. -# Both of the jobs use CMake, as we only support building the Rust -# API with CMake (due to dependencies on CMake plugins). -jobs: - check-ubuntu-22_04-cmake-clang-rust: - runs-on: ubuntu-22.04 - env: - CC: "ccache /usr/bin/clang-13" - CXX: "ccache /usr/bin/clang++-13" - 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-13 clang++-13 flex bison libxml2-utils ccache - - name: Log cargo/rust version - run: cargo --version - - name: Prepare ccache - uses: actions/cache@v3 - with: - path: .ccache - key: ${{ runner.os }}-22.04-cmake-clang-${{ github.ref }}-${{ github.sha }}-PR - restore-keys: | - ${{ runner.os }}-22.04-cmake-clang-${{ github.ref }} - ${{ runner.os }}-22.04-cmake-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 - # In our experiments while building this action script, the Ubuntu 22.04 build was failing with - # the compiler indicating that it wanted the libraries to be built with `-fPIE` while it was - # trying to link the Rust project. This was remedied by adding the `Position Independent Code` - # directive during CBMC build time. It's worth mentioning that this wasn't observed on our - # local experiments on the same platform, but it seems to be doing no harm to the build overall - # and allows us to test the Rust API on Linux without issues. - - name: Configure using CMake - run: cmake -S. -B${{env.default_build_dir}} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DCMAKE_C_COMPILER=/usr/bin/clang-13 -DCMAKE_CXX_COMPILER=/usr/bin/clang++-13 -DWITH_JBMC=OFF - - name: Build with CMake - run: cmake --build ${{env.default_build_dir}} -j2 --target cprover-api-cpp - - name: Print ccache stats - run: ccache -s - # We won't be running any of the regular regression tests, as these are covered - # by the other jobs already present in `pull-request-checks.yaml`. - - name: Run Rust API tests - run: | - VERSION=$(cat src/config.inc | python3 -c "import sys,re;line = [line for line in sys.stdin if re.search(r'CBMC_VERSION = (\d+\.\d+\.\d+)', line)];sys.stdout.write(re.search(r'CBMC_VERSION = (\d+\.\d+\.\d+)', line[0]).group(1))") - cd src/libcprover-rust;\ - cargo clean;\ - CBMC_INCLUDE_DIR=../../${{env.default_include_dir}} CBMC_LIB_DIR=../../${{env.default_build_dir}}/lib CBMC_VERSION=$VERSION cargo test -- --test-threads=1 - - - check-macos-13-cmake-clang-rust: - runs-on: macos-13 - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: Fetch dependencies - run: brew install cmake ninja flex bison ccache - - name: Log cargo/rust version - run: cargo --version - - name: Prepare ccache - uses: actions/cache@v3 - with: - path: .ccache - key: ${{ runner.os }}-Release-Minisat-${{ github.ref }}-${{ github.sha }}-PR-Rust-API - restore-keys: | - ${{ runner.os }}-Release-Minisat-${{ github.ref }} - ${{ runner.os }}-Release-Minisat - - 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: cmake -S. -B${{env.default_build_dir}} -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ -DWITH_JBMC=OFF - - name: Build with Ninja - run: cd ${{env.default_build_dir}}; ninja -j3 cprover-api-cpp - - name: Print ccache stats - run: ccache -s - # We won't be running any of the regular regression tests, as these are covered - # by the other jobs already present in `pull-request-checks.yaml`. - - name: Run Rust API tests - run: | - export MACOSX_DEPLOYMENT_TARGET=10.15 - VERSION=$(cat src/config.inc | python3 -c "import sys,re;line = [line for line in sys.stdin if re.search(r'CBMC_VERSION = (\d+\.\d+\.\d+)', line)];sys.stdout.write(re.search(r'CBMC_VERSION = (\d+\.\d+\.\d+)', line[0]).group(1))") - cd src/libcprover-rust;\ - cargo clean;\ - CBMC_INCLUDE_DIR=../../${{env.default_include_dir}} CBMC_LIB_DIR=../../${{env.default_build_dir}}/lib CBMC_VERSION=$VERSION cargo test -- --test-threads=1 diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml deleted file mode 100644 index f9eacdf8071..00000000000 --- a/.github/workflows/pull-request-checks.yaml +++ /dev/null @@ -1,960 +0,0 @@ -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@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 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@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@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@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@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@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 /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@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@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@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@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@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 -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@v3 - with: - 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@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@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@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@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@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@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@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@v4 - with: - submodules: recursive - - name: Setup Visual Studio environment - uses: microsoft/setup-msbuild@v1 - - 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@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@v4 - with: - submodules: recursive - - name: Setup MSBuild - uses: microsoft/setup-msbuild@v1 - - 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@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@v4 - with: - submodules: recursive - - name: Setup Visual Studio environment - uses: microsoft/setup-msbuild@v1 - - 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@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@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@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 diff --git a/.github/workflows/regular-release.yaml b/.github/workflows/regular-release.yaml deleted file mode 100644 index b9ef25e915f..00000000000 --- a/.github/workflows/regular-release.yaml +++ /dev/null @@ -1,106 +0,0 @@ -on: - push: - tags: - - 'cbmc-*' - -name: Create Release - -jobs: - get-version-information: - name: Get Version Information - runs-on: ubuntu-20.04 - outputs: - version: ${{ steps.split-version.outputs._1 }} - steps: - - uses: jungwinter/split@v2 - id: split - with: - msg: ${{ github.ref }} - seperator: '/' - - uses: jungwinter/split@v2 - id: split-version - with: - msg: ${{ steps.split.outputs._2 }} - seperator: '-' - perform-release: - name: Perform Release - runs-on: ubuntu-20.04 - needs: get-version-information - steps: - - name: Checkout code - uses: actions/checkout@v4 - - name: Create release - uses: actions/create-release@v1 - env: - GITHUB_TOKEN: ${{ secrets.DB_CI_CPROVER_ACCESS_TOKEN }} - CBMC_VERSION: ${{ needs.get-version-information.outputs.version }} - with: - tag_name: cbmc-${{ env.CBMC_VERSION }} - release_name: cbmc-${{ env.CBMC_VERSION }} - draft: false - prerelease: false - body: | - This is CBMC version ${{ env.CBMC_VERSION }}. - - ## MacOS - - On MacOS, install CBMC using [Homebrew](https://brew.sh/) with - - ```sh - brew install cbmc - ``` - - or upgrade (if it's already been installed) with: - - ```sh - brew upgrade cbmc - ``` - - ## Ubuntu - - On Ubuntu, install CBMC by downloading the *.deb package below for your version of Ubuntu and install with - - ```sh - # Ubuntu 20: - $ dpkg -i ubuntu-20.04-cbmc-${{ env.CBMC_VERSION }}-Linux.deb - ``` - - ## Windows - - On Windows, install CBMC by downloading the `cbmc-${{ env.CBMC_VERSION }}-win64.msi` installer below, double-clicking on the installer to run it, and adding the folder `C:\Program Files\cbmc\bin` in your `PATH` environment variable. - - For installation from the windows command prompt, run: - - ```sh - msiexec /i cbmc-${{ env.CBMC_VERSION }}-win64.msi - PATH="C:\Program Files\cbmc\bin";%PATH% - ``` - - Note that we depend on the Visual C++ redistributables. You likely already have these, if not please download and run vcredist.x64.exe from Microsoft to install them prior to running cbmc, or make sure you have Visual Studio 2019 installed. - - You can download either [Visual Studio 2019 Community Edition](https://visualstudio.microsoft.com/vs/community/) or the [Visual C++ Redistributables](https://support.microsoft.com/en-gb/help/2977003/the-latest-supported-visual-c-downloads) from Microsoft for free. - - ## Docker - - We are also releasing new versions as images in [Dockerhub](https://hub.docker.com/r/diffblue/cbmc). - - To run the CProver suite of tools under a Docker container, make sure that - [Docker](https://www.docker.com/) is already installed in your system and - set up correctly, and then issue: - - ```sh - $ docker run -it diffblue/cbmc:${{ env.CBMC_VERSION }} - # - ``` - - That will initialise an execution of the container based on the image pushed - as part of this release. The CProver tools are present in the `$PATH` of the - container. - - name: Slack notification of successful release - uses: rtCamp/action-slack-notify@v2 - env: - SLACK_CHANNEL: team_open_source - SLACK_COLOR: ${{ job.status }} - SLACK_USERNAME: Github Actions CI bot - SLACK_WEBHOOK: ${{ secrets.SLACK_WEBHOOK }} - SLACK_MESSAGE: "${{ job.status == 'success' && 'Successful creation of new CBMC release page' || 'Failed to create new CBMC release page' }}" diff --git a/.github/workflows/release-packages.yaml b/.github/workflows/release-packages.yaml deleted file mode 100644 index a8e08f94804..00000000000 --- a/.github/workflows/release-packages.yaml +++ /dev/null @@ -1,306 +0,0 @@ -on: - release: - types: [created] -env: - cvc5-version: "1.0.0" - -name: Upload additional release assets -jobs: - ubuntu-22_04-package: - runs-on: ubuntu-22.04 - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: Fetch dependencies - run: | - sudo apt-get update - sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev 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 }}-22.04-Release-${{ github.ref }}-${{ github.sha }}-RELEASEPKG - 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 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: Zero ccache stats and limit in size - run: ccache -z --max-size=500M - - name: Build using Ninja - run: ninja -C build -j2 - - name: Print ccache stats - run: ccache -s - - name: Run CTest - run: cd build; ctest . -V -L CORE -C Release -j2 - - name: Create packages - id: create_packages - run: | - cd build - ninja package - deb_package_name="$(ls *.deb)" - echo "deb_package=./build/$deb_package_name" >> $GITHUB_OUTPUT - echo "deb_package_name=ubuntu-22.04-$deb_package_name" >> $GITHUB_OUTPUT - - name: Get release info - id: get_release_info - uses: bruceadams/get-release@v1.3.2 - - name: Upload binary packages - uses: actions/upload-release-asset@v1 - with: - upload_url: ${{ steps.get_release_info.outputs.upload_url }} - asset_path: ${{ steps.create_packages.outputs.deb_package }} - asset_name: ${{ steps.create_packages.outputs.deb_package_name }} - asset_content_type: application/x-deb - - name: Slack notification of CI status - uses: rtCamp/action-slack-notify@v2 - if: success() || failure() - env: - SLACK_CHANNEL: aws-cbmc - SLACK_COLOR: ${{ job.status }} - SLACK_USERNAME: Github Actions CI bot - SLACK_WEBHOOK: ${{ secrets.SLACK_WEBHOOK }} - SLACK_MESSAGE: "${{ job.status == 'success' && 'Ubuntu 22.04 package built and uploaded successfully' || 'Ubuntu 22.04 package build failed' }}" - - ubuntu-20_04-package: - runs-on: ubuntu-20.04 - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: Fetch dependencies - run: | - sudo apt-get update - sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev 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-Release-${{ github.ref }}-${{ github.sha }}-RELEASEPKG - 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 CMake - run: | - mkdir build - cd build - cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -Dsat_impl="minisat2;cadical" - - name: Zero ccache stats and limit in size - run: ccache -z --max-size=500M - - name: Build using Ninja - run: ninja -C build -j2 - - name: Print ccache stats - run: ccache -s - - name: Run CTest - run: cd build; ctest . -V -L CORE -C Release -j2 - - name: Create packages - id: create_packages - run: | - cd build - ninja package - deb_package_name="$(ls *.deb)" - echo "deb_package=./build/$deb_package_name" >> $GITHUB_OUTPUT - echo "deb_package_name=ubuntu-20.04-$deb_package_name" >> $GITHUB_OUTPUT - - name: Get release info - id: get_release_info - uses: bruceadams/get-release@v1.3.2 - - name: Upload binary packages - uses: actions/upload-release-asset@v1 - with: - upload_url: ${{ steps.get_release_info.outputs.upload_url }} - asset_path: ${{ steps.create_packages.outputs.deb_package }} - asset_name: ${{ steps.create_packages.outputs.deb_package_name }} - asset_content_type: application/x-deb - - name: Slack notification of CI status - uses: rtCamp/action-slack-notify@v2 - if: success() || failure() - env: - SLACK_CHANNEL: aws-cbmc - SLACK_COLOR: ${{ job.status }} - SLACK_USERNAME: Github Actions CI bot - SLACK_WEBHOOK: ${{ secrets.SLACK_WEBHOOK }} - SLACK_MESSAGE: "${{ job.status == 'success' && 'Ubuntu 20.04 package built and uploaded successfully' || 'Ubuntu 20.04 package build failed' }}" - - homebrew-pr: - runs-on: macos-11 - steps: - - name: Get release tag name - # The GITHUB_REF we get has refs/tags/ in front of the tag name so we - # strip that here - run: echo "RELEASE_TAG=${GITHUB_REF/refs\/tags\/}" >> $GITHUB_ENV - - name: Configure git user name and email - uses: Homebrew/actions/git-user-config@07da0794847043a11761f14c97cc682577c74d5d - with: - username: db-ci-cprover - - name: Create homebrew PR - run: | - brew update-reset - brew bump-formula-pr --tag "$RELEASE_TAG" --revision "$GITHUB_SHA" cbmc - env: - HOMEBREW_GITHUB_API_TOKEN: ${{ secrets.DB_CI_CPROVER_ACCESS_TOKEN }} - - name: Checkout CBMC project source code to obtain access to scripts - if: always() - uses: actions/checkout@v4 - - name: Slack notification of CI status - if: success() || failure() - env: - SLACK_CHANNEL: aws-cbmc - SLACK_COLOR: ${{ job.status }} - SLACK_USERNAME: Github Actions CI bot - SLACK_WEBHOOK: ${{ secrets.SLACK_WEBHOOK }} - SLACK_MESSAGE: "${{ job.status == 'success' && 'Homebrew PR submitted successfully' || 'Homebrew PR failed' }}" - run: go run scripts/slack_notification_action.go - - 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@v1 - - name: Fetch dependencies - run: | - choco install winflexbison3 - nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0 - echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH - - name: Setup code sign environment - run: | - echo "$(Split-Path -Path $(Get-ChildItem -Path "${env:ProgramFiles(x86)}\Windows Kits\10\App Certification Kit\signtool.exe"))" >> $env:GITHUB_PATH - echo "pfxcert=$([string](Get-Location)+'\CodeSignCertificate.pfx')" >> $env:GITHUB_ENV - - name: Prepare ccache - uses: actions/cache@v3 - with: - path: .ccache - key: ${{ runner.os }}-msbuild-${{ github.ref }}-${{ github.sha }}-RELEASEPKG - 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 -Filter *.msi -Name - echo "msi_installer=build/$msi_name" >> $env:GITHUB_OUTPUT - echo "msi_name=$msi_name" >> $env:GITHUB_OUTPUT - - name: Decode signing certificate - id: decode_certificate - run: | - $pfx_bytes=[System.Convert]::FromBase64String("${{ secrets.CODESIGNCERTPFX }}") - [IO.File]::WriteAllBytes($env:pfxcert, $pfx_bytes) - - name: Sign the installer - id: code_sign - run: | - $servers = @('http://ts.ssl.com', 'http://timestamp.digicert.com', 'http://timestamp.sectigo.com') - foreach($ts_server in $servers) - { - & signtool.exe sign /f $env:pfxcert /p "${{ secrets.CODESIGNCERTPASSWORD }}" /tr $ts_server /td SHA256 /fd SHA256 ${{ steps.create_packages.outputs.msi_installer }} - if ($LastExitCode -eq "0") - { - # Stop if code-signing the binary using this server was successful. - break - } - } - - name: Remove signing certificate - id: remove_certificate - run: | - Remove-Item $env:pfxcert - - name: Verify installer signature - id: verify_codesign - run: | - & signtool.exe verify /pa ${{ steps.create_packages.outputs.msi_installer }} - - name: Get release info - id: get_release_info - uses: bruceadams/get-release@v1.3.2 - - name: Upload binary packages - uses: actions/upload-release-asset@v1 - with: - upload_url: ${{ steps.get_release_info.outputs.upload_url }} - asset_path: ${{ steps.create_packages.outputs.msi_installer }} - asset_name: ${{ steps.create_packages.outputs.msi_name }} - asset_content_type: application/x-msi - - name: Slack notification of CI status - if: success() || failure() - env: - SLACK_CHANNEL: aws-cbmc - SLACK_COLOR: ${{ job.status }} - SLACK_USERNAME: Github Actions CI bot - SLACK_WEBHOOK: ${{ secrets.SLACK_WEBHOOK }} - SLACK_MESSAGE: "${{ job.status == 'success' && 'Windows package built and uploaded successfully' || 'Windows package build failed' }}" - run: go run scripts/slack_notification_action.go - - push-docker-image-dockerhub: - runs-on: ubuntu-20.04 - steps: - - name: Checkout CBMC source - uses: actions/checkout@v4 - with: - submodules: recursive - - name: Set Image Tag - run: | - # Isolate the version number from a reference to a tag, for example, - # '5.20.3' from a string like 'refs/tags/cbmc-5.20.3-exp' - VERSION=$(echo ${{ github.ref }} | cut -d "/" -f 3 | cut -d "-" -f 2) - echo "IMAGE_TAG=diffblue/cbmc:$VERSION" >> $GITHUB_ENV - - name: Build docker image - run: docker build -t "$IMAGE_TAG" . - - name: Push docker image to DockerHub - run: | - echo ${{ secrets.DOCKERHUB_ACCESS_DB_CI_CPROVER }} | docker login --username=dbcicprover --password-stdin - docker image push "$IMAGE_TAG" - # For security reasons remove stored login credentials from - # configuration file they are stored at by docker login. - docker logout - - name: Slack notification of CI status - uses: rtCamp/action-slack-notify@v2 - if: success() || failure() - env: - SLACK_CHANNEL: aws-cbmc - SLACK_COLOR: ${{ job.status }} - SLACK_USERNAME: Github Actions CI bot - SLACK_WEBHOOK: ${{ secrets.SLACK_WEBHOOK }} - SLACK_MESSAGE: "${{ job.status == 'success' && 'Docker Image built and submitted to DockerHub successfully' || 'Docker Image build failed' }}" diff --git a/.github/workflows/smoke_test_assets/Test.java b/.github/workflows/smoke_test_assets/Test.java deleted file mode 100644 index eb27c41854d..00000000000 --- a/.github/workflows/smoke_test_assets/Test.java +++ /dev/null @@ -1,6 +0,0 @@ -public class Test { - public static void main(String[] args) { - System.out.println("Hi"); - assert(1 == 1); - } -} diff --git a/.github/workflows/smoke_test_assets/test.c b/.github/workflows/smoke_test_assets/test.c deleted file mode 100644 index 5e32995f692..00000000000 --- a/.github/workflows/smoke_test_assets/test.c +++ /dev/null @@ -1,9 +0,0 @@ -#include - -#define return_val 0; - -int main(void) -{ - assert(1 == 1); - return return_val; -} diff --git a/.github/workflows/syntax-checks.yaml b/.github/workflows/syntax-checks.yaml deleted file mode 100644 index 4678d6bf388..00000000000 --- a/.github/workflows/syntax-checks.yaml +++ /dev/null @@ -1,61 +0,0 @@ -name: Syntactic checks -on: - pull_request: - branches: [ develop ] - -jobs: - # This job takes approximately 1 minute - check-clang-format: - runs-on: ubuntu-20.04 - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - fetch-depth: 0 - - 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-format-11 - - name: Check updated lines of code match clang-format-11 style - env: - BASE_BRANCH: ${{ github.base_ref }} - MERGE_BRANCH: ${{ github.ref }} - run: ./.github/workflows/pull-request-check-clang-format.sh - - # This job takes approximately 1 minute - check-cpplint: - runs-on: ubuntu-20.04 - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - fetch-depth: 0 - - 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 python3-unidiff - - name: Check updated lines of code meet linting standards - env: - BASE_BRANCH: ${{ github.base_ref }} - MERGE_BRANCH: ${{ github.ref }} - run: ./.github/workflows/pull-request-check-cpplint.sh - - # This job should take about a minute (est) - check-rustfmt: - runs-on: ubuntu-latest - steps: - - name: Checkout CBMC repository - uses: actions/checkout@v4 - - name: Install latest stable Rust toolchain - run: | - rustup toolchain install stable --profile minimal --no-self-update -c clippy -c rustfmt - - name: Run `cargo fmt` on top of Rust API project - run: cd src/libcprover-rust; cargo fmt --all -- --check