Add function harness generator and generator factory

.gitignore

@@ -102,6 +102,8 @@ src/goto-cc/goto-cc
 src/goto-cc/goto-gcc
 src/goto-cc/goto-cc.exe
 src/goto-cc/goto-cl.exe
+src/goto-harness/goto-harness
+src/goto-harness/goto-harness.exe
 src/goto-instrument/goto-instrument
 src/goto-instrument/goto-instrument.exe
 src/solvers/smt2_solver

regression/goto-harness/CMakeLists.txt

@@ -1,2 +1,12 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
 add_test_pl_tests(
-  "$<TARGET_FILE:goto-harness>")
+  "../chain.sh \
+   $<TARGET_FILE:goto-cc> \
+   $<TARGET_FILE:goto-harness> \
+   $<TARGET_FILE:cbmc> \
+   ${is_windows}")

regression/goto-harness/Makefile

@@ -1,12 +1,24 @@
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
 GOTO_HARNESS_EXE=../../../src/goto-harness/goto-harness
+CBMC_EXE=../../../src/cbmc/cbmc
+
+ifeq ($(BUILD_ENV_),MSVC)
+	GOTO_CC_EXE=../../../src/goto-cc/goto-cl
+	is_windows=true
+else
+	GOTO_CC_EXE=../../../src/goto-cc/goto-cc
+	is_windows=false
+endif
 
 test:
-	@../test.pl -p -c ${GOTO_HARNESS_EXE}
+	@../test.pl -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
 
 tests.log: ../test.pl
-	@../test.pl -p -c ${GOTO_HARNESS_EXE}
+	@../test.pl -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(CBMC_EXE) $(is_windows)"
 
 show:
 	@for dir in *; do \

regression/goto-harness/chain.sh

