From 0709d82d1ad90a0882e22fd93e3cee8756061248 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 09:49:33 +0300
Subject: [PATCH 01/32] Add symb_locks test with irrelevant index access

---
 tests/regression/06-symbeq/37-funloop_index.c | 36 +++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 tests/regression/06-symbeq/37-funloop_index.c

diff --git a/tests/regression/06-symbeq/37-funloop_index.c b/tests/regression/06-symbeq/37-funloop_index.c
new file mode 100644
index 0000000000..831ad62769
--- /dev/null
+++ b/tests/regression/06-symbeq/37-funloop_index.c
@@ -0,0 +1,36 @@
+// PARAM: --disable ana.mutex.disjoint_types --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+// copy of 06/02 with additional index accesses
+#include<pthread.h>
+#include<stdio.h>
+
+struct cache_entry {
+  int refs;
+  pthread_mutex_t refs_mutex;
+} cache[10];
+
+void cache_entry_addref(struct cache_entry *entry) {
+  pthread_mutex_lock(&entry->refs_mutex);
+  entry->refs++; // NORACE
+  (*entry).refs++; // NORACE
+  entry[0].refs++; // NORACE
+  pthread_mutex_unlock(&entry->refs_mutex);
+}
+
+void *t_fun(void *arg) {
+  int i;
+  for(i=0; i<10; i++)
+    cache_entry_addref(&cache[i]); // NORACE
+  return NULL;
+}
+
+int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&cache[i].refs_mutex, NULL);
+
+  int i;
+  pthread_t t1;
+  pthread_create(&t1, NULL, t_fun, NULL);
+  for(i=0; i<10; i++)
+    cache_entry_addref(&cache[i]); // NORACE
+  return 0;
+}

From 30c1d7aedabe4deb1f60aba45c1d07f8f8b66f1a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 10:00:23 +0300
Subject: [PATCH 02/32] Add var_eq EqualSet tracing

---
 src/analyses/varEq.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index ce93e043dd..29ff7b2453 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -519,7 +519,8 @@ struct
       D.B.fold add es (Queries.ES.empty ())
 
   let rec eq_set_clos e s =
-    match e with
+    if M.tracing then M.traceli "var_eq" "eq_set_clos %a\n" d_plainexp e;
+    let r = match e with
     | SizeOf _
     | SizeOfE _
     | SizeOfStr _
@@ -541,6 +542,9 @@ struct
       Queries.ES.map (fun e -> CastE (t,e)) (eq_set_clos e s)
     | Question _ -> failwith "Logical operations should be compiled away by CIL."
     | _ -> failwith "Unmatched pattern."
+    in
+    if M.tracing then M.traceu "var_eq" "eq_set_clos %a = %a\n" d_plainexp e Queries.ES.pretty r;
+    r
 
 
   let query ctx (type a) (x: a Queries.t): a Queries.result =
@@ -550,6 +554,7 @@ struct
     | Queries.EqualSet e ->
       let r = eq_set_clos e ctx.local in
       (*          Messages.warn ~msg:("equset of "^(sprint 80 (d_exp () e))^" is "^(Queries.ES.short 80 r)) ();  *)
+      if M.tracing then M.tracel "var_eq" "equalset %a = %a\n" d_plainexp e Queries.ES.pretty r;
       r
     | _ -> Queries.Result.top x
 

From 11cc869352318dcc044bcf1a19b2b55e7d8dfb07 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 10:01:15 +0300
Subject: [PATCH 03/32] Quick fix var_eq eq_set_clos for IndexPI

---
 src/analyses/varEq.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 29ff7b2453..93c01addba 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -521,6 +521,8 @@ struct
   let rec eq_set_clos e s =
     if M.tracing then M.traceli "var_eq" "eq_set_clos %a\n" d_plainexp e;
     let r = match e with
+    | BinOp ((PlusPI | IndexPI), e1, e2, _) ->
+      eq_set_clos e1 s (* TODO: what about e2? add to some Index offset to all? *)
     | SizeOf _
     | SizeOfE _
     | SizeOfStr _

From dd432000a7f062ee8c93e1352f81fe0c1e109110 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 12:04:12 +0300
Subject: [PATCH 04/32] Add chrony Name2IPAddress extracted test for symb_locks

---
 .../06-symbeq/38-chrony-name2ipaddress.c      | 219 ++++++++++++++++++
 1 file changed, 219 insertions(+)
 create mode 100644 tests/regression/06-symbeq/38-chrony-name2ipaddress.c

