Add non-working symbolic locks to symbolic-thread-array-alive-counter…

… example from smtprc

tests/regression/03-practical/49-symbolic-thread-alive-counter.c → tests/regression/03-practical/49-symbolic-thread-array-alive-counter.c

@@ -1,7 +1,10 @@
+// PARAM: --set ana.activated[+] symb_locks
 // Per-thread array index passed via argument.
-// Thread pool joining via threads alive counter decremented in cleaner thread.
+// Thread pool joining via threads alive counter decremented based on thread array values.
 // Extracted from smtprc.
-// TODO: race correctly found here, but not in smtprc.
+// TODO: symb_locks doesn't work for datas and datas_mutex here
+#include <stdlib.h>
+#include <stdbool.h>
 #include <pthread.h>
 #include <goblint.h>
 extern int __VERIFIER_nondet_int();
@@ -11,35 +14,44 @@ int threads_alive = 0;
 pthread_mutex_t threads_alive_mutex = PTHREAD_MUTEX_INITIALIZER;
 
 pthread_t *tids;
-int *datas;
+bool *datas;
+pthread_mutex_t *datas_mutex;
 
 void *thread(void *arg) {
   int i = arg;
-  datas[i] = 1; // RACE!
+  pthread_mutex_lock(&datas_mutex[i]);
+  datas[i] = true; // NORACE
+  pthread_mutex_unlock(&datas_mutex[i]);
   return NULL;
 }
 
 void *cleaner(void *arg) {
   while (1) {
     for (int i = 0; i < threads_total; i++) {
-      if (datas[i]) { // RACE!
+      pthread_mutex_lock(&datas_mutex[i]);
+      if (datas[i]) { // NORACE
         pthread_join(tids[i], NULL); // NORACE
         pthread_mutex_lock(&threads_alive_mutex);
         threads_alive--; // NORACE
         pthread_mutex_unlock(&threads_alive_mutex);
-        datas[i] = 0; // RACE!
+        datas[i] = false; // NORACE
       }
+      pthread_mutex_unlock(&datas_mutex[i]);
     }
   }
   return NULL;
 }
 
 int main() {
   threads_total = __VERIFIER_nondet_int();
-  __goblint_assume(threads_total >= 0);
+  __goblint_assume(threads_total >= 1);
 
   tids = malloc(threads_total * sizeof(pthread_t));
-  datas = calloc(threads_total, sizeof(int));
+  datas = calloc(threads_total, sizeof(bool));
+  datas_mutex = malloc(threads_total * sizeof(pthread_mutex_t));
+
+  for (int i = 0; i < threads_total; i++)
+    pthread_mutex_init(&datas_mutex[i], NULL);
 
   // create threads
   pthread_t cleaner_tid;