cprover
cover_basic_blocks.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Coverage Instrumentation
4 
5 Author: Daniel Kroening
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H
13 #define CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H
14 
15 #include <unordered_set>
16 
17 #include <util/optional.h>
18 
20 
21 #include "source_lines.h"
22 
23 class message_handlert;
24 
26 {
27 public:
28  virtual ~cover_blocks_baset() = default;
31  // part of
32  virtual std::size_t block_of(goto_programt::const_targett t) const = 0;
33 
38  instruction_of(std::size_t block_nr) const = 0;
39 
43  virtual const source_locationt &
44  source_location_of(std::size_t block_nr) const = 0;
45 
47  virtual void output(std::ostream &out) const = 0;
48 
53  virtual void report_block_anomalies(
54  const irep_idt &function_id,
55  const goto_programt &goto_program,
56  message_handlert &message_handler)
57  {
58  // unused parameters
59  (void)function_id;
60  (void)goto_program;
61  (void)message_handler;
62  }
63 };
64 
66 {
67 public:
68  explicit cover_basic_blockst(const goto_programt &goto_program);
69 
73  std::size_t block_of(goto_programt::const_targett t) const override;
74 
79  instruction_of(std::size_t block_nr) const override;
80 
84  const source_locationt &
85  source_location_of(std::size_t block_nr) const override;
86 
92  const irep_idt &function_id,
93  const goto_programt &goto_program,
94  message_handlert &message_handler) override;
95 
97  void output(std::ostream &out) const override;
98 
99 private:
100  typedef std::map<goto_programt::const_targett, std::size_t> block_mapt;
101 
102  struct block_infot
103  {
106 
111 
113  std::unordered_set<std::size_t> lines;
114 
117  };
118 
122  std::vector<block_infot> block_infos;
123 
125  static void add_block_lines(
127  const goto_programt::instructiont &instruction);
128 
131  static void update_covered_lines(block_infot &block_info);
132 
135  static void update_source_lines(block_infot &block_info);
136 
140  const goto_programt::const_targett &instruction,
142 };
143 
145 {
146 private:
147  // map block number to first instruction of the block
148  std::vector<goto_programt::const_targett> block_infos;
149  // map block number to its location
150  std::vector<source_locationt> block_locations;
151  // map java indexes to block indexes
152  std::unordered_map<irep_idt, std::size_t> index_to_block;
153  // map block number to its source lines
154  std::vector<source_linest> block_source_lines;
155 
156 public:
157  explicit cover_basic_blocks_javat(const goto_programt &_goto_program);
158 
161  std::size_t block_of(goto_programt::const_targett t) const override;
162 
166  instruction_of(std::size_t block_number) const override;
167 
170  const source_locationt &
171  source_location_of(std::size_t block_number) const override;
172 
174  void output(std::ostream &out) const override;
175 };
176 
177 #endif // CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H
cover_basic_blockst::instruction_of
optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const override
Definition: cover_basic_blocks.cpp:98
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:152
cover_blocks_baset::source_location_of
virtual const source_locationt & source_location_of(std::size_t block_nr) const =0
optional.h
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:152
cover_basic_blocks_javat::cover_basic_blocks_javat
cover_basic_blocks_javat(const goto_programt &_goto_program)
Definition: cover_basic_blocks.cpp:193
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:110
cover_blocks_baset::output
virtual void output(std::ostream &out) const =0
Outputs the list of blocks.
cover_basic_blocks_javat::block_source_lines
std::vector< source_linest > block_source_lines
Definition: cover_basic_blocks.h:154
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:111
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:116
cover_basic_blockst::block_of
std::size_t block_of(goto_programt::const_targett t) const override
Definition: cover_basic_blocks.cpp:90
source_linest
Definition: source_lines.h:30
cover_basic_blocks_javat
Definition: cover_basic_blocks.h:145
cover_basic_blockst::block_map
block_mapt block_map
map program locations to block numbers
Definition: cover_basic_blocks.h:120
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:122
source_lines.h
Set of source code lines contributing to a basic block.
cover_blocks_baset::instruction_of
virtual optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const =0
cover_basic_blockst::source_location_of
const source_locationt & source_location_of(std::size_t block_nr) const override
Definition: cover_basic_blocks.cpp:105
cover_blocks_baset
Definition: cover_basic_blocks.h:26
cover_basic_blocks_javat::block_of
std::size_t block_of(goto_programt::const_targett t) const override
Definition: cover_basic_blocks.cpp:226
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:182
cover_basic_blocks_javat::block_locations
std::vector< source_locationt > block_locations
Definition: cover_basic_blocks.h:150
message_handlert
Definition: message.h:28
cover_basic_blocks_javat::block_infos
std::vector< goto_programt::const_targett > block_infos
Definition: cover_basic_blocks.h:148
cover_blocks_baset::report_block_anomalies
virtual void report_block_anomalies(const irep_idt &function_id, const goto_programt &goto_program, message_handlert &message_handler)
Output warnings about ignored blocks.
Definition: cover_basic_blocks.h:53
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_program.h
Concrete Goto Program.
source_locationt
Definition: source_location.h:19
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:242
cover_basic_blockst
Definition: cover_basic_blocks.h:66
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:235
cover_basic_blockst::block_mapt
std::map< goto_programt::const_targett, std::size_t > block_mapt
Definition: cover_basic_blocks.h:100
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:113
cover_basic_blocks_javat::output
void output(std::ostream &out) const override
Outputs the list of blocks.
Definition: cover_basic_blocks.cpp:248
cover_basic_blockst::output
void output(std::ostream &out) const override
Outputs the list of blocks.
Definition: cover_basic_blocks.cpp:145
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
cover_blocks_baset::~cover_blocks_baset
virtual ~cover_blocks_baset()=default
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
cover_blocks_baset::block_of
virtual std::size_t block_of(goto_programt::const_targett t) const =0
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:169
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:105
cover_basic_blockst::block_infot
Definition: cover_basic_blocks.h:103
cover_basic_blockst::cover_basic_blockst
cover_basic_blockst(const goto_programt &goto_program)
Definition: cover_basic_blocks.cpp:32