Skip to content

Commit 094fc97

Browse files
thomasspriggsthomasspriggs
authored
Merge pull request #5274 from thomasspriggs/tas/flag_goals
Make it possible to customise the assertions inserted for coverage instrumentation
2 parents 1002ac5 + 443e085 commit 094fc97

10 files changed

+113
-45
lines changed

‎src/goto-instrument/cover.cpp

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -30,12 +30,17 @@ Date: May 2016
3030
/// \param mode: mode of the function to instrument (for instance ID_C or
3131
/// ID_java)
3232
/// \param message_handler: a message handler
33-
void instrument_cover_goals(
33+
/// \param make_assertion: A function which takes an expression, with a source
34+
/// location and makes an assertion based on that expression. The expression
35+
/// asserted is expected to include the expression passed in, but may include
36+
/// other additional conditions.
37+
static void instrument_cover_goals(
3438
const irep_idt &function_id,
3539
goto_programt &goto_program,
3640
const cover_instrumenterst &instrumenters,
3741
const irep_idt &mode,
38-
message_handlert &message_handler)
42+
message_handlert &message_handler,
43+
const cover_instrumenter_baset::assertion_factoryt &make_assertion)
3944
{
4045
const std::unique_ptr<cover_blocks_baset> basic_blocks =
4146
mode == ID_java ? std::unique_ptr<cover_blocks_baset>(
@@ -45,7 +50,7 @@ void instrument_cover_goals(
4550

4651
basic_blocks->report_block_anomalies(
4752
function_id, goto_program, message_handler);
48-
instrumenters(function_id, goto_program, *basic_blocks);
53+
instrumenters(function_id, goto_program, *basic_blocks, make_assertion);
4954
}
5055

5156
/// Create and add an instrumenter based on the given criterion
@@ -309,15 +314,17 @@ static void instrument_cover_goals(
309314
function.body,
310315
cover_config.cover_instrumenters,
311316
function_symbol.mode,
312-
message_handler);
317+
message_handler,
318+
cover_config.make_assertion);
313319
changed = true;
314320
}
315321

316322
if(
317323
cover_config.traces_must_terminate &&
318324
function_symbol.name == goto_functionst::entry_point())
319325
{
320-
cover_instrument_end_of_function(function_symbol.name, function.body);
326+
cover_instrument_end_of_function(
327+
function_symbol.name, function.body, cover_config.make_assertion);
321328
changed = true;
322329
}
323330

‎src/goto-instrument/cover.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,8 @@ struct cover_configt
4444
std::unique_ptr<goal_filterst> goal_filters =
4545
util_make_unique<goal_filterst>();
4646
cover_instrumenterst cover_instrumenters;
47+
cover_instrumenter_baset::assertion_factoryt make_assertion =
48+
goto_programt::make_assertion;
4749
};
4850

4951
void instrument_cover_goals(

‎src/goto-instrument/cover_instrument.h

Lines changed: 41 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -36,18 +36,31 @@ class cover_instrumenter_baset
3636
{
3737
}
3838

39+
/// The type of function used to make goto_program assertions.
40+
using assertion_factoryt = std::function<
41+
goto_programt::instructiont(const exprt &, const source_locationt &)>;
42+
static_assert(
43+
std::is_same<
44+
assertion_factoryt,
45+
std::function<decltype(goto_programt::make_assertion)>>::value,
46+
"`assertion_factoryt` is expected to have the same type as "
47+
"`goto_programt::make_assertion`.");
48+
3949
/// Instruments a goto program
4050
/// \param function_id: name of \p goto_program
4151
/// \param goto_program: a goto program
4252
/// \param basic_blocks: detected basic blocks
43-
virtual void operator()(
53+
/// \param make_assertion: A function which makes goto program assertions.
54+
/// This parameter may be used to customise the expressions asserted.
55+
void operator()(
4456
const irep_idt &function_id,
4557
goto_programt &goto_program,
46-
const cover_blocks_baset &basic_blocks) const
58+
const cover_blocks_baset &basic_blocks,
59+
const assertion_factoryt &make_assertion) const
4760
{
4861
Forall_goto_program_instructions(i_it, goto_program)
4962
{
50-
instrument(function_id, goto_program, i_it, basic_blocks);
63+
instrument(function_id, goto_program, i_it, basic_blocks, make_assertion);
5164
}
5265
}
5366

@@ -63,7 +76,8 @@ class cover_instrumenter_baset
6376
const irep_idt &function_id,
6477
goto_programt &,
6578
goto_programt::targett &,
66-
const cover_blocks_baset &) const = 0;
79+
const cover_blocks_baset &,
80+
const assertion_factoryt &) const = 0;
6781

