From 3747556e90acdced4e01fc21e9c83107d10f93fc Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 31 Oct 2023 17:23:40 +0200 Subject: [PATCH] Remove special MemorySafety SV-COMP property, add full multiproperty handling --- src/autoTune.ml | 10 ---------- src/witness/svcomp.ml | 2 +- src/witness/svcompSpec.ml | 34 +++++++++++++++++----------------- src/witness/witness.ml | 27 ++++++++++++++++++++++----- 4 files changed, 40 insertions(+), 33 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index c00564bce7..06347f3190 100644 --- a/src/autoTune.ml +++ b/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 () = diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml index 6d773f666b..736de0efae 100644 --- a/src/witness/svcomp.ml +++ b/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 ^ ")" diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml index 185f1fbf67..9bd5a35e3e 100644 --- a/src/witness/svcompSpec.ml +++ b/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) diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 310717b9c3..419185400c 100644 --- a/src/witness/witness.ml +++ b/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