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..b792ba6df0f 100644 --- a/src/ansi-c/library/pthread_lib.c +++ b/src/ansi-c/library/pthread_lib.c @@ -293,10 +293,25 @@ 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; +#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]; + __CPROVER_thread_keys[i] = 0; + if(__CPROVER_thread_key_dtors[i] && key) + __CPROVER_thread_key_dtors[i](key); + } +#endif __CPROVER_threads_exited[__CPROVER_thread_id]=1; __CPROVER_assume(0); } @@ -524,6 +539,59 @@ 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, +#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) +{ +__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"); + __CPROVER_clear_may(0, "mutex-locked"); +#endif + start_routine(arg); + __CPROVER_fence( + "WWfence", + "RRfence", + "RWfence", + "WRfence", + "WWcumul", + "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]; + __CPROVER_thread_keys[i] = 0; + if(__CPROVER_thread_key_dtors[i] && key) + __CPROVER_thread_key_dtors[i](key); + } +#endif + __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 +613,26 @@ inline int pthread_create( if(attr) (void)*attr; - __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; + 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 - return 0; + __CPROVER_ASYNC_1: + __spawned_thread( + 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; } /* FUNCTION: pthread_cond_init */ @@ -832,3 +907,76 @@ 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; +#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; +} + +/* 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';