From 4d656eb1dca86d646e46d6ae4d82b05e15f3af35 Mon Sep 17 00:00:00 2001 From: Tuttle Date: Mon, 25 Sep 2017 05:09:07 -0400 Subject: [PATCH] Block coverage now reports all source code lines contributing to a basic block. --- regression/cbmc/block-coverage-report1/main.c | 10 ++ .../cbmc/block-coverage-report1/test.desc | 9 ++ regression/cbmc/block-coverage-report2/main.c | 24 ++++ .../cbmc/block-coverage-report2/test.desc | 12 ++ regression/cbmc/block-coverage-report3/main.c | 6 + .../cbmc/block-coverage-report3/test.desc | 8 ++ regression/cbmc/block-coverage-report4/main.c | 6 + .../cbmc/block-coverage-report4/test.desc | 8 ++ src/goto-instrument/cover.cpp | 136 +++++++++++++++++- 9 files changed, 218 insertions(+), 1 deletion(-) create mode 100644 regression/cbmc/block-coverage-report1/main.c create mode 100644 regression/cbmc/block-coverage-report1/test.desc create mode 100644 regression/cbmc/block-coverage-report2/main.c create mode 100644 regression/cbmc/block-coverage-report2/test.desc create mode 100644 regression/cbmc/block-coverage-report3/main.c create mode 100644 regression/cbmc/block-coverage-report3/test.desc create mode 100644 regression/cbmc/block-coverage-report4/main.c create mode 100644 regression/cbmc/block-coverage-report4/test.desc diff --git a/regression/cbmc/block-coverage-report1/main.c b/regression/cbmc/block-coverage-report1/main.c new file mode 100644 index 00000000000..5325c7b456c --- /dev/null +++ b/regression/cbmc/block-coverage-report1/main.c @@ -0,0 +1,10 @@ +int main() { + + int x; + + if (x<0) + return 0; + else + return 1; + +} diff --git a/regression/cbmc/block-coverage-report1/test.desc b/regression/cbmc/block-coverage-report1/test.desc new file mode 100644 index 00000000000..81080e08cf8 --- /dev/null +++ b/regression/cbmc/block-coverage-report1/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--cover location +block 1 \(lines main.c:main:3,5\): SATISFIED +block 2 \(lines main.c:main:6\): SATISFIED +block 3 \(lines main.c:main:6,10\): FAILED +block 4 \(lines main.c:main:8\): SATISFIED +block 5 \(lines main.c:main:10\): SATISFIED +-- diff --git a/regression/cbmc/block-coverage-report2/main.c b/regression/cbmc/block-coverage-report2/main.c new file mode 100644 index 00000000000..1b653893a93 --- /dev/null +++ b/regression/cbmc/block-coverage-report2/main.c @@ -0,0 +1,24 @@ +// This is supposed to be testing basic blocks with inlining, +// but cbmc has now turned off inlining by default. + +inline int foo(int x) { + int y; + y = x+1; + return y; +} + +main() { + + int x; + x =10; + while (x) { + int y; + y = foo(x); + if (y < 5) + break; + x--; + } + + return; + +} diff --git a/regression/cbmc/block-coverage-report2/test.desc b/regression/cbmc/block-coverage-report2/test.desc new file mode 100644 index 00000000000..64deb7fd348 --- /dev/null +++ b/regression/cbmc/block-coverage-report2/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--cover location +block 1 \(lines main.c:main:12,13\): SATISFIED +block 2 \(lines main.c:main:14\): SATISFIED +block 3 \(lines main.c:main:15,16\): SATISFIED +block 4 \(lines main.c:main:16,17\): SATISFIED +block 5 \(lines main.c:main:18\): SATISFIED +block 6 \(lines main.c:main:14,19,20\): SATISFIED +block 7 \(lines main.c:main:22,24\): SATISFIED +block 1 \(lines main.c:foo:5,6,7,8\): SATISFIED +-- diff --git a/regression/cbmc/block-coverage-report3/main.c b/regression/cbmc/block-coverage-report3/main.c new file mode 100644 index 00000000000..a7301199852 --- /dev/null +++ b/regression/cbmc/block-coverage-report3/main.c @@ -0,0 +1,6 @@ +void main() { + int x = 0; + while (x < 3) { + x++; + } +} diff --git a/regression/cbmc/block-coverage-report3/test.desc b/regression/cbmc/block-coverage-report3/test.desc new file mode 100644 index 00000000000..0aa40b6ae9b --- /dev/null +++ b/regression/cbmc/block-coverage-report3/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--cover location --unwind 1 +block 1 \(lines main.c:main:2\): SATISFIED +block 2 \(lines main.c:main:3\): SATISFIED +block 3 \(lines main.c:main:3,4\): SATISFIED +block 4 \(lines main.c:main:6\): FAILED +-- diff --git a/regression/cbmc/block-coverage-report4/main.c b/regression/cbmc/block-coverage-report4/main.c new file mode 100644 index 00000000000..a7301199852 --- /dev/null +++ b/regression/cbmc/block-coverage-report4/main.c @@ -0,0 +1,6 @@ +void main() { + int x = 0; + while (x < 3) { + x++; + } +} diff --git a/regression/cbmc/block-coverage-report4/test.desc b/regression/cbmc/block-coverage-report4/test.desc new file mode 100644 index 00000000000..f7fcde05814 --- /dev/null +++ b/regression/cbmc/block-coverage-report4/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--cover location --unwind 4 +block 1 \(lines main.c:main:2\): SATISFIED +block 2 \(lines main.c:main:3\): SATISFIED +block 3 \(lines main.c:main:3,4\): SATISFIED +block 4 \(lines main.c:main:6\): SATISFIED +-- diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index d76afe03b71..c232364a23a 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -18,6 +18,7 @@ Date: May 2016 #include #include #include +#include #include #include @@ -30,6 +31,122 @@ Date: May 2016 namespace { +/// The lines of source code contribuing to a basic block. +/// +/// Represent a line of source code by a file name and line number. +/// One line of source code may contribute to many basic blocks of a +/// goto program. +/// +/// The lines contributing to a basic block: A basic block is +/// generally a sequence of consecutive instructions ending with a +/// goto. Exceptions: (1) The block will not continue past an +/// instruction that is itself the target of a goto (so a block may +/// not end with a goto). (2) The block will continue past an +/// unconditional goto (a goto with guard true) to the target of that +/// goto if that target is reachable only by that goto (so the +/// instructions may not be consecutive). +/// +/// The files contributing to a basic block: The lines contributing to a +/// block can come from multiple files via function inlining and +/// definitions in include files. +class source_linest +{ +public: + /// A set of source code line numbers from a single a function + typedef std::set linest; + /// A set of source code line numbers from multiple functions + /// (represented by a mapping from a string "file:function" to a set + /// of line numbers from that function in that file). + typedef std::map block_linest; + block_linest block_lines; + + /// Insert a source code line number given by a source location into + /// the set of source code line numbers. + /// + /// @param loc is a source location + void insert(source_locationt const &loc) + { + if(loc.get_file().empty() || loc.is_built_in()) + return; + std::string file=id2string(loc.get_file()); + + if(loc.get_function().empty()) + return; + std::string func=id2string(loc.get_function()); + + if(loc.get_line().empty()) + return; + unsigned int line=safe_string2unsigned(id2string(loc.get_line())); + + block_lines[file+":"+func].insert(line); + } + + /// Print a list of objects to a stream separated by a delimeter. + /// + /// @param os is an output stream + /// @param start is an iterator pointing to the first object + /// @param end is an iterator pointing past the last object + /// @param delim is a string to use as the separating delimeter + template + void to_stream(std::ostream &os, + Iter start, + Iter end, + std::string const &delim) const + { + if(start==end) + return; + + to_stream(os, *start++); + while(start!=end) { os << delim; to_stream(os, *start++); } + } + + /// A string representing the lines of source code in a goto basic block. + /// + /// A source code line is represented by a triple + /// "file:function:line" for a given line in a given function in a + /// given file. Triples are ordered by sorting lexicographically. + /// Triples from the same function are grouped (collapsed) into a + /// single triple "file:function:n1,n2,n3,n4" where n1, n2, n3, n4 + /// are line numbers in ascending order. Triples are separated by a + /// semicolon. Blocks are usually so small that collapsing consecutive + /// integers into a group n1-n4 is not worth the effort. + /// + /// @return The string representing the lines of source code in a + /// goto basic block. + std::string to_string() const + { + std::stringstream ss; + to_stream(ss, block_lines); + return ss.str(); + } + + /// Print "file:function:lineset" separated by ";" to a stream + void to_stream(std::ostream &os, block_linest const &block_lines) const + { + to_stream(os, block_lines.cbegin(), block_lines.cend(), "; "); + } + + /// Print "file:function" and "lineset" separated by ":" to a stream + void to_stream(std::ostream &os, std::pair const &pair) + const + { + os << pair.first << ":"; + to_stream(os, pair.second); + } + + /// Print line numbers separated by "," to a stream + void to_stream(std::ostream &os, linest const &lines) const + { + to_stream(os, lines.cbegin(), lines.cend(), ","); + } + + /// Print line number to a stream + void to_stream(std::ostream &os, unsigned int const line) const + { + os << line; + } +}; + class basic_blockst { public: @@ -78,7 +195,10 @@ class basic_blockst // update lines belonging to block const irep_idt &line=it->source_location.get_line(); if(!line.empty()) + { block_info.lines.insert(unsafe_string2unsigned(id2string(line))); + block_info.source_lines.insert(it->source_location); + } // set representative program location to instrument if(!it->source_location.is_nil() && @@ -132,6 +252,15 @@ class basic_blockst return block_infos.at(block_nr).source_location; } + /// \param block_nr a block number + /// \return the source lines contributing to the given block + const source_linest &source_lines_of( + unsigned block_nr) + { + INVARIANT(block_nr lines; + /// the set of lines belonging to this block with file names + source_linest source_lines; }; typedef std::vector block_infost; @@ -1330,7 +1461,10 @@ void instrument_cover_goals( !source_location.is_built_in() && cover_curr_function) { - std::string comment="block "+b; + std::string comment="block "+b + + " (lines " + + basic_blocks.source_lines_of(block_nr).to_string() + + ")"; const irep_idt function=i_it->function; goto_program.insert_before_swap(i_it); i_it->make_assertion(false_exprt());