From 065221367db8e46f59f33bd18b07f8802af283e2 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Sun, 19 Nov 2023 16:47:03 +0100
Subject: [PATCH] Autotune termination spec before preprocessing, but not
 others.

---
 src/autoTune.ml | 21 ++++++++++++++-------
 src/goblint.ml  |  2 +-
 2 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 5e0034e6eb..70f61d5172 100644
--- 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
@@ -518,8 +525,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
index 6c5a2df33d..9b95c95da4 100644
--- 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.specificationIsActivated () then AutoTune.focusOnTermination ();
     let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_parse_merge) in
     if get_bool "server.enabled" then (
       let file =