Skip to content
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

Coverage: support instrumenting one function at a time #1744

Merged
merged 2 commits into from
Jan 30, 2018
Merged

Coverage: support instrumenting one function at a time #1744

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
3440018
Provide function name in goto_model_functiont
smowton Jan 16, 2018
311af6d
Coverage: fully support instrumenting one function at a time
smowton Jan 16, 2018
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
182 changes: 109 additions & 73 deletions src/goto-instrument/cover.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,6 @@ Date: May 2016
#include <util/options.h>

#include "cover_basic_blocks.h"
#include "cover_filter.h"
#include "cover_instrument.h"

/// Applies instrumenters to given goto program
/// \param goto_program: the goto program
Expand Down Expand Up @@ -165,91 +163,53 @@ void parse_cover_options(const cmdlinet &cmdline, optionst &options)
cmdline.isset("cover-traces-must-terminate"));
}

/// Applies instrumenters to given goto functions
/// \param goto_functions: the goto functions
/// \param instrumenters: the instrumenters
/// \param function_filters: function filters to discard certain functions
/// \param message_handler: a message handler
void instrument_cover_goals(
goto_functionst &goto_functions,
const cover_instrumenterst &instrumenters,
const function_filterst &function_filters,
message_handlert &message_handler)
{
Forall_goto_functions(f_it, goto_functions)
{
if(!function_filters(f_it->first, f_it->second))
continue;

instrument_cover_goals(f_it->second.body, instrumenters, message_handler);
}
}

