Remove basic_block_covered_lines

The information in basic_block_source_lines is much more accurate for it
distinguishes source lines belonging to different files or functions
(which may still end up in the same basic block after inlining).

Author: tautschnig

jbmc/regression/jdiff/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 \(lines Test.java:java::Test.obsolete:\(\)V:18\)",\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 \(lines Test.java:java::Test.<init>:\(\)V:6\)",\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 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\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 \(lines Test.java:java::Test.<init>:\(\)V: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 \(lines Test.java:java::Test.<init>:\(\)V: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            "class": "coverage",\n            "coveredLines": "7",\n            "description": "block 6 \(lines Test.java:java::Test.<init>:\(\)V:7\)",\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 \(lines Test.java:java::Test.<clinit>:\(\)V:3\)",\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 \(lines Test.java:java::Test.newfun:\(\)V:18\)",\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": "Test.java:java::Test.obsolete:\(\)V:18",\n            "description": "block 1 \(lines Test.java:java::Test.obsolete:\(\)V:18\)",\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": "Test.java:java::Test.<init>:\(\)V:6",\n            "description": "block 2 \(lines Test.java:java::Test.<init>:\(\)V:6\)",\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": "Test.java:java::Test.<init>:\(\)V:4",\n            "description": "block 3 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\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": "Test.java:java::Test.<init>:\(\)V:4",\n            "description": "block 4 \(lines Test.java:java::Test.<init>:\(\)V: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": "Test.java:java::Test.<init>:\(\)V:4",\n            "description": "block 5 \(lines Test.java:java::Test.<init>:\(\)V: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            "class": "coverage",\n            "coveredLines": "Test.java:java::Test.<init>:\(\)V:7",\n            "description": "block 6 \(lines Test.java:java::Test.<init>:\(\)V:7\)",\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": "Test.java:java::Test.<clinit>:\(\)V:3",\n            "description": "block 1 \(lines Test.java:java::Test.<clinit>:\(\)V:3\)",\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": "Test.java:java::Test.newfun:\(\)V:18",\n            "description": "block 1 \(lines Test.java:java::Test.newfun:\(\)V:18\)",\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

jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

@@ -159,12 +159,12 @@ SCENARIO(
               // 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_FALSE(loc.get_basic_block_covered_lines().empty());
+              REQUIRE_FALSE(loc.get_basic_block_source_lines().empty());
             }
             else
             {
               // there is no line coverage goal in the middle of a block
-              REQUIRE(loc.get_basic_block_covered_lines().empty());
+              REQUIRE(loc.get_basic_block_source_lines().empty());
             }
 
             ++it;

src/goto-instrument/cover_basic_blocks.cpp

@@ -11,9 +11,7 @@ Author: Peter Schrammel
 
 #include "cover_basic_blocks.h"
 
-#include <util/format_number_range.h>
 #include <util/message.h>
-#include <util/string2int.h>
 
 optionalt<std::size_t> cover_basic_blockst::continuation_of_block(
   const goto_programt::const_targett &instruction,
@@ -80,12 +78,6 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &goto_program)
       it->is_goto() || it->is_function_call();
 #endif
   }
-
-  for(auto &block_info : block_infos)
-  {
-    update_covered_lines(block_info);
-    update_source_lines(block_info);
-  }
 }
 
 std::size_t cover_basic_blockst::block_of(goto_programt::const_targett t) const
@@ -109,6 +101,13 @@ cover_basic_blockst::source_location_of(const std::size_t block_nr) const
   return block_infos[block_nr].source_location;
 }
 
+const source_linest &
+cover_basic_blockst::source_lines_of(const std::size_t block_nr) const
+{
+  INVARIANT(block_nr < block_infos.size(), "block number out of range");
+  return block_infos[block_nr].source_lines;
+}
+
 void cover_basic_blockst::report_block_anomalies(
   const irep_idt &function_id,
   const goto_programt &goto_program,
@@ -158,7 +157,6 @@ void cover_basic_blockst::add_block_lines(
     const irep_idt &line = location.get_line();
     if(!line.empty())
     {
-      block.lines.insert(unsafe_string2unsigned(id2string(line)));
       block.source_lines.insert(location);
     }
   };
@@ -167,35 +165,9 @@ void cover_basic_blockst::add_block_lines(
     [&](const exprt &expr) { add_location(expr.source_location()); });
 }
 
-void cover_basic_blockst::update_covered_lines(block_infot &block_info)
-{
-  if(block_info.source_location.is_nil())
-    return;
-
-  const auto &cover_set = block_info.lines;
-  INVARIANT(!cover_set.empty(), "covered lines set must not be empty");
-  std::vector<unsigned> line_list(cover_set.begin(), cover_set.end());
-
-  std::string covered_lines = format_number_range(line_list);
-  block_info.source_location.set_basic_block_covered_lines(covered_lines);
-}
-
-void cover_basic_blockst::update_source_lines(block_infot &block_info)
-{
-  if(block_info.source_location.is_nil())
-    return;
-
-  const auto &source_lines = block_info.source_lines;
-  std::string str = source_lines.to_string();
-  INVARIANT(!str.empty(), "source lines set must not be empty");
-  block_info.source_location.set_basic_block_source_lines(str);
-}
-
 cover_basic_blocks_javat::cover_basic_blocks_javat(
   const goto_programt &_goto_program)
 {
-  std::set<std::size_t> source_lines_requiring_update;
-
   forall_goto_program_instructions(it, _goto_program)
   {
     const auto &location = it->source_location();
@@ -205,22 +177,13 @@ cover_basic_blocks_javat::cover_basic_blocks_javat(
     {
       block_infos.push_back(it);
       block_locations.push_back(location);
-      block_locations.back().set_basic_block_covered_lines(location.get_line());
       block_source_lines.emplace_back(location);
-      source_lines_requiring_update.insert(entry.first->second);
     }
     else
     {
       block_source_lines[entry.first->second].insert(location);
-      source_lines_requiring_update.insert(entry.first->second);
     }
   }
-
-  for(std::size_t i : source_lines_requiring_update)
-  {
-    block_locations.at(i).set_basic_block_source_lines(
-      block_source_lines.at(i).to_string());
-  }
 }
 
 std::size_t
@@ -246,6 +209,13 @@ cover_basic_blocks_javat::source_location_of(const std::size_t block_nr) const
   return block_locations[block_nr];
 }
 
+const source_linest &
+cover_basic_blocks_javat::source_lines_of(const std::size_t block_nr) const
+{
+  PRECONDITION(block_nr < block_locations.size());
+  return block_source_lines[block_nr];
+}
+
 void cover_basic_blocks_javat::output(std::ostream &out) const
 {
   for(std::size_t i = 0; i < block_locations.size(); ++i)

src/goto-instrument/cover_basic_blocks.h

@@ -43,6 +43,10 @@ class cover_blocks_baset
   virtual const source_locationt &
   source_location_of(std::size_t block_nr) const = 0;
 
+  /// \param block_nr: a block number
+  /// \return the source lines of the given block
+  virtual const source_linest &source_lines_of(std::size_t block_nr) const = 0;
+
   /// Outputs the list of blocks
   virtual void output(std::ostream &out) const = 0;
 
@@ -84,6 +88,10 @@ class cover_basic_blockst final : public cover_blocks_baset
   const source_locationt &
   source_location_of(std::size_t block_nr) const override;
 
+  /// \param block_nr: a block number
+  /// \return the source lines of the given block
+  const source_linest &source_lines_of(std::size_t block_nr) const override;
+
   /// Output warnings about ignored blocks
   /// \param function_id: name of \p goto_program
   /// \param goto_program: The goto program
@@ -109,9 +117,6 @@ class cover_basic_blockst final : public cover_blocks_baset
     ///  the line number ranges to them)
     source_locationt source_location;
 
-    /// the set of lines belonging to this block
-    std::unordered_set<std::size_t> lines;
-
     /// the set of source code lines belonging to this block
     source_linest source_lines;
   };
@@ -126,14 +131,6 @@ class cover_basic_blockst final : public cover_blocks_baset
     cover_basic_blockst::block_infot &block,
     const goto_programt::instructiont &instruction);
 
