Skip to content

Commit 0512088

Browse files
Tuttletautschnig
Tuttle
authored and
tautschnig
committed
Added basic block source lines to source_locationt
Block coverage obtained with "cbmc --cover locations" now reports the file name and line number of every line of source code contributing to a basic block in the "description" field of the xml output. (The lines contributing to a block can come from multiple files via function inlining and definitions in include files, so reporting line numbers alone is not sufficient.)
1 parent 7f2ff2c commit 0512088

File tree

26 files changed

+279
-46
lines changed

26 files changed

+279
-46
lines changed

‎regression/cbmc-cover/block-coverage-report1/main.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
int main()
2+
{
3+
int x;
4+
5+
if(x < 0)
6+
return 0;
7+
else
8+
return 1;
9+
}

‎regression/cbmc-cover/block-coverage-report1/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--cover location
4+
block 1 \(lines main.c:main:3,5\): SATISFIED
5+
block 2 \(lines main.c:main:6\): SATISFIED
6+
block 3 \(lines main.c:main:6,9\): FAILED
7+
block 4 \(lines main.c:main:8\): SATISFIED
8+
block 5 \(lines main.c:main:9\): SATISFIED
9+
--

‎regression/cbmc-cover/block-coverage-report2/main.c

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
// This is supposed to be testing basic blocks with inlining,
2+
// but cbmc has now turned off inlining by default.
3+
4+
inline int foo(int x)
5+
{
6+
int y;
7+
y = x + 1;
8+
return y;
9+
}
10+
11+
main()
12+
{
13+
int x;
14+
x = 10;
15+
while(x)
16+
{
17+
int y;
18+
y = foo(x);
19+
if(y < 5)
20+
break;
21+
x--;
22+
}
23+
24+
return;
25+
}

‎regression/cbmc-cover/block-coverage-report2/test.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--cover location
4+
block 1 \(lines main.c:main:13,14\): SATISFIED
5+
block 2 \(lines main.c:main:15\): SATISFIED
6+
block 3 \(lines main.c:main:17,18\): SATISFIED
7+
block 4 \(lines main.c:main:18,19\): SATISFIED
8+
block 5 \(lines main.c:main:20\): SATISFIED
9+
block 6 \(lines main.c:main:15,21,22\): SATISFIED
10+
block 7 \(lines main.c:main:24,25\): SATISFIED
11+
block 1 \(lines main.c:foo:6,7,8,9\): SATISFIED
12+
--

‎regression/cbmc-cover/block-coverage-report3/main.c

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
void main()
2+
{
3+
int x = 0;
4+
while(x < 3)
5+
{
6+
x++;
7+
}
8+
}

‎regression/cbmc-cover/block-coverage-report3/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--cover location --unwind 1
4+
block 1 \(lines main.c:main:3\): SATISFIED
5+
block 2 \(lines main.c:main:4\): SATISFIED
6+
block 3 \(lines main.c:main:4,6\): SATISFIED
7+
block 4 \(lines main.c:main:8\): FAILED
8+
--

‎regression/cbmc-cover/block-coverage-report4/main.c

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
void main()
2+
{
3+
int x = 0;
4+
while(x < 3)
5+
{
6+
x++;
7+
}
8+
}

‎regression/cbmc-cover/block-coverage-report4/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--cover location --unwind 4
4+
block 1 \(lines main.c:main:3\): SATISFIED
5+
block 2 \(lines main.c:main:4\): SATISFIED
6+
block 3 \(lines main.c:main:4,6\): SATISFIED
7+
block 4 \(lines main.c:main:8\): SATISFIED
8+
--

‎regression/cbmc-cover/location1/test.desc

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ main.c
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 3 function main block 1: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 10 function main block 2: SATISFIED$
8-
^\[main.coverage.3\] file main.c line 13 function main block 3: SATISFIED$
9-
^\[main.coverage.4\] file main.c line 15 function main block 4: FAILED$
10-
^\[main.coverage.5\] file main.c line 17 function main block 5: SATISFIED$
6+
^\[main.coverage.1\] file main.c line 3 function main block 1.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 13 function main block 3.*: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 15 function main block 4.*: FAILED$
10+
^\[main.coverage.5\] file main.c line 17 function main block 5.*: SATISFIED$
1111
^\*\* 4 of 5 covered \(80.0%\)
1212
--
1313
^warning: ignoring

