cover_basic_blocks.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Coverage Instrumentation
 
Author: Daniel Kroening
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H
#define CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H
 
#include <goto-programs/goto_program.h>
 
#include "source_lines.h"
 
class message_handlert;
 
class cover_blocks_baset
{
public:
  virtual ~cover_blocks_baset() = default;
  //    part of
  virtual std::size_t block_of(goto_programt::const_targett t) const = 0;
 
  virtual std::optional<goto_programt::const_targett>
  instruction_of(std::size_t block_nr) const = 0;
 
  virtual const source_locationt &
  source_location_of(std::size_t block_nr) const = 0;
 
  virtual const source_linest &source_lines_of(std::size_t block_nr) const = 0;
 
  virtual void output(std::ostream &out) const = 0;
 
  virtual void report_block_anomalies(
    const irep_idt &function_id,
    const goto_programt &goto_program,
    message_handlert &message_handler)
  {
    // unused parameters
    (void)function_id;
    (void)goto_program;
    (void)message_handler;
  }
};
 
class cover_basic_blockst final : public cover_blocks_baset
{
public:
  explicit cover_basic_blockst(const goto_programt &goto_program);
 
  std::size_t block_of(goto_programt::const_targett t) const override;
 
  std::optional<goto_programt::const_targett>
  instruction_of(std::size_t block_nr) const override;
 
  const source_locationt &
  source_location_of(std::size_t block_nr) const override;
 
  const source_linest &source_lines_of(std::size_t block_nr) const override;
 
  void report_block_anomalies(
    const irep_idt &function_id,
    const goto_programt &goto_program,
    message_handlert &message_handler) override;
 
  void output(std::ostream &out) const override;
 
private:
  typedef std::map<
    goto_programt::const_targett,
    std::size_t,
    goto_programt::target_less_than>
    block_mapt;
 
  struct block_infot
  {
    std::optional<goto_programt::const_targett> representative_inst;
 
    source_locationt source_location;
 
    source_linest source_lines;
  };
 
  block_mapt block_map;
  std::vector<block_infot> block_infos;
 
  static void add_block_lines(
    cover_basic_blockst::block_infot &block,
    const goto_programt::instructiont &instruction);
 
  static std::optional<std::size_t> continuation_of_block(
    const goto_programt::const_targett &instruction,
    block_mapt &block_map);
};
 
class cover_basic_blocks_javat final : public cover_blocks_baset
{
private:
  // map block number to first instruction of the block
  std::vector<goto_programt::const_targett> block_infos;
  // map block number to its location
  std::vector<source_locationt> block_locations;
  // map java indexes to block indexes
  std::unordered_map<irep_idt, std::size_t> index_to_block;
  // map block number to its source lines
  std::vector<source_linest> block_source_lines;
 
public:
  explicit cover_basic_blocks_javat(const goto_programt &_goto_program);
 
  std::size_t block_of(goto_programt::const_targett t) const override;
 
  std::optional<goto_programt::const_targett>
  instruction_of(std::size_t block_number) const override;
 
  const source_locationt &
  source_location_of(std::size_t block_number) const override;
 
  const source_linest &source_lines_of(std::size_t block_number) const override;
 
  void output(std::ostream &out) const override;
};
 
#endif // CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H