Adding initial version of goto-inspect.

This allows to inspect a goto-binary (this means showing the goto-functions,
for now at least).

The reason this binary is helpful is that different tools (CBMC, goto-instrument, etc)
perform instrumentation before showing the goto-functions, and there's a need
to be able to inspect certain properties of a goto-binary without doing instrumentation.

Author: NlightNFotis

CMakeLists.txt

@@ -230,6 +230,7 @@ cprover_default_properties(
     goto-checker
     goto-diff
     goto-diff-lib
+    goto-inspect
     goto-harness
     goto-instrument
     goto-instrument-lib

src/CMakeLists.txt

@@ -98,6 +98,7 @@ add_subdirectory(xmllang)
 add_subdirectory(goto-checker)
 add_subdirectory(goto-programs)
 add_subdirectory(goto-symex)
+add_subdirectory(goto-inspect)
 add_subdirectory(jsil)
 add_subdirectory(json)
 add_subdirectory(json-symtab-language)

src/goto-inspect/CMakeLists.txt

@@ -0,0 +1,17 @@
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_executable(goto-inspect ${sources})
+generic_includes(goto-inspect)
+
+target_link_libraries(goto-inspect
+  util
+  goto-programs
+)
+install(TARGETS goto-inspect DESTINATION ${CMAKE_INSTALL_BINDIR})
+
+# # Man page
+# if(NOT WIN32)
+#   install(
+#     DIRECTORY ${CMAKE_SOURCE_DIR}/doc/man/
+#     DESTINATION ${CMAKE_INSTALL_MANDIR}/man1
+#     FILES_MATCHING PATTERN "goto-harness*")
+# endif()

src/goto-inspect/goto_inspect_main.cpp

@@ -0,0 +1,8 @@
+// Author: Fotis Koutoulakis for Diffblue Ltd.
+
+#include "goto_inspect_parse_options.h"
+
+int main(int argc, const char *argv[])
+{
+  return goto_inspect_parse_optionst{argc, argv}.main();
+}

src/goto-inspect/goto_inspect_parse_options.cpp

@@ -0,0 +1,99 @@
+// Author: Fotis Koutoulakis for Diffblue Ltd.
+
+#include "goto_inspect_parse_options.h"
+
+#include <util/config.h>
+#include <util/exception_utils.h>
+#include <util/exit_codes.h>
+#include <util/invariant.h>
+#include <util/make_unique.h>
+#include <util/version.h>
+
+#include <goto-programs/goto_model.h>
+#include <goto-programs/read_goto_binary.h>
+#include <goto-programs/show_goto_functions.h>
+
+#include <iostream>
+
+int goto_inspect_parse_optionst::doit()
+{
+  if(cmdline.isset("version"))
+  {
+    std::cout << CBMC_VERSION << '\n';
+    return CPROVER_EXIT_SUCCESS;
+  }
+
+  // Before we do anything else, positional arguments needs to be > 1.
+  // (i.e. a filename has been given).
+  if(cmdline.args.size() < 1)
+  {
+    help();
+    throw invalid_command_line_argument_exceptiont{
+      "failed to supply a goto-binary name",
+      "<input goto-binary> <inspection-option>"};
+  }
+
+  // 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
+
+  auto binary_filename = cmdline.args[0];
+
+  // Read goto binary into goto-model
+  auto read_goto_binary_result =
+    read_goto_binary(binary_filename, ui_message_handler);
+  if(!read_goto_binary_result.has_value())
+  {
+    throw deserialization_exceptiont{
+      "failed to read goto program from file '" + binary_filename + "'"};
+  }
+  auto goto_model = std::move(read_goto_binary_result.value());
+
+  // 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(
+    cmdline.isset("show-goto-functions") ||
+    cmdline.isset("list-goto-functions"))
+  {
+    show_goto_functions(
+      goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
+    return CPROVER_EXIT_SUCCESS;
+  }
+
+  // No options was passed in - erroneously?
+  return CPROVER_EXIT_INCORRECT_TASK;
+}
+
+void goto_inspect_parse_optionst::help()
+{
+  std::cout << '\n'
+            << banner_string("Goto-Inspect", CBMC_VERSION) << '\n'
+            << align_center_with_border("Copyright (C) 2023") << '\n'
+            << align_center_with_border("Diffblue Ltd.") << '\n'
+            << align_center_with_border("[email protected]") << '\n'
+            << '\n'
+            << "Usage:                       Purpose:\n"
+            << '\n'
+            << " goto-inspect [-?] [-h] [--help]     show help\n"
+            << " goto-inspect --version              show version\n"
+            << " goto-inspect --show-goto-functions  show code for "
+               "goto-functions present in goto-binary\n"
+            << "\n"
+            << "<in>                       goto binary to read from\n";
+}
+
+goto_inspect_parse_optionst::goto_inspect_parse_optionst(
+  int argc,
+  const char *argv[])
+  : parse_options_baset{
+      GOTO_INSPECT_OPTIONS,
+      argc,
+      argv,
+      std::string("GOTO-INSPECT ") + CBMC_VERSION}
+{
+}

src/goto-inspect/goto_inspect_parse_options.h

@@ -0,0 +1,26 @@
+// Author: Fotis Koutoulakis for Diffblue Ltd.
+
+#ifndef CPROVER_GOTO_INSPECT_PARSE_OPTIONS_H
+#define CPROVER_GOTO_INSPECT_PARSE_OPTIONS_H
+
+#include <util/parse_options.h>
+
+#include <string>
+
+// clang-format off
+#define GOTO_INSPECT_OPTIONS                                                   \
+  "(version)"                                                                  \
+  "(show-goto-functions)"                                                      \
+// end GOTO_INSPECT_OPTIONS
+
+// clang-format on
+
+struct goto_inspect_parse_optionst : public parse_options_baset
+{
+  int doit() override;
+  void help() override;
+
+  goto_inspect_parse_optionst(int argc, const char *argv[]);
+};
+
+#endif // CPROVER_GOTO_INSPECT_PARSE_OPTIONS_H