From 4693734ea303882d38849ab0483937cac4bc6bf6 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 18 Jul 2023 15:26:20 +0100 Subject: [PATCH] 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 bac822b042c7..6cc5084011fa 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 b48161384c3d..90cf7a9f26d1 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 74d7080448c9..40e65248f262 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 747ff0c58009..817de5431b91 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 d3fac6c4c466..dfdc0dee6f96 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 9f7882b842f8..efa75799614a 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 new-smt-backend 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 81ff18b6b119..c290a1c3ce93 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; } }