Skip to content

Commit bf7da15

Browse files
tautschnigkiro-agent
tautschnig
and
kiro-agent
committed
Investigate slow test root causes: OS vs solver
Add a focused CI workflow that runs the 4 tests marked THOROUGH in 6e616e9 across different OS × solver combinations to determine whether the slowness is inherent to the operating system or caused by the choice of SAT/SMT solver. Test matrix: - Tests 1-3 (StringSubstring, pid/C11, assigns-local-composite): {Linux, macOS-14} × {minisat2, cadical} - Test 4 (large_array_of_struct_nondet_index): {Linux, Windows} × incremental SMT2 The 4 tests are temporarily changed back to CORE so CTest picks them up. All other PR-triggered workflows are disabled to minimize CI load. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
1 parent eee45a7 commit bf7da15

15 files changed

Lines changed: 186 additions & 14 deletions

File tree

‎.github/workflows/bsd.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ on:
33
push:
44
branches: [ develop ]
55
pull_request:
6-
branches: [ develop ]
6+
branches: [ disabled-for-investigation ]
77

88
jobs:
99
# This job takes approximately 6 to 26 minutes

‎.github/workflows/build-and-test-Xen.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ name: Build Xen with CPROVER tools
22

33
on:
44
pull_request:
5-
branches: [ develop ]
5+
branches: [ disabled-for-investigation ]
66

77
jobs:
88
# This job takes approximately 33 minutes

‎.github/workflows/codeql-analysis.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ on:
44
push:
55
branches: [ develop ]
66
pull_request:
7-
branches: [ develop ]
7+
branches: [ disabled-for-investigation ]
88

99
jobs:
1010
# This job takes approximately 82 minutes

‎.github/workflows/coverage.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ on:
33
push:
44
branches: [ develop ]
55
pull_request:
6-
branches: [ develop ]
6+
branches: [ disabled-for-investigation ]
77
env:
88
cvc5-version: "1.2.1"
99
linux-vcpus: 4

‎.github/workflows/csmith.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ name: Run CSmith
22

33
on:
44
pull_request:
5-
branches: [ develop ]
5+
branches: [ disabled-for-investigation ]
66

77
jobs:
88
# This job takes approximately 18 minutes

‎.github/workflows/doxygen-check.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
name: Build Doxygen Documentation
22
on:
33
pull_request:
4-
branches: [ develop ]
4+
branches: [ disabled-for-investigation ]
55

66
jobs:
77
# This job takes approximately 2 minutes

‎.github/workflows/investigate-slow-tests.yaml‎

