cover.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Coverage Instrumentation
 
Author: Daniel Kroening
 
Date: May 2016
 
\*******************************************************************/
 
 
#include "cover.h"
 
#include <util/message.h>
#include <util/cmdline.h>
#include <util/options.h>
 
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_skip.h>
 
#include "cover_basic_blocks.h"
 
static void instrument_cover_goals(
  const irep_idt &function_id,
  goto_programt &goto_program,
  const cover_instrumenterst &instrumenters,
  const irep_idt &mode,
  message_handlert &message_handler,
  const cover_instrumenter_baset::assertion_factoryt &make_assertion)
{
  const std::unique_ptr<cover_blocks_baset> basic_blocks =
    mode == ID_java ? std::unique_ptr<cover_blocks_baset>(
                        new cover_basic_blocks_javat(goto_program))
                    : std::unique_ptr<cover_blocks_baset>(
                        new cover_basic_blockst(goto_program));
 
  basic_blocks->report_block_anomalies(
    function_id, goto_program, message_handler);
  instrumenters(function_id, goto_program, *basic_blocks, make_assertion);
}
 
void cover_instrumenterst::add_from_criterion(
  coverage_criteriont criterion,
  const symbol_table_baset &symbol_table,
  const goal_filterst &goal_filters)
{
  switch(criterion)
  {
  case coverage_criteriont::LOCATION:
    instrumenters.push_back(std::make_unique<cover_location_instrumentert>(
      symbol_table, goal_filters));
    break;
  case coverage_criteriont::BRANCH:
    instrumenters.push_back(
      std::make_unique<cover_branch_instrumentert>(symbol_table, goal_filters));
    break;
  case coverage_criteriont::DECISION:
    instrumenters.push_back(std::make_unique<cover_decision_instrumentert>(
      symbol_table, goal_filters));
    break;
  case coverage_criteriont::CONDITION:
    instrumenters.push_back(std::make_unique<cover_condition_instrumentert>(
      symbol_table, goal_filters));
    break;
  case coverage_criteriont::PATH:
    instrumenters.push_back(
      std::make_unique<cover_path_instrumentert>(symbol_table, goal_filters));
    break;
  case coverage_criteriont::MCDC:
    instrumenters.push_back(
      std::make_unique<cover_mcdc_instrumentert>(symbol_table, goal_filters));
    break;
  case coverage_criteriont::ASSERTION:
    instrumenters.push_back(std::make_unique<cover_assertion_instrumentert>(
      symbol_table, goal_filters));
    break;
  case coverage_criteriont::COVER:
    instrumenters.push_back(
      std::make_unique<cover_cover_instrumentert>(symbol_table, goal_filters));
    break;
  case coverage_criteriont::ASSUME:
    instrumenters.push_back(
      std::make_unique<cover_assume_instrumentert>(symbol_table, goal_filters));
  }
}
 
