goto_harness_parse_options.cpp

Go to the documentation of this file.

/******************************************************************\
 
Module: goto_harness_parse_options
 
Author: Diffblue Ltd.
 
\******************************************************************/
 
#include "goto_harness_parse_options.h"
 
#include <util/config.h>
#include <util/exception_utils.h>
#include <util/exit_codes.h>
#include <util/help_formatter.h>
#include <util/invariant.h>
#include <util/suffix.h>
#include <util/version.h>
 
#include <goto-programs/goto_model.h>
#include <goto-programs/read_goto_binary.h>
#include <goto-programs/write_goto_binary.h>
 
#include <goto-instrument/dump_c.h>
 
#include "function_call_harness_generator.h"
#include "goto_harness_generator_factory.h"
#include "memory_snapshot_harness_generator.h"
 
#include <algorithm>
#include <fstream>
#include <iostream>
#include <set>
#include <string>
#include <unordered_set>
#include <utility>
 
std::unordered_set<irep_idt>
get_symbol_names_from_goto_model(const goto_modelt &goto_model)
{
  auto symbols = std::unordered_set<irep_idt>{};
  std::transform(
    goto_model.get_symbol_table().begin(),
    goto_model.get_symbol_table().end(),
    std::inserter(symbols, symbols.end()),
    [](const std::pair<const irep_idt, symbolt> &key_value_pair) {
      return key_value_pair.first;
    });
  return symbols;
}
 
static void filter_goto_model(
  goto_modelt &goto_model_with_harness,
  const std::unordered_set<irep_idt> &goto_model_without_harness_symbols)
{
  for(auto const &symbol_id : goto_model_without_harness_symbols)
  {
    auto &symbol =
      goto_model_with_harness.symbol_table.get_writeable_ref(symbol_id);
    if(symbol.is_function())
    {
      // We don’t want bodies of functions that already existed in the
      // symbol table (i.e. not generated by us)
      goto_model_with_harness.unload(symbol_id);
      if(symbol.is_file_local)
      {
        goto_model_with_harness.symbol_table.remove(symbol_id);
      }
    }
    else if(!symbol.is_type && symbol.is_file_local)
    {
      // We don’t want file local symbols from an existing goto model
      // except types / typedefs, which also apparently get marked
      // file local sometimes.
      goto_model_with_harness.symbol_table.remove(symbol_id);
    }
    else if(!symbol.is_type && symbol.is_static_lifetime)
    {
      // if it has static lifetime and is *not* a type it is a global variable
      // We keep around other global variables in case we want to initialise
      // them, but mark them as extern so we don't duplicate their definitions
      symbol.value = nil_exprt{};
      symbol.is_extern = true;
    }
  }
}
 
// The basic idea is that this module is handling the following
// sequence of events:
// 1. Initialise a goto-model by parsing an input (goto) binary
// 2. Initialise the harness generator (with some config) that will handle
//    the mutation of the goto-model. The generator should create a new
//    function that can be called by `cbmc --function`. The generated function
//    should implement the behaviour of the harness (What exactly this means
//    depends on the configuration)
// 3. Write the end result of that process to the output binary
 
int goto_harness_parse_optionst::doit()
{
  if(cmdline.isset("version"))
  {
    std::cout << CBMC_VERSION << '\n';
    return CPROVER_EXIT_SUCCESS;
  }
 
  auto got_harness_config = handle_common_options();
  auto factory = make_factory();
 
  auto factory_options = collect_generate_factory_options();
 
  // This just sets up the defaults (and would interpret options such as --32).
  config.set(cmdline);
 
  // Normally we would register language front-ends here but as goto-harness
  // only works on goto binaries, we don't need to
 
  // Read goto binary into goto-model
  auto read_goto_binary_result =
    read_goto_binary(got_harness_config.in_file, ui_message_handler);
  if(!read_goto_binary_result.has_value())
  {
    throw deserialization_exceptiont{"failed to read goto program from file '" +
                                     got_harness_config.in_file + "'"};
  }
  auto goto_model = std::move(read_goto_binary_result.value());
  auto const goto_model_without_harness_symbols =
    get_symbol_names_from_goto_model(goto_model);
 
  // This has to be called after the defaults are set up (as per the
  // config.set(cmdline) above) otherwise, e.g. the architecture specification
  // will be unknown.
  config.set_from_symbol_table(goto_model.symbol_table);
 
  if(goto_model.symbol_table.has_symbol(
       got_harness_config.harness_function_name))
  {
    throw invalid_command_line_argument_exceptiont(
      "harness function `" +
        id2string(got_harness_config.harness_function_name) +
        "` already in "
        "the symbol table",
      "--" GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT);
  }
 
  // Initialise harness generator
  auto harness_generator = factory.factory(
    got_harness_config.harness_type, factory_options, goto_model);
  CHECK_RETURN(harness_generator != nullptr);
 
  harness_generator->generate(
    goto_model, got_harness_config.harness_function_name);
 
  if(has_suffix(got_harness_config.out_file, ".c"))
  {
    filter_goto_model(goto_model, goto_model_without_harness_symbols);
    auto harness_out = std::ofstream{got_harness_config.out_file};
    dump_c(
      goto_model.goto_functions,
      true,
      true,
      false,
      namespacet{goto_model.get_symbol_table()},
      harness_out);
  }
  else
  {
    write_goto_binary(
      got_harness_config.out_file, goto_model, log.get_message_handler());
  }
 
  return CPROVER_EXIT_SUCCESS;
}
 