-  /// create list of covered lines as CSV string and set as property of source
-  /// location of basic block, compress to ranges if applicable
-  static void update_covered_lines(block_infot &block_info);
-
-  /// create a string representing source lines and set as a property of source
-  /// location of basic block
-  static void update_source_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<std::size_t> continuation_of_block(
@@ -170,6 +167,10 @@ class cover_basic_blocks_javat final : public cover_blocks_baset
   const source_locationt &
   source_location_of(std::size_t block_number) const override;
 
+  /// \param block_number: a block number
+  /// \return the source lines of the given block
+  const source_linest &source_lines_of(std::size_t block_number) const override;
+
   /// Outputs the list of blocks
   void output(std::ostream &out) const override;
 };

src/goto-instrument/cover_instrument_location.cpp

@@ -31,15 +31,15 @@ void cover_location_instrumentert::instrument(
   {
     const std::string b = std::to_string(block_nr + 1); // start with 1
     const std::string id = id2string(function_id) + "#" + b;
-    const auto source_location = basic_blocks.source_location_of(block_nr);
+    auto source_location = basic_blocks.source_location_of(block_nr);
 
     // filter goals
     if(goal_filters(source_location))
     {
-      const std::string source_lines =
-        id2string(source_location.get_basic_block_source_lines());
+      const auto &source_lines = basic_blocks.source_lines_of(block_nr);
       const std::string comment =
-        "block " + b + " (lines " + source_lines + ")";
+        "block " + b + " (lines " + source_lines.to_string() + ")";
+      source_location.set_basic_block_source_lines(source_lines.to_string());
       goto_program.insert_before_swap(i_it);
       *i_it = make_assertion(false_exprt(), source_location);
       initialize_source_location(i_it, comment, function_id);

src/goto-programs/show_properties.cpp

@@ -133,9 +133,9 @@ void convert_properties_json(
       {"expression",
        json_stringt(from_expr(ns, identifier, ins.get_condition()))}};
 
-    if(!source_location.get_basic_block_covered_lines().empty())
+    if(!source_location.get_basic_block_source_lines().empty())
       json_property["coveredLines"] =
-        json_stringt(source_location.get_basic_block_covered_lines());
+        json_stringt(source_location.get_basic_block_source_lines());
 
     json_properties.push_back(std::move(json_property));
   }

src/util/irep_ids.def

@@ -642,7 +642,6 @@ IREP_ID_ONE(cprover_string_to_lower_case_func)
 IREP_ID_ONE(cprover_string_to_upper_case_func)
 IREP_ID_ONE(cprover_string_trim_func)
 IREP_ID_ONE(skip_initialize)
-IREP_ID_ONE(basic_block_covered_lines)
 IREP_ID_ONE(basic_block_source_lines)
 IREP_ID_ONE(is_nondet_nullable)
 IREP_ID_ONE(array_replace)

src/util/source_location.h

@@ -82,11 +82,6 @@ class source_locationt:public irept
     return get(ID_java_bytecode_index);
   }
 
-  const irep_idt &get_basic_block_covered_lines() const
-  {
-    return get(ID_basic_block_covered_lines);
-  }
-
   const irep_idt &get_basic_block_source_lines() const
   {
     return get(ID_basic_block_source_lines);
@@ -153,11 +148,6 @@ class source_locationt:public irept
     set(ID_java_bytecode_index, index);
   }
 
-  void set_basic_block_covered_lines(const irep_idt &covered_lines)
-  {
-    return set(ID_basic_block_covered_lines, covered_lines);
-  }
-
   void set_basic_block_source_lines(const irep_idt &source_lines)
   {
     return set(ID_basic_block_source_lines, source_lines);