memory_analyzer_parse_options.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Memory Analyzer
 
Author: Malte Mues <mail.mues@gmail.com>
        Daniel Poetzl
 
\*******************************************************************/

 
#include "memory_analyzer_parse_options.h"
 
#include <util/config.h>
#include <util/exit_codes.h>
#include <util/help_formatter.h>
#include <util/message.h>
#include <util/version.h>
 
#include <goto-programs/goto_model.h>
#include <goto-programs/read_goto_binary.h>
#include <goto-programs/show_symbol_table.h>
 
#include <ansi-c/ansi_c_language.h>
#include <langapi/mode.h>
 
#include "analyze_symbol.h"
 
#include <fstream> // IWYU pragma: keep
#include <iostream>
 
memory_analyzer_parse_optionst::memory_analyzer_parse_optionst(
  int argc,
  const char *argv[])
  : parse_options_baset(
      MEMORY_ANALYZER_OPTIONS,
      argc,
      argv,
      std::string("MEMORY-ANALYZER ") + CBMC_VERSION),
    message(ui_message_handler)
{
}
 
void memory_analyzer_parse_optionst::register_languages()
{
  // For now only C is supported due to the additional challenges of
  // mapping source code to debugging symbols in other languages.
  register_language(new_ansi_c_language);
}
 
int memory_analyzer_parse_optionst::doit()
{
  if(cmdline.isset("version"))
  {
    std::cout << CBMC_VERSION << '\n';
    return CPROVER_EXIT_SUCCESS;
  }
 
  config.set(cmdline);
 
  if(cmdline.args.size() < 1)
  {
    throw invalid_command_line_argument_exceptiont(
      "no binary provided for analysis", "<binary> <args>");
  }
 
  if(!cmdline.isset("symbols"))
  {
    throw invalid_command_line_argument_exceptiont(
      "need to provide symbols to analyse via --symbols", "--symbols");
  }
 
  const bool core_file = cmdline.isset("core-file");
  const bool breakpoint = cmdline.isset("breakpoint");
 
  if(core_file && breakpoint)
  {
    throw invalid_command_line_argument_exceptiont(
      "cannot start gdb from both core-file and breakpoint",
      "--core-file/--breakpoint");
  }
 
  if(!core_file && !breakpoint)
  {
    throw invalid_command_line_argument_exceptiont(
      "need to provide either core-file or breakpoint for gdb",
      "--core-file/--breakpoint");
  }
 
  const bool output_file = cmdline.isset("output-file");
  const bool symtab_snapshot = cmdline.isset("symtab-snapshot");
 
  if(symtab_snapshot && output_file)
  {
    throw invalid_command_line_argument_exceptiont(
      "printing to a file is not supported for symbol table snapshot output",
      "--symtab-snapshot");
  }
 
  register_languages();
 
  std::string binary = cmdline.args.front();
 
  auto opt = read_goto_binary(binary, ui_message_handler);
 
  if(!opt.has_value())
  {
    throw deserialization_exceptiont(
      "cannot read goto binary '" + binary + "'");
  }
 
  const goto_modelt goto_model(std::move(opt.value()));
 
  gdb_value_extractort gdb_value_extractor(
    goto_model.symbol_table, cmdline.args);
  gdb_value_extractor.create_gdb_process();
 
  if(core_file)
  {
    std::string core_file = cmdline.get_value("core-file");
    gdb_value_extractor.run_gdb_from_core(core_file);
  }
  else if(breakpoint)
  {
    std::string breakpoint = cmdline.get_value("breakpoint");
    gdb_value_extractor.run_gdb_to_breakpoint(breakpoint);
  }
 
  gdb_value_extractor.analyze_symbols(
    cmdline.get_comma_separated_values("symbols"));
 
  std::ofstream file;
 
  if(output_file)
  {
    file.open(cmdline.get_value("output-file"));
  }
 
  std::ostream &out =
    output_file ? (std::ostream &)file : (std::ostream &)message.result();
 
  if(symtab_snapshot)
  {
    symbol_tablet snapshot = gdb_value_extractor.get_snapshot_as_symbol_table();
    show_symbol_table(snapshot, ui_message_handler);
  }
  else
  {
    std::string snapshot = gdb_value_extractor.get_snapshot_as_c_code();
    out << snapshot;
  }
 
  if(output_file)
  {
    file.close();
  }
  else
  {
    message.result() << messaget::eom;
  }
 
  return CPROVER_EXIT_SUCCESS;
}
 
void memory_analyzer_parse_optionst::help()
{
  std::cout << '\n'
            << banner_string("Memory-Analyzer", CBMC_VERSION) << '\n'
            << align_center_with_border("Copyright (C) 2019") << '\n'
            << align_center_with_border("Malte Mues, Diffblue Ltd.") << '\n'
            << align_center_with_border("info@diffblue.com") << '\n';
 
  // clang-format off
  std::cout << help_formatter(
    "\n"
    "Usage:                     \tPurpose:\n"
    "\n"
    " {bmemory-analyzer} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
    " {bmemory-analyzer} {y--version} \t show version\n"
    " {bmemory-analyzer} [options] {y--symbols} {usymbol-list} {ubinary} \t"
    " analyze {ubinary}\n"
    "\n"
    "Main options:\n"
    " {y--core-file} {ufile_name} \t analyze from core file {ufile_name}\n"
    " {y--breakpoint} {uname} \t analyze from breakpoint {uname}\n"
    " {y--symbols} {usymbol-list} \t list of symbols to analyze\n"
    " {y--symtab-snapshot} \t output snapshot as symbol table\n"
    " {y--output-file} {ufile_name} \t write snapshot to file {ufile_name}\n"
    " {y--json-ui} \t output snapshot in JSON format\n"
    "\n");
  // clang-format on
}