cprover
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 <iostream>
17 #include <fstream>
18 #include <sstream>
19 
20 #include <util/time_stopping.h>
21 #include <util/xml.h>
22 #include <util/string2int.h>
23 #include <util/cprover_prefix.h>
24 #include <util/prefix.h>
25 
28 
30 {
31 public:
32  explicit coverage_recordt(const std::string &node_id):
33  xml(node_id),
34  lines_covered(0),
35  lines_total(0),
38  {
39  }
40 
42  std::size_t lines_covered;
43  std::size_t lines_total;
44  std::size_t branches_covered;
45  std::size_t branches_total;
46 };
47 
49 {
50 public:
52  const namespacet &ns,
53  goto_functionst::function_mapt::const_iterator gf_it,
54  const symex_coveraget::coveraget &coverage);
55 
56  const irep_idt &get_file() const
57  {
58  return file_name;
59  }
60 
61 protected:
63 
65  {
67  false_taken(false), true_taken(false)
68  {
69  }
70 
72  bool true_taken;
73  };
74 
76  {
78  hits(0)
79  {
80  }
81 
82  unsigned hits;
83  std::map<goto_programt::const_targett, coverage_conditiont>
85  };
86 
87  typedef std::map<unsigned, coverage_linet>
89 
90  void compute_coverage_lines(
91  const goto_programt &goto_program,
92  const irep_idt &file_name,
93  const symex_coveraget::coveraget &coverage,
94  coverage_lines_mapt &dest);
95 };
96 
97 static std::string rate(
98  std::size_t covered,
99  std::size_t total,
100  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 rate_detailed(
124  std::size_t covered,
125  std::size_t total,
126  bool per_cent=false)
127 {
128  std::ostringstream oss;
129  oss << rate(covered, total, per_cent)
130  << " (" << covered << '/' << total << ')';
131  return oss.str();
132 }
133 
135  const namespacet &ns,
136  goto_functionst::function_mapt::const_iterator gf_it,
137  const symex_coveraget::coveraget &coverage):
138  coverage_recordt("method")
139 {
140  assert(gf_it->second.body_available());
141 
142  // identify the file name, inlined functions aren't properly
143  // accounted for
144  goto_programt::const_targett end_function=
145  --gf_it->second.body.instructions.end();
146  assert(end_function->is_end_function());
147  file_name=end_function->source_location.get_file();
148  assert(!file_name.empty());
149 
150  // compute the maximum coverage of individual source-code lines
151  coverage_lines_mapt coverage_lines_map;
153  gf_it->second.body,
154  file_name,
155  coverage,
156  coverage_lines_map);
157 
158  // <method name="foo" signature="int(int)" line-rate="1.0" branch-rate="1.0">
159  // <lines>
160  // <line number="23" hits="1" branch="false"/>
161  // <line number="24" hits="1" branch="false"/>
162  // <line number="25" hits="1" branch="false"/>
163  // <line number="26" hits="1" branch="false"/>
164  // <line number="27" hits="1" branch="false"/>
165  // <line number="28" hits="1" branch="false"/>
166  // <line number="29" hits="1" branch="false"/>
167  // <line number="30" hits="1" branch="false"/>
168  // </lines>
169  // </method>
170  xml.set_attribute("name", id2string(gf_it->first));
171 
172  code_typet sig_type=
173  original_return_type(ns.get_symbol_table(), gf_it->first);
174  if(sig_type.is_nil())
175  sig_type=gf_it->second.type;
176  xml.set_attribute("signature",
177  from_type(ns, gf_it->first, sig_type));
178 
179  xml.set_attribute("line-rate",
181  xml.set_attribute("branch-rate",
183 
184  xmlt &lines=xml.new_element("lines");
185 
186  for(const auto &cov_line : coverage_lines_map)
187  {
188  xmlt &line=lines.new_element("line");
189 
190  line.set_attribute("number", std::to_string(cov_line.first));
191  line.set_attribute("hits", std::to_string(cov_line.second.hits));
192  if(cov_line.second.conditions.empty())
193  line.set_attribute("branch", "false");
194  else
195  {
196  line.set_attribute("branch", "true");
197 
198  xmlt &conditions=line.new_element("conditions");
199 
200  std::size_t number=0, total_taken=0;
201  for(const auto &c : cov_line.second.conditions)
202  {
203  // <condition number="0" type="jump" coverage="50%"/>
204  xmlt &condition=conditions.new_element("condition");
205  condition.set_attribute("number", std::to_string(number++));
206  condition.set_attribute("type", "jump");
207  unsigned taken=c.second.false_taken+c.second.true_taken;
208  total_taken+=taken;
209  condition.set_attribute("coverage", rate(taken, 2, true));
210  }
211 
212  line.set_attribute(
213  "condition-coverage",
214  rate_detailed(total_taken, number*2, true));
215  }
216  }
217 }
218 
220  const goto_programt &goto_program,
221  const irep_idt &file_name,
222  const symex_coveraget::coveraget &coverage,
223  coverage_lines_mapt &dest)
224 {
225  forall_goto_program_instructions(it, goto_program)
226  {
227  if(it->source_location.is_nil() ||
228  it->source_location.get_file()!=file_name ||
229  it->is_dead() ||
230  it->is_end_function())
231  continue;
232 
233  const bool is_branch=it->is_goto() && !it->guard.is_constant();
234 
235  unsigned l=
236  safe_string2unsigned(id2string(it->source_location.get_line()));
237  std::pair<coverage_lines_mapt::iterator, bool> entry=
238  dest.insert(std::make_pair(l, coverage_linet()));
239 
240  if(entry.second)
241  ++lines_total;
242 
243  // mark as branch if any instruction in this source code line is
244  // a branching instruction
245  if(is_branch)
246  {
247  branches_total+=2;
248  if(!entry.first->second.conditions.insert(
249  {it, coverage_conditiont()}).second)
250  assert(false);
251  }
252 
253  symex_coveraget::coveraget::const_iterator c_entry=
254  coverage.find(it);
255  if(c_entry!=coverage.end())
256  {
257  if(!(c_entry->second.size()==1 || is_branch))
258  {
259  std::cerr << it->location_number << '\n';
260  for(const auto &cov : c_entry->second)
261  std::cerr << cov.second.succ->location_number << '\n';
262  }
263  assert(c_entry->second.size()==1 || is_branch);
264 
265  for(const auto &cov : c_entry->second)
266  {
267  assert(cov.second.num_executions>0);
268 
269  if(entry.first->second.hits==0)
270  ++lines_covered;
271 
272  if(cov.second.num_executions>entry.first->second.hits)
273  entry.first->second.hits=cov.second.num_executions;
274 
275  if(is_branch)
276  {
277  auto cond_entry=entry.first->second.conditions.find(it);
278  assert(cond_entry!=entry.first->second.conditions.end());
279 
280  if(it->get_target()==cov.second.succ)
281  {
282  if(!cond_entry->second.false_taken)
283  {
284  cond_entry->second.false_taken=true;
286  }
287  }
288  else
289  {
290  if(!cond_entry->second.true_taken)
291  {
292  cond_entry->second.true_taken=true;
294  }
295  }
296  }
297  }
298  }
299  }
300 }
301 
303  const goto_functionst &goto_functions,
304  coverage_recordt &dest) const
305 {
306  typedef std::map<irep_idt, coverage_recordt> file_recordst;
307  file_recordst file_records;
308 
309  forall_goto_functions(gf_it, goto_functions)
310  {
311  if(!gf_it->second.body_available() ||
312  gf_it->first==goto_functions.entry_point() ||
313  gf_it->first==CPROVER_PREFIX "initialize")
314  continue;
315 
316  goto_program_coverage_recordt func_cov(ns, gf_it, coverage);
317 
318  std::pair<file_recordst::iterator, bool> entry=
319  file_records.insert(std::make_pair(func_cov.get_file(),
320  coverage_recordt("class")));
321  coverage_recordt &file_record=entry.first->second;
322 
323  if(entry.second)
324  {
325  file_record.xml.new_element("methods");
326  file_record.xml.new_element("lines");
327  }
328 
329  // copy the "method" node
330  file_record.xml.elements.front().new_element(func_cov.xml);
331 
332  // copy any lines
333  for(xmlt::elementst::const_iterator
334  it=func_cov.xml.elements.front().elements.begin();
335  it!=func_cov.xml.elements.front().elements.end();
336  ++it)
337  file_record.xml.elements.back().new_element(*it);
338 
339  // merge line/branch info
340  file_record.lines_covered+=func_cov.lines_covered;
341  file_record.lines_total+=func_cov.lines_total;
342  file_record.branches_covered+=func_cov.branches_covered;
343  file_record.branches_total+=func_cov.branches_total;
344  }
345 
346  xmlt &classes=dest.xml.new_element("classes");
347 
348  // <class name="MyProject.GameRules" filename="MyProject/GameRules.java"
349  // line-rate="1.0" branch-rate="1.0" complexity="1.4">
350  for(file_recordst::const_iterator it=file_records.begin();
351  it!=file_records.end();
352  ++it)
353  {
355  continue;
356 
357  const coverage_recordt &f_cov=it->second;
358 
359  xmlt &class_xml=classes.new_element(f_cov.xml);
360  class_xml.set_attribute("name", id2string(it->first));
361  class_xml.set_attribute("filename", id2string(it->first));
362  class_xml.set_attribute("line-rate",
363  rate(f_cov.lines_covered,
364  f_cov.lines_total));
365  class_xml.set_attribute("branch-rate",
366  rate(f_cov.branches_covered,
367  f_cov.branches_total));
368  class_xml.set_attribute("complexity", "0.0");
369 
370  // merge line/branch info
371  dest.lines_covered+=f_cov.lines_covered;
372  dest.lines_total+=f_cov.lines_total;
374  dest.branches_total+=f_cov.branches_total;
375  }
376 }
377 
379  const goto_functionst &goto_functions,
380  xmlt &xml_coverage) const
381 {
382  coverage_recordt overall_cov("package");
383  compute_overall_coverage(goto_functions, overall_cov);
384 
385  std::string overall_line_rate_str=
386  rate(overall_cov.lines_covered, overall_cov.lines_total);
387  std::string overall_branch_rate_str=
388  rate(overall_cov.branches_covered, overall_cov.branches_total);
389 
390  // <coverage line-rate="0.0" branch-rate="0.0" lines-covered="1"
391  // lines-valid="1" branches-covered="1"
392  // branches-valid="1" complexity="0.0"
393  // version="2.1.1" timestamp="0">
394  xml_coverage.set_attribute("line-rate", overall_line_rate_str);
395  xml_coverage.set_attribute("branch-rate", overall_branch_rate_str);
396  xml_coverage.set_attribute("lines-covered",
397  std::to_string(overall_cov.lines_covered));
398  xml_coverage.set_attribute("lines-valid",
399  std::to_string(overall_cov.lines_total));
400  xml_coverage.set_attribute("branches-covered",
401  std::to_string(overall_cov.branches_covered));
402  xml_coverage.set_attribute("branches-valid",
403  std::to_string(overall_cov.branches_total));
404  xml_coverage.set_attribute("complexity", "0.0");
405  xml_coverage.set_attribute("version", "2.1.1");
406  xml_coverage.set_attribute("timestamp",
407  std::to_string(current_time().get_t()));
408 
409  xmlt &packages=xml_coverage.new_element("packages");
410 
411  // <package name="" line-rate="0.0" branch-rate="0.0" complexity="0.0">
412  xmlt &package=packages.new_element(overall_cov.xml);
413  package.set_attribute("name", "");
414  package.set_attribute("line-rate", overall_line_rate_str);
415  package.set_attribute("branch-rate", overall_branch_rate_str);
416  package.set_attribute("complexity", "0.0");
417 }
418 
420  const goto_functionst &goto_functions,
421  std::ostream &os) const
422 {
423  xmlt xml_coverage("coverage");
424  build_cobertura(goto_functions, xml_coverage);
425 
426  os << "<?xml version=\"1.0\"?>\n";
427  os << "<!DOCTYPE coverage SYSTEM \""
428  << "http://cobertura.sourceforge.net/xml/coverage-04.dtd\">\n";
429  os << xml_coverage;
430 
431  return !os.good();
432 }
433 
435  const goto_functionst &goto_functions,
436  const std::string &path) const
437 {
438  assert(!path.empty());
439 
440  if(path=="-")
441  return output_report(goto_functions, std::cout);
442  else
443  {
444  std::ofstream out(path.c_str());
445  return output_report(goto_functions, out);
446  }
447 }
448 
void build_cobertura(const goto_functionst &goto_functions, xmlt &xml_coverage) const
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
const symbol_tablet & get_symbol_table() const
Definition: namespace.h:91
#define CPROVER_PREFIX
void compute_coverage_lines(const goto_programt &goto_program, const irep_idt &file_name, const symex_coveraget::coveraget &coverage, coverage_lines_mapt &dest)
bool generate_report(const goto_functionst &goto_functions, const std::string &path) const
bool is_built_in() const
Goto Programs with Functions.
std::map< goto_programt::const_targett, coverage_innert > coveraget
elementst elements
Definition: xml.h:33
void compute_overall_coverage(const goto_functionst &goto_functions, coverage_recordt &dest) const
instructionst::const_iterator const_targett
bool output_report(const goto_functionst &goto_functions, std::ostream &os) const
const irep_idt & get_file() const
std::size_t lines_total
static std::string rate_detailed(std::size_t covered, std::size_t total, bool per_cent=false)
code_typet original_return_type(const symbol_tablet &symbol_table, const irep_idt &function_id)
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Definition: xml.h:18
Time Stopping.
Remove function returns.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
xmlt & new_element(const std::string &name)
Definition: xml.h:86
std::size_t branches_total
std::map< unsigned, coverage_linet > coverage_lines_mapt
static std::string rate(std::size_t covered, std::size_t total, bool per_cent=false)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
std::size_t lines_covered
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:51
absolute_timet current_time()
goto_program_coverage_recordt(const namespacet &ns, goto_functionst::function_mapt::const_iterator gf_it, const symex_coveraget::coveraget &coverage)
Record and print code coverage of symbolic execution.
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
std::size_t branches_covered
std::map< goto_programt::const_targett, coverage_conditiont > conditions
coverage_recordt(const std::string &node_id)