Skip to content

Commit 1b71b48

Browse files
tautschnigkiro-agent
tautschnig
and
kiro-agent
committed
TEMPORARY: debug FreeBSD fread SSP issue
Disable OpenBSD/NetBSD jobs, strip FreeBSD to just build + fread debugging. Change __fread_chk.desc to --preprocess to dump the preprocessed source on FreeBSD. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
1 parent b82d64e commit 1b71b48

2 files changed

Lines changed: 10 additions & 160 deletions

File tree

‎.github/workflows/bsd.yaml‎

Lines changed: 9 additions & 157 deletions
Original file line numberDiff line numberDiff line change
@@ -36,170 +36,22 @@ jobs:
3636
set -e -x
3737
echo "Fetch dependencies"
3838
pkg install -y bash gmake git www/p5-libwww python python3 patch flex bison ccache cvc5 z3
39-
echo "Fetch JBMC dependencies"
40-
pkg install -y openjdk8 wget maven
4139
echo "Zero ccache stats and limit in size"
4240
export CCACHE_BASEDIR=$PWD
4341
export CCACHE_DIR=$PWD/.ccache
4442
ccache -z --max-size=500M
4543
ccache -p
4644
echo "Build with gmake"
47-
# don't do JBMC as to keep the overall time in check
4845
gmake -C src minisat2-download
4946
gmake -C src -j2 CXX="ccache clang++"
50-
# gmake -C jbmc/src setup-submodules
51-
# gmake -C jbmc/src -j2 CXX="ccache clang++"
52-
# https://github.com/catchorg/Catch2/issues/2910 is an issue
53-
# specific to Clang/LLVM 19 (which is what FreeBSD 15 ships)
54-
gmake -C unit "CXX=ccache clang++" \
55-
CXXFLAGS="-Wall -pedantic -Werror -Wswitch-enum -Wno-deprecated-declarations -Wno-c++20-extensions"
56-
# gmake -C jbmc/unit "CXX=ccache clang++"
5747
echo "Print ccache stats"
5848
ccache -s
59-
echo "Checking completeness of help output"
60-
scripts/check_help.sh clang++
61-
echo "Run unit tests"
62-
gmake -C unit test
63-
# gmake -C jbmc/unit test
64-
echo "Running expected failure tests"
65-
gmake TAGS='[!shouldfail]' -C unit test
66-
# gmake TAGS='[!shouldfail]' -C jbmc/unit test
67-
echo "Run regression tests"
68-
gmake -C regression/cbmc test
69-
gmake -C regression/cbmc-library test
70-
# gmake -C regression test-parallel JOBS=2
71-
# gmake -C regression/cbmc test-paths-lifo
72-
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
73-
# # gmake -C jbmc/regression test-parallel JOBS=2
74-
75-
# This job takes approximately 7 to 34 minutes
76-
OpenBSD:
77-
runs-on: ubuntu-latest
78-
steps:
79-
- uses: actions/checkout@v6
80-
with:
81-
submodules: recursive
82-
- name: Prepare ccache
83-
uses: actions/cache@v5
84-
with:
85-
save-always: true
86-
path: .ccache
87-
key: openbsd-7.7-gmake-${{ github.ref }}-${{ github.sha }}-PR
88-
restore-keys: |
89-
openbsd-7.7-gmake-${{ github.ref }}
90-
openbsd-7.7-gmake
91-
- name: ccache environment
92-
run: |
93-
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
94-
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
95-
- name: Build and Test
96-
uses: vmactions/openbsd-vm@v1
97-
with:
98-
release: "7.7"
99-
run: |
100-
# apparently fail-on-error isn't the default here
101-
set -e -x
102-
echo "Fetch dependencies"
103-
pkg_add -v bash gmake llvm%16 git python3 bison ccache parallel z3
104-
ln -s $(which llvm-ar-16) /usr/local/bin/llvm-ar
105-
echo "Fetch JBMC dependencies"
106-
pkg_add -v jdk%1.8 wget maven
107-
echo "Zero ccache stats and limit in size"
108-
export CCACHE_BASEDIR=$PWD
109-
export CCACHE_DIR=$PWD/.ccache
110-
ccache -z --max-size=500M
111-
ccache -p
112-
echo "Build with gmake"
113-
# don't do JBMC so as to keep the overall time in check
114-
gmake -C src minisat2-download
115-
gmake -C src -j2 CXX="ccache clang++"
116-
# gmake -C jbmc/src setup-submodules
117-
# gmake -C jbmc/src -j2 CXX="ccache clang++"
118-
gmake -C unit "CXX=ccache clang++"
119-
# gmake -C jbmc/unit "CXX=ccache clang++"
120-
echo "Print ccache stats"
121-
ccache -s
122-
echo "Checking completeness of help output"
123-
scripts/check_help.sh clang++
124-
echo "Run unit tests"
125-
gmake -C unit test
126-
# gmake -C jbmc/unit test
127-
echo "Running expected failure tests"
128-
gmake TAGS='[!shouldfail]' -C unit test
129-
# gmake TAGS='[!shouldfail]' -C jbmc/unit test
130-
echo "Run regression tests"
131-
gmake -C regression/cbmc test
132-
# TODO: fileno and *fprintf tests are failing, requires debugging
133-
# https://github.com/openbsd/src/blob/master/include/stdio.h may be
134-
# useful (likely need to allocate __sF)
135-
gmake -C regression/cbmc-library test || true
136-
# gmake -C regression test-parallel JOBS=2
137-
# gmake -C regression/cbmc test-paths-lifo
138-
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
139-
# # gmake -C jbmc/regression test-parallel JOBS=2
140-
141-
# This job takes approximately 6 to 29 minutes
142-
NetBSD:
143-
runs-on: ubuntu-latest
144-
steps:
145-
- uses: actions/checkout@v6
146-
with:
147-
submodules: recursive
148-
- name: Prepare ccache
149-
uses: actions/cache@v5
150-
with:
151-
save-always: true
152-
path: .ccache
153-
key: netbsd-10.1-gmake-${{ github.ref }}-${{ github.sha }}-PR
154-
restore-keys: |
155-
netbsd-10.1-gmake-${{ github.ref }}
156-
netbsd-10.1-gmake
157-
- name: ccache environment
158-
run: |
159-
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
160-
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
161-
- name: Build and Test
162-
uses: vmactions/netbsd-vm@v1
163-
with:
164-
release: "10.1"
165-
run: |
166-
# apparently fail-on-error isn't the default here
167-
set -e -x
168-
echo "Fetch dependencies"
169-
pkg_add -u -v gmake git python311 patch flex bison ccache parallel z3 gcc10
170-
ln -s $(which python3.11) /usr/pkg/bin/python3
171-
export PATH=/usr/pkg/gcc10/bin:$PATH
172-
echo "Fetch JBMC dependencies"
173-
pkg_add -u -v openjdk8 wget apache-maven
174-
echo "Zero ccache stats and limit in size"
175-
export CCACHE_BASEDIR=$PWD
176-
export CCACHE_DIR=$PWD/.ccache
177-
ccache -z --max-size=500M
178-
ccache -p
179-
echo "Build with gmake"
180-
# don't do JBMC so as to keep the overall time in check
181-
gmake -C src minisat2-download
182-
gmake -C src -j2 CXX="ccache g++"
183-
# gmake -C jbmc/src setup-submodules
184-
# gmake -C jbmc/src -j2 CXX="ccache g++"
185-
gmake -C unit "CXX=ccache g++"
186-
# gmake -C jbmc/unit "CXX=ccache g++"
187-
echo "Print ccache stats"
188-
ccache -s
189-
echo "Checking completeness of help output"
190-
scripts/check_help.sh g++
191-
echo "Run unit tests"
192-
# TODO: unit tests are failing, requires debugging
193-
gmake -C unit test || true
194-
# gmake -C jbmc/unit test
195-
echo "Running expected failure tests"
196-
gmake TAGS='[!shouldfail]' -C unit test
197-
# gmake TAGS='[!shouldfail]' -C jbmc/unit test
198-
echo "Run regression tests"
199-
# TODO: we need to model some more library functions
200-
gmake -C regression/cbmc test || true
201-
gmake -C regression/cbmc-library test || true
202-
# gmake -C regression test-parallel JOBS=2
203-
# gmake -C regression/cbmc test-paths-lifo
204-
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
205-
# # gmake -C jbmc/regression test-parallel JOBS=2
49+
echo "Run fread test for debugging"
50+
gmake -C regression/cbmc-library test -j1 || true
51+
cd regression/cbmc-library
52+
echo "=== Preprocessed output ==="
53+
../../src/cbmc/cbmc --preprocess -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2 fread/main.c || true
54+
echo "=== Regular run ==="
55+
../../src/cbmc/cbmc --pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2 --unwindset fread:0 --no-unwinding-assertions fread/main.c || true
56+
echo "=== Show goto functions ==="
57+
../../src/cbmc/cbmc --show-goto-functions -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2 fread/main.c 2>&1 || true

‎regression/cbmc-library/fread/__fread_chk.desc‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,7 @@
11
CORE
22
main.c
3-
--pointer-check --bounds-check -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2 --unwindset fread:0 --no-unwinding-assertions
3+
--preprocess -D_FORTIFY_SOURCE=2 -D__OPTIMIZE__=2
44
^EXIT=0$
55
^SIGNAL=0$
6-
^VERIFICATION SUCCESSFUL$
76
--
8-
^\*\*\*\* WARNING: no body for function __fread_chk
97
^warning: ignoring

0 commit comments

Comments
 (0)