Output C code instead of goto-binary from goto-harness.

Modify goto-harness to output C code that corresponds
to the added harness functions and some global values.
This has been a feature request.

Author: NlightNFotis

regression/goto-harness/chain.sh

@@ -12,22 +12,28 @@ name=${*:$#}
 name=${name%.c}
 args=${*:5:$#-5}
 
+input_c_file="${name}.c"
+input_goto_binary="${name}.gb"
+harness_c_file="${name}-harness.c"
+
+
+
 if [[ "${is_windows}" == "true" ]]; then
-  $goto_cc "${name}.c"
-  mv "${name}.exe" "${name}.gb"
+  $goto_cc "$input_c_file"
+  mv "${name}.exe" "$input_goto_binary"
 else
-  $goto_cc -o "${name}.gb" "${name}.c"
+  $goto_cc -o "$input_goto_binary" "$input_c_file"
 fi
 
-if [ -e "${name}-mod.gb" ] ; then
-  rm -f "${name}-mod.gb"
+if [ -e "$harness_c_file" ] ; then
+  rm -f "$harness_c_file"
 fi
 
 # `# some comment` is an inline comment - basically, cause bash to execute an empty command
-$cbmc --show-goto-functions "${name}.gb"
-$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args}
-$cbmc --show-goto-functions "${name}-mod.gb"
-$cbmc --function $entry_point "${name}-mod.gb" \
+$cbmc --show-goto-functions "$input_goto_binary"
+$goto_harness "$input_goto_binary" "$harness_c_file" --harness-function-name $entry_point ${args}
+$cbmc --show-goto-functions "$harness_c_file"
+$cbmc --function $entry_point "$input_c_file" "$harness_c_file" \
   --pointer-check `# because we want to see out of bounds errors` \
   --unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \
   --unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \

src/Makefile

@@ -8,8 +8,8 @@ DIRS = analyses \
        goto-cc \
        goto-checker \
        goto-diff \
-       goto-harness \
        goto-instrument \
+       goto-harness \
        goto-programs \
        goto-symex \
        jsil \
@@ -66,7 +66,8 @@ languages: util.dir langapi.dir \
 solvers.dir: util.dir
 
 goto-harness.dir: util.dir goto-programs.dir langapi.dir linking.dir \
-                  json.dir json-symtab-language.dir
+                  json.dir json-symtab-language.dir \
+                  goto-instrument.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

@@ -5,6 +5,7 @@ generic_includes(goto-harness)
 target_link_libraries(goto-harness
   util
   goto-programs
+  goto-instrument-lib
   json
   json-symtab-language
 )

src/goto-harness/Makefile

@@ -16,6 +16,10 @@ OBJ += \
   ../linking/linking$(LIBEXT) \
   ../json/json$(LIBEXT) \
   ../json-symtab-language/json-symtab-language$(LIBEXT) \
+  ../ansi-c/ansi-c$(LIBEXT) \
+  ../cpp/cpp$(LIBEXT) \
+  ../goto-instrument/dump_c$(OBJEXT) \
+  ../goto-instrument/goto_program2code$(OBJEXT) \
   # Empty last line
 
 INCLUDES= -I ..

src/goto-harness/goto_harness_parse_options.cpp

@@ -9,24 +9,57 @@ Author: Diffblue Ltd.
 #include "goto_harness_parse_options.h"
 
 #include <cstddef>
+#include <fstream>
 #include <set>
 #include <string>
+#include <unordered_set>
 #include <utility>
 
+#include <goto-instrument/dump_c.h>
 #include <goto-programs/goto_convert.h>
 #include <goto-programs/goto_model.h>
 #include <goto-programs/read_goto_binary.h>
+#include <goto-programs/show_symbol_table.h>
 #include <goto-programs/write_goto_binary.h>
+#include <langapi/mode.h>
 #include <util/config.h>
 #include <util/exception_utils.h>
 #include <util/exit_codes.h>
+#include <util/expr_iterator.h>
 #include <util/invariant.h>
 #include <util/version.h>
 
 #include "function_call_harness_generator.h"
 #include "goto_harness_generator_factory.h"
 #include "memory_snapshot_harness_generator.h"
 
+std::unordered_set<irep_idt>
+get_symbol_names_from_goto_model(const goto_modelt &goto_model)
+{
+  auto symbols = std::unordered_set<irep_idt>{};
+  std::transform(
+    goto_model.get_symbol_table().begin(),
+    goto_model.get_symbol_table().end(),
+    std::inserter(symbols, symbols.end()),
+    [](const std::pair<const irep_idt, symbolt> &key_value_pair) {
+      return key_value_pair.first;
+    });
+  return symbols;
+}
+
+static void filter_goto_model(
+  goto_modelt &goto_model_with_harness,
+  const std::unordered_set<irep_idt> &goto_model_without_harness_symbols)
+{
+  for(auto &symbol : goto_model_with_harness.get_symbol_table())
+  {
+    if(
+      goto_model_without_harness_symbols.count(symbol.first) == 1 &&
+      symbol.second.is_function())
+      goto_model_with_harness.unload(symbol.first);
+  }
+}
+
 // The basic idea is that this module is handling the following
 // sequence of events:
 // 1. Initialise a goto-model by parsing an input (goto) binary
@@ -62,6 +95,8 @@ int goto_harness_parse_optionst::doit()
                                      got_harness_config.in_file + "'"};
   }
   auto goto_model = std::move(read_goto_binary_result.value());
+  auto const goto_model_without_harness_symbols =
+    get_symbol_names_from_goto_model(goto_model);
 
   // This has to be called after the defaults are set up (as per the
   // config.set(cmdline) above) otherwise, e.g. the architecture specification
@@ -87,13 +122,15 @@ int goto_harness_parse_optionst::doit()
   harness_generator->generate(
     goto_model, got_harness_config.harness_function_name);
 
-  // Write end result to new goto-binary
-  if(write_goto_binary(
-       got_harness_config.out_file, goto_model, ui_message_handler))
-  {
-    throw system_exceptiont{"failed to write goto program from file '" +
-                            got_harness_config.out_file + "'"};
-  }
+  filter_goto_model(goto_model, goto_model_without_harness_symbols);
+  auto harness_out = std::ofstream{got_harness_config.out_file};
+  dump_c(
+    goto_model.goto_functions,
+    true,
+    true,
+    false,
+    namespacet{goto_model.get_symbol_table()},
+    harness_out);
 
   return CPROVER_EXIT_SUCCESS;
 }

src/goto-harness/module_dependencies.txt

@@ -1,6 +1,9 @@
+ansi-c
 util
 goto-harness
+goto-instrument
 goto-programs
 json
 json-symtab-language
+langapi
 linking