From 57c5c3f2ff6838150c4e99e703026a5ae9c599b7 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 25 Sep 2023 11:37:24 +0300
Subject: [PATCH 01/32] Add conditional accesses to LibraryDsl

---
 src/analyses/libraryDsl.ml  | 50 ++++++++++++++++++++++++++-----------
 src/analyses/libraryDsl.mli | 29 ++++++++++++---------
 2 files changed, 52 insertions(+), 27 deletions(-)

diff --git a/src/analyses/libraryDsl.ml b/src/analyses/libraryDsl.ml
index 49aac8ce9b..431d778b13 100644
--- a/src/analyses/libraryDsl.ml
+++ b/src/analyses/libraryDsl.ml
@@ -30,8 +30,20 @@ struct
     | [] -> fail "^::"
 end
 
+type access =
+  | Access of LibraryDesc.Access.t
+  | If of (unit -> bool) * access
+
+let rec eval_access = function
+  | Access acc -> Some acc
+  | If (p, access) ->
+    if p () then
+      eval_access access
+    else
+      None
+
 type ('k, 'l, 'r) arg_desc = {
-  accesses: Access.t list;
+  accesses: access list;
   match_arg: (Cil.exp, 'k, 'r) Pattern.t;
   match_var_args: (Cil.exp list, 'l, 'r) Pattern.t;
 }
@@ -51,15 +63,21 @@ let rec accs: type k r. (k, r) args_desc -> Accesses.t = fun args_desc args ->
   match args_desc, args with
   | [], [] -> []
   | VarArgs arg_desc, args ->