coverage_criteriont
parse_coverage_criterion(const std::string &criterion_string)
{
  coverage_criteriont c;
 
  if(criterion_string == "assertion" || criterion_string == "assertions")
    c = coverage_criteriont::ASSERTION;
  else if(criterion_string == "path" || criterion_string == "paths")
    c = coverage_criteriont::PATH;
  else if(criterion_string == "branch" || criterion_string == "branches")
    c = coverage_criteriont::BRANCH;
  else if(criterion_string == "location" || criterion_string == "locations")
    c = coverage_criteriont::LOCATION;
  else if(criterion_string == "decision" || criterion_string == "decisions")
    c = coverage_criteriont::DECISION;
  else if(criterion_string == "condition" || criterion_string == "conditions")
    c = coverage_criteriont::CONDITION;
  else if(criterion_string == "mcdc")
    c = coverage_criteriont::MCDC;
  else if(criterion_string == "cover")
    c = coverage_criteriont::COVER;
  else if(criterion_string == "assume" || criterion_string == "assumes")
    c = coverage_criteriont::ASSUME;
  else
  {
    std::stringstream s;
    s << "unknown coverage criterion " << '\'' << criterion_string << '\'';
    throw invalid_command_line_argument_exceptiont(s.str(), "--cover");
  }
 
  return c;
}
 
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
{
  options.set_option("cover", cmdline.get_values("cover"));
 
  // allow retrieving full traces
  options.set_option("simple-slice", false);
 
  options.set_option(
    "cover-include-pattern", cmdline.get_value("cover-include-pattern"));
  options.set_option("no-trivial-tests", cmdline.isset("no-trivial-tests"));
 
  std::string cover_only = cmdline.get_value("cover-only");
 
  if(!cover_only.empty() && cmdline.isset("cover-function-only"))
    throw invalid_command_line_argument_exceptiont(
      "at most one of --cover-only and --cover-function-only can be used",
      "--cover-only");
 
  options.set_option("cover-only", cmdline.get_value("cover-only"));
  if(cmdline.isset("cover-function-only"))
    options.set_option("cover-only", "function");
 
  options.set_option(
    "cover-traces-must-terminate",
    cmdline.isset("cover-traces-must-terminate"));
  options.set_option(
    "cover-failed-assertions", cmdline.isset("cover-failed-assertions"));
 
  options.set_option("show-test-suite", cmdline.isset("show-test-suite"));
}
 
cover_configt get_cover_config(
  const optionst &options,
  const symbol_tablet &symbol_table,
  message_handlert &message_handler)
{
  cover_configt cover_config;
  function_filterst &function_filters =
    cover_config.cover_configt::function_filters;
  std::unique_ptr<goal_filterst> &goal_filters = cover_config.goal_filters;
  cover_instrumenterst &instrumenters = cover_config.cover_instrumenters;
 
  function_filters.add(std::make_unique<internal_functions_filtert>());
 
  goal_filters->add(std::make_unique<internal_goals_filtert>());
 
  optionst::value_listt criteria_strings = options.get_list_option("cover");
 
  cover_config.keep_assertions = false;
  for(const auto &criterion_string : criteria_strings)
  {
    coverage_criteriont c = parse_coverage_criterion(criterion_string);
 
    if(c == coverage_criteriont::ASSERTION)
      cover_config.keep_assertions = true;
    // Make sure that existing assertions don't get replaced by assumes
    else if(c == coverage_criteriont::ASSUME)
      cover_config.keep_assertions = true;
 
    instrumenters.add_from_criterion(c, symbol_table, *goal_filters);
  }
 
  if(cover_config.keep_assertions && criteria_strings.size() > 1)
  {
    std::stringstream s;
    s << "assertion coverage cannot currently be used together with other"
      << "coverage criteria";
    throw invalid_command_line_argument_exceptiont(s.str(), "--cover");
  }
 
  std::string cover_include_pattern =
    options.get_option("cover-include-pattern");
  if(!cover_include_pattern.empty())
  {
    function_filters.add(
      std::make_unique<include_pattern_filtert>(cover_include_pattern));
  }
 
  if(options.get_bool_option("no-trivial-tests"))
    function_filters.add(std::make_unique<trivial_functions_filtert>());
 
  cover_config.traces_must_terminate =
    options.get_bool_option("cover-traces-must-terminate");
 
  cover_config.cover_failed_assertions =
    options.get_bool_option("cover-failed-assertions");
 
  return cover_config;
}
 