/// Instruments goto functions based on given command line options
/// \param options: the options
/// \param symbol_table: the symbol table
/// \param goto_functions: the goto functions
/// \param message_handler: a message handler
bool instrument_cover_goals(
/// Build data structures controlling coverage from command-line options.
/// \param options: command-line options
/// \param symbol_table: global symbol table
/// \param message_handler: used to log incorrect option specifications
/// \return a cover_configt on success, or null otherwise.
std::unique_ptr<cover_configt> get_cover_config(
const optionst &options,
const symbol_tablet &symbol_table,
goto_functionst &goto_functions,
message_handlert &message_handler)
{
messaget msg(message_handler);
std::unique_ptr<cover_configt> config = util_make_unique<cover_configt>();
Copy link
Collaborator

Choose a reason for hiding this comment

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

Why does this need to be a pointer?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I'd rather not implement move constructors for all the filter kinds -- simpler to let them not support copy/move and pass a handle to the config object instead. Unique-ptr really takes the pain out of managing its lifespan in any case.

Copy link
Collaborator

Choose a reason for hiding this comment

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

It just seems a lot of machinery for a very simple problem where performance doesn't matter either. Why not just return cover_configt by value?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Same thing -- needing copyable and movable everything in the config object. So much simpler to just allocate one and pass it around.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Ok. So while I would have done it differently, you actually did it, so you win :-)

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Are you happy to approve in that case? This is still blocked on code-owner approval

function_filterst &function_filters = config->function_filters;
goal_filterst &goal_filters = config->goal_filters;
cover_instrumenterst &instrumenters = config->cover_instrumenters;

function_filterst function_filters;
function_filters.add(
util_make_unique<internal_functions_filtert>(message_handler));

goal_filterst goal_filters;
goal_filters.add(util_make_unique<internal_goals_filtert>(message_handler));

cover_instrumenterst instrumenters;

optionst::value_listt criteria_strings = options.get_list_option("cover");
bool keep_assertions=false;

config->keep_assertions = false;
for(const auto &criterion_string : criteria_strings)
{
try
{
coverage_criteriont c = parse_coverage_criterion(criterion_string);

if(c == coverage_criteriont::ASSERTION)
keep_assertions = true;
config->keep_assertions = true;

instrumenters.add_from_criterion(c, symbol_table, goal_filters);
}
catch(const std::string &e)
{
msg.error() << e << messaget::eom;
return true;
return {};
}
}

if(keep_assertions && criteria_strings.size()>1)
if(config->keep_assertions && criteria_strings.size()>1)
{
msg.error() << "assertion coverage cannot currently be used together with "
<< "other coverage criteria" << messaget::eom;
return true;
}

msg.status() << "Rewriting existing assertions as assumptions"
<< messaget::eom;

if(!keep_assertions)
{
// turn assertions (from generic checks) into assumptions
Forall_goto_functions(f_it, goto_functions)
{
goto_programt &body=f_it->second.body;
Forall_goto_program_instructions(i_it, body)
{
if(i_it->is_assert())
i_it->type=goto_program_instruction_typet::ASSUME;
}
}
return {};
}

// cover entry point function only
Expand All @@ -266,32 +226,108 @@ bool instrument_cover_goals(
function_filters.add(
util_make_unique<trivial_functions_filtert>(message_handler));

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

instrument_cover_goals(
goto_functions, instrumenters, function_filters, message_handler);
config->traces_must_terminate =
options.get_bool_option("cover-traces-must-terminate");

function_filters.report_anomalies();
goal_filters.report_anomalies();
return config;
}

if(options.get_bool_option("cover-traces-must-terminate"))
/// Instruments a single goto program based on the given configuration
/// \param config: configuration, produced using get_cover_config
/// \param function_id: function name
/// \param function: function function to instrument
/// \param message_handler: log output
static void instrument_cover_goals(
const cover_configt &config,
const irep_idt &function_id,
goto_functionst::goto_functiont &function,
message_handlert &message_handler)
{
if(!config.keep_assertions)
{
// instrument an additional goal in CPROVER_START. This will rephrase
// the reachability problem by asking BMC to provide a solution that
// satisfies a goal while getting to the end of the program-under-test.
const auto sf_it=
goto_functions.function_map.find(goto_functions.entry_point());
if(sf_it==goto_functions.function_map.end())
Forall_goto_program_instructions(i_it, function.body)
Copy link
Contributor

Choose a reason for hiding this comment

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

Can we here swap to using range based for loop? Or perhaps even a std::foreach since the body is so simple

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I'm going to plead "moved code" plus slim benefit and leave this alone :)

{
msg.error() << "cover-traces-must-terminate: invalid entry point ["
<< goto_functions.entry_point() << "]" << messaget::eom;
return true;
if(i_it->is_assert())
i_it->type=goto_program_instruction_typet::ASSUME;
}
}

bool changed = false;

cover_instrument_end_of_function(sf_it->first, sf_it->second.body);
if(config.function_filters(function_id, function))
{
instrument_cover_goals(
function.body, config.cover_instrumenters, message_handler);
changed = true;
}

if(config.traces_must_terminate &&
function_id == goto_functionst::entry_point())
{
cover_instrument_end_of_function(function_id, function.body);
changed = true;
}

if(changed)
function.body.update();
}

/// Instruments a single goto program based on the given configuration
/// \param config: configuration, produced using get_cover_config
/// \param function: goto program to instrument
/// \param message_handler: log output
void instrument_cover_goals(
const cover_configt &config,
goto_model_functiont &function,
message_handlert &message_handler)
{
instrument_cover_goals(
config,
function.get_function_id(),
function.get_goto_function(),
message_handler);

function.compute_location_numbers();
}

/// Instruments goto functions based on given command line options
/// \param options: the options
/// \param symbol_table: the symbol table
/// \param goto_functions: the goto functions
/// \param message_handler: a message handler
bool instrument_cover_goals(
const optionst &options,
const symbol_tablet &symbol_table,
goto_functionst &goto_functions,
message_handlert &message_handler)
{
messaget msg(message_handler);
msg.status() << "Rewriting existing assertions as assumptions"
<< messaget::eom;

std::unique_ptr<cover_configt> config =
get_cover_config(options, symbol_table, message_handler);
if(!config)
return true;

if(config->traces_must_terminate &&
!goto_functions.function_map.count(goto_functions.entry_point()))
{
msg.error() << "cover-traces-must-terminate: invalid entry point ["
<< goto_functions.entry_point() << "]" << messaget::eom;
return true;
}

goto_functions.update();
Forall_goto_functions(f_it, goto_functions)
{
instrument_cover_goals(
*config, f_it->first, f_it->second, message_handler);
}
goto_functions.compute_location_numbers();

config->function_filters.report_anomalies();
config->goal_filters.report_anomalies();

return false;
}

Expand Down
19 changes: 19 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 @@ -15,6 +15,8 @@ Date: May 2016
#define CPROVER_GOTO_INSTRUMENT_COVER_H

#include <goto-programs/goto_model.h>
#include "cover_filter.h"
#include "cover_instrument.h"

class message_handlert;
class cmdlinet;
Expand All @@ -32,6 +34,15 @@ enum class coverage_criteriont
COVER // __CPROVER_cover(x) annotations
};

struct cover_configt
{
bool keep_assertions;
bool traces_must_terminate;
function_filterst function_filters;
goal_filterst goal_filters;
cover_instrumenterst cover_instrumenters;
};

void instrument_cover_goals(
const symbol_tablet &,
goto_functionst &,
Expand All @@ -44,6 +55,14 @@ void instrument_cover_goals(
coverage_criteriont,
message_handlert &message_handler);

std::unique_ptr<cover_configt> get_cover_config(
Copy link
Member

Choose a reason for hiding this comment

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

What about wrapping everything into a covert class to keep the configuration as state? This would avoid exposing the implementation details to the user of the interface.

const optionst &, const symbol_tablet &, message_handlert &);

void instrument_cover_goals(
const cover_configt &,
goto_model_functiont &,
message_handlert &);

void parse_cover_options(const cmdlinet &, optionst &);

bool instrument_cover_goals(
Expand Down
10 changes: 10 additions & 0 deletions src/goto-programs/goto_model.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,9 +86,11 @@ class goto_model_functiont
goto_model_functiont(
journalling_symbol_tablet &symbol_table,
goto_functionst &goto_functions,
const irep_idt &function_id,
goto_functionst::goto_functiont &goto_function):
symbol_table(symbol_table),
goto_functions(goto_functions),
function_id(function_id),
goto_function(goto_function)
{
}
Expand Down Expand Up @@ -117,9 +119,17 @@ class goto_model_functiont
return goto_function;
}

/// Get function id
/// \return `goto_function`'s name (its key in `goto_functions`)
const irep_idt &get_function_id()
{
return function_id;
}

private:
journalling_symbol_tablet &symbol_table;
goto_functionst &goto_functions;
irep_idt function_id;
goto_functionst::goto_functiont &goto_function;
};

Expand Down
3 changes: 2 additions & 1 deletion src/goto-programs/lazy_goto_functions_map.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@ class lazy_goto_functions_mapt final

typedef
std::function<void(
const irep_idt &name,
goto_functionst::goto_functiont &function,
journalling_symbol_tablet &function_symbols)>
post_process_functiont;
Expand Down Expand Up @@ -128,7 +129,7 @@ class lazy_goto_functions_mapt final
if(processed_functions.count(name)==0)
{
// Run function-pass conversions
post_process_function(function, journalling_table);
post_process_function(name, function, journalling_table);
// Assign procedure-local location numbers for now
function.body.compute_location_numbers();
processed_functions.insert(name);
Expand Down
4 changes: 4 additions & 0 deletions src/goto-programs/lazy_goto_model.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,12 +29,14 @@ lazy_goto_modelt::lazy_goto_modelt(
language_files,
symbol_table,
[this] (
const irep_idt &function_name,
goto_functionst::goto_functiont &function,
journalling_symbol_tablet &journalling_symbol_table) -> void
{
goto_model_functiont model_function(
journalling_symbol_table,
goto_model->goto_functions,
function_name,
function);
this->post_process_function(model_function, *this);
},
Expand All @@ -54,12 +56,14 @@ lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other)
language_files,
symbol_table,
[this] (
const irep_idt &function_name,
goto_functionst::goto_functiont &function,
journalling_symbol_tablet &journalling_symbol_table) -> void
{
goto_model_functiont model_function(
journalling_symbol_table,
goto_model->goto_functions,
function_name,
function);
this->post_process_function(model_function, *this);
},
Expand Down