diff --git a/tests/regression/06-symbeq/38-chrony-name2ipaddress.c b/tests/regression/06-symbeq/38-chrony-name2ipaddress.c
new file mode 100644
index 0000000000..6a4fec5ac9
--- /dev/null
+++ b/tests/regression/06-symbeq/38-chrony-name2ipaddress.c
@@ -0,0 +1,219 @@
+// PARAM: --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'mallocFresh'" --set ana.malloc.wrappers '["Malloc"]' --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals
+#include <stddef.h>
+#include <stdint.h>
+// #include <sys/types.h>
+// #include <sys/socket.h>
+#include <netdb.h>
+#include <pthread.h>
+
+void *
+Malloc(size_t size)
+{
+  void *r;
+
+  r = malloc(size);
+  // if (!r && size)
+  //   LOG_FATAL("Could not allocate memory");
+
+  return r;
+}
+
+typedef enum {
+  DNS_Success,
+  DNS_TryAgain,
+  DNS_Failure
+} DNS_Status;
+
+typedef struct {
+  union {
+    uint32_t in4;
+    uint8_t in6[16];
+    uint32_t id;
+  } addr;
+  uint16_t family;
+  uint16_t _pad;
+} IPAddr;
+
+#define DNS_MAX_ADDRESSES 16
+#define IPADDR_UNSPEC 0
+#define IPADDR_INET4 1
+#define IPADDR_INET6 2
+#define IPADDR_ID 3
+
+static int address_family = IPADDR_UNSPEC;
+
+int
+UTI_StringToIP(const char *addr, IPAddr *ip)
+{
+  struct in_addr in4;
+#ifdef FEAT_IPV6
+  struct in6_addr in6;
+#endif
+
+  if (inet_pton(AF_INET, addr, &in4) > 0) {
+    ip->family = IPADDR_INET4;
+    ip->_pad = 0;
+    ip->addr.in4 = ntohl(in4.s_addr);
+    return 1;
+  }
+
+#ifdef FEAT_IPV6
+  if (inet_pton(AF_INET6, addr, &in6) > 0) {
+    ip->family = IPADDR_INET6;
+    ip->_pad = 0;
+    memcpy(ip->addr.in6, in6.s6_addr, sizeof (ip->addr.in6));
+    return 1;
+  }
+#endif
+
+  return 0;
+}
+
+
+#define MIN(x, y) ((x) < (y) ? (x) : (y))
+
+DNS_Status
+DNS_Name2IPAddress(const char *name, IPAddr *ip_addrs, int max_addrs)
+{
+  struct addrinfo hints, *res, *ai;
+  int i, result;
+  IPAddr ip;
+
+  max_addrs = MIN(max_addrs, DNS_MAX_ADDRESSES);
+
+  for (i = 0; i < max_addrs; i++)
+    ip_addrs[i].family = IPADDR_UNSPEC;
+
+// #if 0
+  /* Avoid calling getaddrinfo() if the name is an IP address */
+  if (UTI_StringToIP(name, &ip)) {
+    if (address_family != IPADDR_UNSPEC && ip.family != address_family)
+      return DNS_Failure;
+    if (max_addrs >= 1)
+      ip_addrs[0] = ip;
+    return DNS_Success;
+  }
+
+  memset(&hints, 0, sizeof (hints));
+
+  switch (address_family) {
+    case IPADDR_INET4:
+      hints.ai_family = AF_INET;
+      break;
+#ifdef FEAT_IPV6
+    case IPADDR_INET6:
+      hints.ai_family = AF_INET6;
+      break;
+#endif
+    default:
+      hints.ai_family = AF_UNSPEC;
+  }
+  hints.ai_socktype = SOCK_DGRAM;
+
+  result = getaddrinfo(name, NULL, &hints, &res);
+
+  if (result) {
+#ifdef FORCE_DNSRETRY
+    return DNS_TryAgain;
+#else
+    return result == EAI_AGAIN ? DNS_TryAgain : DNS_Failure;
+#endif
+  }
+
+  for (ai = res, i = 0; i < max_addrs && ai != NULL; ai = ai->ai_next) {
+    switch (ai->ai_family) {
+      case AF_INET:
+        if (address_family != IPADDR_UNSPEC && address_family != IPADDR_INET4)
+          continue;
+        ip_addrs[i].family = IPADDR_INET4;
+        ip_addrs[i].addr.in4 = ntohl(((struct sockaddr_in *)ai->ai_addr)->sin_addr.s_addr);
+        i++;
+        break;
+#ifdef FEAT_IPV6
+      case AF_INET6:
+        if (address_family != IPADDR_UNSPEC && address_family != IPADDR_INET6)
+          continue;
+        /* Don't return an address that would lose a scope ID */
+        if (((struct sockaddr_in6 *)ai->ai_addr)->sin6_scope_id != 0)
+          continue;
+        ip_addrs[i].family = IPADDR_INET6;
+        memcpy(&ip_addrs[i].addr.in6, &((struct sockaddr_in6 *)ai->ai_addr)->sin6_addr.s6_addr,
+               sizeof (ip_addrs->addr.in6));
+        i++;
+        break;
+#endif
+    }
+  }
+
+  freeaddrinfo(res);
+// #endif
+
+  return !max_addrs || ip_addrs[0].family != IPADDR_UNSPEC ? DNS_Success : DNS_Failure;
+}
+
+struct DNS_Async_Instance {
+  const char *name;
+  DNS_Status status;
+  IPAddr addresses[DNS_MAX_ADDRESSES];
+  // DNS_NameResolveHandler handler;
+  // void *arg;
+  pthread_mutex_t mutex;
+
+  pthread_t thread;
+  // int pipe[2];
+};
+
+static pthread_mutex_t privops_lock = PTHREAD_MUTEX_INITIALIZER;
+
+/* ================================================== */
+
+static void *
+start_resolving(void *anything)
+{
+  struct DNS_Async_Instance *inst = (struct DNS_Async_Instance *)anything;
+
+  pthread_mutex_lock(&inst->mutex);
+  inst->status = DNS_Name2IPAddress(inst->name, inst->addresses, DNS_MAX_ADDRESSES);
+  pthread_mutex_unlock(&inst->mutex);
+
+  /* Notify the main thread that the result is ready */
+  // if (write(inst->pipe[1], "", 1) < 0)
+  //   ;
+
+  return NULL;
+}
+
+
+#define MallocNew(T) ((T *) Malloc(sizeof(T)))
+
+void
+DNS_Name2IPAddressAsync(const char *name)
+{
+  struct DNS_Async_Instance *inst;
+
+  inst = MallocNew(struct DNS_Async_Instance);
+  inst->name = name;
+  // inst->handler = handler;
+  // inst->arg = anything;
+  inst->status = DNS_Failure;
+  pthread_mutex_init(&inst->mutex, NULL);
+
+  // if (pipe(inst->pipe)) {
+  //   LOG_FATAL("pipe() failed");
+  // }
+
+  // UTI_FdSetCloexec(inst->pipe[0]);
+  // UTI_FdSetCloexec(inst->pipe[1]);
+
+  if (pthread_create(&inst->thread, NULL, start_resolving, inst)) {
+    // LOG_FATAL("pthread_create() failed");
+  }
+
+  // SCH_AddFileHandler(inst->pipe[0], SCH_FILE_INPUT, end_resolving, inst);
+}
+
+int main() {
+  DNS_Name2IPAddressAsync("foo");
+  DNS_Name2IPAddressAsync("bar");
+  return 0;
+}

From 1ba9590b2f0678255f644acfa368cd15dcf0c990 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 12:05:55 +0300
Subject: [PATCH 05/32] Add symb_locks tracing

---
 src/analyses/symbLocks.ml | 7 ++++++-
 src/cdomains/exp.ml       | 3 +++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index ccf0ffe9d7..a8c74aa3c8 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -59,8 +59,12 @@ struct
       | a when not (Queries.ES.is_bot a) -> Queries.ES.add e a
       | _ -> Queries.ES.singleton e
     in
+    if M.tracing then M.tracel "symb_locks" "get_all_locks exps %a = %a\n" d_plainexp e Queries.ES.pretty exps;
+    if M.tracing then M.tracel "symb_locks" "get_all_locks st = %a\n" D.pretty st;
     let add_locks x xs = PS.union (get_locks x st) xs in
-    Queries.ES.fold add_locks exps (PS.empty ())
+    let r = Queries.ES.fold add_locks exps (PS.empty ()) in
+    if M.tracing then M.tracel "symb_locks" "get_all_locks %a = %a\n" d_plainexp e PS.pretty r;
+    r
 
   let same_unknown_index (ask: Queries.ask) exp slocks =
     let uk_index_equal i1 i2 = ask.f (Queries.MustBeEqual (i1, i2)) in
@@ -148,6 +152,7 @@ struct
     *)
     let one_perelem (e,a,l) xs =
       (* ignore (printf "one_perelem (%a,%a,%a)\n" Exp.pretty e Exp.pretty a Exp.pretty l); *)
