Merge pull request #1255 from goblint/autotune_termination_spec

Autotune termination spec before preprocessing, but not others.
goblint · Nov 19, 2023 · 1be498c · 1be498c
2 parents 116916a + 9d8629d
commit 1be498c
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 10 deletions.
diff --git a/conf/svcomp.json b/conf/svcomp.json
@@ -72,8 +72,7 @@
         "wideningThresholds",
         "loopUnrollHeuristic",
         "memsafetySpecification",
-        "termination",
-        "specification"
+        "termination"
       ]
     }
   },

diff --git a/src/autoTune.ml b/src/autoTune.ml
@@ -237,12 +237,8 @@ let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) =
 let focusOnMemSafetySpecification () =
   List.iter focusOnMemSafetySpecification (Svcomp.Specification.of_option ())
 
-let focusOnSpecification (spec: Svcomp.Specification.t) =
+let focusOnTermination (spec: Svcomp.Specification.t) =
   match spec with
-  | UnreachCall s -> ()
-  | NoDataRace -> (*enable all thread analyses*)
-    print_endline @@ "Specification: NoDataRace -> enabling thread analyses \"" ^ (String.concat ", " notNeccessaryThreadAnalyses) ^ "\"";
-    enableAnalyses notNeccessaryThreadAnalyses;
   | Termination ->
     let terminationAnas = ["termination"; "threadflag"; "apron"] in
     print_endline @@ "Specification: Termination -> enabling termination analyses \"" ^ (String.concat ", " terminationAnas) ^ "\"";
@@ -251,6 +247,17 @@ let focusOnSpecification (spec: Svcomp.Specification.t) =
     set_bool "ana.int.interval" true;
     set_string "ana.apron.domain" "polyhedra"; (* TODO: Needed? *)
     ()
+  | _ -> ()
+
+let focusOnTermination () =
+  List.iter focusOnTermination (Svcomp.Specification.of_option ())
+
+let focusOnSpecification (spec: Svcomp.Specification.t) =
+  match spec with
+  | UnreachCall s -> ()
+  | NoDataRace -> (*enable all thread analyses*)
+    print_endline @@ "Specification: NoDataRace -> enabling thread analyses \"" ^ (String.concat ", " notNeccessaryThreadAnalyses) ^ "\"";
+    enableAnalyses notNeccessaryThreadAnalyses;
   | NoOverflow -> (*We focus on integer analysis*)
     set_bool "ana.int.def_exc" true;
     set_bool "ana.int.interval" true
@@ -499,6 +506,9 @@ let isTerminationTask () = List.mem Svcomp.Specification.Termination (Svcomp.Spe
 let specificationIsActivated () =
   isActivated "specification" && get_string "ana.specification" <> ""
 
+let specificationTerminationIsActivated () =
+  isActivated "termination"
+
 let chooseConfig file =
   let factors = collectFactors visitCilFileSameGlobals file in
   let fileCompplexity = estimateComplexity factors file in
@@ -518,8 +528,8 @@ let chooseConfig file =
   if isActivated "mallocWrappers" then
     findMallocWrappers ();
 
-  (* if specificationIsActivated () then
-     focusOnSpecification (); *)
+  if specificationIsActivated () then
+    focusOnSpecification ();
 
   if isActivated "enums" && hasEnums file then
     set_bool "ana.int.enums" true;

diff --git a/src/goblint.ml b/src/goblint.ml
@@ -39,7 +39,7 @@ let main () =
       print_endline GobSys.command_line;
     );
     (* When analyzing a termination specification, activate the termination analysis before pre-processing. *)
-    if get_bool "ana.autotune.enabled" && AutoTune.specificationIsActivated () then AutoTune.focusOnSpecification ();
+    if get_bool "ana.autotune.enabled" && AutoTune.specificationTerminationIsActivated () then AutoTune.focusOnTermination ();
     let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_parse_merge) in
     if get_bool "server.enabled" then (
       let file =