Disable support for pthread_keyt destructors

They are too expensive due to extensive shared-variable use.

Author: tautschnig

src/ansi-c/library/pthread_lib.c

@@ -301,13 +301,17 @@ 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);
 }
@@ -541,16 +545,24 @@ 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");
@@ -566,13 +578,17 @@ __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];
     __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;
 }
 
@@ -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;
 }