‎regression/cbmc-cover/location11/test.desc

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,15 @@ main.c
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 9 function main block 1: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 11 function main block 2: FAILED$
8-
^\[main.coverage.3\] file main.c line 11 function main block 3: FAILED$
9-
^\[main.coverage.4\] file main.c line 13 function main block 4: SATISFIED$
10-
^\[main.coverage.5\] file main.c line 15 function main block 5: SATISFIED$
11-
^\[main.coverage.6\] file main.c line 16 function main block 6: SATISFIED$
12-
^\[main.coverage.7\] file main.c line 18 function main block 7: FAILED$
13-
^\[main.coverage.8\] file main.c line 20 function main block 8: SATISFIED$
14-
^\[myfunc.coverage.1\] file main.c line 3 function myfunc block 1: FAILED$
6+
^\[main.coverage.1\] file main.c line 9 function main block 1.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 11 function main block 2.*: FAILED$
8+
^\[main.coverage.3\] file main.c line 11 function main block 3.*: FAILED$
9+
^\[main.coverage.4\] file main.c line 13 function main block 4.*: SATISFIED$
10+
^\[main.coverage.5\] file main.c line 15 function main block 5.*: SATISFIED$
11+
^\[main.coverage.6\] file main.c line 16 function main block 6.*: SATISFIED$
12+
^\[main.coverage.7\] file main.c line 18 function main block 7.*: FAILED$
13+
^\[main.coverage.8\] file main.c line 20 function main block 8.*: SATISFIED$
14+
^\[myfunc.coverage.1\] file main.c line 3 function myfunc block 1.*: FAILED$
1515
^\*\* 5 of 9 covered \(55.6%\)
1616
--
1717
^warning: ignoring

‎regression/cbmc-cover/location12/test.desc

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ main.c
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 9 function main block 1: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 10 function main block 2: SATISFIED$
8-
^\[foo.coverage.1\] file main.c line 3 function foo block 1: SATISFIED$
9-
^\[foo.coverage.2\] file main.c line 4 function foo block 2: FAILED$
10-
^\[foo.coverage.3\] file main.c line 5 function foo block 3: SATISFIED$
6+
^\[main.coverage.1\] file main.c line 9 function main block 1.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$
8+
^\[foo.coverage.1\] file main.c line 3 function foo block 1.*: SATISFIED$
9+
^\[foo.coverage.2\] file main.c line 4 function foo block 2.*: FAILED$
10+
^\[foo.coverage.3\] file main.c line 5 function foo block 3.*: SATISFIED$
1111
^\*\* 4 of 5 covered \(80.0%\)
1212
--
1313
^warning: ignoring

‎regression/cbmc-cover/location13/test.desc

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,13 @@ main.c
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 14 function main block 1: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 15 function main block 2: SATISFIED$
8-
^\[myfunc.coverage.1\] file main.c line 3 function myfunc block 1: FAILED$
9-
^\[foo.coverage.1\] file main.c line 8 function foo block 1: SATISFIED$
10-
^\[foo.coverage.2\] file main.c line 9 function foo block 2: FAILED$
11-
^\[foo.coverage.3\] file main.c line 10 function foo block 3: FAILED$
12-
^\[foo.coverage.4\] file main.c line 10 function foo block 4: SATISFIED$
6+
^\[main.coverage.1\] file main.c line 14 function main block 1.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 15 function main block 2.*: SATISFIED$
8+
^\[myfunc.coverage.1\] file main.c line 3 function myfunc block 1.*: FAILED$
9+
^\[foo.coverage.1\] file main.c line 8 function foo block 1.*: SATISFIED$
10+
^\[foo.coverage.2\] file main.c line 9 function foo block 2.*: FAILED$
11+
^\[foo.coverage.3\] file main.c line 10 function foo block 3.*: FAILED$
12+
^\[foo.coverage.4\] file main.c line 10 function foo block 4.*: SATISFIED$
1313
^\*\* 4 of 7 covered \(57.1%\)
1414
--
1515
^warning: ignoring

‎regression/cbmc-cover/location14/test.desc

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ main.c
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 8 function main block 1: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 12 function main block 2: FAILED$
8-
^\[main.coverage.3\] file main.c line 12 function main block 3: FAILED$
9-
^\[main.coverage.4\] file main.c line 13 function main block 4: SATISFIED$
10-
^\[foo.coverage.1\] file main.c line 3 function foo block 1: FAILED$
6+
^\[main.coverage.1\] file main.c line 8 function main block 1.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 12 function main block 2.*: FAILED$
8+
^\[main.coverage.3\] file main.c line 12 function main block 3.*: FAILED$
9+
^\[main.coverage.4\] file main.c line 13 function main block 4.*: SATISFIED$
10+
^\[foo.coverage.1\] file main.c line 3 function foo block 1.*: FAILED$
1111
^\*\* 2 of 5 covered \(40.0%\)
1212
--
1313
^warning: ignoring

