CBMC
cover_basic_blocks.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Coverage Instrumentation
4 
5 Author: 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(
25  in_t->is_goto() && !in_t->is_backwards_goto() &&
26  in_t->condition().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 
55  INVARIANT(
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  !it->source_location().is_built_in() &&
69  block_info.source_location.is_nil())
70  {
71  block_info.representative_inst = it; // update
72  block_info.source_location = it->source_location();
73  }
74 
75  next_is_target =
76 #if 0
77  // Disabled for being too messy
78  it->is_goto() || it->is_function_call() || it->is_assume();
79 #else
80  it->is_goto() || it->is_function_call();
81 #endif
82  }
83 }
84 
86 {
87  const auto it = block_map.find(t);
88  INVARIANT(it != block_map.end(), "instruction must be part of a block");
89  return it->second;
90 }
91 
93 cover_basic_blockst::instruction_of(const std::size_t block_nr) const
94 {
95  INVARIANT(block_nr < block_infos.size(), "block number out of range");
96  return block_infos[block_nr].representative_inst;
97 }
98 
99 const source_locationt &
100 cover_basic_blockst::source_location_of(const std::size_t block_nr) const
101 {
102  INVARIANT(block_nr < block_infos.size(), "block number out of range");
103  return block_infos[block_nr].source_location;
104 }
105 
106 const source_linest &
107 cover_basic_blockst::source_lines_of(const std::size_t block_nr) const
108 {
109  INVARIANT(block_nr < block_infos.size(), "block number out of range");
110  return block_infos[block_nr].source_lines;
111 }
112 
114  const irep_idt &function_id,
115  const goto_programt &goto_program,
116  message_handlert &message_handler)
117 {
118  messaget msg(message_handler);
119  std::set<std::size_t> blocks_seen;
120  forall_goto_program_instructions(it, goto_program)
121  {
122  const std::size_t block_nr = block_of(it);
123  const block_infot &block_info = block_infos.at(block_nr);
124 
125  if(
126  blocks_seen.insert(block_nr).second &&
127  block_info.representative_inst == goto_program.instructions.end())
128  {
129  msg.warning() << "Ignoring block " << (block_nr + 1) << " location "
130  << it->location_number << " " << it->source_location()
131  << " (bytecode-index already instrumented)"
132  << messaget::eom;
133  }
134  else if(
135  block_info.representative_inst == it &&
136  block_info.source_location.is_nil())
137  {
138  msg.warning() << "Ignoring block " << (block_nr + 1) << " location "
139  << it->location_number << " " << function_id
140  << " (missing source location)" << messaget::eom;
141  }
142  // The location numbers printed here are those
143  // before the coverage instrumentation.
144  }
145 }
146 
147 void cover_basic_blockst::output(std::ostream &out) const
148 {
149  for(const auto &block_pair : block_map)
150  out << block_pair.first->source_location() << " -> " << block_pair.second
151  << '\n';
152 }
153 
156  const goto_programt::instructiont &instruction)
157 {
158  const auto &add_location = [&](const source_locationt &location) {
159  const irep_idt &line = location.get_line();
160  if(!line.empty())
161  {
162  block.source_lines.insert(location);
163  }
164  };
165  add_location(instruction.source_location());
166  instruction.get_code().visit_pre([&](const exprt &expr) {
167  const auto &location = expr.source_location();
168  if(!location.get_function().empty())
169  add_location(location);
170  });
171 }
172 
174  const goto_programt &_goto_program)
175 {
176  forall_goto_program_instructions(it, _goto_program)
177  {
178  const auto &location = it->source_location();
179  const auto &bytecode_index = location.get_java_bytecode_index();
180  auto entry = index_to_block.emplace(bytecode_index, block_infos.size());
181  if(entry.second)
182  {
183  block_infos.push_back(it);
184  block_locations.push_back(location);
185  block_source_lines.emplace_back(location);
186  }
187  else
188  {
189  block_source_lines[entry.first->second].insert(location);
190  }
191  }
192 }
193 
194 std::size_t
196 {
197  const auto &bytecode_index = t->source_location().get_java_bytecode_index();
198  const auto it = index_to_block.find(bytecode_index);
199  INVARIANT(it != index_to_block.end(), "instruction must be part of a block");
200  return it->second;
201 }
202 
204 cover_basic_blocks_javat::instruction_of(const std::size_t block_nr) const
205 {
206  PRECONDITION(block_nr < block_infos.size());
207  return block_infos[block_nr];
208 }
209 
210 const source_locationt &
211 cover_basic_blocks_javat::source_location_of(const std::size_t block_nr) const
212 {
213  PRECONDITION(block_nr < block_locations.size());
214  return block_locations[block_nr];
215 }
216 
217 const source_linest &
218 cover_basic_blocks_javat::source_lines_of(const std::size_t block_nr) const
219 {
220  PRECONDITION(block_nr < block_locations.size());
221  return block_source_lines[block_nr];
222 }
223 
224 void cover_basic_blocks_javat::output(std::ostream &out) const
225 {
226  for(std::size_t i = 0; i < block_locations.size(); ++i)
227  out << block_locations[i] << " -> " << i << '\n';
228 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
cover_basic_blockst::instruction_of
optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const override
Definition: cover_basic_blocks.cpp:93
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
cover_basic_blocks_javat::index_to_block
std::unordered_map< irep_idt, std::size_t > index_to_block
Definition: cover_basic_blocks.h:149
cover_basic_blockst::add_block_lines
static void add_block_lines(cover_basic_blockst::block_infot &block, const goto_programt::instructiont &instruction)
Adds the lines which instruction spans to block.
Definition: cover_basic_blocks.cpp:154
cover_basic_blocks_javat::cover_basic_blocks_javat
cover_basic_blocks_javat(const goto_programt &_goto_program)
Definition: cover_basic_blocks.cpp:173
source_locationt::nil
static const source_locationt & nil()
Definition: source_location.h:177
cover_basic_blockst::block_infot::source_location
source_locationt source_location
the source location representative for this block (we need a separate copy of source locations becaus...
Definition: cover_basic_blocks.h:118
cover_basic_blocks_javat::block_source_lines
std::vector< source_linest > block_source_lines
Definition: cover_basic_blocks.h:151
exprt
Base class for all expressions.
Definition: expr.h:55
cover_basic_blockst::report_block_anomalies
void report_block_anomalies(const irep_idt &function_id, const goto_programt &goto_program, message_handlert &message_handler) override
Output warnings about ignored blocks.
Definition: cover_basic_blocks.cpp:113
messaget::eom
static eomt eom
Definition: message.h:297
cover_basic_blockst::block_infot::source_lines
source_linest source_lines
the set of source code lines belonging to this block
Definition: cover_basic_blocks.h:121
cover_basic_blockst::block_of
std::size_t block_of(goto_programt::const_targett t) const override
Definition: cover_basic_blocks.cpp:85
source_linest::insert
void insert(const source_locationt &loc)
Insert a line (a source location) into the set of lines.
Definition: source_lines.cpp:21
source_linest
Definition: source_lines.h:32
cover_basic_blockst::block_map
block_mapt block_map
map program locations to block numbers
Definition: cover_basic_blocks.h:125
goto_programt::instructiont::get_code
const goto_instruction_codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:189
cover_basic_blockst::source_lines_of
const source_linest & source_lines_of(std::size_t block_nr) const override
Definition: cover_basic_blocks.cpp:107
goto_programt::instructiont::source_location
const source_locationt & source_location() const
Definition: goto_program.h:340
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
cover_basic_blockst::continuation_of_block
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,...
Definition: cover_basic_blocks.cpp:16
cover_basic_blockst::block_infos
std::vector< block_infot > block_infos
map block numbers to block information
Definition: cover_basic_blocks.h:127
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
cover_basic_blockst::source_location_of
const source_locationt & source_location_of(std::size_t block_nr) const override
Definition: cover_basic_blocks.cpp:100
cover_basic_blocks_javat::block_of
std::size_t block_of(goto_programt::const_targett t) const override
Definition: cover_basic_blocks.cpp:195
cover_basic_blocks_javat::block_locations
std::vector< source_locationt > block_locations
Definition: cover_basic_blocks.h:147
irept::is_nil
bool is_nil() const
Definition: irep.h:376
message_handlert
Definition: message.h:27
dstringt::empty
bool empty() const
Definition: dstring.h:88
cover_basic_blocks_javat::source_lines_of
const source_linest & source_lines_of(std::size_t block_number) const override
Definition: cover_basic_blocks.cpp:218
cover_basic_blocks_javat::block_infos
std::vector< goto_programt::const_targett > block_infos
Definition: cover_basic_blocks.h:145
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
source_locationt
Definition: source_location.h:18
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:592
cover_basic_blocks_javat::source_location_of
const source_locationt & source_location_of(std::size_t block_number) const override
Definition: cover_basic_blocks.cpp:211
cover_basic_blocks_javat::instruction_of
optionalt< goto_programt::const_targett > instruction_of(std::size_t block_number) const override
Definition: cover_basic_blocks.cpp:204
cover_basic_blockst::block_mapt
std::map< goto_programt::const_targett, std::size_t > block_mapt
Definition: cover_basic_blocks.h:108
cover_basic_blocks_javat::output
void output(std::ostream &out) const override
Outputs the list of blocks.
Definition: cover_basic_blocks.cpp:224
cover_basic_blockst::output
void output(std::ostream &out) const override
Outputs the list of blocks.
Definition: cover_basic_blocks.cpp:147
exprt::visit_pre
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:245
cover_basic_blocks.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:587
message.h
messaget::warning
mstreamt & warning() const
Definition: message.h:404
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:211
cover_basic_blockst::block_infot::representative_inst
optionalt< goto_programt::const_targett > representative_inst
the program location to instrument for this block
Definition: cover_basic_blocks.h:113
cover_basic_blockst::block_infot
Definition: cover_basic_blocks.h:110
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:586
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1229
cover_basic_blockst::cover_basic_blockst
cover_basic_blockst(const goto_programt &goto_program)
Definition: cover_basic_blocks.cpp:32
validation_modet::INVARIANT
@ INVARIANT