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 1/2] 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 2/2] 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 (