Store and report basic block source lines as a structure

tautschnig · tautschnig · commit 691f5e8a1988 · 2022-05-02T20:00:39.000Z
Do not serialise the information to a string early on, but instead leave
this to the user interface. This will make it possible to further
process the information in CBMC Viewer even when function identifiers
also contain semicolons, as is the case with Kani.
diff --git a/doc/assets/xml_spec.xsd b/doc/assets/xml_spec.xsd
@@ -173,6 +173,37 @@
     </xs:complexType>
   </xs:element>
 
+  <xs:element name="line">
+    <xs:complexType>
+      <xs:simpleContent>
+        <xs:extension base="xs:string">
+          <xs:attribute name="file" type="xs:string"/>
+          <xs:attribute name="function" type="xs:string"/>
+        </xs:extension>
+      </xs:simpleContent>
+    </xs:complexType>
+  </xs:element>
+
+  <xs:element name="basic_block_lines">
+    <xs:complexType>
+      <xs:sequence>
+        <xs:element ref="line" minOccurs="0"/>
+      </xs:sequence>
+    </xs:complexType>
+  </xs:element>
+
+  <xs:element name="goal">
+    <xs:complexType>
+      <xs:sequence>
+        <xs:element ref="location" minOccurs="0"/>
+        <xs:element ref="basic_block_lines" minOccurs="0"/>
+      </xs:sequence>
+      <xs:attribute name="description" type="xs:string"/>
+      <xs:attribute name="id" type="xs:string"/>
+      <xs:attribute name="status" type="xs:string"/>
+    </xs:complexType>
+  </xs:element>
+
   <xs:element name="message">
     <xs:complexType>
       <xs:sequence>
@@ -217,6 +248,7 @@
         <xs:element ref="result"/>
         <xs:element ref="refinement-iteration"/>
         <xs:element ref="fault-localization"/>
+        <xs:element ref="goal"/>
        </xs:choice>
       <xs:element ref="cprover-status" minOccurs="0"/>
       </xs:sequence>
diff --git a/jbmc/regression/jdiff/java-properties/test.desc b/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": "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  
+  "deletedFunctions": \[\n      \{\n        "name": "java::Test.obsolete:\(\)V",\n        "properties": \[\n          \{\n            "basicBlockLines": \{\n              "Test.java": \{\n                "java::Test.obsolete:\(\)V": "18"\n              \}\n            \},\n            "class": "coverage",\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            "basicBlockLines": \{\n              "Test.java": \{\n                "java::Test.<init>:\(\)V": "6"\n              \}\n            \},\n            "class": "coverage",\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            "basicBlockLines": \{\n              "Test.java": \{\n                "java::Test.<init>:\(\)V": "4"\n              \}\n            \},\n            "class": "coverage",\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            "basicBlockLines": \{\n              "Test.java": \{\n                "java::Test.<init>:\(\)V": "4"\n              \}\n            \},\n            "class": "coverage",\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            "basicBlockLines": \{\n              "Test.java": \{\n                "java::Test.<init>:\(\)V": "4"\n              \}\n            \},\n            "class": "coverage",\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            "basicBlockLines": \{\n              "Test.java": \{\n                "java::Test.<init>:\(\)V": "7"\n              \}\n            \},\n            "class": "coverage",\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            "basicBlockLines": \{\n              "Test.java": \{\n                "java::Test.<clinit>:\(\)V": "3"\n              \}\n            \},\n            "class": "coverage",\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            "basicBlockLines": \{\n              "Test.java": \{\n                "java::Test.newfun:\(\)V": "18"\n              \}\n            \},\n            "class": "coverage",\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
diff --git a/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp b/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_source_lines().empty());
+              REQUIRE_FALSE(loc.get_basic_block_source_lines().is_nil());
             }
             else
             {
               // there is no line coverage goal in the middle of a block
-              REQUIRE(loc.get_basic_block_source_lines().empty());
+              REQUIRE(loc.get_basic_block_source_lines().is_nil());
             }
 
             ++it;
diff --git a/regression/cbmc-cover/json-goals1/test.desc b/regression/cbmc-cover/json-goals1/test.desc
@@ -4,6 +4,6 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-\{\n\s*"goals": \[\n\s*\{\n\s*"description": ".*",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"description": ".*",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"description": ".*",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"description": ".*",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\}\n\s*\],\n\s*"goalsCovered": 4,\n\s*"totalGoals": 4\n\s*\}
+\{\n\s*"goals": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\}\n\s*\],\n\s*"goalsCovered": 4,\n\s*"totalGoals": 4\n\s*\}
 --
 ^warning: ignoring
diff --git a/src/goto-checker/cover_goals_report_util.cpp b/src/goto-checker/cover_goals_report_util.cpp
@@ -75,9 +75,30 @@ static void output_goals_xml(const propertiest &properties, messaget &log)
                                                               : "FAILED"}},
       {});
 
-    if(property_pair.second.pc->source_location().is_not_nil())
-      xml_result.new_element() =
-        xml(property_pair.second.pc->source_location());
+    const auto &source_location = property_pair.second.pc->source_location();
+    if(source_location.is_not_nil())
+    {
+      xml_result.new_element() = xml(source_location);
+
+      const irept &basic_block_lines =
+        source_location.get_basic_block_source_lines();
+      if(basic_block_lines.is_not_nil())
+      {
+        xmlt basic_block_lines_xml{"basic_block_lines"};
+        for(const auto &file_entry : basic_block_lines.get_named_sub())
+        {
+          for(const auto &lines_entry : file_entry.second.get_named_sub())
+          {
+            xmlt line{"line"};
+            line.set_attribute("file", id2string(file_entry.first));
+            line.set_attribute("function", id2string(lines_entry.first));
+            line.data = id2string(lines_entry.second.id());
+            basic_block_lines_xml.new_element(line);
+          }
+        }
+        xml_result.new_element(basic_block_lines_xml);
+      }
+    }
 
     log.result() << xml_result;
   }
