--cover assume: Add assert statements before assume to check for coverage

doc/cprover-manual/modeling-assumptions.md

@@ -71,3 +71,37 @@ int main() {
 This code fails, as there is a choice of x and y which results in a counterexample
 (any choice in which x and y are different).
 
+## Coverage
+
+You can ask CBMC to give coverage information regarding `__CPROVER_assume` statements.
+This is useful when you need, for example, to check which assume statements may have
+led to an emptying of the search state space, resulting in `assert` statements being
+vaccuously passed.
+
+To use that invoke CBMC with the `--cover assume` option. For example, for a file:
+
+```c
+#include <assert.h>
+
+int main()
+{
+  int x;
+  __CPROVER_assume(x > 0);
+  __CPROVER_assume(x < 0);
+  assert(0 == 1);
+}
+```
+
+CBMC invoked with `cbmc --cover assume test.c` will report:
+
+```sh
+[main.1] file assume_assert.c line 6 function main assert(false) before assume(x > 0): SATISFIED
+[main.2] file assume_assert.c line 6 function main assert(false) after assume(x > 0): SATISFIED
+[main.3] file assume_assert.c line 7 function main assert(false) before assume(x < 0): SATISFIED
+[main.4] file assume_assert.c line 7 function main assert(false) after assume(x < 0): FAILED
+```
+
+When an `assert(false)` statement before the assume has the property status `SATISFIED`,
+but is followed by an `assert(false)` statement *after* the assume statement that has status
+`FAILED`, this is an indication that this specific assume statement (on the line reported)
+is one that is emptying the search space for model checking.

doc/cprover-manual/test-suite.md

@@ -213,6 +213,7 @@ The table below summarizes the coverage criteria that CBMC supports.
 Criterion |Definition
 ----------|----------
 assertion |For every assertion, generate a test that reaches it
+assume    |For every assume, generate tests before and after the assume statement to indicate coverage before and after it
 location  |For every location, generate a test that reaches it
 branch    |Generate a test for every branch outcome
 decision  |Generate a test for both outcomes of every Boolean expression that is not an operand of a propositional connective

jbmc/src/jbmc/Makefile

@@ -24,6 +24,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_basic_blocks$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_filter$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_assume$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_branch$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_condition$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_decision$(OBJEXT) \

jbmc/src/jdiff/Makefile

@@ -18,6 +18,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_basic_blocks$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_filter$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_assume$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_branch$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_condition$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_decision$(OBJEXT) \

jbmc/unit/Makefile

@@ -105,6 +105,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               $(CPROVER_DIR)/src/goto-instrument/cover$(OBJEXT) \
               $(CPROVER_DIR)/src/goto-instrument/cover_basic_blocks$(OBJEXT) \
               $(CPROVER_DIR)/src/goto-instrument/cover_filter$(OBJEXT) \
+              $(CPROVER_DIR)/src/goto-instrument/cover_instrument_assume$(OBJEXT) \
               $(CPROVER_DIR)/src/goto-instrument/cover_instrument_branch$(OBJEXT) \
               $(CPROVER_DIR)/src/goto-instrument/cover_instrument_condition$(OBJEXT) \
               $(CPROVER_DIR)/src/goto-instrument/cover_instrument_decision$(OBJEXT) \

regression/cbmc-cover/assume_assert1/assume_assert.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int main()
+{
+  int x;
+  __CPROVER_assume(x > 0);
+  __CPROVER_assume(x < 0);
+  assert(0 == 1);
+}

regression/cbmc-cover/assume_assert1/test.desc

@@ -0,0 +1,11 @@
+CORE
+assume_assert.c
+--cover assume
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file assume_assert.c line \d function main assert\(false\) before assume\(x > 0\): SATISFIED$
+^\[main.coverage.2\] file assume_assert.c line \d function main assert\(false\) after assume\(x > 0\): SATISFIED$
+^\[main.coverage.3\] file assume_assert.c line \d function main assert\(false\) before assume\(x < 0\): SATISFIED$
+^\[main.coverage.4\] file assume_assert.c line \d function main assert\(false\) after assume\(x < 0\): FAILED$
+--
+^warning: ignoring

regression/cbmc-cover/assume_assert2/assume_assert.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  int a;
+
+  if(a > 0)
+  {
+    assert(a > 0);
+  }
+  else if(a < 0)
+  {
+    __CPROVER_assume(a >= 0);
+    assert(a < 0);
+  }
+  else
+  {
+    assert(a == 0);
+  }
+}