@@ -0,0 +1,27 @@
+#!/bin/bash
+
+set -e
+
+goto_cc=$1
+goto_harness=$2
+cbmc=$3
+is_windows=$4
+entry_point='generated_entry_function'
+
+name=${*:$#}
+name=${name%.c}
+args=${*:5:$#-5}
+
+if [[ "${is_windows}" == "true" ]]; then
+  $goto_cc "${name}.c"
+  mv "${name}.exe" "${name}.gb"
+else
+  $goto_cc -o "${name}.gb" "${name}.c"
+fi
+
+if [ -e "${name}-mod.gb" ] ; then
+  rm -f "${name}-mod.gb"
+fi
+
+$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args} 
+$cbmc --function $entry_point "${name}-mod.gb"

regression/goto-harness/goto-harness-can-generate-trivial-harness/main.c

@@ -0,0 +1,7 @@
+#include <assert.h>
+
+int function_to_test(int some_argument)
+{
+  assert(some_argument == 0);
+  return some_argument;
+}

regression/goto-harness/goto-harness-can-generate-trivial-harness/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--harness-type call-function --function function_to_test
+^\[function_to_test.assertion.1\] line \d+ assertion some_argument == 0: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$

src/Makefile

@@ -49,7 +49,7 @@ languages: util.dir langapi.dir \
 
 solvers.dir: util.dir
 
-goto-harness.dir: util.dir
+goto-harness.dir: util.dir goto-programs.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

@@ -3,5 +3,6 @@ add_executable(goto-harness ${sources})
 generic_includes(goto-harness)
 
 target_link_libraries(goto-harness
-    util
+  util
+  goto-programs
 )

src/goto-harness/Makefile

@@ -1,10 +1,17 @@
 SRC = \
+  function_call_harness_generator.cpp \
+  goto_harness_generator.cpp \
+  goto_harness_generator_factory.cpp \
   goto_harness_main.cpp \
   goto_harness_parse_options.cpp \
   # Empty last line
 
 OBJ += \
   ../util/util$(LIBEXT) \
+  ../goto-programs/goto-programs$(LIBEXT) \
+  ../big-int/big-int$(LIBEXT) \
+  ../langapi/langapi$(LIBEXT) \
+  ../linking/linking$(LIBEXT) \
   # Empty last line
 
 INCLUDES= -I ..

src/goto-harness/function_call_harness_generator.cpp

@@ -0,0 +1,134 @@
+/******************************************************************\
+
+Module: harness generator for functions
+
+Author: Diffblue Ltd.
+
+\******************************************************************/
+
+#include "function_call_harness_generator.h"
+
+#include <goto-programs/goto_convert.h>
+#include <goto-programs/goto_model.h>
+#include <util/allocate_objects.h>
+#include <util/exception_utils.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
+#include <util/ui_message.h>
+
+#include "function_harness_generator_options.h"
+#include "goto_harness_parse_options.h"
+
+struct function_call_harness_generatort::implt
+{
+  ui_message_handlert *message_handler;
+  irep_idt function;
+};
+
+function_call_harness_generatort::function_call_harness_generatort(
+  ui_message_handlert &message_handler)
+  : goto_harness_generatort{}, p_impl(util_make_unique<implt>())
+{
+  p_impl->message_handler = &message_handler;
+}
+
+function_call_harness_generatort::~function_call_harness_generatort() = default;
+
+void function_call_harness_generatort::handle_option(
+  const std::string &option,
+  const std::list<std::string> &values)
+{
+  if(option == FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT)
+  {
+    p_impl->function = require_exactly_one_value(option, values);
+  }
+  else
+  {
+    throw invalid_command_line_argument_exceptiont{
+      "function harness generator cannot handle this option", "--" + option};
+  }
+}
+
+void function_call_harness_generatort::generate(
+  goto_modelt &goto_model,
+  const irep_idt &harness_function_name)
+{
+  auto const &function = p_impl->function;
+  auto &symbol_table = goto_model.symbol_table;
+  auto function_found = symbol_table.lookup(function);
+  auto harness_function_found = symbol_table.lookup(harness_function_name);
+
+  if(function_found == nullptr)
+  {
+    throw invalid_command_line_argument_exceptiont{
+      "function that should be harnessed is not found " + id2string(function),
+      "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT};
+  }
+
+  if(harness_function_found != nullptr)
+  {
+    throw invalid_command_line_argument_exceptiont{
+      "harness function already in the symbol table " +
+        id2string(harness_function_name),
+      "--" GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT};
+  }
+
+  auto allocate_objects = allocate_objectst{function_found->mode,
+                                            function_found->location,
+                                            "__goto_harness",
+                                            symbol_table};
+
+  // create body for the function
+  code_blockt function_body{};
+
+  const auto &function_type = to_code_type(function_found->type);
+  const auto &parameters = function_type.parameters();
+
+  code_function_callt::operandst arguments{};
+  arguments.reserve(parameters.size());
+
+  for(const auto &parameter : parameters)
+  {
+    auto argument = allocate_objects.allocate_automatic_local_object(
+      parameter.type(), parameter.get_base_name());
+    arguments.push_back(std::move(argument));
+  }
+
+  code_function_callt function_call{function_found->symbol_expr(),
+                                    std::move(arguments)};
+  function_call.add_source_location() = function_found->location;
+
+  function_body.add(std::move(function_call));
+
+  // create the function symbol
+  symbolt harness_function_symbol{};
+  harness_function_symbol.name = harness_function_symbol.base_name =
+    harness_function_symbol.pretty_name = harness_function_name;
+
+  harness_function_symbol.is_lvalue = true;
+  harness_function_symbol.mode = function_found->mode;
+  harness_function_symbol.type = code_typet{{}, empty_typet{}};
+  harness_function_symbol.value = function_body;
+
+  symbol_table.insert(harness_function_symbol);
+
+  goto_model.goto_functions.function_map[harness_function_name].type =
+    to_code_type(harness_function_symbol.type);
+  auto &body =
+    goto_model.goto_functions.function_map[harness_function_name].body;
+  goto_convert(
+    static_cast<const codet &>(harness_function_symbol.value),
+    goto_model.symbol_table,
+    body,
+    *p_impl->message_handler,
+    function_found->mode);
+  body.add(goto_programt::make_end_function());
+}
+
+void function_call_harness_generatort::validate_options()
+{
+  if(p_impl->function == ID_empty)
+    throw invalid_command_line_argument_exceptiont{
+      "required parameter entry function not set",
+      "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT};
+}

src/goto-harness/function_call_harness_generator.h

@@ -0,0 +1,43 @@
+/******************************************************************\
+
+Module: harness generator for functions
+
+Author: Diffblue Ltd.
+
+\******************************************************************/
+
+#ifndef CPROVER_GOTO_HARNESS_FUNCTION_CALL_HARNESS_GENERATOR_H
+#define CPROVER_GOTO_HARNESS_FUNCTION_CALL_HARNESS_GENERATOR_H
+
+#include <list>
+#include <memory>
+#include <string>
+
+#include <util/ui_message.h>
+
+#include "goto_harness_generator.h"
+
+/// Function harness generator that for a specified goto-function
+/// generates a harness that sets up its arguments and calls it.
+class function_call_harness_generatort : public goto_harness_generatort
+{
+public:
+  explicit function_call_harness_generatort(
+    ui_message_handlert &message_handler);
+  ~function_call_harness_generatort() override;
+  void generate(goto_modelt &goto_model, const irep_idt &harness_function_name)
+    override;
+
+protected:
+  void handle_option(
+    const std::string &option,
+    const std::list<std::string> &values) override;
+
+  void validate_options() override;
+
+private:
+  struct implt;
+  std::unique_ptr<implt> p_impl;
+};
+
+#endif // CPROVER_GOTO_HARNESS_FUNCTION_CALL_HARNESS_GENERATOR_H

src/goto-harness/function_harness_generator_options.h

@@ -0,0 +1,25 @@
+/******************************************************************\
+
+Module: functions_harness_generator_options
+
+Author: Diffblue Ltd.
+
+\******************************************************************/
+
+#ifndef CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H
+#define CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H
+
+#define FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "function"
+#define FUNCTION_HARNESS_GENERATOR_OPTIONS                                     \
+  "(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):"
+// FUNCTION_HARNESS_GENERATOR_OPTIONS
+
+// clang-format off
+#define FUNCTION_HARNESS_GENERATOR_HELP                                        \
+  "function harness generator (--harness-type call-function)\n\n"              \
+  "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT                                 \
+  "      the function the harness should call\n"                               \
+  // FUNCTION_HARNESS_GENERATOR_HELP
+// clang-format on
+
+#endif // CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H

src/goto-harness/goto_harness_generator.cpp

@@ -0,0 +1,35 @@
+/******************************************************************\
+
+Module: goto_harness_generator
+
+Author: Diffblue Ltd.
+
+\******************************************************************/
+
+#include "goto_harness_generator.h"
+
+#include <list>
+#include <string>
+
+#include <util/exception_utils.h>
+#include <util/invariant.h>
+
+std::string goto_harness_generatort::require_exactly_one_value(
+  const std::string &option,
+  const std::list<std::string> &values)
+{
+  if(values.size() != 1)
+  {
+    throw invalid_command_line_argument_exceptiont{"expected exactly one value",
+                                                   "--" + option};
+  }
+
+  return values.front();
+}
+
+void goto_harness_generatort::assert_no_values(
+  const std::string &option,
+  const std::list<std::string> &values)
+{
+  PRECONDITION_WITH_DIAGNOSTICS(values.empty(), option);
+}