From 28644cad78648d228b780c151b19bdc0bac2b6a9 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 21 Sep 2023 10:41:24 +0300
Subject: [PATCH] Add non-working symbolic locks to
 symbolic-thread-array-alive-counter example from smtprc

---
 ... 49-symbolic-thread-array-alive-counter.c} | 28 +++++++++++++------
 1 file changed, 20 insertions(+), 8 deletions(-)
 rename tests/regression/03-practical/{49-symbolic-thread-alive-counter.c => 49-symbolic-thread-array-alive-counter.c} (65%)

diff --git a/tests/regression/03-practical/49-symbolic-thread-alive-counter.c b/tests/regression/03-practical/49-symbolic-thread-array-alive-counter.c
similarity index 65%
rename from tests/regression/03-practical/49-symbolic-thread-alive-counter.c
rename to tests/regression/03-practical/49-symbolic-thread-array-alive-counter.c
index 6311a5ca4d..79cb823ac4 100644
--- a/tests/regression/03-practical/49-symbolic-thread-alive-counter.c
+++ b/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,24 +14,29 @@ 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;
@@ -36,10 +44,14 @@ void *cleaner(void *arg) {
 
 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;