Merge pull request #7762 from NlightNFotis/esteffin/verifier-only-entry-point

Enrico Steffinlongo · web-flow · commit 79d8a9cbcb0b · 2023-07-06T10:51:01.000+01:00
Add `goto-bmc`, a new tool to run only the verifier
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -228,6 +228,7 @@ cprover_default_properties(
     driver
     goto-analyzer
     goto-analyzer-lib
+    goto-bmc
     goto-cc
     goto-cc-lib
     goto-checker
diff --git a/CODEOWNERS b/CODEOWNERS
@@ -50,6 +50,7 @@
 # These files change frequently and changes are medium-risk
 
 /src/goto-analyzer/ @martin-cs @peterschrammel
+/src/goto-bmc/ @NlightNFotis @thomasspriggs @esteffin @TGWDB @peterschrammel
 /src/goto-harness/ @martin-cs @peterschrammel
 /src/goto-instrument/ @martin-cs @peterschrammel @tautschnig @kroening
 /src/goto-instrument/contracts/ @tautschnig @feliperodri @remi-delmas-3000
diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
@@ -54,6 +54,9 @@ add_subdirectory(invariants)
 add_subdirectory(goto-diff)
 add_subdirectory(test-script)
 add_subdirectory(goto-analyzer-taint)
+add_subdirectory(goto-bmc/goto-bmc-symex-ready-goto)
+add_subdirectory(goto-bmc/goto-bmc-non-symex-ready-goto)
+add_subdirectory(goto-bmc)
 if(NOT WIN32)
   add_subdirectory(goto-gcc)
 else()
diff --git a/regression/goto-bmc/CMakeLists.txt b/regression/goto-bmc/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_test_pl_tests(
+        "$<TARGET_FILE:goto-bmc>"
+)
diff --git a/regression/goto-bmc/arguments/help.desc b/regression/goto-bmc/arguments/help.desc
@@ -0,0 +1,13 @@
+CORE
+
+--help
+^EXIT=0$
+^SIGNAL=0$
+goto-bmc \d\.\d+\.\d+
+Usage\:
+Purpose\:
+show help
+show version and exit
+--
+--
+Test that help is output when help argument is specified.
diff --git a/regression/goto-bmc/arguments/missing-input.desc b/regression/goto-bmc/arguments/missing-input.desc
@@ -0,0 +1,10 @@
+CORE
+
+
+^EXIT=6$
+^SIGNAL=0$
+Please give exactly one binary file
+--
+--
+Test that an appropriate error message is produced when no input goto binary is
+specified.
diff --git a/regression/goto-bmc/arguments/version.desc b/regression/goto-bmc/arguments/version.desc
@@ -0,0 +1,9 @@
+CORE
+
+--version
+^EXIT=0$
+^SIGNAL=0$
+^\d\.\d+\.\d+
+--
+--
+Test that version is output when version argument is specified.
diff --git a/regression/goto-bmc/goto-bmc-non-symex-ready-goto/CMakeLists.txt b/regression/goto-bmc/goto-bmc-non-symex-ready-goto/CMakeLists.txt
@@ -0,0 +1,15 @@
+if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+# Second suite of tests is running `goto-cc` to produce "normal" goto-binaries,
+# which we expect `goto-bmc` to reject in some capacity. For now, it just fails
+# non-gracefully, with invariant violations. This behaviour is important enough
+# that we want to test for it, but we expect the software to become better behaved
+# in the future (by checking that the input binary *is* in symex-ready-goto form
+# and if not produce appropriate error reporting for the user).
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-bmc> ${is_windows}"
+)
diff --git a/regression/goto-bmc/goto-bmc-non-symex-ready-goto/chain.sh b/regression/goto-bmc/goto-bmc-non-symex-ready-goto/chain.sh
@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+
+set -e
+
+goto_cc=$1
+goto_bmc=$2
+is_windows=$3
+
+options=${*:4:$#-4}
+name=${*:$#}
+base_name=${name%.c}
+base_name=${base_name%.cpp}
+
+if [[ "${is_windows}" == "true" ]]; then
+  "${goto_cc}" "${name}" "/Fe${base_name}.gb"
+else
+  "${goto_cc}" "${name}" -o "${base_name}.gb"
+fi
+
+"${goto_bmc}" "${base_name}.gb" ${options}
diff --git a/regression/goto-bmc/goto-bmc-non-symex-ready-goto/negative1/main.c b/regression/goto-bmc/goto-bmc-non-symex-ready-goto/negative1/main.c
@@ -0,0 +1,6 @@
+int main(int argc, char *argv[])
+{
+  int a[] = {0, 1, 2, 3, 4};
+  __CPROVER_assert(a[0] != 0, "expected fail: 0 == 0");
+  return 0;
+}
diff --git a/regression/goto-bmc/goto-bmc-non-symex-ready-goto/negative1/main.desc b/regression/goto-bmc/goto-bmc-non-symex-ready-goto/negative1/main.desc
@@ -0,0 +1,18 @@
+CORE
+main.c
+
+^EXIT=(127|134)$
+^SIGNAL=0$
+^Invariant check failed$
+^Reason: Check return value$
+--
+^warning: ignoring
+--
+This is the same file as in positive1/ but we want to make sure
+that we fail in some way, signalling that we don't support non
+symex-ready goto binaries as input.
+
+We expect the semantics of the test to remain the same as the
+program evolves, but some of the regexes above may fail as the
+program is enhanced with better capacity to detect non symex-ready
+goto binaries and report to the user appropriately.
diff --git a/regression/goto-bmc/goto-bmc-symex-ready-goto/CMakeLists.txt b/regression/goto-bmc/goto-bmc-symex-ready-goto/CMakeLists.txt
@@ -0,0 +1,11 @@
+# `goto-bmc` is supposed to operate only on symex-ready goto binary files, so
+# we follow two different paths to make sure that it's behaviour is correct:
+
+# First suite of tests is supposed to be tests against symex-ready goto. For these,
+# goto-bmc is capable of handling those, and so we produce them using
+# `cbmc --export-symex-ready-goto <file>`.
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:cbmc> $<TARGET_FILE:goto-bmc>"
+)
+
+# Second suite of tests is in folder `regression/goto-bmc-non-symex-ready-goto/`
diff --git a/regression/goto-bmc/goto-bmc-symex-ready-goto/chain.sh b/regression/goto-bmc/goto-bmc-symex-ready-goto/chain.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+set -e
+
+cbmc=$1
+goto_bmc=$2
+
+options=${*:3:$#-3}
+name=${*:$#}
+base_name=${name%.c}
+
+"${cbmc}" --export-symex-ready-goto "${base_name}.goto.symex_ready" "${name}"
+"${goto_bmc}" "${base_name}.goto.symex_ready" ${options}
diff --git a/regression/goto-bmc/goto-bmc-symex-ready-goto/positive1/main.c b/regression/goto-bmc/goto-bmc-symex-ready-goto/positive1/main.c
@@ -0,0 +1,6 @@
+int main(int argc, char *argv[])
+{
+  int a[] = {0, 1, 2, 3, 4};
+  __CPROVER_assert(a[0] != 0, "expected fail: 0 == 0");
+  return 0;
+}
diff --git a/regression/goto-bmc/goto-bmc-symex-ready-goto/positive1/main.desc b/regression/goto-bmc/goto-bmc-symex-ready-goto/positive1/main.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+\[main\.assertion\.1\] line \d expected fail: 0 == 0: FAILURE
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
diff --git a/regression/goto-bmc/goto-bmc-symex-ready-goto/positive1/two_inputs.desc b/regression/goto-bmc/goto-bmc-symex-ready-goto/positive1/two_inputs.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+main.goto.symex_ready
+^EXIT=6$
+^SIGNAL=0$
+Please give exactly one binary file
+--
+--
+Test that an appropriate error message is produced when too many input goto
+binaries are specified. A copy of the `main.goto.symex_ready` argument will
+be generated by the `chain.sh` script from the specified `main.c`. This yields
+2 copies of this argument including the one in this file.
diff --git a/regression/goto-bmc/invalid-files/not-goto-no-header.desc b/regression/goto-bmc/invalid-files/not-goto-no-header.desc
@@ -0,0 +1,12 @@
+CORE
+not-goto-no-header.goto
+
+^EXIT=6$
+^SIGNAL=0$
+Please give exactly one binary file
+--
+not a goto binary
+Unable to read goto-binary from file not-goto-no-header\.goto
+--
+This test confirms that an appropriate error message is displayed in the case
+where a single input file is specified which does not pass the header check.
diff --git a/regression/goto-bmc/invalid-files/not-goto-no-header.goto b/regression/goto-bmc/invalid-files/not-goto-no-header.goto
@@ -0,0 +1,2 @@
+This is not a goto binary. A header would be required to pass the
+`is_goto_binary` check.
diff --git a/regression/goto-bmc/invalid-files/not-goto-with-header.desc b/regression/goto-bmc/invalid-files/not-goto-with-header.desc
@@ -0,0 +1,16 @@
+CORE
+not-goto-with-header.goto
+
+^EXIT=2$
+^SIGNAL=0$
+Unable to read goto-binary from file not-goto-with-header\.goto
+--
+Please give exactly one binary file
+not a goto binary
+--
+This test confirms that an appropriate error message is displayed in the case
+where an input file is specified which passed the header check used to
+determine if the file is a goto binary or not, but which is not followed by
+data of a valid goto binary file. Note that the `is_goto_binary` check works
+based on checking if the first four bytes of the file are the byte 7F followed
+by the characters "GBF".
diff --git a/regression/goto-bmc/invalid-files/not-goto-with-header.goto b/regression/goto-bmc/invalid-files/not-goto-with-header.goto
@@ -0,0 +1,3 @@
+GBF
+This is not a valid goto binary. It does have a header which should pass the
+`is_goto_binary` check though.
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -120,6 +120,7 @@ add_subdirectory(goto-harness)
 add_subdirectory(goto-synthesizer)
 add_subdirectory(symtab2gb)
 add_subdirectory(libcprover-cpp)
+add_subdirectory(goto-bmc)
 
 if(UNIX OR WITH_MEMORY_ANALYZER)
 add_subdirectory(memory-analyzer)
diff --git a/src/goto-bmc/CMakeLists.txt b/src/goto-bmc/CMakeLists.txt
@@ -0,0 +1,6 @@
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_executable(goto-bmc ${sources})
+
+generic_includes(goto-bmc)
+
+target_link_libraries(goto-bmc cprover-api-cpp)
diff --git a/src/goto-bmc/goto_bmc_main.cpp b/src/goto-bmc/goto_bmc_main.cpp
@@ -0,0 +1,11 @@
+// Author: Enrico Steffinlongo for Diffblue Ltd.
+
+#include "goto_bmc_parse_options.h"
+
+#include <iostream>
+#include <vector>
+
+int main(int argc, const char **argv)
+{
+  return goto_bmc_parse_optionst{argc, argv}.main();
+}
diff --git a/src/goto-bmc/goto_bmc_parse_options.cpp b/src/goto-bmc/goto_bmc_parse_options.cpp
@@ -0,0 +1,98 @@
+// Author: Fotis Koutoulakis for Diffblue Ltd.
+
+#include "goto_bmc_parse_options.h"
+
+#include <util/exit_codes.h>
+#include <util/message.h>
+#include <util/version.h>
+
+#include <libcprover-cpp/api_options.h>
+#include <libcprover-cpp/verification_result.h>
+
+#include "api.h"
+
+goto_bmc_parse_optionst::goto_bmc_parse_optionst(int argc, const char **argv)
+  : parse_options_baset(
+      GOTO_BMC_OPTIONS,
+      argc,
+      argv,
+      std::string("goto-bmc") + CBMC_VERSION)
+{
+}
+
+int goto_bmc_parse_optionst::doit()
+{
+  auto api_options = api_optionst::create();
+
+  if(cmdline.isset("version"))
+  {
+    log.status() << CBMC_VERSION << messaget::eom;
+    return CPROVER_EXIT_SUCCESS;
+  }
+
+  api_sessiont api{api_options};
+
+  if(cmdline.args.size() != 1 || !api.is_goto_binary(cmdline.args[0]))
+  {
+    log.error() << "Please give exactly one binary file" << messaget::eom;
+    return CPROVER_EXIT_INCORRECT_TASK;
+  }
+
+  std::string filename = cmdline.args[0];
+
+  if(cmdline.isset("validate-goto-model"))
+  {
+    api_options.validate_goto_model(true);
+  }
+
+  log.status() << "goto-bmc version " << *api.get_api_version()
+               << messaget::eom;
+
+  // The API works with a callback for querying state - we for now just print
+  // collected messages from the message buffer to stdout.
+  struct call_back_contextt
+  {
+    std::reference_wrapper<messaget> log;
+    bool error_seen;
+  } call_back_context{log};
+  const auto callback = [](
+                          const api_messaget &message,
+                          api_call_back_contextt api_call_back_context) {
+    auto context = static_cast<call_back_contextt *>(api_call_back_context);
+    const bool is_error_message = api_message_is_error(message);
+    context->error_seen |= is_error_message;
+    (is_error_message ? context->log.get().error()
+                      : context->log.get().status())
+      << api_message_get_string(message) << messaget::eom;
+  };
+
+  api.set_message_callback(callback, &call_back_context);
+
+  // Finally, we read the goto-binary the user supplied...
+  api.read_goto_binary(filename);
+  if(call_back_context.error_seen)
+    return CPROVER_EXIT_PARSE_ERROR;
+
+  // ... and run analysis on it.
+  auto result = api.run_verifier();
+
+  return verifier_result_to_exit_code(result->final_result());
+}
+
+void goto_bmc_parse_optionst::help()
+{
+  // clang-format off
+  log.status() << '\n' << banner_string("goto-bmc", CBMC_VERSION) << '\n'
+               << align_center_with_border("Copyright (C) 2023") << '\n'
+               << align_center_with_border("Diffblue Ltd.") << '\n' // NOLINT(*)
+               <<
+    "\n"
+    "Usage:                       Purpose:\n"
+    "\n"
+    "goto-bmc [-?] [-h] [--help]      show help\n"
+    "goto-bmc --version               show version and exit\n"
+    // NOLINTNEXTLINE(*)
+    "goto-bmc [options] file.c ...    perform bounded model checking on symex-ready goto-binary\n";
+  // clang-format on
+  log.status() << messaget::eom;
+}
diff --git a/src/goto-bmc/goto_bmc_parse_options.h b/src/goto-bmc/goto_bmc_parse_options.h
@@ -0,0 +1,29 @@
+// Author: Fotis Koutoulakis for Diffblue Ltd.
+
+#ifndef CPROVER_GOTO_BMC_GOTO_BMC_PARSE_OPTIONS_H
+#define CPROVER_GOTO_BMC_GOTO_BMC_PARSE_OPTIONS_H
+
+#include <util/parse_options.h>
+
+#include <libcprover-cpp/api_options.h>
+
+#include <memory>
+#include <string>
+#include <vector>
+
+// clang-format off
+#define GOTO_BMC_OPTIONS \
+  "(version)"
+// clang-format on
+
+class goto_bmc_parse_optionst : public parse_options_baset
+{
+public:
+  goto_bmc_parse_optionst(int argc, const char **argv);
+
+  void help() override;
+
+  int doit() override;
+};
+
+#endif // CPROVER_GOTO_BMC_GOTO_BMC_PARSE_OPTIONS_H
diff --git a/src/goto-bmc/module_dependencies.txt b/src/goto-bmc/module_dependencies.txt
@@ -0,0 +1,2 @@
+util
+libcprover-cpp
diff --git a/src/libcprover-cpp/api.cpp b/src/libcprover-cpp/api.cpp
diff --git a/src/libcprover-cpp/api.h b/src/libcprover-cpp/api.h
diff --git a/src/libcprover-cpp/verification_result.cpp b/src/libcprover-cpp/verification_result.cpp
diff --git a/src/libcprover-cpp/verification_result.h b/src/libcprover-cpp/verification_result.h

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+add_test_pl_tests(`
	`2`	`+ "$<TARGET_FILE:goto-bmc>"`
	`3`	`+)`