C library: model pthread_key_create, pthread_{get,set}specific

tautschnig · tautschnig · commit d62a514264f7 · 2019-02-25T00:33:36.000Z
This is used by pthread-divine/tls_basic_true-unreach-call in SV-COMP.
diff --git a/regression/cbmc/function-return-no-body1/test.desc b/regression/cbmc/function-return-no-body1/test.desc
@@ -5,7 +5,7 @@ activate-multi-line-match
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
-<function_call hidden="false" step_nr="18" thread="0">\n\s*<function display_name="no_body" identifier="no_body">
-<function_return hidden="false" step_nr="19" thread="0">\n\s*<function display_name="no_body" identifier="no_body">
+<function_call hidden="false" step_nr="21" thread="0">\n\s*<function display_name="no_body" identifier="no_body">
+<function_return hidden="false" step_nr="22" thread="0">\n\s*<function display_name="no_body" identifier="no_body">
 --
 ^warning: ignoring
diff --git 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: 12, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, 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_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: 11, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, 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
@@ -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: 11, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, 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
@@ -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: 11, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, 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
@@ -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: 9, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 12, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 11, 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
@@ -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: 10, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 12, 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
@@ -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
@@ -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 <pthread.h>
+#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 <pthread.h>
+#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 <pthread.h>
+#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 <pthread.h>
+#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
@@ -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';
 
