diff --git a/conf/svcomp-ghost.json b/conf/svcomp-ghost.json index d1b4171b2b..43fe4a7a3b 100644 --- a/conf/svcomp-ghost.json +++ b/conf/svcomp-ghost.json @@ -81,7 +81,7 @@ "autotune": { "enabled": true, "activated": [ - "singleThreaded", + "reduceAnalyses", "mallocWrappers", "noRecursiveIntervals", "enums", diff --git a/conf/svcomp-validate.json b/conf/svcomp-validate.json index bec171f1e8..40642e6248 100644 --- a/conf/svcomp-validate.json +++ b/conf/svcomp-validate.json @@ -59,7 +59,7 @@ "autotune": { "enabled": true, "activated": [ - "singleThreaded", + "reduceAnalyses", "mallocWrappers", "noRecursiveIntervals", "enums", diff --git a/conf/svcomp.json b/conf/svcomp.json index dedc393ba1..27203164fe 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -58,7 +58,7 @@ "autotune": { "enabled": true, "activated": [ - "singleThreaded", + "reduceAnalyses", "mallocWrappers", "noRecursiveIntervals", "enums", diff --git a/conf/svcomp23.json b/conf/svcomp23.json index af584f1593..d9afee363c 100644 --- a/conf/svcomp23.json +++ b/conf/svcomp23.json @@ -63,7 +63,7 @@ "autotune": { "enabled": true, "activated": [ - "singleThreaded", + "reduceAnalyses", "mallocWrappers", "noRecursiveIntervals", "enums", diff --git a/conf/svcomp24-validate.json b/conf/svcomp24-validate.json index d83b1767a4..b6e89b5d7e 100644 --- a/conf/svcomp24-validate.json +++ b/conf/svcomp24-validate.json @@ -79,7 +79,7 @@ "autotune": { "enabled": true, "activated": [ - "singleThreaded", + "reduceAnalyses", "mallocWrappers", "noRecursiveIntervals", "enums", diff --git a/conf/svcomp24.json b/conf/svcomp24.json index 1c60f84920..56c70edea3 100644 --- a/conf/svcomp24.json +++ b/conf/svcomp24.json @@ -78,7 +78,7 @@ "autotune": { "enabled": true, "activated": [ - "singleThreaded", + "reduceAnalyses", "mallocWrappers", "noRecursiveIntervals", "enums", diff --git a/conf/svcomp25-validate.json b/conf/svcomp25-validate.json index bec171f1e8..40642e6248 100644 --- a/conf/svcomp25-validate.json +++ b/conf/svcomp25-validate.json @@ -59,7 +59,7 @@ "autotune": { "enabled": true, "activated": [ - "singleThreaded", + "reduceAnalyses", "mallocWrappers", "noRecursiveIntervals", "enums", diff --git a/conf/svcomp25.json b/conf/svcomp25.json index dedc393ba1..27203164fe 100644 --- a/conf/svcomp25.json +++ b/conf/svcomp25.json @@ -58,7 +58,7 @@ "autotune": { "enabled": true, "activated": [ - "singleThreaded", + "reduceAnalyses", "mallocWrappers", "noRecursiveIntervals", "enums", diff --git a/conf/svcomp2var.json b/conf/svcomp2var.json index 7df6a3579c..2c590e88da 100644 --- a/conf/svcomp2var.json +++ b/conf/svcomp2var.json @@ -78,7 +78,7 @@ "autotune": { "enabled": true, "activated": [ - "singleThreaded", + "reduceAnalyses", "mallocWrappers", "noRecursiveIntervals", "enums", diff --git a/src/autoTune.ml b/src/autoTune.ml index 7313d95881..ed5b8a59a0 100644 --- a/src/autoTune.ml +++ b/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; diff --git a/src/config/options.schema.json b/src/config/options.schema.json index ce0f398bee..7cf66cee26 100644 --- a/src/config/options.schema.json +++ b/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", diff --git a/src/util/autoSoundConfig.ml b/src/util/autoSoundConfig.ml index 0bb67e768e..6fcb7003df 100644 --- a/src/util/autoSoundConfig.ml +++ b/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;