Merge pull request #1228 from goblint/sv-comp-multiproperty

Support multi-property SV-COMP specifications

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) ^ "\"";
@@ -232,20 +232,13 @@ let focusOnMemSafetySpecification () =
     );
     print_endline @@ "Specification: ValidMemtrack and ValidMemcleanup -> enabling memLeak analysis \"" ^ (String.concat ", " memLeakAna) ^ "\"";
     enableAnalyses memLeakAna
-  | MemorySafety -> (* TODO: This is a temporary solution for the memory safety category *)
-    set_bool "ana.arrayoob" true;
-    (print_endline "Setting \"cil.addNestedScopeAttr\" to true";
-     set_bool "cil.addNestedScopeAttr" true;
-     if (get_int "ana.malloc.unique_address_count") < 1 then (
-       print_endline "Setting \"ana.malloc.unique_address_count\" to 1";
-       set_int "ana.malloc.unique_address_count" 1;
-     );
-     let memSafetyAnas = ["memOutOfBounds"; "memLeak"; "useAfterFree";] in
-     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 +248,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 +407,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 =

src/util/loopUnrolling.ml

@@ -324,9 +324,8 @@ 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
-            | _ -> ()
+            if Svcomp.is_error_function' info (SvcompSpec.of_option ()) then
+              raise Found
           );
           DoChildren
       )

src/witness/svcomp.ml

@@ -8,31 +8,32 @@ module Specification = SvcompSpec
 module type Task =
 sig
   val file: Cil.file
-  val specification: Specification.t
+  val specification: Specification.multi
 
   module Cfg: MyCFG.CfgBidir
 end
 
 let task: (module Task) option ref = ref None
 
 
+let is_error_function' f spec =
+  let module Task = (val (Option.get !task)) in
+  List.exists (function
+      | Specification.UnreachCall f_spec -> f.vname = f_spec
+      | _ -> false
+    ) spec
+
 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
+  is_error_function' f Task.specification
 
 (* TODO: unused, but should be used? *)
 let is_special_function f =
   let loc = f.vdecl in
   let is_svcomp = String.ends_with loc.file "sv-comp.c" in (* only includes/sv-comp.c functions, not __VERIFIER_assert in benchmark *)
   let is_verifier = match f.vname with
     | 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
+    | fname -> is_error_function f
   in
   is_svcomp && is_verifier
 
@@ -55,7 +56,6 @@ struct
         | ValidFree -> "valid-free"
         | ValidDeref -> "valid-deref"
         | ValidMemtrack -> "valid-memtrack"
-        | MemorySafety -> "memory-safety" (* TODO: Currently here only to complete the pattern match *)
         | ValidMemcleanup -> "valid-memcleanup"
       in
       "false(" ^ result_spec ^ ")"

src/witness/svcompSpec.ml

@@ -9,12 +9,12 @@ type t =
   | ValidFree
   | ValidDeref
   | ValidMemtrack
-  | 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
   let regexp_single = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )" in
   let regexp_negated = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in
   if Str.string_match regexp_negated s 0 then
@@ -30,24 +30,30 @@ let of_string s =
         UnreachCall f
       else
         failwith "Svcomp.Specification.of_string: unknown global not expression"
-  else if Str.string_match regexp_multiple s 0 then
-    let global1 = Str.matched_group 1 s in
-    let global2 = Str.matched_group 2 s in
-    let global3 = Str.matched_group 3 s in
-    let mem_safety_props = ["valid-free"; "valid-deref"; "valid-memtrack";] in
-    if (global1 <> global2 && global1 <> global3 && global2 <> global3) && List.for_all (fun x -> List.mem x mem_safety_props) [global1; global2; global3] then
-      MemorySafety
-    else
-      failwith "Svcomp.Specification.of_string: unknown global expression"
   else if Str.string_match regexp_single s 0 then
     let global = Str.matched_group 1 s in
