Merge pull request #1612 from goblint/svcomp-auto-malloc

Autotune for `ana.malloc.unique_address_count` for NoOverflows in SV-Comp
goblint · Nov 7, 2024 · 06e0554 · 06e0554
2 parents e8b56ec + 72bf7d6
commit 06e0554
Show file tree

Hide file tree

Showing 6 changed files with 55 additions and 21 deletions.
diff --git a/conf/svcomp-validate.json b/conf/svcomp-validate.json
@@ -67,6 +67,7 @@
         "wideningThresholds",
         "loopUnrollHeuristic",
         "memsafetySpecification",
+        "noOverflows",
         "termination",
         "tmpSpecialAnalysis"
       ]

diff --git a/conf/svcomp.json b/conf/svcomp.json
@@ -66,6 +66,7 @@
         "wideningThresholds",
         "loopUnrollHeuristic",
         "memsafetySpecification",
+        "noOverflows",
         "termination",
         "tmpSpecialAnalysis"
       ]

diff --git a/src/autoTune.ml b/src/autoTune.ml
@@ -44,6 +44,34 @@ class functionVisitor(calling, calledBy, argLists, dynamicallyCalled) = object
     DoChildren
 end
 
+exception Found
+class findAllocsInLoops = object
+  inherit nopCilVisitor
+
+  val mutable inloop = false
+
+  method! vstmt stmt =
+    let outOfLoop stmt =
+      match stmt.skind with
+      | Loop _ -> inloop <- false; stmt
+      | _ -> stmt
+    in
+    match stmt.skind with
+    | Loop _ -> inloop <- true; ChangeDoChildrenPost(stmt, outOfLoop)
+    | _ -> DoChildren
+
+  method! vinst = function
+    | Call (_, Lval (Var f, NoOffset), args,_,_) when LibraryFunctions.is_special f ->
+      Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo f) ~finally:Fun.id @@ fun () ->
+      let desc = LibraryFunctions.find f in
+      begin match desc.special args with
+        | Malloc _
+        | Alloca _ when inloop -> raise Found
+        | _ -> DoChildren
+      end
+    | _ -> DoChildren
+end
+
 type functionCallMaps = {
   calling: FunctionSet.t FunctionCallMap.t;
   calledBy: (FunctionSet.t * int) FunctionCallMap.t;
@@ -230,18 +258,28 @@ let focusOnTermination (spec: Svcomp.Specification.t) =
 let focusOnTermination () =
   List.iter focusOnTermination (Svcomp.Specification.of_option ())
 
-let focusOnSpecification (spec: Svcomp.Specification.t) =
+let concurrencySafety (spec: Svcomp.Specification.t) =
   match spec with
-  | UnreachCall s -> ()
   | NoDataRace -> (*enable all thread analyses*)
     Logs.info "Specification: NoDataRace -> enabling thread analyses \"%s\"" (String.concat ", " notNeccessaryThreadAnalyses);
     enableAnalyses notNeccessaryThreadAnalyses;
-  | NoOverflow -> (*We focus on integer analysis*)
-    set_bool "ana.int.def_exc" true
   | _ -> ()
 
-let focusOnSpecification () =
-  List.iter focusOnSpecification (Svcomp.Specification.of_option ())
+let noOverflows (spec: Svcomp.Specification.t) =
+  match spec with
+  | NoOverflow ->
+    (*We focus on integer analysis*)
+    set_bool "ana.int.def_exc" true;
+    begin
+      try
+        ignore @@ visitCilFileSameGlobals (new findAllocsInLoops) (!Cilfacade.current_file);
+        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
@@ -489,15 +527,6 @@ let isActivated a = get_bool "ana.autotune.enabled" && List.mem a @@ get_string_
 
 let isTerminationTask () = List.mem Svcomp.Specification.Termination (Svcomp.Specification.of_option ())
 
-let specificationIsActivated () =
-  isActivated "specification" && get_string "ana.specification" <> ""
-
-let specificationTerminationIsActivated () =
-  isActivated "termination"
-
-let specificationMemSafetyIsActivated () =
-  isActivated "memsafetySpecification"
-
 let chooseConfig file =
   let factors = collectFactors visitCilFileSameGlobals file in
   let fileCompplexity = estimateComplexity factors file in
@@ -517,8 +546,9 @@ let chooseConfig file =
   if isActivated "mallocWrappers" then
     findMallocWrappers ();
 
-  if specificationIsActivated () then
-    focusOnSpecification ();
+  if isActivated "concurrencySafetySpecification" then focusOn concurrencySafety;
+
+  if isActivated "noOverflows" then focusOn noOverflows;
 
   if isActivated "enums" && hasEnums file then
     set_bool "ana.int.enums" true;

diff --git a/src/config/options.schema.json b/src/config/options.schema.json
@@ -535,7 +535,6 @@
                 "enum": [
                   "congruence",
                   "singleThreaded",
-                  "specification",
                   "mallocWrappers",
                   "noRecursiveIntervals",
                   "enums",
@@ -545,14 +544,15 @@
                   "octagon",
                   "wideningThresholds",
                   "memsafetySpecification",
+                  "concurrencySafetySpecification",
+                  "noOverflows",
                   "termination",
                   "tmpSpecialAnalysis"
                 ]
               },
               "default": [
                 "congruence",
                 "singleThreaded",
-                "specification",
                 "mallocWrappers",
                 "noRecursiveIntervals",
                 "enums",
@@ -561,6 +561,8 @@
                 "octagon",
                 "wideningThresholds",
                 "memsafetySpecification",
+                "concurrencySafetySpecification",
+                "noOverflows",
                 "termination",
                 "tmpSpecialAnalysis"
               ]

diff --git a/src/goblint.ml b/src/goblint.ml
@@ -37,7 +37,7 @@ let main () =
     Logs.debug "%s" GobSys.command_line;
     (* When analyzing a termination specification, activate the termination analysis before pre-processing. *)
     if get_string "ana.specification" <> "" then AutoSoundConfig.enableAnalysesForTerminationSpecification ();
-    if AutoTune.specificationTerminationIsActivated () then AutoTune.focusOnTermination ();
+    if AutoTune.isActivated "termination" then AutoTune.focusOnTermination ();
     let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_parse_merge) in
     if get_bool "server.enabled" then (
       let file =

diff --git a/src/maingoblint.ml b/src/maingoblint.ml
@@ -203,7 +203,7 @@ let handle_options () =
   Sys.set_signal (GobSys.signal_of_string (get_string "dbg.solver-signal")) Signal_ignore; (* Ignore solver-signal before solving (e.g. MyCFG), otherwise exceptions self-signal the default, which crashes instead of printing backtrace. *)
   if get_string "ana.specification" <> "" then
     AutoSoundConfig.enableAnalysesForMemSafetySpecification ();
-  if AutoTune.specificationMemSafetyIsActivated () then
+  if AutoTune.isActivated "memsafetySpecification" then
     AutoTune.focusOnMemSafetySpecification ();
   AfterConfig.run ();
   Cilfacade.init_options ();