Adding initial version of goto-inspect.

NlightNFotis · NlightNFotis · commit 5cffca73ce8b · 2023-05-19T16:30:13.000+01:00
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.
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -158,6 +158,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
               "$<TARGET_FILE:goto-cc>"
               "$<TARGET_FILE:goto-diff>"
               "$<TARGET_FILE:goto-instrument>"
+              "$<TARGET_FILE:goto-inspect>"
               "$<TARGET_FILE:goto-synthesizer>"
               "$<TARGET_FILE:janalyzer>"
               "$<TARGET_FILE:jbmc>"
@@ -230,6 +231,7 @@ cprover_default_properties(
     goto-checker
     goto-diff
     goto-diff-lib
+    goto-inspect
     goto-harness
     goto-instrument
     goto-instrument-lib
diff --git a/CODEOWNERS b/CODEOWNERS
@@ -53,6 +53,7 @@
 /src/goto-harness/ @martin-cs @chris-ryder @peterschrammel
 /src/goto-instrument/ @martin-cs @chris-ryder @peterschrammel @tautschnig @kroening
 /src/goto-instrument/contracts/ @tautschnig @feliperodri @remi-delmas-3000
+/src/goto-inspect/ @diffblue/diffblue-opensource
 /src/goto-synthesizer/ @qinheping @tautschnig @feliperodri @remi-delmas-3000
 /src/goto-diff/ @tautschnig @peterschrammel
 /src/jsil/ @kroening @tautschnig
diff --git a/doc/man/goto-inspect.1 b/doc/man/goto-inspect.1
@@ -0,0 +1,33 @@
+.TH GOTO-INSPECT "2" "May 2023" "goto-inspect-5.81.0" "User Commands"
+.SH NAME
+goto\-inspect \- Inspect goto-binaries.
+.SH SYNOPSIS
+.TP
+.B goto\-inspect [\-?] [\-h] [\-\-help]
+show help
+.TP
+.B goto\-inspect \-\-version
+show version and exit
+.TP
+.B goto\-inspect [options] \fIin\fR
+Inspect (show properties, goto-functions, etc of) given goto-binary.  
+.SH DESCRIPTION
+\fBgoto-inspect\fR reads a GOTO binary, and shows goto-functions, properties,
+and other attributes associated with the goto-program.
+.SH OPTIONS
+.SS "User-interface options:"
+.TP
+\fB\-\-show\-goto\-functions\fR
+print the goto-program instructions for the functions contained by the binary.
+.SH ENVIRONMENT
+All tools honor the TMPDIR environment variable when generating temporary
+files and directories.
+.SH BUGS
+If you encounter a problem please create an issue at
+.B https://github.com/diffblue/cbmc/issues
+.SH SEE ALSO
+.BR cbmc (1),
+.BR goto-cc (1)
+.BR goto-instrument (1)
+.SH COPYRIGHT
+2023, Diffblue Ltd.
diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
@@ -46,6 +46,7 @@ add_subdirectory(goto-instrument-chc)
 add_subdirectory(goto-instrument-json)
 add_subdirectory(goto-instrument-wmm-core)
 add_subdirectory(goto-instrument-typedef)
+add_subdirectory(goto-inspect)
 add_subdirectory(smt2_solver)
 add_subdirectory(smt2_strings)
 add_subdirectory(strings)
diff --git a/regression/goto-inspect/CMakeLists.txt b/regression/goto-inspect/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_test_pl_tests(
+  "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-inspect>"
+)
diff --git a/regression/goto-inspect/chain.sh b/regression/goto-inspect/chain.sh
@@ -0,0 +1,25 @@
+#!/bin/bash
+
+set -e
+
+# A test instruction passed to this `chain.sh` file looks like this:
+# 
+# build/bin/goto-cc build/bin/goto-inspect --show-goto-functions main.c
+#
+# This allows us to safely assume for now (as long as we're operating
+# goto-inspect with one binary and one inspection option, which seems
+# to be the case for now) that the option is going to be at $3.
+# If this is no longer the case in the future, this script will need
+# to be made significantly more sophisticated in terms of handling
+# a variable number of options for the goto-inspect binary.
+
+echo $@
+
+goto_cc_exe=$1
+goto_inspect_exe=$2
+
+name=${*:$#}
+name=${name%.c}
+
+$goto_cc_exe -o "${name}.gb" "${name}.c"
+$goto_inspect_exe $3 "${name}.gb" 
diff --git a/regression/goto-inspect/show-goto-functions/main.c b/regression/goto-inspect/show-goto-functions/main.c
@@ -0,0 +1,5 @@
+int main(int argc, char *argv[])
+{
+  int arr[] = {0, 1, 2, 3, 4};
+  __CPROVER_assert(arr[0] != 0, "Expected failure: 0 == 0");
+}
diff --git a/regression/goto-inspect/show-goto-functions/negative.desc b/regression/goto-inspect/show-goto-functions/negative.desc
@@ -0,0 +1,15 @@
+CORE
+main.c
+" "
+^EXIT=6$
+^SIGNAL=0$
+--
+DECL main::1::arr : signedbv\[32\]\[5\]
+ASSIGN main::1::arr := \{ 0, 1, 2, 3, 4 \}
+ASSERT main::1::arr\[cast\(0, signedbv\[64\]\)\] ≠ 0 // Expected failure: 0 == 0
+DEAD main::1::arr
+SET RETURN VALUE side_effect statement="nondet" is_nondet_nullable="1"
+END_FUNCTION
+--
+This is testing the behaviour of the goto-inspect binary in case a binary
+is present, but no inspection option is present.
diff --git a/regression/goto-inspect/show-goto-functions/positive.desc b/regression/goto-inspect/show-goto-functions/positive.desc
@@ -0,0 +1,14 @@
+CORE
+main.c
+--show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+main
+DECL main::1::arr : signedbv\[32\]\[5\]
+ASSIGN main::1::arr := \{ 0, 1, 2, 3, 4 \}
+ASSERT main::1::arr\[cast\(0, signedbv\[64\]\)\] ≠ 0 // Expected failure: 0 == 0
+DEAD main::1::arr
+SET RETURN VALUE side_effect statement="nondet" is_nondet_nullable="1"
+END_FUNCTION
+--
+--
diff --git a/src/CMakeLists.txt b/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)
diff --git a/src/Makefile b/src/Makefile
@@ -10,6 +10,7 @@ DIRS = analyses \
        goto-cc \
        goto-checker \
        goto-diff \
+       goto-inspect \
        goto-instrument \
        goto-harness \
        goto-programs \
@@ -36,6 +37,7 @@ all: cbmc.dir \
      goto-cc.dir \
      goto-diff.dir \
      goto-instrument.dir \
+     goto-inspect.dir \
      goto-harness.dir \
      goto-synthesizer.dir \
      symtab2gb.dir \
@@ -82,6 +84,8 @@ goto-harness.dir: util.dir goto-programs.dir langapi.dir linking.dir \
 goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
                      goto-symex.dir linking.dir analyses.dir solvers.dir
 
+goto-inspect.dir: util.dir goto-programs.dir languages linking.dir
+
 goto-checker.dir: solvers.dir goto-symex.dir goto-programs.dir
 
 cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \
@@ -190,8 +194,8 @@ doc :
 install: all
 	for b in \
 		cbmc crangler \
-		goto-analyzer goto-cc goto-diff goto-instrument goto-harness goto-synthesizer \
-		symtab2gb ; do \
+		goto-analyzer goto-cc goto-diff goto-instrument goto-inspect goto-harness \
+    goto-synthesizer symtab2gb ; do \
 		  cp $$b/$$b $(PREFIX)/bin/ ; \
 			cp ../doc/man/$$b.1 $(PREFIX)/doc/man/man1/ ; \
 	done
diff --git a/src/goto-inspect/CMakeLists.txt b/src/goto-inspect/CMakeLists.txt
@@ -0,0 +1,22 @@
+# For goto-inspect, we are not building a library - only a binary.
+
+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()
diff --git a/src/goto-inspect/Makefile b/src/goto-inspect/Makefile
@@ -0,0 +1,31 @@
+SRC = goto_inspect_main.cpp \
+      goto_inspect_parse_options.cpp \
+      # Empty last line
+
+OBJ += ../big-int/big-int$(LIBEXT) \
+       ../linking/linking$(LIBEXT) \
+       ../langapi/langapi$(LIBEXT) \
+       ../goto-programs/goto-programs$(LIBEXT) \
+       ../util/util$(LIBEXT) \
+       # Empty last line
+
+INCLUDES= -I ..
+
+LIBS =
+
+CLEANFILES = goto-inspect$(EXEEXT) goto-inspect$(LIBEXT)
+
+include ../config.inc
+include ../common
+
+all: goto-inspect$(EXEEXT)
+
+###############################################################################
+
+goto-inspect$(EXEEXT): $(OBJ)
+	$(LINKBIN)
+
+.PHONY: goto-inspect-mac-signed
+
+goto-inspect-mac-signed: goto-inspect$(EXEEXT)
+	codesign -v -s $(OSX_IDENTITY) goto-inspect$(EXEEXT)
diff --git a/src/goto-inspect/goto_inspect_main.cpp b/src/goto-inspect/goto_inspect_main.cpp
@@ -0,0 +1,20 @@
+// Author: Fotis Koutoulakis for Diffblue Ltd.
+
+#ifdef _MSC_VER
+#  include <util/unicode.h>
+#endif
+
+#include "goto_inspect_parse_options.h"
+
+#ifdef _MSC_VER
+int wmain(int argc, const wchar_t **argv_wide)
+{
+  auto vec = narrow_argv(argc, argv_wide);
+  auto narrow = to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv = narrow.data();
+#else
+int main(int argc, const char **argv)
+{
+#endif
+  return goto_inspect_parse_optionst{argc, argv}.main();
+}
diff --git a/src/goto-inspect/goto_inspect_parse_options.cpp b/src/goto-inspect/goto_inspect_parse_options.cpp
@@ -0,0 +1,100 @@
+// 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/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, ensure that a file argument has been given.
+  if(cmdline.args.size() != 1)
+  {
+    help();
+    throw invalid_command_line_argument_exceptiont{
+      "failed to supply a goto-binary name or an option for inspection",
+      "<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-inspect
+  // 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"))
+  {
+    show_goto_functions(
+      goto_model, ui_message_handler, cmdline.isset("list-goto-functions"));
+    return CPROVER_EXIT_SUCCESS;
+  }
+
+  // If an option + binary was provided, the program will have exited
+  // gracefully through a different branch. If we hit the code below, it
+  // means that something has gone wrong - it's also possible to fall through
+  // this case if no optional inspection flag is present in the argument
+  // vector. This will ensure that the return value in that case is
+  // semantically meaningful, and provide a return value that also satisfies
+  // the compiler's requirements based on the signature of `doit()`.
+  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("info@diffblue.com") << '\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}
+{
+}
diff --git a/src/goto-inspect/goto_inspect_parse_options.h b/src/goto-inspect/goto_inspect_parse_options.h
@@ -0,0 +1,24 @@
+// Author: Fotis Koutoulakis for Diffblue Ltd.
+
+#ifndef CPROVER_GOTO_INSPECT_GOTO_INSPECT_PARSE_OPTIONS_H
+#define CPROVER_GOTO_INSPECT_GOTO_INSPECT_PARSE_OPTIONS_H
+
+#include <util/parse_options.h>
+
+// 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_GOTO_INSPECT_PARSE_OPTIONS_H
diff --git a/src/goto-inspect/module_dependencies.txt b/src/goto-inspect/module_dependencies.txt
@@ -0,0 +1,2 @@
+goto-programs
+util
diff --git a/src/goto-inspect/readme.md b/src/goto-inspect/readme.md
@@ -0,0 +1,10 @@
+\ingroup module_hidden
+\defgroup goto-inspect goto-inspect
+
+# Folder goto-inspect
+
+\author Fotis Koutoulakis
+
+The `goto-inspect/` contains the code for the binary `goto-inspect`, intended
+to provide an all-purpose tool for inspection of goto-binaries (properties,
+goto-functions, etc).

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+add_test_pl_tests(`
	`2`	`+ "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-inspect>"`
	`3`	`+)`