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  {
128  }
129 }
130 
131 std::set<exprt> collect_mcdc_controlling(const std::set<exprt> &decisions)
132 {
133  std::set<exprt> result;
134 
135  for(const auto &d : decisions)
136  collect_mcdc_controlling_rec(d, {}, result);
137 
138  return result;
139 }
140 
143 std::set<exprt> replacement_conjunction(
144  const std::set<exprt> &replacement_exprs,
145  const std::vector<exprt> &operands,
146  const std::size_t i)
147 {
148  std::set<exprt> result;
149  for(auto &y : replacement_exprs)
150  {
151  std::vector<exprt> others;
152  for(std::size_t j = 0; j < operands.size(); j++)
153  if(i != j)
154  others.push_back(operands[j]);
155 
156  others.push_back(y);
157  exprt c = conjunction(others);
158  result.insert(c);
159  }
160  return result;
161 }
162 
165 std::set<exprt>
166 collect_mcdc_controlling_nested(const std::set<exprt> &decisions)
167 {
168  // To obtain the 1st-level controlling conditions
169  std::set<exprt> controlling = collect_mcdc_controlling(decisions);
170 
171  std::set<exprt> result;
172  // For each controlling condition, to check if it contains
173  // non-atomic exprs
174  for(auto &src : controlling)
175  {
176  std::set<exprt> s1, s2;
182  s1.insert(src);
183 
184  // dual-loop structure to eliminate complex
185  // non-atomic-conditional terms
186  while(true)
187  {
188  bool changed = false;
189  // the 2nd loop
190  for(auto &x : s1)
191  {
192  // if ''x'' is atomic conditional term, there
193  // is no expansion
194  if(is_condition(x))
195  {
196  s2.insert(x);
197  continue;
198  }
199  // otherwise, we apply the ''nested'' method to
200  // each of its operands
201  std::vector<exprt> operands;
202  collect_operands(x, operands);
203 
204  for(std::size_t i = 0; i < operands.size(); i++)
205  {
206  std::set<exprt> res;
212  if(operands[i].id() == ID_not)
213  {
214  exprt no = operands[i].op0();
215  if(!is_condition(no))
216  {
217  changed = true;
218  std::set<exprt> ctrl_no;
219  ctrl_no.insert(no);
220  res = collect_mcdc_controlling(ctrl_no);
221  }
222  }
223  else if(!is_condition(operands[i]))
224  {
225  changed = true;
226  std::set<exprt> ctrl;
227  ctrl.insert(operands[i]);
228  res = collect_mcdc_controlling(ctrl);
229  }
230 
231  // To replace a non-atomic expr with its expansion
232  std::set<exprt> co = replacement_conjunction(res, operands, i);
233  s2.insert(co.begin(), co.end());
234  if(!res.empty())
235  break;
236  }
237  // if there is no change x.r.t current operands of ''x'',
238  // i.e., they are all atomic, we reserve ''x''
239  if(!changed)
240  s2.insert(x);
241  }
242  // update ''s1'' and check if change happens
243  s1 = s2;
244  if(!changed)
245  break;
246  s2.clear();
247  }
248 
249  // The expansions of each ''src'' should be added into
250  // the ''result''
251  result.insert(s1.begin(), s1.end());
252  }
253 
254  return result;
255 }
256 
261 std::set<signed> sign_of_expr(const exprt &e, const exprt &E)
262 {
263  std::set<signed> signs;
264 
265  // At fist, we pre-screen the case such that ''E''
266  // is an atomic condition
267  if(is_condition(E))
268  {
269  if(e == E)
270  signs.insert(+1);
271  return signs;
272  }
273 
274  // or, ''E'' is the negation of ''e''?
275  if(E.id() == ID_not)
276  {
277  if(e == E.op0())
278  {
279  signs.insert(-1);
280  return signs;
281  }
282  }
283 
287  std::vector<exprt> ops;
288  collect_operands(E, ops);
289  for(auto &x : ops)
290  {
291  exprt y(x);
292  if(y == e)
293  signs.insert(+1);
294  else if(y.id() == ID_not)
295  {
296  y.make_not();
297  if(y == e)
298  signs.insert(-1);
299  if(!is_condition(y))
300  {
301  std::set<signed> re = sign_of_expr(e, y);
302  signs.insert(re.begin(), re.end());
303  }
304  }
305  else if(!is_condition(y))
306  {
307  std::set<signed> re = sign_of_expr(e, y);
308  signs.insert(re.begin(), re.end());
309  }
310  }
311 
312  return signs;
313 }
314 
318 void remove_repetition(std::set<exprt> &exprs)
319 {
320  // to obtain the set of atomic conditions
321  std::set<exprt> conditions;
322  for(auto &x : exprs)
323  {
324  std::set<exprt> new_conditions = collect_conditions(x);
325  conditions.insert(new_conditions.begin(), new_conditions.end());
326  }
327  // exprt that contains multiple (inconsistent) signs should
328  // be removed
329  std::set<exprt> new_exprs;
330  for(auto &x : exprs)
331  {
332  bool kept = true;
333  for(auto &c : conditions)
334  {
335  std::set<signed> signs = sign_of_expr(c, x);
336  if(signs.size() > 1)
337  {
338  kept = false;
339  break;
340  }
341  }
342  if(kept)
343  new_exprs.insert(x);
344  }
345  exprs = new_exprs;
346  new_exprs.clear();
347 
348  for(auto &x : exprs)
349  {
350  bool red = false;
357  for(auto &y : new_exprs)
358  {
359  bool iden = true;
360  for(auto &c : conditions)
361  {
362  std::set<signed> signs1 = sign_of_expr(c, x);
363  std::set<signed> signs2 = sign_of_expr(c, y);
364  int s1 = signs1.size(), s2 = signs2.size();
365  // it is easy to check non-equivalence;
366  if(s1 != s2)
367  {
368  iden = false;
369  break;
370  }
371  else
372  {
373  if(s1 == 0 && s2 == 0)
374  continue;
375  // it is easy to check non-equivalence
376  if(*(signs1.begin()) != *(signs2.begin()))
377  {
378  iden = false;
379  break;
380  }
381  }
382  }
388  if(iden)
389  {
390  red = true;
391  break;
392  }
393  }
394  // an expr is added into ''new_exprs''
395  // if it is not found repetitive
396  if(!red)
397  new_exprs.insert(x);
398  }
399 
400  // update the original ''exprs''
401  exprs = new_exprs;
402 }
403 
405 bool eval_expr(const std::map<exprt, signed> &atomic_exprs, const exprt &src)
406 {
407  std::vector<exprt> operands;
408  collect_operands(src, operands);
409  // src is AND
410  if(src.id() == ID_and)
411  {
412  for(auto &x : operands)
413  if(!eval_expr(atomic_exprs, x))
414  return false;
415  return true;
416  }
417  // src is OR
418  else if(src.id() == ID_or)
419  {
420  std::size_t fcount = 0;
421 
422  for(auto &x : operands)
423  if(!eval_expr(atomic_exprs, x))
424  fcount++;
425 
426  if(fcount < operands.size())
427  return true;
428  else
429  return false;
430  }
431  // src is NOT
432  else if(src.id() == ID_not)
433  {
434  exprt no_op(src);
435  no_op.make_not();
436  return !eval_expr(atomic_exprs, no_op);
437  }
438  else // if(is_condition(src))
439  {
440  // ''src'' should be guaranteed to be consistent
441  // with ''atomic_exprs''
442  if(atomic_exprs.find(src)->second == +1)
443  return true;
444  else // if(atomic_exprs.find(src)->second==-1)
445  return false;
446  }
447 }
448 
450 std::map<exprt, signed>
451 values_of_atomic_exprs(const exprt &e, const std::set<exprt> &conditions)
452 {
453  std::map<exprt, signed> atomic_exprs;
454  for(auto &c : conditions)
455  {
456  std::set<signed> signs = sign_of_expr(c, e);
457  if(signs.empty())
458  {
459  // ''c'' is not contained in ''e''
460  atomic_exprs.insert(std::pair<exprt, signed>(c, 0));
461  continue;
462  }
463  // we do not consider inconsistent expr ''e''
464  if(signs.size() != 1)
465  continue;
466 
467  atomic_exprs.insert(std::pair<exprt, signed>(c, *signs.begin()));
468  }
469  return atomic_exprs;
470 }
471 
477  const exprt &e1,
478  const exprt &e2,
479  const exprt &c,
480  const std::set<exprt> &conditions,
481  const exprt &decision)
482 {
483  // An controlling expr cannot be mcdc pair of itself
484  if(e1 == e2)
485  return false;
486 
487  // To obtain values of each atomic condition within ''e1''
488  // and ''e2''
489  std::map<exprt, signed> atomic_exprs_e1 =
490  values_of_atomic_exprs(e1, conditions);
491  std::map<exprt, signed> atomic_exprs_e2 =
492  values_of_atomic_exprs(e2, conditions);
493 
494  // the sign of ''c'' inside ''e1'' and ''e2''
495  signed cs1 = atomic_exprs_e1.find(c)->second;
496  signed cs2 = atomic_exprs_e2.find(c)->second;
497  // a mcdc pair should both contain ''c'', i.e., sign=+1 or -1
498  if(cs1 == 0 || cs2 == 0)
499  return false;
500 
501  // A mcdc pair regarding an atomic expr ''c''
502  // should have different values of ''c''
503  if(cs1 == cs2)
504  return false;
505 
506  // A mcdc pair should result in different ''decision''
507  if(
508  eval_expr(atomic_exprs_e1, decision) ==
509  eval_expr(atomic_exprs_e2, decision))
510  return false;
511 
518  int diff_count = 0;
519  auto e1_it = atomic_exprs_e1.begin();
520  auto e2_it = atomic_exprs_e2.begin();
521  while(e1_it != atomic_exprs_e1.end())
522  {
523  if(e1_it->second != e2_it->second)
524  diff_count++;
525  if(diff_count > 1)
526  break;
527  e1_it++;
528  e2_it++;
529  }
530 
531  if(diff_count == 1)
532  return true;
533  else
534  return false;
535 }
536 
540  const exprt &c,
541  const std::set<exprt> &expr_set,
542  const std::set<exprt> &conditions,
543  const exprt &decision)
544 {
545  for(auto y1 : expr_set)
546  {
547  for(auto y2 : expr_set)
548  {
549  if(is_mcdc_pair(y1, y2, c, conditions, decision))
550  {
551  return true;
552  }
553  }
554  }
555  return false;
556 }
557 
565  std::set<exprt> &controlling,
566  const exprt &decision)
567 {
568  // to obtain the set of atomic conditions
569  std::set<exprt> conditions;
570  for(auto &x : controlling)
571  {
572  std::set<exprt> new_conditions = collect_conditions(x);
573  conditions.insert(new_conditions.begin(), new_conditions.end());
574  }
575 
576  while(true)
577  {
578  std::set<exprt> new_controlling;
579  bool ctrl_update = false;
596  for(auto &x : controlling)
597  {
598  // To create a new ''controlling'' set without ''x''
599  new_controlling.clear();
600  for(auto &y : controlling)
601  if(y != x)
602  new_controlling.insert(y);
603 
604  bool removing_x = true;
605  // For each atomic expr condition ''c'', to check if its is
606  // covered by at least a mcdc pair.
607  for(auto &c : conditions)
608  {
609  bool cOK = has_mcdc_pair(c, new_controlling, conditions, decision);
615  if(!cOK)
616  {
617  removing_x = false;
618  break;
619  }
620  }
621 
622  // If ''removing_x'' is valid, it is safe to remove ''x''
623  // from the original ''controlling''
624  if(removing_x)
625  {
626  ctrl_update = true;
627  break;
628  }
629  }
630  // Update ''controlling'' or break the while loop
631  if(ctrl_update)
632  {
633  controlling = new_controlling;
634  }
635  else
636  break;
637  }
638 }
639 
643  const cover_blocks_baset &basic_blocks) const
644 {
645  if(is_non_cover_assertion(i_it))
646  i_it->make_skip();
647 
648  // 1. Each entry and exit point is invoked
649  // 2. Each decision takes every possible outcome
650  // 3. Each condition in a decision takes every possible outcome
651  // 4. Each condition in a decision is shown to independently
652  // affect the outcome of the decision.
653  if(!i_it->source_location.is_built_in())
654  {
655  const std::set<exprt> conditions = collect_conditions(i_it);
656  const std::set<exprt> decisions = collect_decisions(i_it);
657 
658  std::set<exprt> both;
659  std::set_union(
660  conditions.begin(),
661  conditions.end(),
662  decisions.begin(),
663  decisions.end(),
664  inserter(both, both.end()));
665 
666  const source_locationt source_location = i_it->source_location;
667 
668  for(const auto &p : both)
669  {
670  bool is_decision = decisions.find(p) != decisions.end();
671  bool is_condition = conditions.find(p) != conditions.end();
672 
673  std::string description = (is_decision && is_condition)
674  ? "decision/condition"
675  : is_decision ? "decision" : "condition";
676 
677  std::string p_string = from_expr(ns, i_it->function, p);
678 
679  std::string comment_t = description + " `" + p_string + "' true";
680  const irep_idt function = i_it->function;
682  // i_it->make_assertion(p);
683  i_it->make_assertion(not_exprt(p));
684  i_it->source_location = source_location;
685  i_it->source_location.set_comment(comment_t);
686  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
687  i_it->source_location.set_property_class(property_class);
688  i_it->source_location.set_function(function);
689  i_it->function = function;
690 
691  std::string comment_f = description + " `" + p_string + "' false";
693  // i_it->make_assertion(not_exprt(p));
694  i_it->make_assertion(p);
695  i_it->source_location = source_location;
696  i_it->source_location.set_comment(comment_f);
697  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
698  i_it->source_location.set_property_class(property_class);
699  i_it->source_location.set_function(function);
700  i_it->function = function;
701  }
702 
703  std::set<exprt> controlling;
704  // controlling=collect_mcdc_controlling(decisions);
705  controlling = collect_mcdc_controlling_nested(decisions);
706  remove_repetition(controlling);
707  // for now, we restrict to the case of a single ''decision'';
708  // however, this is not true, e.g., ''? :'' operator.
709  INVARIANT(!decisions.empty(), "There must be at least one decision");
710  minimize_mcdc_controlling(controlling, *decisions.begin());
711 
712  for(const auto &p : controlling)
713  {
714  std::string p_string = from_expr(ns, i_it->function, p);
715 
716  std::string description =
717  "MC/DC independence condition `" + p_string + "'";
718 
719  const irep_idt function = i_it->function;
721  i_it->make_assertion(not_exprt(p));
722  // i_it->make_assertion(p);
723  i_it->source_location = source_location;
724  i_it->source_location.set_comment(description);
725  i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
726  i_it->source_location.set_property_class(property_class);
727  i_it->source_location.set_function(function);
728  i_it->function = function;
729  }
730 
731  for(std::size_t i = 0; i < both.size() * 2 + controlling.size(); i++)
732  i_it++;
733  }
734 }
std::set< exprt > collect_decisions(const exprt &src)
Definition: cover_util.cpp:109
Boolean negation.
Definition: std_expr.h:3230
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
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:48
const irep_idt & id() const
Definition: irep.h:189
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.
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:3254
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