+      if M.tracing then M.tracel "symb_locks" "one_perelem (%a,%a,%a)\n" Exp.pretty e Exp.pretty a Exp.pretty l;
       match Exp.fold_offs (Exp.replace_base (dummyFunDec.svar,`NoOffset) e l) with
       | Some (v, o) ->
         (* ignore (printf "adding lock %s\n" l); *)
diff --git a/src/cdomains/exp.ml b/src/cdomains/exp.ml
index 35c585f8ef..9fd075c204 100644
--- a/src/cdomains/exp.ml
+++ b/src/cdomains/exp.ml
@@ -1,6 +1,8 @@
 open Pretty
 open Cil
 
+module M = Messages
+
 module Exp =
 struct
   include CilType.Exp
@@ -331,6 +333,7 @@ struct
     List.rev el, fs
 
   let from_exps a l : t option =
+    if M.tracing then M.tracel "symb_locks" "from_exps %a (%s) %a (%s)\n" d_plainexp a (ees_to_str (toEl a)) d_plainexp l (ees_to_str (toEl l));
     let a, l = toEl a, toEl l in
     (* ignore (printf "from_exps:\n %s\n %s\n" (ees_to_str a) (ees_to_str l)); *)
     (*let rec fold_left2 f a xs ys =

From f5c4e895b2ed3cfa0c0e74347de1fdf7bc71c56f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 12:06:33 +0300
Subject: [PATCH 06/32] Quick fix symb_locks toEl for IndexPI

---
 src/cdomains/exp.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/cdomains/exp.ml b/src/cdomains/exp.ml
index 9fd075c204..9d2b7fee07 100644
--- a/src/cdomains/exp.ml
+++ b/src/cdomains/exp.ml
@@ -292,6 +292,8 @@ struct
     in
     let rec helper exp =
       match exp with
+      | BinOp ((PlusPI | IndexPI), e1, e2, _) ->
+        helper e1 (* TODO: what about e2? add to some Index offset to all? *)
       | SizeOf _
       | SizeOfE _
       | SizeOfStr _

From 752d16caf2beae97f7ecbb08bdb071de435b731c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 12:08:18 +0300
Subject: [PATCH 07/32] Fix symb_locks toEl for StartOf

---
 src/cdomains/exp.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/cdomains/exp.ml b/src/cdomains/exp.ml
index 9d2b7fee07..b4d1890496 100644
--- a/src/cdomains/exp.ml
+++ b/src/cdomains/exp.ml
@@ -301,12 +301,13 @@ struct
       | AlignOfE _
       | UnOp _
       | BinOp _
-      | StartOf _
       | Const _ -> raise NotSimpleEnough
       | Lval (Var v, os) -> EVar v :: conv_o os
       | Lval (Mem e, os) -> helper e @ [EDeref] @ conv_o os
       | AddrOf (Var v, os) -> EVar v :: conv_o os @ [EAddr]
       | AddrOf (Mem e, os) -> helper e @ [EDeref] @ conv_o os @ [EAddr]
+      | StartOf (Var v, os) -> EVar v :: conv_o os @ [EAddr]
+      | StartOf (Mem e, os) -> helper e @ [EDeref] @ conv_o os @ [EAddr]
       | CastE (_,e) -> helper e
       | Question _ -> failwith "Logical operations should be compiled away by CIL."
       | _ -> failwith "Unmatched pattern."

From 180ed23bcf5c64bd02b7e02e26c43817313bd542 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 12:09:04 +0300
Subject: [PATCH 08/32] Fix VarEq.may_change with constant

Previously "changing" a constant could change anything.
---
 src/analyses/varEq.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 93c01addba..7bc952e598 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -315,7 +315,8 @@ struct
            | _ -> failwith "Unmatched pattern."
     in
     let r =
-      if Queries.LS.is_top bls || Queries.LS.mem (dummyFunDec.svar, `NoOffset) bls
+      if Cil.isConstant b then false
+      else if Queries.LS.is_top bls || Queries.LS.mem (dummyFunDec.svar, `NoOffset) bls
       then ((*Messages.warn "No PT-set: switching to types ";*) type_may_change_apt a )
       else Queries.LS.exists (lval_may_change_pt a) bls
     in
@@ -323,7 +324,9 @@ struct
           then (Messages.warn ~msg:("Kill " ^sprint 80 (Exp.pretty () a)^" because of "^sprint 80 (Exp.pretty () b)) (); r)
           else (Messages.warn ~msg:("Keep " ^sprint 80 (Exp.pretty () a)^" because of "^sprint 80 (Exp.pretty () b)) (); r)
           Messages.warn ~msg:(sprint 80 (Exp.pretty () b) ^" changed lvalues: "^sprint 80 (Queries.LS.pretty () bls)) ();
-    *)    r
+    *)
+    if M.tracing then M.tracel "var_eq" "may_change %a %a = %B\n" CilType.Exp.pretty b CilType.Exp.pretty a r;
+    r
 
   (* Remove elements, that would change if the given lval would change.*)
   let remove_exp ask (e:exp) (st:D.t) : D.t =

From 653d0bb5786383ef00433397eff9edebf97c02c8 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 12:41:10 +0300
Subject: [PATCH 09/32] Enable all code paths in chrony-name2ipaddress

This makes it match default chrony analysis.
---
 tests/regression/06-symbeq/38-chrony-name2ipaddress.c | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/tests/regression/06-symbeq/38-chrony-name2ipaddress.c b/tests/regression/06-symbeq/38-chrony-name2ipaddress.c
index 6a4fec5ac9..05259683ee 100644
--- a/tests/regression/06-symbeq/38-chrony-name2ipaddress.c
+++ b/tests/regression/06-symbeq/38-chrony-name2ipaddress.c
@@ -1,10 +1,11 @@
-// PARAM: --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'mallocFresh'" --set ana.malloc.wrappers '["Malloc"]' --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals
+// PARAM: --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'mallocFresh'" --set ana.malloc.wrappers '["Malloc"]' --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals --set pre.cppflags[+] -D_FORTIFY_SOURCE=2 --set pre.cppflags[+] -O3
 #include <stddef.h>
 #include <stdint.h>
 // #include <sys/types.h>
 // #include <sys/socket.h>
 #include <netdb.h>
 #include <pthread.h>
+#include <string.h>
 
 void *
 Malloc(size_t size)
@@ -40,6 +41,8 @@ typedef struct {
 #define IPADDR_INET6 2
 #define IPADDR_ID 3
 
+#define FEAT_IPV6 1
+
 static int address_family = IPADDR_UNSPEC;
 
 int

From a4be26255157b495fc74b6353d83c856a3ebd5a7 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 12:41:33 +0300
Subject: [PATCH 10/32] Add var_eq add_eq tracing

---
 src/analyses/varEq.ml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 7bc952e598..9ff73d090e 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -379,6 +379,12 @@ struct
           let st =
     *)  let lvt = unrollType @@ Cilfacade.typeOfLval lv in
     (*     Messages.warn ~msg:(sprint 80 (d_type () lvt)) (); *)
+    if M.tracing then (
+      M.tracel "var_eq" "add_eq is_global_var %a = %B\n" d_plainlval lv (is_global_var ask (Lval lv) = Some false);
+      M.tracel "var_eq" "add_eq interesting %a = %B\n" d_plainexp rv (Exp.interesting rv);
+      M.tracel "var_eq" "add_eq is_global_var %a = %B\n" d_plainexp rv (is_global_var ask rv = Some false);
+      M.tracel "var_eq" "add_eq type %a = %B\n" d_plainlval lv ((isArithmeticType lvt && match lvt with | TFloat _ -> false | _ -> true ) || isPointerType lvt);
+    );
     if is_global_var ask (Lval lv) = Some false
     && Exp.interesting rv
     && is_global_var ask rv = Some false

From f753df5ca377d7000c5519ef6dd9c8264a1057da Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 12:41:56 +0300
Subject: [PATCH 11/32] Quick fix var_eq interesting for IndexPI

---
 src/cdomains/exp.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/cdomains/exp.ml b/src/cdomains/exp.ml
index b4d1890496..3e382642bd 100644
--- a/src/cdomains/exp.ml
+++ b/src/cdomains/exp.ml
@@ -12,6 +12,8 @@ struct
   (* TODO: what does interesting mean? *)
   let rec interesting x =
     match x with
+    | BinOp ((PlusPI | IndexPI), e1, e2, _) ->
+    interesting e1 (* TODO: what about e2? *)
     | SizeOf _
     | SizeOfE _
     | SizeOfStr _

From e10102e24532905e813d58db77a37474d93f0345 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 12:59:26 +0300
Subject: [PATCH 12/32] Add __goblint_assume_join test

---
 .../51-threadjoins/03-other-assume.c          | 34 +++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 tests/regression/51-threadjoins/03-other-assume.c

diff --git a/tests/regression/51-threadjoins/03-other-assume.c b/tests/regression/51-threadjoins/03-other-assume.c
new file mode 100644
index 0000000000..71db72fcec
--- /dev/null
+++ b/tests/regression/51-threadjoins/03-other-assume.c
@@ -0,0 +1,34 @@
+//PARAM: --set ana.activated[+] threadJoins
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  return NULL;
+}
+
+void *t_benign(void *arg) {
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_fun, NULL);
+  __goblint_assume_join(id2, NULL);
+  // t_fun should be in here
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  pthread_t id2[10];
+  for(int i =0; i < 10;i++) {
+  pthread_create(&id2[i], NULL, t_benign, NULL);
+  }
+
+  __goblint_assume_join(id2[2]);
+
+  // t_benign and t_fun should be in here
+
+  return 0;
+}

From 4a8aa8575c48f4e224ac7753e4bf2a09e525da95 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 12:59:45 +0300
Subject: [PATCH 13/32] Implement __goblint_assume_join in threadJoins analysis

---
 src/analyses/libraryFunctions.ml |  1 +
 src/analyses/threadJoins.ml      | 13 +++++++++++++
 2 files changed, 14 insertions(+)

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index be3875c4a7..fd8f7b1219 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -521,6 +521,7 @@ let invalidate_actions = [
     "down_trylock", readsAll;
     "up", readsAll;
     "ZSTD_customFree", frees [1]; (* only used with extraspecials *)
+    "__goblint_assume_join", readsAll;
   ]
 
 (* used by get_invalidate_action to make sure
diff --git a/src/analyses/threadJoins.ml b/src/analyses/threadJoins.ml
index 4638f6417e..72a91be836 100644
--- a/src/analyses/threadJoins.ml
+++ b/src/analyses/threadJoins.ml
@@ -45,6 +45,19 @@ struct
         | _ -> ctx.local (* if multiple possible thread ids are joined, none of them is must joined*)
         (* Possible improvement: Do the intersection first, things that are must joined in all possibly joined threads are must-joined *)
       )
+    | `Unknown "__goblint_assume_join" ->
+      let id = List.hd arglist in
+      let threads = ctx.ask (Queries.EvalThread id) in
+      if TIDs.is_top threads then
+        D.bot () (* consider everything joined, D is reversed so bot is All threads *)
+      else (
+        (* elements throws if the thread set is top *)
+        let threads = TIDs.elements threads in
+        List.fold_left (fun acc tid ->
+            let joined = ctx.global tid in
+            D.union (D.add tid acc) joined
+          ) ctx.local threads
+      )
     | _ -> ctx.local
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =

From ed6b2e4b7d5e4addc3b4606f00dce98412306920 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 14:33:47 +0300
Subject: [PATCH 14/32] Fix MHP.must_be_joined for top joined set

---
 src/cdomains/mHP.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cdomains/mHP.ml b/src/cdomains/mHP.ml
index 9b4d773a3c..acf74e4ca9 100644
--- a/src/cdomains/mHP.ml
+++ b/src/cdomains/mHP.ml
@@ -54,7 +54,7 @@ let exists_definitely_not_started_in_joined (current,created) other_joined =
 (** Must the thread with thread id other be already joined  *)
 let must_be_joined other joined =
   if ConcDomain.ThreadSet.is_top joined then
-    false
+    true (* top means all threads are joined, so [other] must be as well *)
   else
     List.mem other (ConcDomain.ThreadSet.elements joined)
 

From c5cf5265256e88e10b6d57238682252c32bac071 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 14:34:28 +0300
Subject: [PATCH 15/32] Quick fix realloc read accesses to be shallow

---
 src/analyses/accessAnalysis.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index d19e75b528..9757f39cd3 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -220,6 +220,7 @@ struct
         | "memset" | "__builtin_memset" | "__builtin___memset_chk" -> false
         | "bzero" | "__builtin_bzero" | "explicit_bzero" | "__explicit_bzero_chk" -> false
         | "__builtin_object_size" -> false
+        | "realloc" -> false
         | _ -> true
       in
       List.iter (access_one_top ctx `Read reach) (arg_acc `Read);

From 2b60af7e495ee5e1a11d8b97ae41a0bc87594932 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 14:34:48 +0300
Subject: [PATCH 16/32] Add option sem.unknown_function.read.args

---
 src/analyses/accessAnalysis.ml |  6 +++++-
 src/util/options.schema.json   | 14 ++++++++++++++
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index 9757f39cd3..26b30e5fcb 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -207,7 +207,11 @@ struct
       let arg_acc act =
         match act, LF.get_threadsafe_inv_ac x with
         | _, Some fnc -> (fnc act arglist)
-        | `Read, None -> arglist
+        | `Read, None ->
+          if get_bool "sem.unknown_function.read.args" then
+            arglist
+          else
+            []
         | (`Write | `Free), None ->
           if get_bool "sem.unknown_function.invalidate.args" then
             arglist
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 987d8f32a3..82257c8afb 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1136,6 +1136,20 @@
                 }
               },
               "additionalProperties": false
