cover_instrument.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Coverage Instrumentation
 
Author: Peter Schrammel
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H
#define CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H
 
#include <memory>
 
#include <util/symbol_table.h>
 
#include <goto-programs/goto_program.h>
 
enum class coverage_criteriont;
class cover_blocks_baset;
class goal_filterst;
 
class cover_instrumenter_baset
{
public:
  virtual ~cover_instrumenter_baset() = default;
  cover_instrumenter_baset(
    const symbol_tablet &_symbol_table,
    const goal_filterst &_goal_filters,
    const irep_idt &_coverage_criterion)
    : coverage_criterion(_coverage_criterion),
      ns(_symbol_table),
      goal_filters(_goal_filters)
  {
  }
 
  using assertion_factoryt = std::function<
    goto_programt::instructiont(const exprt &, const source_locationt &)>;
  static_assert(
    std::is_same<
      assertion_factoryt,
      std::function<decltype(goto_programt::make_assertion)>>::value,
    "`assertion_factoryt` is expected to have the same type as "
    "`goto_programt::make_assertion`.");
 
  void operator()(
    const irep_idt &function_id,
    goto_programt &goto_program,
    const cover_blocks_baset &basic_blocks,
    const assertion_factoryt &make_assertion) const
  {
    Forall_goto_program_instructions(i_it, goto_program)
    {
      instrument(function_id, goto_program, i_it, basic_blocks, make_assertion);
    }
  }
 
  const irep_idt property_class = "coverage";
  const irep_idt coverage_criterion;
 
protected:
  const namespacet ns;
  const goal_filterst &goal_filters;
 
  virtual void instrument(
    const irep_idt &function_id,
    goto_programt &,
    goto_programt::targett &,
    const cover_blocks_baset &,
    const assertion_factoryt &) const = 0;
 
  void initialize_source_location(
    goto_programt::targett t,
    const std::string &comment,
    const irep_idt &function_id) const
  {
    t->source_location_nonconst().set_comment(comment);
    t->source_location_nonconst().set(
      ID_coverage_criterion, coverage_criterion);
    t->source_location_nonconst().set_property_class(property_class);
    t->source_location_nonconst().set_function(function_id);
  }
 
  bool is_non_cover_assertion(goto_programt::const_targett t) const
  {
    return t->is_assert() &&
           t->source_location().get_property_class() != property_class;
  }
};
 
class cover_instrumenterst
{
public:
  void add_from_criterion(
    coverage_criteriont,
    const symbol_tablet &,
    const goal_filterst &);
 
  void operator()(
    const irep_idt &function_id,
    goto_programt &goto_program,
    const cover_blocks_baset &basic_blocks,
    const cover_instrumenter_baset::assertion_factoryt &make_assertion) const
  {
    for(const auto &instrumenter : instrumenters)
      (*instrumenter)(function_id, goto_program, basic_blocks, make_assertion);
  }
 
private:
  std::vector<std::unique_ptr<cover_instrumenter_baset>> instrumenters;
};
 
class cover_location_instrumentert : public cover_instrumenter_baset
{
public:
  cover_location_instrumentert(
    const symbol_tablet &_symbol_table,
    const goal_filterst &_goal_filters)
    : cover_instrumenter_baset(_symbol_table, _goal_filters, "location")
  {
  }
 
protected:
  void instrument(
    const irep_idt &function_id,
    goto_programt &,
    goto_programt::targett &,
    const cover_blocks_baset &,
    const assertion_factoryt &) const override;
};
 
class cover_branch_instrumentert : public cover_instrumenter_baset
{
public:
  cover_branch_instrumentert(
    const symbol_tablet &_symbol_table,
    const goal_filterst &_goal_filters)
    : cover_instrumenter_baset(_symbol_table, _goal_filters, "branch")
  {
  }
 
protected:
  void instrument(
    const irep_idt &function_id,
    goto_programt &,
    goto_programt::targett &,
    const cover_blocks_baset &,
    const assertion_factoryt &) const override;
};
 
