Skip to content

Make it possible to customise the assertions inserted for coverage instrumentation #5274

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Mar 19, 2020
Merged

Make it possible to customise the assertions inserted for coverage instrumentation #5274

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
36cfa17
Remove `virtual` from `cover_instrumenter_baset::operator()`
thomasspriggs Feb 27, 2020
443e085
Make assertions made by existing instrumenters customisable
thomasspriggs Feb 27, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 12 additions & 5 deletions src/goto-instrument/cover.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,12 +30,17 @@ Date: May 2016
/// \param mode: mode of the function to instrument (for instance ID_C or
/// ID_java)
/// \param message_handler: a message handler
void instrument_cover_goals(
/// \param make_assertion: A function which takes an expression, with a source
/// location and makes an assertion based on that expression. The expression
/// asserted is expected to include the expression passed in, but may include
/// other additional conditions.
static void instrument_cover_goals(
const irep_idt &function_id,
goto_programt &goto_program,
const cover_instrumenterst &instrumenters,
const irep_idt &mode,
message_handlert &message_handler)
message_handlert &message_handler,
const cover_instrumenter_baset::assertion_factoryt &make_assertion)
{
const std::unique_ptr<cover_blocks_baset> basic_blocks =
mode == ID_java ? std::unique_ptr<cover_blocks_baset>(
Expand All @@ -45,7 +50,7 @@ void instrument_cover_goals(

basic_blocks->report_block_anomalies(
function_id, goto_program, message_handler);
instrumenters(function_id, goto_program, *basic_blocks);
instrumenters(function_id, goto_program, *basic_blocks, make_assertion);
}

/// Create and add an instrumenter based on the given criterion
Expand Down Expand Up @@ -309,15 +314,17 @@ static void instrument_cover_goals(
function.body,
cover_config.cover_instrumenters,
function_symbol.mode,
message_handler);
message_handler,
cover_config.make_assertion);
changed = true;
}

if(
cover_config.traces_must_terminate &&
function_symbol.name == goto_functionst::entry_point())
{
cover_instrument_end_of_function(function_symbol.name, function.body);
cover_instrument_end_of_function(
function_symbol.name, function.body, cover_config.make_assertion);
changed = true;
}

Expand Down
2 changes: 2 additions & 0 deletions src/goto-instrument/cover.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,8 @@ struct cover_configt
std::unique_ptr<goal_filterst> goal_filters =
util_make_unique<goal_filterst>();
cover_instrumenterst cover_instrumenters;
cover_instrumenter_baset::assertion_factoryt make_assertion =
goto_programt::make_assertion;
};

void instrument_cover_goals(
Expand Down
56 changes: 41 additions & 15 deletions src/goto-instrument/cover_instrument.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,18 +36,31 @@ class cover_instrumenter_baset
{
}

/// The type of function used to make goto_program assertions.
using assertion_factoryt = std::function<
goto_programt::instructiont(const exprt &, const source_locationt &)>;
static_assert(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice :-)

std::is_same<
assertion_factoryt,
std::function<decltype(goto_programt::make_assertion)>>::value,
"`assertion_factoryt` is expected to have the same type as "
"`goto_programt::make_assertion`.");

/// Instruments a goto program
/// \param function_id: name of \p goto_program
/// \param goto_program: a goto program
/// \param basic_blocks: detected basic blocks
virtual void operator()(
/// \param make_assertion: A function which makes goto program assertions.
/// This parameter may be used to customise the expressions asserted.
void operator()(
const irep_idt &function_id,
goto_programt &goto_program,
const cover_blocks_baset &basic_blocks) const
const cover_blocks_baset &basic_blocks,
const assertion_factoryt &make_assertion) const
{
Forall_goto_program_instructions(i_it, goto_program)
{
instrument(function_id, goto_program, i_it, basic_blocks);
instrument(function_id, goto_program, i_it, basic_blocks, make_assertion);
}
}

Expand All @@ -63,7 +76,8 @@ class cover_instrumenter_baset
const irep_idt &function_id,
goto_programt &,
goto_programt::targett &,
const cover_blocks_baset &) const = 0;
const cover_blocks_baset &,
const assertion_factoryt &) const = 0;

