Merge pull request #1604 from goblint/issue-1181

Consider all spawning functions in autotuner
goblint · Oct 24, 2024 · 0a85a53 · 0a85a53
2 parents cdfb4a2 + b00c608
commit 0a85a53
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 8 deletions.
diff --git 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,9 +191,10 @@ 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
+    | _ -> LibraryDesc.Accesses.find_kind desc.accs Spawn args <> []
   in
   let hasThreadCreate = hasFunction isThreadCreate in
   if not @@ hasThreadCreate then (
@@ -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
@@ -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