Merge pull request #5636 from hannes-steffenhagen-diffblue/feature/cover-failed-assertions

Cover failed assertions

Author: hannes-steffenhagen-diffblue

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -367,7 +367,7 @@ void jdiff_parse_optionst::help()
     "\n"
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
-    " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
+    HELP_COVER
     "Java Bytecode frontend options:\n"
     JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
     "Other options:\n"

jbmc/src/jdiff/jdiff_parse_options.h

@@ -23,6 +23,8 @@ Author: Peter Schrammel
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
+#include <goto-instrument/cover.h>
+
 class goto_modelt;
 
 // clang-format off
@@ -31,7 +33,7 @@ class goto_modelt;
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
   OPT_GOTO_CHECK \
-  "(cover):" \
+  OPT_COVER \
   "(verbosity):(version)" \
   "(no-lazy-methods)" /* should go away */ \
   "(no-refine-strings)" /* should go away */ \

regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc

@@ -0,0 +1,14 @@
+CORE paths-lifo-expected-failure
+test.c
+--cover location --pointer-check --malloc-may-fail --malloc-fail-null
+\[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:17,18\): SATISFIED
+\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:15\): FAILED
+\[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12,14\): SATISFIED
+\[main\.coverage\.1\] file test\.c line \d+ function main block 1 \(lines test\.c:main:5\): SATISFIED
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This is checking that without the --cover-failed-assertions flag we still get the same result as we did before adding
+it in this example.

regression/cbmc/cover-failed-assertions/test.c

@@ -0,0 +1,18 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *ptr = malloc(sizeof(*ptr));
+  int a;
+
+  // pointer check would detect the dereference of a null pointer here
+  // default --cover lines behaviour is to treat non-cover assertions as
+  // assumptions instead, so in the ptr == NULL case we don't get past this line
+  // leading to failed coverage for the body of the if statement down below
+  a = *ptr;
+
+  if(ptr == NULL)
+    a = 1;
+
+  return 0;
+}

regression/cbmc/cover-failed-assertions/test.desc

@@ -0,0 +1,13 @@
+CORE paths-lifo-expected-failure
+test.c
+--cover location --cover-failed-assertions --pointer-check --malloc-may-fail --malloc-fail-null
+\[main.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:17,18\): SATISFIED
+\[main.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:15\): SATISFIED
+\[main.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12,14\): SATISFIED
+\[main.coverage\.1\] file test\.c line \d+ function main block 1 \(lines test\.c:main:5\): SATISFIED
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This is checking that the if statement body can actually be covered with the new flag

regression/validate-trace-xml-schema/check.py

@@ -34,6 +34,9 @@
     ['unknown-argument-suggestion', 'test.desc'],
     # this one produces XML intermingled with main XML output when used with --xml-ui
     ['graphml_witness2', 'test.desc'],
+    # these are producing coverage goals which aren't included in the schema
+    ['cover-failed-assertions', 'test.desc'],
+    ['cover-failed-assertions', 'test-no-failed-assertions.desc'],
     # produces intermingled XML on the command line
     ['coverage_report1', 'test.desc'],
     ['coverage_report1', 'paths.desc'],

src/cbmc/README.md

@@ -77,13 +77,15 @@ by other mechanism may categorise their properties differently.
 
 ### Coverage mode
 
-There is one further BMC mode that differs more fundamentally: when `--cover` is
-passed, assertions in the program text are converted into assumptions (these
+There is one further BMC mode that differs more fundamentally: when `--cover`
+is passed, assertions in the program text are converted into assumptions (these
 must hold for control flow to proceed past them, but are not goals for the
-equation solver), while new `assert(false)` statements are added throughout the
-source program representing coverage goals. The equation solving process then
-proceeds the same as in all-properties mode. Coverage solving is implemented by
-`bmc_covert`, but is structurally practically identical to
+equation solver; In cases where this behaviour is undesirable you can pass the
+`--cover-failed-assertions` which makes coverage checking continue even for
+paths where assertions fail), while new `assert(false)` statements are added
+throughout the source program representing coverage goals. The equation solving
+process then proceeds the same as in all-properties mode. Coverage solving is
+implemented by `bmc_covert`, but is structurally practically identical to
 `bmc_all_propertiest`-- only the reporting differs (goals are called "covered"
 rather than "failed").
 

src/cbmc/cbmc_parse_options.cpp

