From d97fda14f9303d9fdcf4566a07c2f1a057f3e330 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 30 Jan 2025 19:44:03 +0200 Subject: [PATCH 01/12] Disable race analyses for other ConcurrencySafety properties in autotuner --- src/autoTune.ml | 16 ++++++++++------ src/witness/svcompSpec.ml | 12 ++++++++++++ 2 files changed, 22 insertions(+), 6 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 7313d95881..7e13d7cb3e 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -218,17 +218,21 @@ let enableAnalyses anas = (*does not consider dynamic calls!*) let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"; "pthreadMutexType"] -let reduceThreadAnalyses () = +let notNeccessaryRaceAnalyses = ["race"; "symb_locks"; "region"] +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; - ) + let hasDataRaceSpec = List.exists (SvcompSpec.equals SvcompSpec.NoDataRace) (Svcomp.Specification.of_option ()) in + let disable reason analyses = + Logs.info "%s -> disabling analyses \"%s\"" reason (String.concat ", " analyses); + disableAnalyses analyses + in + if not hasThreadCreate then disable "no thread creation" notNeccessaryThreadAnalyses; + if not hasDataRaceSpec then disable "no data race property in spec" notNeccessaryRaceAnalyses let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) = match spec with @@ -554,7 +558,7 @@ let chooseConfig file = set_bool "ana.int.enums" true; if isActivated "singleThreaded" then - reduceThreadAnalyses (); + reduceAnalyses (); if isActivated "arrayDomain" then selectArrayDomains file; diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml index 3a41cb250d..4cf778148c 100644 --- a/src/witness/svcompSpec.ml +++ b/src/witness/svcompSpec.ml @@ -97,3 +97,15 @@ let to_string spec = let to_string spec = String.concat "\n" (List.map to_string spec) + +let equals spec1 spec2 = + match spec1, spec2 with + | UnreachCall f1, UnreachCall f2 -> String.equal f1 f2 + | NoDataRace, NoDataRace + | NoOverflow, NoOverflow + | Termination, Termination + | ValidFree, ValidFree + | ValidDeref, ValidDeref + | ValidMemtrack, ValidMemtrack + | ValidMemcleanup, ValidMemcleanup -> true + | _, _ -> false From db21e8a74af70e0652ca573b2c83bd1ae5344e47 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 30 Jan 2025 19:45:21 +0200 Subject: [PATCH 02/12] =?UTF-8?q?Rename=20autotune=20option=20`singleThrea?= =?UTF-8?q?ded`=20=E2=86=92=20`reduceAnalyses`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/autoTune.ml | 2 +- src/config/options.schema.json | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 7e13d7cb3e..75bd8b4662 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -557,7 +557,7 @@ let chooseConfig file = if isActivated "enums" && hasEnums file then set_bool "ana.int.enums" true; - if isActivated "singleThreaded" then + if isActivated "reduceAnalyses" then reduceAnalyses (); if isActivated "arrayDomain" then diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 39c863ad49..ddbbfae96a 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -534,7 +534,7 @@ "type": "string", "enum": [ "congruence", - "singleThreaded", + "reduceAnalyses", "mallocWrappers", "noRecursiveIntervals", "enums", @@ -552,7 +552,7 @@ }, "default": [ "congruence", - "singleThreaded", + "reduceAnalyses", "mallocWrappers", "noRecursiveIntervals", "enums", From 99738705aa1a2b64e8c8887efb70dd183c6b3ae3 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 30 Jan 2025 19:45:44 +0200 Subject: [PATCH 03/12] Add conf for SV-COMP 2026 --- conf/svcomp26.json | 119 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 119 insertions(+) create mode 100644 conf/svcomp26.json diff --git a/conf/svcomp26.json b/conf/svcomp26.json new file mode 100644 index 0000000000..2ce2db822f --- /dev/null +++ b/conf/svcomp26.json @@ -0,0 +1,119 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "reduceAnalyses", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } + } + \ No newline at end of file From d8717b7f0f3a6b755ce3e63f1e41046405073814 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 30 Jan 2025 23:48:00 +0200 Subject: [PATCH 04/12] Only disable race analyses if the task is not single-threaded to begin with --- src/autoTune.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 75bd8b4662..0c653ee8c4 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -231,8 +231,8 @@ let reduceAnalyses () = Logs.info "%s -> disabling analyses \"%s\"" reason (String.concat ", " analyses); disableAnalyses analyses in - if not hasThreadCreate then disable "no thread creation" notNeccessaryThreadAnalyses; - if not hasDataRaceSpec then disable "no data race property in spec" notNeccessaryRaceAnalyses + if not hasThreadCreate then disable "no thread creation" notNeccessaryThreadAnalyses + else if not hasDataRaceSpec then disable "no data race property in spec" notNeccessaryRaceAnalyses let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) = match spec with From 6fb51c440fe49096264d6904bcd715ca0a62ca9f Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 31 Jan 2025 00:01:01 +0200 Subject: [PATCH 05/12] Update previous configurations --- conf/svcomp-ghost.json | 2 +- conf/svcomp-validate.json | 2 +- conf/svcomp.json | 2 +- conf/svcomp23.json | 2 +- conf/svcomp24-validate.json | 2 +- conf/svcomp24.json | 2 +- conf/svcomp25-validate.json | 2 +- conf/svcomp25.json | 2 +- conf/svcomp2var.json | 2 +- 9 files changed, 9 insertions(+), 9 deletions(-) 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", From adc71bc328175774bed81fc144e92005517e88fb Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 31 Jan 2025 12:00:53 +0200 Subject: [PATCH 06/12] Revert "Add conf for SV-COMP 2026" This reverts commit 99738705aa1a2b64e8c8887efb70dd183c6b3ae3. --- conf/svcomp26.json | 119 --------------------------------------------- 1 file changed, 119 deletions(-) delete mode 100644 conf/svcomp26.json diff --git a/conf/svcomp26.json b/conf/svcomp26.json deleted file mode 100644 index 2ce2db822f..0000000000 --- a/conf/svcomp26.json +++ /dev/null @@ -1,119 +0,0 @@ -{ - "ana": { - "sv-comp": { - "enabled": true, - "functions": true - }, - "int": { - "def_exc": true, - "enums": false, - "interval": true - }, - "float": { - "interval": true, - "evaluate_math_functions": true - }, - "activated": [ - "base", - "threadid", - "threadflag", - "threadreturn", - "mallocWrapper", - "mutexEvents", - "mutex", - "access", - "race", - "escape", - "expRelation", - "mhp", - "assert", - "var_eq", - "symb_locks", - "region", - "thread", - "threadJoins", - "abortUnless" - ], - "path_sens": [ - "mutex", - "malloc_null", - "uninit", - "expsplit", - "activeSetjmp", - "memLeak", - "threadflag" - ], - "context": { - "widen": false - }, - "base": { - "arrays": { - "domain": "partitioned" - } - }, - "race": { - "free": false, - "call": false - }, - "autotune": { - "enabled": true, - "activated": [ - "reduceAnalyses", - "mallocWrappers", - "noRecursiveIntervals", - "enums", - "congruence", - "octagon", - "wideningThresholds", - "loopUnrollHeuristic", - "memsafetySpecification", - "noOverflows", - "termination", - "tmpSpecialAnalysis" - ] - } - }, - "exp": { - "region-offsets": true - }, - "solver": "td3", - "sem": { - "unknown_function": { - "spawn": false - }, - "int": { - "signed_overflow": "assume_none" - }, - "null-pointer": { - "dereference": "assume_none" - } - }, - "witness": { - "graphml": { - "enabled": true, - "id": "enumerate", - "unknown": false - }, - "yaml": { - "enabled": true, - "format-version": "2.0", - "entry-types": [ - "invariant_set" - ], - "invariant-types": [ - "loop_invariant" - ] - }, - "invariant": { - "loop-head": true, - "after-lock": false, - "other": false, - "accessed": false, - "exact": true - } - }, - "pre": { - "enabled": false - } - } - \ No newline at end of file From 0035350bdd4c31f29f93ddcb62481c76b527734f Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 31 Jan 2025 12:07:33 +0200 Subject: [PATCH 07/12] Use List.mem instead of List.exists --- src/autoTune.ml | 2 +- src/witness/svcompSpec.ml | 12 ------------ 2 files changed, 1 insertion(+), 13 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 0c653ee8c4..95d198878d 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -226,7 +226,7 @@ let reduceAnalyses () = | _ -> LibraryDesc.Accesses.find_kind desc.accs Spawn args <> [] in let hasThreadCreate = hasFunction isThreadCreate in - let hasDataRaceSpec = List.exists (SvcompSpec.equals SvcompSpec.NoDataRace) (Svcomp.Specification.of_option ()) in + let hasDataRaceSpec = List.mem SvcompSpec.NoDataRace (Svcomp.Specification.of_option ()) in let disable reason analyses = Logs.info "%s -> disabling analyses \"%s\"" reason (String.concat ", " analyses); disableAnalyses analyses diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml index 4cf778148c..3a41cb250d 100644 --- a/src/witness/svcompSpec.ml +++ b/src/witness/svcompSpec.ml @@ -97,15 +97,3 @@ let to_string spec = let to_string spec = String.concat "\n" (List.map to_string spec) - -let equals spec1 spec2 = - match spec1, spec2 with - | UnreachCall f1, UnreachCall f2 -> String.equal f1 f2 - | NoDataRace, NoDataRace - | NoOverflow, NoOverflow - | Termination, Termination - | ValidFree, ValidFree - | ValidDeref, ValidDeref - | ValidMemtrack, ValidMemtrack - | ValidMemcleanup, ValidMemcleanup -> true - | _, _ -> false From 786cd7eb7ec62b99c1c49107206aeba76c232ca7 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Mon, 10 Feb 2025 17:22:37 +0200 Subject: [PATCH 08/12] Construct `notNeccessaryThreadAnalyses` through `notNeccessaryRaceAnalyses` --- src/autoTune.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 95d198878d..dd6be86696 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -216,9 +216,8 @@ let enableAnalyses anas = (*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 notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"; "pthreadMutexType"] let notNeccessaryRaceAnalyses = ["race"; "symb_locks"; "region"] +let notNeccessaryThreadAnalyses = notNeccessaryRaceAnalyses @ ["deadlock"; "maylocks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "pthreadMutexType"] let reduceAnalyses () = let isThreadCreate (desc: LibraryDesc.t) args = match desc.special args with From 78ab3ede5faa417727848534e6abae35ca7e41f6 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Mon, 10 Feb 2025 22:33:31 +0200 Subject: [PATCH 09/12] Move disabling data race analyses for non-NoDataRace prop tasks to focusOnConcurrencySafety --- src/autoTune.ml | 31 ++++++++++++++++--------------- 1 file changed, 16 insertions(+), 15 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index dd6be86696..e940643eb6 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -206,8 +206,9 @@ 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 @@ -218,6 +219,7 @@ let enableAnalyses anas = (*does not consider dynamic calls!*) let notNeccessaryRaceAnalyses = ["race"; "symb_locks"; "region"] let notNeccessaryThreadAnalyses = notNeccessaryRaceAnalyses @ ["deadlock"; "maylocks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "pthreadMutexType"] + let reduceAnalyses () = let isThreadCreate (desc: LibraryDesc.t) args = match desc.special args with @@ -225,13 +227,7 @@ let reduceAnalyses () = | _ -> LibraryDesc.Accesses.find_kind desc.accs Spawn args <> [] in let hasThreadCreate = hasFunction isThreadCreate in - let hasDataRaceSpec = List.mem SvcompSpec.NoDataRace (Svcomp.Specification.of_option ()) in - let disable reason analyses = - Logs.info "%s -> disabling analyses \"%s\"" reason (String.concat ", " analyses); - disableAnalyses analyses - in - if not hasThreadCreate then disable "no thread creation" notNeccessaryThreadAnalyses - else if not hasDataRaceSpec then disable "no data race property in spec" notNeccessaryRaceAnalyses + if not hasThreadCreate then disableAnalyses "no thread creation" notNeccessaryThreadAnalyses let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) = match spec with @@ -261,12 +257,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*) +let focusOnConcurrencySafety () = + let hasDataRaceSpec = List.mem SvcompSpec.NoDataRace (Svcomp.Specification.of_option ()) in + if hasDataRaceSpec 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? *) Logs.info "Specification: NoDataRace -> enabling thread analyses \"%s\"" (String.concat ", " notNeccessaryThreadAnalyses); - enableAnalyses notNeccessaryThreadAnalyses; - | _ -> () + enableAnalyses notNeccessaryThreadAnalyses + ) + else + disableAnalyses "NoDataRace property is not in spec" notNeccessaryRaceAnalyses let noOverflows (spec: Svcomp.Specification.t) = match spec with @@ -549,7 +549,8 @@ 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; From d6b9ee76add892a63d4a96a8e28bf58ac28f9222 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Mon, 10 Feb 2025 22:50:24 +0200 Subject: [PATCH 10/12] Refactor logging info about enabling analyses into enableAnalyses function --- src/autoTune.ml | 19 ++++++++----------- src/util/autoSoundConfig.ml | 9 +++------ 2 files changed, 11 insertions(+), 17 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index e940643eb6..dce028086b 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -207,11 +207,12 @@ let hasFunction pred = calls.dynamicallyCalled |> FunctionSet.exists relevant_dynamic let disableAnalyses reason analyses = - Logs.info "%s -> disabling analyses \"%s\"" reason (String.concat ", " 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 *) @@ -246,8 +247,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? *) @@ -259,12 +259,10 @@ let focusOnTermination () = let focusOnConcurrencySafety () = let hasDataRaceSpec = List.mem SvcompSpec.NoDataRace (Svcomp.Specification.of_option ()) in - if hasDataRaceSpec then ( + if hasDataRaceSpec 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? *) - Logs.info "Specification: NoDataRace -> enabling thread analyses \"%s\"" (String.concat ", " notNeccessaryThreadAnalyses); - enableAnalyses notNeccessaryThreadAnalyses - ) + enableAnalyses "Specification: NoDataRace" "thread analyses" notNeccessaryThreadAnalyses else disableAnalyses "NoDataRace property is not in spec" notNeccessaryRaceAnalyses @@ -495,8 +493,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; ) diff --git a/src/util/autoSoundConfig.ml b/src/util/autoSoundConfig.ml index 0bb67e768e..6875df9bae 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" longjmpAnalyses; From 3fca576c2bf8cbe9ba547f1ed83843a941a53e81 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Mon, 10 Feb 2025 22:55:28 +0200 Subject: [PATCH 11/12] Use List.mem when looking for one specific element in list instead of iterating over the whole list --- src/autoTune.ml | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index dce028086b..ed5b8a59a0 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -221,6 +221,8 @@ let enableAnalyses reason description analyses = let notNeccessaryRaceAnalyses = ["race"; "symb_locks"; "region"] let notNeccessaryThreadAnalyses = notNeccessaryRaceAnalyses @ ["deadlock"; "maylocks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "pthreadMutexType"] +let hasSpec spec = List.mem spec (Svcomp.Specification.of_option ()) + let reduceAnalyses () = let isThreadCreate (desc: LibraryDesc.t) args = match desc.special args with @@ -258,17 +260,15 @@ let focusOnTermination () = List.iter focusOnTermination (Svcomp.Specification.of_option ()) let focusOnConcurrencySafety () = - let hasDataRaceSpec = List.mem SvcompSpec.NoDataRace (Svcomp.Specification.of_option ()) in - if hasDataRaceSpec then + 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 @@ -277,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 @@ -549,7 +546,8 @@ let chooseConfig file = 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; From 9f6bf249971fb49b38d67fefe1f746e11dc2a4d8 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Mon, 10 Feb 2025 23:09:11 +0200 Subject: [PATCH 12/12] Fix incomplete description --- src/util/autoSoundConfig.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/autoSoundConfig.ml b/src/util/autoSoundConfig.ml index 6875df9bae..6fcb7003df 100644 --- a/src/util/autoSoundConfig.ml +++ b/src/util/autoSoundConfig.ml @@ -65,4 +65,4 @@ let activateLongjmpAnalysesWhenRequired () = | _ -> false in if hasFunction isLongjmp then - enableAnalyses "Longjmp" "longjmp" longjmpAnalyses; + enableAnalyses "Longjmp" "longjmp analyses" longjmpAnalyses;