From e28f72b22f55fa0412d14b5877c8c90577c1c3eb Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 2 Aug 2023 14:29:13 +0200 Subject: [PATCH] Improve SVComp result generation and support all 3 memory-safety props --- src/autoTune.ml | 11 ++++--- src/witness/svcomp.ml | 4 ++- src/witness/svcompSpec.ml | 41 +++++++++++++++++++------- src/witness/witness.ml | 62 ++++++++++++++++++++++++++++++++++++++- 4 files changed, 101 insertions(+), 17 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index bce12302cd..d532081799 100644 --- a/src/autoTune.ml +++ b/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 diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml index b762d2eb5d..f1ee18ed72 100644 --- a/src/witness/svcomp.ml +++ b/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" diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml index 784155ab9b..8dafb8873c 100644 --- a/src/witness/svcompSpec.ml +++ b/src/witness/svcompSpec.ml @@ -6,19 +6,20 @@ 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 @@ -26,6 +27,16 @@ 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 + 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 diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 6dc0d04034..797541c606 100644 --- a/src/witness/witness.ml +++ b/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 =