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