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