From 1384f733d812996399648b4a846389fcbac29afb Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Mon, 2 Oct 2023 09:57:38 +0200 Subject: [PATCH] Add support for SV-COMP's valid-memcleanup property --- src/autoTune.ml | 1 + src/framework/analysisState.ml | 3 +++ src/util/analysisStateUtil.ml | 4 +++- src/witness/svcomp.ml | 1 + src/witness/svcompSpec.ml | 13 +++++++++++-- src/witness/witness.ml | 30 ++++++++++++++++++++++++++++++ 6 files changed, 49 insertions(+), 3 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 9e3508ccd2..ac7c150546 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -227,6 +227,7 @@ let focusOnSpecification () = | ValidDeref | ValidMemtrack -> () | MemorySafety -> () (* TODO: This is here for now just to complete the pattern match *) + | ValidMemcleanup -> () (*Detect enumerations and enable the "ana.int.enums" option*) exception EnumFound diff --git a/src/framework/analysisState.ml b/src/framework/analysisState.ml index ca619d4dfb..1416f99f69 100644 --- a/src/framework/analysisState.ml +++ b/src/framework/analysisState.ml @@ -16,6 +16,9 @@ let svcomp_may_invalid_deref = ref false (** Whether an invalid memtrack happened *) let svcomp_may_invalid_memtrack = ref false +(** Whether an invalid memcleanup happened *) +let svcomp_may_invalid_memcleanup = ref false + (** A hack to see if we are currently doing global inits *) let global_initialization = ref false diff --git a/src/util/analysisStateUtil.ml b/src/util/analysisStateUtil.ml index 25914f8c8e..a34be33f18 100644 --- a/src/util/analysisStateUtil.ml +++ b/src/util/analysisStateUtil.ml @@ -2,10 +2,12 @@ type mem_safety_violation = | InvalidFree | InvalidDeref | InvalidMemTrack + | InvalidMemcleanup let set_mem_safety_flag violation_type = if !AnalysisState.postsolving then match violation_type with | InvalidFree -> AnalysisState.svcomp_may_invalid_free := true | InvalidDeref -> AnalysisState.svcomp_may_invalid_deref := true - | InvalidMemTrack -> AnalysisState.svcomp_may_invalid_memtrack := true \ No newline at end of file + | InvalidMemTrack -> AnalysisState.svcomp_may_invalid_memtrack := true + | InvalidMemcleanup -> AnalysisState.svcomp_may_invalid_memcleanup := true \ No newline at end of file diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml index 15d41c0210..22543d48a9 100644 --- a/src/witness/svcomp.ml +++ b/src/witness/svcomp.ml @@ -56,6 +56,7 @@ struct | 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 ^ ")" | Unknown -> "unknown" diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml index fbe206dabb..25a9f522bc 100644 --- a/src/witness/svcompSpec.ml +++ b/src/witness/svcompSpec.ml @@ -10,10 +10,12 @@ type t = | ValidDeref | ValidMemtrack | MemorySafety (* Internal property for use in Goblint; serves as a summary for ValidFree, ValidDeref and ValidMemtrack *) + | ValidMemcleanup let of_string s = let s = String.strip s in - let regexp = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )" 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 let global_not = Str.matched_group 1 s in @@ -28,7 +30,7 @@ let of_string s = UnreachCall f else failwith "Svcomp.Specification.of_string: unknown global not expression" - else if Str.string_match regexp s 0 then + 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 @@ -43,6 +45,12 @@ let of_string s = ValidMemtrack *) 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 + ValidMemcleanup + else + failwith "Svcomp.Specification.of_string: unknown global expression" else failwith "Svcomp.Specification.of_string: unknown expression" @@ -72,5 +80,6 @@ let to_string spec = | 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 diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 17dd14472e..35d932210d 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -625,6 +625,36 @@ struct in (module TaskResult:WitnessTaskResult) ) + | ValidMemcleanup -> + let module TrivialArg = + struct + include Arg + let next _ = [] + end + in + if not !AnalysisState.svcomp_may_invalid_memcleanup 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 =