6882
void initialize_source_location(
6983
goto_programt::targett t,
@@ -96,13 +110,16 @@ class cover_instrumenterst
96110
/// \param function_id: name of \p goto_program
97111
/// \param goto_program: a goto program
98112
/// \param basic_blocks: detected basic blocks of the goto program
113+
/// \param make_assertion: A function which makes goto program assertions.
114+
/// This parameter may be used to customise the expressions asserted.
99115
void operator()(
100116
const irep_idt &function_id,
101117
goto_programt &goto_program,
102-
const cover_blocks_baset &basic_blocks) const
118+
const cover_blocks_baset &basic_blocks,
119+
const cover_instrumenter_baset::assertion_factoryt &make_assertion) const
103120
{
104121
for(const auto &instrumenter : instrumenters)
105-
(*instrumenter)(function_id, goto_program, basic_blocks);
122+
(*instrumenter)(function_id, goto_program, basic_blocks, make_assertion);
106123
}
107124

108125
private:
@@ -125,7 +142,8 @@ class cover_location_instrumentert : public cover_instrumenter_baset
125142
const irep_idt &function_id,
126143
goto_programt &,
127144
goto_programt::targett &,
128-
const cover_blocks_baset &) const override;
145+
const cover_blocks_baset &,
146+
const assertion_factoryt &) const override;
129147
};
130148

131149
/// Branch coverage instrumenter
@@ -144,7 +162,8 @@ class cover_branch_instrumentert : public cover_instrumenter_baset
144162
const irep_idt &function_id,
145163
goto_programt &,
146164
goto_programt::targett &,
147-
const cover_blocks_baset &) const override;
165+
const cover_blocks_baset &,
166+
const assertion_factoryt &) const override;
148167
};
149168

150169
/// Condition coverage instrumenter
@@ -163,7 +182,8 @@ class cover_condition_instrumentert : public cover_instrumenter_baset
163182
const irep_idt &function_id,
164183
goto_programt &,
165184
goto_programt::targett &,
166-
const cover_blocks_baset &) const override;
185+
const cover_blocks_baset &,
186+
const assertion_factoryt &) const override;
167187
};
168188

169189
/// Decision coverage instrumenter
@@ -182,7 +202,8 @@ class cover_decision_instrumentert : public cover_instrumenter_baset
182202
const irep_idt &function_id,
183203
goto_programt &,
184204
goto_programt::targett &,
185-
const cover_blocks_baset &) const override;
205+
const cover_blocks_baset &,
206+
const assertion_factoryt &) const override;
186207
};
187208

188209
/// MC/DC coverage instrumenter
@@ -201,7 +222,8 @@ class cover_mcdc_instrumentert : public cover_instrumenter_baset
201222
const irep_idt &function_id,
202223
goto_programt &,
203224
goto_programt::targett &,
204-
const cover_blocks_baset &) const override;
225+
const cover_blocks_baset &,
226+
const assertion_factoryt &) const override;
205227
};
206228

207229
/// Path coverage instrumenter
@@ -220,7 +242,8 @@ class cover_path_instrumentert : public cover_instrumenter_baset
220242
const irep_idt &function_id,
221243
goto_programt &,
222244
goto_programt::targett &,
223-
const cover_blocks_baset &) const override;
245+
const cover_blocks_baset &,
246+
const assertion_factoryt &) const override;
224247
};
225248

