cprover
cover.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Coverage Instrumentation
4 
5 Author: Daniel Kroening
6 
7 Date: May 2016
8 
9 \*******************************************************************/
10 
13 
14 #include "cover.h"
15 
16 #include <algorithm>
17 #include <iterator>
18 
19 #include <util/prefix.h>
20 #include <util/message.h>
21 
23 {
24 public:
25  explicit basic_blockst(const goto_programt &_goto_program)
26  {
27  bool next_is_target=true;
28  unsigned block_count=0;
29 
30  forall_goto_program_instructions(it, _goto_program)
31  {
32  if(next_is_target || it->is_target())
33  block_count++;
34 
35  block_map[it]=block_count;
36 
37  if(!it->source_location.is_nil() &&
38  source_location_map.find(block_count)==source_location_map.end())
39  source_location_map[block_count]=it->source_location;
40 
41  next_is_target=
42  it->is_goto() || it->is_function_call() || it->is_assume();
43  }
44  }
45 
46  // map program locations to block numbers
47  typedef std::map<goto_programt::const_targett, unsigned> block_mapt;
48  block_mapt block_map;
49 
50  // map block numbers to source code locations
51  typedef std::map<unsigned, source_locationt> source_location_mapt;
52  source_location_mapt source_location_map;
53 
55  {
56  return block_map[t];
57  }
58 
59  void output(std::ostream &out)
60  {
61  for(block_mapt::const_iterator
62  b_it=block_map.begin();
63  b_it!=block_map.end();
64  b_it++)
65  out << b_it->first->source_location
66  << " -> " << b_it->second
67  << '\n';
68  }
69 };
70 
72 {
73  switch(c)
74  {
75  case coverage_criteriont::LOCATION: return "location";
76  case coverage_criteriont::BRANCH: return "branch";
77  case coverage_criteriont::DECISION: return "decision";
78  case coverage_criteriont::CONDITION: return "condition";
79  case coverage_criteriont::PATH: return "path";
80  case coverage_criteriont::MCDC: return "MC/DC";
81  case coverage_criteriont::ASSERTION: return "assertion";
82  case coverage_criteriont::COVER: return "cover instructions";
83  default: return "";
84  }
85 }
86 
87 bool is_condition(const exprt &src)
88 {
89  if(src.type().id()!=ID_bool)
90  return false;
91 
92  // conditions are 'atomic predicates'
93  if(src.id()==ID_and || src.id()==ID_or ||
94  src.id()==ID_not || src.id()==ID_implies)
95  return false;
96 
97  return true;
98 }
99 
100 void collect_conditions_rec(const exprt &src, std::set<exprt> &dest)
101 {
102  if(src.id()==ID_address_of)
103  {
104  return;
105  }
106 
107  for(const auto &op : src.operands())
108  collect_conditions_rec(op, dest);
109 
110  if(is_condition(src) && !src.is_constant())
111  dest.insert(src);
112 }
113 
114 std::set<exprt> collect_conditions(const exprt &src)
115 {
116  std::set<exprt> result;
117  collect_conditions_rec(src, result);
118  return result;
119 }
120 
122 {
123  switch(t->type)
124  {
125  case GOTO:
126  case ASSERT:
127  return collect_conditions(t->guard);
128 
129  case ASSIGN:
130  case FUNCTION_CALL:
131  return collect_conditions(t->code);
132 
133  default:
134  {
135  }
136  }
137 
138  return std::set<exprt>();
139 }
140 
141 void collect_operands(const exprt &src, std::vector<exprt> &dest)
142 {
143  for(const exprt &op : src.operands())
144  {
145  if(op.id()==src.id())
146  collect_operands(op, dest);
147  else
148  dest.push_back(op);
149  }
150 }
151 
154  const exprt &src,
155  const std::vector<exprt> &conditions,
156  std::set<exprt> &result)
157 {
158  // src is conjunction (ID_and) or disjunction (ID_or)
159  if(src.id()==ID_and ||
160  src.id()==ID_or)
161  {
162  std::vector<exprt> operands;
163  collect_operands(src, operands);
164 
165  if(operands.size()==1)
166  {
167  exprt e=*operands.begin();
168  collect_mcdc_controlling_rec(e, conditions, result);
169  }
170  else if(!operands.empty())
171  {
172  for(std::size_t i=0; i<operands.size(); i++)
173  {
174  const exprt op=operands[i];
175 
176  if(is_condition(op))
177  {
178  if(src.id()==ID_or)
179  {
180  std::vector<exprt> others1, others2;
181  if(!conditions.empty())
182  {
183  others1.push_back(conjunction(conditions));
184  others2.push_back(conjunction(conditions));
185  }
186 
187  for(std::size_t j=0; j<operands.size(); j++)
188  {
189  others1.push_back(not_exprt(operands[j]));
190  if(i!=j)
191  others2.push_back(not_exprt(operands[j]));
192  else
193  others2.push_back((operands[j]));
194  }
195 
196  result.insert(conjunction(others1));
197  result.insert(conjunction(others2));
198  continue;
199  }
200 
201  std::vector<exprt> o=operands;
202 
203  // 'o[i]' needs to be true and false
204  std::vector<exprt> new_conditions=conditions;
205  new_conditions.push_back(conjunction(o));
206  result.insert(conjunction(new_conditions));
207 
208  o[i].make_not();
209  new_conditions.back()=conjunction(o);
210  result.insert(conjunction(new_conditions));
211  }
212  else
213  {
214  std::vector<exprt> others;
215  others.reserve(operands.size()-1);
216 
217  for(std::size_t j=0; j<operands.size(); j++)
218  if(i!=j)
219  {
220  if(src.id()==ID_or)
221  others.push_back(not_exprt(operands[j]));
222  else
223  others.push_back(operands[j]);
224  }
225 
226  exprt c=conjunction(others);
227  std::vector<exprt> new_conditions=conditions;
228  new_conditions.push_back(c);
229 
230  collect_mcdc_controlling_rec(op, new_conditions, result);
231  }
232  }
233  }
234  }
235  else if(src.id()==ID_not)
236  {
237  exprt e=to_not_expr(src).op();
238  if(!is_condition(e))
239  collect_mcdc_controlling_rec(e, conditions, result);
240  else
241  {
242  // to store a copy of ''src''
243  std::vector<exprt> new_conditions1=conditions;
244  new_conditions1.push_back(src);
245  result.insert(conjunction(new_conditions1));
246 
247  // to store a copy of its negation, i.e., ''e''
248  std::vector<exprt> new_conditions2=conditions;
249  new_conditions2.push_back(e);
250  result.insert(conjunction(new_conditions2));
251  }
252  }
253  else
254  {
260  }
261 }
262 
263 std::set<exprt> collect_mcdc_controlling(
264  const std::set<exprt> &decisions)
265 {
266  std::set<exprt> result;
267 
268  for(const auto &d : decisions)
269  collect_mcdc_controlling_rec(d, { }, result);
270 
271  return result;
272 }
273 
276 std::set<exprt> replacement_conjunction(
277  const std::set<exprt> &replacement_exprs,
278  const std::vector<exprt> &operands,
279  const std::size_t i)
280 {
281  std::set<exprt> result;
282  for(auto &y : replacement_exprs)
283  {
284  std::vector<exprt> others;
285  for(std::size_t j=0; j<operands.size(); j++)
286  if(i!=j)
287  others.push_back(operands[j]);
288 
289  others.push_back(y);
290  exprt c=conjunction(others);
291  result.insert(c);
292  }
293  return result;
294 }
295 
299  const std::set<exprt> &decisions)
300 {
301  // To obtain the 1st-level controlling conditions
302  std::set<exprt> controlling = collect_mcdc_controlling(decisions);
303 
304  std::set<exprt> result;
305  // For each controlling condition, to check if it contains
306  // non-atomic exprs
307  for(auto &src : controlling)
308  {
309  std::set<exprt> s1, s2;
315  s1.insert(src);
316 
317  // dual-loop structure to eliminate complex
318  // non-atomic-conditional terms
319  while(true)
320  {
321  bool changed=false;
322  // the 2nd loop
323  for(auto &x : s1)
324  {
325  // if ''x'' is atomic conditional term, there
326  // is no expansion
327  if(is_condition(x))
328  {
329  s2.insert(x);
330  continue;
331  }
332  // otherwise, we apply the ''nested'' method to
333  // each of its operands
334  std::vector<exprt> operands;
335  collect_operands(x, operands);
336 
337  for(std::size_t i=0; i<operands.size(); i++)
338  {
339  std::set<exprt> res;
345  if(operands[i].id()==ID_not)
346  {
347  exprt no=operands[i].op0();
348  if(!is_condition(no))
349  {
350  changed=true;
351  std::set<exprt> ctrl_no;
352  ctrl_no.insert(no);
353  res=collect_mcdc_controlling(ctrl_no);
354  }
355  }
356  else if(!is_condition(operands[i]))
357  {
358  changed=true;
359  std::set<exprt> ctrl;
360  ctrl.insert(operands[i]);
361  res=collect_mcdc_controlling(ctrl);
362  }
363 
364  // To replace a non-atomic expr with its expansion
365  std::set<exprt> co=
366  replacement_conjunction(res, operands, i);
367  s2.insert(co.begin(), co.end());
368  if(!res.empty())
369  break;
370  }
371  // if there is no change x.r.t current operands of ''x'',
372  // i.e., they are all atomic, we reserve ''x''
373  if(!changed)
374  s2.insert(x);
375  }
376  // update ''s1'' and check if change happens
377  s1=s2;
378  if(!changed)
379  break;
380  s2.clear();
381  }
382 
383  // The expansions of each ''src'' should be added into
384  // the ''result''
385  result.insert(s1.begin(), s1.end());
386  }
387 
388  return result;
389 }
390 
395 std::set<signed> sign_of_expr(const exprt &e, const exprt &E)
396 {
397  std::set<signed> signs;
398 
399  // At fist, we pre-screen the case such that ''E''
400  // is an atomic condition
401  if(is_condition(E))
402  {
403  if(e==E)
404  signs.insert(+1);
405  return signs;
406  }
407 
408  // or, ''E'' is the negation of ''e''?
409  if(E.id()==ID_not)
410  {
411  if(e==E.op0())
412  {
413  signs.insert(-1);
414  return signs;
415  }
416  }
417 
421  std::vector<exprt> ops;
422  collect_operands(E, ops);
423  for(auto &x : ops)
424  {
425  exprt y(x);
426  if(y==e)
427  signs.insert(+1);
428  else if(y.id()==ID_not)
429  {
430  y.make_not();
431  if(y==e)
432  signs.insert(-1);
433  if(!is_condition(y))
434  {
435  std::set<signed> re=sign_of_expr(e, y);
436  signs.insert(re.begin(), re.end());
437  }
438  }
439  else if(!is_condition(y))
440  {
441  std::set<signed> re=sign_of_expr(e, y);
442  signs.insert(re.begin(), re.end());
443  }
444  }
445 
446  return signs;
447 }
448 
452 void remove_repetition(std::set<exprt> &exprs)
453 {
454  // to obtain the set of atomic conditions
455  std::set<exprt> conditions;
456  for(auto &x : exprs)
457  {
458  std::set<exprt> new_conditions=collect_conditions(x);
459  conditions.insert(new_conditions.begin(), new_conditions.end());
460  }
461  // exprt that contains multiple (inconsistent) signs should
462  // be removed
463  std::set<exprt> new_exprs;
464  for(auto &x : exprs)
465  {
466  bool kept=true;
467  for(auto &c : conditions)
468  {
469  std::set<signed> signs=sign_of_expr(c, x);
470  if(signs.size()>1)
471  {
472  kept=false;
473  break;
474  }
475  }
476  if(kept)
477  new_exprs.insert(x);
478  }
479  exprs=new_exprs;
480  new_exprs.clear();
481 
482  for(auto &x : exprs)
483  {
484  bool red=false;
491  for(auto &y : new_exprs)
492  {
493  bool iden = true;
494  for(auto &c : conditions)
495  {
496  std::set<signed> signs1=sign_of_expr(c, x);
497  std::set<signed> signs2=sign_of_expr(c, y);
498  int s1=signs1.size(), s2=signs2.size();
499  // it is easy to check non-equivalence;
500  if(s1!=s2)
501  {
502  iden=false;
503  break;
504  }
505  else
506  {
507  if(s1==0 && s2==0)
508  continue;
509  // it is easy to check non-equivalence
510  if(*(signs1.begin())!=*(signs2.begin()))
511  {
512  iden=false;
513  break;
514  }
515  }
516  }
522  if(iden)
523  {
524  red=true;
525  break;
526  }
527  }
528  // an expr is added into ''new_exprs''
529  // if it is not found repetitive
530  if(!red)
531  new_exprs.insert(x);
532  }
533 
534  // update the original ''exprs''
535  exprs = new_exprs;
536 }
537 
540  const std::map<exprt, signed> &atomic_exprs,
541  const exprt &src)
542 {
543  std::vector<exprt> operands;
544  collect_operands(src, operands);
545  // src is AND
546  if(src.id()==ID_and)
547  {
548  for(auto &x : operands)
549  if(!eval_expr(atomic_exprs, x))
550  return false;
551  return true;
552  }
553  // src is OR
554  else if(src.id()==ID_or)
555  {
556  std::size_t fcount=0;
557 
558  for(auto &x : operands)
559  if(!eval_expr(atomic_exprs, x))
560  fcount++;
561 
562  if(fcount<operands.size())
563  return true;
564  else
565  return false;
566  }
567  // src is NOT
568  else if(src.id()==ID_not)
569  {
570  exprt no_op(src);
571  no_op.make_not();
572  return !eval_expr(atomic_exprs, no_op);
573  }
574  else // if(is_condition(src))
575  {
576  // ''src'' should be guaranteed to be consistent
577  // with ''atomic_exprs''
578  if(atomic_exprs.find(src)->second==+1)
579  return true;
580  else // if(atomic_exprs.find(src)->second==-1)
581  return false;
582  }
583 }
584 
586 std::map<exprt, signed> values_of_atomic_exprs(
587  const exprt &e,
588  const std::set<exprt> &conditions)
589 {
590  std::map<exprt, signed> atomic_exprs;
591  for(auto &c : conditions)
592  {
593  std::set<signed> signs=sign_of_expr(c, e);
594  if(signs.empty())
595  {
596  // ''c'' is not contained in ''e''
597  atomic_exprs.insert(std::pair<exprt, signed>(c, 0));
598  continue;
599  }
600  // we do not consider inconsistent expr ''e''
601  if(signs.size()!=1)
602  continue;
603 
604  atomic_exprs.insert(
605  std::pair<exprt, signed>(c, *signs.begin()));
606  }
607  return atomic_exprs;
608 }
609 
615  const exprt &e1,
616  const exprt &e2,
617  const exprt &c,
618  const std::set<exprt> &conditions,
619  const exprt &decision)
620 {
621  // An controlling expr cannot be mcdc pair of itself
622  if(e1==e2)
623  return false;
624 
625  // To obtain values of each atomic condition within ''e1''
626  // and ''e2''
627  std::map<exprt, signed> atomic_exprs_e1=
628  values_of_atomic_exprs(e1, conditions);
629  std::map<exprt, signed> atomic_exprs_e2=
630  values_of_atomic_exprs(e2, conditions);
631 
632  // the sign of ''c'' inside ''e1'' and ''e2''
633  signed cs1=atomic_exprs_e1.find(c)->second;
634  signed cs2=atomic_exprs_e2.find(c)->second;
635  // a mcdc pair should both contain ''c'', i.e., sign=+1 or -1
636  if(cs1==0 || cs2==0)
637  return false;
638 
639  // A mcdc pair regarding an atomic expr ''c''
640  // should have different values of ''c''
641  if(cs1==cs2)
642  return false;
643 
644  // A mcdc pair should result in different ''decision''
645  if(eval_expr(atomic_exprs_e1, decision)==
646  eval_expr(atomic_exprs_e2, decision))
647  return false;
648 
655  int diff_count=0;
656  auto e1_it=atomic_exprs_e1.begin();
657  auto e2_it=atomic_exprs_e2.begin();
658  while(e1_it!=atomic_exprs_e1.end())
659  {
660  if(e1_it->second!=e2_it->second)
661  diff_count++;
662  if(diff_count>1)
663  break;
664  e1_it++;
665  e2_it++;
666  }
667 
668  if(diff_count==1)
669  return true;
670  else return false;
671 }
672 
676  const exprt &c,
677  const std::set<exprt> &expr_set,
678  const std::set<exprt> &conditions,
679  const exprt &decision)
680 {
681  for(auto y1 : expr_set)
682  {
683  for(auto y2 : expr_set)
684  {
685  if(is_mcdc_pair(y1, y2, c, conditions, decision))
686  {
687  return true;
688  }
689  }
690  }
691  return false;
692 }
693 
701  std::set<exprt> &controlling,
702  const exprt &decision)
703 {
704  // to obtain the set of atomic conditions
705  std::set<exprt> conditions;
706  for(auto &x : controlling)
707  {
708  std::set<exprt> new_conditions=collect_conditions(x);
709  conditions.insert(new_conditions.begin(), new_conditions.end());
710  }
711 
712  while(true)
713  {
714  std::set<exprt> new_controlling;
715  bool ctrl_update=false;
732  for(auto &x : controlling)
733  {
734  // To create a new ''controlling'' set without ''x''
735  new_controlling.clear();
736  for(auto &y : controlling)
737  if(y!=x)
738  new_controlling.insert(y);
739 
740  bool removing_x=true;
741  // For each atomic expr condition ''c'', to check if its is
742  // covered by at least a mcdc pair.
743  for(auto &c : conditions)
744  {
745  bool cOK=
746  has_mcdc_pair(c, new_controlling, conditions, decision);
752  if(!cOK)
753  {
754  removing_x=false;
755  break;
756  }
757  }
758 
759  // If ''removing_x'' is valid, it is safe to remove ''x''
760  // from the original ''controlling''
761  if(removing_x)
762  {
763  ctrl_update=true;
764  break;
765  }
766  }
767  // Update ''controlling'' or break the while loop
768  if(ctrl_update)
769  {
770  controlling=new_controlling;
771  }
772  else break;
773  }
774 }
775 
776 void collect_decisions_rec(const exprt &src, std::set<exprt> &dest)
777 {
778  if(src.id()==ID_address_of)
779  {
780  return;
781  }
782 
783  if(src.type().id()==ID_bool)
784  {
785  if(src.is_constant())
786  {
787  // ignore me
788  }
789  else if(src.id()==ID_not)
790  {
791  collect_decisions_rec(src.op0(), dest);
792  }
793  else
794  {
795  dest.insert(src);
796  }
797  }
798  else
799  {
800  for(const auto &op : src.operands())
801  collect_decisions_rec(op, dest);
802  }
803 }
804 
805 std::set<exprt> collect_decisions(const exprt &src)
806 {
807  std::set<exprt> result;
808  collect_decisions_rec(src, result);
809  return result;
810 }
811 
813 {
814  switch(t->type)
815  {
816  case GOTO:
817  case ASSERT:
818  return collect_decisions(t->guard);
819 
820  case ASSIGN:
821  case FUNCTION_CALL:
822  return collect_decisions(t->code);
823 
824  default:
825  {
826  }
827  }
828 
829  return std::set<exprt>();
830 }
831 
833  const symbol_tablet &symbol_table,
834  goto_programt &goto_program,
835  coverage_criteriont criterion)
836 {
837  const namespacet ns(symbol_table);
838  basic_blockst basic_blocks(goto_program);
839  std::set<unsigned> blocks_done;
840 
841  // ignore if built-in library
842  if(!goto_program.instructions.empty() &&
843  goto_program.instructions.front().source_location.is_built_in())
844  return;
845 
846  const irep_idt coverage_criterion=as_string(criterion);
847  const irep_idt property_class="coverage";
848 
849  Forall_goto_program_instructions(i_it, goto_program)
850  {
851  switch(criterion)
852  {
854  // turn into 'assert(false)' to avoid simplification
855  if(i_it->is_assert())
856  {
857  i_it->guard=false_exprt();
858  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
859  i_it->source_location.set_property_class(property_class);
860  }
861  break;
862 
864  // turn __CPROVER_cover(x) into 'assert(!x)'
865  if(i_it->is_function_call())
866  {
867  const code_function_callt &code_function_call=
868  to_code_function_call(i_it->code);
869  if(code_function_call.function().id()==ID_symbol &&
870  to_symbol_expr(code_function_call.function()).get_identifier()==
871  "__CPROVER_cover" &&
872  code_function_call.arguments().size()==1)
873  {
874  const exprt c=code_function_call.arguments()[0];
875  std::string comment="condition `"+from_expr(ns, "", c)+"'";
876  i_it->guard=not_exprt(c);
877  i_it->type=ASSERT;
878  i_it->code.clear();
879  i_it->source_location.set_comment(comment);
880  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
881  i_it->source_location.set_property_class(property_class);
882  }
883  }
884  else if(i_it->is_assert())
885  i_it->make_skip();
886  break;
887 
889  if(i_it->is_assert())
890  i_it->make_skip();
891 
892  {
893  unsigned block_nr=basic_blocks[i_it];
894  if(blocks_done.insert(block_nr).second)
895  {
896  std::string b=std::to_string(block_nr);
897  std::string id=id2string(i_it->function)+"#"+b;
898  source_locationt source_location=
899  basic_blocks.source_location_map[block_nr];
900 
901  if(!source_location.get_file().empty() &&
902  !source_location.is_built_in())
903  {
904  std::string comment="block "+b;
905  goto_program.insert_before_swap(i_it);
906  i_it->make_assertion(false_exprt());
907  i_it->source_location=source_location;
908  i_it->source_location.set_comment(comment);
909  i_it->source_location.set(
910  ID_coverage_criterion, coverage_criterion);
911  i_it->source_location.set_property_class(property_class);
912 
913  i_it++;
914  }
915  }
916  }
917  break;
918 
920  if(i_it->is_assert())
921  i_it->make_skip();
922 
923  if(i_it==goto_program.instructions.begin())
924  {
925  // we want branch coverage to imply 'entry point of function'
926  // coverage
927  std::string comment=
928  "function "+id2string(i_it->function)+" entry point";
929 
930  source_locationt source_location=i_it->source_location;
931 
932  goto_programt::targett t=goto_program.insert_before(i_it);
933  t->make_assertion(false_exprt());
934  t->source_location=source_location;
935  t->source_location.set_comment(comment);
936  t->source_location.set(ID_coverage_criterion, coverage_criterion);
937  t->source_location.set_property_class(property_class);
938  }
939 
940  if(i_it->is_goto() && !i_it->guard.is_true() &&
941  !i_it->source_location.is_built_in())
942  {
943  std::string b=std::to_string(basic_blocks[i_it]);
944  std::string true_comment=
945  "function "+id2string(i_it->function)+" block "+b+" branch true";
946  std::string false_comment=
947  "function "+id2string(i_it->function)+" block "+b+" branch false";
948 
949  exprt guard=i_it->guard;
950  source_locationt source_location=i_it->source_location;
951 
952  goto_program.insert_before_swap(i_it);
953  i_it->make_assertion(not_exprt(guard));
954  i_it->source_location=source_location;
955  i_it->source_location.set_comment(true_comment);
956  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
957  i_it->source_location.set_property_class(property_class);
958 
959  goto_program.insert_before_swap(i_it);
960  i_it->make_assertion(guard);
961  i_it->source_location=source_location;
962  i_it->source_location.set_comment(false_comment);
963  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
964  i_it->source_location.set_property_class(property_class);
965 
966  i_it++;
967  i_it++;
968  }
969  break;
970 
972  if(i_it->is_assert())
973  i_it->make_skip();
974 
975  // Conditions are all atomic predicates in the programs.
976  if(!i_it->source_location.is_built_in())
977  {
978  const std::set<exprt> conditions=collect_conditions(i_it);
979 
980  const source_locationt source_location=i_it->source_location;
981 
982  for(const auto &c : conditions)
983  {
984  const std::string c_string=from_expr(ns, "", c);
985 
986  const std::string comment_t="condition `"+c_string+"' true";
987  goto_program.insert_before_swap(i_it);
988  i_it->make_assertion(c);
989  i_it->source_location=source_location;
990  i_it->source_location.set_comment(comment_t);
991  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
992  i_it->source_location.set_property_class(property_class);
993 
994  const std::string comment_f="condition `"+c_string+"' false";
995  goto_program.insert_before_swap(i_it);
996  i_it->make_assertion(not_exprt(c));
997  i_it->source_location=source_location;
998  i_it->source_location.set_comment(comment_f);
999  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
1000  i_it->source_location.set_property_class(property_class);
1001  }
1002 
1003  for(std::size_t i=0; i<conditions.size()*2; i++)
1004  i_it++;
1005  }
1006  break;
1007 
1009  if(i_it->is_assert())
1010  i_it->make_skip();
1011 
1012  // Decisions are maximal Boolean combinations of conditions.
1013  if(!i_it->source_location.is_built_in())
1014  {
1015  const std::set<exprt> decisions=collect_decisions(i_it);
1016 
1017  const source_locationt source_location=i_it->source_location;
1018 
1019  for(const auto &d : decisions)
1020  {
1021  const std::string d_string=from_expr(ns, "", d);
1022 
1023  const std::string comment_t="decision `"+d_string+"' true";
1024  goto_program.insert_before_swap(i_it);
1025  i_it->make_assertion(d);
1026  i_it->source_location=source_location;
1027  i_it->source_location.set_comment(comment_t);
1028  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
1029  i_it->source_location.set_property_class(property_class);
1030 
1031  const std::string comment_f="decision `"+d_string+"' false";
1032  goto_program.insert_before_swap(i_it);
1033  i_it->make_assertion(not_exprt(d));
1034  i_it->source_location=source_location;
1035  i_it->source_location.set_comment(comment_f);
1036  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
1037  i_it->source_location.set_property_class(property_class);
1038  }
1039 
1040  for(std::size_t i=0; i<decisions.size()*2; i++)
1041  i_it++;
1042  }
1043  break;
1044 
1046  if(i_it->is_assert())
1047  i_it->make_skip();
1048 
1049  // 1. Each entry and exit point is invoked
1050  // 2. Each decision takes every possible outcome
1051  // 3. Each condition in a decision takes every possible outcome
1052  // 4. Each condition in a decision is shown to independently
1053  // affect the outcome of the decision.
1054  if(!i_it->source_location.is_built_in())
1055  {
1056  const std::set<exprt> conditions=collect_conditions(i_it);
1057  const std::set<exprt> decisions=collect_decisions(i_it);
1058 
1059  std::set<exprt> both;
1060  std::set_union(conditions.begin(), conditions.end(),
1061  decisions.begin(), decisions.end(),
1062  inserter(both, both.end()));
1063 
1064  const source_locationt source_location=i_it->source_location;
1065 
1066  for(const auto &p : both)
1067  {
1068  bool is_decision=decisions.find(p)!=decisions.end();
1069  bool is_condition=conditions.find(p)!=conditions.end();
1070 
1071  std::string description=
1072  (is_decision && is_condition)?"decision/condition":
1073  is_decision?"decision":"condition";
1074 
1075  std::string p_string=from_expr(ns, "", p);
1076 
1077  std::string comment_t=description+" `"+p_string+"' true";
1078  goto_program.insert_before_swap(i_it);
1079  // i_it->make_assertion(p);
1080  i_it->make_assertion(not_exprt(p));
1081  i_it->source_location=source_location;
1082  i_it->source_location.set_comment(comment_t);
1083  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
1084  i_it->source_location.set_property_class(property_class);
1085 
1086  std::string comment_f=description+" `"+p_string+"' false";
1087  goto_program.insert_before_swap(i_it);
1088  // i_it->make_assertion(not_exprt(p));
1089  i_it->make_assertion(p);
1090  i_it->source_location=source_location;
1091  i_it->source_location.set_comment(comment_f);
1092  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
1093  i_it->source_location.set_property_class(property_class);
1094  }
1095 
1096  std::set<exprt> controlling;
1097  // controlling=collect_mcdc_controlling(decisions);
1098  controlling=collect_mcdc_controlling_nested(decisions);
1099  remove_repetition(controlling);
1100  // for now, we restrict to the case of a single ''decision'';
1101  // however, this is not true, e.g., ''? :'' operator.
1102  minimize_mcdc_controlling(controlling, *decisions.begin());
1103 
1104  for(const auto &p : controlling)
1105  {
1106  std::string p_string=from_expr(ns, "", p);
1107 
1108  std::string description=
1109  "MC/DC independence condition `"+p_string+"'";
1110 
1111  goto_program.insert_before_swap(i_it);
1112  i_it->make_assertion(not_exprt(p));
1113  // i_it->make_assertion(p);
1114  i_it->source_location=source_location;
1115  i_it->source_location.set_comment(description);
1116  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
1117  i_it->source_location.set_property_class(property_class);
1118  }
1119 
1120  for(std::size_t i=0; i<both.size()*2+controlling.size(); i++)
1121  i_it++;
1122  }
1123  break;
1124 
1126  if(i_it->is_assert())
1127  i_it->make_skip();
1128  break;
1129 
1130  default:
1131  {
1132  }
1133  }
1134  }
1135 }
1136 
1138  const symbol_tablet &symbol_table,
1139  goto_functionst &goto_functions,
1140  coverage_criteriont criterion)
1141 {
1142  Forall_goto_functions(f_it, goto_functions)
1143  {
1144  if(f_it->first==goto_functions.entry_point() ||
1145  f_it->first=="__CPROVER_initialize" ||
1146  f_it->second.is_hidden())
1147  continue;
1148 
1149  instrument_cover_goals(symbol_table, f_it->second.body, criterion);
1150  }
1151 }
1152 
1154  const cmdlinet &cmdline,
1155  const symbol_tablet &symbol_table,
1156  goto_functionst &goto_functions,
1157  message_handlert &msgh)
1158 {
1159  messaget msg(msgh);
1160  std::list<std::string> criteria_strings=cmdline.get_values("cover");
1161  std::set<coverage_criteriont> criteria;
1162  bool keep_assertions=false;
1163 
1164  for(const auto &criterion_string : criteria_strings)
1165  {
1167 
1168  if(criterion_string=="assertion" || criterion_string=="assertions")
1169  {
1170  keep_assertions=true;
1172  }
1173  else if(criterion_string=="path" || criterion_string=="paths")
1175  else if(criterion_string=="branch" || criterion_string=="branches")
1177  else if(criterion_string=="location" || criterion_string=="locations")
1179  else if(criterion_string=="decision" || criterion_string=="decisions")
1181  else if(criterion_string=="condition" || criterion_string=="conditions")
1183  else if(criterion_string=="mcdc")
1185  else if(criterion_string=="cover")
1187  else
1188  {
1189  msg.error() << "unknown coverage criterion "
1190  << '\'' << criterion_string << '\''
1191  << messaget::eom;
1192  return true;
1193  }
1194 
1195  criteria.insert(c);
1196  }
1197 
1198  if(keep_assertions && criteria_strings.size()>1)
1199  {
1200  msg.error() << "assertion coverage cannot currently be used together with "
1201  << "other coverage criteria" << messaget::eom;
1202  return true;
1203  }
1204 
1205  msg.status() << "Rewriting existing assertions as assumptions"
1206  << messaget::eom;
1207 
1208  if(!keep_assertions)
1209  {
1210  // turn assertions (from generic checks) into assumptions
1211  Forall_goto_functions(f_it, goto_functions)
1212  {
1213  goto_programt &body=f_it->second.body;
1215  {
1216  if(i_it->is_assert())
1218  }
1219  }
1220  }
1221 
1222  msg.status() << "Instrumenting coverage goals" << messaget::eom;
1223 
1224  for(const auto &criterion : criteria)
1225  instrument_cover_goals(symbol_table, goto_functions, criterion);
1226 
1227  goto_functions.update();
1228  return false;
1229 }
coverage_criteriont
Definition: cover.h:22
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:90
void collect_operands(const exprt &src, std::vector< exprt > &dest)
Definition: cover.cpp:141
Boolean negation.
Definition: std_expr.h:2648
basic_blockst(const goto_programt &_goto_program)
Definition: cover.cpp:25
void minimize_mcdc_controlling(std::set< exprt > &controlling, const exprt &decision)
This method minimizes the controlling conditions for mcdc coverage.
Definition: cover.cpp:700
std::set< exprt > collect_conditions(const exprt &src)
Definition: cover.cpp:114
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
exprt & op0()
Definition: expr.h:84
std::set< exprt > collect_mcdc_controlling_nested(const std::set< exprt > &decisions)
This nested method iteratively applies &#39;&#39;collect_mcdc_controlling&#39;&#39; to every non-atomic expr within a...
Definition: cover.cpp:298
static bool is_built_in(const std::string &s)
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:115
mstreamt & status()
Definition: message.h:238
std::set< exprt > collect_mcdc_controlling(const std::set< exprt > &decisions)
Definition: cover.cpp:263
instructionst instructions
The list of instructions in the goto program.
void set_comment(const irep_idt &comment)
std::map< exprt, signed > values_of_atomic_exprs(const exprt &e, const std::set< exprt > &conditions)
To obtain values of atomic exprs within the super expr.
Definition: cover.cpp:586
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool eval_expr(const std::map< exprt, signed > &atomic_exprs, const exprt &src)
To evaluate the value of expr &#39;&#39;src&#39;&#39;, according to the atomic expr values.
Definition: cover.cpp:539
typet & type()
Definition: expr.h:60
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
unsigned operator[](goto_programt::const_targett t)
Definition: cover.cpp:54
const char * as_string(coverage_criteriont c)
Definition: cover.cpp:71
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:50
const irep_idt & id() const
Definition: irep.h:189
void collect_mcdc_controlling_rec(const exprt &src, const std::vector< exprt > &conditions, std::set< exprt > &result)
To recursively collect controlling exprs for for mcdc coverage.
Definition: cover.cpp:153
instructionst::const_iterator const_targett
argumentst & arguments()
Definition: std_code.h:689
std::map< goto_programt::const_targett, unsigned > block_mapt
Definition: cover.cpp:47
std::map< unsigned, source_locationt > source_location_mapt
Definition: cover.cpp:51
void instrument_cover_goals(const symbol_tablet &symbol_table, goto_programt &goto_program, coverage_criteriont criterion)
Definition: cover.cpp:832
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void collect_decisions_rec(const exprt &src, std::set< exprt > &dest)
Definition: cover.cpp:776
A function call.
Definition: std_code.h:657
bool has_mcdc_pair(const exprt &c, const std::set< exprt > &expr_set, const std::set< exprt > &conditions, const exprt &decision)
To check if we can find the mcdc pair of the input &#39;&#39;expr_set&#39;&#39; regarding the atomic expr &#39;&#39;c&#39;&#39;...
Definition: cover.cpp:675
The boolean constant false.
Definition: std_expr.h:3753
bool is_constant() const
Definition: expr.cpp:128
targett insert_before(const_targett target)
Insertion before the given target.
const not_exprt & to_not_expr(const exprt &expr)
Cast a generic exprt to an not_exprt.
Definition: std_expr.h:2682
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
exprt & op()
Definition: std_expr.h:2661
const irep_idt & get_file() const
void make_not()
Definition: expr.cpp:100
std::set< signed > sign_of_expr(const exprt &e, const exprt &E)
The sign of expr &#39;&#39;e&#39;&#39; within the super-expr &#39;&#39;E&#39;&#39;.
Definition: cover.cpp:395
void basic_blocks(goto_programt &goto_program, unsigned max_block_size)
convert basic blocks into single expressions of type "block"
exprt & function()
Definition: std_code.h:677
void output(std::ostream &out)
Definition: cover.cpp:59
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
#define Forall_goto_functions(it, functions)
source_location_mapt source_location_map
Definition: cover.cpp:52
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
mstreamt & error()
Definition: message.h:223
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
int8_t s1
Definition: bytecode_info.h:59
bool is_condition(const exprt &src)
Definition: cover.cpp:87
Coverage Instrumentation.
int16_t s2
Definition: bytecode_info.h:60
std::set< exprt > replacement_conjunction(const std::set< exprt > &replacement_exprs, const std::vector< exprt > &operands, const std::size_t i)
To replace the i-th expr of &#39;&#39;operands&#39;&#39; with each expr inside &#39;&#39;replacement_exprs&#39;&#39;.
Definition: cover.cpp:276
operandst & operands()
Definition: expr.h:70
bool is_mcdc_pair(const exprt &e1, const exprt &e2, const exprt &c, const std::set< exprt > &conditions, const exprt &decision)
To check if the two input controlling exprs are mcdc pairs regarding an atomic expr &#39;&#39;c&#39;&#39;...
Definition: cover.cpp:614
std::set< exprt > collect_decisions(const exprt &src)
Definition: cover.cpp:805
void collect_conditions_rec(const exprt &src, std::set< exprt > &dest)
Definition: cover.cpp:100
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
bool empty() const
Definition: dstring.h:61
block_mapt block_map
Definition: cover.cpp:48
void remove_repetition(std::set< exprt > &exprs)
After the &#39;&#39;collect_mcdc_controlling_nested&#39;&#39;, there can be the recurrence of the same expr in the re...
Definition: cover.cpp:452
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700