Add stub for new goto-harness tool

This adds a new executable called goto-harness. Right now it doesn't actually do
anything, but ultimately its purpose will be to generate "harness" functions for
goto-programs - i.e. given some specification, it'll generate a function
suitable as a cbmc entry point function that implements that specification.

Planned for now are two types of harnesses: One that takes the name of a
function with parameters and then generates a function that sets up these
parameters and calls the function with them. This is similar to what cbmc does
already, however will allow more flexibility in choosing how exactly these
parameters will be initialised which was deemed out of scope for cbmc. The other
will be able to take a snapshot of a concrete execution of a program, and then
start an analysis from that point.

Author: hannes-steffenhagen-diffblue

CMakeLists.txt

@@ -99,6 +99,7 @@ set_target_properties(
     goto-checker
     goto-diff
     goto-diff-lib
+    goto-harness
     goto-instrument
     goto-instrument-lib
     goto-programs

src/CMakeLists.txt

@@ -103,3 +103,4 @@ add_subdirectory(goto-cc)
 add_subdirectory(goto-instrument)
 add_subdirectory(goto-analyzer)
 add_subdirectory(goto-diff)
+add_subdirectory(goto-harness)

src/Makefile

@@ -8,6 +8,7 @@ DIRS = analyses \
        goto-cc \
        goto-checker \
        goto-diff \
+       goto-harness \
        goto-instrument \
        goto-programs \
        goto-symex \
@@ -27,6 +28,7 @@ all: cbmc.dir \
      goto-cc.dir \
      goto-diff.dir \
      goto-instrument.dir \
+     goto-harness.dir \
      # Empty last line
 
 ###############################################################################
@@ -47,6 +49,8 @@ languages: util.dir langapi.dir \
 
 solvers.dir: util.dir
 
+goto-harness.dir: util.dir
+
 goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
                      goto-symex.dir linking.dir analyses.dir solvers.dir
 

src/goto-harness/CMakeLists.txt

@@ -0,0 +1,7 @@
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_executable(goto-harness ${sources})
+generic_includes(goto-harness)
+
+target_link_libraries(goto-harness
+    util
+)

src/goto-harness/Makefile

@@ -0,0 +1,29 @@
+SRC = \
+  goto_harness_main.cpp \
+  goto_harness_parse_options.cpp \
+  # Empty last line
+
+OBJ += \
+  ../util/util$(LIBEXT) \
+  # Empty last line
+
+INCLUDES= -I ..
+
+LIBS =
+
+CLEANFILES = goto-harness$(EXEEXT)
+
+include ../config.inc
+include ../common
+
+all: goto-harness$(EXEEXT)
+
+###############################################################################
+
+goto-harness$(EXEEXT): $(OBJ)
+	$(LINKBIN)
+
+.PHONY: goto-harness-mac-signed
+
+goto-harness-mac-signed: goto-harness$(EXEEXT)
+	codesign -v -s $(OSX_IDENTITY) goto-harness$(EXEEXT)

src/goto-harness/goto_harness_main.cpp

@@ -0,0 +1,15 @@
+/******************************************************************\
+
+Module: goto_harness_main
+
+Author: Diffblue Ltd.
+
+\******************************************************************/
+
+#include "goto_harness_parse_options.h"
+
+int main(int argc, const char *argv[])
+{
+  auto parse_options = goto_harness_parse_optionst(argc, argv);
+  return parse_options.main();
+}

src/goto-harness/goto_harness_parse_options.cpp

@@ -0,0 +1,51 @@
+/******************************************************************\
+
+Module: goto_harness_parse_options
+
+Author: Diffblue Ltd.
+
+\******************************************************************/
+
+#include <cstddef>
+#include <iostream>
+#include <string>
+
+#include <util/exit_codes.h>
+#include <util/version.h>
+
+#include "goto_harness_parse_options.h"
+
+int goto_harness_parse_optionst::doit()
+{
+  if(cmdline.isset("version"))
+  {
+    std::cout << CBMC_VERSION << '\n';
+    return CPROVER_EXIT_SUCCESS;
+  }
+
+  help();
+  return CPROVER_EXIT_USAGE_ERROR;
+}
+
+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("[email protected]")
+            // ^--- No idea if this is the right email address
+            << '\n'
+            << '\n'
+            << "Usage:                       Purpose:\n"
+            << '\n'
+            << " goto-harness [-?] [-h] [--help]  show help\n"
+            << " goto-harness --version           show version\n";
+}
+
+goto_harness_parse_optionst::goto_harness_parse_optionst(
+  int argc,
+  const char *argv[])
+  : parse_options_baset{GOTO_HARNESS_OPTIONS, argc, argv}
+{
+}

src/goto-harness/goto_harness_parse_options.h

@@ -0,0 +1,25 @@
+/******************************************************************\
+
+Module: goto_harness_parse_options
+
+Author: Diffblue Ltd.
+
+\******************************************************************/
+
+#ifndef CPROVER_GOTO_HARNESS_GOTO_HARNESS_PARSE_OPTIONS_H
+#define CPROVER_GOTO_HARNESS_GOTO_HARNESS_PARSE_OPTIONS_H
+
+#include <util/parse_options.h>
+
+#define GOTO_HARNESS_OPTIONS "(version)" // end GOTO_HARNESS_OPTIONS
+
+class goto_harness_parse_optionst : public parse_options_baset
+{
+public:
+  int doit() override;
+  void help() override;
+
+  goto_harness_parse_optionst(int argc, const char *argv[]);
+};
+
+#endif // CPROVER_GOTO_HARNESS_GOTO_HARNESS_PARSE_OPTIONS_H

src/goto-harness/module_dependencies.txt

@@ -0,0 +1,2 @@
+util
+goto-harness