diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index bb32c61ccd8..750cdd5e010 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -20,8 +20,6 @@ Date: May 2016 #include #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 @@ -165,51 +163,30 @@ 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 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 config = util_make_unique(); + 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(message_handler)); - goal_filterst goal_filters; goal_filters.add(util_make_unique(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 @@ -217,39 +194,22 @@ bool instrument_cover_goals( 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 @@ -266,32 +226,108 @@ bool instrument_cover_goals( function_filters.add( util_make_unique(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) { - 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 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; } diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index d8dd994e700..75352ac9039 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -15,6 +15,8 @@ Date: May 2016 #define CPROVER_GOTO_INSTRUMENT_COVER_H #include +#include "cover_filter.h" +#include "cover_instrument.h" class message_handlert; class cmdlinet; @@ -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 &, @@ -44,6 +55,14 @@ void instrument_cover_goals( coverage_criteriont, message_handlert &message_handler); +std::unique_ptr get_cover_config( + 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( diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index a04d7aa5bc8..04236c201c9 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -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) { } @@ -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; }; diff --git a/src/goto-programs/lazy_goto_functions_map.h b/src/goto-programs/lazy_goto_functions_map.h index 2ee31010f75..c52243e0580 100644 --- a/src/goto-programs/lazy_goto_functions_map.h +++ b/src/goto-programs/lazy_goto_functions_map.h @@ -49,6 +49,7 @@ class lazy_goto_functions_mapt final typedef std::function post_process_functiont; @@ -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); diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp index a2f86cef74d..cde0250f12e 100644 --- a/src/goto-programs/lazy_goto_model.cpp +++ b/src/goto-programs/lazy_goto_model.cpp @@ -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); }, @@ -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); },