Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Define coverage blocks so as to be terminated by assumptions #7810

Merged
merged 2 commits into from
Dec 12, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions regression/cbmc-cover/location-assume/end.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
#include <assert.h>

void main()
{
int i;
int *p = &i;
int j;
__CPROVER_assume(j == 1 / (*p));
}
14 changes: 14 additions & 0 deletions regression/cbmc-cover/location-assume/end.desc
Original file line number Diff line number Diff line change
@@ -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.
11 changes: 11 additions & 0 deletions regression/cbmc-cover/location-assume/middle.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
#include <assert.h>

int main()
{
int i;
int j;
j = i;
__CPROVER_assume(0);
j = i + 2;
return 0;
}
15 changes: 15 additions & 0 deletions regression/cbmc-cover/location-assume/middle.desc
Original file line number Diff line number Diff line change
@@ -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.
5 changes: 3 additions & 2 deletions regression/cbmc-cover/location12/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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
3 changes: 2 additions & 1 deletion regression/cbmc-cover/location15/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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
--
Expand Down
5 changes: 3 additions & 2 deletions regression/cbmc-cover/location16/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions regression/cbmc-cover/location2/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cover/simple_assert/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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$
Expand Down
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
30 changes: 22 additions & 8 deletions src/goto-instrument/cover_basic_blocks.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -29,15 +29,34 @@ optionalt<std::size_t> 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))
{
Expand Down Expand Up @@ -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;
}
}

Expand Down