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 <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 
25 #include <langapi/language_util.h>
26 
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  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<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,
92  coverage_lines_mapt &dest);
93 };
94 
95 static std::string
96 rate(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 
119 static std::string
120 rate_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,
207  coverage_lines_mapt &dest)
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->condition().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)
234  UNREACHABLE;
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)
257  ++lines_covered;
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;
363  dest.branches_covered += f_cov.branches_covered;
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 }
coverage_recordt::branches_covered
std::size_t branches_covered
Definition: symex_coverage.cpp:46
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
symex_coveraget::compute_overall_coverage
void compute_overall_coverage(const goto_functionst &goto_functions, coverage_recordt &dest) const
Definition: symex_coverage.cpp:291
xmlt::elements
elementst elements
Definition: xml.h:42
goto_program_coverage_recordt::coverage_linet
Definition: symex_coverage.cpp:77
rate
static std::string rate(std::size_t covered, std::size_t total, bool per_cent=false)
Definition: symex_coverage.cpp:96
coverage_recordt::coverage_recordt
coverage_recordt(const std::string &node_id)
Definition: symex_coverage.cpp:34
goto_program_coverage_recordt::coverage_conditiont::coverage_conditiont
coverage_conditiont()
Definition: symex_coverage.cpp:69
symex_coveraget::coveraget
std::map< goto_programt::const_targett, coverage_innert > coveraget
Definition: symex_coverage.h:69
goto_program_coverage_recordt::goto_program_coverage_recordt
goto_program_coverage_recordt(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, const symex_coveraget::coveraget &coverage)
Definition: symex_coverage.cpp:128
goto_program_coverage_recordt::get_file
const irep_idt & get_file() const
Definition: symex_coverage.cpp:59
from_type
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
Definition: language_util.cpp:51
source_locationt::is_built_in
bool is_built_in() const
Definition: source_location.h:168
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:58
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
symex_coveraget::build_cobertura
void build_cobertura(const goto_functionst &goto_functions, xmlt &xml_coverage) const
Definition: symex_coverage.cpp:368
xml.h
symex_coveraget::coverage
coveraget coverage
Definition: symex_coverage.h:70
goto_program_coverage_recordt::compute_coverage_lines
void compute_coverage_lines(const goto_programt &goto_program, const symex_coveraget::coveraget &coverage, coverage_lines_mapt &dest)
Definition: symex_coverage.cpp:204
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
string2int.h
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
goto_program_coverage_recordt::coverage_conditiont::false_taken
bool false_taken
Definition: symex_coverage.cpp:73
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:510
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
symex_coverage.h
language_util.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
symex_coveraget::output_report
bool output_report(const goto_functionst &goto_functions, std::ostream &os) const
Definition: symex_coverage.cpp:412
symex_coveraget::generate_report
bool generate_report(const goto_functionst &goto_functions, const std::string &path) const
Definition: symex_coverage.cpp:427
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:22
goto_program_coverage_recordt::coverage_lines_mapt
std::map< unsigned, coverage_linet > coverage_lines_mapt
Definition: symex_coverage.cpp:87
coverage_recordt::lines_total
std::size_t lines_total
Definition: symex_coverage.cpp:45
symbol.h
Symbol table entry.
dstringt::empty
bool empty() const
Definition: dstring.h:88
goto_program_coverage_recordt::coverage_conditiont
Definition: symex_coverage.cpp:67
xmlt
Definition: xml.h:20
safe_string2unsigned
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:16
coverage_recordt::branches_total
std::size_t branches_total
Definition: symex_coverage.cpp:47
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:592
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:24
goto_program_coverage_recordt::coverage_linet::conditions
std::map< goto_programt::const_targett, coverage_conditiont > conditions
Definition: symex_coverage.cpp:84
symex_coveraget::ns
const namespacet & ns
Definition: symex_coverage.h:50
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:198
goto_program_coverage_recordt::coverage_linet::hits
unsigned hits
Definition: symex_coverage.cpp:83
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
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:587
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:92
goto_program_coverage_recordt::file_name
irep_idt file_name
Definition: symex_coverage.cpp:65
rate_detailed
static std::string rate_detailed(std::size_t covered, std::size_t total, bool per_cent=false)
Definition: symex_coverage.cpp:120
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:1229
validation_modet::INVARIANT
@ INVARIANT
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95