27 bool next_is_target=
true;
28 unsigned block_count=0;
32 if(next_is_target || it->is_target())
37 if(!it->source_location.is_nil() &&
42 it->is_goto() || it->is_function_call() || it->is_assume();
47 typedef std::map<goto_programt::const_targett, unsigned>
block_mapt;
61 for(block_mapt::const_iterator
62 b_it=block_map.begin();
63 b_it!=block_map.end();
65 out << b_it->first->source_location
66 <<
" -> " << b_it->second
89 if(src.
type().
id()!=ID_bool)
93 if(src.
id()==ID_and || src.
id()==ID_or ||
94 src.
id()==ID_not || src.
id()==ID_implies)
102 if(src.
id()==ID_address_of)
107 for(
const auto &op : src.
operands())
116 std::set<exprt> result;
138 return std::set<exprt>();
145 if(op.id()==src.
id())
155 const std::vector<exprt> &conditions,
156 std::set<exprt> &result)
159 if(src.
id()==ID_and ||
162 std::vector<exprt> operands;
165 if(operands.size()==1)
167 exprt e=*operands.begin();
170 else if(!operands.empty())
172 for(std::size_t i=0; i<operands.size(); i++)
174 const exprt op=operands[i];
180 std::vector<exprt> others1, others2;
181 if(!conditions.empty())
187 for(std::size_t j=0; j<operands.size(); j++)
189 others1.push_back(
not_exprt(operands[j]));
191 others2.push_back(
not_exprt(operands[j]));
193 others2.push_back((operands[j]));
201 std::vector<exprt> o=operands;
204 std::vector<exprt> new_conditions=conditions;
214 std::vector<exprt> others;
215 others.reserve(operands.size()-1);
217 for(std::size_t j=0; j<operands.size(); j++)
221 others.push_back(
not_exprt(operands[j]));
223 others.push_back(operands[j]);
227 std::vector<exprt> new_conditions=conditions;
228 new_conditions.push_back(c);
235 else if(src.
id()==ID_not)
243 std::vector<exprt> new_conditions1=conditions;
244 new_conditions1.push_back(src);
248 std::vector<exprt> new_conditions2=conditions;
249 new_conditions2.push_back(e);
264 const std::set<exprt> &decisions)
266 std::set<exprt> result;
268 for(
const auto &d : decisions)
277 const std::set<exprt> &replacement_exprs,
278 const std::vector<exprt> &operands,
281 std::set<exprt> result;
282 for(
auto &y : replacement_exprs)
284 std::vector<exprt> others;
285 for(std::size_t j=0; j<operands.size(); j++)
287 others.push_back(operands[j]);
299 const std::set<exprt> &decisions)
304 std::set<exprt> result;
307 for(
auto &src : controlling)
309 std::set<exprt>
s1,
s2;
334 std::vector<exprt> operands;
337 for(std::size_t i=0; i<operands.size(); i++)
345 if(operands[i].
id()==ID_not)
347 exprt no=operands[i].op0();
351 std::set<exprt> ctrl_no;
359 std::set<exprt> ctrl;
360 ctrl.insert(operands[i]);
367 s2.insert(co.begin(), co.end());
385 result.insert(s1.begin(), s1.end());
397 std::set<signed> signs;
421 std::vector<exprt> ops;
428 else if(y.
id()==ID_not)
436 signs.insert(re.begin(), re.end());
442 signs.insert(re.begin(), re.end());
455 std::set<exprt> conditions;
459 conditions.insert(new_conditions.begin(), new_conditions.end());
463 std::set<exprt> new_exprs;
467 for(
auto &c : conditions)
491 for(
auto &y : new_exprs)
494 for(
auto &c : conditions)
498 int s1=signs1.size(),
s2=signs2.size();
510 if(*(signs1.begin())!=*(signs2.begin()))
540 const std::map<exprt, signed> &atomic_exprs,
543 std::vector<exprt> operands;
548 for(
auto &x : operands)
554 else if(src.
id()==ID_or)
556 std::size_t fcount=0;
558 for(
auto &x : operands)
562 if(fcount<operands.size())
568 else if(src.
id()==ID_not)
578 if(atomic_exprs.find(src)->second==+1)
588 const std::set<exprt> &conditions)
590 std::map<exprt, signed> atomic_exprs;
591 for(
auto &c : conditions)
597 atomic_exprs.insert(std::pair<exprt, signed>(c, 0));
605 std::pair<exprt, signed>(c, *signs.begin()));
618 const std::set<exprt> &conditions,
619 const exprt &decision)
627 std::map<exprt, signed> atomic_exprs_e1=
629 std::map<exprt, signed> atomic_exprs_e2=
633 signed cs1=atomic_exprs_e1.find(c)->second;
634 signed cs2=atomic_exprs_e2.find(c)->second;
645 if(
eval_expr(atomic_exprs_e1, decision)==
656 auto e1_it=atomic_exprs_e1.begin();
657 auto e2_it=atomic_exprs_e2.begin();
658 while(e1_it!=atomic_exprs_e1.end())
660 if(e1_it->second!=e2_it->second)
677 const std::set<exprt> &expr_set,
678 const std::set<exprt> &conditions,
679 const exprt &decision)
681 for(
auto y1 : expr_set)
683 for(
auto y2 : expr_set)
701 std::set<exprt> &controlling,
702 const exprt &decision)
705 std::set<exprt> conditions;
706 for(
auto &x : controlling)
709 conditions.insert(new_conditions.begin(), new_conditions.end());
714 std::set<exprt> new_controlling;
715 bool ctrl_update=
false;
732 for(
auto &x : controlling)
735 new_controlling.clear();
736 for(
auto &y : controlling)
738 new_controlling.insert(y);
740 bool removing_x=
true;
743 for(
auto &c : conditions)
770 controlling=new_controlling;
778 if(src.
id()==ID_address_of)
783 if(src.
type().
id()==ID_bool)
789 else if(src.
id()==ID_not)
800 for(
const auto &op : src.
operands())
807 std::set<exprt> result;
829 return std::set<exprt>();
839 std::set<unsigned> blocks_done;
843 goto_program.
instructions.front().source_location.is_built_in())
847 const irep_idt property_class=
"coverage";
855 if(i_it->is_assert())
858 i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
859 i_it->source_location.set_property_class(property_class);
865 if(i_it->is_function_call())
869 if(code_function_call.
function().
id()==ID_symbol &&
872 code_function_call.
arguments().size()==1)
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);
884 else if(i_it->is_assert())
889 if(i_it->is_assert())
893 unsigned block_nr=basic_blocks[i_it];
894 if(blocks_done.insert(block_nr).second)
896 std::string b=std::to_string(block_nr);
897 std::string
id=
id2string(i_it->function)+
"#"+b;
904 std::string
comment=
"block "+b;
907 i_it->source_location=source_location;
909 i_it->source_location.set(
910 ID_coverage_criterion, coverage_criterion);
911 i_it->source_location.set_property_class(property_class);
920 if(i_it->is_assert())
928 "function "+
id2string(i_it->function)+
" entry point";
934 t->source_location=source_location;
936 t->source_location.set(ID_coverage_criterion, coverage_criterion);
937 t->source_location.set_property_class(property_class);
940 if(i_it->is_goto() && !i_it->guard.is_true() &&
941 !i_it->source_location.is_built_in())
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";
949 exprt guard=i_it->guard;
954 i_it->source_location=source_location;
956 i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
957 i_it->source_location.set_property_class(property_class);
960 i_it->make_assertion(guard);
961 i_it->source_location=source_location;
963 i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
964 i_it->source_location.set_property_class(property_class);
972 if(i_it->is_assert())
976 if(!i_it->source_location.is_built_in())
982 for(
const auto &c : conditions)
984 const std::string c_string=
from_expr(ns,
"", c);
986 const std::string comment_t=
"condition `"+c_string+
"' true";
988 i_it->make_assertion(c);
989 i_it->source_location=source_location;
991 i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
992 i_it->source_location.set_property_class(property_class);
994 const std::string comment_f=
"condition `"+c_string+
"' false";
997 i_it->source_location=source_location;
999 i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
1000 i_it->source_location.set_property_class(property_class);
1003 for(std::size_t i=0; i<conditions.size()*2; i++)
1009 if(i_it->is_assert())
1013 if(!i_it->source_location.is_built_in())
1019 for(
const auto &d : decisions)
1021 const std::string d_string=
from_expr(ns,
"", d);
1023 const std::string comment_t=
"decision `"+d_string+
"' true";
1025 i_it->make_assertion(d);
1026 i_it->source_location=source_location;
1028 i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
1029 i_it->source_location.set_property_class(property_class);
1031 const std::string comment_f=
"decision `"+d_string+
"' false";
1034 i_it->source_location=source_location;
1036 i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
1037 i_it->source_location.set_property_class(property_class);
1040 for(std::size_t i=0; i<decisions.size()*2; i++)
1046 if(i_it->is_assert())
1054 if(!i_it->source_location.is_built_in())
1059 std::set<exprt> both;
1060 std::set_union(conditions.begin(), conditions.end(),
1061 decisions.begin(), decisions.end(),
1062 inserter(both, both.end()));
1066 for(
const auto &p : both)
1068 bool is_decision=decisions.find(p)!=decisions.end();
1069 bool is_condition=conditions.find(p)!=conditions.end();
1071 std::string description=
1073 is_decision?
"decision":
"condition";
1075 std::string p_string=
from_expr(ns,
"", p);
1077 std::string comment_t=description+
" `"+p_string+
"' true";
1081 i_it->source_location=source_location;
1083 i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
1084 i_it->source_location.set_property_class(property_class);
1086 std::string comment_f=description+
" `"+p_string+
"' false";
1089 i_it->make_assertion(p);
1090 i_it->source_location=source_location;
1092 i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
1093 i_it->source_location.set_property_class(property_class);
1096 std::set<exprt> controlling;
1104 for(
const auto &p : controlling)
1106 std::string p_string=
from_expr(ns,
"", p);
1108 std::string description=
1109 "MC/DC independence condition `"+p_string+
"'";
1114 i_it->source_location=source_location;
1116 i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
1117 i_it->source_location.set_property_class(property_class);
1120 for(std::size_t i=0; i<both.size()*2+controlling.size(); i++)
1126 if(i_it->is_assert())
1145 f_it->first==
"__CPROVER_initialize" ||
1146 f_it->second.is_hidden())
1160 std::list<std::string> criteria_strings=cmdline.
get_values(
"cover");
1161 std::set<coverage_criteriont> criteria;
1162 bool keep_assertions=
false;
1164 for(
const auto &criterion_string : criteria_strings)
1168 if(criterion_string==
"assertion" || criterion_string==
"assertions")
1170 keep_assertions=
true;
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")
1189 msg.
error() <<
"unknown coverage criterion " 1190 <<
'\'' << criterion_string <<
'\'' 1198 if(keep_assertions && criteria_strings.size()>1)
1200 msg.
error() <<
"assertion coverage cannot currently be used together with " 1205 msg.
status() <<
"Rewriting existing assertions as assumptions" 1208 if(!keep_assertions)
1216 if(i_it->is_assert())
1224 for(
const auto &criterion : criteria)
const std::list< std::string > & get_values(const std::string &option) const
void collect_operands(const exprt &src, std::vector< exprt > &dest)
basic_blockst(const goto_programt &_goto_program)
void minimize_mcdc_controlling(std::set< exprt > &controlling, const exprt &decision)
This method minimizes the controlling conditions for mcdc coverage.
std::set< exprt > collect_conditions(const exprt &src)
const std::string & id2string(const irep_idt &d)
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...
static bool is_built_in(const std::string &s)
std::string comment(const rw_set_baset::entryt &entry, bool write)
std::set< exprt > collect_mcdc_controlling(const std::set< exprt > &decisions)
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.
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 ''src'', according to the atomic expr values.
static mstreamt & eom(mstreamt &m)
unsigned operator[](goto_programt::const_targett t)
const char * as_string(coverage_criteriont c)
exprt conjunction(const exprt::operandst &op)
const irep_idt & id() const
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.
instructionst::const_iterator const_targett
std::map< goto_programt::const_targett, unsigned > block_mapt
std::map< unsigned, source_locationt > source_location_mapt
static irep_idt entry_point()
void instrument_cover_goals(const symbol_tablet &symbol_table, goto_programt &goto_program, coverage_criteriont criterion)
void collect_decisions_rec(const exprt &src, std::set< exprt > &dest)
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''...
The boolean constant false.
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.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
const irep_idt & get_file() const
std::set< signed > sign_of_expr(const exprt &e, const exprt &E)
The sign of expr ''e'' within the super-expr ''E''.
void basic_blocks(goto_programt &goto_program, unsigned max_block_size)
convert basic blocks into single expressions of type "block"
void output(std::ostream &out)
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
#define Forall_goto_functions(it, functions)
source_location_mapt source_location_map
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
#define Forall_goto_program_instructions(it, program)
bool is_condition(const exprt &src)
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''...
std::set< exprt > collect_decisions(const exprt &src)
void collect_conditions_rec(const exprt &src, std::set< exprt > &dest)
#define forall_goto_program_instructions(it, program)
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...
const code_function_callt & to_code_function_call(const codet &code)
instructionst::iterator targett