From b994da4cf200025ae95239983de8b97db13d9858 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 25 Feb 2019 17:45:10 +0000 Subject: [PATCH 1/2] pthread tests should not be run on Windows These will never work on Windows, which doesn't have POSIX threads. --- regression/cbmc-library/CMakeLists.txt | 10 ++++++++++ regression/cbmc-library/Makefile | 11 +++++++++-- .../cbmc-library/pthread_barrier_destroy-01/test.desc | 2 +- .../cbmc-library/pthread_barrier_init-01/test.desc | 2 +- .../cbmc-library/pthread_barrier_wait-01/test.desc | 2 +- regression/cbmc-library/pthread_cancel-01/test.desc | 2 +- .../cbmc-library/pthread_cond_broadcast-01/test.desc | 2 +- .../cbmc-library/pthread_cond_init-01/test.desc | 2 +- .../cbmc-library/pthread_cond_signal-01/test.desc | 2 +- .../cbmc-library/pthread_cond_wait-01/test.desc | 2 +- regression/cbmc-library/pthread_create-01/test.desc | 2 +- regression/cbmc-library/pthread_exit-01/test.desc | 2 +- regression/cbmc-library/pthread_join-01/test.desc | 2 +- .../cbmc-library/pthread_mutex_destroy-01/test.desc | 2 +- .../cbmc-library/pthread_mutex_init-01/test.desc | 2 +- .../cbmc-library/pthread_mutex_lock-01/test.desc | 2 +- .../cbmc-library/pthread_mutex_trylock-01/test.desc | 2 +- .../cbmc-library/pthread_mutex_unlock-01/test.desc | 2 +- .../pthread_mutexattr_settype-01/test.desc | 2 +- .../cbmc-library/pthread_rwlock_destroy-01/test.desc | 2 +- .../cbmc-library/pthread_rwlock_init-01/test.desc | 2 +- .../cbmc-library/pthread_rwlock_rdlock-01/test.desc | 2 +- .../pthread_rwlock_tryrdlock-01/test.desc | 2 +- .../pthread_rwlock_trywrlock-01/test.desc | 2 +- .../cbmc-library/pthread_rwlock_unlock-01/test.desc | 2 +- .../cbmc-library/pthread_rwlock_wrlock-01/test.desc | 2 +- .../cbmc-library/pthread_spin_lock-01/test.desc | 2 +- .../cbmc-library/pthread_spin_trylock-01/test.desc | 2 +- .../cbmc-library/pthread_spin_unlock-01/test.desc | 2 +- 29 files changed, 46 insertions(+), 29 deletions(-) diff --git a/regression/cbmc-library/CMakeLists.txt b/regression/cbmc-library/CMakeLists.txt index 93d5ee716c2..a0480f01be2 100644 --- a/regression/cbmc-library/CMakeLists.txt +++ b/regression/cbmc-library/CMakeLists.txt @@ -1,3 +1,13 @@ +if(NOT WIN32) add_test_pl_tests( "$" ) +else() +add_test_pl_tests( + "$" + "cbmc-library" + "$" + "-C;-X;pthread" + "CORE" +) +endif() diff --git a/regression/cbmc-library/Makefile b/regression/cbmc-library/Makefile index 1b66f1b4124..7484e76464c 100644 --- a/regression/cbmc-library/Makefile +++ b/regression/cbmc-library/Makefile @@ -1,10 +1,17 @@ default: tests.log +include ../../src/config.inc +include ../../src/common + +ifeq ($(BUILD_ENV_),MSVC) + no_pthread = -X pthread +endif + test: - @../test.pl -e -p -c ../../../src/cbmc/cbmc + @../test.pl -e -p -c ../../../src/cbmc/cbmc $(no_pthread) tests.log: ../test.pl - @../test.pl -e -p -c ../../../src/cbmc/cbmc + @../test.pl -e -p -c ../../../src/cbmc/cbmc $(no_pthread) show: @for dir in *; do \ diff --git a/regression/cbmc-library/pthread_barrier_destroy-01/test.desc b/regression/cbmc-library/pthread_barrier_destroy-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_barrier_destroy-01/test.desc +++ b/regression/cbmc-library/pthread_barrier_destroy-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_barrier_init-01/test.desc b/regression/cbmc-library/pthread_barrier_init-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_barrier_init-01/test.desc +++ b/regression/cbmc-library/pthread_barrier_init-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_barrier_wait-01/test.desc b/regression/cbmc-library/pthread_barrier_wait-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_barrier_wait-01/test.desc +++ b/regression/cbmc-library/pthread_barrier_wait-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_cancel-01/test.desc b/regression/cbmc-library/pthread_cancel-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_cancel-01/test.desc +++ b/regression/cbmc-library/pthread_cancel-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_cond_broadcast-01/test.desc b/regression/cbmc-library/pthread_cond_broadcast-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_cond_broadcast-01/test.desc +++ b/regression/cbmc-library/pthread_cond_broadcast-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_cond_init-01/test.desc b/regression/cbmc-library/pthread_cond_init-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_cond_init-01/test.desc +++ b/regression/cbmc-library/pthread_cond_init-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_cond_signal-01/test.desc b/regression/cbmc-library/pthread_cond_signal-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_cond_signal-01/test.desc +++ b/regression/cbmc-library/pthread_cond_signal-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_cond_wait-01/test.desc b/regression/cbmc-library/pthread_cond_wait-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_cond_wait-01/test.desc +++ b/regression/cbmc-library/pthread_cond_wait-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_create-01/test.desc b/regression/cbmc-library/pthread_create-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_create-01/test.desc +++ b/regression/cbmc-library/pthread_create-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_exit-01/test.desc b/regression/cbmc-library/pthread_exit-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_exit-01/test.desc +++ b/regression/cbmc-library/pthread_exit-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_join-01/test.desc b/regression/cbmc-library/pthread_join-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_join-01/test.desc +++ b/regression/cbmc-library/pthread_join-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_mutex_destroy-01/test.desc b/regression/cbmc-library/pthread_mutex_destroy-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_mutex_destroy-01/test.desc +++ b/regression/cbmc-library/pthread_mutex_destroy-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_mutex_init-01/test.desc b/regression/cbmc-library/pthread_mutex_init-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_mutex_init-01/test.desc +++ b/regression/cbmc-library/pthread_mutex_init-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_mutex_lock-01/test.desc b/regression/cbmc-library/pthread_mutex_lock-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_mutex_lock-01/test.desc +++ b/regression/cbmc-library/pthread_mutex_lock-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_mutex_trylock-01/test.desc b/regression/cbmc-library/pthread_mutex_trylock-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_mutex_trylock-01/test.desc +++ b/regression/cbmc-library/pthread_mutex_trylock-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_mutex_unlock-01/test.desc b/regression/cbmc-library/pthread_mutex_unlock-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_mutex_unlock-01/test.desc +++ b/regression/cbmc-library/pthread_mutex_unlock-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_mutexattr_settype-01/test.desc b/regression/cbmc-library/pthread_mutexattr_settype-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_mutexattr_settype-01/test.desc +++ b/regression/cbmc-library/pthread_mutexattr_settype-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_rwlock_destroy-01/test.desc b/regression/cbmc-library/pthread_rwlock_destroy-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_rwlock_destroy-01/test.desc +++ b/regression/cbmc-library/pthread_rwlock_destroy-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_rwlock_init-01/test.desc b/regression/cbmc-library/pthread_rwlock_init-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_rwlock_init-01/test.desc +++ b/regression/cbmc-library/pthread_rwlock_init-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_rwlock_rdlock-01/test.desc b/regression/cbmc-library/pthread_rwlock_rdlock-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_rwlock_rdlock-01/test.desc +++ b/regression/cbmc-library/pthread_rwlock_rdlock-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_rwlock_tryrdlock-01/test.desc b/regression/cbmc-library/pthread_rwlock_tryrdlock-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_rwlock_tryrdlock-01/test.desc +++ b/regression/cbmc-library/pthread_rwlock_tryrdlock-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_rwlock_trywrlock-01/test.desc b/regression/cbmc-library/pthread_rwlock_trywrlock-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_rwlock_trywrlock-01/test.desc +++ b/regression/cbmc-library/pthread_rwlock_trywrlock-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_rwlock_unlock-01/test.desc b/regression/cbmc-library/pthread_rwlock_unlock-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_rwlock_unlock-01/test.desc +++ b/regression/cbmc-library/pthread_rwlock_unlock-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_rwlock_wrlock-01/test.desc b/regression/cbmc-library/pthread_rwlock_wrlock-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_rwlock_wrlock-01/test.desc +++ b/regression/cbmc-library/pthread_rwlock_wrlock-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_spin_lock-01/test.desc b/regression/cbmc-library/pthread_spin_lock-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_spin_lock-01/test.desc +++ b/regression/cbmc-library/pthread_spin_lock-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_spin_trylock-01/test.desc b/regression/cbmc-library/pthread_spin_trylock-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_spin_trylock-01/test.desc +++ b/regression/cbmc-library/pthread_spin_trylock-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/regression/cbmc-library/pthread_spin_unlock-01/test.desc b/regression/cbmc-library/pthread_spin_unlock-01/test.desc index 9542d988e8d..3cb4011c85b 100644 --- a/regression/cbmc-library/pthread_spin_unlock-01/test.desc +++ b/regression/cbmc-library/pthread_spin_unlock-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +KNOWNBUG pthread main.c --pointer-check --bounds-check ^EXIT=0$ From 4c6a9fcd30bf80cea2c01200a804c21c4f74ea4b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 26 Nov 2018 18:12:31 +0000 Subject: [PATCH 2/2] pthread_cond_wait may return spuriously The man page states: "In general, whenever a condition wait returns, the thread has to re-evaluate the predicate associated with the condition wait to determine whether it can safely proceed, should wait again, or should declare a timeout. A return from the wait does not imply that the associated predicate is either true or false." The regression test is based on pthread-divine/condvar_spurious_wakeup_false-unreach-call.c from SV-COMP. --- .../cbmc-library/pthread_cond_wait-01/main.c | 31 ++++++++++++++++--- .../pthread_cond_wait-01/test.desc | 9 +++--- src/ansi-c/library/pthread_lib.c | 4 +-- 3 files changed, 34 insertions(+), 10 deletions(-) diff --git a/regression/cbmc-library/pthread_cond_wait-01/main.c b/regression/cbmc-library/pthread_cond_wait-01/main.c index 38963cb967d..024df7dad26 100644 --- a/regression/cbmc-library/pthread_cond_wait-01/main.c +++ b/regression/cbmc-library/pthread_cond_wait-01/main.c @@ -1,9 +1,32 @@ #include -#include +#include + +pthread_mutex_t lock; +pthread_cond_t cond; + +// only accessed in critical section guarded by mutex, so there is no need to +// make this variable atomic or volatile +int x; + +void *thread(void *arg) +{ + (void)arg; + pthread_mutex_lock(&lock); + pthread_cond_wait(&cond, &lock); + // may fail: pthread_cond_wait can be waken up spuriously (see man + // pthread_cond_wait) + assert(x == 1); + pthread_mutex_unlock(&lock); + return NULL; +} int main() { - pthread_cond_wait(); - assert(0); - return 0; + pthread_t t; + pthread_mutex_init(&lock, 0); + pthread_cond_init(&cond, 0); + pthread_create(&t, NULL, thread, NULL); + x = 1; + pthread_cond_broadcast(&cond); + pthread_join(t, NULL); } diff --git a/regression/cbmc-library/pthread_cond_wait-01/test.desc b/regression/cbmc-library/pthread_cond_wait-01/test.desc index 3cb4011c85b..02dd330eb2c 100644 --- a/regression/cbmc-library/pthread_cond_wait-01/test.desc +++ b/regression/cbmc-library/pthread_cond_wait-01/test.desc @@ -1,8 +1,9 @@ -KNOWNBUG pthread +CORE pthread main.c ---pointer-check --bounds-check -^EXIT=0$ +--bounds-check +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ +^\*\* 1 of 2 failed +^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c index a1d244c6db9..5a90eb9b9c9 100644 --- a/src/ansi-c/library/pthread_lib.c +++ b/src/ansi-c/library/pthread_lib.c @@ -636,8 +636,8 @@ inline int pthread_cond_wait( #endif __CPROVER_atomic_begin(); - __CPROVER_assume(*((unsigned *)cond)); - (*((unsigned *)cond))--; + if(*((unsigned *)cond)) + (*((unsigned *)cond))--; __CPROVER_atomic_end(); return 0; // we never fail