First approximation of pthread_setspecific by escaping things reachable from the argument and invalidating all globals

src/analyses/libraryFunctions.ml

@@ -75,6 +75,9 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_cond_broadcast", special [__ "cond" []] @@ fun cond -> Broadcast cond);
     ("pthread_cond_wait", special [__ "cond" []; __ "mutex" []] @@ fun cond mutex -> Wait {cond; mutex});
     ("pthread_cond_timedwait", special [__ "cond" []; __ "mutex" []; __ "abstime" [r]] @@ fun cond mutex abstime -> TimedWait {cond; mutex; abstime});
+    ("pthread_setspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []; drop "value" [w_deep]]);
+    ("pthread_getspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []]);
+    ("pthread_key_delete", unknown [drop "key" [f]]);
   ]
 
 (** GCC builtin functions.

src/analyses/threadEscape.ml

@@ -90,8 +90,17 @@ struct
   let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t =
     au
 
-  let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
-    ctx.local
+  let special ctx (lval: lval option) (f:varinfo) (args:exp list) : D.t =
+    let desc = LibraryFunctions.find f in
+    match desc.special args, f.vname, args with
+    | _, "pthread_setspecific" , [key; pt_value] ->
+      let escaped = reachable (Analyses.ask_of_ctx ctx) pt_value in
+      let escaped = D.filter (fun v -> not v.vglob) escaped in
+      if not (D.is_empty escaped) then (* avoid emitting unnecessary event *)
+        ctx.emit (Events.Escape escaped);
+      let extra = D.fold (fun v acc -> D.join acc (ctx.global v)) escaped (D.empty ()) in (* TODO: must transitively join escapes of every ctx.global v as well? *)
+      D.join ctx.local (D.join escaped extra)
+    | _ -> ctx.local
 
   let startstate v = D.bot ()
   let exitstate  v = D.bot ()

tests/regression/41-stdlib/04-pthread-specific.c

@@ -0,0 +1,29 @@
+#include<pthread.h>
+#include<goblint.h>
+
+pthread_key_t key;
+
+void *t_fun(void *arg) {
+  int var = 8;
+  pthread_setspecific(key,&var);
+  int* ptr = (int*)pthread_getspecific(key);
+  *ptr = 12;
+  var = 8;
+  *ptr = 12;
+  __goblint_check(var == 8); //UNKNOWN!
+}
+
+int main (void)
+{
+    pthread_t tid1, tid2;
+
+    pthread_key_create (&key, NULL);
+    pthread_create (&tid1, NULL, (void *)t_fun, NULL);
+    pthread_create (&tid2, NULL, (void *)t_fun, NULL);
+    pthread_join (tid1, NULL);
+    pthread_join (tid2, NULL);
+
+    pthread_key_delete(key);
+
+    return 0;
+}