From 2ef935e28a2ddead645488eaf9056d84364555a3 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 15 Feb 2018 07:40:25 +0000
Subject: [PATCH] Add unit tests for java block instrumentation

This checks that coverage instrumentation assertions are added at the
first instruction with given bytecode index.
And that there is no such assertion in the middle of instructions with
same bytecode index.
---
 src/goto-instrument/Makefile                  |  7 ++-
 unit/CMakeLists.txt                           | 11 +++-
 unit/Makefile                                 |  1 +
 .../virtual_functions.cpp                     | 55 ++++++++++++++++++-
 4 files changed, 68 insertions(+), 6 deletions(-)

diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
index 720a3981d3c..9fe42bddd18 100644
--- a/src/goto-instrument/Makefile
+++ b/src/goto-instrument/Makefile
@@ -94,12 +94,12 @@ INCLUDES= -I ..
 
 LIBS =
 
-CLEANFILES = goto-instrument$(EXEEXT)
+CLEANFILES = goto-instrument$(EXEEXT) goto-instrument$(LIBEXT)
 
 include ../config.inc
 include ../common
 
-all: goto-instrument$(EXEEXT)
+all: goto-instrument$(EXEEXT) goto-instrument$(LIBEXT)
 
 ifneq ($(LIB_GLPK),)
   LIBS += $(LIB_GLPK)
@@ -111,6 +111,9 @@ endif
 goto-instrument$(EXEEXT): $(OBJ)
 	$(LINKBIN)
 
+goto-instrument$(LIBEXT): $(OBJ)
+	$(LINKLIB)
+
 .PHONY: goto-instrument-mac-signed
 
 goto-instrument-mac-signed: goto-instrument$(EXEEXT)
diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt
index 166c1f8c894..21316d73a38 100644
--- a/unit/CMakeLists.txt
+++ b/unit/CMakeLists.txt
@@ -36,7 +36,16 @@ target_include_directories(unit
     ${CBMC_SOURCE_DIR}
     ${CMAKE_CURRENT_SOURCE_DIR}
 )
-target_link_libraries(unit testing-utils ansi-c solvers java_bytecode)
+target_link_libraries(
+        unit
+        testing-utils
+        ansi-c
+        solvers
+        java_bytecode
+        goto-programs
+        goto-instrument-lib
+)
+
 add_test(
     NAME unit
     COMMAND $<TARGET_FILE:unit>
diff --git a/unit/Makefile b/unit/Makefile
index 16f985fa47a..100bd0a1edd 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -67,6 +67,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               ../src/util/util$(LIBEXT) \
               ../src/big-int/big-int$(LIBEXT) \
               ../src/goto-programs/goto-programs$(LIBEXT) \
+              ../src/goto-instrument/goto-instrument$(LIBEXT) \
               ../src/pointer-analysis/pointer-analysis$(LIBEXT) \
               ../src/langapi/langapi$(LIBEXT) \
               ../src/assembler/assembler$(LIBEXT) \
diff --git a/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp b/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp
index 128c19b2e5b..5f61d323142 100644
--- a/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp
+++ b/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp
@@ -8,13 +8,13 @@
 
 #include <testing-utils/catch.hpp>
 #include <testing-utils/load_java_class.h>
-#include <testing-utils/require_goto_statements.h>
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <util/config.h>
-
-#include <util/std_expr.h>
+#include <goto-instrument/cover.h>
+#include <util/options.h>
+#include <iostream>
 
 void check_function_call(
   const equal_exprt &eq_expr,
@@ -115,6 +115,55 @@ SCENARIO(
       }
 
       REQUIRE(found_function);
+
+      WHEN("basic blocks are instrumented")
+      {
+        optionst options;
+        options.set_option("cover", "location");
+        REQUIRE_FALSE(
+          instrument_cover_goals(
+            options, new_table, new_goto_functions, null_output));
+
+        auto function = new_goto_functions.function_map.find(function_name);
+        REQUIRE(function != new_goto_functions.function_map.end());
+
+        const goto_programt &goto_program = function->second.body;
+        auto it = goto_program.instructions.begin();
+        REQUIRE(it != goto_program.instructions.end());
+
+        // Skip the first instruction which is a declaration with no location
+        ++it;
+
+        THEN("Each instruction with a new bytecode index begins with ASSERT"
+               " and coverage assertions are at the beginning of the block")
+        {
+          irep_idt current_index;
+
+          while(it->type != goto_program_instruction_typet::END_FUNCTION)
+          {
+            const source_locationt &loc = it->source_location;
+            REQUIRE(loc != source_locationt::nil());
+            REQUIRE(!loc.get_java_bytecode_index().empty());
+            const auto new_index = loc.get_java_bytecode_index();
+
+            if(new_index != current_index)
+            {
+              current_index = new_index;
+              // instruction with a new bytecode index begins with ASSERT
+              REQUIRE(it->type == goto_program_instruction_typet::ASSERT);
+              // the assertion corresponds to a line coverage goal
+              REQUIRE(!loc.get_basic_block_covered_lines().empty());
+            }
+            else
+            {
+              // there is no line coverage goal in the middle of a block
+              REQUIRE(loc.get_basic_block_covered_lines().empty());
+            }
+
+            ++it;
+          }
+        }
+      }
     }
   }
 }