‎regression/cbmc-cover/location15/test.desc

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ main.c
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 10 function main block 1: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 11 function main block 2: SATISFIED$
8-
^\[main.coverage.3\] file main.c line 13 function main block 3: FAILED$
9-
^\[main.coverage.4\] file main.c line 16 function main block 4: SATISFIED$
10-
^\[foo.coverage.1\] file main.c line 5 function foo block 1: FAILED$
6+
^\[main.coverage.1\] file main.c line 10 function main block 1.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 11 function main block 2.*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 13 function main block 3.*: FAILED$
9+
^\[main.coverage.4\] file main.c line 16 function main block 4.*: SATISFIED$
10+
^\[foo.coverage.1\] file main.c line 5 function foo block 1.*: FAILED$
1111
^\*\* 3 of 5 covered \(60.0%\)
1212
--
1313
^warning: ignoring

‎regression/cbmc-cover/location16/test.desc

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,13 @@ main.c
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 19 function main block 1: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 20 function main block 2: SATISFIED$
8-
^\[func.coverage.1\] file main.c line 3 function func block 1: SATISFIED$
9-
^\[func.coverage.2\] file main.c line 6 function func block 2: FAILED$
10-
^\[func.coverage.3\] file main.c line 8 function func block 3: FAILED$
11-
^\[func.coverage.4\] file main.c line 12 function func block 4: FAILED$
12-
^\[func.coverage.5\] file main.c line 15 function func block 5: SATISFIED$
6+
^\[main.coverage.1\] file main.c line 19 function main block 1.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 20 function main block 2.*: SATISFIED$
8+
^\[func.coverage.1\] file main.c line 3 function func block 1.*: SATISFIED$
9+
^\[func.coverage.2\] file main.c line 6 function func block 2.*: FAILED$
10+
^\[func.coverage.3\] file main.c line 8 function func block 3.*: FAILED$
11+
^\[func.coverage.4\] file main.c line 12 function func block 4.*: FAILED$
12+
^\[func.coverage.5\] file main.c line 15 function func block 5.*: SATISFIED$
1313
^\*\* 4 of 7 covered \(57.1%\)
1414
--
1515
^warning: ignoring

‎regression/cbmc-cover/simple_assert/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ main.c
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main\.coverage\.1\] .* function main block 1: SATISFIED$
6+
^\[main\.coverage\.1\] .* function main block 1.*: SATISFIED$
77
(1 of 1|3 of 3) covered \(100\.0%\)$
88
--
99
^warning: ignoring
1010
^CONVERSION ERROR$
11-
^\[main\.coverage\..\] .* function main block .: FAILED$
11+
^\[main\.coverage\..\] .* function main block .*: FAILED$
1212
--
1313
On Windows/Visual Studio, "assert" does not introduce any branching.

‎src/cbmc/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
2626
../pointer-analysis/add_failed_symbols$(OBJEXT) \
2727
../pointer-analysis/rewrite_index$(OBJEXT) \
2828
../pointer-analysis/goto_program_dereference$(OBJEXT) \
29+
../goto-instrument/source_lines$(OBJEXT) \
2930
../goto-instrument/cover$(OBJEXT) \
3031
../goto-instrument/cover_basic_blocks$(OBJEXT) \
3132
../goto-instrument/cover_filter$(OBJEXT) \

‎src/goto-diff/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
1414
../goto-programs/goto-programs$(LIBEXT) \
1515
../assembler/assembler$(LIBEXT) \
1616
../pointer-analysis/pointer-analysis$(LIBEXT) \
17+
../goto-instrument/source_lines$(OBJEXT) \
1718
../goto-instrument/cover$(OBJEXT) \
1819
../goto-instrument/cover_basic_blocks$(OBJEXT) \
1920
../goto-instrument/cover_filter$(OBJEXT) \

‎src/goto-instrument/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,7 @@ SRC = accelerate/accelerate.cpp \
5757
rw_set.cpp \
5858
show_locations.cpp \
5959
skip_loops.cpp \
60+
source_lines.cpp \
6061
splice_call.cpp \
6162
stack_depth.cpp \
6263
thread_instrumentation.cpp \

