Autotune for ana.malloc.unique_address_count for NoOverflows in SV-Comp

conf/svcomp.json

@@ -66,6 +66,7 @@
         "wideningThresholds",
         "loopUnrollHeuristic",
         "memsafetySpecification",
+        "noOverflows",
         "termination",
         "tmpSpecialAnalysis"
       ]

src/autoTune.ml

@@ -44,6 +44,26 @@ class functionVisitor(calling, calledBy, argLists, dynamicallyCalled) = object
     DoChildren
 end
 
+exception Found
+class findAllocsNotInLoops = object
+  inherit nopCilVisitor
+
+  method! vstmt stmt =
+    match stmt.skind with
+    | Loop _ -> SkipChildren
+    | _ -> DoChildren
+
+  method! vinst = function
+    | Call (_, Lval (Var f, NoOffset), args,_,_) ->
+      let desc = LibraryFunctions.find f in
+      begin match desc.special args with
+        | Malloc _
+        | Alloca _ -> raise Found
+        | _ -> DoChildren
+      end
+    | _ -> DoChildren
+end
+
 type functionCallMaps = {
   calling: FunctionSet.t FunctionCallMap.t;
   calledBy: (FunctionSet.t * int) FunctionCallMap.t;
@@ -230,18 +250,28 @@ let focusOnTermination (spec: Svcomp.Specification.t) =
 let focusOnTermination () =
   List.iter focusOnTermination (Svcomp.Specification.of_option ())
 
-let focusOnSpecification (spec: Svcomp.Specification.t) =
+let reachSafety (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 findAllocsNotInLoops) (!Cilfacade.current_file)
+      with Found -> set_int "ana.malloc.unique_address_count" 1;
+    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 +519,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 +538,11 @@ let chooseConfig file =
   if isActivated "mallocWrappers" then
     findMallocWrappers ();
 
-  if specificationIsActivated () then
-    focusOnSpecification ();
+  if isActivated "reachSafetySpecification" then focusOn reachSafety;
+
+  if isActivated "concurrencySafetySpecification" then focusOn concurrencySafety;
+
+  if isActivated "noOverflows" then focusOn noOverflows;
 
   if isActivated "enums" && hasEnums file then
     set_bool "ana.int.enums" true;

src/config/options.schema.json

@@ -535,7 +535,6 @@
                 "enum": [
                   "congruence",
                   "singleThreaded",
-                  "specification",
                   "mallocWrappers",
                   "noRecursiveIntervals",
                   "enums",
@@ -545,14 +544,16 @@
                   "octagon",
                   "wideningThresholds",
                   "memsafetySpecification",
+                  "reachSafetySpecification",
+                  "concurrencySafetySpecification",
+                  "noOverflows",
                   "termination",
                   "tmpSpecialAnalysis"
                 ]
               },
               "default": [
                 "congruence",
                 "singleThreaded",
-                "specification",
                 "mallocWrappers",
                 "noRecursiveIntervals",
                 "enums",
@@ -561,6 +562,9 @@
                 "octagon",
                 "wideningThresholds",
                 "memsafetySpecification",
+                "reachSafetySpecification",
+                "concurrencySafetySpecification",
+                "noOverflows",
                 "termination",
                 "tmpSpecialAnalysis"
               ]

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 =

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 ();