Merge pull request #7810 from thomasspriggs/tas/cover_assume_blocks

Define coverage blocks so as to be terminated by assumptions

regression/cbmc-cover/location-assume/end.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+void main()
+{
+  int i;
+  int *p = &i;
+  int j;
+  __CPROVER_assume(j == 1 / (*p));
+}

regression/cbmc-cover/location-assume/end.desc

@@ -0,0 +1,14 @@
+CORE
+end.c
+--pointer-check --div-by-zero-check --cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file end.c line 5 function main block 1 \(lines end\.c:main:5-8\): SATISFIED$
+^\[main.coverage.2\] file end.c line 9 function main block 2 \(lines end\.c:main:9\): SATISFIED$
+^\*\* 2 of 2 covered \(100.0%\)
+--
+^warning: ignoring
+--
+Test that in the case where multiple assertions are added on the same line of
+code due to the addition of instrumentation checks, these do not result in
+further splitting blocks.

regression/cbmc-cover/location-assume/middle.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main()
+{
+  int i;
+  int j;
+  j = i;
+  __CPROVER_assume(0);
+  j = i + 2;
+  return 0;
+}

regression/cbmc-cover/location-assume/middle.desc

@@ -0,0 +1,15 @@
+CORE
+middle.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.1\] file middle.c line 5 function main block 1 \(lines middle\.c:main:5-8\): SATISFIED$
+^\[main.coverage.2\] file middle.c line 9 function main block 2 \(lines middle\.c:main:9-11\): FAILED$
+^\*\* 1 of 2 covered \(50.0%\)
+--
+^warning: ignoring
+--
+This test confirms that assumptions in the middle of what would otherwise be a
+single blocks without control flow will cause the code to be split into 2
+coverage blocks. This is required as an unsatisfiable assumption can result in
+the following statements being unreachable.

regression/cbmc-cover/location12/test.desc

@@ -7,7 +7,8 @@ main.c
 ^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$
 ^\[foo.coverage.1\] file main.c line 3 function foo block 1.*: SATISFIED$
 ^\[foo.coverage.2\] file main.c line 4 function foo block 2.*: FAILED$
-^\[foo.coverage.3\] file main.c line 5 function foo block 3.*: SATISFIED$
-^\*\* 4 of 5 covered \(80.0%\)
+^\[foo.coverage.3\] file main.c line 5 function foo block 3.*: FAILED$
+^\[foo.coverage.4\] file main.c line 5 function foo block 4.*: SATISFIED$
+^\*\* 4 of 6 covered \(66.7%\)
 --
 ^warning: ignoring

regression/cbmc-cover/location15/test.desc

@@ -6,7 +6,8 @@ main.c
 ^\[main.coverage.1\] file main.c line 10 function main block 1.*: SATISFIED$
 ^\[main.coverage.2\] file main.c line 10 function main block 2.*: SATISFIED$
 ^\[main.coverage.3\] file main.c line 13 function main block 3.*: FAILED$
-^\[main.coverage.4\] file main.c line 16 function main block 4.*: SATISFIED$
+^\[main.coverage.4\] file main.c line 14 function main block 4.*: FAILED$
+^\[main.coverage.5\] file main.c line 16 function main block 5.*: SATISFIED$
 ^\[foo.coverage.1\] file main.c line 5 function foo block 1.*: FAILED$
 ^\*\* 3 of \d+ covered
 --

regression/cbmc-cover/location16/test.desc

@@ -9,7 +9,8 @@ main.c
 ^\[func.coverage.2\] file main.c line 6 function func block 2.*: FAILED$
 ^\[func.coverage.3\] file main.c line 8 function func block 3.*: FAILED$
 ^\[func.coverage.4\] file main.c line 12 function func block 4.*: FAILED$
-^\[func.coverage.5\] file main.c line 15 function func block 5.*: SATISFIED$
-^\*\* 4 of 7 covered \(57.1%\)
+^\[func.coverage.5\] file main.c line 14 function func block 5.*: FAILED$
+^\[func.coverage.6\] file main.c line 15 function func block 6.*: SATISFIED$
+^\*\* 4 of 8 covered \(50.0%\)
 --
 ^warning: ignoring

regression/cbmc-cover/location2/test.desc

@@ -4,8 +4,8 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.coverage.1\] file main.c line 9 function main block 1 \(lines main.c:main:9,10\): SATISFIED$
-^\[main.coverage.2\] file main.c line 11 function main block 2 \(lines main.c:main:11\): SATISFIED$
-^\*\* 2 of 2 covered \(100.0%\)
+^\[main.coverage.3\] file main.c line 11 function main block 3 \(lines main.c:main:11\): SATISFIED$
+^\*\* 3 of 3 covered \(100.0%\)
 --
 ^warning: ignoring
 main.c::5

regression/cbmc-cover/simple_assert/test.desc

@@ -4,7 +4,7 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.coverage\.1\] .* function main block 1.*: SATISFIED$
-(1 of 1|3 of 3) covered \(100\.0%\)$
+(1 of 1|2 of 2|3 of 3) covered \(100\.0%\)$
 --
 ^warning: ignoring
 ^CONVERSION ERROR$

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

@@ -1,9 +1,10 @@
 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\.5\] file test\.c line \d+ function main block 5 \(lines test\.c:main:17,18\): SATISFIED
+\[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:15\): FAILED
+\[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:12,14\): SATISFIED
+\[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12\): SATISFIED
 \[main\.coverage\.1\] file test\.c line \d+ function main block 1 \(lines test\.c:main:5\): SATISFIED
 ^EXIT=0$
 ^SIGNAL=0$

src/goto-instrument/cover_basic_blocks.cpp

@@ -29,15 +29,34 @@ optionalt<std::size_t> cover_basic_blockst::continuation_of_block(
   return {};
 }
 
+static bool
+same_source_line(const source_locationt &a, const source_locationt &b)
+{
+  return a.get_file() == b.get_file() && a.get_line() == b.get_line();
+}
+
 cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program)
 {
   bool next_is_target = true;
+  const goto_programt::instructiont *preceding_assume = nullptr;
   std::size_t current_block = 0;
 
   forall_goto_program_instructions(it, goto_program)
   {
+    // For the purposes of coverage blocks, multiple consecutive assume
+    // instructions with the same source location are considered to be part of
+    // the same block. Assumptions should terminate a block, as subsequent
+    // instructions may be unreachable. However check instrumentation passes
+    // may insert multiple assertions in the same program location. Therefore
+    // these are combined for reasons of readability of the coverage output.
+    bool end_of_assume_group =
+      preceding_assume &&
+      !(it->is_assume() &&
+        same_source_line(
+          preceding_assume->source_location(), it->source_location()));
+
     // Is it a potential beginning of a block?
-    if(next_is_target || it->is_target())
+    if(next_is_target || it->is_target() || end_of_assume_group)
     {
       if(auto block_number = continuation_of_block(it, block_map))
       {
@@ -72,13 +91,8 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program)
       block_info.source_location = it->source_location();
     }
 
-    next_is_target =
-#if 0
-      // Disabled for being too messy
-      it->is_goto() || it->is_function_call() || it->is_assume();
-#else
-      it->is_goto() || it->is_function_call();
-#endif
+    next_is_target = it->is_goto() || it->is_function_call();
+    preceding_assume = it->is_assume() ? &*it : nullptr;
   }
 }