cprover
cover_instrument_mcdc.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Coverage Instrumentation
4 
5 Author: Daniel Kroening
6 
7 \*******************************************************************/
8 
11 
12 #include "cover_instrument.h"
13 
14 #include <langapi/language_util.h>
15 
16 #include <algorithm>
17 #include <iterator>
18 
19 #include "cover_util.h"
20 
23  const exprt &src,
24  const std::vector<exprt> &conditions,
25  std::set<exprt> &result)
26 {
27  // src is conjunction (ID_and) or disjunction (ID_or)
28  if(src.id() == ID_and || src.id() == ID_or)
29  {
30  std::vector<exprt> operands;
31  collect_operands(src, operands);
32 
33  if(operands.size() == 1)
34  {
35  exprt e = *operands.begin();
36  collect_mcdc_controlling_rec(e, conditions, result);
37  }
38  else if(!operands.empty())
39  {
40  for(std::size_t i = 0; i < operands.size(); i++)
41  {
42  const exprt op = operands[i];
43 
44  if(is_condition(op))
45  {
46  if(src.id() == ID_or)
47  {
48  std::vector<exprt> others1, others2;
49  if(!conditions.empty())
50  {
51  others1.push_back(conjunction(conditions));
52  others2.push_back(conjunction(conditions));
53  }
54 
55  for(std::size_t j = 0; j < operands.size(); j++)
56  {
57  others1.push_back(not_exprt(operands[j]));
58  if(i != j)
59  others2.push_back(not_exprt(operands[j]));
60  else
61  others2.push_back((operands[j]));
62  }
63 
64  result.insert(conjunction(others1));
65  result.insert(conjunction(others2));
66  continue;
67  }
68 
69  std::vector<exprt> o = operands;
70 
71  // 'o[i]' needs to be true and false
72  std::vector<exprt> new_conditions = conditions;
73  new_conditions.push_back(conjunction(o));
74  result.insert(conjunction(new_conditions));
75 
76  o[i].make_not();
77  new_conditions.back() = conjunction(o);
78  result.insert(conjunction(new_conditions));
79  }
80  else
81  {
82  std::vector<exprt> others;
83  others.reserve(operands.size() - 1);
84 
85  for(std::size_t j = 0; j < operands.size(); j++)
86  if(i != j)
87  {
88  if(src.id() == ID_or)
89  others.push_back(not_exprt(operands[j]));
90  else
91  others.push_back(operands[j]);
92  }
93 
94  exprt c = conjunction(others);
95  std::vector<exprt> new_conditions = conditions;
96  new_conditions.push_back(c);
97 
98  collect_mcdc_controlling_rec(op, new_conditions, result);
99  }
100  }
101  }
102  }
103  else if(src.id() == ID_not)
104  {
105  exprt e = to_not_expr(src).op();
106  if(!is_condition(e))
107  collect_mcdc_controlling_rec(e, conditions, result);
108  else
109  {
110  // to store a copy of ''src''
111  std::vector<exprt> new_conditions1 = conditions;
112  new_conditions1.push_back(src);
113  result.insert(conjunction(new_conditions1));
114 
115  // to store a copy of its negation, i.e., ''e''
116  std::vector<exprt> new_conditions2 = conditions;
117  new_conditions2.push_back(e);
118  result.insert(conjunction(new_conditions2));
119  }
120  }
121  else
122  {
123  // It may happen that ''is_condition(src)'' is valid,
124  // but we ignore this case here as it can be handled
125  // by the routine decision/condition detection.
126  }
127 }
128 
129 std::set<exprt> collect_mcdc_controlling(const std::set<exprt> &decisions)
130 {
131  std::set<exprt> result;
132 
133  for(const auto &d : decisions)
134  collect_mcdc_controlling_rec(d, {}, result);
135 
136  return result;
137 }
138 
141 std::set<exprt> replacement_conjunction(
142  const std::set<exprt> &replacement_exprs,
143  const std::vector<exprt> &operands,
144  const std::size_t i)
145 {
146  std::set<exprt> result;
147  for(auto &y : replacement_exprs)
148  {
149  std::vector<exprt> others;
150  for(std::size_t j = 0; j < operands.size(); j++)
151  if(i != j)
152  others.push_back(operands[j]);
153 
154  others.push_back(y);
155  exprt c = conjunction(others);
156  result.insert(c);
157  }
158  return result;
159 }
160 
163 std::set<exprt>
164 collect_mcdc_controlling_nested(const std::set<exprt> &decisions)
165 {
166  // To obtain the 1st-level controlling conditions
167  std::set<exprt> controlling = collect_mcdc_controlling(decisions);
168 
169  std::set<exprt> result;
170  // For each controlling condition, to check if it contains
171  // non-atomic exprs
172  for(auto &src : controlling)
173  {
174  std::set<exprt> s1, s2;
175 
176  // The final controlling conditions resulted from ''src''
177  // will be stored in ''s1''; ''s2'' is usd to hold the
178  // temporary expansion.
179  s1.insert(src);
180 
181  // dual-loop structure to eliminate complex
182  // non-atomic-conditional terms
183  while(true)
184  {
185  bool changed = false;
186  // the 2nd loop
187  for(auto &x : s1)
188  {
189  // if ''x'' is atomic conditional term, there
190  // is no expansion
191  if(is_condition(x))
192  {
193  s2.insert(x);
194  continue;
195  }
196  // otherwise, we apply the ''nested'' method to
197  // each of its operands
198  std::vector<exprt> operands;
199  collect_operands(x, operands);
200 
201  for(std::size_t i = 0; i < operands.size(); i++)
202  {
203  std::set<exprt> res;
204  // To expand an operand if it is not atomic,
205  // and label the ''changed'' flag; the resulted
206  // expansion of such an operand is stored in ''res''.
207  if(operands[i].id() == ID_not)
208  {
209  exprt no = operands[i].op0();
210  if(!is_condition(no))
211  {
212  changed = true;
213  std::set<exprt> ctrl_no;
214  ctrl_no.insert(no);
215  res = collect_mcdc_controlling(ctrl_no);
216  }
217  }
218  else if(!is_condition(operands[i]))
219  {
220  changed = true;
221  std::set<exprt> ctrl;
222  ctrl.insert(operands[i]);
223  res = collect_mcdc_controlling(ctrl);
224  }
225 
226  // To replace a non-atomic expr with its expansion
227  std::set<exprt> co = replacement_conjunction(res, operands, i);
228  s2.insert(co.begin(), co.end());
229  if(!res.empty())
230  break;
231  }
232  // if there is no change x.r.t current operands of ''x'',
233  // i.e., they are all atomic, we reserve ''x''
234  if(!changed)
235  s2.insert(x);
236  }
237  // update ''s1'' and check if change happens
238  s1 = s2;
239  if(!changed)
240  break;
241  s2.clear();
242  }
243 
244  // The expansions of each ''src'' should be added into
245  // the ''result''
246  result.insert(s1.begin(), s1.end());
247  }
248 
249  return result;
250 }
251 
256 std::set<signed> sign_of_expr(const exprt &e, const exprt &E)
257 {
258  std::set<signed> signs;
259 
260  // At fist, we pre-screen the case such that ''E''
261  // is an atomic condition
262  if(is_condition(E))
263  {
264  if(e == E)
265  signs.insert(+1);
266  return signs;
267  }
268 
269  // or, ''E'' is the negation of ''e''?
270  if(E.id() == ID_not)
271  {
272  if(e == E.op0())
273  {
274  signs.insert(-1);
275  return signs;
276  }
277  }
278 
279  // In the general case, we analyze each operand of ''E''.
280  std::vector<exprt> ops;
281  collect_operands(E, ops);
282  for(auto &x : ops)
283  {
284  exprt y(x);
285  if(y == e)
286  signs.insert(+1);
287  else if(y.id() == ID_not)
288  {
289  y.make_not();
290  if(y == e)
291  signs.insert(-1);
292  if(!is_condition(y))
293  {
294  std::set<signed> re = sign_of_expr(e, y);
295  signs.insert(re.begin(), re.end());
296  }
297  }
298  else if(!is_condition(y))
299  {
300  std::set<signed> re = sign_of_expr(e, y);
301  signs.insert(re.begin(), re.end());
302  }
303  }
304 
305  return signs;
306 }
307 
311 void remove_repetition(std::set<exprt> &exprs)
312 {
313  // to obtain the set of atomic conditions
314  std::set<exprt> conditions;
315  for(auto &x : exprs)
316  {
317  std::set<exprt> new_conditions = collect_conditions(x);
318  conditions.insert(new_conditions.begin(), new_conditions.end());
319  }
320  // exprt that contains multiple (inconsistent) signs should
321  // be removed
322  std::set<exprt> new_exprs;
323  for(auto &x : exprs)
324  {
325  bool kept = true;
326  for(auto &c : conditions)
327  {
328  std::set<signed> signs = sign_of_expr(c, x);
329  if(signs.size() > 1)
330  {
331  kept = false;
332  break;
333  }
334  }
335  if(kept)
336  new_exprs.insert(x);
337  }
338  exprs = new_exprs;
339  new_exprs.clear();
340 
341  for(auto &x : exprs)
342  {
343  bool red = false;
344  // To check if ''x'' is identical with some
345  // expr in ''new_exprs''. Two exprs ''x''
346  // and ''y'' are identical iff they have the
347  // same sign for every atomic condition ''c''.
348  for(auto &y : new_exprs)
349  {
350  bool iden = true;
351  for(auto &c : conditions)
352  {
353  std::set<signed> signs1 = sign_of_expr(c, x);
354  std::set<signed> signs2 = sign_of_expr(c, y);
355  int s1 = signs1.size(), s2 = signs2.size();
356  // it is easy to check non-equivalence;
357  if(s1 != s2)
358  {
359  iden = false;
360  break;
361  }
362  else
363  {
364  if(s1 == 0 && s2 == 0)
365  continue;
366  // it is easy to check non-equivalence
367  if(*(signs1.begin()) != *(signs2.begin()))
368  {
369  iden = false;
370  break;
371  }
372  }
373  }
374  // If ''x'' is found identical w.r.t some
375  // expr in ''new_conditions, we label it
376  // and break.
377  if(iden)
378  {
379  red = true;
380  break;
381  }
382  }
383  // an expr is added into ''new_exprs''
384  // if it is not found repetitive
385  if(!red)
386  new_exprs.insert(x);
387  }
388 
389  // update the original ''exprs''
390  exprs = new_exprs;
391 }
392 
394 bool eval_expr(const std::map<exprt, signed> &atomic_exprs, const exprt &src)
395 {
396  std::vector<exprt> operands;
397  collect_operands(src, operands);
398  // src is AND
399  if(src.id() == ID_and)
400  {
401  for(auto &x : operands)
402  if(!eval_expr(atomic_exprs, x))
403  return false;
404  return true;
405  }
406  // src is OR
407  else if(src.id() == ID_or)
408  {
409  std::size_t fcount = 0;
410 
411  for(auto &x : operands)
412  if(!eval_expr(atomic_exprs, x))
413  fcount++;
414 
415  if(fcount < operands.size())
416  return true;
417  else
418  return false;
419  }
420  // src is NOT
421  else if(src.id() == ID_not)
422  {
423  exprt no_op(src);
424  no_op.make_not();
425  return !eval_expr(atomic_exprs, no_op);
426  }
427  else // if(is_condition(src))
428  {
429  // ''src'' should be guaranteed to be consistent
430  // with ''atomic_exprs''
431  if(atomic_exprs.find(src)->second == +1)
432  return true;
433  else // if(atomic_exprs.find(src)->second==-1)
434  return false;
435  }
436 }
437 
439 std::map<exprt, signed>
440 values_of_atomic_exprs(const exprt &e, const std::set<exprt> &conditions)
441 {
442  std::map<exprt, signed> atomic_exprs;
443  for(auto &c : conditions)
444  {
445  std::set<signed> signs = sign_of_expr(c, e);
446  if(signs.empty())
447  {
448  // ''c'' is not contained in ''e''
449  atomic_exprs.insert(std::pair<exprt, signed>(c, 0));
450  continue;
451  }
452  // we do not consider inconsistent expr ''e''
453  if(signs.size() != 1)
454  continue;
455 
456  atomic_exprs.insert(std::pair<exprt, signed>(c, *signs.begin()));
457  }
458  return atomic_exprs;
459 }
460 
466  const exprt &e1,
467  const exprt &e2,
468  const exprt &c,
469  const std::set<exprt> &conditions,
470  const exprt &decision)
471 {
472  // An controlling expr cannot be mcdc pair of itself
473  if(e1 == e2)
474  return false;
475 
476  // To obtain values of each atomic condition within ''e1''
477  // and ''e2''
478  std::map<exprt, signed> atomic_exprs_e1 =
479  values_of_atomic_exprs(e1, conditions);
480  std::map<exprt, signed> atomic_exprs_e2 =
481  values_of_atomic_exprs(e2, conditions);
482 
483  // the sign of ''c'' inside ''e1'' and ''e2''
484  signed cs1 = atomic_exprs_e1.find(c)->second;
485  signed cs2 = atomic_exprs_e2.find(c)->second;
486  // a mcdc pair should both contain ''c'', i.e., sign=+1 or -1
487  if(cs1 == 0 || cs2 == 0)
488  return false;
489 
490  // A mcdc pair regarding an atomic expr ''c''
491  // should have different values of ''c''
492  if(cs1 == cs2)
493  return false;
494 
495  // A mcdc pair should result in different ''decision''
496  if(
497  eval_expr(atomic_exprs_e1, decision) ==
498  eval_expr(atomic_exprs_e2, decision))
499  return false;
500 
501  // A mcdc pair of controlling exprs regarding ''c''
502  // can have different values for only one atomic
503  // expr, i.e., ''c''. Otherwise, they are not
504  // a mcdc pair.
505  int diff_count = 0;
506  auto e1_it = atomic_exprs_e1.begin();
507  auto e2_it = atomic_exprs_e2.begin();
508  while(e1_it != atomic_exprs_e1.end())
509  {
510  if(e1_it->second != e2_it->second)
511  diff_count++;
512  if(diff_count > 1)
513  break;
514  e1_it++;
515  e2_it++;
516  }
517 
518  if(diff_count == 1)
519  return true;
520  else
521  return false;
522 }
523 
527  const exprt &c,
528  const std::set<exprt> &expr_set,
529  const std::set<exprt> &conditions,
530  const exprt &decision)
531 {
532  for(auto y1 : expr_set)
533  {
534  for(auto y2 : expr_set)
535  {
536  if(is_mcdc_pair(y1, y2, c, conditions, decision))
537  {
538  return true;
539  }
540  }
541  }
542  return false;
543 }
544 
552  std::set<exprt> &controlling,
553  const exprt &decision)
554 {
555  // to obtain the set of atomic conditions
556  std::set<exprt> conditions;
557  for(auto &x : controlling)
558  {
559  std::set<exprt> new_conditions = collect_conditions(x);
560  conditions.insert(new_conditions.begin(), new_conditions.end());
561  }
562 
563  while(true)
564  {
565  std::set<exprt> new_controlling;
566  bool ctrl_update = false;
567  // Iteratively, we test that after removing an item ''x''
568  // from the ''controlling'', can a complete mcdc coverage
569  // over ''decision'' still be reserved?
570  //
571  // If yes, we update ''controlling'' with the
572  // ''new_controlling'' without ''x''; otherwise, we should
573  // keep ''x'' within ''controlling''.
574  //
575  // If in the end all elements ''x'' in ''controlling'' are
576  // reserved, this means that current ''controlling'' set is
577  // minimum and the ''while'' loop should be broken out of.
578  //
579  // Note: implementation here for the above procedure is
580  // not (meant to be) optimal.
581  for(auto &x : controlling)
582  {
583  // To create a new ''controlling'' set without ''x''
584  new_controlling.clear();
585  for(auto &y : controlling)
586  if(y != x)
587  new_controlling.insert(y);
588 
589  bool removing_x = true;
590  // For each atomic expr condition ''c'', to check if its is
591  // covered by at least a mcdc pair.
592  for(auto &c : conditions)
593  {
594  bool cOK = has_mcdc_pair(c, new_controlling, conditions, decision);
595  // If there is no mcdc pair for an atomic condition ''c'',
596  // then ''x'' should not be removed from the original
597  // ''controlling'' set
598  if(!cOK)
599  {
600  removing_x = false;
601  break;
602  }
603  }
604 
605  // If ''removing_x'' is valid, it is safe to remove ''x''
606  // from the original ''controlling''
607  if(removing_x)
608  {
609  ctrl_update = true;
610  break;
611  }
612  }
613  // Update ''controlling'' or break the while loop
614  if(ctrl_update)
615  {
616  controlling = new_controlling;
617  }
618  else
619  break;
620  }
621 }
622 
626  const cover_blocks_baset &) const
627 {
628  if(is_non_cover_assertion(i_it))
629  i_it->make_skip();
630 
631  // 1. Each entry and exit point is invoked
632  // 2. Each decision takes every possible outcome
633  // 3. Each condition in a decision takes every possible outcome
634  // 4. Each condition in a decision is shown to independently
635  // affect the outcome of the decision.
636  if(!i_it->source_location.is_built_in())
637  {
638  const std::set<exprt> conditions = collect_conditions(i_it);
639  const std::set<exprt> decisions = collect_decisions(i_it);
640 
641  std::set<exprt> both;
642  std::set_union(
643  conditions.begin(),
644  conditions.end(),
645  decisions.begin(),
646  decisions.end(),
647  inserter(both, both.end()));
648 
649  const source_locationt source_location = i_it->source_location;
650 
651  for(const auto &p : both)
652  {
653  bool is_decision = decisions.find(p) != decisions.end();
654  bool is_condition = conditions.find(p) != conditions.end();
655 
656  std::string description = (is_decision && is_condition)
657  ? "decision/condition"
658  : is_decision ? "decision" : "condition";
659 
660  std::string p_string = from_expr(ns, i_it->function, p);
661 
662  std::string comment_t = description + " `" + p_string + "' true";
663  const irep_idt function = i_it->function;
665  i_it->make_assertion(not_exprt(p));
666  i_it->source_location = source_location;
667  i_it->source_location.set_comment(comment_t);
668  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
669  i_it->source_location.set_property_class(property_class);
670  i_it->source_location.set_function(function);
671  i_it->function = function;
672 
673  std::string comment_f = description + " `" + p_string + "' false";
675  i_it->make_assertion(p);
676  i_it->source_location = source_location;
677  i_it->source_location.set_comment(comment_f);
678  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
679  i_it->source_location.set_property_class(property_class);
680  i_it->source_location.set_function(function);
681  i_it->function = function;
682  }
683 
684  std::set<exprt> controlling;
685  controlling = collect_mcdc_controlling_nested(decisions);
686  remove_repetition(controlling);
687  // for now, we restrict to the case of a single ''decision'';
688  // however, this is not true, e.g., ''? :'' operator.
689  if(!decisions.empty())
690  {
691  minimize_mcdc_controlling(controlling, *decisions.begin());
692  }
693 
694  for(const auto &p : controlling)
695  {
696  std::string p_string = from_expr(ns, i_it->function, p);
697 
698  std::string description =
699  "MC/DC independence condition `" + p_string + "'";
700 
701  const irep_idt function = i_it->function;
703  i_it->make_assertion(not_exprt(p));
704  i_it->source_location = source_location;
705  i_it->source_location.set_comment(description);
706  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
707  i_it->source_location.set_property_class(property_class);
708  i_it->source_location.set_function(function);
709  i_it->function = function;
710  }
711 
712  for(std::size_t i = 0; i < both.size() * 2 + controlling.size(); i++)
713  i_it++;
714  }
715 }
std::set< exprt > collect_decisions(const exprt &src)
Definition: cover_util.cpp:109
Boolean negation.
Definition: std_expr.h:3228
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:441
void collect_operands(const exprt &src, std::vector< exprt > &dest)
Definition: cover_util.cpp:69
exprt & op0()
Definition: expr.h:72
const exprt & op() const
Definition: std_expr.h:340
void set_comment(const irep_idt &comment)
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...
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
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;.
Coverage Instrumentation.
bool is_condition(const exprt &src)
Definition: cover_util.cpp:14
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:48
const irep_idt & id() const
Definition: irep.h:259
std::set< exprt > collect_conditions(const exprt &src)
Definition: cover_util.cpp:42
void minimize_mcdc_controlling(std::set< exprt > &controlling, const exprt &decision)
This method minimizes the controlling conditions for mcdc coverage.
instructionst::iterator targett
Definition: goto_program.h:397
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;.
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.
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.
const irep_idt coverage_criterion
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;...
Coverage Instrumentation Utilities.
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
std::set< exprt > collect_mcdc_controlling(const std::set< exprt > &decisions)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
void make_not()
Definition: expr.cpp:91
Base class for all expressions.
Definition: expr.h:42
const irep_idt property_class
const not_exprt & to_not_expr(const exprt &expr)
Cast a generic exprt to an not_exprt.
Definition: std_expr.h:3252
goto_programt & goto_program
Definition: cover.cpp:63
int8_t s1
Definition: bytecode_info.h:59
int16_t s2
Definition: bytecode_info.h:60
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;...
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...
bool is_non_cover_assertion(goto_programt::const_targett t) const