Update memory analyzer driver and options parsing

Author: danpoe

src/memory-analyzer/memory_analyzer_main.cpp

@@ -1,5 +1,13 @@
 // Copyright 2018 Author: Malte Mues <[email protected]>
-#ifdef __linux__
+
+// clang-format off
+#if defined(__linux__) || \
+    defined(__FreeBSD_kernel__) || \
+    defined(__GNU__) || \
+    defined(__unix__) || \
+    defined(__CYGWIN__) || \
+    defined(__MACH__)
+// clang-format on
 
 #include "memory_analyzer_parse_options.h"
 
@@ -8,9 +16,12 @@ int main(int argc, const char **argv)
   memory_analyzer_parse_optionst parse_options(argc, argv);
   return parse_options.main();
 }
+
 #else
+
 int main()
 {
-  throw "only supported on Linux platforms currently\n";
+  throw "the memory analyzer is only supported on Unices\n";
 }
+
 #endif

src/memory-analyzer/memory_analyzer_parse_options.cpp

@@ -1,102 +1,188 @@
-// Copyright 2018 Author: Malte Mues <[email protected]>
+/*******************************************************************\
+
+Module: Memory Analyzer
+
+Author: Malte Mues <[email protected]>
+        Daniel Poetzl
+
+\*******************************************************************/
 
 /// \file
 /// Commandline parser for the memory analyzer executing main work.
 
-#ifdef __linux__
+// clang-format off
+#if defined(__linux__) || \
+    defined(__FreeBSD_kernel__) || \
+    defined(__GNU__) || \
+    defined(__unix__) || \
+    defined(__CYGWIN__) || \
+    defined(__MACH__)
+// clang-format on
 
 #include "memory_analyzer_parse_options.h"
 #include "analyze_symbol.h"
 #include "gdb_api.h"
 
+#include <fstream>
+
+#include <ansi-c/ansi_c_language.h>
+
 #include <goto-programs/goto_model.h>
 #include <goto-programs/read_goto_binary.h>
+#include <goto-programs/show_symbol_table.h>
+
+#include <langapi/mode.h>
+
 #include <util/config.h>
 #include <util/exit_codes.h>
 #include <util/message.h>
 #include <util/string_utils.h>
+#include <util/version.h>
+
+memory_analyzer_parse_optionst::memory_analyzer_parse_optionst(
+  int argc,
+  const char *argv[])
+  : parse_options_baset(
+      MEMORY_ANALYZER_OPTIONS,
+      argc,
+      argv,
+      ui_message_handler),
+    ui_message_handler(cmdline, std::string("MEMORY-ANALYZER ") + CBMC_VERSION),
+    message(ui_message_handler)
+{
+}
 
 int memory_analyzer_parse_optionst::doit()
 {
-  // This script is the entry point and has to make sure
-  // that the config object is set to a valid architecture.
-  // config is later used to determine right size for types.
-  // If config is not set, you might see a bunch of types with
-  // size 0.
-  // It might be desierable to convert this into flags in the future.
-  config.ansi_c.mode = configt::ansi_ct::flavourt::GCC;
-  config.ansi_c.set_arch_spec_x86_64();
+  if(cmdline.isset("version"))
+  {
+    message.status() << CBMC_VERSION << '\n';
+    return CPROVER_EXIT_SUCCESS;
+  }
+
+  config.set(cmdline);
 
   if(cmdline.args.size() != 1)
   {
-    error() << "Please provide one binary with symbols to process" << eom;
-    return CPROVER_EXIT_USAGE_ERROR;
+    throw invalid_command_line_argument_exceptiont(
+      "no binary provided for analysis", "<binary>");
+  }
+
+  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(
+      "need to provide either option --core-file or option --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");
   }
 
-  std::string binary = cmdline.args[0];
+  register_language(new_ansi_c_language);
 
-  gdb_apit gdb_api = gdb_apit(binary.c_str());
+  std::string binary = cmdline.args.front();
+
+  gdb_apit gdb_api(binary.c_str());
   gdb_api.create_gdb_process();
 
-  if(cmdline.isset("core-file"))
+  if(core_file)
   {
     std::string core_file = cmdline.get_value("core-file");
     gdb_api.run_gdb_from_core(core_file);
   }
-  else if(cmdline.isset("breakpoint"))
+  else if(breakpoint)
   {
     std::string breakpoint = cmdline.get_value("breakpoint");
     gdb_api.run_gdb_to_breakpoint(breakpoint);
   }
-  else
-  {
-    error() << "Either the 'core-file' or 'breakpoint; flag must be provided\n"
-            << "Cannot execute memory-analyzer. Going to shut it down...\n"
-            << messaget::eom;
 
-    gdb_api.terminate_gdb_process();
+  const std::string symbol_list(cmdline.get_value("symbols"));
+  std::vector<std::string> result;
+  split_string(symbol_list, ',', result, true, true);
 
-    help();
-    return CPROVER_EXIT_USAGE_ERROR;
-  }
+  auto opt = read_goto_binary(binary, ui_message_handler);
 
