cprover
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 
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 
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  // update lines belonging to block
62  const irep_idt &line = it->source_location.get_line();
63  if(!line.empty())
64  block_info.lines.insert(unsafe_string2unsigned(id2string(line)));
65 
66  // set representative program location to instrument
67  if(
68  !it->source_location.is_nil() &&
69  !it->source_location.get_file().empty() &&
70  !it->source_location.get_line().empty() &&
71  block_info.source_location.is_nil())
72  {
73  block_info.representative_inst = it; // update
74  block_info.source_location = it->source_location;
75  }
76 
77  next_is_target =
78 #if 0
79  // Disabled for being too messy
80  it->is_goto() || it->is_function_call() || it->is_assume();
81 #else
82  it->is_goto() || it->is_function_call();
83 #endif
84  }
85 
86  for(auto &block_info : block_infos)
87  update_covered_lines(block_info);
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 
98 cover_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 
104 const source_locationt &
105 cover_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 goto_programt &goto_program,
113  message_handlert &message_handler)
114 {
115  messaget msg(message_handler);
116  std::set<std::size_t> blocks_seen;
117  forall_goto_program_instructions(it, goto_program)
118  {
119  const std::size_t block_nr = block_of(it);
120  const block_infot &block_info = block_infos.at(block_nr);
121 
122  if(
123  blocks_seen.insert(block_nr).second &&
124  block_info.representative_inst == goto_program.instructions.end())
125  {
126  msg.warning() << "Ignoring block " << (block_nr + 1) << " location "
127  << it->location_number << " " << it->source_location
128  << " (bytecode-index already instrumented)"
129  << messaget::eom;
130  }
131  else if(
132  block_info.representative_inst == it &&
133  block_info.source_location.is_nil())
134  {
135  msg.warning() << "Ignoring block " << (block_nr + 1) << " location "
136  << it->location_number << " " << it->function
137  << " (missing source location)" << messaget::eom;
138  }
139  // The location numbers printed here are those
140  // before the coverage instrumentation.
141  }
142 }
143 
144 void cover_basic_blockst::output(std::ostream &out) const
145 {
146  for(const auto &block_pair : block_map)
147  out << block_pair.first->source_location << " -> " << block_pair.second
148  << '\n';
149 }
150 
152 {
153  if(block_info.source_location.is_nil())
154  return;
155 
156  const auto &cover_set = block_info.lines;
157  INVARIANT(!cover_set.empty(), "covered lines set must not be empty");
158  std::vector<unsigned> line_list(cover_set.begin(), cover_set.end());
159 
160  std::string covered_lines = format_number_range(line_list);
161  block_info.source_location.set_basic_block_covered_lines(covered_lines);
162 }
163 
165  const goto_programt &_goto_program)
166 {
167  forall_goto_program_instructions(it, _goto_program)
168  {
169  const auto &location = it->source_location;
170  const auto &bytecode_index = location.get_java_bytecode_index();
171  if(index_to_block.emplace(bytecode_index, block_infos.size()).second)
172  {
173  block_infos.push_back(it);
174  block_locations.push_back(location);
175  block_locations.back().set_basic_block_covered_lines(location.get_line());
176  }
177  }
178 }
179 
180 std::size_t
182 {
183  const auto &bytecode_index = t->source_location.get_java_bytecode_index();
184  const auto it = index_to_block.find(bytecode_index);
185  INVARIANT(it != index_to_block.end(), "instruction must be part of a block");
186  return it->second;
187 }
188 
190 cover_basic_blocks_javat::instruction_of(const std::size_t block_nr) const
191 {
192  PRECONDITION(block_nr < block_infos.size());
193  return block_infos[block_nr];
194 }
195 
196 const source_locationt &
197 cover_basic_blocks_javat::source_location_of(const std::size_t block_nr) const
198 {
199  PRECONDITION(block_nr < block_locations.size());
200  return block_locations[block_nr];
201 }
202 
203 void cover_basic_blocks_javat::output(std::ostream &out) const
204 {
205  for(std::size_t i = 0; i < block_locations.size(); ++i)
206  out << block_locations[i] << " -> " << i << '\n';
207 }
const source_locationt & source_location_of(std::size_t block_number) const override
std::unordered_set< std::size_t > lines
the set of lines belonging to this block
optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const override
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
cover_basic_blockst(const goto_programt &_goto_program)
static const source_locationt & nil()
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:69
optionalt< goto_programt::const_targett > representative_inst
the program location to instrument for this block
Basic blocks detection for Coverage Instrumentation.
const source_locationt & source_location_of(std::size_t block_nr) const override
mstreamt & warning() const
Definition: message.h:391
std::vector< goto_programt::const_targett > block_infos
instructionst::iterator targett
Definition: goto_program.h:414
source_locationt source_location
Definition: message.h:236
nonstd::optional< T > optionalt
Definition: optional.h:35
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
instructionst::const_iterator const_targett
Definition: goto_program.h:415
std::unordered_map< irep_idt, std::size_t > index_to_block
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
source_locationt source_location
the source location representative for this block (we need a separate copy of source locations becaus...
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...
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
optionalt< goto_programt::const_targett > instruction_of(std::size_t block_number) const override
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
std::vector< source_locationt > block_locations
static eomt eom
Definition: message.h:284
std::string format_number_range(const std::vector< unsigned > &input_numbers)
create shorter representation for output
void output(std::ostream &out) const override
Outputs the list of blocks.
void report_block_anomalies(const goto_programt &goto_program, message_handlert &message_handler) override
Output warnings about ignored blocks.
cover_basic_blocks_javat(const goto_programt &_goto_program)
void output(std::ostream &out) const override
Outputs the list of blocks.
Format vector of numbers into a compressed range.
block_mapt block_map
map program locations to block numbers
std::size_t block_of(goto_programt::const_targett t) const override
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...
std::map< goto_programt::const_targett, std::size_t > block_mapt
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
std::size_t block_of(goto_programt::const_targett t) const override
bool empty() const
Definition: dstring.h:75
std::vector< block_infot > block_infos
map block numbers to block information
void set_basic_block_covered_lines(const irep_idt &covered_lines)