cprover
Loading...
Searching...
No Matches
cover_basic_blocks.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Coverage Instrumentation
4
5Author: Peter Schrammel
6
7\*******************************************************************/
8
11
12#include "cover_basic_blocks.h"
13
15#include <util/message.h>
16#include <util/string2int.h>
17
19 const goto_programt::const_targett &instruction,
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
33{
34 bool next_is_target = true;
35 std::size_t current_block = 0;
36
37 forall_goto_program_instructions(it, goto_program)
38 {
39 // Is it a potential beginning of a block?
40 if(next_is_target || it->is_target())
41 {
42 if(auto block_number = continuation_of_block(it, block_map))
43 {
44 current_block = *block_number;
45 }
46 else
47 {
48 block_infos.emplace_back();
49 block_infos.back().representative_inst = it;
50 block_infos.back().source_location = source_locationt::nil();
51 current_block = block_infos.size() - 1;
52 }
53 }
54
56 current_block < block_infos.size(), "current block number out of range");
57 block_infot &block_info = block_infos.at(current_block);
58
59 block_map[it] = current_block;
60
61 add_block_lines(block_info, *it);
62
63 // set representative program location to instrument
64 if(
65 !it->source_location().is_nil() &&
66 !it->source_location().get_file().empty() &&
67 !it->source_location().get_line().empty() &&
68 block_info.source_location.is_nil())
69 {
70 block_info.representative_inst = it; // update
71 block_info.source_location = it->source_location();
72 }
73
74 next_is_target =
75#if 0
76 // Disabled for being too messy
77 it->is_goto() || it->is_function_call() || it->is_assume();
78#else
79 it->is_goto() || it->is_function_call();
80#endif
81 }
82
83 for(auto &block_info : block_infos)
84 {
85 update_covered_lines(block_info);
86 update_source_lines(block_info);
87 }
88}
89
91{
92 const auto it = block_map.find(t);
93 INVARIANT(it != block_map.end(), "instruction must be part of a block");
94 return it->second;
95}
96
98cover_basic_blockst::instruction_of(const std::size_t block_nr) const
99{
100 INVARIANT(block_nr < block_infos.size(), "block number out of range");
101 return block_infos[block_nr].representative_inst;
102}
103
104const source_locationt &
105cover_basic_blockst::source_location_of(const std::size_t block_nr) const
106{
107 INVARIANT(block_nr < block_infos.size(), "block number out of range");
108 return block_infos[block_nr].source_location;
109}
110
112 const irep_idt &function_id,
113 const goto_programt &goto_program,
114 message_handlert &message_handler)
115{
116 messaget msg(message_handler);
117 std::set<std::size_t> blocks_seen;
118 forall_goto_program_instructions(it, goto_program)
119 {
120 const std::size_t block_nr = block_of(it);
121 const block_infot &block_info = block_infos.at(block_nr);
122
123 if(
124 blocks_seen.insert(block_nr).second &&
125 block_info.representative_inst == goto_program.instructions.end())
126 {
127 msg.warning() << "Ignoring block " << (block_nr + 1) << " location "
128 << it->location_number << " " << it->source_location()
129 << " (bytecode-index already instrumented)"
130 << messaget::eom;
131 }
132 else if(
133 block_info.representative_inst == it &&
134 block_info.source_location.is_nil())
135 {
136 msg.warning() << "Ignoring block " << (block_nr + 1) << " location "
137 << it->location_number << " " << function_id
138 << " (missing source location)" << messaget::eom;
139 }
140 // The location numbers printed here are those
141 // before the coverage instrumentation.
142 }
143}
144
145void cover_basic_blockst::output(std::ostream &out) const
146{
147 for(const auto &block_pair : block_map)
148 out << block_pair.first->source_location() << " -> " << block_pair.second
149 << '\n';
150}
151
154 const goto_programt::instructiont &instruction)
155{
156 const auto &add_location = [&](const source_locationt &location) {
157 const irep_idt &line = location.get_line();
158 if(!line.empty())
159 {
160 block.lines.insert(unsafe_string2unsigned(id2string(line)));
161 block.source_lines.insert(location);
162 }
163 };
164 add_location(instruction.source_location());
165 instruction.get_code().visit_pre(
166 [&](const exprt &expr) { add_location(expr.source_location()); });
167}
168
170{
171 if(block_info.source_location.is_nil())
172 return;
173
174 const auto &cover_set = block_info.lines;
175 INVARIANT(!cover_set.empty(), "covered lines set must not be empty");
176 std::vector<unsigned> line_list(cover_set.begin(), cover_set.end());
177
178 std::string covered_lines = format_number_range(line_list);
179 block_info.source_location.set_basic_block_covered_lines(covered_lines);
180}
181
183{
184 if(block_info.source_location.is_nil())
185 return;
186
187 const auto &source_lines = block_info.source_lines;
188 std::string str = source_lines.to_string();
189 INVARIANT(!str.empty(), "source lines set must not be empty");
191}
192
194 const goto_programt &_goto_program)
195{
196 std::set<std::size_t> source_lines_requiring_update;
197
198 forall_goto_program_instructions(it, _goto_program)
199 {
200 const auto &location = it->source_location();
201 const auto &bytecode_index = location.get_java_bytecode_index();
202 auto entry = index_to_block.emplace(bytecode_index, block_infos.size());
203 if(entry.second)
204 {
205 block_infos.push_back(it);
206 block_locations.push_back(location);
207 block_locations.back().set_basic_block_covered_lines(location.get_line());
208 block_source_lines.emplace_back(location);
209 source_lines_requiring_update.insert(entry.first->second);
210 }
211 else
212 {
213 block_source_lines[entry.first->second].insert(location);
214 source_lines_requiring_update.insert(entry.first->second);
215 }
216 }
217
218 for(std::size_t i : source_lines_requiring_update)
219 {
220 block_locations.at(i).set_basic_block_source_lines(
221 block_source_lines.at(i).to_string());
222 }
223}
224
225std::size_t
227{
228 const auto &bytecode_index = t->source_location().get_java_bytecode_index();
229 const auto it = index_to_block.find(bytecode_index);
230 INVARIANT(it != index_to_block.end(), "instruction must be part of a block");
231 return it->second;
232}
233
235cover_basic_blocks_javat::instruction_of(const std::size_t block_nr) const
236{
237 PRECONDITION(block_nr < block_infos.size());
238 return block_infos[block_nr];
239}
240
241const source_locationt &
242cover_basic_blocks_javat::source_location_of(const std::size_t block_nr) const
243{
244 PRECONDITION(block_nr < block_locations.size());
245 return block_locations[block_nr];
246}
247
248void cover_basic_blocks_javat::output(std::ostream &out) const
249{
250 for(std::size_t i = 0; i < block_locations.size(); ++i)
251 out << block_locations[i] << " -> " << i << '\n';
252}
cover_basic_blocks_javat(const goto_programt &_goto_program)
std::vector< goto_programt::const_targett > block_infos
const source_locationt & source_location_of(std::size_t block_number) const override
std::vector< source_locationt > block_locations
void output(std::ostream &out) const override
Outputs the list of blocks.
std::size_t block_of(goto_programt::const_targett t) const override
std::vector< source_linest > block_source_lines
optionalt< goto_programt::const_targett > instruction_of(std::size_t block_number) const override
std::unordered_map< irep_idt, std::size_t > index_to_block
static void update_source_lines(block_infot &block_info)
create a string representing source lines and set as a property of source location of basic block
std::map< goto_programt::const_targett, std::size_t > block_mapt
void output(std::ostream &out) const override
Outputs the list of blocks.
cover_basic_blockst(const goto_programt &goto_program)
static optionalt< std::size_t > continuation_of_block(const goto_programt::const_targett &instruction, block_mapt &block_map)
If this block is a continuation of a previous block through unconditional forward gotos,...
optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const override
std::vector< block_infot > block_infos
map block numbers to block information
void report_block_anomalies(const irep_idt &function_id, const goto_programt &goto_program, message_handlert &message_handler) override
Output warnings about ignored blocks.
std::size_t block_of(goto_programt::const_targett t) const override
static void add_block_lines(cover_basic_blockst::block_infot &block, const goto_programt::instructiont &instruction)
Adds the lines which instruction spans to block.
static void update_covered_lines(block_infot &block_info)
create list of covered lines as CSV string and set as property of source location of basic block,...
const source_locationt & source_location_of(std::size_t block_nr) const override
block_mapt block_map
map program locations to block numbers
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:245
const source_locationt & source_location() const
Definition: expr.h:230
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:187
const source_locationt & source_location() const
Definition: goto_program.h:332
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
instructionst::iterator targett
Definition: goto_program.h:592
instructionst::const_iterator const_targett
Definition: goto_program.h:593
bool is_nil() const
Definition: irep.h:376
source_locationt source_location
Definition: message.h:247
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
void insert(const source_locationt &loc)
Insert a line (a source location) into the set of lines.
std::string to_string() const
Construct a string representing the set of lines.
void set_basic_block_covered_lines(const irep_idt &covered_lines)
static const source_locationt & nil()
void set_basic_block_source_lines(const irep_idt &source_lines)
Basic blocks detection for Coverage Instrumentation.
std::string format_number_range(const std::vector< unsigned > &input_numbers)
create shorter representation for output
Format vector of numbers into a compressed range.
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
nonstd::optional< T > optionalt
Definition: optional.h:35
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:35
std::unordered_set< std::size_t > lines
the set of lines belonging to this block
source_locationt source_location
the source location representative for this block (we need a separate copy of source locations becaus...
source_linest source_lines
the set of source code lines belonging to this block
optionalt< goto_programt::const_targett > representative_inst
the program location to instrument for this block