From 9e3fd5d26f0488b950dfae59a6a4135e006e28e0 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 18 Jul 2023 15:26:20 +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 | 7 +++-- src/goto-instrument/cover_basic_blocks.cpp | 30 ++++++++++++++----- 7 files changed, 37 insertions(+), 19 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..7754c1e36e6 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,10 @@ 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\.5\] file test\.c line \d+ function main block 5 \(lines test\.c:main:17,18\): SATISFIED +\[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:15\): FAILED +\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:12,14\): 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..c290a1c3ce9 100644 --- a/src/goto-instrument/cover_basic_blocks.cpp +++ b/src/goto-instrument/cover_basic_blocks.cpp @@ -29,15 +29,34 @@ optionalt cover_basic_blockst::continuation_of_block( return {}; } +static bool +same_source_line(const source_locationt &a, const source_locationt &b) +{ + return a.get_file() == b.get_file() && a.get_line() == b.get_line(); +} + cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program) { bool next_is_target = true; + const goto_programt::instructiont *preceding_assume = nullptr; std::size_t current_block = 0; forall_goto_program_instructions(it, goto_program) { + // For the purposes of coverage blocks, multiple consecutive assume + // instructions with the same source location are considered to be part of + // the same block. Assumptions should terminate a block, as subsequent + // instructions may be unreachable. However check instrumentation passes + // may insert multiple assertions in the same program location. Therefore + // these are combined for reasons of readability of the coverage output. + bool end_of_assume_group = + preceding_assume && + !(it->is_assume() && + same_source_line( + preceding_assume->source_location(), it->source_location())); + // Is it a potential beginning of a block? - if(next_is_target || it->is_target()) + if(next_is_target || it->is_target() || end_of_assume_group) { if(auto block_number = continuation_of_block(it, block_map)) { @@ -72,13 +91,8 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program) block_info.source_location = it->source_location(); } - next_is_target = -#if 0 - // Disabled for being too messy - it->is_goto() || it->is_function_call() || it->is_assume(); -#else - it->is_goto() || it->is_function_call(); -#endif + next_is_target = it->is_goto() || it->is_function_call(); + preceding_assume = it->is_assume() ? &*it : nullptr; } } From ac26185fb43f7508945f2efa2597342d694df12c 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 | 14 ++++++++++++++ regression/cbmc-cover/location-assume/middle.c | 11 +++++++++++ regression/cbmc-cover/location-assume/middle.desc | 15 +++++++++++++++ 4 files changed, 49 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..4d1bffdc81c --- /dev/null +++ b/regression/cbmc-cover/location-assume/end.desc @@ -0,0 +1,14 @@ +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 9 function main block 2 \(lines end\.c:main:9\): SATISFIED$ +^\*\* 2 of 2 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.