Lines changed: 172 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,172 @@
1+
# Temporary workflow to investigate why 4 tests are extremely slow on
2+
# certain platforms. Tests OS vs solver to determine root cause.
3+
#
4+
# Tests under investigation:
5+
# 1. jbmc-strings/StringSubstring — 650x slower on macOS-14
6+
# 2. book-examples/pid/C11.desc — 38x slower on macOS-14
7+
# 3. contracts-dfcc/assigns-local-composite — 10-14x slower on macOS/Windows
8+
# 4. cbmc-incr-smt2/structs/large_array_of_struct_nondet_index — Windows-slow
9+
#
10+
# Matrix:
11+
# Tests 1-3: {Linux, macOS-14} × {minisat2, cadical}
12+
# Test 4: {Linux, Windows} × {z3, cvc5} (incremental SMT2)
13+
14+
name: Investigate slow tests
15+
on:
16+
pull_request:
17+
branches: [ develop ]
18+
19+
env:
20+
cvc5-version: "1.2.1"
21+
22+
jobs:
23+
linux-minisat2:
24+
runs-on: ubuntu-24.04
25+
steps:
26+
- uses: actions/checkout@v6
27+
with:
28+
submodules: recursive
29+
- name: Fetch dependencies
30+
env:
31+
DEBIAN_FRONTEND: noninteractive
32+
run: |
33+
sudo apt-get update
34+
sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ flex bison maven ccache
35+
- name: Build with minisat2
36+
run: |
37+
cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -Dsat_impl=minisat2
38+
cmake --build build -j$(nproc)
39+
- name: Test StringSubstring
40+
run: cd jbmc/regression/jbmc-strings && time ../../../regression/test.pl -e -p -c "../../../../build/bin/jbmc --validate-goto-model --validate-ssa-equation" -C StringSubstring
41+
- name: Test pid/C11
42+
run: cd regression/book-examples && time ../test.pl -e -p -c "../../../build/bin/cbmc --validate-goto-model --validate-ssa-equation" -C pid
43+
- name: Test assigns-local-composite
44+
run: cd regression/contracts-dfcc && time ../test.pl -e -p -c '../chain.sh ../../../build/bin/goto-cc ../../../build/bin/goto-instrument ../../../build/bin/cbmc false true' -C assigns-local-composite
45+
46+
linux-cadical:
47+
runs-on: ubuntu-24.04
48+
steps:
49+
- uses: actions/checkout@v6
50+
with:
51+
submodules: recursive
52+
- name: Fetch dependencies
53+
env:
54+
DEBIAN_FRONTEND: noninteractive
55+
run: |
56+
sudo apt-get update
57+
sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ flex bison maven ccache
58+
- name: Build with cadical
59+
run: |
60+
cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -Dsat_impl=cadical
61+
cmake --build build -j$(nproc)
62+
- name: Test StringSubstring
63+
run: cd jbmc/regression/jbmc-strings && time ../../../regression/test.pl -e -p -c "../../../../build/bin/jbmc --validate-goto-model --validate-ssa-equation" -C StringSubstring
64+
- name: Test pid/C11
65+
run: cd regression/book-examples && time ../test.pl -e -p -c "../../../build/bin/cbmc --validate-goto-model --validate-ssa-equation" -C pid
66+
- name: Test assigns-local-composite
67+
run: cd regression/contracts-dfcc && time ../test.pl -e -p -c '../chain.sh ../../../build/bin/goto-cc ../../../build/bin/goto-instrument ../../../build/bin/cbmc false true' -C assigns-local-composite
68+
69+
macos-minisat2:
70+
runs-on: macos-14
71+
steps:
72+
- uses: actions/checkout@v6
73+
with:
74+
submodules: recursive
75+
- name: Fetch dependencies
76+
run: brew install ninja maven flex bison ccache
77+
- name: Build with minisat2
78+
run: |
79+
cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release \
80+
-DCMAKE_C_COMPILER=/usr/bin/clang \
81+
-DCMAKE_CXX_COMPILER=/usr/bin/clang++ \
82+
-Dsat_impl=minisat2
83+
cmake --build build -j3
84+
- name: Test StringSubstring
85+
run: cd jbmc/regression/jbmc-strings && time ../../../regression/test.pl -e -p -c "../../../../build/bin/jbmc --validate-goto-model --validate-ssa-equation" -C StringSubstring
86+
- name: Test pid/C11
87+
run: cd regression/book-examples && time ../test.pl -e -p -c "../../../build/bin/cbmc --validate-goto-model --validate-ssa-equation" -C pid
88+
- name: Test assigns-local-composite
89+
run: cd regression/contracts-dfcc && time ../test.pl -e -p -c '../chain.sh ../../../build/bin/goto-cc ../../../build/bin/goto-instrument ../../../build/bin/cbmc false true' -C assigns-local-composite
90+
91+
macos-cadical:
92+
runs-on: macos-14
93+
steps:
94+
- uses: actions/checkout@v6
95+
with:
96+
submodules: recursive
97+
- name: Fetch dependencies
98+
run: brew install ninja maven flex bison ccache
99+
- name: Build with cadical
100+
run: |
101+
cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release \
102+
-DCMAKE_C_COMPILER=/usr/bin/clang \
103+
-DCMAKE_CXX_COMPILER=/usr/bin/clang++ \
104+
-Dsat_impl=cadical
105+
cmake --build build -j3
106+
- name: Test StringSubstring
107+
run: cd jbmc/regression/jbmc-strings && time ../../../regression/test.pl -e -p -c "../../../../build/bin/jbmc --validate-goto-model --validate-ssa-equation" -C StringSubstring
108+
- name: Test pid/C11
109+
run: cd regression/book-examples && time ../test.pl -e -p -c "../../../build/bin/cbmc --validate-goto-model --validate-ssa-equation" -C pid
110+
- name: Test assigns-local-composite
111+
run: cd regression/contracts-dfcc && time ../test.pl -e -p -c '../chain.sh ../../../build/bin/goto-cc ../../../build/bin/goto-instrument ../../../build/bin/cbmc false true' -C assigns-local-composite
112+
113+
linux-incr-smt2:
114+
runs-on: ubuntu-24.04
115+
steps:
116+
- uses: actions/checkout@v6
117+
with:
118+
submodules: recursive
119+
- name: Fetch dependencies
120+
env:
121+
DEBIAN_FRONTEND: noninteractive
122+
run: |
123+
sudo apt-get update
124+
sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ flex bison ccache z3
125+
wget -q https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip
126+
unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5
127+
rm cvc5-Linux-x86_64-static.zip
128+
- name: Build
129+
run: |
130+
cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -Dsat_impl="minisat2;cadical"
131+
cmake --build build -j$(nproc)
132+
- name: Test large_array_of_struct_nondet_index
133+
run: cd regression/cbmc-incr-smt2 && time ../test.pl -e -p -c "../../../build/bin/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" -C structs
134+
- name: Test large_array_of_struct_nondet_index (cvc5)
135+
run: cd regression/cbmc-incr-smt2 && time ../test.pl -e -p -c "../../../build/bin/cbmc --incremental-smt2-solver 'cvc5 --lang smt2 --incremental'" -C structs
136+
137+
windows-incr-smt2:
138+
runs-on: windows-2022
139+
steps:
140+
- uses: actions/checkout@v6
141+
with:
142+
submodules: recursive
143+
- uses: microsoft/setup-msbuild@v2
144+
- uses: ilammy/msvc-dev-cmd@v1
145+
- name: Fetch dependencies
146+
run: |
147+
choco install winflexbison3 strawberryperl -y
148+
nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
149+
echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH
150+
Invoke-WebRequest -Uri https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-win.zip -OutFile .\z3.zip
151+
Expand-Archive -LiteralPath '.\z3.Zip' -DestinationPath C:\tools
152+
echo "c:\tools\z3-4.8.10-x64-win\bin;" >> $env:GITHUB_PATH
153+
New-Item -ItemType directory "C:\tools\cvc5"
154+
Invoke-WebRequest -Uri https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Win64-x86_64-static.zip -OutFile .\cvc5.zip
155+
Expand-Archive -LiteralPath '.\cvc5.zip'
156+
Move-Item -Path .\cvc5\cvc5-Win64-x86_64-static\bin\cvc5.exe c:\tools\cvc5\cvc5.exe
157+
echo "c:\tools\cvc5;" >> $env:GITHUB_PATH
158+
echo "c:\Strawberry\" >> $env:GITHUB_PATH
159+
- name: Configure and build
160+
run: |
161+
cmake -S . -B build
162+
cmake --build build --config Release
163+
- name: Test large_array_of_struct_nondet_index (z3)
164+
shell: bash
165+
run: |
166+
cd regression/cbmc-incr-smt2
167+
time perl ../test.pl -e -p -c "../../../build/bin/Release/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" -C structs
168+
- name: Test large_array_of_struct_nondet_index (cvc5)
169+
shell: bash
170+
run: |
171+
cd regression/cbmc-incr-smt2
172+
time perl ../test.pl -e -p -c "../../../build/bin/Release/cbmc --incremental-smt2-solver 'cvc5 --lang smt2 --incremental'" -C structs

‎.github/workflows/performance.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ on:
44
push:
55
branches: [ develop ]
66
pull_request:
7-
branches: [ develop ]
7+
branches: [ disabled-for-investigation ]
88

99
jobs:
1010
perf-benchcomp:

‎.github/workflows/pull-request-check-rust-api.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ on:
33
push:
44
branches: [ develop ]
55
pull_request:
6-
branches: [ develop ]
6+
branches: [ disabled-for-investigation ]
77
env:
88
default_build_dir: "build/"
99
default_solver: "minisat2"

‎.github/workflows/pull-request-checks.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ on:
33
push:
44
branches: [ develop ]
55
pull_request:
6-
branches: [ develop ]
6+
branches: [ disabled-for-investigation ]
77
env:
88
cvc5-version: "1.2.1"
99
linux-vcpus: 4

0 commit comments

Comments
 (0)