Skip to content

ci: temporarily disable CBMC checks (known-broken) #14

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
shigoel wants to merge 1 commit into
base: main
Choose a base branch
from
+71 −58
Open

ci: temporarily disable CBMC checks (known-broken) #14

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
129 changes: 71 additions & 58 deletions .github/workflows/cbmc.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,63 +10,76 @@ jobs:
permissions:
contents: read
steps:
- name: Checkout
uses: actions/checkout@v6
- name: Install cvc5
uses: strata-org/Strata/.github/actions/install-cvc5@main
- name: Install z3
uses: strata-org/Strata/.github/actions/install-z3@main
- name: Restore lake cache
# The cache is safe to use here because we just saved it for this exact
# SHA in the build_and_test_lean job from ci.yml. Restoring it also
# brings back the cloned Strata dependency under .lake/packages/Strata,
# which holds the Laurel/regex/quantifier CBMC patches applied below.
# https://github.com/strata-org/Strata/issues/952
uses: ./.github/actions/restore-lake-cache
with:
path: .lake
fail-on-cache-miss: "true"
use-restore-keys: "false"
- name: Prepare ccache
uses: actions/cache@v5
with:
save-always: true
path: .ccache
key: cbmc-${{ runner.os }}-${{ runner.arch }}-cbmc-${{ github.sha }}
restore-keys: |
cbmc-${{ runner.os }}-${{ runner.arch }}-cbmc
- name: Build CBMC from source (with string support patch)
# CBMC checks are temporarily disabled — they are currently known-broken
# and will be re-enabled once fixed. The original steps are preserved as
# comments below; to restore CBMC, delete the no-op step and uncomment
# everything between the ORIGINAL CBMC STEPS markers.
- name: CBMC temporarily disabled
shell: bash
run: |
sudo apt-get -qq update
sudo apt-get -qq install -y cmake ninja-build flex bison ccache
git clone --depth 1 --branch cbmc-6.8.0 https://github.com/diffblue/cbmc.git cbmc-src
cd cbmc-src
STRATA="$GITHUB_WORKSPACE/.lake/packages/Strata"
git apply "$GITHUB_WORKSPACE/StrataPythonTest/cbmc-string-support.patch"
git apply "$STRATA/StrataTest/Languages/Laurel/CBMC/cbmc-bounds-check.patch"
git apply "$STRATA/StrataTest/Backends/CBMC/cbmc-regex-support.patch"
git apply "$STRATA/StrataTest/Backends/CBMC/cbmc-quantifier-simplify.patch"
export CCACHE_BASEDIR=$PWD
export CCACHE_DIR=$GITHUB_WORKSPACE/.ccache
cmake -S . -B build -G Ninja \
-DCMAKE_BUILD_TYPE=Release \
-DWITH_JBMC=OFF
ccache -z --max-size=500M
ninja -C build cbmc symtab2gb goto-cc goto-instrument
ccache -s
echo "$GITHUB_WORKSPACE/cbmc-src/build/bin/" >> $GITHUB_PATH
- name: Build StrataPython
uses: leanprover/lean-action@v1
with:
auto-config: false
build: true
use-github-cache: false
- uses: actions/setup-python@v6
with:
python-version: '3.14'
- name: Run Python CBMC pipeline tests
shell: bash
run: |
pip install ./.lake/packages/StrataDDM/Python/strata ./Python/strata-python
./StrataPythonTest/run_py_cbmc_tests.sh
echo "::warning::CBMC checks are temporarily disabled (known-broken; will be re-enabled once fixed)."
echo "CBMC checks are temporarily disabled."
echo "These checks are currently known-broken and will be re-enabled once fixed."
exit 0
# --- ORIGINAL CBMC STEPS (temporarily disabled) ---
# - name: Checkout
# uses: actions/checkout@v6
# - name: Install cvc5
# uses: strata-org/Strata/.github/actions/install-cvc5@main
# - name: Install z3
# uses: strata-org/Strata/.github/actions/install-z3@main
# - name: Restore lake cache
# # The cache is safe to use here because we just saved it for this exact
# # SHA in the build_and_test_lean job from ci.yml. Restoring it also
# # brings back the cloned Strata dependency under .lake/packages/Strata,
# # which holds the Laurel/regex/quantifier CBMC patches applied below.
# # https://github.com/strata-org/Strata/issues/952
# uses: ./.github/actions/restore-lake-cache
# with:
# path: .lake
# fail-on-cache-miss: "true"
# use-restore-keys: "false"
# - name: Prepare ccache
# uses: actions/cache@v5
# with:
# save-always: true
# path: .ccache
# key: cbmc-${{ runner.os }}-${{ runner.arch }}-cbmc-${{ github.sha }}
# restore-keys: |
# cbmc-${{ runner.os }}-${{ runner.arch }}-cbmc
# - name: Build CBMC from source (with string support patch)
# shell: bash
# run: |
# sudo apt-get -qq update
# sudo apt-get -qq install -y cmake ninja-build flex bison ccache
# git clone --depth 1 --branch cbmc-6.8.0 https://github.com/diffblue/cbmc.git cbmc-src
# cd cbmc-src
# STRATA="$GITHUB_WORKSPACE/.lake/packages/Strata"
# git apply "$GITHUB_WORKSPACE/StrataPythonTest/cbmc-string-support.patch"
# git apply "$STRATA/StrataTest/Languages/Laurel/CBMC/cbmc-bounds-check.patch"
# git apply "$STRATA/StrataTest/Backends/CBMC/cbmc-regex-support.patch"
# git apply "$STRATA/StrataTest/Backends/CBMC/cbmc-quantifier-simplify.patch"
# export CCACHE_BASEDIR=$PWD
# export CCACHE_DIR=$GITHUB_WORKSPACE/.ccache
# cmake -S . -B build -G Ninja \
# -DCMAKE_BUILD_TYPE=Release \
# -DWITH_JBMC=OFF
# ccache -z --max-size=500M
# ninja -C build cbmc symtab2gb goto-cc goto-instrument
# ccache -s
# echo "$GITHUB_WORKSPACE/cbmc-src/build/bin/" >> $GITHUB_PATH
# - name: Build StrataPython
# uses: leanprover/lean-action@v1
# with:
# auto-config: false
# build: true
# use-github-cache: false
# - uses: actions/setup-python@v6
# with:
# python-version: '3.14'
# - name: Run Python CBMC pipeline tests
# shell: bash
# run: |
# pip install ./.lake/packages/StrataDDM/Python/strata ./Python/strata-python
# ./StrataPythonTest/run_py_cbmc_tests.sh
# --- END ORIGINAL CBMC STEPS ---