Skip to content

Commit a7f0c3d

Browse files
peterschrammelpeterschrammel
committed
Introduce cover instrumenter
1 parent 873627a commit a7f0c3d

8 files changed

+360
-177
lines changed

‎src/goto-instrument/cover.cpp

+107-97
Original file line numberDiff line numberDiff line change
@@ -28,92 +28,124 @@ Date: May 2016
2828
#include "cover_instrument.h"
2929

3030
void instrument_cover_goals(
31-
const symbol_tablet &symbol_table,
3231
goto_programt &goto_program,
33-
coverage_criteriont criterion,
34-
message_handlert &message_handler,
35-
const goal_filterst &goal_filters)
32+
const cover_instrumenterst &instrumenters,
33+
message_handlert &message_handler)
3634
{
37-
const namespacet ns(symbol_table);
3835
cover_basic_blockst basic_blocks(goto_program);
3936
basic_blocks.select_unique_java_bytecode_indices(
4037
goto_program, message_handler);
4138
basic_blocks.report_block_anomalies(goto_program, message_handler);
4239

43-
Forall_goto_program_instructions(i_it, goto_program)
44-
{
45-
switch(criterion)
46-
{
47-
case coverage_criteriont::ASSERTION:
48-
cover_instrument_assertion(i_it);
49-
break;
50-
51-
case coverage_criteriont::COVER:
52-
cover_instrument_cover(ns, i_it);
53-
break;
54-
55-
case coverage_criteriont::LOCATION:
56-
cover_instrument_location(goto_program, i_it, basic_blocks, goal_filters);
57-
break;
40+
instrumenters(goto_program, basic_blocks);
41+
}
5842

59-
case coverage_criteriont::BRANCH:
60-
cover_instrument_branch(goto_program, i_it, basic_blocks);
61-
break;
43+
void instrument_cover_goals(
44+
const symbol_tablet &symbol_table,
45+
goto_programt &goto_program,
46+
coverage_criteriont criterion,
47+
message_handlert &message_handler)
48+
{
49+
goal_filterst goal_filters;
50+
goal_filters.add(util_make_unique<internal_goals_filtert>(message_handler));
6251

63-
case coverage_criteriont::CONDITION:
64-
cover_instrument_condition(ns, goto_program, i_it);
65-
break;
52+
cover_instrumenterst instrumenters;
53+
instrumenters.add_from_criterion(criterion, symbol_table, goal_filters);
6654

67-
case coverage_criteriont::DECISION:
68-
cover_instrument_decision(ns, goto_program, i_it);
69-
break;
55+
instrument_cover_goals(goto_program, instrumenters, message_handler);
56+
}
7057

71-
case coverage_criteriont::MCDC:
72-
cover_instrument_mcdc(ns, goto_program, i_it);
73-
break;
58+
void cover_instrumenterst::add_from_criterion(
59+
coverage_criteriont criterion,
60+
const symbol_tablet &symbol_table,
61+
const goal_filterst &goal_filters)
62+
{
63+
switch(criterion)
64+
{
65+
case coverage_criteriont::LOCATION:
66+
instrumenters.push_back(
67+
util_make_unique<cover_location_instrumentert>(
68+
symbol_table, goal_filters));
69+
break;
70+
case coverage_criteriont::BRANCH:
71+
instrumenters.push_back(
72+
util_make_unique<cover_branch_instrumentert>(symbol_table, goal_filters));
73+
break;
74+
case coverage_criteriont::DECISION:
75+
instrumenters.push_back(
76+
util_make_unique<cover_decision_instrumentert>(
77+
symbol_table, goal_filters));
78+
break;
79+
case coverage_criteriont::CONDITION:
80+
instrumenters.push_back(
81+
util_make_unique<cover_condition_instrumentert>(
82+
symbol_table, goal_filters));
83+
break;
84+
case coverage_criteriont::PATH:
85+
instrumenters.push_back(
86+
util_make_unique<cover_path_instrumentert>(symbol_table, goal_filters));
87+
break;
88+
case coverage_criteriont::MCDC:
89+
instrumenters.push_back(
90+
util_make_unique<cover_mcdc_instrumentert>(symbol_table, goal_filters));
91+
break;
92+
case coverage_criteriont::ASSERTION:
93+
instrumenters.push_back(
94+
util_make_unique<cover_assertion_instrumentert>(
95+
symbol_table, goal_filters));
96+
break;
97+
case coverage_criteriont::COVER:
98+
instrumenters.push_back(
99+
util_make_unique<cover_cover_instrumentert>(symbol_table, goal_filters));
100+
}
101+
}
74102

75-
case coverage_criteriont::PATH:
76-
cover_instrument_path(i_it);
77-
break;
78-
}
103+
coverage_criteriont
104+
parse_coverage_criterion(const std::string &criterion_string)
105+
{
106+
coverage_criteriont c;
107+
108+
if(criterion_string == "assertion" || criterion_string == "assertions")
109+
c = coverage_criteriont::ASSERTION;
110+
else if(criterion_string == "path" || criterion_string == "paths")
111+
c = coverage_criteriont::PATH;
112+
else if(criterion_string == "branch" || criterion_string == "branches")
113+
c = coverage_criteriont::BRANCH;
114+
else if(criterion_string == "location" || criterion_string == "locations")
115+
c = coverage_criteriont::LOCATION;
116+
else if(criterion_string == "decision" || criterion_string == "decisions")
117+
c = coverage_criteriont::DECISION;
118+
else if(criterion_string == "condition" || criterion_string == "conditions")
119+
c = coverage_criteriont::CONDITION;
120+
else if(criterion_string == "mcdc")
121+
c = coverage_criteriont::MCDC;
122+
else if(criterion_string == "cover")
123+
c = coverage_criteriont::COVER;
124+
else
125+
{
126+
std::stringstream s;
127+
s << "unknown coverage criterion " << '\'' << criterion_string << '\'';
128+
throw s.str();
79129
}
130+
131+
return c;
80132
}
81133

82134
void instrument_cover_goals(
83-
const symbol_tablet &symbol_table,
84135
goto_functionst &goto_functions,
85-
coverage_criteriont criterion,
86-
message_handlert &message_handler,
136+
const cover_instrumenterst &instrumenters,
87137
const function_filterst &function_filters,
88-
const goal_filterst &goal_filters)
138+
message_handlert &message_handler)
89139
{
90140
Forall_goto_functions(f_it, goto_functions)
91141
{
92142
if(!function_filters(f_it->first, f_it->second))
93143
continue;
94144

95-
instrument_cover_goals(
96-
symbol_table,
97-
f_it->second.body,
98-
criterion,
99-
message_handler,
100-
goal_filters);
145+
instrument_cover_goals(f_it->second.body, instrumenters, message_handler);
101146
}
102147
}
103148

