Remove special MemorySafety SV-COMP property, add full multiproperty …

…handling

src/autoTune.ml

@@ -232,16 +232,6 @@ let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) =
     );
     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 focusOnMemSafetySpecification () =

src/witness/svcomp.ml

@@ -45,6 +45,7 @@ struct
     | True
     | False of Specification.t option
     | Unknown
+  [@@deriving ord]
 
   let to_string = function
     | True -> "true"
@@ -57,7 +58,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,14 +9,13 @@ type t =
   | ValidFree
   | ValidDeref
   | ValidMemtrack
-  | MemorySafety (* Internal property for use in Goblint; serves as a summary for ValidFree, ValidDeref and ValidMemtrack *)
   | ValidMemcleanup
+[@@deriving ord]
 
 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
@@ -32,25 +31,29 @@ 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 = [of_string s]
+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
@@ -77,12 +80,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 =
-  match spec with
-  | [spec] -> to_string spec
-  | _ -> assert false (* TODO: aggregate *)
+  String.concat "\n" (List.map to_string spec)

src/witness/witness.ml

@@ -507,8 +507,7 @@ struct
       )
     | ValidFree
     | ValidDeref
-    | ValidMemtrack
-    | MemorySafety ->
+    | ValidMemtrack ->
       let module TrivialArg =
       struct
         include Arg
@@ -570,9 +569,27 @@ struct
       )
 
   let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
-    match Task.specification with
-    | [spec] -> determine_result entrystates (module Task) spec
-    | _ -> assert false (* TODO: aggregate *)
+    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