cover_block implementation using bytecode location

This is a specific implementation of cover block for Java.
It uses the bytecode index to determine blocks and replace the use of
select_unique_java_bytecode_indices.

Author: romainbrenguier

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

@@ -108,74 +108,6 @@ cover_basic_blockst::source_location_of(const std::size_t block_nr) const
   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<std::size_t> blocks_seen;
-  std::set<irep_idt> bytecode_indices_seen;
-
-  forall_goto_program_instructions(it, goto_program)
-  {
-    const std::size_t 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;
-        }
-      }
-    }
-  }
-}
-
 void cover_basic_blockst::report_block_anomalies(
   const goto_programt &goto_program,
   message_handlert &message_handler)
@@ -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';
+}

src/goto-instrument/cover_basic_blocks.h

@@ -38,16 +38,6 @@ class cover_blocks_baset
   virtual const source_locationt &
   source_location_of(std::size_t block_nr) const = 0;
 
-  /// Select an instruction to be instrumented for each basic block such that
-  /// the java bytecode indices for each basic block is unique
-  /// \param goto_program The goto program
-  /// \param message_handler The message handler
-  virtual void select_unique_java_bytecode_indices(
-    const goto_programt &goto_program,
-    message_handlert &message_handler)
-  {
-  }
-
   /// Outputs the list of blocks
   virtual void output(std::ostream &out) const = 0;
 
@@ -83,14 +73,6 @@ class cover_basic_blockst final : public cover_blocks_baset
   const source_locationt &
   source_location_of(std::size_t block_nr) const override;
 
-  /// Select an instruction to be instrumented for each basic block such that
-  /// the java bytecode indices for each basic block is unique
-  /// \param goto_program The goto program
-  /// \param message_handler The message handler
-  void select_unique_java_bytecode_indices(
-    const goto_programt &goto_program,
-    message_handlert &message_handler) override;
-
   /// Output warnings about ignored blocks
   /// \param goto_program The goto program
   /// \param message_handler The message handler
@@ -134,4 +116,35 @@ class cover_basic_blockst final : public cover_blocks_baset
     block_mapt &block_map);
 };
 
+class cover_basic_blocks_javat final : public cover_blocks_baset
+{
+private:
+  // map block number to first instruction of the block
+  std::vector<goto_programt::const_targett> block_infos;
+  // map block number to its location
+  std::vector<source_locationt> block_locations;
+  // map java indexes to block indexes
+  std::unordered_map<irep_idt, std::size_t, irep_id_hash> index_to_block;
+
+public:
+  explicit cover_basic_blocks_javat(const goto_programt &_goto_program);
+
+  /// \param t a goto instruction
+  /// \return block number the given goto instruction is part of
+  std::size_t block_of(goto_programt::const_targett t) const override;
+
+  /// \param block_number a block number
+  /// \return first instruction of the given block
+  optionalt<goto_programt::const_targett>
+  instruction_of(std::size_t block_number) const override;
+
+  /// \param block_number a block number
+  /// \return source location corresponding to the given block
+  const source_locationt &
+  source_location_of(std::size_t block_number) const override;
+
+  /// Outputs the list of blocks
+  void output(std::ostream &out) const override;
+};
+
 #endif // CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H