Merge pull request #1667 from goblint/auto-disable-race-analyses

Disable race analyses for other ConcurrencySafety properties

conf/svcomp-ghost.json

@@ -81,7 +81,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

conf/svcomp-validate.json

@@ -59,7 +59,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

conf/svcomp.json

@@ -58,7 +58,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

conf/svcomp23.json

@@ -63,7 +63,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

conf/svcomp24-validate.json

@@ -79,7 +79,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

conf/svcomp24.json

@@ -78,7 +78,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

conf/svcomp25-validate.json

@@ -59,7 +59,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

conf/svcomp25.json

@@ -58,7 +58,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

conf/svcomp2var.json

@@ -78,7 +78,7 @@
     "autotune": {
       "enabled": true,
       "activated": [
-        "singleThreaded",
+        "reduceAnalyses",
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",

src/autoTune.ml

@@ -206,29 +206,31 @@ let hasFunction pred =
   calls.calledBy |> FunctionCallMap.exists (fun var _ -> relevant_static var) ||
   calls.dynamicallyCalled |> FunctionSet.exists relevant_dynamic
 
-let disableAnalyses anas =
-  List.iter (GobConfig.set_auto "ana.activated[-]") anas
+let disableAnalyses reason analyses =
+  Logs.info "%s -> disabling analyses: \"%s\"" reason (String.concat ", " analyses);
+  List.iter (GobConfig.set_auto "ana.activated[-]") analyses
 
-let enableAnalyses anas =
-  List.iter (GobConfig.set_auto "ana.activated[+]") anas
+let enableAnalyses reason description analyses =
+  Logs.info "%s -> enabling %s: \"%s\"" reason description (String.concat ", " analyses);
+  List.iter (GobConfig.set_auto "ana.activated[+]") analyses
 
 (*If only one thread is used in the program, we can disable most thread analyses*)
 (*The exceptions are analyses that are depended on by others: base -> mutex -> mutexEvents, access; termination -> threadflag *)
 (*escape is also still enabled, because otherwise we get a warning*)
 (*does not consider dynamic calls!*)
+let notNeccessaryRaceAnalyses = ["race"; "symb_locks"; "region"]
+let notNeccessaryThreadAnalyses = notNeccessaryRaceAnalyses @ ["deadlock"; "maylocks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "pthreadMutexType"]
 
-let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"; "pthreadMutexType"]
-let reduceThreadAnalyses () =
+let hasSpec spec = List.mem spec (Svcomp.Specification.of_option ())
+
+let reduceAnalyses () =
   let isThreadCreate (desc: LibraryDesc.t) args =
     match desc.special args with
     | LibraryDesc.ThreadCreate _ -> true
     | _ -> LibraryDesc.Accesses.find_kind desc.accs Spawn args <> []
   in
   let hasThreadCreate = hasFunction isThreadCreate in
-  if not @@ hasThreadCreate then (
-    Logs.info "no thread creation -> disabling thread analyses \"%s\"" (String.concat ", " notNeccessaryThreadAnalyses);
-    disableAnalyses notNeccessaryThreadAnalyses;
-  )
+  if not hasThreadCreate then disableAnalyses "no thread creation" notNeccessaryThreadAnalyses
 
 let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) =
   match spec with
@@ -247,8 +249,7 @@ let focusOnTermination (spec: Svcomp.Specification.t) =
   match spec with
   | Termination ->
     let terminationAnas = ["threadflag"; "apron"] in
-    Logs.info "Specification: Termination -> enabling termination analyses \"%s\"" (String.concat ", " terminationAnas);
-    enableAnalyses terminationAnas;
+    enableAnalyses "Specification: Termination" "termination analyses" terminationAnas;
     set_string "sem.int.signed_overflow" "assume_none";
     set_bool "ana.int.interval" true;
     set_string "ana.apron.domain" "polyhedra"; (* TODO: Needed? *)
@@ -258,16 +259,16 @@ let focusOnTermination (spec: Svcomp.Specification.t) =
 let focusOnTermination () =
   List.iter focusOnTermination (Svcomp.Specification.of_option ())
 
-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 () =
+  if hasSpec SvcompSpec.NoDataRace then
+    (*enable all thread analyses*)
+    (* TODO: what's the exact relation between thread analyses enabled in conf, the ones we disable in reduceAnalyses and the ones we enable here? *)
+    enableAnalyses "Specification: NoDataRace" "thread analyses" notNeccessaryThreadAnalyses
+  else
+    disableAnalyses "NoDataRace property is not in spec" notNeccessaryRaceAnalyses
 
-let noOverflows (spec: Svcomp.Specification.t) =
-  match spec with
-  | NoOverflow ->
+let focusOnNoOverflows () =
+  if hasSpec SvcompSpec.NoOverflow then (
     (*We focus on integer analysis*)
     set_bool "ana.int.def_exc" true;
     begin
@@ -276,10 +277,7 @@ let noOverflows (spec: Svcomp.Specification.t) =
         set_int "ana.malloc.unique_address_count" 1
       with Found -> set_int "ana.malloc.unique_address_count" 0;
     end
-  | _ -> ()
-
-let focusOn (f : SvcompSpec.t -> unit) =
-  List.iter f (Svcomp.Specification.of_option ())
+  )
 
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound
@@ -492,8 +490,7 @@ let activateTmpSpecialAnalysis () =
   in
   let hasMathFunctions = hasFunction isMathFun in
   if hasMathFunctions then (
-    Logs.info "math function -> enabling tmpSpecial analysis and floating-point domain";
-    enableAnalyses ["tmpSpecial"];
+    enableAnalyses "Math function" "tmpSpecial analysis and floating-point domain" ["tmpSpecial"];
     set_bool "ana.float.interval" true;
   )
 
@@ -546,15 +543,17 @@ let chooseConfig file =
   if isActivated "mallocWrappers" then
     findMallocWrappers ();
 
-  if isActivated "concurrencySafetySpecification" then focusOn concurrencySafety;
+  if isActivated "concurrencySafetySpecification" then
+    focusOnConcurrencySafety ();
 
-  if isActivated "noOverflows" then focusOn noOverflows;
+  if isActivated "noOverflows" then
+    focusOnNoOverflows ();
 
   if isActivated "enums" && hasEnums file then
     set_bool "ana.int.enums" true;
 
-  if isActivated "singleThreaded" then
-    reduceThreadAnalyses ();
+  if isActivated "reduceAnalyses" then
+    reduceAnalyses ();
 
   if isActivated "arrayDomain" then
     selectArrayDomains file;

src/config/options.schema.json

@@ -541,7 +541,7 @@
                 "type": "string",
                 "enum": [
                   "congruence",
-                  "singleThreaded",
+                  "reduceAnalyses",
                   "mallocWrappers",
                   "noRecursiveIntervals",
                   "enums",
@@ -559,7 +559,7 @@
               },
               "default": [
                 "congruence",
-                "singleThreaded",
+                "reduceAnalyses",
                 "mallocWrappers",
                 "noRecursiveIntervals",
                 "enums",

src/util/autoSoundConfig.ml

@@ -9,8 +9,7 @@ open GobConfig
 open AutoTune
 
 let enableSpecAnalyses spec analyses =
-  Logs.info "Specification: %s -> enabling soundness analyses \"%s\"" (Svcomp.Specification.to_string [spec]) (String.concat ", " analyses);
-  enableAnalyses analyses
+  enableAnalyses ("Specification: " ^ (Svcomp.Specification.to_string [spec])) "soundness analyses" analyses
 
 let enableOptions options =
   let enableOpt option =
@@ -65,7 +64,5 @@ let activateLongjmpAnalysesWhenRequired () =
     | LibraryDesc.Longjmp _ -> true
     | _ -> false
   in
-  if hasFunction isLongjmp  then (
-    Logs.info "longjmp -> enabling longjmp analyses \"%s\"" (String.concat ", " longjmpAnalyses);
-    enableAnalyses longjmpAnalyses;
-  )
+  if hasFunction isLongjmp then
+    enableAnalyses "Longjmp" "longjmp analyses" longjmpAnalyses;