Skip to content

Commit 2bb98d9

Browse files
Merge pull request diffblue#1819 from romainbrenguier/refactor/coverage-instrumentation
Refactoring in coverage instrumentation
2 parents 678218a + 6492b3a commit 2bb98d9

File tree

5 files changed

+54
-52
lines changed

5 files changed

+54
-52
lines changed

src/goto-instrument/cover_basic_blocks.cpp

+26-25
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,20 @@ Author: Peter Schrammel
1515
#include <util/message.h>
1616
#include <util/string2int.h>
1717

18+
optionalt<unsigned> cover_basic_blockst::continuation_of_block(
19+
const goto_programt::const_targett &instruction,
20+
cover_basic_blockst::block_mapt &block_map)
21+
{
22+
if(instruction->incoming_edges.size() != 1)
23+
return {};
24+
25+
const goto_programt::targett in_t = *instruction->incoming_edges.cbegin();
26+
if(in_t->is_goto() && !in_t->is_backwards_goto() && in_t->guard.is_true())
27+
return block_map[in_t];
28+
29+
return {};
30+
}
31+
1832
cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
1933
{
2034
bool next_is_target = true;
@@ -25,25 +39,13 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
2539
// Is it a potential beginning of a block?
2640
if(next_is_target || it->is_target())
2741
{
28-
// We keep the block number if this potential block
29-
// is a continuation of a previous block through
30-
// unconditional forward gotos; otherwise we increase the
31-
// block number.
32-
bool increase_block_nr = true;
33-
if(it->incoming_edges.size() == 1)
42+
if(auto block_number = continuation_of_block(it, block_map))
3443
{
35-
goto_programt::targett in_t = *it->incoming_edges.begin();
36-
if(
37-
in_t->is_goto() && !in_t->is_backwards_goto() &&
38-
in_t->guard.is_true())
39-
{
40-
current_block = block_map[in_t];
41-
increase_block_nr = false;
42-
}
44+
current_block = *block_number;
4345
}
44-
if(increase_block_nr)
46+
else
4547
{
46-
block_infos.push_back(block_infot());
48+
block_infos.emplace_back();
4749
block_infos.back().representative_inst = it;
4850
block_infos.back().source_location = source_locationt::nil();
4951
current_block = block_infos.size() - 1;
@@ -87,12 +89,12 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
8789

8890
unsigned cover_basic_blockst::block_of(goto_programt::const_targett t) const
8991
{
90-
block_mapt::const_iterator it = block_map.find(t);
92+
const auto it = block_map.find(t);
9193
INVARIANT(it != block_map.end(), "instruction must be part of a block");
9294
return it->second;
9395
}
9496

95-
goto_programt::const_targett
97+
optionalt<goto_programt::const_targett>
9698
cover_basic_blockst::instruction_of(unsigned block_nr) const
9799
{
98100
INVARIANT(block_nr < block_infos.size(), "block number out of range");
@@ -116,13 +118,13 @@ void cover_basic_blockst::select_unique_java_bytecode_indices(
116118

117119
forall_goto_program_instructions(it, goto_program)
118120
{
119-
unsigned block_nr = block_of(it);
121+
const unsigned block_nr = block_of(it);
120122
if(blocks_seen.find(block_nr) != blocks_seen.end())
121123
continue;
122124

123125
INVARIANT(block_nr < block_infos.size(), "block number out of range");
124126
block_infot &block_info = block_infos.at(block_nr);
125-
if(block_info.representative_inst == goto_program.instructions.end())
127+
if(!block_info.representative_inst)
126128
{
127129
if(!it->source_location.get_java_bytecode_index().empty())
128130
{
@@ -144,7 +146,7 @@ void cover_basic_blockst::select_unique_java_bytecode_indices(
144146
}
145147
}
146148
}
147-
else if(it == block_info.representative_inst)
149+
else if(it == *block_info.representative_inst)
148150
{
149151
// check the existing representative
150152
if(!it->source_location.get_java_bytecode_index().empty())
@@ -159,7 +161,7 @@ void cover_basic_blockst::select_unique_java_bytecode_indices(
159161
else
160162
{
161163
// clash, reset to search for a new one
162-
block_info.representative_inst = goto_program.instructions.end();
164+
block_info.representative_inst = {};
163165
block_info.source_location = source_locationt::nil();
164166
msg.debug() << it->function << " block " << (block_nr + 1)
165167
<< ", location " << it->location_number
@@ -182,7 +184,7 @@ void cover_basic_blockst::report_block_anomalies(
182184
std::set<unsigned> blocks_seen;
183185
forall_goto_program_instructions(it, goto_program)
184186
{
185-
unsigned block_nr = block_of(it);
187+
const unsigned block_nr = block_of(it);
186188
const block_infot &block_info = block_infos.at(block_nr);
187189

188190
if(
@@ -223,7 +225,6 @@ void cover_basic_blockst::update_covered_lines(block_infot &block_info)
223225
INVARIANT(!cover_set.empty(), "covered lines set must not be empty");
224226
std::vector<unsigned> line_list(cover_set.begin(), cover_set.end());
225227

226-
format_number_ranget format_lines;
227-
std::string covered_lines = format_lines(line_list);
228+
std::string covered_lines = format_number_range(line_list);
228229
block_info.source_location.set_basic_block_covered_lines(covered_lines);
229230
}

src/goto-instrument/cover_basic_blocks.h

+18-12
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ Author: Daniel Kroening
1818

1919
class message_handlert;
2020

21-
class cover_basic_blockst
21+
class cover_basic_blockst final
2222
{
2323
public:
2424
explicit cover_basic_blockst(const goto_programt &_goto_program);
@@ -31,7 +31,8 @@ class cover_basic_blockst
3131
/// \param block_nr a block number
3232
/// \return the instruction selected for
3333
/// instrumentation representative of the given block
34-
goto_programt::const_targett instruction_of(unsigned block_nr) const;
34+
optionalt<goto_programt::const_targett>
35+
instruction_of(unsigned block_nr) const;
3536

3637
/// \param block_nr a block number
3738
/// \return the source location selected for
@@ -56,32 +57,37 @@ class cover_basic_blockst
5657
/// Outputs the list of blocks
5758
void output(std::ostream &out) const;
5859

59-
protected:
60-
// map program locations to block numbers
60+
private:
6161
typedef std::map<goto_programt::const_targett, unsigned> block_mapt;
62-
block_mapt block_map;
6362

6463
struct block_infot
6564
{
6665
/// the program location to instrument for this block
67-
goto_programt::const_targett representative_inst;
66+
optionalt<goto_programt::const_targett> representative_inst;
6867

6968
/// the source location representative for this block
70-
// (we need a separate copy of source locations because we attach
71-
// the line number ranges to them)
69+
/// (we need a separate copy of source locations because we attach
70+
/// the line number ranges to them)
7271
source_locationt source_location;
7372

74-
// map block numbers to source code locations
7573
/// the set of lines belonging to this block
7674
std::unordered_set<unsigned> lines;
7775
};
7876

79-
typedef std::vector<block_infot> block_infost;
80-
block_infost block_infos;
77+
/// map program locations to block numbers
78+
block_mapt block_map;
79+
/// map block numbers to block information
80+
std::vector<block_infot> block_infos;
8181

8282
/// create list of covered lines as CSV string and set as property of source
8383
/// location of basic block, compress to ranges if applicable
84-
void update_covered_lines(block_infot &block_info);
84+
static void update_covered_lines(block_infot &block_info);
85+
86+
/// If this block is a continuation of a previous block through unconditional
87+
/// forward gotos, return this blocks number.
88+
static optionalt<unsigned> continuation_of_block(
89+
const goto_programt::const_targett &instruction,
90+
block_mapt &block_map);
8591
};
8692

8793
#endif // CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H

src/goto-instrument/cover_instrument_location.cpp

+7-8
Original file line numberDiff line numberDiff line change
@@ -22,20 +22,19 @@ void cover_location_instrumentert::instrument(
2222
if(is_non_cover_assertion(i_it))
2323
i_it->make_skip();
2424

25-
unsigned block_nr = basic_blocks.block_of(i_it);
26-
goto_programt::const_targett in_t = basic_blocks.instruction_of(block_nr);
25+
const unsigned block_nr = basic_blocks.block_of(i_it);
26+
const auto representative_instruction = basic_blocks.instruction_of(block_nr);
2727
// we only instrument the selected instruction
28-
if(in_t == i_it)
28+
if(representative_instruction && *representative_instruction == i_it)
2929
{
30-
std::string b = std::to_string(block_nr + 1); // start with 1
31-
std::string id = id2string(i_it->function) + "#" + b;
32-
source_locationt source_location =
33-
basic_blocks.source_location_of(block_nr);
30+
const std::string b = std::to_string(block_nr + 1); // start with 1
31+
const std::string id = id2string(i_it->function) + "#" + b;
32+
const auto source_location = basic_blocks.source_location_of(block_nr);
3433

3534
// filter goals
3635
if(goal_filters(source_location))
3736
{
38-
std::string comment = "block " + b;
37+
const std::string comment = "block " + b;
3938
const irep_idt function = i_it->function;
4039
goto_program.insert_before_swap(i_it);
4140
i_it->make_assertion(false_exprt());

src/util/format_number_range.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,9 @@ Author: Daniel Kroening, [email protected]
1616
#include "format_number_range.h"
1717

1818
/// create shorter representation for output
19-
/// \par parameters: vector of numbers
19+
/// \param parameters: vector of numbers
2020
/// \return string of compressed number range representation
21-
std::string format_number_ranget::operator()(std::vector<unsigned> &numbers)
21+
std::string format_number_range(std::vector<unsigned> &numbers)
2222
{
2323
std::string number_range;
2424
std::sort(numbers.begin(), numbers.end());

src/util/format_number_range.h

+1-5
Original file line numberDiff line numberDiff line change
@@ -15,10 +15,6 @@ Author: Daniel Kroening, [email protected]
1515
#include <string>
1616
#include <vector>
1717

18-
class format_number_ranget
19-
{
20-
public:
21-
std::string operator()(std::vector<unsigned> &);
22-
};
18+
std::string format_number_range(std::vector<unsigned> &);
2319

2420
#endif // CPROVER_UTIL_FORMAT_NUMBER_RANGE_H

0 commit comments

Comments
 (0)