Block coverage now reports all source code lines contributing to a ba… #1439
Conversation
|
@kroening @peterschrammel @thk123 @rjmunro @lucasccordeiro My pull request is breaking appveyor and travis because I'm breaking some of your regression tests. My pull request changes the behavior of "cbmc --cover location" to output the file names and line numbers of all source code lines contributing to a basic block. The original behavior was to output just the line number of the first line in the basic block. This information is being output in the description field. Should I change the cbmc-cover regression tests to be consistent with my output? Should I add a flag to cbmc that causes cbmc to output my behavior instead of the original behavior. |
|
@markrtuttle, a few side questions to see what is the desired solution to this problem:
|
|
@peterschrammel, I'm sorry for my delay, I'm traveling... I wrote a tool I'd like to contribute to cbmc that annotates source code with coverage information similar to gcov, links symbols in the source code to definitions similar to any code browser, but most interesting lists and links errors to source code lines and links error traces to source code lines to make it easy to single-step through a trace and triage a result. It is all a bunch of html that I can view in a browser. I need to know the source code lines that contribute to a goto program basic block so I can annotate them appropriately. The mapping from goto basic blocks to source code lines does not seem obvious (it seems hard to guess where goto programs insert goto) and the goto program has basic blocks attributed to a line that don't come from the source code (eg, the goto program seems to have code to return unconstrained values when a function with a return value runs off the bottom of the function). I can't tell from the code how the "description" field in the xml listing the first line number of the basic block is intended to be used. I was just elaborating that field with the file and line number of each line contributing to the basic block. For the code I'm looking at, simply turning off the inlining (or doing the inlining later) wouldn't solve the problem of basic blocks coming from multiple files. For example, the header file for a device might include a multi-line definition of code for accessing the device. The source locations from that code point to the header file and not the target source file. One could get the same effect with defining a function and inlining it, but that is not what the source code is doing. |
|
@markrtuttle
when you look at the output of CBMC with the options
```
--json-ui --show-properties --cover location
```
you will get an output that gives the covered lines for each basic
block. Maybe that is already sufficient for you?
for example
```
class long_block {
int f(int n) {
if(n>=0) {
int x=n;
int y=n*2;
int z = x + y;
y=z+z;
x=y+n+z;
return x;
}
else
return 0;
}
}
```
gives (I removed the implicit constructor)
```
{
"properties": [
{
"class": "coverage",
"coveredLines": "4",
"description": "block 1",
"expression": "false",
"name": "java::long_block.f:(I)I.coverage.1",
"sourceLocation": {
"bytecodeIndex": "1",
"file": "long_block.java",
"function": "java::long_block.f:(I)I",
"line": "4"
}
},
{
"class": "coverage",
"coveredLines": "5-10",
"description": "block 2",
"expression": "false",
"name": "java::long_block.f:(I)I.coverage.2",
"sourceLocation": {
"bytecodeIndex": "3",
"file": "long_block.java",
"function": "java::long_block.f:(I)I",
"line": "5"
}
},
{
"class": "coverage",
"coveredLines": "13",
"description": "block 3",
"expression": "false",
"name": "java::long_block.f:(I)I.coverage.3",
"sourceLocation": {
"bytecodeIndex": "25",
"file": "long_block.java",
"function": "java::long_block.f:(I)I",
"line": "13"
}
}
]
}
```
|
|
Thanks, I'll take a look, but does this handle multiple files contributing to a basic block? The code I saw (implementing line sets and formatting compact representations of line sets) did not appear to deal with source code lines from multiple files contributing to a single basic block of a goto program. In a previous comment you might have missed I wrote that, "For the code I'm looking at, simply turning off the inlining (or doing the inlining later) wouldn't solve the problem of basic blocks coming from multiple files. For example, the header file for a device might include a multi-line definition of code for accessing the device. The source locations from that code point to the header file and not the target source file. One could get the same effect with defining a function and inlining it, but that is not what the source code is doing." |
|
@mgudemann
Thanks, I'll take a look, but does this handle multiple files contributing to a basic block?
The code I saw (implementing line sets and formatting compact representations of line sets) did not appear to deal with source code lines from multiple files contributing to a single basic block of a goto program.
In a previous comment you might have missed I wrote that, "For the code I'm looking at, simply turning off the inlining (or doing the inlining later) wouldn't solve the problem of basic blocks coming from multiple files. For example, the header file for a device might include a multi-line definition of code for accessing the device. The source locations from that code point to the header file and not the target source file. One could get the same effect with defining a function and inlining it, but that is not what the source code is doing."
true, I didn't see that you are dealing with this situation. I don't
think the current implementation would handle this, it was not written
with this in mind.
|
|
An updated version of the patch is now PR'ed as #3967. |
Block coverage obtained with "cbmc --cover locations" now reports the file name and line number of every line of source code contributing to a basic block in the "description" field of the xml output. (The lines contributing to a block can come from multiple files via function inlining and definitions in include files, so reporting line numbers alone is not sufficient.)