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