-  if(cmdline.isset("symbols"))
+  if(!opt.has_value())
   {
-    const std::string symbol_list(cmdline.get_value("symbols"));
-    std::vector<std::string> result;
-    split_string(symbol_list, ',', result, false, false);
+    throw deserialization_exceptiont(
+      "cannot read goto binary `" + binary + "`");
+  }
 
-    goto_modelt goto_model;
-    read_goto_binary(binary, goto_model, ui_message_handler);
+  const goto_modelt goto_model(std::move(opt.value()));
 
-    symbol_analyzert analyzer(
-      goto_model.symbol_table, gdb_api, ui_message_handler);
+  symbol_analyzert analyzer(goto_model.symbol_table, gdb_api);
 
-    for(auto it = result.begin(); it != result.end(); it++)
-    {
-      messaget::result() << "analyzing symbol: " << (*it) << "\n";
-      analyzer.analyse_symbol(*it);
-    }
+  analyzer.analyze_symbols(result);
 
-    messaget::result() << "GENERATED CODE: \n" << messaget::eom;
-    messaget::result() << analyzer.get_code() << "\n" << messaget::eom;
+  std::ofstream file;
 
-    gdb_api.terminate_gdb_process();
-    return CPROVER_EXIT_SUCCESS;
+  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 = analyzer.get_snapshot_as_symbol_table();
+    show_symbol_table(snapshot, ui_message_handler);
+  }
+  else
+  {
+    std::string snapshot = analyzer.get_snapshot_as_c_code();
+    out << snapshot;
+  }
+
+  if(output_file)
+  {
+    file.close();
   }
   else
   {
-    error() << "It is required to provide the symbols flag in order to make "
-            << "this tool work.\n"
-            << messaget::eom;
+    message.result() << messaget::eom;
   }
-  gdb_api.terminate_gdb_process();
-  help();
-  return CPROVER_EXIT_USAGE_ERROR;
+
+  return CPROVER_EXIT_SUCCESS;
 }
 
 void memory_analyzer_parse_optionst::help()
 {
+  message.status()
+    << '\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("[email protected]") << '\n'
+    << '\n'
+    << "Usage:                       Purpose:\n"
+    << '\n'
+    << " memory-analyzer [-?] [-h] [--help]  show help\n"
+    << " memory-analyzer --version           show version\n"
+    << " memory-analyzer <options> <binary>  analyze binary"
+    << "\n"
+    << " --core-file <file>           analyze from core file\n"
+    << " --breakpoint <breakpoint>    analyze from breakpoint\n"
+    << " --symbols <symbol-list>      list of symbols to analyze\n"
+    << " --symtab-snapshot            output snapshot as symbol table\n"
+    << " --output-file <file>         write snapshot to file\n"
+    << messaget::eom;
 }
 
-#endif // __linux__
+#endif

src/memory-analyzer/memory_analyzer_parse_options.h

@@ -1,38 +1,53 @@
-// Copyright 2018 Author: Malte Mues <[email protected]>
+/*******************************************************************\
+
+Module: Memory Analyzer
+
+Author: Malte Mues <[email protected]>
+        Daniel Poetzl
+
+\*******************************************************************/
 
 /// \file
 /// This code does the command line parsing for the memory-analyzer tool
 
+// clang-format off
+#if defined(__linux__) || \
+    defined(__FreeBSD_kernel__) || \
+    defined(__GNU__) || \
+    defined(__unix__) || \
+    defined(__CYGWIN__) || \
+    defined(__MACH__)
+// clang-format on
+
 #ifndef CPROVER_MEMORY_ANALYZER_MEMORY_ANALYZER_PARSE_OPTIONS_H
 #define CPROVER_MEMORY_ANALYZER_MEMORY_ANALYZER_PARSE_OPTIONS_H
-#ifdef __linux__
+
 #include <util/parse_options.h>
 #include <util/ui_message.h>
 
 // clang-format off
-#define MEMMORY_ANALYZER_OPTIONS \
+#define MEMORY_ANALYZER_OPTIONS \
+  "(version)" \
+  "(json-ui)" \
   "(core-file):" \
   "(breakpoint):" \
-  "(symbols):"
-
+  "(symbols):" \
+  "(symtab-snapshot)" \
+  "(output-file):"
 // clang-format on
 
-class memory_analyzer_parse_optionst : public parse_options_baset,
-                                       public messaget
+class memory_analyzer_parse_optionst : public parse_options_baset
 {
 public:
+  memory_analyzer_parse_optionst(int argc, const char *argv[]);
+
   int doit() override;
   void help() override;
 
-  memory_analyzer_parse_optionst(int argc, const char **argv)
-    : parse_options_baset(MEMMORY_ANALYZER_OPTIONS, argc, argv),
-      messaget(ui_message_handler),
-      ui_message_handler(cmdline, "memory-analyzer")
-  {
-  }
-
 protected:
   ui_message_handlert ui_message_handler;
+  messaget message;
 };
-#endif // __linux__
+
 #endif // CPROVER_MEMORY_ANALYZER_MEMORY_ANALYZER_PARSE_OPTIONS_H
+#endif