cprover
symex_coverage.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Record and print code coverage of symbolic execution
4
5Author: Michael Tautschnig
6
7Date: March 2016
8
9\*******************************************************************/
10
13
14#include "symex_coverage.h"
15
16#include <chrono>
17#include <ctime>
18#include <fstream>
19#include <iostream>
20
21#include <util/string2int.h>
22#include <util/symbol.h>
23#include <util/xml.h>
24
26
28
30
32{
33public:
34 explicit coverage_recordt(const std::string &node_id)
35 : xml(node_id),
37 lines_total(0),
40 {
41 }
42
44 std::size_t lines_covered;
45 std::size_t lines_total;
46 std::size_t branches_covered;
47 std::size_t branches_total;
48};
49
51{
52public:
54 const namespacet &ns,
55 const irep_idt &function_id,
56 const goto_programt &goto_program,
57 const symex_coveraget::coveraget &coverage);
58
59 const irep_idt &get_file() const
60 {
61 return file_name;
62 }
63
64protected:
66
68 {
70 {
71 }
72
75 };
76
78 {
80 {
81 }
82
83 unsigned hits;
84 std::map<goto_programt::const_targett, coverage_conditiont> conditions;
85 };
86
87 typedef std::map<unsigned, coverage_linet> coverage_lines_mapt;
88
90 const goto_programt &goto_program,
91 const symex_coveraget::coveraget &coverage,
93};
94
95static std::string
96rate(std::size_t covered, std::size_t total, bool per_cent = false)
97{
98 std::ostringstream oss;
99
100#if 1
101 float fraction;
102
103 if(total == 0)
104 fraction = 1.0;
105 else
106 fraction = static_cast<float>(covered) / static_cast<float>(total);
107
108 if(per_cent)
109 oss << fraction * 100.0 << '%';
110 else
111 oss << fraction;
112#else
113 oss << covered << " of " << total;
114#endif
115
116 return oss.str();
117}
118
119static std::string
120rate_detailed(std::size_t covered, std::size_t total, bool per_cent = false)
121{
122 std::ostringstream oss;
123 oss << rate(covered, total, per_cent) << " (" << covered << '/' << total
124 << ')';
125 return oss.str();
126}
127
129 const namespacet &ns,
130 const irep_idt &function_id,
131 const goto_programt &goto_program,
132 const symex_coveraget::coveraget &coverage)
133 : coverage_recordt("method")
134{
135 PRECONDITION(!goto_program.instructions.empty());
136
137 // identify the file name, inlined functions aren't properly
138 // accounted for
139 goto_programt::const_targett end_function = --goto_program.instructions.end();
141 end_function->is_end_function(),
142 "last instruction in a function body is end function");
143 file_name = end_function->source_location().get_file();
144 DATA_INVARIANT(!file_name.empty(), "should have a valid source location");
145
146 // compute the maximum coverage of individual source-code lines
147 coverage_lines_mapt coverage_lines_map;
148 compute_coverage_lines(goto_program, coverage, coverage_lines_map);
149
150 // <method name="foo" signature="int(int)" line-rate="1.0" branch-rate="1.0">
151 // <lines>
152 // <line number="23" hits="1" branch="false"/>
153 // <line number="24" hits="1" branch="false"/>
154 // <line number="25" hits="1" branch="false"/>
155 // <line number="26" hits="1" branch="false"/>
156 // <line number="27" hits="1" branch="false"/>
157 // <line number="28" hits="1" branch="false"/>
158 // <line number="29" hits="1" branch="false"/>
159 // <line number="30" hits="1" branch="false"/>
160 // </lines>
161 // </method>
162 xml.set_attribute("name", id2string(function_id));
163
165 "signature", from_type(ns, function_id, ns.lookup(function_id).type));
166
169
170 xmlt &lines = xml.new_element("lines");
171
172 for(const auto &cov_line : coverage_lines_map)
173 {
174 xmlt &line = lines.new_element("line");
175
176 line.set_attribute("number", std::to_string(cov_line.first));
177 line.set_attribute("hits", std::to_string(cov_line.second.hits));
178 if(cov_line.second.conditions.empty())
179 line.set_attribute("branch", "false");
180 else
181 {
182 line.set_attribute("branch", "true");
183
184 xmlt &conditions = line.new_element("conditions");
185
186 std::size_t number = 0, total_taken = 0;
187 for(const auto &c : cov_line.second.conditions)
188 {
189 // <condition number="0" type="jump" coverage="50%"/>
190 xmlt &condition = conditions.new_element("condition");
191 condition.set_attribute("number", std::to_string(number++));
192 condition.set_attribute("type", "jump");
193 unsigned taken = c.second.false_taken + c.second.true_taken;
194 total_taken += taken;
195 condition.set_attribute("coverage", rate(taken, 2, true));
196 }
197
198 line.set_attribute(
199 "condition-coverage", rate_detailed(total_taken, number * 2, true));
200 }
201 }
202}
203
205 const goto_programt &goto_program,
206 const symex_coveraget::coveraget &coverage,
208{
209 forall_goto_program_instructions(it, goto_program)
210 {
211 if(
212 it->source_location().is_nil() ||
213 it->source_location().get_file() != file_name || it->is_dead() ||
214 it->is_end_function())
215 continue;
216
217 const bool is_branch = it->is_goto() && !it->guard.is_constant();
218
219 unsigned l =
220 safe_string2unsigned(id2string(it->source_location().get_line()));
221 std::pair<coverage_lines_mapt::iterator, bool> entry =
222 dest.insert(std::make_pair(l, coverage_linet()));
223
224 if(entry.second)
225 ++lines_total;
226
227 // mark as branch if any instruction in this source code line is
228 // a branching instruction
229 if(is_branch)
230 {
231 branches_total += 2;
232 if(!entry.first->second.conditions.insert({it, coverage_conditiont()})
233 .second)
235 }
236
237 symex_coveraget::coveraget::const_iterator c_entry = coverage.find(it);
238 if(c_entry != coverage.end())
239 {
240 if(!(c_entry->second.size() == 1 || is_branch))
241 {
242 std::cerr << it->location_number << '\n';
243 for(const auto &cov : c_entry->second)
244 std::cerr << cov.second.succ->location_number << '\n';
245 }
247 c_entry->second.size() == 1 || is_branch,
248 "instructions other than branch instructions have exactly 1 successor");
249
250 for(const auto &cov : c_entry->second)
251 {
253 cov.second.num_executions > 0,
254 "coverage entries can only exist with at least one execution");
255
256 if(entry.first->second.hits == 0)
258
259 if(cov.second.num_executions > entry.first->second.hits)
260 entry.first->second.hits = cov.second.num_executions;
261
262 if(is_branch)
263 {
264 auto cond_entry = entry.first->second.conditions.find(it);
265 INVARIANT(
266 cond_entry != entry.first->second.conditions.end(),
267 "branch should have condition");
268
269 if(it->get_target() == cov.second.succ)
270 {
271 if(!cond_entry->second.false_taken)
272 {
273 cond_entry->second.false_taken = true;
275 }
276 }
277 else
278 {
279 if(!cond_entry->second.true_taken)
280 {
281 cond_entry->second.true_taken = true;
283 }
284 }
285 }
286 }
287 }
288 }
289}
290
292 const goto_functionst &goto_functions,
293 coverage_recordt &dest) const
294{
295 typedef std::map<irep_idt, coverage_recordt> file_recordst;
296 file_recordst file_records;
297
298 for(const auto &gf_entry : goto_functions.function_map)
299 {
300 if(
301 !gf_entry.second.body_available() ||
302 gf_entry.first == goto_functions.entry_point() ||
303 gf_entry.first == INITIALIZE_FUNCTION)
304 {
305 continue;
306 }
307
309 ns, gf_entry.first, gf_entry.second.body, coverage);
310
311 std::pair<file_recordst::iterator, bool> entry = file_records.insert(
312 std::make_pair(func_cov.get_file(), coverage_recordt("class")));
313 coverage_recordt &file_record = entry.first->second;
314
315 if(entry.second)
316 {
317 file_record.xml.new_element("methods");
318 file_record.xml.new_element("lines");
319 }
320
321 // copy the "method" node
322 file_record.xml.elements.front().new_element(func_cov.xml);
323
324 // copy any lines
325 for(xmlt::elementst::const_iterator it =
326 func_cov.xml.elements.front().elements.begin();
327 it != func_cov.xml.elements.front().elements.end();
328 ++it)
329 file_record.xml.elements.back().new_element(*it);
330
331 // merge line/branch info
332 file_record.lines_covered += func_cov.lines_covered;
333 file_record.lines_total += func_cov.lines_total;
334 file_record.branches_covered += func_cov.branches_covered;
335 file_record.branches_total += func_cov.branches_total;
336 }
337
338 xmlt &classes = dest.xml.new_element("classes");
339
340 // <class name="MyProject.GameRules" filename="MyProject/GameRules.java"
341 // line-rate="1.0" branch-rate="1.0" complexity="1.4">
342 for(file_recordst::const_iterator it = file_records.begin();
343 it != file_records.end();
344 ++it)
345 {
347 continue;
348
349 const coverage_recordt &f_cov = it->second;
350
351 xmlt &class_xml = classes.new_element(f_cov.xml);
352 class_xml.set_attribute("name", id2string(it->first));
353 class_xml.set_attribute("filename", id2string(it->first));
354 class_xml.set_attribute(
355 "line-rate", rate(f_cov.lines_covered, f_cov.lines_total));
356 class_xml.set_attribute(
357 "branch-rate", rate(f_cov.branches_covered, f_cov.branches_total));
358 class_xml.set_attribute("complexity", "0.0");
359
360 // merge line/branch info
361 dest.lines_covered += f_cov.lines_covered;
362 dest.lines_total += f_cov.lines_total;
364 dest.branches_total += f_cov.branches_total;
365 }
366}
367
369 const goto_functionst &goto_functions,
370 xmlt &xml_coverage) const
371{
372 coverage_recordt overall_cov("package");
373 compute_overall_coverage(goto_functions, overall_cov);
374
375 std::string overall_line_rate_str =
376 rate(overall_cov.lines_covered, overall_cov.lines_total);
377 std::string overall_branch_rate_str =
378 rate(overall_cov.branches_covered, overall_cov.branches_total);
379
380 auto now = std::chrono::system_clock::now();
381 auto current_time = std::chrono::time_point_cast<std::chrono::seconds>(now);
382 std::time_t tt = std::chrono::system_clock::to_time_t(current_time);
383
384 // <coverage line-rate="0.0" branch-rate="0.0" lines-covered="1"
385 // lines-valid="1" branches-covered="1"
386 // branches-valid="1" complexity="0.0"
387 // version="2.1.1" timestamp="0">
388 xml_coverage.set_attribute("line-rate", overall_line_rate_str);
389 xml_coverage.set_attribute("branch-rate", overall_branch_rate_str);
390 xml_coverage.set_attribute(
391 "lines-covered", std::to_string(overall_cov.lines_covered));
392 xml_coverage.set_attribute(
393 "lines-valid", std::to_string(overall_cov.lines_total));
394 xml_coverage.set_attribute(
395 "branches-covered", std::to_string(overall_cov.branches_covered));
396 xml_coverage.set_attribute(
397 "branches-valid", std::to_string(overall_cov.branches_total));
398 xml_coverage.set_attribute("complexity", "0.0");
399 xml_coverage.set_attribute("version", "2.1.1");
400 xml_coverage.set_attribute("timestamp", std::to_string(tt));
401
402 xmlt &packages = xml_coverage.new_element("packages");
403
404 // <package name="" line-rate="0.0" branch-rate="0.0" complexity="0.0">
405 xmlt &package = packages.new_element(overall_cov.xml);
406 package.set_attribute("name", "");
407 package.set_attribute("line-rate", overall_line_rate_str);
408 package.set_attribute("branch-rate", overall_branch_rate_str);
409 package.set_attribute("complexity", "0.0");
410}
411
413 const goto_functionst &goto_functions,
414 std::ostream &os) const
415{
416 xmlt xml_coverage("coverage");
417 build_cobertura(goto_functions, xml_coverage);
418
419 os << "<?xml version=\"1.0\"?>\n";
420 os << "<!DOCTYPE coverage SYSTEM \""
421 << "http://cobertura.sourceforge.net/xml/coverage-04.dtd\">\n";
422 os << xml_coverage;
423
424 return !os.good();
425}
426
428 const goto_functionst &goto_functions,
429 const std::string &path) const
430{
431 PRECONDITION(!path.empty());
432
433 if(path == "-")
434 return output_report(goto_functions, std::cout);
435 else
436 {
437 std::ofstream out(path.c_str());
438 return output_report(goto_functions, out);
439 }
440}
std::size_t lines_covered
std::size_t branches_total
std::size_t lines_total
std::size_t branches_covered
coverage_recordt(const std::string &node_id)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
A collection of goto functions.
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void compute_coverage_lines(const goto_programt &goto_program, const symex_coveraget::coveraget &coverage, coverage_lines_mapt &dest)
const irep_idt & get_file() const
std::map< unsigned, coverage_linet > coverage_lines_mapt
goto_program_coverage_recordt(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, const symex_coveraget::coveraget &coverage)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
instructionst::const_iterator const_targett
Definition: goto_program.h:593
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
bool is_built_in() const
void compute_overall_coverage(const goto_functionst &goto_functions, coverage_recordt &dest) const
bool generate_report(const goto_functionst &goto_functions, const std::string &path) const
std::map< goto_programt::const_targett, coverage_innert > coveraget
bool output_report(const goto_functionst &goto_functions, std::ostream &os) const
void build_cobertura(const goto_functionst &goto_functions, xmlt &xml_coverage) const
const namespacet & ns
coveraget coverage
Definition: xml.h:21
xmlt & new_element(const std::string &key)
Definition: xml.h:95
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:198
elementst elements
Definition: xml.h:42
Goto Programs with Functions.
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INITIALIZE_FUNCTION
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:16
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::map< goto_programt::const_targett, coverage_conditiont > conditions
Symbol table entry.
static std::string rate(std::size_t covered, std::size_t total, bool per_cent=false)
static std::string rate_detailed(std::size_t covered, std::size_t total, bool per_cent=false)
Record and print code coverage of symbolic execution.