+            },
+            "read": {
+              "title": "sem.unknown_function.read",
+              "type": "object",
+              "properties": {
+                "args": {
+                  "title": "sem.unknown_function.read.args",
+                  "description":
+                    "Unknown function call reads arguments passed to it",
+                  "type": "boolean",
+                  "default": true
+                }
+              },
+              "additionalProperties": false
             }
           },
           "additionalProperties": false

From ea05ea88e70b590cc62fb1011564a33aa2b327ea Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 5 May 2022 15:48:09 +0300
Subject: [PATCH 17/32] Fix 02-base/78-realloc-free write-free race

---
 tests/regression/02-base/78-realloc-free.c | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/regression/02-base/78-realloc-free.c b/tests/regression/02-base/78-realloc-free.c
index a34e112a03..9eeb44cc4a 100644
--- a/tests/regression/02-base/78-realloc-free.c
+++ b/tests/regression/02-base/78-realloc-free.c
@@ -21,7 +21,7 @@ void test1() {
 
 void* test2_f(void *arg) {
   int *p = arg;
-  *p = 1; // RACE!
+  *p = 1; // NORACE
   return NULL;
 }
 
@@ -29,7 +29,7 @@ void test2() {
   int *p = malloc(sizeof(int));
   pthread_t id;
   pthread_create(&id, NULL, test2_f, p);
-  realloc(p, sizeof(int)); // RACE!
+  realloc(p, sizeof(int)); // NORACE
 }
 
 void* test3_f(void *arg) {

From 577f6f33e83d9d3f64974dbe06c7e68374a679eb Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 11 May 2022 10:27:23 +0200
Subject: [PATCH 18/32] Add test that's unsound because of
 __goblint_assume_join(...)

---
 tests/regression/46-apron2/03-other-assume.c | 38 ++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 tests/regression/46-apron2/03-other-assume.c

diff --git a/tests/regression/46-apron2/03-other-assume.c b/tests/regression/46-apron2/03-other-assume.c
new file mode 100644
index 0000000000..066ddac122
--- /dev/null
+++ b/tests/regression/46-apron2/03-other-assume.c
@@ -0,0 +1,38 @@
+//PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --sets ana.apron.privatization mutex-meet-tid
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  return NULL;
+}
+
+void *t_benign(void *arg) {
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_fun, NULL);
+  __goblint_assume_join(id2, NULL);
+  // t_fun should be in here
+
+  g = 7;
+
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  pthread_t id2[10];
+  for(int i =0; i < 10;i++) {
+    pthread_create(&id2[i], NULL, t_benign, NULL);
+  }
+
+  __goblint_assume_join(id2[2]);
+  // t_benign and t_fun should be in here
+
+  assert(g==h); //FAIL
+
+  return 0;
+}

