CBMC
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
14#include <util/message.h>
15
17 const goto_programt::const_targett &instruction,
19{
20 if(instruction->incoming_edges.size() != 1)
21 return {};
22
23 const goto_programt::targett in_t = *instruction->incoming_edges.cbegin();
24 if(in_t->is_goto() && !in_t->is_backwards_goto() && in_t->condition() == true)
25 return block_map[in_t];
26
27 return {};
28}
29
30static bool
32{
33 return a.get_file() == b.get_file() && a.get_line() == b.get_line();
34}
35
37{
38 bool next_is_target = true;
40 std::size_t current_block = 0;
41
42 forall_goto_program_instructions(it, goto_program)
43 {
44 // For the purposes of coverage blocks, multiple consecutive assume
45 // instructions with the same source location are considered to be part of
46 // the same block. Assumptions should terminate a block, as subsequent
47 // instructions may be unreachable. However check instrumentation passes
48 // may insert multiple assertions in the same program location. Therefore
49 // these are combined for reasons of readability of the coverage output.
52 !(it->is_assume() &&
54 preceding_assume->source_location(), it->source_location()));
55
56 // Is it a potential beginning of a block?
57 if(next_is_target || it->is_target() || end_of_assume_group)
58 {
60 {
62 }
63 else
64 {
65 block_infos.emplace_back();
66 block_infos.back().representative_inst = it;
67 block_infos.back().source_location = source_locationt::nil();
68 current_block = block_infos.size() - 1;
69 }
70 }
71
73 current_block < block_infos.size(), "current block number out of range");
75
77
79
80 // set representative program location to instrument
81 if(
82 !it->source_location().is_nil() &&
83 !it->source_location().get_file().empty() &&
84 !it->source_location().get_line().empty() &&
85 !it->source_location().is_built_in() &&
86 block_info.source_location.is_nil())
87 {
88 block_info.representative_inst = it; // update
89 block_info.source_location = it->source_location();
90 }
91
92 next_is_target = it->is_goto() || it->is_function_call();
93 preceding_assume = it->is_assume() ? &*it : nullptr;
94 }
95}
96
98{
99 const auto it = block_map.find(t);
100 INVARIANT(it != block_map.end(), "instruction must be part of a block");
101 return it->second;
102}
103
104std::optional<goto_programt::const_targett>
106{
107 INVARIANT(block_nr < block_infos.size(), "block number out of range");
108 return block_infos[block_nr].representative_inst;
109}
110
111const source_locationt &
113{
114 INVARIANT(block_nr < block_infos.size(), "block number out of range");
115 return block_infos[block_nr].source_location;
116}
117
118const source_linest &
120{
121 INVARIANT(block_nr < block_infos.size(), "block number out of range");
122 return block_infos[block_nr].source_lines;
123}
124
126 const irep_idt &function_id,
127 const goto_programt &goto_program,
128 message_handlert &message_handler)
129{
130 messaget msg(message_handler);
131 std::set<std::size_t> blocks_seen;
132 forall_goto_program_instructions(it, goto_program)
133 {
134 const std::size_t block_nr = block_of(it);
136
137 if(
138 blocks_seen.insert(block_nr).second &&
139 block_info.representative_inst == goto_program.instructions.end())
140 {
141 msg.warning() << "Ignoring block " << (block_nr + 1) << " location "
142 << it->location_number << " " << it->source_location()
143 << " (bytecode-index already instrumented)"
144 << messaget::eom;
145 }
146 else if(
147 block_info.representative_inst == it &&
148 block_info.source_location.is_nil())
149 {
150 msg.warning() << "Ignoring block " << (block_nr + 1) << " location "
151 << it->location_number << " " << function_id
152 << " (missing source location)" << messaget::eom;
153 }
154 // The location numbers printed here are those
155 // before the coverage instrumentation.
156 }
157}
158
159void cover_basic_blockst::output(std::ostream &out) const
160{
161 for(const auto &block_pair : block_map)
162 out << block_pair.first->source_location() << " -> " << block_pair.second
163 << '\n';
164}
165
168 const goto_programt::instructiont &instruction)
169{
170 const auto &add_location = [&](const source_locationt &location) {
171 const irep_idt &line = location.get_line();
172 if(!line.empty())
173 {
174 block.source_lines.insert(location);
175 }
176 };
177 add_location(instruction.source_location());
178 instruction.code().visit_pre([&](const exprt &expr) {
179 const auto &location = expr.source_location();
180 if(!location.get_function().empty())
181 add_location(location);
182 });
183}
184
187{
189 {
190 const auto &location = it->source_location();
191 const auto &bytecode_index = location.get_java_bytecode_index();
192 auto entry = index_to_block.emplace(bytecode_index, block_infos.size());
193 if(entry.second)
194 {
195 block_infos.push_back(it);
196 block_locations.push_back(location);
197 block_source_lines.emplace_back(location);
198 }
199 else
200 {
201 block_source_lines[entry.first->second].insert(location);
202 }
203 }
204}
205
206std::size_t
208{
209 const auto &bytecode_index = t->source_location().get_java_bytecode_index();
210 const auto it = index_to_block.find(bytecode_index);
211 INVARIANT(it != index_to_block.end(), "instruction must be part of a block");
212 return it->second;
213}
214
215std::optional<goto_programt::const_targett>
217{
219 return block_infos[block_nr];
220}
221
222const source_locationt &
228
229const source_linest &
235
236void cover_basic_blocks_javat::output(std::ostream &out) const
237{
238 for(std::size_t i = 0; i < block_locations.size(); ++i)
239 out << block_locations[i] << " -> " << i << '\n';
240}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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
const source_linest & source_lines_of(std::size_t block_number) const override
std::vector< source_linest > block_source_lines
std::optional< goto_programt::const_targett > instruction_of(std::size_t block_number) const override
std::unordered_map< irep_idt, std::size_t > index_to_block
void output(std::ostream &out) const override
Outputs the list of blocks.
std::optional< goto_programt::const_targett > instruction_of(std::size_t block_nr) const override
static std::optional< 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,...
cover_basic_blockst(const goto_programt &goto_program)
std::map< goto_programt::const_targett, std::size_t, goto_programt::target_less_than > block_mapt
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.
const source_linest & source_lines_of(std::size_t block_nr) const override
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.
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:38
bool empty() const
Definition dstring.h:89
Base class for all expressions.
Definition expr.h:57
const source_locationt & source_location() const
Definition expr.h:236
This class represents an instruction in the GOTO intermediate representation.
const goto_instruction_codet & code() const
Get the code represented by this instruction.
const source_locationt & source_location() const
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::iterator targett
instructionst::const_iterator const_targett
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static eomt eom
Definition message.h:289
void insert(const source_locationt &loc)
Insert a line (a source location) into the set of lines.
static const source_locationt & nil()
static bool same_source_line(const source_locationt &a, const source_locationt &b)
Basic blocks detection for Coverage Instrumentation.
#define forall_goto_program_instructions(it, program)
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
source_linest source_lines
the set of source code lines belonging to this block