class cover_condition_instrumentert : public cover_instrumenter_baset
{
public:
  cover_condition_instrumentert(
    const symbol_tablet &_symbol_table,
    const goal_filterst &_goal_filters)
    : cover_instrumenter_baset(_symbol_table, _goal_filters, "condition")
  {
  }
 
protected:
  void instrument(
    const irep_idt &function_id,
    goto_programt &,
    goto_programt::targett &,
    const cover_blocks_baset &,
    const assertion_factoryt &) const override;
};
 
class cover_decision_instrumentert : public cover_instrumenter_baset
{
public:
  cover_decision_instrumentert(
    const symbol_tablet &_symbol_table,
    const goal_filterst &_goal_filters)
    : cover_instrumenter_baset(_symbol_table, _goal_filters, "decision")
  {
  }
 
protected:
  void instrument(
    const irep_idt &function_id,
    goto_programt &,
    goto_programt::targett &,
    const cover_blocks_baset &,
    const assertion_factoryt &) const override;
};
 
class cover_mcdc_instrumentert : public cover_instrumenter_baset
{
public:
  cover_mcdc_instrumentert(
    const symbol_tablet &_symbol_table,
    const goal_filterst &_goal_filters)
    : cover_instrumenter_baset(_symbol_table, _goal_filters, "MC/DC")
  {
  }
 
protected:
  void instrument(
    const irep_idt &function_id,
    goto_programt &,
    goto_programt::targett &,
    const cover_blocks_baset &,
    const assertion_factoryt &) const override;
};
 
class cover_path_instrumentert : public cover_instrumenter_baset
{
public:
  cover_path_instrumentert(
    const symbol_tablet &_symbol_table,
    const goal_filterst &_goal_filters)
    : cover_instrumenter_baset(_symbol_table, _goal_filters, "path")
  {
  }
 
protected:
  void instrument(
    const irep_idt &function_id,
    goto_programt &,
    goto_programt::targett &,
    const cover_blocks_baset &,
    const assertion_factoryt &) const override;
};
 
class cover_assertion_instrumentert : public cover_instrumenter_baset
{
public:
  cover_assertion_instrumentert(
    const symbol_tablet &_symbol_table,
    const goal_filterst &_goal_filters)
    : cover_instrumenter_baset(_symbol_table, _goal_filters, "assertion")
  {
  }
 
protected:
  void instrument(
    const irep_idt &function_id,
    goto_programt &,
    goto_programt::targett &,
    const cover_blocks_baset &,
    const assertion_factoryt &) const override;
};
 
class cover_cover_instrumentert : public cover_instrumenter_baset
{
public:
  cover_cover_instrumentert(
    const symbol_tablet &_symbol_table,
    const goal_filterst &_goal_filters)
    : cover_instrumenter_baset(_symbol_table, _goal_filters, "cover")
  {
  }
 
protected:
  void instrument(
    const irep_idt &function_id,
    goto_programt &,
    goto_programt::targett &,
    const cover_blocks_baset &,
    const assertion_factoryt &) const override;
};
 
void cover_instrument_end_of_function(
  const irep_idt &function_id,
  goto_programt &goto_program,
  const cover_instrumenter_baset::assertion_factoryt &);
 
// assume-instructions instrumenter.
class cover_assume_instrumentert : public cover_instrumenter_baset
{
public:
  cover_assume_instrumentert(
    const symbol_tablet &_symbol_table,
    const goal_filterst &_goal_filters)
    : cover_instrumenter_baset(_symbol_table, _goal_filters, "location")
  {
  }
 
protected:
  void instrument(
    const irep_idt &,
    goto_programt &,
    goto_programt::targett &,
    const cover_blocks_baset &,
    const assertion_factoryt &) const override;
};
 
#endif // CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H