Merge pull request #5821 from tautschnig/goto-harness-output

tautschnig · web-flow · commit 3cd40542b02e · 2021-04-01T21:09:34.000+02:00
goto-harness: create goto binary or C output
diff --git a/doc/architectural/goto-harness.md b/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.
diff --git a/regression/goto-harness/chain.sh b/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
diff --git a/regression/goto-harness/havoc-global-int-02/test.desc b/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.
diff --git a/regression/goto-harness/havoc-global-int-03/test.desc b/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.
diff --git a/regression/goto-harness/havoc-global-struct/test.desc b/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$
diff --git a/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc b/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
diff --git a/regression/goto-harness/load-snapshot-static-global-array-01/test.desc b/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
diff --git a/regression/goto-harness/load-snapshot-static-global-int-01/test.desc b/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.
diff --git a/regression/goto-harness/load-snapshot-static-global-int-02/test.desc b/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.
diff --git a/regression/goto-harness/load-snapshot-static-global-int-03/test.desc b/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.
diff --git a/regression/goto-harness/load-snapshot-static-global-int-04/test.desc b/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.
diff --git a/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc b/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
diff --git a/src/goto-harness/goto_harness_parse_options.cpp b/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"))
+  {
+    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);
+  }
+  else
+  {
+    write_goto_binary(
+      got_harness_config.out_file, goto_model, log.get_message_handler());
+  }
 
   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];