-    if global = "valid-memcleanup" then
+    if global = "valid-free" then
+      ValidFree
+    else if global = "valid-deref" then
+      ValidDeref
+    else if global = "valid-memtrack" then
+      ValidMemtrack
+    else if global = "valid-memcleanup" then
       ValidMemcleanup
     else
       failwith "Svcomp.Specification.of_string: unknown global expression"
   else
     failwith "Svcomp.Specification.of_string: unknown expression"
 
+let of_string s: multi =
+  List.filter_map (fun line ->
+      let line = String.strip line in
+      if line = "" then
+        None
+      else
+        Some (of_string line)
+    ) (String.split_on_char '\n' s)
+
 let of_file path =
   let s = BatFile.with_file_in path BatIO.read_all in
   of_string s
@@ -73,7 +79,9 @@ let to_string spec =
     | ValidFree -> "valid-free", false
     | ValidDeref -> "valid-deref", false
     | ValidMemtrack -> "valid-memtrack", false
-    | MemorySafety -> "memory-safety", false (* TODO: That's false, it's currently here just to complete the pattern match *)
     | ValidMemcleanup -> "valid-memcleanup", false
   in
   print_output spec_str is_neg
+
+let to_string spec =
+  String.concat "\n" (List.map to_string spec)

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.graphml.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
@@ -505,17 +505,74 @@ struct
         in
         (module TaskResult:WitnessTaskResult)
       )
-    | ValidFree
-    | ValidDeref
-    | ValidMemtrack
-    | MemorySafety ->
+    | ValidFree ->
+      let module TrivialArg =
+      struct
+        include Arg
+        let next _ = []
+      end
+      in
+      if not !AnalysisState.svcomp_may_invalid_free then (
+        let module TaskResult =
+        struct
+          module Arg = Arg
+          let result = Result.True
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      ) else (
+        let module TaskResult =
+        struct
+          module Arg = TrivialArg
+          let result = Result.Unknown
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      )
+    | ValidDeref ->
       let module TrivialArg =
       struct
         include Arg
         let next _ = []
       end
       in
-      if not !AnalysisState.svcomp_may_invalid_free && not !AnalysisState.svcomp_may_invalid_deref && not !AnalysisState.svcomp_may_invalid_memtrack then (
+      if not !AnalysisState.svcomp_may_invalid_deref then (
+        let module TaskResult =
+        struct
+          module Arg = Arg
+          let result = Result.True
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      ) else (
+        let module TaskResult =
+        struct
+          module Arg = TrivialArg
+          let result = Result.Unknown
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      )
+    | ValidMemtrack ->
+      let module TrivialArg =
+      struct
+        include Arg
+        let next _ = []
+      end
+      in
+      if not !AnalysisState.svcomp_may_invalid_memtrack then (
         let module TaskResult =
         struct
           module Arg = Arg
@@ -569,6 +626,28 @@ struct
         (module TaskResult:WitnessTaskResult)
       )
 
+  let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
+    Task.specification
+    |> List.fold_left (fun acc spec ->
+        let module TaskResult = (val determine_result entrystates (module Task) spec) in
+        match acc with
+        | None -> Some (module TaskResult: WitnessTaskResult)
+        | Some (module Acc: WitnessTaskResult) ->
+          match Acc.result, TaskResult.result with
+          (* keep old violation/unknown *)
+          | False _, True
+          | False _, Unknown
+          | Unknown, True -> Some (module Acc: WitnessTaskResult)
+          (* use new violation/unknown *)
+          | True, False _
+          | Unknown, False _
+          | True, Unknown -> Some (module TaskResult: WitnessTaskResult)
+          (* both same, arbitrarily keep old *)
+          | True, True -> Some (module Acc: WitnessTaskResult)
+          | Unknown, Unknown -> Some (module Acc: WitnessTaskResult)
+          | False _, False _ -> failwith "multiple violations"
+      ) None
+    |> Option.get
 
   let write entrystates =
     let module Task = (val (BatOption.get !task)) in