Merge pull request #1819 from romainbrenguier/refactor/coverage-instrumentation

Refactoring in coverage instrumentation

Author: romainbrenguier

src/goto-instrument/cover_basic_blocks.cpp

@@ -15,6 +15,20 @@ Author: Peter Schrammel
 #include <util/message.h>
 #include <util/string2int.h>
 
+optionalt<unsigned> cover_basic_blockst::continuation_of_block(
+  const goto_programt::const_targett &instruction,
+  cover_basic_blockst::block_mapt &block_map)
+{
+  if(instruction->incoming_edges.size() != 1)
+    return {};
+
+  const goto_programt::targett in_t = *instruction->incoming_edges.cbegin();
+  if(in_t->is_goto() && !in_t->is_backwards_goto() && in_t->guard.is_true())
+    return block_map[in_t];
+
+  return {};
+}
+
 cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
 {
   bool next_is_target = true;
@@ -25,25 +39,13 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
     // Is it a potential beginning of a block?
     if(next_is_target || it->is_target())
     {
-      // We keep the block number if this potential block
-      // is a continuation of a previous block through
-      // unconditional forward gotos; otherwise we increase the
-      // block number.
-      bool increase_block_nr = true;
-      if(it->incoming_edges.size() == 1)
+      if(auto block_number = continuation_of_block(it, block_map))
       {
-        goto_programt::targett in_t = *it->incoming_edges.begin();
-        if(
-          in_t->is_goto() && !in_t->is_backwards_goto() &&
-          in_t->guard.is_true())
-        {
-          current_block = block_map[in_t];
-          increase_block_nr = false;
-        }
+        current_block = *block_number;
       }
-      if(increase_block_nr)
+      else
       {
-        block_infos.push_back(block_infot());
+        block_infos.emplace_back();
         block_infos.back().representative_inst = it;
         block_infos.back().source_location = source_locationt::nil();
         current_block = block_infos.size() - 1;
@@ -87,12 +89,12 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
 
 unsigned cover_basic_blockst::block_of(goto_programt::const_targett t) const
 {
-  block_mapt::const_iterator it = block_map.find(t);
+  const auto it = block_map.find(t);
   INVARIANT(it != block_map.end(), "instruction must be part of a block");
   return it->second;
 }
 
-goto_programt::const_targett
+optionalt<goto_programt::const_targett>
 cover_basic_blockst::instruction_of(unsigned block_nr) const
 {
   INVARIANT(block_nr < block_infos.size(), "block number out of range");
@@ -116,13 +118,13 @@ void cover_basic_blockst::select_unique_java_bytecode_indices(
 
   forall_goto_program_instructions(it, goto_program)
   {
-    unsigned block_nr = block_of(it);
+    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 == goto_program.instructions.end())
+    if(!block_info.representative_inst)
     {
       if(!it->source_location.get_java_bytecode_index().empty())
       {
@@ -144,7 +146,7 @@ void cover_basic_blockst::select_unique_java_bytecode_indices(
         }
       }
     }
-    else if(it == block_info.representative_inst)
+    else if(it == *block_info.representative_inst)
     {
       // check the existing representative
       if(!it->source_location.get_java_bytecode_index().empty())
@@ -159,7 +161,7 @@ void cover_basic_blockst::select_unique_java_bytecode_indices(
         else
         {
           // clash, reset to search for a new one
-          block_info.representative_inst = goto_program.instructions.end();
+          block_info.representative_inst = {};
           block_info.source_location = source_locationt::nil();
           msg.debug() << it->function << " block " << (block_nr + 1)
                       << ", location " << it->location_number
@@ -182,7 +184,7 @@ void cover_basic_blockst::report_block_anomalies(
   std::set<unsigned> blocks_seen;
   forall_goto_program_instructions(it, goto_program)
   {
-    unsigned block_nr = block_of(it);
+    const unsigned block_nr = block_of(it);
     const block_infot &block_info = block_infos.at(block_nr);
 
     if(
@@ -223,7 +225,6 @@ void cover_basic_blockst::update_covered_lines(block_infot &block_info)
   INVARIANT(!cover_set.empty(), "covered lines set must not be empty");
   std::vector<unsigned> line_list(cover_set.begin(), cover_set.end());
 
-  format_number_ranget format_lines;
-  std::string covered_lines = format_lines(line_list);
+  std::string covered_lines = format_number_range(line_list);
   block_info.source_location.set_basic_block_covered_lines(covered_lines);
 }

src/goto-instrument/cover_basic_blocks.h

@@ -18,7 +18,7 @@ Author: Daniel Kroening
 
 class message_handlert;
 
-class cover_basic_blockst
+class cover_basic_blockst final
 {
 public:
   explicit cover_basic_blockst(const goto_programt &_goto_program);
@@ -31,7 +31,8 @@ class cover_basic_blockst
   /// \param block_nr a block number
   /// \return  the instruction selected for
   ///   instrumentation representative of the given block
-  goto_programt::const_targett instruction_of(unsigned block_nr) const;
+  optionalt<goto_programt::const_targett>
+  instruction_of(unsigned block_nr) const;
 
   /// \param block_nr a block number
   /// \return  the source location selected for
@@ -56,32 +57,37 @@ class cover_basic_blockst
   /// Outputs the list of blocks
   void output(std::ostream &out) const;
 
-protected:
-  // map program locations to block numbers
+private:
   typedef std::map<goto_programt::const_targett, unsigned> block_mapt;
-  block_mapt block_map;
 
   struct block_infot
   {
     /// the program location to instrument for this block
-    goto_programt::const_targett representative_inst;
+    optionalt<goto_programt::const_targett> representative_inst;
 
     /// the source location representative for this block
-    // (we need a separate copy of source locations because we attach
-    //  the line number ranges to them)
+    /// (we need a separate copy of source locations because we attach
+    ///  the line number ranges to them)
     source_locationt source_location;
 
-    // map block numbers to source code locations
     /// the set of lines belonging to this block
     std::unordered_set<unsigned> lines;
   };
 
-  typedef std::vector<block_infot> block_infost;
-  block_infost block_infos;
+  /// map program locations to block numbers
+  block_mapt block_map;
+  /// map block numbers to block information
+  std::vector<block_infot> block_infos;
 
   /// create list of covered lines as CSV string and set as property of source
   /// location of basic block, compress to ranges if applicable
-  void update_covered_lines(block_infot &block_info);
+  static void update_covered_lines(block_infot &block_info);
+
+  /// If this block is a continuation of a previous block through unconditional
+  /// forward gotos, return this blocks number.
+  static optionalt<unsigned> continuation_of_block(
+    const goto_programt::const_targett &instruction,
+    block_mapt &block_map);
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H

src/goto-instrument/cover_instrument_location.cpp

@@ -22,20 +22,19 @@ void cover_location_instrumentert::instrument(
   if(is_non_cover_assertion(i_it))
     i_it->make_skip();
 
-  unsigned block_nr = basic_blocks.block_of(i_it);
-  goto_programt::const_targett in_t = basic_blocks.instruction_of(block_nr);
+  const unsigned block_nr = basic_blocks.block_of(i_it);
+  const auto representative_instruction = basic_blocks.instruction_of(block_nr);
   // we only instrument the selected instruction
-  if(in_t == i_it)
+  if(representative_instruction && *representative_instruction == i_it)
   {
-    std::string b = std::to_string(block_nr + 1); // start with 1
-    std::string id = id2string(i_it->function) + "#" + b;
-    source_locationt source_location =
-      basic_blocks.source_location_of(block_nr);
+    const std::string b = std::to_string(block_nr + 1); // start with 1
+    const std::string id = id2string(i_it->function) + "#" + b;
+    const auto source_location = basic_blocks.source_location_of(block_nr);
 
     // filter goals
     if(goal_filters(source_location))
     {
-      std::string comment = "block " + b;
+      const std::string comment = "block " + b;
       const irep_idt function = i_it->function;
       goto_program.insert_before_swap(i_it);
       i_it->make_assertion(false_exprt());

src/util/format_number_range.cpp

@@ -16,9 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "format_number_range.h"
 
 /// create shorter representation for output
-/// \par parameters: vector of numbers
+/// \param parameters: vector of numbers
 /// \return string of compressed number range representation
-std::string format_number_ranget::operator()(std::vector<unsigned> &numbers)
+std::string format_number_range(std::vector<unsigned> &numbers)
 {
   std::string number_range;
   std::sort(numbers.begin(), numbers.end());

src/util/format_number_range.h

@@ -15,10 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <string>
 #include <vector>
 
-class format_number_ranget
-{
-public:
-  std::string operator()(std::vector<unsigned> &);
-};
+std::string format_number_range(std::vector<unsigned> &);
 
 #endif // CPROVER_UTIL_FORMAT_NUMBER_RANGE_H