Merge pull request #3875 from hannes-steffenhagen-diffblue/feature-goto_harness_stub

Add stub for new goto-harness tool [depends-on: #3920]

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

regression/CMakeLists.txt

@@ -47,3 +47,4 @@ add_subdirectory(cbmc-cpp)
 add_subdirectory(goto-cc-goto-analyzer)
 add_subdirectory(systemc)
 add_subdirectory(contracts)
+add_subdirectory(goto-harness)

regression/Makefile

@@ -16,6 +16,7 @@ DIRS = cbmc \
        test-script \
        goto-analyzer-taint \
        goto-gcc \
+       goto-harness \
        goto-cl \
        goto-cc-cbmc \
        cbmc-cpp \

regression/goto-harness/CMakeLists.txt

@@ -0,0 +1,2 @@
+add_test_pl_tests(
+  "$<TARGET_FILE:goto-harness>")

regression/goto-harness/Makefile

@@ -0,0 +1,21 @@
+default: tests.log
+
+GOTO_HARNESS_EXE=../../../src/goto-harness/goto-harness
+
+test:
+	@../test.pl -p -c ${GOTO_HARNESS_EXE}
+
+tests.log: ../test.pl
+	@../test.pl -p -c ${GOTO_HARNESS_EXE}
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) {} \;
+	$(RM) tests.log

regression/goto-harness/goto-harness-exists/test.desc

@@ -0,0 +1,6 @@
+CORE
+dummy
+--version
+^\d+\.\d+ \([^)]+\)
+^EXIT=0$
+^SIGNAL=0$

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