From a3b436284771cea0e1d86bda1a5b32da12f5e849 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 13 Jun 2024 18:04:33 +0300 Subject: [PATCH 1/9] Add YAML witness violation_sequence entry type --- src/witness/yamlWitnessType.ml | 200 +++++++++++++++++++++++++++++++++ 1 file changed, 200 insertions(+) diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml index 1630e05b69..526d52d327 100644 --- a/src/witness/yamlWitnessType.ml +++ b/src/witness/yamlWitnessType.ml @@ -426,6 +426,200 @@ struct let entry_type = "precondition_loop_invariant_certificate" end +module ViolationSequence = +struct + + module Constraint = + struct + type t = { + value: string; + format: string; + } + [@@deriving ord] + + let to_yaml {value; format} = + `O [ + ("value", `String value); + ("format", `String format); + ] + + let of_yaml y = + let open GobYaml in + let+ value = y |> find "value" >>= to_string + and+ format = y |> find "format" >>= to_string in + {value; format} + end + + module Assumption = + struct + type t = { + location: Location.t; + action: string; + constraint_: Constraint.t; + } + [@@deriving ord] + + let waypoint_type = "assumption" + + let to_yaml' {location; action; constraint_} = + [ + ("location", Location.to_yaml location); + ("action", `String action); + ("constraint", Constraint.to_yaml constraint_); + ] + + let of_yaml y = + let open GobYaml in + let+ location = y |> find "location" >>= Location.of_yaml + and+ action = y |> find "action" >>= to_string + and+ constraint_ = y |> find "constraint" >>= Constraint.of_yaml in + {location; action; constraint_} + end + + module Target = + struct + type t = { + location: Location.t; + action: string; + } + [@@deriving ord] + + let waypoint_type = "target" + + let to_yaml' {location; action} = + [ + ("location", Location.to_yaml location); + ("action", `String action); + ] + + let of_yaml y = + let open GobYaml in + let+ location = y |> find "location" >>= Location.of_yaml + and+ action = y |> find "action" >>= to_string in + {location; action} + end + + module FunctionEnter = + struct + include Target + + let waypoint_type = "function_enter" + end + + module FunctionReturn = + struct + include Assumption + + let waypoint_type = "function_return" + end + + module Branching = + struct + include Assumption + + let waypoint_type = "branching" + end + + (* TODO: could maybe use GADT, but adds ugly existential layer to entry type pattern matching *) + module WaypointType = + struct + type t = + | Assumption of Assumption.t + | Target of Target.t + | FunctionEnter of FunctionEnter.t + | FunctionReturn of FunctionReturn.t + | Branching of Branching.t + [@@deriving ord] + + let waypoint_type = function + | Assumption _ -> Assumption.waypoint_type + | Target _ -> Target.waypoint_type + | FunctionEnter _ -> FunctionEnter.waypoint_type + | FunctionReturn _ -> FunctionReturn.waypoint_type + | Branching _ -> Branching.waypoint_type + + let to_yaml' = function + | Assumption x -> Assumption.to_yaml' x + | Target x -> Target.to_yaml' x + | FunctionEnter x -> FunctionEnter.to_yaml' x + | FunctionReturn x -> FunctionReturn.to_yaml' x + | Branching x -> Branching.to_yaml' x + + let of_yaml y = + let open GobYaml in + let* waypoint_type = y |> find "type" >>= to_string in + if waypoint_type = Assumption.waypoint_type then + let+ x = y |> Assumption.of_yaml in + Assumption x + else if waypoint_type = Target.waypoint_type then + let+ x = y |> Target.of_yaml in + Target x + else if waypoint_type = FunctionEnter.waypoint_type then + let+ x = y |> FunctionEnter.of_yaml in + FunctionEnter x + else if waypoint_type = FunctionReturn.waypoint_type then + let+ x = y |> FunctionReturn.of_yaml in + FunctionReturn x + else if waypoint_type = Branching.waypoint_type then + let+ x = y |> Branching.of_yaml in + Branching x + else + Error (`Msg "type") + end + + module Waypoint = + struct + type t = { + waypoint_type: WaypointType.t; + } + [@@deriving ord] + + let to_yaml {waypoint_type} = + `O [ + ("waypoint", `O ([ + ("type", `String (WaypointType.waypoint_type waypoint_type)); + ] @ WaypointType.to_yaml' waypoint_type) + ) + ] + + let of_yaml y = + let open GobYaml in + let+ waypoint_type = y |> find "waypoint" >>= WaypointType.of_yaml in + {waypoint_type} + end + + module Segment = + struct + type t = { + segment: Waypoint.t list; + } + [@@deriving ord] + + let to_yaml {segment} = + `O [("segment", `A (List.map Waypoint.to_yaml segment))] + + let of_yaml y = + let open GobYaml in + let+ segment = y |> find "segment" >>= list >>= list_map Waypoint.of_yaml in + {segment} + end + + type t = { + content: Segment.t list; + } + [@@deriving ord] + + let entry_type = "violation_sequence" + + let to_yaml' {content} = + [("content", `A (List.map Segment.to_yaml content))] + + let of_yaml y = + let open GobYaml in + let+ content = y |> find "content" >>= list >>= list_map Segment.of_yaml in + {content} +end + (* TODO: could maybe use GADT, but adds ugly existential layer to entry type pattern matching *) module EntryType = struct @@ -437,6 +631,7 @@ struct | LoopInvariantCertificate of LoopInvariantCertificate.t | PreconditionLoopInvariantCertificate of PreconditionLoopInvariantCertificate.t | InvariantSet of InvariantSet.t + | ViolationSequence of ViolationSequence.t [@@deriving ord] let entry_type = function @@ -447,6 +642,7 @@ struct | LoopInvariantCertificate _ -> LoopInvariantCertificate.entry_type | PreconditionLoopInvariantCertificate _ -> PreconditionLoopInvariantCertificate.entry_type | InvariantSet _ -> InvariantSet.entry_type + | ViolationSequence _ -> ViolationSequence.entry_type let to_yaml' = function | LocationInvariant x -> LocationInvariant.to_yaml' x @@ -456,6 +652,7 @@ struct | LoopInvariantCertificate x -> LoopInvariantCertificate.to_yaml' x | PreconditionLoopInvariantCertificate x -> PreconditionLoopInvariantCertificate.to_yaml' x | InvariantSet x -> InvariantSet.to_yaml' x + | ViolationSequence x -> ViolationSequence.to_yaml' x let of_yaml y = let open GobYaml in @@ -481,6 +678,9 @@ struct else if entry_type = InvariantSet.entry_type then let+ x = y |> InvariantSet.of_yaml in InvariantSet x + else if entry_type = ViolationSequence.entry_type then + let+ x = y |> ViolationSequence.of_yaml in + ViolationSequence x else Error (`Msg "entry_type") end From a98da9d0c838a6073aff78515de848fb9d01047e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 14 Jun 2024 12:19:38 +0300 Subject: [PATCH 2/9] Implement violation_sequence in yamlWitnessStrip --- tests/util/yamlWitnessStrip.ml | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/tests/util/yamlWitnessStrip.ml b/tests/util/yamlWitnessStrip.ml index 8a5046d6ff..75c6cf3583 100644 --- a/tests/util/yamlWitnessStrip.ml +++ b/tests/util/yamlWitnessStrip.ml @@ -26,6 +26,25 @@ struct in {invariant_type} in + let waypoint_strip_file_hash ({waypoint_type}: ViolationSequence.Waypoint.t): ViolationSequence.Waypoint.t = + let waypoint_type: ViolationSequence.WaypointType.t = + match waypoint_type with + | Assumption x -> + Assumption {x with location = location_strip_file_hash x.location} + | Target x -> + Target {x with location = location_strip_file_hash x.location} + | FunctionEnter x -> + FunctionEnter {x with location = location_strip_file_hash x.location} + | FunctionReturn x -> + FunctionReturn {x with location = location_strip_file_hash x.location} + | Branching x -> + Branching {x with location = location_strip_file_hash x.location} + in + {waypoint_type} + in + let segment_strip_file_hash ({segment}: ViolationSequence.Segment.t): ViolationSequence.Segment.t = + {segment = List.map waypoint_strip_file_hash segment} + in let entry_type: EntryType.t = match entry_type with | LocationInvariant x -> @@ -42,6 +61,8 @@ struct PreconditionLoopInvariantCertificate {x with target = target_strip_file_hash x.target} | InvariantSet x -> InvariantSet {content = List.map invariant_strip_file_hash x.content} + | ViolationSequence x -> + ViolationSequence {content = List.map segment_strip_file_hash x.content} in {entry_type} From e286a48decb04641f2e9bbe7fa1b96d1ba845293 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 14 Jun 2024 13:50:46 +0300 Subject: [PATCH 3/9] Make YAML witness location function optional In updated version 2.0 schema. --- src/witness/yamlWitness.ml | 2 +- src/witness/yamlWitnessType.ml | 23 ++++++++++++++--------- 2 files changed, 15 insertions(+), 10 deletions(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 42254f30de..f5a8ae94e2 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -48,7 +48,7 @@ struct file_hash = sha256_file loc.file; line = loc.line; column = loc.column; - function_ = location_function; + function_ = Some location_function; } let invariant invariant: Invariant.t = { diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml index 1630e05b69..ff11fcbe9d 100644 --- a/src/witness/yamlWitnessType.ml +++ b/src/witness/yamlWitnessType.ml @@ -109,18 +109,23 @@ struct file_hash: string; line: int; column: int; - function_: string; + function_: string option; } [@@deriving ord] let to_yaml {file_name; file_hash; line; column; function_} = - `O [ - ("file_name", `String file_name); - ("file_hash", `String file_hash); - ("line", `Float (float_of_int line)); - ("column", `Float (float_of_int column)); - ("function", `String function_); - ] + `O ([ + ("file_name", `String file_name); + ("file_hash", `String file_hash); + ("line", `Float (float_of_int line)); + ("column", `Float (float_of_int column)); + ] @ match function_ with + | Some function_ -> [ + ("function", `String function_); + ] + | None -> + [] + ) let of_yaml y = let open GobYaml in @@ -128,7 +133,7 @@ struct and+ file_hash = y |> find "file_hash" >>= to_string and+ line = y |> find "line" >>= to_int and+ column = y |> find "column" >>= to_int - and+ function_ = y |> find "function" >>= to_string in + and+ function_ = y |> Yaml.Util.find "function" >>= option_map to_string in {file_name; file_hash; line; column; function_} end From 6a3569521a4dec529ceef50d82854db1ed350b0d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 14 Jun 2024 13:55:14 +0300 Subject: [PATCH 4/9] Make YAML witness location column optional In updated version 2.0 schema. --- src/analyses/unassumeAnalysis.ml | 22 +++++----------------- src/witness/yamlWitness.ml | 24 ++++++++++++------------ src/witness/yamlWitnessType.ml | 25 +++++++++++++++---------- 3 files changed, 32 insertions(+), 39 deletions(-) diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml index 265e9c6925..ae7a8bc9a8 100644 --- a/src/analyses/unassumeAnalysis.ml +++ b/src/analyses/unassumeAnalysis.ml @@ -71,18 +71,6 @@ struct | _ -> () ); - let loc_of_location (location: YamlWitnessType.Location.t): Cil.location = { - file = location.file_name; - line = location.line; - column = location.column; - byte = -1; - endLine = -1; - endColumn = -1; - endByte = -1; - synthetic = false; - } - in - let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.unassume")) with | Ok yaml -> yaml | Error (`Msg m) -> failwith ("Yaml_unix.of_file: " ^ m) @@ -123,7 +111,7 @@ struct in let unassume_location_invariant (location_invariant: YamlWitnessType.LocationInvariant.t) = - let loc = loc_of_location location_invariant.location in + let loc = YamlWitness.loc_of_location location_invariant.location in let inv = location_invariant.location_invariant.string in let msgLoc: M.Location.t = CilLocation loc in @@ -135,7 +123,7 @@ struct in let unassume_loop_invariant (loop_invariant: YamlWitnessType.LoopInvariant.t) = - let loc = loc_of_location loop_invariant.location in + let loc = YamlWitness.loc_of_location loop_invariant.location in let inv = loop_invariant.loop_invariant.string in let msgLoc: M.Location.t = CilLocation loc in @@ -185,7 +173,7 @@ struct in let unassume_precondition_loop_invariant (precondition_loop_invariant: YamlWitnessType.PreconditionLoopInvariant.t) = - let loc = loc_of_location precondition_loop_invariant.location in + let loc = YamlWitness.loc_of_location precondition_loop_invariant.location in let pre = precondition_loop_invariant.precondition.string in let inv = precondition_loop_invariant.loop_invariant.string in let msgLoc: M.Location.t = CilLocation loc in @@ -200,7 +188,7 @@ struct let unassume_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) = let unassume_location_invariant (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) = - let loc = loc_of_location location_invariant.location in + let loc = YamlWitness.loc_of_location location_invariant.location in let inv = location_invariant.value in let msgLoc: M.Location.t = CilLocation loc in @@ -212,7 +200,7 @@ struct in let unassume_loop_invariant (loop_invariant: YamlWitnessType.InvariantSet.LoopInvariant.t) = - let loc = loc_of_location loop_invariant.location in + let loc = YamlWitness.loc_of_location loop_invariant.location in let inv = loop_invariant.value in let msgLoc: M.Location.t = CilLocation loc in diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index f5a8ae94e2..cf6b1dfc44 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -47,7 +47,7 @@ struct file_name = loc.file; file_hash = sha256_file loc.file; line = loc.line; - column = loc.column; + column = Some loc.column; function_ = Some location_function; } @@ -515,6 +515,17 @@ struct end +let loc_of_location (location: YamlWitnessType.Location.t): Cil.location = { + file = location.file_name; + line = location.line; + column = Option.value location.column ~default:1; + byte = -1; + endLine = -1; + endColumn = -1; + endByte = -1; + synthetic = false; +} + module ValidationResult = struct (* constructor order is important for the chain lattice *) @@ -553,17 +564,6 @@ struct module InvariantParser = WitnessUtil.InvariantParser module VR = ValidationResult - let loc_of_location (location: YamlWitnessType.Location.t): Cil.location = { - file = location.file_name; - line = location.line; - column = location.column; - byte = -1; - endLine = -1; - endColumn = -1; - endByte = -1; - synthetic = false; - } - let validate () = let location_locator = Locator.create () in let loop_locator = Locator.create () in diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml index ff11fcbe9d..23a0343c18 100644 --- a/src/witness/yamlWitnessType.ml +++ b/src/witness/yamlWitnessType.ml @@ -108,7 +108,7 @@ struct file_name: string; file_hash: string; line: int; - column: int; + column: int option; function_: string option; } [@@deriving ord] @@ -118,21 +118,26 @@ struct ("file_name", `String file_name); ("file_hash", `String file_hash); ("line", `Float (float_of_int line)); - ("column", `Float (float_of_int column)); - ] @ match function_ with - | Some function_ -> [ - ("function", `String function_); - ] - | None -> - [] - ) + ] @ (match column with + | Some column -> [ + ("column", `Float (float_of_int column)); + ] + | None -> + [] + ) @ (match function_ with + | Some function_ -> [ + ("function", `String function_); + ] + | None -> + [] + )) let of_yaml y = let open GobYaml in let+ file_name = y |> find "file_name" >>= to_string and+ file_hash = y |> find "file_hash" >>= to_string and+ line = y |> find "line" >>= to_int - and+ column = y |> find "column" >>= to_int + and+ column = y |> Yaml.Util.find "column" >>= option_map to_int and+ function_ = y |> Yaml.Util.find "function" >>= option_map to_string in {file_name; file_hash; line; column; function_} end From b3dd140985c1db0e086bb42b51f5d5a6a045fc92 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 14 Jun 2024 14:03:04 +0300 Subject: [PATCH 5/9] Make YAML witness location file_hash optional Removed from version 2.0 schema. --- src/witness/yamlWitness.ml | 21 ++++++++++++++------- src/witness/yamlWitnessType.ml | 16 +++++++++++----- tests/util/yamlWitnessStrip.ml | 9 +++++++-- 3 files changed, 32 insertions(+), 14 deletions(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index cf6b1dfc44..d880663547 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -43,13 +43,20 @@ struct specification } - let location ~location:(loc: Cil.location) ~(location_function): Location.t = { - file_name = loc.file; - file_hash = sha256_file loc.file; - line = loc.line; - column = Some loc.column; - function_ = Some location_function; - } + let location ~location:(loc: Cil.location) ~(location_function): Location.t = + let file_hash = + match GobConfig.get_string "witness.yaml.format-version" with + | "0.1" -> Some (sha256_file loc.file) + | "2.0" -> None + | _ -> assert false + in + { + file_name = loc.file; + file_hash; + line = loc.line; + column = Some loc.column; + function_ = Some location_function; + } let invariant invariant: Invariant.t = { string = invariant; diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml index 23a0343c18..aabf551109 100644 --- a/src/witness/yamlWitnessType.ml +++ b/src/witness/yamlWitnessType.ml @@ -106,7 +106,7 @@ module Location = struct type t = { file_name: string; - file_hash: string; + file_hash: string option; line: int; column: int option; function_: string option; @@ -116,9 +116,15 @@ struct let to_yaml {file_name; file_hash; line; column; function_} = `O ([ ("file_name", `String file_name); - ("file_hash", `String file_hash); - ("line", `Float (float_of_int line)); - ] @ (match column with + ] @ (match file_hash with + | Some file_hash -> [ + ("file_hash", `String file_hash); + ] + | None -> + [] + ) @ [ + ("line", `Float (float_of_int line)); + ] @ (match column with | Some column -> [ ("column", `Float (float_of_int column)); ] @@ -135,7 +141,7 @@ struct let of_yaml y = let open GobYaml in let+ file_name = y |> find "file_name" >>= to_string - and+ file_hash = y |> find "file_hash" >>= to_string + and+ file_hash = y |> Yaml.Util.find "file_hash" >>= option_map to_string and+ line = y |> find "line" >>= to_int and+ column = y |> Yaml.Util.find "column" >>= option_map to_int and+ function_ = y |> Yaml.Util.find "function" >>= option_map to_string in diff --git a/tests/util/yamlWitnessStrip.ml b/tests/util/yamlWitnessStrip.ml index 8a5046d6ff..1a463d1390 100644 --- a/tests/util/yamlWitnessStrip.ml +++ b/tests/util/yamlWitnessStrip.ml @@ -10,8 +10,13 @@ struct let strip_file_hashes {entry_type} = let stripped_file_hash = "$FILE_HASH" in - let location_strip_file_hash location: Location.t = - {location with file_hash = stripped_file_hash} + let location_strip_file_hash (location: Location.t): Location.t = + let file_hash = + match location.file_hash with + | Some _ -> Some stripped_file_hash (* TODO: or just map to None always? *) + | None -> None + in + {location with file_hash} in let target_strip_file_hash target: Target.t = {target with file_hash = stripped_file_hash} From 28cff0f0917ecd5d2bd38972b6f0d66369b2d873 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 14 Jun 2024 14:10:45 +0300 Subject: [PATCH 6/9] Make YAML witness waypoint constraint format optional --- src/witness/yamlWitnessType.ml | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml index 159b0eedae..4fc2029801 100644 --- a/src/witness/yamlWitnessType.ml +++ b/src/witness/yamlWitnessType.ml @@ -449,20 +449,25 @@ struct struct type t = { value: string; - format: string; + format: string option; } [@@deriving ord] let to_yaml {value; format} = - `O [ - ("value", `String value); - ("format", `String format); - ] + `O ([ + ("value", `String value); + ] @ (match format with + | Some format -> [ + ("format", `String format); + ] + | None -> + [] + )) let of_yaml y = let open GobYaml in let+ value = y |> find "value" >>= to_string - and+ format = y |> find "format" >>= to_string in + and+ format = y |> Yaml.Util.find "format" >>= option_map to_string in {value; format} end @@ -593,8 +598,8 @@ struct let to_yaml {waypoint_type} = `O [ ("waypoint", `O ([ - ("type", `String (WaypointType.waypoint_type waypoint_type)); - ] @ WaypointType.to_yaml' waypoint_type) + ("type", `String (WaypointType.waypoint_type waypoint_type)); + ] @ WaypointType.to_yaml' waypoint_type) ) ] From 1bdb1aec3d0de987c83a3e3ff5ab0514bc965772 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 14 Jun 2024 14:58:32 +0300 Subject: [PATCH 7/9] Add primitive YAML violation_sequence refutation (issue #1301) --- src/config/options.schema.json | 3 ++- src/witness/yamlWitness.ml | 13 ++++++++++++- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 488fc494b0..95fb1a9ff5 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -2574,7 +2574,8 @@ "precondition_loop_invariant", "loop_invariant_certificate", "precondition_loop_invariant_certificate", - "invariant_set" + "invariant_set", + "violation_sequence" ] }, "default": [ diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index d880663547..36e1e2b589 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -802,6 +802,15 @@ struct None in + let validate_violation_sequence (violation_sequence: YamlWitnessType.ViolationSequence.t) = + (* TODO: update cnt-s appropriately (needs access to SV-COMP result pre-witness validation) *) + (* Nothing needs to be checked here! + If program is correct and we can prove it, we output true, which counts as refutation of violation witness. + If program is correct and we cannot prove it, we output unknown. + If program is incorrect, we output unknown. *) + None + in + match entry_type_enabled target_type, entry.entry_type with | true, LocationInvariant x -> validate_location_invariant x @@ -811,7 +820,9 @@ struct validate_precondition_loop_invariant x | true, InvariantSet x -> validate_invariant_set x - | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _) -> + | true, ViolationSequence x -> + validate_violation_sequence x + | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _ | ViolationSequence _) -> incr cnt_disabled; M.info_noloc ~category:Witness "disabled entry of type %s" target_type; None From c546f2df8208ac3ff22886e65f64f3eb84c8e044 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 14 Jun 2024 15:00:10 +0300 Subject: [PATCH 8/9] Add svcomp-validate conf for next SV-COMP Compared to svcomp24-validate: 1. Enables abortUnless (like svcomp over svcomp24). 2. Enables YAML violation_sequence validation. --- conf/svcomp-validate.json | 142 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 142 insertions(+) create mode 100644 conf/svcomp-validate.json diff --git a/conf/svcomp-validate.json b/conf/svcomp-validate.json new file mode 100644 index 0000000000..a234aeb0d5 --- /dev/null +++ b/conf/svcomp-validate.json @@ -0,0 +1,142 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless", + "unassume" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "malloc": { + "wrappers": [ + "kmalloc", + "__kmalloc", + "usb_alloc_urb", + "__builtin_alloca", + "kzalloc", + + "ldv_malloc", + + "kzalloc_node", + "ldv_zalloc", + "kmalloc_array", + "kcalloc", + + "ldv_xmalloc", + "ldv_xzalloc", + "ldv_calloc", + "ldv_kzalloc" + ] + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "termination", + "tmpSpecialAnalysis" + ] + }, + "widen": { + "tokens": true + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": false + }, + "yaml": { + "enabled": false, + "strict": true, + "format-version": "2.0", + "entry-types": [ + "location_invariant", + "loop_invariant", + "invariant_set", + "violation_sequence" + ], + "invariant-types": [ + "location_invariant", + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": true, + "other": true + } + }, + "pre": { + "enabled": false + } +} From fccc91efee6c2dc0ad92c3d82946e1b1e994d7d8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 14 Jun 2024 15:57:34 +0300 Subject: [PATCH 9/9] Add cram test for YAML violation witness refutation --- .../witness/violation.t/correct-hard.c | 9 +++ .../witness/violation.t/correct-hard.yml | 26 +++++++++ .../regression/witness/violation.t/correct.c | 5 ++ .../witness/violation.t/correct.yml | 26 +++++++++ .../witness/violation.t/incorrect.c | 6 ++ .../witness/violation.t/incorrect.yml | 26 +++++++++ tests/regression/witness/violation.t/run.t | 57 +++++++++++++++++++ 7 files changed, 155 insertions(+) create mode 100644 tests/regression/witness/violation.t/correct-hard.c create mode 100644 tests/regression/witness/violation.t/correct-hard.yml create mode 100644 tests/regression/witness/violation.t/correct.c create mode 100644 tests/regression/witness/violation.t/correct.yml create mode 100644 tests/regression/witness/violation.t/incorrect.c create mode 100644 tests/regression/witness/violation.t/incorrect.yml create mode 100644 tests/regression/witness/violation.t/run.t diff --git a/tests/regression/witness/violation.t/correct-hard.c b/tests/regression/witness/violation.t/correct-hard.c new file mode 100644 index 0000000000..ce2b50a0c0 --- /dev/null +++ b/tests/regression/witness/violation.t/correct-hard.c @@ -0,0 +1,9 @@ +void reach_error(){} +extern int __VERIFIER_nondet_int(); + +int main() { + int x = __VERIFIER_nondet_int(); + if (x != x) + reach_error(); + return 0; +} diff --git a/tests/regression/witness/violation.t/correct-hard.yml b/tests/regression/witness/violation.t/correct-hard.yml new file mode 100644 index 0000000000..b8af2c2193 --- /dev/null +++ b/tests/regression/witness/violation.t/correct-hard.yml @@ -0,0 +1,26 @@ +- entry_type: violation_sequence + metadata: + format_version: "2.0" + uuid: 4412af70-389a-475e-849c-e57e5b92019e + creation_time: 2024-06-14T15:35:00+03:00 + producer: + name: Simmo Saan + version: n/a + task: + input_files: + - correct-hard.c + input_file_hashes: + correct-hard.c: 5cc49c1ce5a9aef64286c2a6e57f6955c5f4f9b19b43056507ae87a802802447 + specification: G ! call(reach_error()) + data_model: ILP32 + language: C + content: + - segment: + - waypoint: + type: target + action: follow + location: + file_name: correct-hard.c + line: 7 + column: 5 + function: main diff --git a/tests/regression/witness/violation.t/correct.c b/tests/regression/witness/violation.t/correct.c new file mode 100644 index 0000000000..30f58a2f7e --- /dev/null +++ b/tests/regression/witness/violation.t/correct.c @@ -0,0 +1,5 @@ +void reach_error(){} + +int main() { + return 0; +} diff --git a/tests/regression/witness/violation.t/correct.yml b/tests/regression/witness/violation.t/correct.yml new file mode 100644 index 0000000000..1f1d4f41da --- /dev/null +++ b/tests/regression/witness/violation.t/correct.yml @@ -0,0 +1,26 @@ +- entry_type: violation_sequence + metadata: + format_version: "2.0" + uuid: 4412af70-389a-475e-849c-e57e5b92019d + creation_time: 2024-06-14T15:35:00+03:00 + producer: + name: Simmo Saan + version: n/a + task: + input_files: + - correct.c + input_file_hashes: + correct.c: 6f760cf7f33fc152738bf3514fe623cc94e52cad9ddc2f0e744595ce0de07530 + specification: G ! call(reach_error()) + data_model: ILP32 + language: C + content: + - segment: + - waypoint: + type: target + action: follow + location: + file_name: correct.c + line: 4 + column: 3 + function: main diff --git a/tests/regression/witness/violation.t/incorrect.c b/tests/regression/witness/violation.t/incorrect.c new file mode 100644 index 0000000000..ff56fa2ef4 --- /dev/null +++ b/tests/regression/witness/violation.t/incorrect.c @@ -0,0 +1,6 @@ +void reach_error(){} + +int main() { + reach_error(); + return 0; +} diff --git a/tests/regression/witness/violation.t/incorrect.yml b/tests/regression/witness/violation.t/incorrect.yml new file mode 100644 index 0000000000..dd57ce3ca1 --- /dev/null +++ b/tests/regression/witness/violation.t/incorrect.yml @@ -0,0 +1,26 @@ +- entry_type: violation_sequence + metadata: + format_version: "2.0" + uuid: 4412af70-389a-475e-849c-e57e5b92019c + creation_time: 2024-06-14T15:35:00+03:00 + producer: + name: Simmo Saan + version: n/a + task: + input_files: + - incorrect.c + input_file_hashes: + incorrect.c: 1af4fd9e76418e4b95af9950b58248127e7c2d9eb791e1c9b92da53952e0fca2 + specification: G ! call(reach_error()) + data_model: ILP32 + language: C + content: + - segment: + - waypoint: + type: target + action: follow + location: + file_name: incorrect.c + line: 4 + column: 3 + function: main diff --git a/tests/regression/witness/violation.t/run.t b/tests/regression/witness/violation.t/run.t new file mode 100644 index 0000000000..1fc408635e --- /dev/null +++ b/tests/regression/witness/violation.t/run.t @@ -0,0 +1,57 @@ +Violation witness for a correct program can be refuted by proving the program correct and returning `true`: + + $ goblint --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" correct.c --set witness.yaml.validate correct.yml + [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) ) + [Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (correct.c:1:1-1:20) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 2 + dead: 1 (1 in uncalled functions) + total lines: 3 + [Info][Witness] witness validation summary: + confirmed: 0 + unconfirmed: 0 + refuted: 0 + error: 0 + unchecked: 0 + unsupported: 0 + disabled: 0 + total validation entries: 0 + SV-COMP result: true + +If a correct progtam cannot be proven correct, return `unknown` for the violation witness: + + $ goblint --set ana.activated[-] expRelation --enable ana.sv-comp.functions --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" correct-hard.c --set witness.yaml.validate correct-hard.yml + [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) ) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Info][Witness] witness validation summary: + confirmed: 0 + unconfirmed: 0 + refuted: 0 + error: 0 + unchecked: 0 + unsupported: 0 + disabled: 0 + total validation entries: 0 + SV-COMP result: unknown + +Violation witness for an incorrect program cannot be proven correct, so return `unknown`: + + $ goblint --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" incorrect.c --set witness.yaml.validate incorrect.yml + [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) ) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 4 + dead: 0 + total lines: 4 + [Info][Witness] witness validation summary: + confirmed: 0 + unconfirmed: 0 + refuted: 0 + error: 0 + unchecked: 0 + unsupported: 0 + disabled: 0 + total validation entries: 0 + SV-COMP result: unknown