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.

Author: romainbrenguier

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)

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>

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

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;
+          }
+        }
+      }
     }
   }
 }