void initialize_source_location(
goto_programt::targett t,
Expand Down Expand Up @@ -96,13 +110,16 @@ class cover_instrumenterst
/// \param function_id: name of \p goto_program
/// \param goto_program: a goto program
/// \param basic_blocks: detected basic blocks of the goto program
/// \param make_assertion: A function which makes goto program assertions.
/// This parameter may be used to customise the expressions asserted.
void operator()(
const irep_idt &function_id,
goto_programt &goto_program,
const cover_blocks_baset &basic_blocks) const
const cover_blocks_baset &basic_blocks,
const cover_instrumenter_baset::assertion_factoryt &make_assertion) const
{
for(const auto &instrumenter : instrumenters)
(*instrumenter)(function_id, goto_program, basic_blocks);
(*instrumenter)(function_id, goto_program, basic_blocks, make_assertion);
}

private:
Expand All @@ -125,7 +142,8 @@ class cover_location_instrumentert : public cover_instrumenter_baset
const irep_idt &function_id,
goto_programt &,
goto_programt::targett &,
const cover_blocks_baset &) const override;
const cover_blocks_baset &,
const assertion_factoryt &) const override;
};

/// Branch coverage instrumenter
Expand All @@ -144,7 +162,8 @@ class cover_branch_instrumentert : public cover_instrumenter_baset
const irep_idt &function_id,
goto_programt &,
goto_programt::targett &,
const cover_blocks_baset &) const override;
const cover_blocks_baset &,
const assertion_factoryt &) const override;
};

/// Condition coverage instrumenter
Expand All @@ -163,7 +182,8 @@ class cover_condition_instrumentert : public cover_instrumenter_baset
const irep_idt &function_id,
goto_programt &,
goto_programt::targett &,
const cover_blocks_baset &) const override;
const cover_blocks_baset &,
const assertion_factoryt &) const override;
};

/// Decision coverage instrumenter
Expand All @@ -182,7 +202,8 @@ class cover_decision_instrumentert : public cover_instrumenter_baset
const irep_idt &function_id,
goto_programt &,
goto_programt::targett &,
const cover_blocks_baset &) const override;
const cover_blocks_baset &,
const assertion_factoryt &) const override;
};

/// MC/DC coverage instrumenter
Expand All @@ -201,7 +222,8 @@ class cover_mcdc_instrumentert : public cover_instrumenter_baset
const irep_idt &function_id,
goto_programt &,
goto_programt::targett &,
const cover_blocks_baset &) const override;
const cover_blocks_baset &,
const assertion_factoryt &) const override;
};

/// Path coverage instrumenter
Expand All @@ -220,7 +242,8 @@ class cover_path_instrumentert : public cover_instrumenter_baset
const irep_idt &function_id,
goto_programt &,
goto_programt::targett &,
const cover_blocks_baset &) const override;
const cover_blocks_baset &,
const assertion_factoryt &) const override;
};

/// Assertion coverage instrumenter
Expand All @@ -239,7 +262,8 @@ class cover_assertion_instrumentert : public cover_instrumenter_baset
const irep_idt &function_id,
goto_programt &,
goto_programt::targett &,
const cover_blocks_baset &) const override;
const cover_blocks_baset &,
const assertion_factoryt &) const override;
};

/// __CPROVER_cover coverage instrumenter
Expand All @@ -258,11 +282,13 @@ class cover_cover_instrumentert : public cover_instrumenter_baset
const irep_idt &function_id,
goto_programt &,
goto_programt::targett &,
const cover_blocks_baset &) const override;
const cover_blocks_baset &,
const assertion_factoryt &) const override;
};

void cover_instrument_end_of_function(
const irep_idt &function_id,
goto_programt &goto_program);
goto_programt &goto_program,
const cover_instrumenter_baset::assertion_factoryt &);

#endif // CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H
9 changes: 5 additions & 4 deletions src/goto-instrument/cover_instrument_branch.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,8 @@ void cover_branch_instrumentert::instrument(
const irep_idt &function_id,
goto_programt &goto_program,
goto_programt::targett &i_it,
const cover_blocks_baset &basic_blocks) const
const cover_blocks_baset &basic_blocks,
const assertion_factoryt &make_assertion) const
{
if(is_non_cover_assertion(i_it))
i_it->turn_into_skip();
Expand All @@ -40,7 +41,7 @@ void cover_branch_instrumentert::instrument(
source_locationt source_location = i_it->source_location;

goto_programt::targett t = goto_program.insert_before(
i_it, goto_programt::make_assertion(false_exprt(), source_location));
i_it, make_assertion(false_exprt(), source_location));
initialize_source_location(t, comment, function_id);
}

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

goto_program.insert_before_swap(i_it);
*i_it = goto_programt::make_assertion(not_exprt(guard), source_location);
*i_it = make_assertion(not_exprt(guard), source_location);
initialize_source_location(i_it, true_comment, function_id);