104-
void instrument_cover_goals(
105-
const symbol_tablet &symbol_table,
106-
goto_programt &goto_program,
107-
coverage_criteriont criterion,
108-
message_handlert &message_handler)
109-
{
110-
goal_filterst goal_filters;
111-
goal_filters.add(util_make_unique<internal_goals_filtert>(message_handler));
112-
113-
instrument_cover_goals(
114-
symbol_table, goto_program, criterion, message_handler, goal_filters);
115-
}
116-
117149
bool instrument_cover_goals(
118150
const cmdlinet &cmdline,
119151
const symbol_tablet &symbol_table,
@@ -129,42 +161,27 @@ bool instrument_cover_goals(
129161
goal_filterst goal_filters;
130162
goal_filters.add(util_make_unique<internal_goals_filtert>(message_handler));
131163

164+
cover_instrumenterst instrumenters;
165+
132166
std::list<std::string> criteria_strings=cmdline.get_values("cover");
133-
std::set<coverage_criteriont> criteria;
134167
bool keep_assertions=false;
135168

136169
for(const auto &criterion_string : criteria_strings)
137170
{
138-
coverage_criteriont c;
139-
140-
if(criterion_string=="assertion" || criterion_string=="assertions")
171+
try
141172
{
142-
keep_assertions=true;
143-
c=coverage_criteriont::ASSERTION;
173+
coverage_criteriont c = parse_coverage_criterion(criterion_string);
174+
175+
if(c == coverage_criteriont::ASSERTION)
176+
keep_assertions = true;
177+
178+
instrumenters.add_from_criterion(c, symbol_table, goal_filters);
144179
}
145-
else if(criterion_string=="path" || criterion_string=="paths")
146-
c=coverage_criteriont::PATH;
147-
else if(criterion_string=="branch" || criterion_string=="branches")
148-
c=coverage_criteriont::BRANCH;
149-
else if(criterion_string=="location" || criterion_string=="locations")
150-
c=coverage_criteriont::LOCATION;
151-
else if(criterion_string=="decision" || criterion_string=="decisions")
152-
c=coverage_criteriont::DECISION;
153-
else if(criterion_string=="condition" || criterion_string=="conditions")
154-
c=coverage_criteriont::CONDITION;
155-
else if(criterion_string=="mcdc")
156-
c=coverage_criteriont::MCDC;
157-
else if(criterion_string=="cover")
158-
c=coverage_criteriont::COVER;
159-
else
180+
catch(const std::string &e)
160181
{
161-
msg.error() << "unknown coverage criterion "
162-
<< '\'' << criterion_string << '\''
163-
<< messaget::eom;
182+
msg.error() << e << messaget::eom;
164183
return true;
165184
}
166-
167-
criteria.insert(c);
168185
}
169186

170187
if(keep_assertions && criteria_strings.size()>1)
@@ -203,8 +220,9 @@ bool instrument_cover_goals(
203220
}
204221
if(!cover_include_pattern.empty())
205222
{
206-
function_filters.add(util_make_unique<include_pattern_filtert>(
207-
message_handler, cover_include_pattern));
223+
function_filters.add(
224+
util_make_unique<include_pattern_filtert>(
225+
message_handler, cover_include_pattern));
208226
}
209227

210228
if(cmdline.isset("no-trivial-tests"))
@@ -213,16 +231,8 @@ bool instrument_cover_goals(
213231

214232
msg.status() << "Instrumenting coverage goals" << messaget::eom;
215233

216-
for(const auto &criterion : criteria)
217-
{
218-
instrument_cover_goals(
219-
symbol_table,
220-
goto_functions,
221-
criterion,
222-
message_handler,
223-
function_filters,
224-
goal_filters);
225-
}
234+
instrument_cover_goals(
235+
goto_functions, instrumenters, function_filters, message_handler);
226236

227237
function_filters.report_anomalies();
228238
goal_filters.report_anomalies();

0 commit comments

Comments
 (0)