Improve SVComp result generation and support all 3 memory-safety props

src/autoTune.ml

@@ -185,7 +185,6 @@ let enableAnalyses anas =
 (*does not consider dynamic calls!*)
 
 let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"]
-let memorySafetyAnalyses = ["useAfterFree"]
 let reduceThreadAnalyses () =
   let isThreadCreate = function
     | LibraryDesc.ThreadCreate _ -> true
@@ -220,9 +219,13 @@ let focusOnSpecification () =
   | NoOverflow -> (*We focus on integer analysis*)
     set_bool "ana.int.def_exc" true;
     set_bool "ana.int.interval" true
-  | MemorySafety -> (* Enable the memory safety analyses *)
-    print_endline @@ "Specification: MemorySafety -> enabling memory safety analyses \"" ^ (String.concat ", " memorySafetyAnalyses) ^ "\"";
-    enableAnalyses memorySafetyAnalyses
+  | ValidFree -> (* Enable the useAfterFree analysis *)
+    let uafAna = ["useAfterFree"] in
+    print_endline @@ "Specification: ValidFree -> enabling useAfterFree analysis \"" ^ (String.concat ", " uafAna) ^ "\"";
+    enableAnalyses uafAna
+  (* TODO: Finish these two below later *)
+  | ValidDeref
+  | ValidMemtrack -> ()
 
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound

src/witness/svcomp.ml

@@ -52,7 +52,9 @@ struct
         | UnreachCall _ -> "unreach-call"
         | NoOverflow -> "no-overflow"
         | NoDataRace -> "no-data-race" (* not yet in SV-COMP/Benchexec *)
-        | MemorySafety -> "memory-safety"
+        | ValidFree -> "valid-free"
+        | ValidDeref -> "valid-deref"
+        | ValidMemtrack -> "valid-memtrack"
       in
       "false(" ^ result_spec ^ ")"
     | Unknown -> "unknown"

src/witness/svcompSpec.ml

@@ -6,26 +6,37 @@ type t =
   | UnreachCall of string
   | NoDataRace
   | NoOverflow
-  | MemorySafety
+  | ValidFree
+  | ValidDeref
+  | ValidMemtrack
 
 let of_string s =
   let s = String.strip s in
-  let regexp = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in
-  if Str.string_match regexp s 0 then
+  let regexp = 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
     let global_not = Str.matched_group 1 s in
     if global_not = "data-race" then
       NoDataRace
     else if global_not = "overflow" then
       NoOverflow
-    else if global_not = "memory-safety" then
-      MemorySafety
     else
       let call_regex = Str.regexp "call(\\(.*\\)())" in
       if Str.string_match call_regex global_not 0 then
         let f = Str.matched_group 1 global_not in
         UnreachCall f
       else
         failwith "Svcomp.Specification.of_string: unknown global not expression"
+  else if Str.string_match regexp s 0 then
+    let global = Str.matched_group 1 s in
+    if global = "valid-free" then
+      ValidFree
+    else if global = "valid-deref" then
+      ValidDeref
+    else if global = "valid-memtrack" then
+      ValidMemtrack
+    else
+      failwith "Svcomp.Specification.of_string: unknown global expression"
   else
     failwith "Svcomp.Specification.of_string: unknown expression"
 
@@ -41,10 +52,18 @@ let of_option () =
     of_string s
 
 let to_string spec =
-  let global_not = match spec with
-    | UnreachCall f -> "call(" ^ f ^ "())"
-    | NoDataRace -> "data-race"
-    | NoOverflow -> "overflow"
-    | MemorySafety -> "memory-safety"
+  let print_output spec_str is_neg =
+    if is_neg then
+      Printf.sprintf "CHECK( init(main()), LTL(G ! %s) )" spec_str
+    else
+      Printf.sprintf "CHECK( init(main()), LTL(G %s) )" spec_str
+  in
+  let spec_str, is_neg = match spec with
+    | UnreachCall f -> "call(" ^ f ^ "())", true
+    | NoDataRace -> "data-race", true
+    | NoOverflow -> "overflow", true
+    | ValidFree -> "valid-free", false
+    | ValidDeref -> "valid-deref", false
+    | ValidMemtrack -> "valid-memtrack", false
   in
-  "CHECK( init(main()), LTL(G ! " ^ global_not ^ ") )"
+  print_output spec_str is_neg

src/witness/witness.ml

@@ -472,7 +472,7 @@ struct
         in
         (module TaskResult:WitnessTaskResult)
       )
-    | MemorySafety ->
+    | ValidFree ->
       let module TrivialArg =
       struct
         include Arg
@@ -502,6 +502,66 @@ struct
         in
         (module TaskResult:WitnessTaskResult)
       )
+    | ValidDeref ->
+      let module TrivialArg =
+      struct
+        include Arg
+        let next _ = []
+      end
+      in
+      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
+          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)
+      )
 
 
   let write entrystates =