Merge pull request #6839 from tautschnig/feature/block-coverage-lines

Report basic block lines in a reliably parseable form

Author: tautschnig

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>

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            "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

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().is_nil());
             }
             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().is_nil());
             }
 
             ++it;

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

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));
   }