From 76f9b29884da7c8ec329979d35db92f4838d6a02 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 12 May 2022 12:09:20 +0300
Subject: [PATCH 19/32] Add threadJoins test where recreated threads should be
 removed from must-join set

---
 .../51-threadjoins/04-assume-recreate.c       | 23 +++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 tests/regression/51-threadjoins/04-assume-recreate.c

diff --git a/tests/regression/51-threadjoins/04-assume-recreate.c b/tests/regression/51-threadjoins/04-assume-recreate.c
new file mode 100644
index 0000000000..8424303e97
--- /dev/null
+++ b/tests/regression/51-threadjoins/04-assume-recreate.c
@@ -0,0 +1,23 @@
+//PARAM: --set ana.activated[+] threadJoins --disable ana.thread.include-node --set ana.thread.domain plain
+#include <pthread.h>
+#include <assert.h>
+
+int g = 0;
+
+void *t_fun(void *arg) {
+  g++; // RACE!
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  __goblint_assume_join(id); // should add to must-joined
+
+  pthread_create(&id, NULL, t_fun, NULL); // should remove from must-joined again
+
+  g++; // RACE!
+
+  return 0;
+}

From 84a98bfde82b70e21609041e4263a844122cd19d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 12 May 2022 12:14:24 +0300
Subject: [PATCH 20/32] Make threadspawn remove must-joined threads

---
 src/analyses/threadJoins.ml | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/analyses/threadJoins.ml b/src/analyses/threadJoins.ml
index 72a91be836..024cfe41be 100644
--- a/src/analyses/threadJoins.ml
+++ b/src/analyses/threadJoins.ml
@@ -60,6 +60,13 @@ struct
       )
     | _ -> ctx.local
 
+  let threadspawn ctx lval f args fctx =
+    match ThreadId.get_current (Analyses.ask_of_ctx fctx) with
+    | `Lifted tid ->
+      D.remove tid ctx.local
+    | _ ->
+      ctx.local
+
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with
     | Queries.MustJoinedThreads -> (ctx.local:ConcDomain.MustThreadSet.t) (* type annotation needed to avoid "would escape the scope of its equation" *)

From b09b1fd4ea29082968836e5166b38b5fc016e9ff Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 12 May 2022 12:16:35 +0300
Subject: [PATCH 21/32] Add SKIP to 36-apron2/03-other-assume like other Apron
 tests

---
 tests/regression/46-apron2/03-other-assume.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/regression/46-apron2/03-other-assume.c b/tests/regression/46-apron2/03-other-assume.c
index 066ddac122..e02d33d386 100644
--- a/tests/regression/46-apron2/03-other-assume.c
+++ b/tests/regression/46-apron2/03-other-assume.c
@@ -1,4 +1,4 @@
-//PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --sets ana.apron.privatization mutex-meet-tid
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --sets ana.apron.privatization mutex-meet-tid
 #include <pthread.h>
 #include <assert.h>
 

From f2b8673e53e32ac1ef953467abb3d9bcf7cf2667 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 12 May 2022 12:27:40 +0300
Subject: [PATCH 22/32] Fix __goblint_assume_join with Apron mutex-meet-tid
 privatization

---
 src/analyses/apron/apronAnalysis.apron.ml |  3 ++
 src/analyses/apron/apronPriv.apron.ml     | 49 +++++++++++++++--------
 2 files changed, 35 insertions(+), 17 deletions(-)

diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml
index b1ef74bd4d..5ffd4b67a1 100644
--- a/src/analyses/apron/apronAnalysis.apron.ml
+++ b/src/analyses/apron/apronAnalysis.apron.ml
@@ -323,6 +323,9 @@ struct
         | Some lv -> invalidate_one st' lv
         | None -> st'
       )
+    | `Unknown "__goblint_assume_join" ->
+      let id = List.hd args in
+      Priv.thread_join ~force:true ask ctx.global id st
     | _ ->
       let ask = Analyses.ask_of_ctx ctx in
       let invalidate_one st lv =
diff --git a/src/analyses/apron/apronPriv.apron.ml b/src/analyses/apron/apronPriv.apron.ml
index 49ef99302f..83299dad58 100644
--- a/src/analyses/apron/apronPriv.apron.ml
+++ b/src/analyses/apron/apronPriv.apron.ml
@@ -37,7 +37,7 @@ module type S =
     val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> apron_components_t -> apron_components_t
     val threadenter: Q.ask -> (V.t -> G.t) -> apron_components_t -> apron_components_t
 
-    val thread_join: Q.ask -> (V.t -> G.t) -> Cil.exp -> apron_components_t -> apron_components_t
+    val thread_join: ?force:bool -> Q.ask -> (V.t -> G.t) -> Cil.exp -> apron_components_t -> apron_components_t
     val thread_return: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> ThreadIdDomain.Thread.t -> apron_components_t -> apron_components_t
     val iter_sys_vars: (V.t -> G.t) -> VarQuery.t -> V.t VarQuery.f -> unit (** [Queries.IterSysVars] for apron. *)
 
@@ -62,7 +62,7 @@ struct
   let lock ask getg st m = st
   let unlock ask getg sideg st m = st
 
-  let thread_join ask getg exp st = st
+  let thread_join ?(force=false) ask getg exp st = st
   let thread_return ask getg sideg tid st = st
 
   let sync ask getg sideg st reason = st