regression/cbmc-cover/assume_assert2/test.desc

@@ -0,0 +1,9 @@
+CORE
+assume_assert.c
+--cover assume
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file assume_assert.c line \d+ function main assert\(false\) before assume\(a >= 0\): SATISFIED$
+^\[main.coverage.2\] file assume_assert.c line \d+ function main assert\(false\) after assume\(a >= 0\): FAILED$
+--
+^warning: ignoring

src/cbmc/Makefile

@@ -26,6 +26,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../goto-instrument/cover$(OBJEXT) \
       ../goto-instrument/cover_basic_blocks$(OBJEXT) \
       ../goto-instrument/cover_filter$(OBJEXT) \
+      ../goto-instrument/cover_instrument_assume$(OBJEXT) \
       ../goto-instrument/cover_instrument_branch$(OBJEXT) \
       ../goto-instrument/cover_instrument_condition$(OBJEXT) \
       ../goto-instrument/cover_instrument_decision$(OBJEXT) \

src/goto-checker/properties.h

@@ -12,7 +12,7 @@ Author: Daniel Kroening, Peter Schrammel
 #ifndef CPROVER_GOTO_CHECKER_PROPERTIES_H
 #define CPROVER_GOTO_CHECKER_PROPERTIES_H
 
-#include <unordered_map>
+#include <map>
 
 #include <goto-programs/goto_program.h>
 
@@ -73,7 +73,7 @@ struct property_infot
 };
 
 /// A map of property IDs to property infos
-typedef std::unordered_map<irep_idt, property_infot> propertiest;
+typedef std::map<irep_idt, property_infot> propertiest;
 
 /// Returns the properties in the goto model
 propertiest initialize_properties(const abstract_goto_modelt &);

src/goto-diff/Makefile

@@ -18,6 +18,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../goto-instrument/cover$(OBJEXT) \
       ../goto-instrument/cover_basic_blocks$(OBJEXT) \
       ../goto-instrument/cover_filter$(OBJEXT) \
+      ../goto-instrument/cover_instrument_assume$(OBJEXT) \
       ../goto-instrument/cover_instrument_branch$(OBJEXT) \
       ../goto-instrument/cover_instrument_condition$(OBJEXT) \
       ../goto-instrument/cover_instrument_decision$(OBJEXT) \

src/goto-instrument/Makefile

@@ -24,6 +24,7 @@ SRC = accelerate/accelerate.cpp \
       cover.cpp \
       cover_basic_blocks.cpp \
       cover_filter.cpp \
+      cover_instrument_assume.cpp \
       cover_instrument_branch.cpp \
       cover_instrument_condition.cpp \
       cover_instrument_decision.cpp \

src/goto-instrument/cover.cpp

@@ -99,6 +99,10 @@ void cover_instrumenterst::add_from_criterion(
   case coverage_criteriont::COVER:
     instrumenters.push_back(
       util_make_unique<cover_cover_instrumentert>(symbol_table, goal_filters));
+    break;
+  case coverage_criteriont::ASSUME:
+    instrumenters.push_back(
+      util_make_unique<cover_assume_instrumentert>(symbol_table, goal_filters));
   }
 }
 
@@ -126,6 +130,8 @@ parse_coverage_criterion(const std::string &criterion_string)
     c = coverage_criteriont::MCDC;
   else if(criterion_string == "cover")
     c = coverage_criteriont::COVER;