-    List.map (fun acc ->
-        (acc, args)
+    List.filter_map (fun access ->
+        match eval_access access with
+        | Some acc -> Some (acc, args)
+        | None -> None
       ) arg_desc.accesses
   | arg_desc :: args_desc, arg :: args ->
     let accs'' = accs args_desc args in
-    List.fold_left (fun (accs'': (Access.t * Cil.exp list) list) (acc: Access.t) ->
-        match List.assoc_opt acc accs'' with
-        | Some args -> (acc, arg :: args) :: List.remove_assoc acc accs''
-        | None -> (acc, [arg]) :: accs''
+    List.fold_left (fun (accs'': (Access.t * Cil.exp list) list) (access: access) ->
+        match eval_access access with
+        | Some acc ->
+          begin match List.assoc_opt acc accs'' with
+            | Some args -> (acc, arg :: args) :: List.remove_assoc acc accs''
+            | None -> (acc, [arg]) :: accs''
+          end
+        | None -> accs''
       ) accs'' arg_desc.accesses
   | _, _ -> invalid_arg "accs"
 
@@ -94,11 +112,13 @@ let drop (_name: string) accesses = { empty_drop_desc with accesses; }
 let drop' accesses = { empty_drop_desc with accesses; }
 
 
-let r = Access.{ kind = Read; deep = false; }
-let r_deep = Access.{ kind = Read; deep = true; }
-let w = Access.{ kind = Write; deep = false; }
-let w_deep = Access.{ kind = Write; deep = true; }
-let f = Access.{ kind = Free; deep = false; }
-let f_deep = Access.{ kind = Free; deep = true; }
-let s = Access.{ kind = Spawn; deep = false; }
-let s_deep = Access.{ kind = Spawn; deep = true; }
+let r = Access { kind = Read; deep = false; }
+let r_deep = Access { kind = Read; deep = true; }
+let w = Access { kind = Write; deep = false; }
+let w_deep = Access { kind = Write; deep = true; }
+let f = Access { kind = Free; deep = false; }
+let f_deep = Access { kind = Free; deep = true; }
+let s = Access { kind = Spawn; deep = false; }
+let s_deep = Access { kind = Spawn; deep = true; }
+
+let if_ p access = If (p, access)
diff --git a/src/analyses/libraryDsl.mli b/src/analyses/libraryDsl.mli
index fd0bc45c26..4ea6d7dae4 100644
--- a/src/analyses/libraryDsl.mli
+++ b/src/analyses/libraryDsl.mli
@@ -28,46 +28,51 @@ val special': ?attrs:LibraryDesc.attr list -> (LibraryDesc.special, LibraryDesc.
 (** Create unknown library function descriptor from arguments descriptor, which must {!drop} all arguments. *)
 val unknown: ?attrs:LibraryDesc.attr list -> (LibraryDesc.special, LibraryDesc.special) args_desc -> LibraryDesc.t
 
+(** Argument access descriptor. *)
+type access
 
 (** Argument descriptor, which captures the named argument with accesses for continuation function of {!special}. *)
-val __: string -> LibraryDesc.Access.t list -> (Cil.exp -> 'r, Cil.exp list -> 'r, 'r) arg_desc
+val __: string -> access list -> (Cil.exp -> 'r, Cil.exp list -> 'r, 'r) arg_desc
 
 (** Argument descriptor, which captures an unnamed argument with accesses for continuation function of {!special}. *)
-val __': LibraryDesc.Access.t list -> (Cil.exp -> 'r, Cil.exp list -> 'r, 'r) arg_desc
+val __': access list -> (Cil.exp -> 'r, Cil.exp list -> 'r, 'r) arg_desc
 
 (** Argument descriptor, which drops (does not capture) the named argument with accesses. *)
-val drop: string -> LibraryDesc.Access.t list -> ('r, 'r, 'r) arg_desc
+val drop: string -> access list -> ('r, 'r, 'r) arg_desc
 
 (** Argument descriptor, which drops (does not capture) an unnamed argument with accesses. *)
-val drop': LibraryDesc.Access.t list -> ('r, 'r, 'r) arg_desc
+val drop': access list -> ('r, 'r, 'r) arg_desc
 
 
 (** Shallow {!AccessKind.Read} access.
     All immediate arguments of function calls are always read, this specifies the reading of pointed-to values. *)
-val r: LibraryDesc.Access.t
+val r: access
 
 (** Deep {!AccessKind.Read} access.
     All immediate arguments of function calls are always read, this specifies the reading of pointed-to values.
     Rarely needed. *)
-val r_deep: LibraryDesc.Access.t
+val r_deep: access
 
 (** Shallow {!AccessKind.Write} access. *)
-val w: LibraryDesc.Access.t
+val w: access
 
 (** Deep {!AccessKind.Write} access.
     Rarely needed. *)
-val w_deep: LibraryDesc.Access.t
+val w_deep: access
 
 (** Shallow {!AccessKind.Free} access. *)
-val f: LibraryDesc.Access.t
+val f: access
 
 (** Deep {!AccessKind.Free} access.
     Rarely needed. *)
-val f_deep: LibraryDesc.Access.t
+val f_deep: access
 
 (** Shallow {!AccessKind.Spawn} access. *)
-val s: LibraryDesc.Access.t
+val s: access
 
 (** Deep {!AccessKind.Spawn} access.
     Rarely needed. *)
-val s_deep: LibraryDesc.Access.t
+val s_deep: access
+
+(** Conditional access, e.g. on an option. *)
+val if_: (unit -> bool) -> access -> access

From eed1e27067c47b2c86015d6fb1402f23ee7ffa22 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 18 Oct 2024 12:32:44 +0300
Subject: [PATCH 02/32] Improve flat string domain hash

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

diff --git a/src/cdomain/value/cdomains/stringDomain.ml b/src/cdomain/value/cdomains/stringDomain.ml
index 2b968b0321..5ed704ce69 100644
--- a/src/cdomain/value/cdomains/stringDomain.ml
+++ b/src/cdomain/value/cdomains/stringDomain.ml
@@ -20,9 +20,10 @@ let reset_lazy () =
 
 
 type t = string option [@@deriving eq, ord, hash]
+(** [None] means top. *)
 
 let hash x =
-  if get_string_domain () = Disjoint then
+  if get_string_domain () <> Unit then
     hash x
   else
     13859

From 2284da8ed5f909c39f204f9b123c3ce3d9149fee Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 18 Oct 2024 12:36:26 +0300
Subject: [PATCH 03/32] Improve StringDomain type safety by matching all
 domains

This is more robust against changes to the possible choices of domain.
It would have avoided issue #1594.
---
 src/cdomain/value/cdomains/stringDomain.ml | 35 +++++++++++-----------
 1 file changed, 17 insertions(+), 18 deletions(-)

diff --git a/src/cdomain/value/cdomains/stringDomain.ml b/src/cdomain/value/cdomains/stringDomain.ml
index 5ed704ce69..35054590f9 100644
--- a/src/cdomain/value/cdomains/stringDomain.ml
+++ b/src/cdomain/value/cdomains/stringDomain.ml
@@ -23,10 +23,9 @@ type t = string option [@@deriving eq, ord, hash]
 (** [None] means top. *)
 
 let hash x =
-  if get_string_domain () <> Unit then
-    hash x
-  else
-    13859
+  match get_string_domain () with
+  | Disjoint | Flat -> hash x
+  | Unit -> 13859
 
 let show = function
   | Some x -> "\"" ^ x ^ "\""
@@ -40,10 +39,9 @@ include Printable.SimpleShow (
   )
 
 let of_string x =
-  if get_string_domain () = Unit then
-    None
-  else
-    Some x
+  match get_string_domain () with
+  | Unit -> None
+  | Disjoint | Flat -> Some x
 let to_string x = x
 
 (* only keep part before first null byte *)
@@ -92,10 +90,10 @@ let join x y =
   | _, None -> None
   | Some a, Some b when a = b -> Some a
   | Some a, Some b (* when a <> b *) ->
-    if get_string_domain () = Disjoint then
-      raise Lattice.Uncomparable
-    else
-      None
+    match get_string_domain () with
+    | Disjoint -> raise Lattice.Uncomparable
+    | Flat -> None
+    | Unit -> assert false
 
 let meet x y =
   match x, y with
@@ -103,13 +101,14 @@ let meet x y =
   | a, None -> a
   | Some a, Some b when a = b -> Some a
   | Some a, Some b (* when a <> b *) ->
-    if get_string_domain () = Disjoint then
-      raise Lattice.Uncomparable
-    else
-      raise Lattice.BotValue
+    match get_string_domain () with
+    | Disjoint -> raise Lattice.Uncomparable
+    | Flat -> raise Lattice.BotValue
+    | Unit -> assert false
 
 let repr x =
-  if get_string_domain () = Disjoint then
+  match get_string_domain () with
+  | Disjoint ->
     x (* everything else is kept separate, including strings if not limited *)
-  else
+  | Flat | Unit ->
     None (* all strings together if limited *)

From bf0c28fd0ef83f3202b27e9b7a982dfa2b48b0cf Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 23 Oct 2024 16:48:07 +0300
Subject: [PATCH 04/32] Revert "Work around old LibraryFunctions spawning even
 with sem.unknown_function.spawn disabled"

This reverts commit e5799bcb81dd50bea45bc36657fe0b28a703c95d.
---
 src/analyses/base.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index e429155e4d..cea2c8bcee 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2172,11 +2172,7 @@ struct
         in
         List.filter_map (create_thread ~multiple (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown
       end
-    | _, _ when get_bool "sem.unknown_function.spawn" ->
-      (* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions.
-         But here we consider all non-ThreadCreate functions also unknown, so old-style LibraryFunctions access
-         definitions using `Write would still spawn because they are not truly unknown functions (missing from LibraryFunctions).
-         Need this to not have memmove spawn in SV-COMP. *)
+    | _, _ ->
       let shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = false } args in
       let deep_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = true } args in
       let shallow_flist = collect_invalidate ~deep:false ~ctx ctx.local shallow_args in
@@ -2185,7 +2181,6 @@ struct
       let addrs = List.concat_map AD.to_var_may flist in
       if addrs <> [] then M.debug ~category:Analyzer "Spawning non-unique functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs;
       List.filter_map (create_thread ~multiple:true None None) addrs
-    | _, _ -> []
 
   let assert_fn ctx e refine =
     (* make the state meet the assertion in the rest of the code *)

From 4d4de22cad91068002242a2942bad0c300da772b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 23 Oct 2024 17:05:36 +0300
Subject: [PATCH 05/32] Add option sem.atexit.ignore

---
 src/config/options.schema.json                  | 13 +++++++++++++
 src/util/library/libraryFunctions.ml            |  2 +-
 tests/regression/41-stdlib/08-atexit-no-spawn.c |  2 +-
 3 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 447290b44d..5d87eb51f6 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1544,6 +1544,19 @@
             }
           },
           "additionalProperties": false
+        },
+        "atexit": {
+          "title": "sem.atexit",
+          "type": "object",
+          "properties": {
+            "ignore": {
+              "title": "sem.atexit.ignore",
+              "description": "Ignore atexit callbacks (unsound).",
+              "type": "boolean",
+              "default": false
+            }
+          },
+          "additionalProperties": false
         }
       },
       "additionalProperties": false
diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
index 25a90da2d3..31fcf0510e 100644
--- a/src/util/library/libraryFunctions.ml
+++ b/src/util/library/libraryFunctions.ml
@@ -145,7 +145,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
     ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env });
     ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
-    ("atexit", unknown [drop "function" [s]]);
+    ("atexit", unknown [drop "function" [if_ (fun () -> not (get_bool "sem.atexit.ignore")) s]]);
     ("atoi", unknown [drop "nptr" [r]]);
     ("atol", unknown [drop "nptr" [r]]);
     ("atoll", unknown [drop "nptr" [r]]);
diff --git a/tests/regression/41-stdlib/08-atexit-no-spawn.c b/tests/regression/41-stdlib/08-atexit-no-spawn.c
index 7f25f42183..3bbba82634 100644
--- a/tests/regression/41-stdlib/08-atexit-no-spawn.c
+++ b/tests/regression/41-stdlib/08-atexit-no-spawn.c
@@ -1,4 +1,4 @@
-// PARAM: --disable sem.unknown_function.spawn
+// PARAM: --enable sem.atexit.ignore
 #include <stdlib.h>
 #include <goblint.h>
 

From 6b77fb3298d2d6f716510767d3a6411a91382348 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 23 Oct 2024 17:15:14 +0300
Subject: [PATCH 06/32] Generalize AutoTune.hasFunction predicate

---
 src/autoTune.ml             | 10 ++++++----
 src/util/autoSoundConfig.ml |  7 ++++---
 2 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 0def6021fa..843c977ae2 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -157,7 +157,7 @@ let hasFunction pred =
     Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo var) @@ fun () ->
     if LibraryFunctions.is_special var then
       let desc = LibraryFunctions.find var in
-      GobOption.exists (fun args -> pred (desc.special args)) (functionArgs var)
+      GobOption.exists (fun args -> pred desc args) (functionArgs var)
     else
       false
   in
@@ -169,7 +169,7 @@ let hasFunction pred =
       match unrollType var.vtype with
       | TFun (_, args, _, _) ->
         let args = BatOption.map_default (List.map (fun (x,_,_) -> MyCFG.unknown_exp)) [] args in
-        pred (desc.special args)
+        pred desc args
       | _ -> false
     else
       false
@@ -191,7 +191,8 @@ let enableAnalyses anas =
 
 let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"; "pthreadMutexType"]
 let reduceThreadAnalyses () =
-  let isThreadCreate = function
+  let isThreadCreate (desc: LibraryDesc.t) args =
+    match desc.special args with
     | LibraryDesc.ThreadCreate _ -> true
     | _ -> false
   in
@@ -446,7 +447,8 @@ let wideningOption factors file =
   }
 
 let activateTmpSpecialAnalysis () =
-  let isMathFun = function
+  let isMathFun (desc: LibraryDesc.t) args =
+    match desc.special args with
     | LibraryDesc.Math _ -> true
     | _ -> false
   in
diff --git a/src/util/autoSoundConfig.ml b/src/util/autoSoundConfig.ml
index 7a30bdf5ce..0bb67e768e 100644
--- a/src/util/autoSoundConfig.ml
+++ b/src/util/autoSoundConfig.ml
@@ -12,8 +12,8 @@ let enableSpecAnalyses spec analyses =
   Logs.info "Specification: %s -> enabling soundness analyses \"%s\"" (Svcomp.Specification.to_string [spec]) (String.concat ", " analyses);
   enableAnalyses analyses
 
-let enableOptions options = 
-  let enableOpt option = 
+let enableOptions options =
+  let enableOpt option =
     Logs.info "Setting \"%s\" to true" option;
     set_bool option true
   in
@@ -60,7 +60,8 @@ let enableAnalysesForSpecification () =
 let longjmpAnalyses = ["activeLongjmp"; "activeSetjmp"; "taintPartialContexts"; "modifiedSinceSetjmp"; "poisonVariables"; "expsplit"; "vla"]
 
 let activateLongjmpAnalysesWhenRequired () =
-  let isLongjmp = function
+  let isLongjmp (desc: LibraryDesc.t) args =
+    match desc.special args with
     | LibraryDesc.Longjmp _ -> true
     | _ -> false
   in

From b00c608f70c115bc442d8c355653655541527d37 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 23 Oct 2024 17:19:48 +0300
Subject: [PATCH 07/32] Consider all spawning functions in autotuner (closes
 #1181)

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

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 843c977ae2..f59a10ee8a 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -194,7 +194,7 @@ let reduceThreadAnalyses () =
   let isThreadCreate (desc: LibraryDesc.t) args =
     match desc.special args with
     | LibraryDesc.ThreadCreate _ -> true
-    | _ -> false
+    | _ -> LibraryDesc.Accesses.find_kind desc.accs Spawn args <> []
   in
   let hasThreadCreate = hasFunction isThreadCreate in
   if not @@ hasThreadCreate then (

From 3970a2fde041afba272b4a93e3a7c4a73f05cdca Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 28 Oct 2024 13:48:12 +0200
Subject: [PATCH 08/32] Add regression test for joining main thread

---
 .../regression/51-threadjoins/09-join-main.c  | 23 +++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 tests/regression/51-threadjoins/09-join-main.c

diff --git a/tests/regression/51-threadjoins/09-join-main.c b/tests/regression/51-threadjoins/09-join-main.c
new file mode 100644
index 0000000000..249de594bf
--- /dev/null
+++ b/tests/regression/51-threadjoins/09-join-main.c
@@ -0,0 +1,23 @@
+//PARAM: --set ana.activated[+] threadJoins
+#include <pthread.h>
+
+pthread_t mainid;
+
+int g = 10;
+
+void *t_fun(void *arg) {
+  pthread_join(mainid, NULL);
+  g++; // TODO NORACE
+  return NULL;
+}
+
+
+int main(void) {
+  mainid = pthread_self();
+
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_fun, NULL);
+
+  g++; // TODO NORACE
+  return 0;
+}

From 3d048eb1035479f26854a23402bb2aad0e53fd31 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 28 Oct 2024 13:48:37 +0200
Subject: [PATCH 09/32] Add pthread_self support

---
 src/analyses/base.ml                           | 9 +++++++++
 src/util/library/libraryDesc.ml                | 1 +
 src/util/library/libraryFunctions.ml           | 2 +-
 tests/regression/51-threadjoins/09-join-main.c | 4 ++--
 4 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index cea2c8bcee..e5bcbfede5 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2651,6 +2651,15 @@ struct
     | Unknown, "__goblint_assume_join" ->
       let id = List.hd args in
       Priv.thread_join ~force:true (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) id st
+    | ThreadSelf, _ ->
+      begin match lv, ThreadId.get_current (Analyses.ask_of_ctx ctx) with
+        | Some lv, `Lifted tid ->
+          set ~ctx st (eval_lv ~ctx st lv) (Cilfacade.typeOfLval lv) (Thread (ValueDomain.Threads.singleton tid))
+        | Some lv, _ ->
+          invalidate_ret_lv st
+        | None, _ ->
+          st
+      end
     | Alloca size, _ -> begin
         match lv with
         | Some lv ->
diff --git a/src/util/library/libraryDesc.ml b/src/util/library/libraryDesc.ml
index 80cf86b1e2..6f34de1864 100644
--- a/src/util/library/libraryDesc.ml
+++ b/src/util/library/libraryDesc.ml
@@ -56,6 +56,7 @@ type special =
   | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; multiple: bool }
   | ThreadJoin of { thread: Cil.exp; ret_var: Cil.exp; }
   | ThreadExit of { ret_val: Cil.exp; }
+  | ThreadSelf
   | Globalize of Cil.exp
   | Signal of Cil.exp
   | Broadcast of Cil.exp
diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
index 31fcf0510e..fbcaa4fe60 100644
--- a/src/util/library/libraryFunctions.ml
+++ b/src/util/library/libraryFunctions.ml
@@ -504,7 +504,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_attr_setstacksize", unknown [drop "attr" [w]; drop "stacksize" []]);
     ("pthread_attr_getscope", unknown [drop "attr" [r]; drop "scope" [w]]);
     ("pthread_attr_setscope", unknown [drop "attr" [w]; drop "scope" []]);
-    ("pthread_self", unknown []);
+    ("pthread_self", special [] ThreadSelf);
     ("pthread_sigmask", unknown [drop "how" []; drop "set" [r]; drop "oldset" [w]]);
     ("pthread_setspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []; drop "value" [w_deep]]);
     ("pthread_getspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []]);
diff --git a/tests/regression/51-threadjoins/09-join-main.c b/tests/regression/51-threadjoins/09-join-main.c
index 249de594bf..1d61eedf89 100644
--- a/tests/regression/51-threadjoins/09-join-main.c
+++ b/tests/regression/51-threadjoins/09-join-main.c
@@ -7,7 +7,7 @@ int g = 10;
 
 void *t_fun(void *arg) {
   pthread_join(mainid, NULL);
-  g++; // TODO NORACE
+  g++; // NORACE
   return NULL;
 }
 
@@ -18,6 +18,6 @@ int main(void) {
   pthread_t id2;
   pthread_create(&id2, NULL, t_fun, NULL);
 
-  g++; // TODO NORACE
+  g++; // NORACE
   return 0;
 }

From 01bff20b3fea1bb077c12ba9b0b7d7eba6d27c72 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 28 Oct 2024 14:00:52 +0200
Subject: [PATCH 10/32] Make 51-threadjoins/09-join-main runnable

---
 tests/regression/51-threadjoins/09-join-main.c | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/tests/regression/51-threadjoins/09-join-main.c b/tests/regression/51-threadjoins/09-join-main.c
index 1d61eedf89..196ef8bc00 100644
--- a/tests/regression/51-threadjoins/09-join-main.c
+++ b/tests/regression/51-threadjoins/09-join-main.c
@@ -1,13 +1,16 @@
 //PARAM: --set ana.activated[+] threadJoins
 #include <pthread.h>
+#include <stdio.h>
 
 pthread_t mainid;
 
 int g = 10;
 
 void *t_fun(void *arg) {
-  pthread_join(mainid, NULL);
+  int r = pthread_join(mainid, NULL); // TSan doesn't like this...
+  printf("j: %d\n", r);
   g++; // NORACE
+  printf("t_fun: %d\n", g);
   return NULL;
 }
 
@@ -19,5 +22,8 @@ int main(void) {
   pthread_create(&id2, NULL, t_fun, NULL);
 
   g++; // NORACE
+  printf("main: %d\n", g);
+
+  pthread_exit(NULL); // exit main thread but keep id2 alive, otherwise main returning kills id2
   return 0;
 }

From bdc288e9706d3bfd0ae09785b891bc545ac3225e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 28 Oct 2024 15:27:55 +0200
Subject: [PATCH 11/32] Copy 51-threadjoins/09-join-main for plain thread IDs

---
 .../51-threadjoins/10-join-main-plain.c       | 29 +++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 tests/regression/51-threadjoins/10-join-main-plain.c

diff --git a/tests/regression/51-threadjoins/10-join-main-plain.c b/tests/regression/51-threadjoins/10-join-main-plain.c
new file mode 100644
index 0000000000..8bcb2b3a79
--- /dev/null
+++ b/tests/regression/51-threadjoins/10-join-main-plain.c
@@ -0,0 +1,29 @@
+//PARAM: --set ana.activated[+] threadJoins --set ana.thread.domain plain
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_t mainid;
+
+int g = 10;
+
+void *t_fun(void *arg) {
+  int r = pthread_join(mainid, NULL); // TSan doesn't like this...
+  printf("j: %d\n", r);
+  g++; // RACE (imprecise by plain thread IDs)
+  printf("t_fun: %d\n", g);
+  return NULL;
+}
+
+
+int main(void) {
+  mainid = pthread_self();
+
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_fun, NULL);
+
+  g++; // TODO NORACE
+  printf("main: %d\n", g);
+
+  pthread_exit(NULL); // exit main thread but keep id2 alive, otherwise main returning kills id2
+  return 0;
+}

From 568e97cf331e7b0cd0b7b035dadaa198435867a6 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 28 Oct 2024 15:29:04 +0200
Subject: [PATCH 12/32] Improve plain thread ID is_unique

---
 src/cdomain/value/cdomains/threadIdDomain.ml         | 2 +-
 tests/regression/51-threadjoins/10-join-main-plain.c | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index fff6734f27..290a6b316b 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -86,7 +86,7 @@ struct
     | ({vname; _}, None) -> List.mem vname @@ GobConfig.get_string_list "mainfun"
     | _ -> false
 
-  let is_unique _ = false (* TODO: should this consider main unique? *)
+  let is_unique = is_main
   let may_create _ _ = true
   let is_must_parent _ _ = false
 end
diff --git a/tests/regression/51-threadjoins/10-join-main-plain.c b/tests/regression/51-threadjoins/10-join-main-plain.c
index 8bcb2b3a79..5b2c188bf5 100644
--- a/tests/regression/51-threadjoins/10-join-main-plain.c
+++ b/tests/regression/51-threadjoins/10-join-main-plain.c
@@ -21,7 +21,7 @@ int main(void) {
   pthread_t id2;
   pthread_create(&id2, NULL, t_fun, NULL);
 
-  g++; // TODO NORACE
+  g++; // NORACE
   printf("main: %d\n", g);
 
   pthread_exit(NULL); // exit main thread but keep id2 alive, otherwise main returning kills id2

From 1bb8db120146e371451cd3b1c34bfcf2d44e798b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 30 Oct 2024 15:36:48 +0200
Subject: [PATCH 13/32] Fix plain thread ID is_main unsoundness when
 ana.thread.include-node is disabled

---
 src/cdomain/value/cdomains/threadIdDomain.ml  |  2 +-
 .../11-join-main-plain-no-node.c              | 29 +++++++++++++++++++
 2 files changed, 30 insertions(+), 1 deletion(-)
 create mode 100644 tests/regression/51-threadjoins/11-join-main-plain-no-node.c

diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml
index 290a6b316b..226905ed6f 100644
--- a/src/cdomain/value/cdomains/threadIdDomain.ml
+++ b/src/cdomain/value/cdomains/threadIdDomain.ml
@@ -83,7 +83,7 @@ struct
       (v, None)
 
   let is_main = function
-    | ({vname; _}, None) -> List.mem vname @@ GobConfig.get_string_list "mainfun"
+    | ({vname; _}, None) -> GobConfig.get_bool "ana.thread.include-node" && List.mem vname @@ GobConfig.get_string_list "mainfun"
     | _ -> false
 
   let is_unique = is_main
diff --git a/tests/regression/51-threadjoins/11-join-main-plain-no-node.c b/tests/regression/51-threadjoins/11-join-main-plain-no-node.c
new file mode 100644
index 0000000000..7f235fd1d8
--- /dev/null
+++ b/tests/regression/51-threadjoins/11-join-main-plain-no-node.c
@@ -0,0 +1,29 @@
+//PARAM: --set ana.activated[+] threadJoins --set ana.thread.domain plain --disable ana.thread.include-node
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_t mainid;
+
+int g = 10;
+
+void *t_fun(void *arg) {
+  int r = pthread_join(mainid, NULL); // TSan doesn't like this...
+  printf("j: %d\n", r);
+  g++; // RACE (imprecise by plain thread IDs)
+  printf("t_fun: %d\n", g);
+  return NULL;
+}
+
+
+int main(void) {
+  mainid = pthread_self();
+
+  pthread_t id2;
+  pthread_create(&id2, NULL, t_fun, NULL);
+
+  g++; // RACE (imprecise by plain thread IDs not knowing if main is actual main or spawned by program)
+  printf("main: %d\n", g);
+
+  pthread_exit(NULL); // exit main thread but keep id2 alive, otherwise main returning kills id2
+  return 0;
+}

From 7adeb5a8ac8b45cb01f9649c106606696bb29993 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 31 Oct 2024 18:34:39 +0200
Subject: [PATCH 14/32] Add visitor for finding mallocs/allocs that are not in
 loops

---
 src/autoTune.ml | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index f59a10ee8a..7194d1ece7 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -44,6 +44,26 @@ class functionVisitor(calling, calledBy, argLists, dynamicallyCalled) = object
     DoChildren
 end
 
+exception Found
+class findAllocsNotInLoops = object
+  inherit nopCilVisitor
+
+  method! vstmt stmt =
+    match stmt.skind with
+    | Loop _ -> SkipChildren
+    | _ -> DoChildren
+
+  method! vinst = function
+    | Call (_, Lval (Var f, NoOffset), args,_,_) ->
+      let desc = LibraryFunctions.find f in
+      begin match desc.special args with
+        | Malloc _
+        | Alloca _ -> raise Found
+        | _ -> DoChildren
+      end
+    | _ -> DoChildren
+end
+
 type functionCallMaps = {
   calling: FunctionSet.t FunctionCallMap.t;
   calledBy: (FunctionSet.t * int) FunctionCallMap.t;

From cb16bae9fc8ee6da2f2e07a703ce93eba62e85c1 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 31 Oct 2024 19:47:38 +0200
Subject: [PATCH 15/32] Set ana.malloc.unique_address_count to 1 when alloc is
 found in program for noOverflow tasks

---
 src/autoTune.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 7194d1ece7..1eb9aba5fc 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -257,7 +257,11 @@ let focusOnSpecification (spec: Svcomp.Specification.t) =
     Logs.info "Specification: NoDataRace -> enabling thread analyses \"%s\"" (String.concat ", " notNeccessaryThreadAnalyses);
     enableAnalyses notNeccessaryThreadAnalyses;
   | NoOverflow -> (*We focus on integer analysis*)
-    set_bool "ana.int.def_exc" true
+    set_bool "ana.int.def_exc" true;
+    begin
+      try ignore @@ visitCilFileSameGlobals (new findAllocsNotInLoops) (!Cilfacade.current_file)
+      with Found -> set_int "ana.malloc.unique_address_count" 1;
+    end
   | _ -> ()
 
 let focusOnSpecification () =

From c6a6ee0be729198fd594acf025ffa5b337217c3b Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 31 Oct 2024 19:47:59 +0200
Subject: [PATCH 16/32] Enable autotune.specification

---
 conf/svcomp.json | 1 +
 1 file changed, 1 insertion(+)

diff --git a/conf/svcomp.json b/conf/svcomp.json
index 50136def50..1e05da580c 100644
--- a/conf/svcomp.json
+++ b/conf/svcomp.json
@@ -60,6 +60,7 @@
         "singleThreaded",
         "mallocWrappers",
         "noRecursiveIntervals",
+        "specification",
         "enums",
         "congruence",
         "octagon",

From 5ceb7205dd2e14ed9bf8135c554dda17e090a92d Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 31 Oct 2024 20:11:28 +0200
Subject: [PATCH 17/32] Separate autotune for each category as options

---
 conf/svcomp.json               |  2 +-
 src/autoTune.ml                | 42 ++++++++++++++++++++++++++--------
 src/config/options.schema.json |  8 +++++--
 3 files changed, 40 insertions(+), 12 deletions(-)

diff --git a/conf/svcomp.json b/conf/svcomp.json
index 1e05da580c..c1ccaa4ab3 100644
--- a/conf/svcomp.json
+++ b/conf/svcomp.json
@@ -60,13 +60,13 @@
         "singleThreaded",
         "mallocWrappers",
         "noRecursiveIntervals",
-        "specification",
         "enums",
         "congruence",
         "octagon",
         "wideningThresholds",
         "loopUnrollHeuristic",
         "memsafetySpecification",
+        "noOverflows",
         "termination",
         "tmpSpecialAnalysis"
       ]
diff --git a/src/autoTune.ml b/src/autoTune.ml
index 1eb9aba5fc..c54b84d0e9 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -250,13 +250,25 @@ let focusOnTermination (spec: Svcomp.Specification.t) =
 let focusOnTermination () =
   List.iter focusOnTermination (Svcomp.Specification.of_option ())
 
-let focusOnSpecification (spec: Svcomp.Specification.t) =
+let focusOnReachSafety (spec: Svcomp.Specification.t) = ()
+
+let focusOnReachSafety () =
+  List.iter focusOnReachSafety (Svcomp.Specification.of_option ())
+
+let focusOnConcurrencySafety (spec: Svcomp.Specification.t) =
   match spec with
-  | UnreachCall s -> ()
   | NoDataRace -> (*enable all thread analyses*)
     Logs.info "Specification: NoDataRace -> enabling thread analyses \"%s\"" (String.concat ", " notNeccessaryThreadAnalyses);
     enableAnalyses notNeccessaryThreadAnalyses;
-  | NoOverflow -> (*We focus on integer analysis*)
+  | _ -> ()
+
+let focusOnConcurrencySafety () =
+  List.iter focusOnConcurrencySafety (Svcomp.Specification.of_option ())
+
+let focusOnNoOverflows (spec: Svcomp.Specification.t) =
+  match spec with
+  | NoOverflow ->
+    (*We focus on integer analysis*)
     set_bool "ana.int.def_exc" true;
     begin
       try ignore @@ visitCilFileSameGlobals (new findAllocsNotInLoops) (!Cilfacade.current_file)
@@ -264,8 +276,8 @@ let focusOnSpecification (spec: Svcomp.Specification.t) =
     end
   | _ -> ()
 
-let focusOnSpecification () =
-  List.iter focusOnSpecification (Svcomp.Specification.of_option ())
+let focusOnNoOverflows () =
+  List.iter focusOnNoOverflows (Svcomp.Specification.of_option ())
 
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound
@@ -513,8 +525,14 @@ let isActivated a = get_bool "ana.autotune.enabled" && List.mem a @@ get_string_
 
 let isTerminationTask () = List.mem Svcomp.Specification.Termination (Svcomp.Specification.of_option ())
 
-let specificationIsActivated () =
-  isActivated "specification" && get_string "ana.specification" <> ""
+let specificationReachSafetyIsActivated () =
+  isActivated "reachSafetySpecification"
+
+let specificationConcurrencySafetyIsActivated () =
+  isActivated "concurrencySafetySpecification"
+
+let specificationNoOverflowsIsActivated () =
+  isActivated "noOverflows"
 
 let specificationTerminationIsActivated () =
   isActivated "termination"
@@ -541,8 +559,14 @@ let chooseConfig file =
   if isActivated "mallocWrappers" then
     findMallocWrappers ();
 
-  if specificationIsActivated () then
-    focusOnSpecification ();
+  if specificationReachSafetyIsActivated () then
+    focusOnReachSafety ();
+
+  if specificationConcurrencySafetyIsActivated () then
+    focusOnConcurrencySafety ();
+
+  if specificationNoOverflowsIsActivated () then
+    focusOnNoOverflows ();
 
   if isActivated "enums" && hasEnums file then
     set_bool "ana.int.enums" true;
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 5d87eb51f6..d8a7d3adc7 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -535,7 +535,6 @@
                 "enum": [
                   "congruence",
                   "singleThreaded",
-                  "specification",
                   "mallocWrappers",
                   "noRecursiveIntervals",
                   "enums",
@@ -545,6 +544,9 @@
                   "octagon",
                   "wideningThresholds",
                   "memsafetySpecification",
+                  "reachSafetySpecification",
+                  "concurrencySafetySpecification",
+                  "noOverflows",
                   "termination",
                   "tmpSpecialAnalysis"
                 ]
@@ -552,7 +554,6 @@
               "default": [
                 "congruence",
                 "singleThreaded",
-                "specification",
                 "mallocWrappers",
                 "noRecursiveIntervals",
                 "enums",
@@ -561,6 +562,9 @@
                 "octagon",
                 "wideningThresholds",
                 "memsafetySpecification",
+                "reachSafetySpecification",
+                "concurrencySafetySpecification",
+                "noOverflows",
                 "termination",
                 "tmpSpecialAnalysis"
               ]

From 506fb21001924edb008760da682a4e59bc5283dc Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 31 Oct 2024 20:16:09 +0200
Subject: [PATCH 18/32] Refactor: inline functions

---
 src/autoTune.ml    | 21 +++------------------
 src/goblint.ml     |  2 +-
 src/maingoblint.ml |  2 +-
 3 files changed, 5 insertions(+), 20 deletions(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index c54b84d0e9..af7b9ab478 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -525,21 +525,6 @@ let isActivated a = get_bool "ana.autotune.enabled" && List.mem a @@ get_string_
 
 let isTerminationTask () = List.mem Svcomp.Specification.Termination (Svcomp.Specification.of_option ())
 
-let specificationReachSafetyIsActivated () =
-  isActivated "reachSafetySpecification"
-
-let specificationConcurrencySafetyIsActivated () =
-  isActivated "concurrencySafetySpecification"
-
-let specificationNoOverflowsIsActivated () =
-  isActivated "noOverflows"
-
-let specificationTerminationIsActivated () =
-  isActivated "termination"
-
-let specificationMemSafetyIsActivated () =
-  isActivated "memsafetySpecification"
-
 let chooseConfig file =
   let factors = collectFactors visitCilFileSameGlobals file in
   let fileCompplexity = estimateComplexity factors file in
@@ -559,13 +544,13 @@ let chooseConfig file =
   if isActivated "mallocWrappers" then
     findMallocWrappers ();
 
-  if specificationReachSafetyIsActivated () then
+  if isActivated "reachSafetySpecification" then
     focusOnReachSafety ();
 
-  if specificationConcurrencySafetyIsActivated () then
+  if isActivated "concurrencySafetySpecification" then
     focusOnConcurrencySafety ();
 
-  if specificationNoOverflowsIsActivated () then
+  if isActivated "noOverflows" then
     focusOnNoOverflows ();
 
   if isActivated "enums" && hasEnums file then
diff --git a/src/goblint.ml b/src/goblint.ml
index 6f8f8c20e5..2a0ab3ce0f 100644
--- a/src/goblint.ml
+++ b/src/goblint.ml
@@ -37,7 +37,7 @@ let main () =
     Logs.debug "%s" GobSys.command_line;
     (* When analyzing a termination specification, activate the termination analysis before pre-processing. *)
     if get_string "ana.specification" <> "" then AutoSoundConfig.enableAnalysesForTerminationSpecification ();
-    if AutoTune.specificationTerminationIsActivated () then AutoTune.focusOnTermination ();
+    if AutoTune.isActivated "termination" then AutoTune.focusOnTermination ();
     let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_parse_merge) in
     if get_bool "server.enabled" then (
       let file =
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 95849bce36..cb81ea0b86 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -203,7 +203,7 @@ let handle_options () =
   Sys.set_signal (GobSys.signal_of_string (get_string "dbg.solver-signal")) Signal_ignore; (* Ignore solver-signal before solving (e.g. MyCFG), otherwise exceptions self-signal the default, which crashes instead of printing backtrace. *)
   if get_string "ana.specification" <> "" then
     AutoSoundConfig.enableAnalysesForMemSafetySpecification ();
-  if AutoTune.specificationMemSafetyIsActivated () then
+  if AutoTune.isActivated "memsafetySpecification" then
     AutoTune.focusOnMemSafetySpecification ();
   AfterConfig.run ();
   Cilfacade.init_options ();

From 2508f1ac655401a13c4831ddfc008be72dacd977 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 31 Oct 2024 20:20:28 +0200
Subject: [PATCH 19/32] Refactor: generalize repetitive function definition

---
 src/autoTune.ml | 25 ++++++++-----------------
 1 file changed, 8 insertions(+), 17 deletions(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index af7b9ab478..8dfcc6480e 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -250,22 +250,16 @@ let focusOnTermination (spec: Svcomp.Specification.t) =
 let focusOnTermination () =
   List.iter focusOnTermination (Svcomp.Specification.of_option ())
 
-let focusOnReachSafety (spec: Svcomp.Specification.t) = ()
+let reachSafety (spec: Svcomp.Specification.t) = ()
 
-let focusOnReachSafety () =
-  List.iter focusOnReachSafety (Svcomp.Specification.of_option ())
-
-let focusOnConcurrencySafety (spec: Svcomp.Specification.t) =
+let concurrencySafety (spec: Svcomp.Specification.t) =
   match spec with
   | NoDataRace -> (*enable all thread analyses*)
     Logs.info "Specification: NoDataRace -> enabling thread analyses \"%s\"" (String.concat ", " notNeccessaryThreadAnalyses);
     enableAnalyses notNeccessaryThreadAnalyses;
   | _ -> ()
 
-let focusOnConcurrencySafety () =
-  List.iter focusOnConcurrencySafety (Svcomp.Specification.of_option ())
-
-let focusOnNoOverflows (spec: Svcomp.Specification.t) =
+let noOverflows (spec: Svcomp.Specification.t) =
   match spec with
   | NoOverflow ->
     (*We focus on integer analysis*)
@@ -276,8 +270,8 @@ let focusOnNoOverflows (spec: Svcomp.Specification.t) =
     end
   | _ -> ()
 
-let focusOnNoOverflows () =
-  List.iter focusOnNoOverflows (Svcomp.Specification.of_option ())
+let focusOn (f : SvcompSpec.t -> unit) =
+  List.iter f (Svcomp.Specification.of_option ())
 
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound
@@ -544,14 +538,11 @@ let chooseConfig file =
   if isActivated "mallocWrappers" then
     findMallocWrappers ();
 
-  if isActivated "reachSafetySpecification" then
-    focusOnReachSafety ();
+  if isActivated "reachSafetySpecification" then focusOn reachSafety;
 
-  if isActivated "concurrencySafetySpecification" then
-    focusOnConcurrencySafety ();
+  if isActivated "concurrencySafetySpecification" then focusOn concurrencySafety;
 
-  if isActivated "noOverflows" then
-    focusOnNoOverflows ();
+  if isActivated "noOverflows" then focusOn noOverflows;
 
   if isActivated "enums" && hasEnums file then
     set_bool "ana.int.enums" true;

From 0b6f98174c544631c4a1cc80f47c19ac75e992dd Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 1 Nov 2024 12:45:19 +0200
Subject: [PATCH 20/32] Add semgrep rules for finding exists/forall-like folds

---
 .semgrep/fold.yml | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 .semgrep/fold.yml

diff --git a/.semgrep/fold.yml b/.semgrep/fold.yml
new file mode 100644
index 0000000000..8e4739791f
--- /dev/null
+++ b/.semgrep/fold.yml
@@ -0,0 +1,26 @@
+rules:
+  - id: fold-exists
+    patterns:
+      - pattern-either:
+        - pattern: $D.fold ... false
+        - pattern: $D.fold_left ... false
+        - pattern: $D.fold_right ... false
+        - pattern: fold ... false
+        - pattern: fold_left ... false
+        - pattern: fold_right ... false
+    message: consider replacing fold with exists
+    languages: [ocaml]
+    severity: WARNING
+
+  - id: fold-for_all
+    patterns:
+      - pattern-either:
+        - pattern: $D.fold ... true
+        - pattern: $D.fold_left ... true
+        - pattern: $D.fold_right ... true
+        - pattern: fold ... true
+        - pattern: fold_left ... true
+        - pattern: fold_right ... true
+    message: consider replacing fold with for_all
+    languages: [ocaml]
+    severity: WARNING

From 513662ce92e14b6a8fe25a92c6b47622de858dfb Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 1 Nov 2024 12:55:08 +0200
Subject: [PATCH 21/32] Fix or suppress semgrep fold-exists/for_all warnings

---
 src/analyses/basePriv.ml      | 12 ++++++------
 src/domain/partitionDomain.ml |  6 +++---
 src/incremental/compareCFG.ml |  2 +-
 src/solver/td3.ml             |  2 +-
 src/witness/witness.ml        |  8 ++++----
 5 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 946b8f8cc5..e69757c7a8 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -1040,11 +1040,11 @@ struct
     let s = MustLockset.remove m (current_lockset ask) in
     let t = current_thread ask in
     let side_cpa = CPA.filter (fun x _ ->
-        GWeak.fold (fun s' tm acc ->
+        GWeak.exists (fun s' tm ->
             (* TODO: swap 2^M and T partitioning for lookup by t here first? *)
             let v = ThreadMap.find t tm in
-            (MustLockset.mem m s' && not (VD.is_bot v)) || acc
-          ) (G.weak (getg (V.global x))) false
+            (MustLockset.mem m s' && not (VD.is_bot v))
+          ) (G.weak (getg (V.global x)))
       ) st.cpa
     in
     sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa));
@@ -1098,9 +1098,9 @@ struct
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let s = MustLockset.remove m (current_lockset ask) in
     let side_cpa = CPA.filter (fun x _ ->
-        GWeak.fold (fun s' v acc ->
-            (MustLockset.mem m s' && not (VD.is_bot v)) || acc
-          ) (G.weak (getg (V.global x))) false
+        GWeak.exists (fun s' v ->
+            (MustLockset.mem m s' && not (VD.is_bot v))
+          ) (G.weak (getg (V.global x)))
       ) st.cpa
     in
     sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa));
diff --git a/src/domain/partitionDomain.ml b/src/domain/partitionDomain.ml
index 9675e9bfce..316f4fb705 100644
--- a/src/domain/partitionDomain.ml
+++ b/src/domain/partitionDomain.ml
@@ -31,10 +31,10 @@ struct
   let meet _ _ = failwith "PartitonDomain.Set.meet: unsound"
 
   let collapse (s1:t) (s2:t): bool =
-    let f vf2 res =
-      res || exists (fun vf1 -> S.collapse vf1 vf2) s1
+    let f vf2 =
+      exists (fun vf1 -> S.collapse vf1 vf2) s1
     in
-    fold f s2 false
+    exists f s2
 
   let add e s = join s (singleton e)
 
diff --git a/src/incremental/compareCFG.ml b/src/incremental/compareCFG.ml
index 6c314ef7c9..a663b80833 100644
--- a/src/incremental/compareCFG.ml
+++ b/src/incremental/compareCFG.ml
@@ -131,7 +131,7 @@ let reexamine f1 f2 (same : biDirectionNodeMap) (diffNodes1 : unit NH.t) (module
           false
         end in
     let cond n2 = Node.equal n2 (FunctionEntry f2) || check_all_nodes_in_same (List.map snd (CfgNew.prev n2)) n2 in
-    let forall = NH.fold (fun n2 n1 acc -> acc && cond n2) same.node2to1 true in
+    let forall = NH.fold (fun n2 n1 acc -> acc && cond n2) same.node2to1 true in (* nosemgrep: fold-for_all *) (* cond does side effects *)
     if not forall then repeat () in
   repeat ();
   NH.to_seq same.node1to2, NH.to_seq_keys diffNodes1
diff --git a/src/solver/td3.ml b/src/solver/td3.ml
index c7bec621e3..049dce2a0d 100644
--- a/src/solver/td3.ml
+++ b/src/solver/td3.ml
@@ -289,7 +289,7 @@ module Base =
               destabilize_vs y || b || was_stable && List.mem_cmp S.Var.compare y vs
             else
               true
-          ) w false
+          ) w false (* nosemgrep: fold-exists *) (* does side effects *)
       and solve ?reuse_eq x phase =
         if tracing then trace "sol2" "solve %a, phase: %s, called: %b, stable: %b, wpoint: %b" S.Var.pretty_trace x (show_phase phase) (HM.mem called x) (HM.mem stable x) (HM.mem wpoint x);
         init x;
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 5da46a1011..bb70c3319f 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -342,14 +342,14 @@ struct
     | UnreachCall _ ->
       (* error function name is globally known through Svcomp.task *)
       let is_unreach_call =
-        LHT.fold (fun (n, c) v acc ->
+        LHT.for_all (fun (n, c) v ->
             match n with
             (* FunctionEntry isn't used for extern __VERIFIER_error... *)
             | FunctionEntry f when Svcomp.is_error_function f.svar ->
               let is_dead = Spec.D.is_bot v in
-              acc && is_dead
-            | _ -> acc
-          ) lh true
+              is_dead
+            | _ -> true
+          ) lh
       in
 
       if is_unreach_call then (

From 62cb655ab97c9fe2bf2967ba68af5d6247bb3f8d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 1 Nov 2024 12:56:32 +0200
Subject: [PATCH 22/32] Extend semgrep tracing rule for abbreviated module name

---
 .semgrep/tracing.yml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/.semgrep/tracing.yml b/.semgrep/tracing.yml
index 061b3efa0d..9c7813a7e8 100644
--- a/.semgrep/tracing.yml
+++ b/.semgrep/tracing.yml
@@ -8,8 +8,16 @@ rules:
         - pattern: Messages.tracec
         - pattern: Messages.traceu
         - pattern: Messages.traceli
+        - pattern: M.trace
+        - pattern: M.tracel
+        - pattern: M.tracei
+        - pattern: M.tracec
+        - pattern: M.traceu
+        - pattern: M.traceli
       - pattern-not-inside: if Messages.tracing then ...
       - pattern-not-inside: if Messages.tracing && ... then ...
+      - pattern-not-inside: if M.tracing then ...
+      - pattern-not-inside: if M.tracing && ... then ...
     message: trace functions should only be called if tracing is enabled at compile time
     languages: [ocaml]
     severity: WARNING

From c0d51c321042153900101d7cf92b489cf119e425 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 3 Nov 2024 17:24:42 +0100
Subject: [PATCH 23/32] Fix `thread` for non-unique spawns

---
 src/analyses/threadAnalysis.ml                | 10 +++---
 .../40-threadid/12-multiple-created-only.c    | 26 ++++++++++++++++
 tests/regression/40-threadid/13-no-crash.c    | 31 +++++++++++++++++++
 3 files changed, 61 insertions(+), 6 deletions(-)
 create mode 100644 tests/regression/40-threadid/12-multiple-created-only.c
 create mode 100644 tests/regression/40-threadid/13-no-crash.c

diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index 07f46e915d..a67c26092c 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -95,9 +95,7 @@ struct
   let startstate v = D.bot ()
 
   let threadenter ctx ~multiple lval f args =
-    if multiple then
-      (let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx ctx) in
-       ctx.sideg tid (true, TS.bot (), false));
+    (* ctx is of creator, side-effects to denote non-uniqueness are performed in threadspawn *)
     [D.bot ()]
 
   let threadspawn ctx ~multiple lval f args fctx =
@@ -106,9 +104,9 @@ struct
     let repeated = D.mem tid ctx.local in
     let eff =
       match creator with
-      | `Lifted ctid -> (repeated, TS.singleton ctid, false)
-      | `Top         -> (true,     TS.bot (),         false)
-      | `Bot         -> (false,    TS.bot (),         false)
+      | `Lifted ctid -> (repeated || multiple, TS.singleton ctid, false)
+      | `Top         -> (true, TS.bot (), false)
+      | `Bot         -> (false || multiple, TS.bot (), false)
     in
     ctx.sideg tid eff;
     D.join ctx.local (D.singleton tid)
diff --git a/tests/regression/40-threadid/12-multiple-created-only.c b/tests/regression/40-threadid/12-multiple-created-only.c
new file mode 100644
index 0000000000..e65021caaf
--- /dev/null
+++ b/tests/regression/40-threadid/12-multiple-created-only.c
@@ -0,0 +1,26 @@
+// PARAM: --set ana.activated[+] thread --set ana.activated[+] threadid --set ana.thread.domain plain
+
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+int myglobal2;
+
+void* bla(void *arg) {
+  // This is created multiple times, it should race with itself
+  myglobal = 10; //RACE
+  return NULL;
+}
+
+void* other(void) {
+  // This is created only once, it should not be marked as non-unique
+  unknown(bla);
+  myglobal2 = 30; //NORACE
+}
+
+int main(void) {
+    pthread_t id;
+    pthread_create(&id, NULL, other, NULL);
+
+    return 0;
+}
diff --git a/tests/regression/40-threadid/13-no-crash.c b/tests/regression/40-threadid/13-no-crash.c
new file mode 100644
index 0000000000..c9a6c7d88b
--- /dev/null
+++ b/tests/regression/40-threadid/13-no-crash.c
@@ -0,0 +1,31 @@
+// PARAM: --set ana.context.gas_value 0 --set ana.activated[+] thread --set ana.activated[+] threadid
+
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+int myglobal2;
+
+void *t_flurb(void *arg) {
+  myglobal=40; //RACE
+  return NULL;
+}
+
+void* bla(void *arg) {
+    return NULL;
+}
+
+void *t_fun(void *arg) {
+  unknown(t_flurb); // NOCRASH
+  return NULL;
+}
+
+int main(void) {
+    pthread_t id;
+    pthread_create(&id, NULL, t_fun, NULL);
+    pthread_create(&id, NULL, t_fun, NULL);
+
+    unknown(bla);
+
+    return 0;
+}

From 39d0a8aa8664b9296645a4b69f639179a7224efd Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 4 Nov 2024 10:29:14 +0200
Subject: [PATCH 24/32] Use HM.exists instead of HM.fold in td3 (closes #1618)

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

diff --git a/src/solver/td3.ml b/src/solver/td3.ml
index 049dce2a0d..3cab3cf7f7 100644
--- a/src/solver/td3.ml
+++ b/src/solver/td3.ml
@@ -49,7 +49,7 @@ module Base =
     open SolverBox.Warrow (S.Dom)
     include Generic.SolverStats (S) (HM)
     module VS = Set.Make (S.Var)
-    let exists_key f hm = HM.fold (fun k _ a -> a || f k) hm false
+    let exists_key f hm = HM.exists (fun k _ -> f k) hm
 
     type solver_data = {
       st: (S.Var.t * S.Dom.t) list; (* needed to destabilize start functions if their start state changed because of some changed global initializer *)

From 1bb50df301ddfd63b9a15677c3bf6f9cf5d026ff Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 4 Nov 2024 10:38:13 +0100
Subject: [PATCH 25/32] Use multiple also in bot case

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
---
 src/analyses/threadAnalysis.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index a67c26092c..435e1a6afe 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -106,7 +106,7 @@ struct
       match creator with
       | `Lifted ctid -> (repeated || multiple, TS.singleton ctid, false)
       | `Top         -> (true, TS.bot (), false)
-      | `Bot         -> (false || multiple, TS.bot (), false)
+      | `Bot         -> (multiple, TS.bot (), false)
     in
     ctx.sideg tid eff;
     D.join ctx.local (D.singleton tid)

From eb149f9520a05664bb1d7addd90d6a23f44f5832 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 4 Nov 2024 10:39:24 +0100
Subject: [PATCH 26/32] Move tests

---
 .../29-multiple-created-only.c}                                   | 0
 .../{40-threadid/13-no-crash.c => 10-synch/30-no-crash.c}         | 0
 2 files changed, 0 insertions(+), 0 deletions(-)
 rename tests/regression/{40-threadid/12-multiple-created-only.c => 10-synch/29-multiple-created-only.c} (100%)
 rename tests/regression/{40-threadid/13-no-crash.c => 10-synch/30-no-crash.c} (100%)

diff --git a/tests/regression/40-threadid/12-multiple-created-only.c b/tests/regression/10-synch/29-multiple-created-only.c
similarity index 100%
rename from tests/regression/40-threadid/12-multiple-created-only.c
rename to tests/regression/10-synch/29-multiple-created-only.c
diff --git a/tests/regression/40-threadid/13-no-crash.c b/tests/regression/10-synch/30-no-crash.c
similarity index 100%
rename from tests/regression/40-threadid/13-no-crash.c
rename to tests/regression/10-synch/30-no-crash.c

From 7c4581b400f242bb005e9d329e7594231e156708 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 5 Nov 2024 12:35:34 +0200
Subject: [PATCH 27/32] Remove empty focusOn reachSafety and its (yet)
 pointless option reachSafetySpecification

---
 src/autoTune.ml                | 4 ----
 src/config/options.schema.json | 2 --
 2 files changed, 6 deletions(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 8dfcc6480e..3db3729d0d 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -250,8 +250,6 @@ let focusOnTermination (spec: Svcomp.Specification.t) =
 let focusOnTermination () =
   List.iter focusOnTermination (Svcomp.Specification.of_option ())
 
-let reachSafety (spec: Svcomp.Specification.t) = ()
-
 let concurrencySafety (spec: Svcomp.Specification.t) =
   match spec with
   | NoDataRace -> (*enable all thread analyses*)
@@ -538,8 +536,6 @@ let chooseConfig file =
   if isActivated "mallocWrappers" then
     findMallocWrappers ();
 
-  if isActivated "reachSafetySpecification" then focusOn reachSafety;
-
   if isActivated "concurrencySafetySpecification" then focusOn concurrencySafety;
 
   if isActivated "noOverflows" then focusOn noOverflows;
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index d8a7d3adc7..746b950547 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -544,7 +544,6 @@
                   "octagon",
                   "wideningThresholds",
                   "memsafetySpecification",
-                  "reachSafetySpecification",
                   "concurrencySafetySpecification",
                   "noOverflows",
                   "termination",
@@ -562,7 +561,6 @@
                 "octagon",
                 "wideningThresholds",
                 "memsafetySpecification",
-                "reachSafetySpecification",
                 "concurrencySafetySpecification",
                 "noOverflows",
                 "termination",

From 53f540da9d9d1814622255d08c5342234ffe1861 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 5 Nov 2024 12:36:45 +0200
Subject: [PATCH 28/32] Add autotune 'noOverflows' option

---
 conf/svcomp-validate.json | 1 +
 1 file changed, 1 insertion(+)

diff --git a/conf/svcomp-validate.json b/conf/svcomp-validate.json
index 8e11fee7f5..64564f480f 100644
--- a/conf/svcomp-validate.json
+++ b/conf/svcomp-validate.json
@@ -67,6 +67,7 @@
         "wideningThresholds",
         "loopUnrollHeuristic",
         "memsafetySpecification",
+        "noOverflows",
         "termination",
         "tmpSpecialAnalysis"
       ]

From 4e7bfaeb472c4e60c4d84bb8ab7258297672f810 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 5 Nov 2024 12:47:45 +0200
Subject: [PATCH 29/32] Detect mallocs in loops instead of detecting mallocs
 outside of loops

---
 src/autoTune.ml | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 3db3729d0d..56fdfcca25 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -45,12 +45,14 @@ class functionVisitor(calling, calledBy, argLists, dynamicallyCalled) = object
 end
 
 exception Found
-class findAllocsNotInLoops = object
+class findAllocsInLoops = object
   inherit nopCilVisitor
 
+  val mutable inloop = false
+
   method! vstmt stmt =
     match stmt.skind with
-    | Loop _ -> SkipChildren
+    | Loop _ -> inloop <- true; DoChildren
     | _ -> DoChildren
 
   method! vinst = function
@@ -58,7 +60,7 @@ class findAllocsNotInLoops = object
       let desc = LibraryFunctions.find f in
       begin match desc.special args with
         | Malloc _
-        | Alloca _ -> raise Found
+        | Alloca _ when inloop -> raise Found
         | _ -> DoChildren
       end
     | _ -> DoChildren
@@ -263,8 +265,10 @@ let noOverflows (spec: Svcomp.Specification.t) =
     (*We focus on integer analysis*)
     set_bool "ana.int.def_exc" true;
     begin
-      try ignore @@ visitCilFileSameGlobals (new findAllocsNotInLoops) (!Cilfacade.current_file)
-      with Found -> set_int "ana.malloc.unique_address_count" 1;
+      try
+        ignore @@ visitCilFileSameGlobals (new findAllocsInLoops) (!Cilfacade.current_file);
+        set_int "ana.malloc.unique_address_count" 1
+      with Found -> set_int "ana.malloc.unique_address_count" 0;
     end
   | _ -> ()
 

From fa31b55e85b54355b0d61c0c4f46272527ec4ea2 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 5 Nov 2024 15:44:46 +0200
Subject: [PATCH 30/32] Reset inloop after processing children

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

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 56fdfcca25..cae6c62c68 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -51,8 +51,13 @@ class findAllocsInLoops = object
   val mutable inloop = false
 
   method! vstmt stmt =
+    let outOfLoop stmt =
+      match stmt.skind with
+      | Loop _ -> inloop <- false; stmt
+      | _ -> stmt
+    in
     match stmt.skind with
-    | Loop _ -> inloop <- true; DoChildren
+    | Loop _ -> inloop <- true; ChangeDoChildrenPost(stmt, outOfLoop)
     | _ -> DoChildren
 
   method! vinst = function

From 9f7ef77000ef2a86e24c060c767f19ea2840e121 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Wed, 6 Nov 2024 20:13:37 +0200
Subject: [PATCH 31/32] Add backtrace marker around LibraryFunctions special
 call

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

diff --git a/src/autoTune.ml b/src/autoTune.ml
index cae6c62c68..3277291823 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -62,6 +62,7 @@ class findAllocsInLoops = object
 
   method! vinst = function
     | Call (_, Lval (Var f, NoOffset), args,_,_) ->
+      Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo f) ~finally:Fun.id @@ fun () ->
       let desc = LibraryFunctions.find f in
       begin match desc.special args with
         | Malloc _

From 72bf7d6e7815c27acee1d8b7feedadd8109baff6 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 7 Nov 2024 10:14:18 +0200
Subject: [PATCH 32/32] Add is_special check to AutoTune.findAllocsInLoops

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

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 3277291823..05f651ee62 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -61,7 +61,7 @@ class findAllocsInLoops = object
     | _ -> DoChildren
 
   method! vinst = function
-    | Call (_, Lval (Var f, NoOffset), args,_,_) ->
+    | Call (_, Lval (Var f, NoOffset), args,_,_) when LibraryFunctions.is_special f ->
       Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo f) ~finally:Fun.id @@ fun () ->
       let desc = LibraryFunctions.find f in
       begin match desc.special args with