226249
/// Assertion coverage instrumenter
@@ -239,7 +262,8 @@ class cover_assertion_instrumentert : public cover_instrumenter_baset
239262
const irep_idt &function_id,
240263
goto_programt &,
241264
goto_programt::targett &,
242-
const cover_blocks_baset &) const override;
265+
const cover_blocks_baset &,
266+
const assertion_factoryt &) const override;
243267
};
244268

245269
/// __CPROVER_cover coverage instrumenter
@@ -258,11 +282,13 @@ class cover_cover_instrumentert : public cover_instrumenter_baset
258282
const irep_idt &function_id,
259283
goto_programt &,
260284
goto_programt::targett &,
261-
const cover_blocks_baset &) const override;
285+
const cover_blocks_baset &,
286+
const assertion_factoryt &) const override;
262287
};
263288

264289
void cover_instrument_end_of_function(
265290
const irep_idt &function_id,
266-
goto_programt &goto_program);
291+
goto_programt &goto_program,
292+
const cover_instrumenter_baset::assertion_factoryt &);
267293

268294
#endif // CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H

‎src/goto-instrument/cover_instrument_branch.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,8 @@ void cover_branch_instrumentert::instrument(
1717
const irep_idt &function_id,
1818
goto_programt &goto_program,
1919
goto_programt::targett &i_it,
20-
const cover_blocks_baset &basic_blocks) const
20+
const cover_blocks_baset &basic_blocks,
21+
const assertion_factoryt &make_assertion) const
2122
{
2223
if(is_non_cover_assertion(i_it))
2324
i_it->turn_into_skip();
@@ -40,7 +41,7 @@ void cover_branch_instrumentert::instrument(
4041
source_locationt source_location = i_it->source_location;
4142

4243
goto_programt::targett t = goto_program.insert_before(
43-
i_it, goto_programt::make_assertion(false_exprt(), source_location));
44+
i_it, make_assertion(false_exprt(), source_location));
4445
initialize_source_location(t, comment, function_id);
4546
}
4647

