Add regression tests for basic functionality of goto-bmc

regression/CMakeLists.txt

@@ -54,6 +54,8 @@ add_subdirectory(invariants)
 add_subdirectory(goto-diff)
 add_subdirectory(test-script)
 add_subdirectory(goto-analyzer-taint)
+add_subdirectory(goto-bmc)
+add_subdirectory(goto-bmc-non-symex-ready-goto)
 if(NOT WIN32)
   add_subdirectory(goto-gcc)
 else()

regression/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}"
+)

regression/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}

regression/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;
+}

regression/goto-bmc-non-symex-ready-goto/negative1/main.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+
+^EXIT=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.

regression/goto-bmc/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/`

regression/goto-bmc/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}"

regression/goto-bmc/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;
+}

regression/goto-bmc/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
+--

src/goto-bmc/goto_bmc_parse_options.cpp

@@ -50,7 +50,7 @@ int core_cbmc_only_parse_optionst::doit()
   }
 
   if(
-    cmdline.args.size() != 1 ||
+    cmdline.args.size() > 1 &&
     !is_goto_binary(cmdline.args[0], ui_message_handler))
   {
     log.error() << "Please give exactly one binary file" << messaget::eom;