Autotune termination spec before preprocessing, but not others.

goblint · Nov 19, 2023 · 0652213 · 0652213
1 parent 116916a
commit 0652213
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 8 deletions.
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
@@ -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
@@ -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 =