void goto_harness_parse_optionst::help()
{
  std::cout << '\n'
            << banner_string("Goto-Harness", CBMC_VERSION) << '\n'
            << align_center_with_border("Copyright (C) 2019") << '\n'
            << align_center_with_border("Diffblue Ltd.") << '\n'
            << align_center_with_border("info@diffblue.com") << '\n';
 
  // clang-format off
  std::cout << help_formatter(
    "\n"
    "Usage:                     \tPurpose:\n"
    "\n"
    " {bgoto-harness} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
    " {bgoto-harness} {y--version} \t show version and exit\n"
    " {bgoto-harness} {uin} {uout} {y--harness-function-name} {uname}"
    " {y--harness-type} {uharness-type} [harness options]\n"
    "\n"
    "  {uin} \t goto binary to read from\n"
    "  {uout} \t file to write the harness to; the harness is printed as C"
    " code, if {uout} has a .c suffix, else a goto binary including the harness"
    " is generated\n"
    " {y--harness-function-name} {uname} \t the name of the harness function to"
    " generate\n"
    " {y--harness-type} {utype} \t one of the harness types listed below\n"
    "\n"
    FUNCTION_HARNESS_GENERATOR_HELP
    "\n"
    MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP
    "\n");
  // clang-format on
}
 
goto_harness_parse_optionst::goto_harness_parse_optionst(
  int argc,
  const char *argv[])
  : parse_options_baset{GOTO_HARNESS_OPTIONS,
                        argc,
                        argv,
                        std::string("GOTO-HARNESS ") + CBMC_VERSION}
{
}
 
goto_harness_parse_optionst::goto_harness_configt
goto_harness_parse_optionst::handle_common_options()
{
  goto_harness_configt goto_harness_config{};
 
  // This just checks the positional arguments to be 2.
  // Options are not in .args
  if(cmdline.args.size() != 2)
  {
    help();
    throw invalid_command_line_argument_exceptiont{
      "need to specify both input and output file names (may be "
      "the same)",
      "<in goto binary> <output C file or goto binary>"};
  }
 
  goto_harness_config.in_file = cmdline.args[0];
  goto_harness_config.out_file = cmdline.args[1];
 
  if(!cmdline.isset(GOTO_HARNESS_GENERATOR_TYPE_OPT))
  {
    throw invalid_command_line_argument_exceptiont{
      "required option not set", "--" GOTO_HARNESS_GENERATOR_TYPE_OPT};
  }
  goto_harness_config.harness_type =
    cmdline.get_value(GOTO_HARNESS_GENERATOR_TYPE_OPT);
 
  // Read the name of the harness function to generate
  if(!cmdline.isset(GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT))
  {
    throw invalid_command_line_argument_exceptiont{
      "required option not set",
      "--" GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT};
  }
  goto_harness_config.harness_function_name = {
    cmdline.get_value(GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT)};
 
  return goto_harness_config;
}
 
goto_harness_generator_factoryt goto_harness_parse_optionst::make_factory()
{
  auto factory = goto_harness_generator_factoryt{};
  factory.register_generator("call-function", [this]() {
    return std::make_unique<function_call_harness_generatort>(
      ui_message_handler);
  });
 
  factory.register_generator("initialize-with-memory-snapshot", [this]() {
    return std::make_unique<memory_snapshot_harness_generatort>(
      ui_message_handler);
  });
 
  return factory;
}
 
goto_harness_generator_factoryt::generator_optionst
goto_harness_parse_optionst::collect_generate_factory_options()
{
  auto const common_options =
    std::set<std::string>{"version",
                          GOTO_HARNESS_GENERATOR_TYPE_OPT,
                          GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT};
 
  auto factory_options = goto_harness_generator_factoryt::generator_optionst{};
 
  for(auto const &option : cmdline.option_names())
  {
    if(common_options.find(option) == common_options.end())
    {
      factory_options.insert({option, cmdline.get_values(option.c_str())});
    }
  }
 
  return factory_options;
}