[TG-1404] Specific implementation of cover basic block for Java

regression/cbmc-java/covered1/test.desc

@@ -4,7 +4,16 @@ covered1.class
 ^EXIT=0$
 ^SIGNAL=0$
 .*\"coveredLines\": \"22\",$
-.*\"coveredLines\": \"4,6,7,23-25,31-33,36\",$
+.*\"coveredLines\": \"4\",$
+.*\"coveredLines\": \"6\",$
+.*\"coveredLines\": \"7\",$
+.*\"coveredLines\": \"23\",$
+.*\"coveredLines\": \"24\",$
+.*\"coveredLines\": \"25\",$
+.*\"coveredLines\": \"31\",$
+.*\"coveredLines\": \"32\",$
+.*\"coveredLines\": \"33\",$
+.*\"coveredLines\": \"36\",$
 .*\"coveredLines\": \"26\",$
 .*\"coveredLines\": \"28\",$
 .*\"coveredLines\": \"28\",$

regression/goto-diff/java-properties/test.desc

@@ -5,6 +5,6 @@ old.jar --json-ui --show-properties --cover location
 activate-multi-line-match
 EXIT=0
 SIGNAL=0
-  "deletedFunctions": \[\n    {\n      "name": "java::Test\.obsolete:\(\)V",\n      "properties": \[\n        {\n          "class": "coverage",\n          "coveredLines": "18",\n          "description": "block 1",\n          "expression": "false",\n          "name": "java::Test\.obsolete:\(\)V\.coverage\.1",\n          "sourceLocation": {\n            "bytecodeIndex": "0",\n            "file": "Test\.java",\n            "function": "java::Test\.obsolete:\(\)V",\n            "line": "18"\n          }\n        }\n      ],\n      "sourceLocation": {\n        "file": "Test\.java",\n        "function": "java::Test\.obsolete:\(\)V",\n        "line": "18"\n      }\n    }\n  ],\n  "modifiedFunctions": \[\n    {\n      "name": "java::Test\.<init>:\(\)V",\n      "properties": \[\n        {\n          "class": "coverage",\n          "coveredLines": "6",\n          "description": "block 1",\n          "expression": "false",\n          "name": "java::Test\.<init>:\(\)V\.coverage\.1",\n          "sourceLocation": {\n            "bytecodeIndex": "1",\n            "file": "Test\.java",\n            "function": "java::Test\.<init>:\(\)V",\n            "line": "6"\n          }\n        },\n        {\n          "class": "coverage",\n          "coveredLines": "4",\n          "description": "block 2",\n          "expression": "false",\n          "name": "java::Test\.<init>:\(\)V\.coverage\.2",\n          "sourceLocation": {\n            "bytecodeIndex": "3",\n            "file": "Test\.java",\n            "function": "java::Test\.<init>:\(\)V",\n            "line": "4"\n          }\n        },\n        {\n          "class": "coverage",\n          "coveredLines": "4",\n          "description": "block 3",\n          "expression": "false",\n          "name": "java::Test\.<init>:\(\)V\.coverage\.3",\n          "sourceLocation": {\n            "bytecodeIndex": "5",\n            "file": "Test\.java",\n            "function": "java::Test\.<init>:\(\)V",\n            "line": "4"\n          }\n        },\n        {\n          "class": "coverage",\n          "coveredLines": "4,7",\n          "description": "block 4",\n          "expression": "false",\n          "name": "java::Test\.<init>:\(\)V\.coverage\.4",\n          "sourceLocation": {\n            "bytecodeIndex": "6",\n            "file": "Test\.java",\n            "function": "java::Test\.<init>:\(\)V",\n            "line": "4"\n          }\n        }\n      ],\n      "sourceLocation": {\n        "file": "Test\.java",\n        "function": "java::Test\.<init>:\(\)V",\n        "line": "6"\n      }\n    },\n    {\n      "name": "java::Test\.<clinit>:\(\)V",\n      "properties": \[\n        {\n          "class": "coverage",\n          "coveredLines": "3",\n          "description": "block 1",\n          "expression": "false",\n          "name": "java::Test\.<clinit>:\(\)V\.coverage\.1",\n          "sourceLocation": {\n            "bytecodeIndex": "1",\n            "file": "Test\.java",\n            "function": "java::Test\.<clinit>:\(\)V",\n            "line": "3"\n          }\n        }\n      ],\n      "sourceLocation": {\n        "file": "Test\.java",\n        "function": "java::Test\.<clinit>:\(\)V",\n        "line": "3"\n      }\n    }\n  ],\n  "newFunctions": \[\n    {\n      "name": "java::Test\.newfun:\(\)V",\n      "properties": \[\n        {\n          "class": "coverage",\n          "coveredLines": "18",\n          "description": "block 1",\n          "expression": "false",\n          "name": "java::Test\.newfun:\(\)V\.coverage\.1",\n          "sourceLocation": {\n            "bytecodeIndex": "0",\n            "file": "Test\.java",\n            "function": "java::Test\.newfun:\(\)V",\n            "line": "18"\n          }\n        }\n      ],\n      "sourceLocation": {\n        "file": "Test\.java",\n        "function": "java::Test\.newfun:\(\)V",\n        "line": "18"\n      }\n    }\n  ],\n
+  "deletedFunctions": \[\n    \{\n      "name": "java::Test.obsolete:\(\)V",\n      "properties": \[\n        \{\n          "class": "coverage",\n          "coveredLines": "18",\n          "description": "block 1",\n          "expression": "false",\n          "name": "java::Test.obsolete:\(\)V.coverage.1",\n          "sourceLocation": \{\n            "bytecodeIndex": "0",\n            "file": "Test.java",\n            "function": "java::Test.obsolete:\(\)V",\n            "line": "18"\n          }\n        }\n      ],\n      "sourceLocation": \{\n        "file": "Test.java",\n        "function": "java::Test.obsolete:\(\)V",\n        "line": "18"\n      }\n    }\n  ],\n  "modifiedFunctions": \[\n    \{\n      "name": "java::Test.<init>:\(\)V",\n      "properties": \[\n        \{\n          "class": "coverage",\n          "coveredLines": "6",\n          "description": "block 2",\n          "expression": "false",\n          "name": "java::Test.<init>:\(\)V.coverage.1",\n          "sourceLocation": \{\n            "bytecodeIndex": "1",\n            "file": "Test.java",\n            "function": "java::Test.<init>:\(\)V",\n            "line": "6"\n          }\n        },\n        \{\n          "class": "coverage",\n          "coveredLines": "4",\n          "description": "block 3",\n          "expression": "false",\n          "name": "java::Test.<init>:\(\)V.coverage.2",\n          "sourceLocation": \{\n            "bytecodeIndex": "3",\n            "file": "Test.java",\n            "function": "java::Test.<init>:\(\)V",\n            "line": "4"\n          }\n        },\n        \{\n          "class": "coverage",\n          "coveredLines": "4",\n          "description": "block 4",\n          "expression": "false",\n          "name": "java::Test.<init>:\(\)V.coverage.3",\n          "sourceLocation": \{\n            "bytecodeIndex": "5",\n            "file": "Test.java",\n            "function": "java::Test.<init>:\(\)V",\n            "line": "4"\n          }\n        },\n        \{\n          "class": "coverage",\n          "coveredLines": "4",\n          "description": "block 5",\n          "expression": "false",\n          "name": "java::Test.<init>:\(\)V.coverage.4",\n          "sourceLocation": \{\n            "bytecodeIndex": "6",\n            "file": "Test.java",\n            "function": "java::Test.<init>:\(\)V",\n            "line": "4"\n          }\n        },\n        \{\n          "class": "coverage",\n          "coveredLines": "7",\n          "description": "block 6",\n          "expression": "false",\n          "name": "java::Test.<init>:\(\)V.coverage.5",\n          "sourceLocation": \{\n            "bytecodeIndex": "7",\n            "file": "Test.java",\n            "function": "java::Test.<init>:\(\)V",\n            "line": "7"\n          }\n        }\n      ],\n      "sourceLocation": \{\n        "file": "Test.java",\n        "function": "java::Test.<init>:\(\)V",\n        "line": "6"\n      }\n    },\n    \{\n      "name": "java::Test.<clinit>:\(\)V",\n      "properties": \[\n        \{\n          "class": "coverage",\n          "coveredLines": "3",\n          "description": "block 1",\n          "expression": "false",\n          "name": "java::Test.<clinit>:\(\)V.coverage.1",\n          "sourceLocation": \{\n            "bytecodeIndex": "1",\n            "file": "Test.java",\n            "function": "java::Test.<clinit>:\(\)V",\n            "line": "3"\n          }\n        }\n      ],\n      "sourceLocation": \{\n        "file": "Test.java",\n        "function": "java::Test.<clinit>:\(\)V",\n        "line": "3"\n      }\n    }\n  ],\n  "newFunctions": \[\n    \{\n      "name": "java::Test.newfun:\(\)V",\n      "properties": \[\n        \{\n          "class": "coverage",\n          "coveredLines": "18",\n          "description": "block 1",\n          "expression": "false",\n          "name": "java::Test.newfun:\(\)V.coverage.1",\n          "sourceLocation": \{\n            "bytecodeIndex": "0",\n            "file": "Test.java",\n            "function": "java::Test.newfun:\(\)V",\n            "line": "18"\n          }\n        }\n      ],\n      "sourceLocation": \{\n        "file": "Test.java",\n        "function": "java::Test.newfun:\(\)V",\n        "line": "18"\n      }\n    }\n  ],\n
 --
 ^warning: ignoring

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.cpp