+  else if(criterion_string == "assume")
+    c = coverage_criteriont::ASSUME;
   else
   {
     std::stringstream s;
@@ -201,6 +207,9 @@ cover_configt get_cover_config(
 
     if(c == coverage_criteriont::ASSERTION)
       cover_config.keep_assertions = true;
+    // Make sure that existing assertions don't get replaced by assumes
+    else if(c == coverage_criteriont::ASSUME)
+      cover_config.keep_assertions = true;
 
     instrumenters.add_from_criterion(c, symbol_table, *goal_filters);
   }

src/goto-instrument/cover.h

@@ -41,6 +41,7 @@ class optionst;
 
 enum class coverage_criteriont
 {
+  ASSUME,
   LOCATION,
   BRANCH,
   DECISION,

src/goto-instrument/cover_instrument.h

@@ -292,4 +292,24 @@ void cover_instrument_end_of_function(
   goto_programt &goto_program,
   const cover_instrumenter_baset::assertion_factoryt &);
 
+// assume-instructions instrumenter.
+class cover_assume_instrumentert : public cover_instrumenter_baset
+{
+public:
+  cover_assume_instrumentert(
+    const symbol_tablet &_symbol_table,
+    const goal_filterst &_goal_filters)
+    : cover_instrumenter_baset(_symbol_table, _goal_filters, "location")
+  {
+  }
+
+protected:
+  void instrument(
+    const irep_idt &,
+    goto_programt &,
+    goto_programt::targett &,
+    const cover_blocks_baset &,
+    const assertion_factoryt &) const override;
+};
+
 #endif // CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H

src/goto-instrument/cover_instrument_assume.cpp

@@ -0,0 +1,52 @@
+/// \file cover_instrument_assume.cpp
+/// Author: Diffblue Ltd.
+/// Coverage Instrumentation for ASSUME instructions.
+
+#include "cover_instrument.h"
+
+#include "ansi-c/expr2c.h"
+#include "goto-programs/goto_program.h"
+#include "util/std_expr.h"
+#include <util/namespace.h>
+
+/// Instrument program to check coverage of assume statements.
+/// \param function_id The name of the function under instrumentation.
+/// \param goto_program The goto-program (function under instrumentation).
+/// \param i_it The current instruction (instruction under instrumentation).
+/// \param make_assertion The assertion generator function.
+void cover_assume_instrumentert::instrument(
+  const irep_idt &function_id,
+  goto_programt &goto_program,
+  goto_programt::targett &i_it,
+  const cover_blocks_baset &,
+  const assertion_factoryt &make_assertion) const
+{
+  if(i_it->is_assume())
+  {
+    const auto location = i_it->source_location;
+    const auto assume_condition =
+      expr2c(i_it->get_condition(), namespacet{symbol_tablet()});
+    const auto comment_before =
+      "assert(false) before assume(" + assume_condition + ")";
+    const auto comment_after =
+      "assert(false) after assume(" + assume_condition + ")";
+
+    const auto assert_before = make_assertion(false_exprt{}, location);
+    goto_programt::targett t = goto_program.insert_before(i_it, assert_before);
+    initialize_source_location(t, comment_before, function_id);
+
+    const auto assert_after = make_assertion(false_exprt{}, location);
+    t = goto_program.insert_after(i_it, assert_after);
+    initialize_source_location(t, comment_after, function_id);
+  }
+  // Otherwise, skip existing assertions.
+  else if(i_it->is_assert())
+  {
+    const auto location = i_it->source_location;
+    // Filter based on if assertion was added by us as part of instrumentation.
+    if(location.get_property_class() != "coverage")
+    {
+      i_it->turn_into_skip();
+    }
+  }
+}

unit/Makefile

@@ -221,6 +221,7 @@ BMC_DEPS =../src/cbmc/c_test_input_generator$(OBJEXT) \
           ../src/goto-instrument/cover$(OBJEXT) \
           ../src/goto-instrument/cover_basic_blocks$(OBJEXT) \
           ../src/goto-instrument/cover_filter$(OBJEXT) \
+          ../src/goto-instrument/cover_instrument_assume$(OBJEXT) \
           ../src/goto-instrument/cover_instrument_branch$(OBJEXT) \
           ../src/goto-instrument/cover_instrument_condition$(OBJEXT) \
           ../src/goto-instrument/cover_instrument_decision$(OBJEXT) \