@@ -270,7 +270,7 @@ struct
     {apr = apr_local'; priv = (p', w')}
 
 
-  let thread_join ask getg exp st = st
+  let thread_join ?(force=false) ask getg exp st = st
   let thread_return ask getg sideg tid st = st
 
   let sync ask getg sideg (st: apron_components_t) reason =
@@ -461,7 +461,7 @@ struct
     let apr_local = remove_globals_unprotected_after_unlock ask m apr in
     {st with apr = apr_local}
 
-  let thread_join ask getg exp st = st
+  let thread_join ?(force=false) ask getg exp st = st
   let thread_return ask getg sideg tid st = st
 
   let sync ask getg sideg (st: apron_components_t) reason =
@@ -983,22 +983,37 @@ struct
       let l' = L.add lm apr_side l in
       {apr = apr_local; priv = (w',LMust.add lm lmust,l')}
 
-  let thread_join (ask:Q.ask) getg exp (st: apron_components_t) =
+  let thread_join ?(force=false) (ask:Q.ask) getg exp (st: apron_components_t) =
     let w,lmust,l = st.priv in
     let tids = ask.f (Q.EvalThread exp) in
-    if ConcDomain.ThreadSet.is_top tids then
-      st (* TODO: why needed? *)
+    if force then (
+      if ConcDomain.ThreadSet.is_top tids then
+        failwith "TODO"
+      else (
+        (* fold throws if the thread set is top *)
+        let (lmust', l') = ConcDomain.ThreadSet.fold (fun tid (lmust, l) ->
+            let lmust',l' = G.thread (getg (V.thread tid)) in
+            (LMust.union lmust' lmust, L.join l l')
+          ) tids (lmust, l)
+        in
+        {st with priv = (w, lmust', l')}
+      )
+    )
     else (
-      (* elements throws if the thread set is top *)
-      let tids = ConcDomain.ThreadSet.elements tids in
-      match tids with
-      | [tid] ->
-        let lmust',l' = G.thread (getg (V.thread tid)) in
-        {st with priv = (w, LMust.union lmust' lmust, L.join l l')}
-      | _ ->
-        (* To match the paper more closely, one would have to join in the non-definite case too *)
-        (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *)
-        st
+      if ConcDomain.ThreadSet.is_top tids then
+        st (* TODO: why needed? *)
+      else (
+        (* elements throws if the thread set is top *)
+        let tids = ConcDomain.ThreadSet.elements tids in
+        match tids with
+        | [tid] ->
+          let lmust',l' = G.thread (getg (V.thread tid)) in
+          {st with priv = (w, LMust.union lmust' lmust, L.join l l')}
+        | _ ->
+          (* To match the paper more closely, one would have to join in the non-definite case too *)
+          (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *)
+          st
+      )
     )
 
   let thread_return ask getg sideg tid (st: apron_components_t) =

From d5a0c27e3aec3d88621241e5193a5810d0d67370 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 12 May 2022 12:53:34 +0300
Subject: [PATCH 23/32] Add __goblint_assume_join to annotating docs

---
 docs/user-guide/annotating.md | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/docs/user-guide/annotating.md b/docs/user-guide/annotating.md
index 17698e6eda..db4749ccbb 100644
--- a/docs/user-guide/annotating.md
+++ b/docs/user-guide/annotating.md
@@ -25,3 +25,11 @@ The following string arguments are supported:
 3. `base.non-ptr`/`base.no-non-ptr` to override the `ana.base.context.non-ptr` option.
 4. `apron.context`/`apron.no-context` to override the `ana.apron.context` option.
 5. `widen`/`no-widen` to override the `ana.context.widen` option.
+
+
+## Functions
+Goblint-specific functions can be called in the code, where they assist the analyzer but have no runtime effect.
+
+* `__goblint_assume_join(id)` is like `pthread_join(id)`, but considers the given thread IDs must-joined even if Goblint cannot, e.g. due to non-uniqueness.
+  Notably, this annotation can be used after a threads joining loop to make the assumption that the loop correctly joined all those threads.
+  _Misuse of this annotation can cause unsoundness._

From a4db1a0e0a897b2b82793b8a8f944370ac42b52f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 13 May 2022 10:04:15 +0300
Subject: [PATCH 24/32] Add assume join test with unknown thread ID

---
 .../51-threadjoins/05-assume-unknown.c        | 21 +++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 tests/regression/51-threadjoins/05-assume-unknown.c

diff --git a/tests/regression/51-threadjoins/05-assume-unknown.c b/tests/regression/51-threadjoins/05-assume-unknown.c
new file mode 100644
index 0000000000..d870918240
--- /dev/null
+++ b/tests/regression/51-threadjoins/05-assume-unknown.c
@@ -0,0 +1,21 @@
+//PARAM: --set ana.activated[+] threadJoins
+#include <pthread.h>
+#include <assert.h>
+
+int g = 0;
+
+void *t_fun(void *arg) {
+  g++; // RACE!
+  return NULL;
+}
+
+int main() {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  __goblint_assume_join(id2); // joining unknown thread ID, shouldn't make joined set All threads
+
+  g++; // RACE!
+
+  return 0;
+}

From e6e33b290d54a126774097a6b16364ccf43e60f6 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 13 May 2022 10:06:48 +0300
Subject: [PATCH 25/32] Change assume join behavior with unknown thread ID

---
 src/analyses/apron/apronPriv.apron.ml | 2 +-
 src/analyses/threadJoins.ml           | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analyses/apron/apronPriv.apron.ml b/src/analyses/apron/apronPriv.apron.ml
index 83299dad58..1b8a71f4c4 100644
--- a/src/analyses/apron/apronPriv.apron.ml
+++ b/src/analyses/apron/apronPriv.apron.ml
@@ -988,7 +988,7 @@ struct
     let tids = ask.f (Q.EvalThread exp) in
     if force then (
       if ConcDomain.ThreadSet.is_top tids then
-        failwith "TODO"
+        st (* don't consider anything more joined, matches threadJoins analysis *)
       else (
         (* fold throws if the thread set is top *)
         let (lmust', l') = ConcDomain.ThreadSet.fold (fun tid (lmust, l) ->
diff --git a/src/analyses/threadJoins.ml b/src/analyses/threadJoins.ml
index 024cfe41be..c85061de71 100644
--- a/src/analyses/threadJoins.ml
+++ b/src/analyses/threadJoins.ml
@@ -49,7 +49,7 @@ struct
       let id = List.hd arglist in
       let threads = ctx.ask (Queries.EvalThread id) in
       if TIDs.is_top threads then
-        D.bot () (* consider everything joined, D is reversed so bot is All threads *)
+        ctx.local (* don't consider everything joined, because would be confusing to have All threads unsoundly joined due to imprecision *)
       else (
         (* elements throws if the thread set is top *)
         let threads = TIDs.elements threads in

From 60168357f464e13ef0d11217215049164cbe2aff Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 13 May 2022 17:34:50 +0200
Subject: [PATCH 26/32] Add example where `__goblint_assume_join` causes
 unneccessary precision loss

---
 .../46-apron2/04-other-assume-inprec.c        | 30 +++++++++++++++++++
 1 file changed, 30 insertions(+)
 create mode 100644 tests/regression/46-apron2/04-other-assume-inprec.c

diff --git a/tests/regression/46-apron2/04-other-assume-inprec.c b/tests/regression/46-apron2/04-other-assume-inprec.c
new file mode 100644
index 0000000000..b07c5b42f1
--- /dev/null
+++ b/tests/regression/46-apron2/04-other-assume-inprec.c
@@ -0,0 +1,30 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --sets ana.apron.privatization mutex-meet-tid
+#include <pthread.h>
+#include <assert.h>
+
+int g = 10;
+int h = 10;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  g = 7;
+  return NULL;
+}
+
+int main(void) {
+  int t;
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_join(id,NULL);
+
+  g = h;
+  assert(g == h);
+
+  // __goblint_assume_join for something Goblint knows is joined should not worsen precision
+  __goblint_assume_join(id);
+
+  assert(g == h);
+
+  return 0;
+}

From 22d6da850252ca8f422452e4626b727d4fdb5a16 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 13 May 2022 17:40:51 +0200
Subject: [PATCH 27/32] Add problematic index access

---
 .../06-symbeq/39-funloop_index_bad.c          | 36 +++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 tests/regression/06-symbeq/39-funloop_index_bad.c

diff --git a/tests/regression/06-symbeq/39-funloop_index_bad.c b/tests/regression/06-symbeq/39-funloop_index_bad.c
new file mode 100644
index 0000000000..7bd0bb78ea
--- /dev/null
+++ b/tests/regression/06-symbeq/39-funloop_index_bad.c
@@ -0,0 +1,36 @@
+// PARAM: --disable ana.mutex.disjoint_types --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+// copy of 06/02 with additional index accesses (that are wrong)
+#include<pthread.h>
+#include<stdio.h>
+
+struct cache_entry {
+  int refs;
+  pthread_mutex_t refs_mutex;
+} cache[10];
+
+void cache_entry_addref(struct cache_entry *entry) {
+  pthread_mutex_lock(&entry->refs_mutex);
+  entry->refs++; // NORACE
+  (*entry).refs++; // NORACE
+  entry[1].refs++; // RACE
+  pthread_mutex_unlock(&entry->refs_mutex);
+}
+
+void *t_fun(void *arg) {
+  int i;
+  for(i=0; i<9; i++)
+    cache_entry_addref(&cache[i]); // NORACE
+  return NULL;
+}
+
+int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&cache[i].refs_mutex, NULL);
+
+  int i;
+  pthread_t t1;
+  pthread_create(&t1, NULL, t_fun, NULL);
+  for(i=0; i<9; i++)
+    cache_entry_addref(&cache[i]); // NORACE
+  return 0;
+}

From a482bd1c266490441a080ddd8fd88605b3ca6355 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 16 May 2022 12:20:19 +0300
Subject: [PATCH 28/32] Fix Apron mutex-meet-tid imprecision by force joining
 must-joined threads

---
 src/analyses/apron/apronPriv.apron.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/analyses/apron/apronPriv.apron.ml b/src/analyses/apron/apronPriv.apron.ml
index 1b8a71f4c4..0959828fe1 100644
--- a/src/analyses/apron/apronPriv.apron.ml
+++ b/src/analyses/apron/apronPriv.apron.ml
@@ -991,10 +991,11 @@ struct
         st (* don't consider anything more joined, matches threadJoins analysis *)
       else (
         (* fold throws if the thread set is top *)
+        let tids' = ConcDomain.ThreadSet.diff tids (ask.f Q.MustJoinedThreads) in (* avoid unnecessary imprecision by force joining already must-joined threas, e.g. 46-apron2/04-other-assume-inprec *)
         let (lmust', l') = ConcDomain.ThreadSet.fold (fun tid (lmust, l) ->
             let lmust',l' = G.thread (getg (V.thread tid)) in
             (LMust.union lmust' lmust, L.join l l')
-          ) tids (lmust, l)
+          ) tids' (lmust, l)
         in
         {st with priv = (w, lmust', l')}
       )

From 67211c2c0eb7c2b61efa5b9db82976fecaf7ed77 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 16 May 2022 13:01:08 +0300
Subject: [PATCH 29/32] Fix annotations in 06-symbeq/39-funloop_index_bad

---
 tests/regression/06-symbeq/39-funloop_index_bad.c | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/regression/06-symbeq/39-funloop_index_bad.c b/tests/regression/06-symbeq/39-funloop_index_bad.c
index 7bd0bb78ea..1983887796 100644
--- a/tests/regression/06-symbeq/39-funloop_index_bad.c
+++ b/tests/regression/06-symbeq/39-funloop_index_bad.c
@@ -10,9 +10,9 @@ struct cache_entry {
 
 void cache_entry_addref(struct cache_entry *entry) {
   pthread_mutex_lock(&entry->refs_mutex);
-  entry->refs++; // NORACE
-  (*entry).refs++; // NORACE
-  entry[1].refs++; // RACE
+  entry->refs++; // RACE!
+  (*entry).refs++; // RACE!
+  entry[1].refs++; // RACE!
   pthread_mutex_unlock(&entry->refs_mutex);
 }
 

From 92c7ea46264bee2eda7ceb621310affb7a2ed0ac Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 16 May 2022 15:41:11 +0300
Subject: [PATCH 30/32] Replace symb_locks and var_eq IndexPI handling with
 very ad-hoc one

This fixes the soundness, but still works for chrony story.
---
 src/analyses/varEq.ml                         | 12 ++++++++++--
 src/cdomains/exp.ml                           |  6 ++----
 tests/regression/06-symbeq/37-funloop_index.c |  6 +++---
 3 files changed, 15 insertions(+), 9 deletions(-)

diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 9ff73d090e..dfde1a3de8 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -530,8 +530,16 @@ struct
   let rec eq_set_clos e s =
     if M.tracing then M.traceli "var_eq" "eq_set_clos %a\n" d_plainexp e;
     let r = match e with
-    | BinOp ((PlusPI | IndexPI), e1, e2, _) ->
-      eq_set_clos e1 s (* TODO: what about e2? add to some Index offset to all? *)
+    | AddrOf (Mem (BinOp (IndexPI, a, i, _)), os) ->
+      (* convert IndexPI to Index offset *)
+      (* TODO: this applies eq_set_clos under the offset, unlike cases below; should generalize? *)
+      Queries.ES.fold (fun e acc -> (* filter_map *)
+        match e with
+        | CastE (_, StartOf a') -> (* eq_set adds casts *)
+          let e' = AddrOf (Cil.addOffsetLval (Index (i, os)) a') in (* TODO: re-add cast? *)
+          Queries.ES.add e' acc
+        | _ -> acc
+      ) (eq_set_clos a s) (Queries.ES.empty ())
     | SizeOf _
     | SizeOfE _
     | SizeOfStr _
diff --git a/src/cdomains/exp.ml b/src/cdomains/exp.ml
index 3e382642bd..d02a90a6b8 100644
--- a/src/cdomains/exp.ml
+++ b/src/cdomains/exp.ml
@@ -12,8 +12,7 @@ struct
   (* TODO: what does interesting mean? *)
   let rec interesting x =
     match x with
-    | BinOp ((PlusPI | IndexPI), e1, e2, _) ->
-    interesting e1 (* TODO: what about e2? *)
+    (* TODO: handle IndexPI like var_eq eq_set_clos? *)
     | SizeOf _
     | SizeOfE _
     | SizeOfStr _
@@ -294,8 +293,7 @@ struct
     in
     let rec helper exp =
       match exp with
-      | BinOp ((PlusPI | IndexPI), e1, e2, _) ->
-        helper e1 (* TODO: what about e2? add to some Index offset to all? *)
+      (* TODO: handle IndexPI like var_eq eq_set_clos? *)
       | SizeOf _
       | SizeOfE _
       | SizeOfStr _
diff --git a/tests/regression/06-symbeq/37-funloop_index.c b/tests/regression/06-symbeq/37-funloop_index.c
index 831ad62769..d4c269cc05 100644
--- a/tests/regression/06-symbeq/37-funloop_index.c
+++ b/tests/regression/06-symbeq/37-funloop_index.c
@@ -10,9 +10,9 @@ struct cache_entry {
 
 void cache_entry_addref(struct cache_entry *entry) {
   pthread_mutex_lock(&entry->refs_mutex);
-  entry->refs++; // NORACE
-  (*entry).refs++; // NORACE
-  entry[0].refs++; // NORACE
+  entry->refs++; // TODO NORACE
+  (*entry).refs++; // TODO NORACE
+  entry[0].refs++; // TODO NORACE
   pthread_mutex_unlock(&entry->refs_mutex);
 }
 

From 94fd11f57f0b74c5033e40ff42725c525bc4bd33 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 16 May 2022 17:59:15 +0300
Subject: [PATCH 31/32] Handle IndexPI in Exp.interesting to fix
 string_fortified.h race in 06-symbeq/38-chrony-name2ipaddress

---
 src/cdomains/exp.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/cdomains/exp.ml b/src/cdomains/exp.ml
index d02a90a6b8..8e74a6f417 100644
--- a/src/cdomains/exp.ml
+++ b/src/cdomains/exp.ml
@@ -12,7 +12,8 @@ struct
   (* TODO: what does interesting mean? *)
   let rec interesting x =
     match x with
-    (* TODO: handle IndexPI like var_eq eq_set_clos? *)
+    | AddrOf (Mem (BinOp (IndexPI, a, _i, _)), _os) ->
+      interesting a
     | SizeOf _
     | SizeOfE _
     | SizeOfStr _

From c491dbba47f257ce6f2e296cf48533195a22799b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 19 May 2022 15:37:22 +0300
Subject: [PATCH 32/32] Re-allow All threads must joined for chrony story, but
 warn about it

---
 scripts/update_suite.rb                       |  1 +
 src/analyses/apron/apronPriv.apron.ml         |  8 ++++---
 src/analyses/threadJoins.ml                   | 21 ++++++++++++-------
 .../51-threadjoins/05-assume-unknown.c        |  5 ++++-
 4 files changed, 24 insertions(+), 11 deletions(-)

diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb
index a573208a21..06c4d4dda3 100755
--- a/scripts/update_suite.rb
+++ b/scripts/update_suite.rb
@@ -159,6 +159,7 @@ def collect_warnings
                     when /Assertion .* is unknown/   then "unknown"
                     when /^\[Warning\]/              then "warn"
                     when /^\[Error\]/                then "warn"
+                    when /^\[Info\]/                 then "warn"
                     when /\[Debug\]/                 then next # debug "warnings" shouldn't count as other warnings (against NOWARN)
                     when /^  on line \d+ $/          then next # dead line warnings shouldn't count (used for unreachability with NOWARN)
                     when /^  on lines \d+..\d+ $/    then next # dead line warnings shouldn't count (used for unreachability with NOWARN)
diff --git a/src/analyses/apron/apronPriv.apron.ml b/src/analyses/apron/apronPriv.apron.ml
index 0959828fe1..86683a45d0 100644
--- a/src/analyses/apron/apronPriv.apron.ml
+++ b/src/analyses/apron/apronPriv.apron.ml
@@ -987,11 +987,13 @@ struct
     let w,lmust,l = st.priv in
     let tids = ask.f (Q.EvalThread exp) in
     if force then (
-      if ConcDomain.ThreadSet.is_top tids then
-        st (* don't consider anything more joined, matches threadJoins analysis *)
+      if ConcDomain.ThreadSet.is_top tids then (
+        M.info ~category:Unsound "Unknown thread ID assume-joined, Apron privatization unsound"; (* TODO: something more sound *)
+        st (* cannot find all thread IDs to join them all *)
+      )
       else (
         (* fold throws if the thread set is top *)
-        let tids' = ConcDomain.ThreadSet.diff tids (ask.f Q.MustJoinedThreads) in (* avoid unnecessary imprecision by force joining already must-joined threas, e.g. 46-apron2/04-other-assume-inprec *)
+        let tids' = ConcDomain.ThreadSet.diff tids (ask.f Q.MustJoinedThreads) in (* avoid unnecessary imprecision by force joining already must-joined threads, e.g. 46-apron2/04-other-assume-inprec *)
         let (lmust', l') = ConcDomain.ThreadSet.fold (fun tid (lmust, l) ->
             let lmust',l' = G.thread (getg (V.thread tid)) in
             (LMust.union lmust' lmust, L.join l l')
diff --git a/src/analyses/threadJoins.ml b/src/analyses/threadJoins.ml
index c85061de71..488e573e31 100644
--- a/src/analyses/threadJoins.ml
+++ b/src/analyses/threadJoins.ml
@@ -48,8 +48,10 @@ struct
     | `Unknown "__goblint_assume_join" ->
       let id = List.hd arglist in
       let threads = ctx.ask (Queries.EvalThread id) in
-      if TIDs.is_top threads then
-        ctx.local (* don't consider everything joined, because would be confusing to have All threads unsoundly joined due to imprecision *)
+      if TIDs.is_top threads then (
+        M.info ~category:Unsound "Unknown thread ID assume-joined, assuming ALL threads must-joined.";
+        D.bot () (* consider everything joined, D is reversed so bot is All threads *)
+      )
       else (
         (* elements throws if the thread set is top *)
         let threads = TIDs.elements threads in
@@ -61,11 +63,16 @@ struct
     | _ -> ctx.local
 
   let threadspawn ctx lval f args fctx =
-    match ThreadId.get_current (Analyses.ask_of_ctx fctx) with
-    | `Lifted tid ->
-      D.remove tid ctx.local
-    | _ ->
-      ctx.local
+    if D.is_bot ctx.local then ( (* bot is All threads *)
+      M.info ~category:Imprecise "Thread created while ALL threads must-joined, continuing with no threads joined.";
+      D.top () (* top is no threads *)
+    )
+    else
+      match ThreadId.get_current (Analyses.ask_of_ctx fctx) with
+      | `Lifted tid ->
+        D.remove tid ctx.local
+      | _ ->
+        ctx.local
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with
diff --git a/tests/regression/51-threadjoins/05-assume-unknown.c b/tests/regression/51-threadjoins/05-assume-unknown.c
index d870918240..7c113715cd 100644
--- a/tests/regression/51-threadjoins/05-assume-unknown.c
+++ b/tests/regression/51-threadjoins/05-assume-unknown.c
@@ -13,8 +13,11 @@ int main() {
   pthread_t id, id2;
   pthread_create(&id, NULL, t_fun, NULL);
 
-  __goblint_assume_join(id2); // joining unknown thread ID, shouldn't make joined set All threads
+  __goblint_assume_join(id2); // WARN joining unknown thread ID, make joined set All threads
 
+  g++; // NORACE
+
+  pthread_create(&id, NULL, t_fun, NULL); // WARN make joined set different from All threads
   g++; // RACE!
 
   return 0;