@@ -24,25 +24,33 @@ Date: May 2016
 /// Applies instrumenters to given goto program
 /// \param goto_program: the goto program
 /// \param instrumenters: the instrumenters
+/// \param mode: mode of the function to instrument (for instance ID_C or
+///        ID_java)
 /// \param message_handler: a message handler
 void instrument_cover_goals(
   goto_programt &goto_program,
   const cover_instrumenterst &instrumenters,
+  const irep_idt &mode,
   message_handlert &message_handler)
 {
-  cover_basic_blockst basic_blocks(goto_program);
-  basic_blocks.select_unique_java_bytecode_indices(
-    goto_program, message_handler);
-  basic_blocks.report_block_anomalies(goto_program, message_handler);
-
-  instrumenters(goto_program, basic_blocks);
+  const std::unique_ptr<cover_blocks_baset> basic_blocks =
+    mode == ID_java ? std::unique_ptr<cover_blocks_baset>(
+                        new cover_basic_blocks_javat(goto_program))
+                    : std::unique_ptr<cover_blocks_baset>(
+                        new cover_basic_blockst(goto_program));
+
+  basic_blocks->report_block_anomalies(goto_program, message_handler);
+  instrumenters(goto_program, *basic_blocks);
 }
 
 /// Instruments goto program for a given coverage criterion
 /// \param symbol_table: the symbol table
 /// \param goto_program: the goto program
 /// \param criterion: the coverage criterion
 /// \param message_handler: a message handler
