[TG-2356] skip basic block instrumentation from virtual call removal

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)

src/goto-instrument/cover_filter.cpp

@@ -101,5 +101,8 @@ operator()(const source_locationt &source_location) const
   if(source_location.is_built_in())
     return false;
 
+  if(source_location.get_java_removed_virtual_call())
+    return false;
+
   return true;
 }

src/goto-programs/remove_virtual_functions.cpp

@@ -276,6 +276,8 @@ void remove_virtual_functionst::remove_virtual_function(
     const irep_idt property_class=it->source_location.get_property_class();
     const irep_idt comment=it->source_location.get_comment();
     it->source_location=target->source_location;
+    // mark instruction as originating from a removed virtual function call
+    it->source_location.set_java_removed_virtual_call();
     it->function=target->function;
     if(!property_class.empty())
       it->source_location.set_property_class(property_class);

src/util/irep_ids.def

@@ -840,6 +840,7 @@ IREP_ID_TWO(type_variables, #type_variables)
 IREP_ID_ONE(havoc_object)
 IREP_ID_TWO(overflow_shl, overflow-shl)
 IREP_ID_TWO(C_no_initialization_required, #no_initialization_required)
+IREP_ID_TWO(C_java_removed_virtual_call, #java_removed_virtual_call)
 
 #undef IREP_ID_ONE
 #undef IREP_ID_TWO

src/util/source_location.h

@@ -151,6 +151,19 @@ class source_locationt:public irept
     return set(ID_basic_block_covered_lines, covered_lines);
   }
 
+  /// Add comment to source location as originating from removed virtual call
+  void set_java_removed_virtual_call()
+  {
+    set(ID_C_java_removed_virtual_call, true);
+  }
+
+  /// Get information about whether call originated from a removed virtual
+  /// function call
+  bool get_java_removed_virtual_call() const
+  {
+    return get_bool(ID_C_java_removed_virtual_call);
+  }
+
   void set_hide()
   {
     set(ID_hide, true);

unit/CMakeLists.txt

@@ -36,7 +36,15 @@ 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

@@ -66,6 +66,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

@@ -13,7 +13,8 @@
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <util/config.h>
-
+#include <goto-instrument/cover.h>
+#include <util/options.h>
 #include <util/std_expr.h>
 
 void check_function_call(
@@ -113,8 +114,54 @@ SCENARIO(
           }
         }
       }
-
       REQUIRE(found_function);
+
+      WHEN("basic blocks are instrumented")
+      {
+        optionst options;
+        options.set_option("cover", "location");
+        THEN("instrumentation assertions are inserted")
+        {
+          REQUIRE_FALSE(
+            instrument_cover_goals(
+              options, new_table, new_goto_functions, null_output));
+        }
+        THEN(
+          "instructions are marked as originating from virtual function call "
+          "removal")
+        {
+          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 = std::find_if(
+            goto_program.instructions.begin(),
+            goto_program.instructions.end(),
+            [](const goto_programt::instructiont &instruction) {
+              return instruction.type == goto_program_instruction_typet::GOTO &&
+                     instruction.guard.id() == ID_equal;
+            });
+          REQUIRE(it != goto_program.instructions.end());
+          THEN(
+            "all instructions that share the same bytecode index "
+            "are marked as originating from a removed virtual function "
+            "call and there is no GOTO ASSERT")
+          {
+            const source_locationt &loc = it->source_location;
+            REQUIRE(loc != source_locationt::nil());
+            REQUIRE(!loc.get_java_bytecode_index().empty());
+
+            while(it->source_location != source_locationt::nil() &&
+                  it->source_location.get_java_bytecode_index() ==
+                    loc.get_java_bytecode_index())
+            {
+              REQUIRE(it->source_location.get_java_removed_virtual_call());
+              REQUIRE(it->type != goto_program_instruction_typet::ASSERT);
+              ++it;
+            }
+          }
+        }
+      }
     }
   }
 }