Merge pull request #6329 from NlightNFotis/assertions_before_assume

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

Author: TGWDB

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) \