goto_program.insert_before_swap(i_it);
*i_it = goto_programt::make_assertion(guard, source_location);
*i_it = make_assertion(guard, source_location);
initialize_source_location(i_it, false_comment, function_id);

std::advance(i_it, 2);
Expand Down
7 changes: 4 additions & 3 deletions src/goto-instrument/cover_instrument_condition.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,8 @@ void cover_condition_instrumentert::instrument(
const irep_idt &function_id,
goto_programt &goto_program,
goto_programt::targett &i_it,
const cover_blocks_baset &) const
const cover_blocks_baset &,
const assertion_factoryt &make_assertion) const
{
if(is_non_cover_assertion(i_it))
i_it->turn_into_skip();
Expand All @@ -38,12 +39,12 @@ void cover_condition_instrumentert::instrument(

const std::string comment_t = "condition '" + c_string + "' true";
goto_program.insert_before_swap(i_it);
*i_it = goto_programt::make_assertion(c, source_location);
*i_it = make_assertion(c, source_location);
initialize_source_location(i_it, comment_t, function_id);

const std::string comment_f = "condition '" + c_string + "' false";
goto_program.insert_before_swap(i_it);
*i_it = goto_programt::make_assertion(not_exprt(c), source_location);
*i_it = make_assertion(not_exprt(c), source_location);
initialize_source_location(i_it, comment_f, function_id);
}

Expand Down
7 changes: 4 additions & 3 deletions src/goto-instrument/cover_instrument_decision.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,8 @@ void cover_decision_instrumentert::instrument(
const irep_idt &function_id,
goto_programt &goto_program,
goto_programt::targett &i_it,
const cover_blocks_baset &) const
const cover_blocks_baset &,
const assertion_factoryt &make_assertion) const
{
if(is_non_cover_assertion(i_it))
i_it->turn_into_skip();
Expand All @@ -37,12 +38,12 @@ void cover_decision_instrumentert::instrument(

const std::string comment_t = "decision '" + d_string + "' true";
goto_program.insert_before_swap(i_it);
*i_it = goto_programt::make_assertion(d, source_location);
*i_it = make_assertion(d, source_location);
initialize_source_location(i_it, comment_t, function_id);

const std::string comment_f = "decision '" + d_string + "' false";
goto_program.insert_before_swap(i_it);
*i_it = goto_programt::make_assertion(not_exprt(d), source_location);
*i_it = make_assertion(not_exprt(d), source_location);
initialize_source_location(i_it, comment_f, function_id);
}

Expand Down
5 changes: 3 additions & 2 deletions src/goto-instrument/cover_instrument_location.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,8 @@ void cover_location_instrumentert::instrument(
const irep_idt &function_id,
goto_programt &goto_program,
goto_programt::targett &i_it,
const cover_blocks_baset &basic_blocks) const
const cover_blocks_baset &basic_blocks,
const assertion_factoryt &make_assertion) const
{
if(is_non_cover_assertion(i_it))
i_it->turn_into_skip();
Expand All @@ -40,7 +41,7 @@ void cover_location_instrumentert::instrument(
const std::string comment =
"block " + b + " (lines " + source_lines + ")";
goto_program.insert_before_swap(i_it);
*i_it = goto_programt::make_assertion(false_exprt(), source_location);
*i_it = make_assertion(false_exprt(), source_location);
initialize_source_location(i_it, comment, function_id);
i_it++;
}
Expand Down
9 changes: 5 additions & 4 deletions src/goto-instrument/cover_instrument_mcdc.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -623,7 +623,8 @@ void cover_mcdc_instrumentert::instrument(
const irep_idt &function_id,
goto_programt &goto_program,
goto_programt::targett &i_it,
const cover_blocks_baset &) const
const cover_blocks_baset &,
const assertion_factoryt &make_assertion) const
{
if(is_non_cover_assertion(i_it))
i_it->turn_into_skip();
Expand Down Expand Up @@ -661,15 +662,15 @@ void cover_mcdc_instrumentert::instrument(

std::string comment_t = description + " '" + p_string + "' true";
goto_program.insert_before_swap(i_it);
*i_it = goto_programt::make_assertion(not_exprt(p), source_location);
*i_it = make_assertion(not_exprt(p), source_location);
i_it->source_location.set_comment(comment_t);
i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
i_it->source_location.set_property_class(property_class);
i_it->source_location.set_function(function_id);

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

goto_program.insert_before_swap(i_it);
*i_it = goto_programt::make_assertion(not_exprt(p), source_location);
*i_it = make_assertion(not_exprt(p), source_location);
i_it->source_location.set_comment(description);
i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
i_it->source_location.set_property_class(property_class);
Expand Down
Loading