@@ -55,11 +56,11 @@ void cover_branch_instrumentert::instrument(
5556
source_locationt source_location = i_it->source_location;
5657

5758
goto_program.insert_before_swap(i_it);
58-
*i_it = goto_programt::make_assertion(not_exprt(guard), source_location);
59+
*i_it = make_assertion(not_exprt(guard), source_location);
5960
initialize_source_location(i_it, true_comment, function_id);
6061

6162
goto_program.insert_before_swap(i_it);
62-
*i_it = goto_programt::make_assertion(guard, source_location);
63+
*i_it = make_assertion(guard, source_location);
6364
initialize_source_location(i_it, false_comment, function_id);
6465

6566
std::advance(i_it, 2);

‎src/goto-instrument/cover_instrument_condition.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,8 @@ void cover_condition_instrumentert::instrument(
2020
const irep_idt &function_id,
2121
goto_programt &goto_program,
2222
goto_programt::targett &i_it,
23-
const cover_blocks_baset &) const
23+
const cover_blocks_baset &,
24+
const assertion_factoryt &make_assertion) const
2425
{
2526
if(is_non_cover_assertion(i_it))
2627
i_it->turn_into_skip();
@@ -38,12 +39,12 @@ void cover_condition_instrumentert::instrument(
3839

3940
const std::string comment_t = "condition '" + c_string + "' true";
4041
goto_program.insert_before_swap(i_it);
41-
*i_it = goto_programt::make_assertion(c, source_location);
42+
*i_it = make_assertion(c, source_location);
4243
initialize_source_location(i_it, comment_t, function_id);
4344

4445
const std::string comment_f = "condition '" + c_string + "' false";
4546
goto_program.insert_before_swap(i_it);
46-
*i_it = goto_programt::make_assertion(not_exprt(c), source_location);
47+
*i_it = make_assertion(not_exprt(c), source_location);
4748
initialize_source_location(i_it, comment_f, function_id);
4849
}
4950

‎src/goto-instrument/cover_instrument_decision.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,8 @@ void cover_decision_instrumentert::instrument(
1919
const irep_idt &function_id,
2020
goto_programt &goto_program,
2121
goto_programt::targett &i_it,
22-
const cover_blocks_baset &) const
22+
const cover_blocks_baset &,
23+
const assertion_factoryt &make_assertion) const
2324
{
2425
if(is_non_cover_assertion(i_it))
2526
i_it->turn_into_skip();
@@ -37,12 +38,12 @@ void cover_decision_instrumentert::instrument(
3738

3839
const std::string comment_t = "decision '" + d_string + "' true";
3940
goto_program.insert_before_swap(i_it);
40-
*i_it = goto_programt::make_assertion(d, source_location);
41+
*i_it = make_assertion(d, source_location);
4142
initialize_source_location(i_it, comment_t, function_id);
4243

4344
const std::string comment_f = "decision '" + d_string + "' false";
4445
goto_program.insert_before_swap(i_it);
45-
*i_it = goto_programt::make_assertion(not_exprt(d), source_location);
46+
*i_it = make_assertion(not_exprt(d), source_location);
4647
initialize_source_location(i_it, comment_f, function_id);
4748
}
4849

‎src/goto-instrument/cover_instrument_location.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,8 @@ void cover_location_instrumentert::instrument(
1818
const irep_idt &function_id,
1919
goto_programt &goto_program,
2020
goto_programt::targett &i_it,
21-
const cover_blocks_baset &basic_blocks) const
21+
const cover_blocks_baset &basic_blocks,
22+
const assertion_factoryt &make_assertion) const
2223
{
2324
if(is_non_cover_assertion(i_it))
2425
i_it->turn_into_skip();
@@ -40,7 +41,7 @@ void cover_location_instrumentert::instrument(
4041
const std::string comment =
4142
"block " + b + " (lines " + source_lines + ")";
4243
goto_program.insert_before_swap(i_it);
43-
*i_it = goto_programt::make_assertion(false_exprt(), source_location);
44+
*i_it = make_assertion(false_exprt(), source_location);
4445
initialize_source_location(i_it, comment, function_id);
4546
i_it++;
4647
}

‎src/goto-instrument/cover_instrument_mcdc.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -623,7 +623,8 @@ void cover_mcdc_instrumentert::instrument(
623623
const irep_idt &function_id,
624624
goto_programt &goto_program,
625625
goto_programt::targett &i_it,
626-
const cover_blocks_baset &) const
626+
const cover_blocks_baset &,
627+
const assertion_factoryt &make_assertion) const
627628
{
628629
if(is_non_cover_assertion(i_it))
629630
i_it->turn_into_skip();
@@ -661,15 +662,15 @@ void cover_mcdc_instrumentert::instrument(
661662

662663
std::string comment_t = description + " '" + p_string + "' true";
663664
goto_program.insert_before_swap(i_it);
664-
*i_it = goto_programt::make_assertion(not_exprt(p), source_location);
665+
*i_it = make_assertion(not_exprt(p), source_location);
665666
i_it->source_location.set_comment(comment_t);
666667
i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
667668
i_it->source_location.set_property_class(property_class);
668669
i_it->source_location.set_function(function_id);
669670

670671
std::string comment_f = description + " '" + p_string + "' false";
671672
goto_program.insert_before_swap(i_it);
672-
*i_it = goto_programt::make_assertion(p, source_location);
673+
*i_it = make_assertion(p, source_location);
673674
i_it->source_location.set_comment(comment_f);
674675
i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
675676
i_it->source_location.set_property_class(property_class);
@@ -694,7 +695,7 @@ void cover_mcdc_instrumentert::instrument(
694695
"MC/DC independence condition '" + p_string + "'";
695696

696697
goto_program.insert_before_swap(i_it);
697-
*i_it = goto_programt::make_assertion(not_exprt(p), source_location);
698+
*i_it = make_assertion(not_exprt(p), source_location);
698699
i_it->source_location.set_comment(description);
699700
i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
700701
i_it->source_location.set_property_class(property_class);

0 commit comments

Comments
 (0)