From fccc91efee6c2dc0ad92c3d82946e1b1e994d7d8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 14 Jun 2024 15:57:34 +0300 Subject: [PATCH] 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