@@ -103,8 +124,29 @@ static void output_goals_json(
     json_goal["goal"] = json_stringt(property_pair.first);
     json_goal["description"] = json_stringt(property_info.description);
 
-    if(property_info.pc->source_location().is_not_nil())
-      json_goal["sourceLocation"] = json(property_info.pc->source_location());
+    const auto &source_location = property_info.pc->source_location();
+    if(source_location.is_not_nil())
+    {
+      json_goal["sourceLocation"] = json(source_location);
+
+      const irept &basic_block_lines =
+        source_location.get_basic_block_source_lines();
+      if(basic_block_lines.is_not_nil())
+      {
+        json_objectt basic_block_lines_json;
+        for(const auto &file_entry : basic_block_lines.get_named_sub())
+        {
+          json_objectt file_lines_json;
+          for(const auto &lines_entry : file_entry.second.get_named_sub())
+          {
+            file_lines_json[id2string(lines_entry.first)] =
+              json_stringt{lines_entry.second.id()};
+          }
+          basic_block_lines_json[id2string(file_entry.first)] = file_lines_json;
+        }
+        json_goal["basicBlockLines"] = basic_block_lines_json;
+      }
+    }
 
     goals_array.push_back(std::move(json_goal));
   }
diff --git a/src/goto-instrument/cover_instrument_location.cpp b/src/goto-instrument/cover_instrument_location.cpp
@@ -39,7 +39,7 @@ void cover_location_instrumentert::instrument(
       const auto &source_lines = basic_blocks.source_lines_of(block_nr);
       const std::string comment =
         "block " + b + " (lines " + source_lines.to_string() + ")";
-      source_location.set_basic_block_source_lines(source_lines.to_string());
+      source_location.set_basic_block_source_lines(source_lines.to_irep());
       goto_program.insert_before_swap(i_it);
       *i_it = make_assertion(false_exprt(), source_location);
       initialize_source_location(i_it, comment, function_id);
diff --git a/src/goto-instrument/source_lines.cpp b/src/goto-instrument/source_lines.cpp
@@ -32,18 +32,45 @@ void source_linest::insert(const source_locationt &loc)
     return;
   std::size_t line = safe_string2size_t(id2string(loc.get_line()));
 
-  block_lines[file + ":" + func].insert(line);
+  block_lines[file][func].insert(line);
 }
 
 std::string source_linest::to_string() const
 {
-  std::stringstream ss;
-  const auto map =
-    make_range(block_lines).map([&](const block_linest::value_type &pair) {
+  std::stringstream result;
+  const auto full_map =
+    make_range(block_lines)
+      .map([&](const block_linest::value_type &file_entry) {
+        std::stringstream ss;
+        const auto map = make_range(file_entry.second)
+                           .map([&](const function_linest::value_type &pair) {
+                             std::vector<unsigned> line_numbers(
+                               pair.second.begin(), pair.second.end());
+                             return file_entry.first + ':' + pair.first + ':' +
+                                    format_number_range(line_numbers);
+                           });
+        join_strings(ss, map.begin(), map.end(), "; ");
+        return ss.str();
+      });
+  join_strings(result, full_map.begin(), full_map.end(), "; ");
+  return result.str();
+}
+
+irept source_linest::to_irep() const
+{
+  irept result;
+
+  for(const auto &file_entry : block_lines)
+  {
+    irept file_result;
+    for(const auto &lines_entry : file_entry.second)
+    {
       std::vector<unsigned> line_numbers(
-        pair.second.begin(), pair.second.end());
-      return pair.first + ':' + format_number_range(line_numbers);
-    });
-  join_strings(ss, map.begin(), map.end(), "; ");
-  return ss.str();
+        lines_entry.second.begin(), lines_entry.second.end());
+      file_result.set(lines_entry.first, format_number_range(line_numbers));
+    }
+    result.add(file_entry.first, std::move(file_result));
+  }
+
+  return result;
 }
diff --git a/src/goto-instrument/source_lines.h b/src/goto-instrument/source_lines.h
diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp
diff --git a/src/util/source_location.h b/src/util/source_location.h

Original file line number	Diff line number	Diff line change
`@@ -159,12 +159,12 @@ SCENARIO(`
`159`	`159`	`// instruction with a new bytecode index begins with ASSERT`
`160`	`160`	`REQUIRE(it->type() == goto_program_instruction_typet::ASSERT);`
`161`	`161`	`// the assertion corresponds to a line coverage goal`
`162`		`- REQUIRE_FALSE(loc.get_basic_block_source_lines().empty());`
	`162`	`+ REQUIRE_FALSE(loc.get_basic_block_source_lines().is_nil());`
`163`	`163`	`}`
`164`	`164`	`else`
`165`	`165`	`{`
`166`	`166`	`// there is no line coverage goal in the middle of a block`
`167`		`- REQUIRE(loc.get_basic_block_source_lines().empty());`
	`167`	`+ REQUIRE(loc.get_basic_block_source_lines().is_nil());`
`168`	`168`	`}`
`169`	`169`
`170`	`170`	`++it;`