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  {
65  block_info.lines.insert(unsafe_string2unsigned(id2string(line)));
66  block_info.source_lines.insert(it->source_location);
67  }
68 
69  // set representative program location to instrument
70  if(
71  !it->source_location.is_nil() &&
72  !it->source_location.get_file().empty() &&
73  !it->source_location.get_line().empty() &&
74  block_info.source_location.is_nil())
75  {
76  block_info.representative_inst = it; // update
77  block_info.source_location = it->source_location;
78  }
79 
80  next_is_target =
81 #if 0
82  // Disabled for being too messy
83  it->is_goto() || it->is_function_call() || it->is_assume();
84 #else
85  it->is_goto() || it->is_function_call();
86 #endif
87  }
88 
89  for(auto &block_info : block_infos)
90  {
91  update_covered_lines(block_info);
92  update_source_lines(block_info);
93  }
94 }
95 
97 {
98  const auto it = block_map.find(t);
99  INVARIANT(it != block_map.end(), "instruction must be part of a block");
100  return it->second;
101 }
102 
104 cover_basic_blockst::instruction_of(const std::size_t block_nr) const
105 {
106  INVARIANT(block_nr < block_infos.size(), "block number out of range");
107  return block_infos[block_nr].representative_inst;
108 }
109 
110 const source_locationt &
111 cover_basic_blockst::source_location_of(const std::size_t block_nr) const
112 {
113  INVARIANT(block_nr < block_infos.size(), "block number out of range");
114  return block_infos[block_nr].source_location;
115 }
116 
118  const irep_idt &function_id,
119  const goto_programt &goto_program,
120  message_handlert &message_handler)
121 {
122  messaget msg(message_handler);
123  std::set<std::size_t> blocks_seen;
124  forall_goto_program_instructions(it, goto_program)
125  {
126  const std::size_t block_nr = block_of(it);
127  const block_infot &block_info = block_infos.at(block_nr);
128 
129  if(
130  blocks_seen.insert(block_nr).second &&
131  block_info.representative_inst == goto_program.instructions.end())
132  {
133  msg.warning() << "Ignoring block " << (block_nr + 1) << " location "
134  << it->location_number << " " << it->source_location
135  << " (bytecode-index already instrumented)"
136  << messaget::eom;
137  }
138  else if(
139  block_info.representative_inst == it &&
140  block_info.source_location.is_nil())
141  {
142  msg.warning() << "Ignoring block " << (block_nr + 1) << " location "
143  << it->location_number << " " << function_id
144  << " (missing source location)" << messaget::eom;
145  }
146  // The location numbers printed here are those
147  // before the coverage instrumentation.
148  }
149 }
150 
151 void cover_basic_blockst::output(std::ostream &out) const
152 {
153  for(const auto &block_pair : block_map)
154  out << block_pair.first->source_location << " -> " << block_pair.second
155  << '\n';
156 }
157 
159 {
160  if(block_info.source_location.is_nil())
161  return;
162 
163  const auto &cover_set = block_info.lines;
164  INVARIANT(!cover_set.empty(), "covered lines set must not be empty");
165  std::vector<unsigned> line_list(cover_set.begin(), cover_set.end());
166 
167  std::string covered_lines = format_number_range(line_list);
168  block_info.source_location.set_basic_block_covered_lines(covered_lines);
169 }
170 
172 {
173  if(block_info.source_location.is_nil())
174  return;
175 
176  const auto &source_lines = block_info.source_lines;
177  std::string str = source_lines.to_string();
178  INVARIANT(!str.empty(), "source lines set must not be empty");
180 }
181 
183  const goto_programt &_goto_program)
184 {
185  std::set<std::size_t> source_lines_requiring_update;
186 
187  forall_goto_program_instructions(it, _goto_program)
188  {
189  const auto &location = it->source_location;
190  const auto &bytecode_index = location.get_java_bytecode_index();
191  auto entry = index_to_block.emplace(bytecode_index, block_infos.size());
192  if(entry.second)
193  {
194  block_infos.push_back(it);
195  block_locations.push_back(location);
196  block_locations.back().set_basic_block_covered_lines(location.get_line());
197  block_source_lines.emplace_back(location);
198  source_lines_requiring_update.insert(entry.first->second);
199  }
200  else
201  {
202  block_source_lines[entry.first->second].insert(location);
203  source_lines_requiring_update.insert(entry.first->second);
204  }
205  }
206 
207  for(std::size_t i : source_lines_requiring_update)
208  {
209  block_locations.at(i).set_basic_block_source_lines(
210  block_source_lines.at(i).to_string());
211  }
212 }
213 
214 std::size_t
216 {
217  const auto &bytecode_index = t->source_location.get_java_bytecode_index();
218  const auto it = index_to_block.find(bytecode_index);
219  INVARIANT(it != index_to_block.end(), "instruction must be part of a block");
220  return it->second;
221 }
222 
224 cover_basic_blocks_javat::instruction_of(const std::size_t block_nr) const
225 {
226  PRECONDITION(block_nr < block_infos.size());
227  return block_infos[block_nr];
228 }
229 
230 const source_locationt &
231 cover_basic_blocks_javat::source_location_of(const std::size_t block_nr) const
232 {
233  PRECONDITION(block_nr < block_locations.size());
234  return block_locations[block_nr];
235 }
236 
237 void cover_basic_blocks_javat::output(std::ostream &out) const
238 {
239  for(std::size_t i = 0; i < block_locations.size(); ++i)
240  out << block_locations[i] << " -> " << i << '\n';
241 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
cover_basic_blockst::instruction_of
optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const override
Definition: cover_basic_blocks.cpp:104
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
cover_basic_blocks_javat::index_to_block
std::unordered_map< irep_idt, std::size_t > index_to_block
Definition: cover_basic_blocks.h:145
cover_basic_blocks_javat::cover_basic_blocks_javat
cover_basic_blocks_javat(const goto_programt &_goto_program)
Definition: cover_basic_blocks.cpp:182
source_locationt::nil
static const source_locationt & nil()
Definition: source_location.h:188
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:108
cover_basic_blocks_javat::block_source_lines
std::vector< source_linest > block_source_lines
Definition: cover_basic_blocks.h:147
source_locationt::set_basic_block_source_lines
void set_basic_block_source_lines(const irep_idt &source_lines)
Definition: source_location.h:162
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:117
cover_basic_blockst::cover_basic_blockst
cover_basic_blockst(const goto_programt &_goto_program)
Definition: cover_basic_blocks.cpp:32
messaget::eom
static eomt eom
Definition: message.h:297
source_linest::to_string
std::string to_string() const
Construct a string representing the set of lines.
Definition: source_lines.cpp:38
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:114
cover_basic_blockst::block_of
std::size_t block_of(goto_programt::const_targett t) const override
Definition: cover_basic_blocks.cpp:96
source_linest::insert
void insert(const source_locationt &loc)
Insert a line (a source location) into the set of lines.
Definition: source_lines.cpp:22
string2int.h
cover_basic_blockst::block_map
block_mapt block_map
map program locations to block numbers
Definition: cover_basic_blocks.h:118
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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:18
cover_basic_blockst::block_infos
std::vector< block_infot > block_infos
map block numbers to block information
Definition: cover_basic_blocks.h:120
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
cover_basic_blockst::source_location_of
const source_locationt & source_location_of(std::size_t block_nr) const override
Definition: cover_basic_blocks.cpp:111
cover_basic_blocks_javat::block_of
std::size_t block_of(goto_programt::const_targett t) const override
Definition: cover_basic_blocks.cpp:215
cover_basic_blockst::update_source_lines
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
Definition: cover_basic_blocks.cpp:171
cover_basic_blocks_javat::block_locations
std::vector< source_locationt > block_locations
Definition: cover_basic_blocks.h:143
irept::is_nil
bool is_nil() const
Definition: irep.h:398
message_handlert
Definition: message.h:28
dstringt::empty
bool empty() const
Definition: dstring.h:88
format_number_range
std::string format_number_range(const std::vector< unsigned > &input_numbers)
create shorter representation for output
Definition: format_number_range.cpp:25
cover_basic_blocks_javat::block_infos
std::vector< goto_programt::const_targett > block_infos
Definition: cover_basic_blocks.h:141
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
source_locationt
Definition: source_location.h:20
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
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:231
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:224
cover_basic_blockst::block_mapt
std::map< goto_programt::const_targett, std::size_t > block_mapt
Definition: cover_basic_blocks.h:98
cover_basic_blockst::block_infot::lines
std::unordered_set< std::size_t > lines
the set of lines belonging to this block
Definition: cover_basic_blocks.h:111
cover_basic_blocks_javat::output
void output(std::ostream &out) const override
Outputs the list of blocks.
Definition: cover_basic_blocks.cpp:237
unsafe_string2unsigned
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:38
cover_basic_blockst::output
void output(std::ostream &out) const override
Outputs the list of blocks.
Definition: cover_basic_blocks.cpp:151
cover_basic_blocks.h
Basic blocks detection for Coverage Instrumentation.
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
source_locationt::set_basic_block_covered_lines
void set_basic_block_covered_lines(const irep_idt &covered_lines)
Definition: source_location.h:157
message.h
messaget::warning
mstreamt & warning() const
Definition: message.h:404
format_number_range.h
Format vector of numbers into a compressed range.
cover_basic_blockst::update_covered_lines
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,...
Definition: cover_basic_blocks.cpp:158
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:103
cover_basic_blockst::block_infot
Definition: cover_basic_blocks.h:101
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
validation_modet::INVARIANT
@ INVARIANT