‎src/goto-instrument/cover_basic_blocks.cpp

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,10 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
6161
// update lines belonging to block
6262
const irep_idt &line = it->source_location.get_line();
6363
if(!line.empty())
64+
{
6465
block_info.lines.insert(unsafe_string2unsigned(id2string(line)));
66+
block_info.source_lines.insert(it->source_location);
67+
}
6568

6669
// set representative program location to instrument
6770
if(
@@ -84,7 +87,10 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
8487
}
8588

8689
for(auto &block_info : block_infos)
90+
{
8791
update_covered_lines(block_info);
92+
update_source_lines(block_info);
93+
}
8894
}
8995

9096
std::size_t cover_basic_blockst::block_of(goto_programt::const_targett t) const
@@ -162,6 +168,17 @@ void cover_basic_blockst::update_covered_lines(block_infot &block_info)
162168
block_info.source_location.set_basic_block_covered_lines(covered_lines);
163169
}
164170

171+
void cover_basic_blockst::update_source_lines(block_infot &block_info)
172+
{
173+
if(block_info.source_location.is_nil())
174+
return;
175+
176+
const auto &source_lines = block_info.source_lines;
177+
std::string str = source_lines.to_string();
178+
INVARIANT(!str.empty(), "source lines set must not be empty");
179+
block_info.source_location.set_basic_block_source_lines(str);
180+
}
181+
165182
cover_basic_blocks_javat::cover_basic_blocks_javat(
166183
const goto_programt &_goto_program)
167184
{

‎src/goto-instrument/cover_basic_blocks.h

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,8 @@ Author: Daniel Kroening
1818

1919
#include <goto-programs/goto_model.h>
2020

21+
#include "source_lines.h"
22+
2123
class cover_blocks_baset
2224
{
2325
public:
@@ -107,6 +109,9 @@ class cover_basic_blockst final : public cover_blocks_baset
107109

108110
/// the set of lines belonging to this block
109111
std::unordered_set<std::size_t> lines;
112+
113+
/// the set of source code lines belonging to this block
114+
source_linest source_lines;
110115
};
111116

112117
/// map program locations to block numbers
@@ -118,6 +123,10 @@ class cover_basic_blockst final : public cover_blocks_baset
118123
/// location of basic block, compress to ranges if applicable
119124
static void update_covered_lines(block_infot &block_info);
120125

126+
/// create a string representing source lines and set as a property of source
127+
/// location of basic block
128+
static void update_source_lines(block_infot &block_info);
129+
121130
/// If this block is a continuation of a previous block through unconditional
122131
/// forward gotos, return this blocks number.
123132
static optionalt<std::size_t> continuation_of_block(

‎src/goto-instrument/cover_instrument_location.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,10 @@ void cover_location_instrumentert::instrument(
3535
// filter goals
3636
if(goal_filters(source_location))
3737
{
38-
const std::string comment = "block " + b;
38+
const std::string source_lines =
39+
id2string(source_location.get_basic_block_source_lines());
40+
const std::string comment =
41+
"block " + b + " (lines " + source_lines + ")";
3942
goto_program.insert_before_swap(i_it);
4043
i_it->make_assertion(false_exprt());
4144
i_it->source_location = source_location;

‎src/goto-instrument/source_lines.cpp

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
/*******************************************************************\
2+
3+
Module: Source Lines
4+
5+
Author: Mark R. Tuttle
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Set of source code lines contributing to a basic block
11+
12+
#include "source_lines.h"
13+
14+
#include <util/range.h>
15+
#include <util/source_location.h>
16+
#include <util/string2int.h>
17+
#include <util/string_utils.h>
18+
19+
#include <sstream>
20+
21+
void source_linest::insert(source_locationt const &loc)
22+
{
23+
if(loc.get_file().empty() || loc.is_built_in())
24+
return;
25+
std::string file = id2string(loc.get_file());
26+
27+
// the function of a source location can fail to be set
28+
std::string func = id2string(loc.get_function());
29+
30+
if(loc.get_line().empty())
31+
return;
32+
unsigned int line = safe_string2unsigned(id2string(loc.get_line()));
33+
34+
block_lines[file + ":" + func].insert(line);
35+
}
36+
37+
std::string source_linest::to_string() const
38+
{
39+
std::stringstream ss;
40+
const auto map =
41+
make_range(block_lines).map([&](const block_linest::value_type &pair) {
42+
std::stringstream str;
43+
str << pair.first << ':';
44+
join_strings(str, pair.second.cbegin(), pair.second.cend(), ',');
45+
return str.str();
46+
});
47+
join_strings(ss, map.begin(), map.end(), "; ");
48+
return ss.str();
49+
}

0 commit comments

Comments
 (0)