+/// \deprecated use instrument_cover_goals(goto_programt &goto_program,
+/// const cover_instrumenterst &instrumenters,
+/// message_handlert &message_handler, const irep_idt mode) instead
 void instrument_cover_goals(
   const symbol_tablet &symbol_table,
   goto_programt &goto_program,
@@ -55,7 +63,8 @@ void instrument_cover_goals(
   cover_instrumenterst instrumenters;
   instrumenters.add_from_criterion(criterion, symbol_table, goal_filters);
 
-  instrument_cover_goals(goto_program, instrumenters, message_handler);
+  instrument_cover_goals(
+    goto_program, instrumenters, ID_unknown, message_handler);
 }
 
 /// Create and add an instrumenter based on the given criterion
@@ -257,7 +266,7 @@ static void instrument_cover_goals(
   if(config.function_filters(function_id, function))
   {
     instrument_cover_goals(
-      function.body, config.cover_instrumenters, message_handler);
+      function.body, config.cover_instrumenters, config.mode, message_handler);
     changed = true;
   }
 
@@ -320,6 +329,7 @@ bool instrument_cover_goals(
 
   Forall_goto_functions(f_it, goto_functions)
   {
+    config->mode = symbol_table.lookup(f_it->first)->mode;
     instrument_cover_goals(
       *config, f_it->first, f_it->second, message_handler);
   }

src/goto-instrument/cover.h

@@ -38,6 +38,7 @@ struct cover_configt
 {
   bool keep_assertions;
   bool traces_must_terminate;
+  irep_idt mode;
   function_filterst function_filters;
   goal_filterst goal_filters;
   cover_instrumenterst cover_instrumenters;

src/goto-instrument/cover_basic_blocks.cpp

@@ -15,7 +15,7 @@ Author: Peter Schrammel
 #include <util/message.h>
 #include <util/string2int.h>
 
-optionalt<unsigned> cover_basic_blockst::continuation_of_block(
+optionalt<std::size_t> cover_basic_blockst::continuation_of_block(
   const goto_programt::const_targett &instruction,
   cover_basic_blockst::block_mapt &block_map)
 {
@@ -32,7 +32,7 @@ optionalt<unsigned> cover_basic_blockst::continuation_of_block(
 cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
 {
   bool next_is_target = true;
-  unsigned current_block = 0;
+  std::size_t current_block = 0;
 
   forall_goto_program_instructions(it, _goto_program)
   {
@@ -87,104 +87,36 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
     update_covered_lines(block_info);
 }
 
-unsigned cover_basic_blockst::block_of(goto_programt::const_targett t) const
+std::size_t cover_basic_blockst::block_of(goto_programt::const_targett t) const
 {
   const auto it = block_map.find(t);
   INVARIANT(it != block_map.end(), "instruction must be part of a block");
   return it->second;
 }
 
 optionalt<goto_programt::const_targett>
-cover_basic_blockst::instruction_of(unsigned block_nr) const
+cover_basic_blockst::instruction_of(const std::size_t block_nr) const
 {
   INVARIANT(block_nr < block_infos.size(), "block number out of range");
-  return block_infos.at(block_nr).representative_inst;
+  return block_infos[block_nr].representative_inst;
 }
 
 const source_locationt &
-cover_basic_blockst::source_location_of(unsigned block_nr) const
+cover_basic_blockst::source_location_of(const std::size_t block_nr) const
 {
   INVARIANT(block_nr < block_infos.size(), "block number out of range");
-  return block_infos.at(block_nr).source_location;
-}
-
-void cover_basic_blockst::select_unique_java_bytecode_indices(
-  const goto_programt &goto_program,
-  message_handlert &message_handler)
-{
-  messaget msg(message_handler);
-  std::set<unsigned> blocks_seen;
-  std::set<irep_idt> bytecode_indices_seen;
-
-  forall_goto_program_instructions(it, goto_program)
-  {
-    const unsigned block_nr = block_of(it);
-    if(blocks_seen.find(block_nr) != blocks_seen.end())
-      continue;
-
-    INVARIANT(block_nr < block_infos.size(), "block number out of range");
-    block_infot &block_info = block_infos.at(block_nr);
-    if(!block_info.representative_inst)
-    {
-      if(!it->source_location.get_java_bytecode_index().empty())
-      {
-        // search for a representative
-        if(
-          bytecode_indices_seen
-            .insert(it->source_location.get_java_bytecode_index())
-            .second)
-        {
-          block_info.representative_inst = it;
-          block_info.source_location = it->source_location;
-          update_covered_lines(block_info);
-          blocks_seen.insert(block_nr);
-          msg.debug() << it->function << " block " << (block_nr + 1)
-                      << ": location " << it->location_number
-                      << ", bytecode-index "
-                      << it->source_location.get_java_bytecode_index()
-                      << " selected for instrumentation." << messaget::eom;
-        }
-      }
-    }
-    else if(it == *block_info.representative_inst)
-    {
-      // check the existing representative
-      if(!it->source_location.get_java_bytecode_index().empty())
-      {
-        if(
-          bytecode_indices_seen
-            .insert(it->source_location.get_java_bytecode_index())
-            .second)
-        {
-          blocks_seen.insert(block_nr);
-        }
-        else
-        {
-          // clash, reset to search for a new one
-          block_info.representative_inst = {};
-          block_info.source_location = source_locationt::nil();
-          msg.debug() << it->function << " block " << (block_nr + 1)
-                      << ", location " << it->location_number
-                      << ": bytecode-index "
-                      << it->source_location.get_java_bytecode_index()
-                      << " already instrumented."
-                      << " Searching for alternative instruction"
-                      << " to instrument." << messaget::eom;
-        }
-      }
-    }
-  }
+  return block_infos[block_nr].source_location;
 }
 
 void cover_basic_blockst::report_block_anomalies(
   const goto_programt &goto_program,
   message_handlert &message_handler)
 {
   messaget msg(message_handler);
-  std::set<unsigned> blocks_seen;
+  std::set<std::size_t> blocks_seen;
   forall_goto_program_instructions(it, goto_program)
   {
-    const unsigned block_nr = block_of(it);
+    const std::size_t block_nr = block_of(it);
     const block_infot &block_info = block_infos.at(block_nr);
 
     if(
@@ -228,3 +160,48 @@ void cover_basic_blockst::update_covered_lines(block_infot &block_info)
   std::string covered_lines = format_number_range(line_list);
   block_info.source_location.set_basic_block_covered_lines(covered_lines);
 }
+
+cover_basic_blocks_javat::cover_basic_blocks_javat(
+  const goto_programt &_goto_program)
+{
+  forall_goto_program_instructions(it, _goto_program)
+  {
+    const auto &location = it->source_location;
+    const auto &bytecode_index = location.get_java_bytecode_index();
+    if(index_to_block.emplace(bytecode_index, block_infos.size()).second)
+    {
+      block_infos.push_back(it);
+      block_locations.push_back(location);
+      block_locations.back().set_basic_block_covered_lines(location.get_line());
+    }
+  }
+}
+
+std::size_t
+cover_basic_blocks_javat::block_of(goto_programt::const_targett t) const
+{
+  const auto &bytecode_index = t->source_location.get_java_bytecode_index();
+  const auto it = index_to_block.find(bytecode_index);
+  INVARIANT(it != index_to_block.end(), "instruction must be part of a block");
+  return it->second;
+}
+
+optionalt<goto_programt::const_targett>
+cover_basic_blocks_javat::instruction_of(const std::size_t block_nr) const
+{
+  PRECONDITION(block_nr < block_infos.size());
+  return block_infos[block_nr];
+}
+
+const source_locationt &
+cover_basic_blocks_javat::source_location_of(const std::size_t block_nr) const
+{
+  PRECONDITION(block_nr < block_locations.size());
+  return block_locations[block_nr];
+}
+
+void cover_basic_blocks_javat::output(std::ostream &out) const
+{
+  for(std::size_t i = 0; i < block_locations.size(); ++i)
+    out << block_locations[i] << " -> " << i << '\n';
+}