From 4d6b570d6d3c20850fcbe0e95f86638e8595c78b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 31 Oct 2023 16:29:10 +0200 Subject: [PATCH 1/5] Add type for SV-COMP multiproperty --- src/autoTune.ml | 21 ++++++++++++++------- src/util/loopUnrolling.ml | 7 ++++--- src/witness/svcomp.ml | 16 +++++++++------- src/witness/svcompSpec.ml | 9 +++++++++ src/witness/witness.ml | 10 +++++++--- 5 files changed, 43 insertions(+), 20 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index b96848c841..c00564bce7 100644 --- 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 index 62d0f662f3..9a2f6c7b29 100644 --- 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 index 22543d48a9..6d773f666b 100644 --- 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 index 4a3da23d9b..185f1fbf67 100644 --- 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 index 9f5a3c1801..310717b9c3 100644 --- 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 From 3747556e90acdced4e01fc21e9c83107d10f93fc Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 31 Oct 2023 17:23:40 +0200 Subject: [PATCH 2/5] 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 From 5093b5dd90a6ec7aca4c541e007c7d4f3025b707 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 31 Oct 2023 17:25:11 +0200 Subject: [PATCH 3/5] Fix witness determine_result for memsafety --- src/witness/witness.ml | 64 ++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 61 insertions(+), 3 deletions(-) diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 419185400c..dd829dd9e2 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -505,8 +505,66 @@ struct in (module TaskResult:WitnessTaskResult) ) - | ValidFree - | ValidDeref + | 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_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 @@ -514,7 +572,7 @@ struct 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_memtrack then ( let module TaskResult = struct module Arg = Arg From bb163a55ba1e06afcd267a02e521a4907f694db2 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 31 Oct 2023 19:13:04 +0200 Subject: [PATCH 4/5] Deduplicate Svcomp.is_error_function --- src/util/loopUnrolling.ml | 6 ++---- src/witness/svcomp.ml | 15 +++++++-------- 2 files changed, 9 insertions(+), 12 deletions(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index 9a2f6c7b29..4ce8fc06b4 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -324,10 +324,8 @@ class loopUnrollingCallVisitor = object raise Found; | _ -> if List.mem "specification" @@ get_string_list "ana.autotune.activated" && get_string "ana.specification" <> "" then ( - List.iter (function - | SvcompSpec.UnreachCall s -> if info.vname = s then raise Found - | _ -> () - ) (SvcompSpec.of_option ()) + if Svcomp.is_error_function' info (SvcompSpec.of_option ()) then + raise Found ); DoChildren ) diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml index 736de0efae..218f0716ae 100644 --- a/src/witness/svcomp.ml +++ b/src/witness/svcomp.ml @@ -16,12 +16,16 @@ end let task: (module Task) option ref = ref None -let is_error_function f = +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 - ) Task.specification + ) spec + +let is_error_function f = + let module Task = (val (Option.get !task)) in + is_error_function' f Task.specification (* TODO: unused, but should be used? *) let is_special_function f = @@ -29,12 +33,7 @@ let is_special_function f = 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 - List.exists (function - | Specification.UnreachCall f_spec -> fname = f_spec - | _ -> false - ) Task.specification + | fname -> is_error_function f in is_svcomp && is_verifier From f147d9bdd67fda7d77907631b643678eebe4284a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 2 Nov 2023 10:05:22 +0200 Subject: [PATCH 5/5] Remove unused [@@deriving ord] on SV-COMP spec --- src/witness/svcomp.ml | 1 - src/witness/svcompSpec.ml | 1 - 2 files changed, 2 deletions(-) diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml index 218f0716ae..eae97b1199 100644 --- a/src/witness/svcomp.ml +++ b/src/witness/svcomp.ml @@ -44,7 +44,6 @@ struct | True | False of Specification.t option | Unknown - [@@deriving ord] let to_string = function | True -> "true" diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml index 9bd5a35e3e..66b3b83ac8 100644 --- a/src/witness/svcompSpec.ml +++ b/src/witness/svcompSpec.ml @@ -10,7 +10,6 @@ type t = | ValidDeref | ValidMemtrack | ValidMemcleanup -[@@deriving ord] type multi = t list