Skip to content

Commit

Permalink
Work around bitwuzla/bitwuzla#96 on Ubuntu 20.04
Browse files Browse the repository at this point in the history
Sadly, Ubuntu 20.04's version of `glibc` is susceptible to
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=58909. We work around the issue
by applying a workaround taken from
https://bbs.archlinux.org/viewtopic.php?pid=2022393#p2022393.
  • Loading branch information
RyanGlScott committed Dec 18, 2023
1 parent 38ac8f1 commit 3193856
Show file tree
Hide file tree
Showing 3 changed files with 42 additions and 0 deletions.
7 changes: 7 additions & 0 deletions .github/ci.sh
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,13 @@ build_abc() {

build_bitwuzla() {
pushd repos/bitwuzla
if [ "$GITHUB_MATRIX_OS" == 'ubuntu-20.04' ] ; then
# Ubuntu 20.04 uses an older version of glibc that is susceptible to
# https://gcc.gnu.org/bugzilla/show_bug.cgi?id=58909, so we must apply a
# crude workaround for it. Thankfully, this is not required for the version
# of glibc that ships with Ubuntu 22.04.
patch -p1 -i $PATCHES/bitwuzla-T58909-workaround.patch
fi
./configure.py
cd build
ninja -j4
Expand Down
4 changes: 4 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -83,11 +83,15 @@ jobs:
- name: build_solver (non-Windows)
shell: bash
run: .github/ci.sh build_${{ matrix.solver }}
env:
GITHUB_MATRIX_OS: ${{ matrix.os }}
if: runner.os != 'Windows'

- name: build_solver (Windows)
shell: msys2 {0}
run: .github/ci.sh build_${{ matrix.solver }}
env:
GITHUB_MATRIX_OS: ${{ matrix.os }}
if: runner.os == 'Windows'

- uses: actions/upload-artifact@v2
Expand Down
31 changes: 31 additions & 0 deletions patches/bitwuzla-T58909-workaround.patch
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp
index 45238be4..f1ee25cb 100644
--- a/src/main/time_limit.cpp
+++ b/src/main/time_limit.cpp
@@ -6,6 +6,7 @@
#include <cstdlib>
#include <iostream>
#include <thread>
+#include <pthread.h>

namespace bzla::main {

@@ -15,6 +16,18 @@ std::condition_variable cv;
std::mutex cv_m;
bool time_limit_set = false;

+// Work around https://gcc.gnu.org/bugzilla/show_bug.cgi?id=58909
+// on old versions of glibc
+void pthread_cond_bug() {
+ pthread_cond_signal((pthread_cond_t *) nullptr);
+ pthread_cond_init((pthread_cond_t *) nullptr,
+ (const pthread_condattr_t *) nullptr);
+ pthread_cond_destroy((pthread_cond_t *) nullptr);
+ pthread_cond_timedwait((pthread_cond_t *) nullptr, (pthread_mutex_t *)
+ nullptr, (const struct timespec *) nullptr);
+ pthread_cond_wait((pthread_cond_t *) nullptr, (pthread_mutex_t *) nullptr);
+}
+
void
timeout_reached()
{

0 comments on commit 3193856

Please sign in to comment.