goto-harness: create goto binary or C output

It is not always necessary or desirable to produce C output. An ability
to produce goto binaries also avoids possible limitations of C and/or
dump-c (such as goto-harness creating initialisers for structs with bit
fields, which yield functions that take bit fields as parameters, which
isn't possible in C).

While at it, also clean up the help output to fix confusing language
about goto binaries when the output was actually C code.

Fixes: diffblue#5351

Author: tautschnig

doc/architectural/goto-harness.md

@@ -20,7 +20,7 @@ $ goto-cc program.c -o program.gb
 # Run goto-harness to produce harness file
 $ goto-harness --harness-type call-function --harness-function-name generated_harness_test_function --function test_function program.gb harness.c
 # Run the checks targetting the generated harness
-$ cbmc --pointer-check harness.c --function generated_harness_test_function
+$ cbmc --pointer-check harness.c program.c --function generated_harness_test_function
 ```
 
 ## Detailed Usage
@@ -32,11 +32,9 @@ without having any information about the program state.
 * The `memory-snapshot` harness, which loads an existing program state (in form
 of a JSON file) and selectively _havoc-ing_ some variables.
 
-**NOTE**: Due to a [bug](https://github.com/diffblue/cbmc/issues/5351), the
-`memory-snapshot` harness is currently inoperable. We are working to fix this.
-
-It is used similarly to how `goto-instrument` is used by modifying an existing
-GOTO binary, as produced by `goto-cc`.
+The harness generator can either produce the harness (i.e., the function
+environment) as C code, or a full GOTO binary. C code is generated when the
+output file name ends in ".c".
 
 ### The function call harness generator
 
@@ -364,12 +362,6 @@ VERIFICATION SUCCESSFUL
 
 ## The memory snapshot harness
 
-***NOTE:*** The memory snapshot harness is temporarily inoperable because of
-a bug that occured when we changed the implementation of `goto-harness` to
-produce C files instead of `goto` binaries. The bug is being tracked
-[here](https://github.com/diffblue/cbmc/issues/5351). We are sorry for the
-inconvenience, and hope to get it back to working properly soon.
-
 The `function-call` harness is used in situations in which we want to analyze a
 function in an arbitrary environment. If we want to analyze a function starting
 from a _real_ program state, we can use the `memory-snapshot` harness instead.

regression/goto-harness/chain.sh

@@ -8,13 +8,20 @@ cbmc=$3
 is_windows=$4
 entry_point='generated_entry_function'
 
+shift 4
 name=${*:$#}
 name=${name%.c}
-args=${*:5:$#-5}
 
 input_c_file="${name}.c"
 input_goto_binary="${name}.gb"
-harness_c_file="${name}-harness.c"
+if [[ "$1" == "harness.gb" ]]; then
+  harness_file=$1
+  shift
+else
+  harness_file="${name}-harness.c"
+fi
+
+args=${*:1:$#-1}
 
 
 
@@ -25,16 +32,24 @@ else
   $goto_cc -o "$input_goto_binary" "$input_c_file"
 fi
 
-if [ -e "$harness_c_file" ] ; then
-  rm -f "$harness_c_file"
+if [ -e "$harness_file" ] ; then
+  rm -f "$harness_file"
 fi
 
 # `# some comment` is an inline comment - basically, cause bash to execute an empty command
 $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" \
+$goto_harness "$input_goto_binary" "$harness_file" --harness-function-name $entry_point ${args}
+$cbmc --show-goto-functions "$harness_file"
+if [[ "${harness_file}" == "harness.gb" ]];then
+  $cbmc --function $entry_point "$harness_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` \
+    # cbmc args end
+else
+$cbmc --function $entry_point "$input_c_file" "$harness_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` \
   # cbmc args end
+fi

regression/goto-harness/havoc-global-int-02/test.desc

@@ -1,11 +1,9 @@
-KNOWNBUG
+CORE
 main.c
---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:7 --havoc-variables y
+harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:7 --havoc-variables y
 ^\[main.assertion.1\] line \d+ assertion y \+ 2 > y: FAILURE$
 ^\[main.assertion.2\] line \d+ assertion 0: FAILURE$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
---
-More information can be found in github#5351.

regression/goto-harness/havoc-global-int-03/test.desc

@@ -1,12 +1,10 @@
-KNOWNBUG
+CORE
 main.c
---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-source-location main.c:6 --havoc-variables x
+harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-source-location main.c:6 --havoc-variables x
 ^EXIT=10$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS
 \[main.assertion.2\] line [0-9]+ assertion x == 2: FAILURE
 \[main.assertion.3\] line [0-9]+ assertion x == 3: FAILURE
 --
 ^warning: ignoring
---
-More information can be found in github#5351.

regression/goto-harness/havoc-global-struct/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-goto-location main:3 --havoc-variables simple
+harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-goto-location main:3 --havoc-variables simple
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] line \d+ assertion simple.j > simple.i: FAILURE$

regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1
+harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

regression/goto-harness/load-snapshot-static-global-array-01/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0
+harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

regression/goto-harness/load-snapshot-static-global-int-01/test.desc

@@ -1,10 +1,8 @@
-KNOWNBUG
+CORE
 main.c
---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0
+harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
---
-More information can be found in github#5351.

regression/goto-harness/load-snapshot-static-global-int-02/test.desc

@@ -1,11 +1,9 @@
-KNOWNBUG
+CORE
 main.c
---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0
+harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0
 ^EXIT=10$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS
 \[main.assertion.2\] line [0-9]+ assertion y == 1: FAILURE
 --
 ^warning: ignoring
---
-More information can be found in github#5351.

regression/goto-harness/load-snapshot-static-global-int-03/test.desc

@@ -1,10 +1,8 @@
-KNOWNBUG
+CORE
 main.c
---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0
+harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
---
-More information can be found in github#5351.

regression/goto-harness/load-snapshot-static-global-int-04/test.desc

@@ -1,10 +1,8 @@
-KNOWNBUG
+CORE
 main.c
---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1
+harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring
---
-More information can be found in github#5351.

regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0
+harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

src/goto-harness/goto_harness_parse_options.cpp

@@ -15,20 +15,21 @@ Author: Diffblue Ltd.
 #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/suffix.h>
 #include <util/version.h>
 
+#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 "function_call_harness_generator.h"
 #include "goto_harness_generator_factory.h"
 #include "memory_snapshot_harness_generator.h"
@@ -145,15 +146,23 @@ int goto_harness_parse_optionst::doit()
   harness_generator->generate(
     goto_model, got_harness_config.harness_function_name);
 
-  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);
+  if(!has_suffix(got_harness_config.out_file, ".c"))
+  {
+    write_goto_binary(
+      got_harness_config.out_file, goto_model, log.get_message_handler());
+  }
+  else
+  {
+    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;
 }
@@ -174,8 +183,12 @@ void goto_harness_parse_optionst::help()
     << " goto-harness <in> <out> --harness-function-name <name> --harness-type "
        "<harness-type> [harness options]\n"
     << "\n"
-    << "<in>                       goto binaries to read from\n"
-    << "<out>                      C file to write the harness to\n"
+    << "<in>                       goto binary to read from\n"
+    << "<out>                      file to write the harness to\n"
+    << "                           the harness is printed as C code, if <out> "
+       "has a .c suffix,\n"
+       "                           else a goto binary including the harness is "
+       "generated\n"
     << "--harness-function-name    the name of the harness function to "
        "generate\n"
     << "--harness-type             one of the harness types listed below\n"
@@ -205,9 +218,9 @@ goto_harness_parse_optionst::handle_common_options()
   {
     help();
     throw invalid_command_line_argument_exceptiont{
-      "need to specify both input and output goto binary file names (may be "
+      "need to specify both input and output file names (may be "
       "the same)",
-      "<in goto binary> <out goto binary>"};
+      "<in goto binary> <output C file or goto binary>"};
   }
 
   goto_harness_config.in_file = cmdline.args[0];