@@ -1119,7 +1119,7 @@ void cbmc_parse_optionst::help()
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"
     " --error-label label          check that label is unreachable\n"
-    " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
+    HELP_COVER
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
     // NOLINTNEXTLINE(whitespace/line_length)
     " --malloc-fail-assert         set malloc failure mode to assert-then-assume\n"

src/cbmc/cbmc_parse_options.h

@@ -34,6 +34,8 @@ Author: Daniel Kroening, [email protected]
 #include <json/json_interface.h>
 #include <xmllang/xml_interface.h>
 
+#include <goto-instrument/cover.h>
+
 class goto_functionst;
 class optionst;
 
@@ -74,7 +76,8 @@ class optionst;
   "(error-label):(verbosity):(no-library)" \
   "(nondet-static)" \
   "(version)" \
-  "(cover):(symex-coverage-report):" \
+  OPT_COVER \
+  "(symex-coverage-report):" \
   "(mm):" \
   OPT_TIMESTAMP \
   "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \

src/goto-diff/goto_diff_parse_options.cpp

@@ -411,7 +411,7 @@ void goto_diff_parse_optionst::help()
     "\n"
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
-    " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
+    HELP_COVER
     "Other options:\n"
     " --version                    show version and exit\n"
     " --json-ui                    use JSON-formatted output\n"

src/goto-diff/goto_diff_parse_options.h

@@ -22,6 +22,8 @@ Author: Peter Schrammel
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
+#include <goto-instrument/cover.h>
+
 class goto_modelt;
 class optionst;
 
@@ -31,7 +33,7 @@ class optionst;
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
   OPT_GOTO_CHECK \
-  "(cover):" \
+  OPT_COVER \
   "(verbosity):(version)" \
   OPT_FLUSH \
   OPT_TIMESTAMP \

src/goto-instrument/cover.cpp

@@ -164,6 +164,8 @@ void parse_cover_options(const cmdlinet &cmdline, optionst &options)
   options.set_option(
     "cover-traces-must-terminate",
     cmdline.isset("cover-traces-must-terminate"));
+  options.set_option(
+    "cover-failed-assertions", cmdline.isset("cover-failed-assertions"));
 }
 
 /// Build data structures controlling coverage from command-line options.
@@ -223,6 +225,9 @@ cover_configt get_cover_config(
   cover_config.traces_must_terminate =
     options.get_bool_option("cover-traces-must-terminate");
 
+  cover_config.cover_failed_assertions =
+    options.get_bool_option("cover-failed-assertions");
+
   return cover_config;
 }
 
@@ -285,16 +290,22 @@ static void instrument_cover_goals(
       // Simplify the common case where we have ASSERT(x); ASSUME(x):
       if(i_it->is_assert())
       {
-        auto successor = std::next(i_it);
-        if(
-          successor != function.body.instructions.end() &&
-          successor->is_assume() &&
-          successor->get_condition() == i_it->get_condition())
+        if(!cover_config.cover_failed_assertions)
         {
-          successor->turn_into_skip();
+          auto successor = std::next(i_it);
+          if(
+            successor != function.body.instructions.end() &&
+            successor->is_assume() &&
+            successor->get_condition() == i_it->get_condition())
+          {
+            successor->turn_into_skip();
+          }
+          i_it->type = goto_program_instruction_typet::ASSUME;
+        }
+        else
+        {
+          i_it->turn_into_skip();
         }
-
-        i_it->type = goto_program_instruction_typet::ASSUME;
       }
     }
   }

src/goto-instrument/cover.h

@@ -22,6 +22,18 @@ class message_handlert;
 class cmdlinet;
 class optionst;
 
+#define OPT_COVER                                                              \
+  "(cover):"                                                                   \
+  "(cover-failed-assertions)"
+
+#define HELP_COVER                                                             \
+  " --cover CC                   create test-suite with coverage criterion "   \
+  "CC\n"                                                                       \
+  " --cover-failed-assertions    do not stop coverage checking at failed "     \
+  "assertions\n"                                                               \
+  "                              (this is the default for --cover "            \
+  "assertions)\n"
+
 enum class coverage_criteriont
 {
   LOCATION,
@@ -37,6 +49,7 @@ enum class coverage_criteriont
 struct cover_configt
 {
   bool keep_assertions;
+  bool cover_failed_assertions;
   bool traces_must_terminate;
   irep_idt mode;
   function_filterst function_filters;