Add type for SV-COMP multiproperty

goblint · Oct 31, 2023 · 4d6b570 · 4d6b570
1 parent 6131273
commit 4d6b570
Show file tree

Hide file tree

Showing 5 changed files with 43 additions and 20 deletions.
diff --git a/src/autoTune.ml b/src/autoTune.ml
@@ -210,8 +210,8 @@ let activateLongjmpAnalysesWhenRequired () =
     enableAnalyses longjmpAnalyses;
   )
 
-let focusOnMemSafetySpecification () =
-  match Svcomp.Specification.of_option () with
+let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) =
+  match spec with
   | ValidFree -> (* Enable the useAfterFree analysis *)
     let uafAna = ["useAfterFree"] in
     print_endline @@ "Specification: ValidFree -> enabling useAfterFree analysis \"" ^ (String.concat ", " uafAna) ^ "\"";
@@ -244,8 +244,11 @@ let focusOnMemSafetySpecification () =
      enableAnalyses memSafetyAnas)
   | _ -> ()
 
-let focusOnSpecification () =
-  match Svcomp.Specification.of_option () with
+let focusOnMemSafetySpecification () =
+  List.iter focusOnMemSafetySpecification (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) ^ "\"";
@@ -255,6 +258,9 @@ let focusOnSpecification () =
     set_bool "ana.int.interval" true
   | _ -> ()
 
+let focusOnSpecification () =
+  List.iter focusOnSpecification (Svcomp.Specification.of_option ())
+
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound
 class enumVisitor = object
@@ -411,9 +417,10 @@ let congruenceOption factors file =
 let apronOctagonOption factors file =
   let locals =
     if List.mem "specification" (get_string_list "ana.autotune.activated" ) && get_string "ana.specification" <> "" then
-      match Svcomp.Specification.of_option () with
-      | NoOverflow -> 12
-      | _ -> 8
+      if List.mem Svcomp.Specification.NoOverflow (Svcomp.Specification.of_option ()) then
+        12
+      else
+        8
     else 8
   in let globals = 2 in
   let selectedLocals =

diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
@@ -324,9 +324,10 @@ class loopUnrollingCallVisitor = object
           raise Found;
         | _ ->
           if List.mem "specification" @@ get_string_list "ana.autotune.activated" && get_string "ana.specification" <> "" then (
-            match SvcompSpec.of_option () with
-            | UnreachCall s -> if info.vname = s then raise Found
-            | _ -> ()
+            List.iter (function
+                | SvcompSpec.UnreachCall s -> if info.vname = s then raise Found
+                | _ -> ()
+              ) (SvcompSpec.of_option ())
           );
           DoChildren
       )

diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml
@@ -8,7 +8,7 @@ module Specification = SvcompSpec
 module type Task =
 sig
   val file: Cil.file
-  val specification: Specification.t
+  val specification: Specification.multi
 
   module Cfg: MyCFG.CfgBidir
 end
@@ -18,9 +18,10 @@ let task: (module Task) option ref = ref None
 
 let is_error_function f =
   let module Task = (val (Option.get !task)) in
-  match Task.specification with
-  | UnreachCall f_spec -> f.vname = f_spec
-  | _ -> false
+  List.exists (function
+      | Specification.UnreachCall f_spec -> f.vname = f_spec
+      | _ -> false
+    ) Task.specification
 
 (* TODO: unused, but should be used? *)
 let is_special_function f =
@@ -30,9 +31,10 @@ let is_special_function f =
     | fname when String.starts_with fname "__VERIFIER" -> true
     | fname ->
       let module Task = (val (Option.get !task)) in
-      match Task.specification with
-      | UnreachCall f_spec -> fname = f_spec
-      | _ -> false
+      List.exists (function
+          | Specification.UnreachCall f_spec -> fname = f_spec
+          | _ -> false
+        ) Task.specification
   in
   is_svcomp && is_verifier
 

diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml
@@ -12,6 +12,8 @@ type t =
   | MemorySafety (* Internal property for use in Goblint; serves as a summary for ValidFree, ValidDeref and ValidMemtrack *)
   | ValidMemcleanup
 
+type multi = t list
+
 let of_string s =
   let s = String.strip s in
   let regexp_multiple = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )" in
@@ -48,6 +50,8 @@ let of_string s =
   else
     failwith "Svcomp.Specification.of_string: unknown expression"
 
+let of_string s: multi = [of_string s]
+
 let of_file path =
   let s = BatFile.with_file_in path BatIO.read_all in
   of_string s
@@ -77,3 +81,8 @@ let to_string spec =
     | ValidMemcleanup -> "valid-memcleanup", false
   in
   print_output spec_str is_neg
+
+let to_string spec =
+  match spec with
+  | [spec] -> to_string spec
+  | _ -> assert false (* TODO: aggregate *)
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
@@ -303,7 +303,7 @@ struct
     val find_invariant: Node.t -> Invariant.t
   end
 
-  let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
+  let determine_result entrystates (module Task:Task) (spec: Svcomp.Specification.t): (module WitnessTaskResult) =
     let module Arg: BiArgInvariant =
       (val if GobConfig.get_bool "witness.enabled" then (
            let module Arg = (val ArgTool.create entrystates) in
@@ -338,7 +338,7 @@ struct
       )
     in
 
-    match Task.specification with
+    match spec with
     | UnreachCall _ ->
       (* error function name is globally known through Svcomp.task *)
       let is_unreach_call =
@@ -410,7 +410,7 @@ struct
             let module TaskResult =
             struct
               module Arg = PathArg
-              let result = Result.False (Some Task.specification)
+              let result = Result.False (Some spec)
               let invariant _ = Invariant.none
               let is_violation = is_violation
               let is_sink _ = false
@@ -569,6 +569,10 @@ struct
         (module TaskResult:WitnessTaskResult)
       )
 
+  let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
+    match Task.specification with
+    | [spec] -> determine_result entrystates (module Task) spec
+    | _ -> assert false (* TODO: aggregate *)
 
   let write entrystates =
     let module Task = (val (BatOption.get !task)) in