From aab8b1cebbf89f77e72bfd73aede23a2dcbc9b9d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 25 Nov 2018 08:06:43 +0000 Subject: [PATCH 1/2] C library: model pthread_key_create, pthread_{get,set}specific This is used by pthread-divine/tls_basic_true-unreach-call in SV-COMP. --- .../constant_propagation_01/test.desc | 4 +- .../constant_propagation_02/test.desc | 4 +- .../constant_propagation_03/test.desc | 4 +- .../constant_propagation_04/test.desc | 4 +- .../constant_propagation_07/test.desc | 4 +- .../constant_propagation_12/test.desc | 4 +- src/ansi-c/ansi_c_internal_additions.cpp | 6 + src/ansi-c/library/pthread_lib.c | 136 ++++++++++++++++-- src/cpp/cpp_internal_additions.cpp | 10 ++ 9 files changed, 153 insertions(+), 23 deletions(-) diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc index e219da8cbc2..f7de54ad46b 100644 --- a/regression/goto-analyzer/constant_propagation_01/test.desc +++ b/regression/goto-analyzer/constant_propagation_01/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc index 8de026212bf..47aea19e28b 100644 --- a/regression/goto-analyzer/constant_propagation_02/test.desc +++ b/regression/goto-analyzer/constant_propagation_02/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc index 8de026212bf..47aea19e28b 100644 --- a/regression/goto-analyzer/constant_propagation_03/test.desc +++ b/regression/goto-analyzer/constant_propagation_03/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc index 8de026212bf..47aea19e28b 100644 --- a/regression/goto-analyzer/constant_propagation_04/test.desc +++ b/regression/goto-analyzer/constant_propagation_04/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc index 834532f9fa3..a791723bfd2 100644 --- a/regression/goto-analyzer/constant_propagation_07/test.desc +++ b/regression/goto-analyzer/constant_propagation_07/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 3, assigns: 11, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 12, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc index 60a7a7e0891..c605898b19d 100644 --- a/regression/goto-analyzer/constant_propagation_12/test.desc +++ b/regression/goto-analyzer/constant_propagation_12/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$ -- ^warning: ignoring diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 9c8de954b65..99102773d75 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -136,6 +136,12 @@ void ansi_c_internal_additions(std::string &code) CPROVER_PREFIX "bool " CPROVER_PREFIX "threads_exited[" CPROVER_PREFIX "constant_infinity_uint];\n" "unsigned long " CPROVER_PREFIX "next_thread_id=0;\n" + CPROVER_PREFIX "thread_local const void* " CPROVER_PREFIX "thread_keys[" + CPROVER_PREFIX "constant_infinity_uint];\n" + CPROVER_PREFIX "thread_local void (*" CPROVER_PREFIX "thread_key_dtors[" + CPROVER_PREFIX "constant_infinity_uint])(void *);\n" + CPROVER_PREFIX "thread_local unsigned long " + CPROVER_PREFIX "next_thread_key = 0;\n" "extern unsigned char " CPROVER_PREFIX "memory[" CPROVER_PREFIX "constant_infinity_uint];\n" diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c index 5a90eb9b9c9..637c42eb9ea 100644 --- a/src/ansi-c/library/pthread_lib.c +++ b/src/ansi-c/library/pthread_lib.c @@ -293,10 +293,21 @@ inline int pthread_mutex_destroy(pthread_mutex_t *mutex) extern __CPROVER_bool __CPROVER_threads_exited[]; extern __CPROVER_thread_local unsigned long __CPROVER_thread_id; +extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; +extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *); +extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key; + inline void pthread_exit(void *value_ptr) { __CPROVER_HIDE:; if(value_ptr!=0) (void)*(char*)value_ptr; + for(unsigned long i = 0; i < __CPROVER_next_thread_key; ++i) + { + const void *key = __CPROVER_thread_keys[i]; + __CPROVER_thread_keys[i] = 0; + if(__CPROVER_thread_key_dtors[i] && key) + __CPROVER_thread_key_dtors[i](key); + } __CPROVER_threads_exited[__CPROVER_thread_id]=1; __CPROVER_assume(0); } @@ -524,6 +535,47 @@ extern __CPROVER_bool __CPROVER_threads_exited[]; extern __CPROVER_thread_local unsigned long __CPROVER_thread_id; extern unsigned long __CPROVER_next_thread_id; +extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; +extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *); +extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key; + +inline void __spawned_thread( + unsigned long this_thread_id, + void (**thread_key_dtors)(void *), + unsigned long next_thread_key, + void *(*start_routine)(void *), + void *arg) +{ +__CPROVER_HIDE:; + __CPROVER_thread_id = this_thread_id; + __CPROVER_next_thread_key = next_thread_key; + for(unsigned long i = 0; i < __CPROVER_next_thread_key; ++i) + __CPROVER_thread_key_dtors[i] = thread_key_dtors[i]; +#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS + // Clear all locked mutexes; locking must happen in same thread. + __CPROVER_clear_must(0, "mutex-locked"); + __CPROVER_clear_may(0, "mutex-locked"); +#endif + start_routine(arg); + __CPROVER_fence( + "WWfence", + "RRfence", + "RWfence", + "WRfence", + "WWcumul", + "RRcumul", + "RWcumul", + "WRcumul"); + for(unsigned long i = 0; i < __CPROVER_next_thread_key; ++i) + { + const void *key = __CPROVER_thread_keys[i]; + __CPROVER_thread_keys[i] = 0; + if(__CPROVER_thread_key_dtors[i] && key) + __CPROVER_thread_key_dtors[i](key); + } + __CPROVER_threads_exited[this_thread_id] = 1; +} + inline int pthread_create( pthread_t *thread, // must not be null const pthread_attr_t *attr, // may be null @@ -545,19 +597,14 @@ inline int pthread_create( if(attr) (void)*attr; + unsigned long next_thread_key = __CPROVER_next_thread_key; + void (**thread_key_dtors)(void *) = __CPROVER_thread_key_dtors; + __CPROVER_ASYNC_1: - __CPROVER_thread_id=this_thread_id, - #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS - // Clear all locked mutexes; locking must happen in same thread. - __CPROVER_clear_must(0, "mutex-locked"), - __CPROVER_clear_may(0, "mutex-locked"), - #endif - start_routine(arg), - __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence", - "WWcumul", "RRcumul", "RWcumul", "WRcumul"), - __CPROVER_threads_exited[this_thread_id]=1; + __spawned_thread( + this_thread_id, thread_key_dtors, next_thread_key, start_routine, arg); - return 0; + return 0; } /* FUNCTION: pthread_cond_init */ @@ -832,3 +879,70 @@ inline int pthread_barrier_wait(pthread_barrier_t *barrier) return result; } #endif + +/* FUNCTION: pthread_key_create */ + +#ifndef __CPROVER_PTHREAD_H_INCLUDED +#include +#define __CPROVER_PTHREAD_H_INCLUDED +#endif + +extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; +extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *); +extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key; + +inline int pthread_key_create(pthread_key_t *key, void (*destructor)(void *)) +{ +__CPROVER_HIDE:; + __CPROVER_thread_keys[__CPROVER_next_thread_key] = 0; + __CPROVER_thread_key_dtors[__CPROVER_next_thread_key] = destructor; + *key = __CPROVER_next_thread_key++; + return 0; +} + +/* FUNCTION: pthread_key_delete */ + +#ifndef __CPROVER_PTHREAD_H_INCLUDED +#include +#define __CPROVER_PTHREAD_H_INCLUDED +#endif + +extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; + +inline int pthread_key_delete(pthread_key_t key) +{ +__CPROVER_HIDE:; + __CPROVER_thread_keys[key] = 0; + return 0; +} + +/* FUNCTION: pthread_getspecific */ + +#ifndef __CPROVER_PTHREAD_H_INCLUDED +#include +#define __CPROVER_PTHREAD_H_INCLUDED +#endif + +extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; + +inline void *pthread_getspecific(pthread_key_t key) +{ +__CPROVER_HIDE:; + return (void *)__CPROVER_thread_keys[key]; +} + +/* FUNCTION: pthread_setspecific */ + +#ifndef __CPROVER_PTHREAD_H_INCLUDED +#include +#define __CPROVER_PTHREAD_H_INCLUDED +#endif + +extern __CPROVER_thread_local const void *__CPROVER_thread_keys[]; + +inline int pthread_setspecific(pthread_key_t key, const void *value) +{ +__CPROVER_HIDE:; + __CPROVER_thread_keys[key] = value; + return 0; +} diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index 3a11eb1be04..b1a376f455d 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -72,6 +72,16 @@ void cpp_internal_additions(std::ostream &out) << CPROVER_PREFIX "threads_exited[__CPROVER::constant_infinity_uint];" << '\n'; out << "unsigned long " CPROVER_PREFIX "next_thread_id = 0;" << '\n'; + // TODO: thread_local is still broken + out << "void* " + << CPROVER_PREFIX "thread_keys[__CPROVER::constant_infinity_uint];" + << '\n'; + // TODO: thread_local is still broken + out << "void (*" + << CPROVER_PREFIX "thread_key_dtors[__CPROVER::constant_infinity_uint])" + << "(void *);" << '\n'; + // TODO: thread_local is still broken + out << "unsigned long " CPROVER_PREFIX "next_thread_key = 0;" << '\n'; out << "extern unsigned char " << CPROVER_PREFIX "memory[__CPROVER::constant_infinity_uint];" << '\n'; From f9fee65f9315c7c3cd0e9701efa3c0f5a2b5a0f4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 27 Nov 2018 06:20:37 +0000 Subject: [PATCH 2/2] Disable support for pthread_keyt destructors They are too expensive due to extensive shared-variable use. --- src/ansi-c/library/pthread_lib.c | 36 +++++++++++++++++++++++++++++++- 1 file changed, 35 insertions(+), 1 deletion(-) diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c index 637c42eb9ea..b792ba6df0f 100644 --- a/src/ansi-c/library/pthread_lib.c +++ b/src/ansi-c/library/pthread_lib.c @@ -301,6 +301,9 @@ inline void pthread_exit(void *value_ptr) { __CPROVER_HIDE:; if(value_ptr!=0) (void)*(char*)value_ptr; +#if 0 + // Destructor support is disabled as it is too expensive due to its extensive + // use of shared variables. for(unsigned long i = 0; i < __CPROVER_next_thread_key; ++i) { const void *key = __CPROVER_thread_keys[i]; @@ -308,6 +311,7 @@ inline void pthread_exit(void *value_ptr) if(__CPROVER_thread_key_dtors[i] && key) __CPROVER_thread_key_dtors[i](key); } +#endif __CPROVER_threads_exited[__CPROVER_thread_id]=1; __CPROVER_assume(0); } @@ -541,7 +545,11 @@ extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key; inline void __spawned_thread( unsigned long this_thread_id, +#if 0 + // Destructor support is disabled as it is too expensive due to its extensive + // use of shared variables. void (**thread_key_dtors)(void *), +#endif unsigned long next_thread_key, void *(*start_routine)(void *), void *arg) @@ -549,8 +557,12 @@ inline void __spawned_thread( __CPROVER_HIDE:; __CPROVER_thread_id = this_thread_id; __CPROVER_next_thread_key = next_thread_key; +#if 0 + // Destructor support is disabled as it is too expensive due to its extensive + // use of shared variables. for(unsigned long i = 0; i < __CPROVER_next_thread_key; ++i) __CPROVER_thread_key_dtors[i] = thread_key_dtors[i]; +#endif #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS // Clear all locked mutexes; locking must happen in same thread. __CPROVER_clear_must(0, "mutex-locked"); @@ -566,6 +578,9 @@ __CPROVER_HIDE:; "RRcumul", "RWcumul", "WRcumul"); +#if 0 + // Destructor support is disabled as it is too expensive due to its extensive + // use of shared variables. for(unsigned long i = 0; i < __CPROVER_next_thread_key; ++i) { const void *key = __CPROVER_thread_keys[i]; @@ -573,6 +588,7 @@ __CPROVER_HIDE:; if(__CPROVER_thread_key_dtors[i] && key) __CPROVER_thread_key_dtors[i](key); } +#endif __CPROVER_threads_exited[this_thread_id] = 1; } @@ -598,11 +614,23 @@ inline int pthread_create( if(attr) (void)*attr; unsigned long next_thread_key = __CPROVER_next_thread_key; +#if 0 + // Destructor support is disabled as it is too expensive due to its extensive + // use of shared variables. void (**thread_key_dtors)(void *) = __CPROVER_thread_key_dtors; +#endif __CPROVER_ASYNC_1: __spawned_thread( - this_thread_id, thread_key_dtors, next_thread_key, start_routine, arg); + this_thread_id, +#if 0 + // Destructor support is disabled as it is too expensive due to its + // extensive use of shared variables. + thread_key_dtors, +#endif + next_thread_key, + start_routine, + arg); return 0; } @@ -895,7 +923,13 @@ inline int pthread_key_create(pthread_key_t *key, void (*destructor)(void *)) { __CPROVER_HIDE:; __CPROVER_thread_keys[__CPROVER_next_thread_key] = 0; +#if 0 + // Destructor support is disabled as it is too expensive due to its extensive + // use of shared variables. __CPROVER_thread_key_dtors[__CPROVER_next_thread_key] = destructor; +#else + __CPROVER_precondition(destructor == 0, "destructors are not yet supported"); +#endif *key = __CPROVER_next_thread_key++; return 0; }