cover_configt get_cover_config(
  const optionst &options,
  const irep_idt &main_function_id,
  const symbol_tablet &symbol_table,
  message_handlert &message_handler)
{
  cover_configt cover_config =
    get_cover_config(options, symbol_table, message_handler);
 
  std::string cover_only = options.get_option("cover-only");
 
  // cover entry point function only
  if(cover_only == "function")
  {
    const symbolt &main_symbol = symbol_table.lookup_ref(main_function_id);
    cover_config.function_filters.add(
      std::make_unique<single_function_filtert>(main_symbol.name));
  }
  else if(cover_only == "file")
  {
    const symbolt &main_symbol = symbol_table.lookup_ref(main_function_id);
    cover_config.function_filters.add(
      std::make_unique<file_filtert>(main_symbol.location.get_file()));
  }
  else if(!cover_only.empty())
  {
    std::stringstream s;
    s << "Argument to --cover-only not recognized: " << cover_only;
    throw invalid_command_line_argument_exceptiont(s.str(), "--cover-only");
  }
 
  return cover_config;
}
 
static void instrument_cover_goals(
  const cover_configt &cover_config,
  const symbolt &function_symbol,
  goto_functionst::goto_functiont &function,
  message_handlert &message_handler)
{
  if(!cover_config.keep_assertions)
  {
    Forall_goto_program_instructions(i_it, function.body)
    {
      // Simplify the common case where we have ASSERT(x); ASSUME(x):
      if(i_it->is_assert())
      {
        if(!cover_config.cover_failed_assertions)
        {
          auto successor = std::next(i_it);
          if(
            successor != function.body.instructions.end() &&
            successor->is_assume() &&
            successor->condition() == i_it->condition())
          {
            successor->turn_into_skip();
          }
 
          i_it->turn_into_assume();
        }
        else
        {
          i_it->turn_into_skip();
        }
      }
    }
  }
 
  bool changed = false;
 
  if(cover_config.function_filters(function_symbol, function))
  {
    messaget msg(message_handler);
    msg.debug() << "Instrumenting coverage for function "
                << id2string(function_symbol.name) << messaget::eom;
    instrument_cover_goals(
      function_symbol.name,
      function.body,
      cover_config.cover_instrumenters,
      function_symbol.mode,
      message_handler,
      cover_config.make_assertion);
    changed = true;
  }
 
  if(
    cover_config.traces_must_terminate &&
    function_symbol.name == goto_functionst::entry_point())
  {
    cover_instrument_end_of_function(
      function_symbol.name, function.body, cover_config.make_assertion);
    changed = true;
  }
 
  if(changed)
    remove_skip(function.body);
}
 
void instrument_cover_goals(
  const cover_configt &cover_config,
  goto_model_functiont &function,
  message_handlert &message_handler)
{
  const symbolt function_symbol =
    function.get_symbol_table().lookup_ref(function.get_function_id());
  instrument_cover_goals(
    cover_config,
    function_symbol,
    function.get_goto_function(),
    message_handler);
 
  function.compute_location_numbers();
}
 
bool instrument_cover_goals(
  const cover_configt &cover_config,
  const symbol_tablet &symbol_table,
  goto_functionst &goto_functions,
  message_handlert &message_handler)
{
  messaget msg(message_handler);
  msg.status() << "Rewriting existing assertions as assumptions"
               << messaget::eom;
 
  if(
    cover_config.traces_must_terminate &&
    !goto_functions.function_map.count(goto_functions.entry_point()))
  {
    msg.error() << "cover-traces-must-terminate: invalid entry point ["
                << goto_functions.entry_point() << "]" << messaget::eom;
    return true;
  }
 
  for(auto &gf_entry : goto_functions.function_map)
  {
    const symbolt function_symbol = symbol_table.lookup_ref(gf_entry.first);
    instrument_cover_goals(
      cover_config, function_symbol, gf_entry.second, message_handler);
  }
  goto_functions.compute_location_numbers();
 
  cover_config.function_filters.report_anomalies();
  cover_config.goal_filters->report_anomalies();
 
  return false;
}
 
bool instrument_cover_goals(
  const cover_configt &cover_config,
  goto_modelt &goto_model,
  message_handlert &message_handler)
{
  return instrument_cover_goals(
    cover_config,
    goto_model.symbol_table,
    goto_model.goto_functions,
    message_handler);
}