From 3d5dc4365937f258b9331ad3598599ae02e5efb0 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 29 Sep 2023 17:44:39 +0100 Subject: [PATCH 1/2] Define coverage blocks so as to be terminated by assumptions If a coverage block has an assumption in the middle then then an assertion at the end of the block could be reported as covered but actually be unreachable due to the preceding the assumption. Therefore coverage blocks should be terminated by assumptions in order to ensure than coverage reporting is accurate. --- regression/cbmc-cover/location12/test.desc | 5 +++-- regression/cbmc-cover/location15/test.desc | 3 ++- regression/cbmc-cover/location16/test.desc | 5 +++-- regression/cbmc-cover/location2/test.desc | 4 ++-- regression/cbmc-cover/simple_assert/test.desc | 2 +- .../test-no-failed-assertions.desc | 12 +++++++++--- src/goto-instrument/cover_basic_blocks.cpp | 5 +++-- 7 files changed, 23 insertions(+), 13 deletions(-) diff --git a/regression/cbmc-cover/location12/test.desc b/regression/cbmc-cover/location12/test.desc index bac822b042c..6cc5084011f 100644 --- a/regression/cbmc-cover/location12/test.desc +++ b/regression/cbmc-cover/location12/test.desc @@ -7,7 +7,8 @@ main.c ^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$ ^\[foo.coverage.1\] file main.c line 3 function foo block 1.*: SATISFIED$ ^\[foo.coverage.2\] file main.c line 4 function foo block 2.*: FAILED$ -^\[foo.coverage.3\] file main.c line 5 function foo block 3.*: SATISFIED$ -^\*\* 4 of 5 covered \(80.0%\) +^\[foo.coverage.3\] file main.c line 5 function foo block 3.*: FAILED$ +^\[foo.coverage.4\] file main.c line 5 function foo block 4.*: SATISFIED$ +^\*\* 4 of 6 covered \(66.7%\) -- ^warning: ignoring diff --git a/regression/cbmc-cover/location15/test.desc b/regression/cbmc-cover/location15/test.desc index b48161384c3..90cf7a9f26d 100644 --- a/regression/cbmc-cover/location15/test.desc +++ b/regression/cbmc-cover/location15/test.desc @@ -6,7 +6,8 @@ main.c ^\[main.coverage.1\] file main.c line 10 function main block 1.*: SATISFIED$ ^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$ ^\[main.coverage.3\] file main.c line 13 function main block 3.*: FAILED$ -^\[main.coverage.4\] file main.c line 16 function main block 4.*: SATISFIED$ +^\[main.coverage.4\] file main.c line 14 function main block 4.*: FAILED$ +^\[main.coverage.5\] file main.c line 16 function main block 5.*: SATISFIED$ ^\[foo.coverage.1\] file main.c line 5 function foo block 1.*: FAILED$ ^\*\* 3 of \d+ covered -- diff --git a/regression/cbmc-cover/location16/test.desc b/regression/cbmc-cover/location16/test.desc index 74d7080448c..40e65248f26 100644 --- a/regression/cbmc-cover/location16/test.desc +++ b/regression/cbmc-cover/location16/test.desc @@ -9,7 +9,8 @@ main.c ^\[func.coverage.2\] file main.c line 6 function func block 2.*: FAILED$ ^\[func.coverage.3\] file main.c line 8 function func block 3.*: FAILED$ ^\[func.coverage.4\] file main.c line 12 function func block 4.*: FAILED$ -^\[func.coverage.5\] file main.c line 15 function func block 5.*: SATISFIED$ -^\*\* 4 of 7 covered \(57.1%\) +^\[func.coverage.5\] file main.c line 14 function func block 5.*: FAILED$ +^\[func.coverage.6\] file main.c line 15 function func block 6.*: SATISFIED$ +^\*\* 4 of 8 covered \(50.0%\) -- ^warning: ignoring diff --git a/regression/cbmc-cover/location2/test.desc b/regression/cbmc-cover/location2/test.desc index 747ff0c5800..817de5431b9 100644 --- a/regression/cbmc-cover/location2/test.desc +++ b/regression/cbmc-cover/location2/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[main.coverage.1\] file main.c line 9 function main block 1 \(lines main.c:main:9,10\): SATISFIED$ -^\[main.coverage.2\] file main.c line 11 function main block 2 \(lines main.c:main:11\): SATISFIED$ -^\*\* 2 of 2 covered \(100.0%\) +^\[main.coverage.3\] file main.c line 11 function main block 3 \(lines main.c:main:11\): SATISFIED$ +^\*\* 3 of 3 covered \(100.0%\) -- ^warning: ignoring main.c::5 diff --git a/regression/cbmc-cover/simple_assert/test.desc b/regression/cbmc-cover/simple_assert/test.desc index d3fac6c4c46..dfdc0dee6f9 100644 --- a/regression/cbmc-cover/simple_assert/test.desc +++ b/regression/cbmc-cover/simple_assert/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[main\.coverage\.1\] .* function main block 1.*: SATISFIED$ -(1 of 1|3 of 3) covered \(100\.0%\)$ +(1 of 1|2 of 2|3 of 3) covered \(100\.0%\)$ -- ^warning: ignoring ^CONVERSION ERROR$ diff --git a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc index 0544dcdb715..1d0b8b404bc 100644 --- a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc +++ b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc @@ -1,9 +1,15 @@ CORE paths-lifo-expected-failure test.c --cover location --pointer-check --malloc-may-fail --malloc-fail-null -\[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:17,18\): SATISFIED -\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:15\): FAILED -\[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12,14\): SATISFIED +\[main\.coverage\.10\] file test\.c line \d+ function main block 10 \(lines test\.c:main:17,18\): SATISFIED +\[main\.coverage\.9\] file test\.c line \d+ function main block 9 \(lines test\.c:main:15\): FAILED +\[main\.coverage\.8\] file test\.c line \d+ function main block 8 \(lines test\.c:main:12,14\): SATISFIED +\[main\.coverage\.7\] file test\.c line \d+ function main block 7 \(lines test\.c:main:12\): SATISFIED +\[main\.coverage\.6\] file test\.c line \d+ function main block 6 \(lines test\.c:main:12\): SATISFIED +\[main\.coverage\.5\] file test\.c line \d+ function main block 5 \(lines test\.c:main:12\): SATISFIED +\[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:12\): SATISFIED +\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:12\): SATISFIED +\[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12\): SATISFIED \[main\.coverage\.1\] file test\.c line \d+ function main block 1 \(lines test\.c:main:5\): SATISFIED ^EXIT=0$ ^SIGNAL=0$ diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp index 81ff18b6b11..466dddfe813 100644 --- a/src/goto-instrument/cover_basic_blocks.cpp +++ b/src/goto-instrument/cover_basic_blocks.cpp @@ -73,10 +73,11 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program) } next_is_target = -#if 0 - // Disabled for being too messy +#if 1 + // Previously disabled for being too messy. it->is_goto() || it->is_function_call() || it->is_assume(); #else + // Disabled for being misleading. it->is_goto() || it->is_function_call(); #endif } From e6c4e1962662839a6fc6224221e3f1110ac67682 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 29 Sep 2023 13:50:56 +0100 Subject: [PATCH 2/2] Add tests of the affect of assumptions on coverage blocks --- regression/cbmc-cover/location-assume/end.c | 9 +++++++++ regression/cbmc-cover/location-assume/end.desc | 17 +++++++++++++++++ regression/cbmc-cover/location-assume/middle.c | 11 +++++++++++ .../cbmc-cover/location-assume/middle.desc | 15 +++++++++++++++ 4 files changed, 52 insertions(+) create mode 100644 regression/cbmc-cover/location-assume/end.c create mode 100644 regression/cbmc-cover/location-assume/end.desc create mode 100644 regression/cbmc-cover/location-assume/middle.c create mode 100644 regression/cbmc-cover/location-assume/middle.desc diff --git a/regression/cbmc-cover/location-assume/end.c b/regression/cbmc-cover/location-assume/end.c new file mode 100644 index 00000000000..0429196a1a1 --- /dev/null +++ b/regression/cbmc-cover/location-assume/end.c @@ -0,0 +1,9 @@ +#include + +void main() +{ + int i; + int *p = &i; + int j; + __CPROVER_assume(j == 1 / (*p)); +} diff --git a/regression/cbmc-cover/location-assume/end.desc b/regression/cbmc-cover/location-assume/end.desc new file mode 100644 index 00000000000..b89e0ead3be --- /dev/null +++ b/regression/cbmc-cover/location-assume/end.desc @@ -0,0 +1,17 @@ +CORE +end.c +--pointer-check --div-by-zero-check --cover location +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file end.c line 5 function main block 1 \(lines end\.c:main:5-8\): SATISFIED$ +^\[main.coverage.2\] file end.c line 8 function main block 2 \(lines end\.c:main:8\): SATISFIED$ +^\[main.coverage.3\] file end.c line 8 function main block 3 \(lines end\.c:main:8\): SATISFIED$ +^\[main.coverage.4\] file end.c line 8 function main block 4 \(lines end\.c:main:8\): SATISFIED$ +^\[main.coverage.5\] file end.c line 9 function main block 5 \(lines end\.c:main:9\): SATISFIED$ +^\*\* 5 of 5 covered \(100.0%\) +-- +^warning: ignoring +-- +Test that in the case where multiple assertions are added on the same line of +code due to the addition of instrumentation checks, these do not result in +further splitting blocks. diff --git a/regression/cbmc-cover/location-assume/middle.c b/regression/cbmc-cover/location-assume/middle.c new file mode 100644 index 00000000000..64da9f6a25d --- /dev/null +++ b/regression/cbmc-cover/location-assume/middle.c @@ -0,0 +1,11 @@ +#include + +int main() +{ + int i; + int j; + j = i; + __CPROVER_assume(0); + j = i + 2; + return 0; +} diff --git a/regression/cbmc-cover/location-assume/middle.desc b/regression/cbmc-cover/location-assume/middle.desc new file mode 100644 index 00000000000..650c62b33b1 --- /dev/null +++ b/regression/cbmc-cover/location-assume/middle.desc @@ -0,0 +1,15 @@ +CORE +middle.c +--cover location +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file middle.c line 5 function main block 1 \(lines middle\.c:main:5-8\): SATISFIED$ +^\[main.coverage.2\] file middle.c line 9 function main block 2 \(lines middle\.c:main:9-11\): FAILED$ +^\*\* 1 of 2 covered \(50.0%\) +-- +^warning: ignoring +-- +This test confirms that assumptions in the middle of what would otherwise be a +single blocks without control flow will cause the code to be split into 2 +coverage blocks. This is required as an unsatisfiable assumption can result in +the following statements being unreachable.