From 8e7f129c641e942da63008195663ebd453da23eb Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 14 Feb 2018 07:03:56 +0000 Subject: [PATCH 1/8] Correct types from unsigned to std::size_t The block numbers in cover_basic_blockst are obtained from `block_info.size() - 1`, they should have type std::size_t rather than unsigned. Also mark const a couple of arguments that are constant. --- src/goto-instrument/cover_basic_blocks.cpp | 18 +++++++++--------- src/goto-instrument/cover_basic_blocks.h | 12 ++++++------ 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp index 9288281d4f7..bffdabbe230 100644 --- a/src/goto-instrument/cover_basic_blocks.cpp +++ b/src/goto-instrument/cover_basic_blocks.cpp @@ -15,7 +15,7 @@ Author: Peter Schrammel #include #include -optionalt cover_basic_blockst::continuation_of_block( +optionalt cover_basic_blockst::continuation_of_block( const goto_programt::const_targett &instruction, cover_basic_blockst::block_mapt &block_map) { @@ -32,7 +32,7 @@ optionalt cover_basic_blockst::continuation_of_block( cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program) { bool next_is_target = true; - unsigned current_block = 0; + std::size_t current_block = 0; forall_goto_program_instructions(it, _goto_program) { @@ -87,7 +87,7 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program) update_covered_lines(block_info); } -unsigned cover_basic_blockst::block_of(goto_programt::const_targett t) const +std::size_t cover_basic_blockst::block_of(goto_programt::const_targett t) const { const auto it = block_map.find(t); INVARIANT(it != block_map.end(), "instruction must be part of a block"); @@ -95,14 +95,14 @@ unsigned cover_basic_blockst::block_of(goto_programt::const_targett t) const } optionalt -cover_basic_blockst::instruction_of(unsigned block_nr) const +cover_basic_blockst::instruction_of(const std::size_t block_nr) const { INVARIANT(block_nr < block_infos.size(), "block number out of range"); return block_infos.at(block_nr).representative_inst; } const source_locationt & -cover_basic_blockst::source_location_of(unsigned block_nr) const +cover_basic_blockst::source_location_of(const std::size_t block_nr) const { INVARIANT(block_nr < block_infos.size(), "block number out of range"); return block_infos.at(block_nr).source_location; @@ -113,12 +113,12 @@ void cover_basic_blockst::select_unique_java_bytecode_indices( message_handlert &message_handler) { messaget msg(message_handler); - std::set blocks_seen; + std::set blocks_seen; std::set bytecode_indices_seen; forall_goto_program_instructions(it, goto_program) { - const unsigned block_nr = block_of(it); + const std::size_t block_nr = block_of(it); if(blocks_seen.find(block_nr) != blocks_seen.end()) continue; @@ -181,10 +181,10 @@ void cover_basic_blockst::report_block_anomalies( message_handlert &message_handler) { messaget msg(message_handler); - std::set blocks_seen; + std::set blocks_seen; forall_goto_program_instructions(it, goto_program) { - const unsigned block_nr = block_of(it); + const std::size_t block_nr = block_of(it); const block_infot &block_info = block_infos.at(block_nr); if( diff --git a/src/goto-instrument/cover_basic_blocks.h b/src/goto-instrument/cover_basic_blocks.h index b8ad052443c..0d929d26b34 100644 --- a/src/goto-instrument/cover_basic_blocks.h +++ b/src/goto-instrument/cover_basic_blocks.h @@ -26,18 +26,18 @@ class cover_basic_blockst final /// \param t a goto instruction /// \return the block number of the block /// the given goto instruction is part of - unsigned block_of(goto_programt::const_targett t) const; + std::size_t block_of(goto_programt::const_targett t) const; /// \param block_nr a block number /// \return the instruction selected for /// instrumentation representative of the given block optionalt - instruction_of(unsigned block_nr) const; + instruction_of(std::size_t block_nr) const; /// \param block_nr a block number /// \return the source location selected for /// instrumentation representative of the given block - const source_locationt &source_location_of(unsigned block_nr) const; + const source_locationt &source_location_of(std::size_t block_nr) const; /// Select an instruction to be instrumented for each basic block such that /// the java bytecode indices for each basic block is unique @@ -58,7 +58,7 @@ class cover_basic_blockst final void output(std::ostream &out) const; private: - typedef std::map block_mapt; + typedef std::map block_mapt; struct block_infot { @@ -71,7 +71,7 @@ class cover_basic_blockst final source_locationt source_location; /// the set of lines belonging to this block - std::unordered_set lines; + std::unordered_set lines; }; /// map program locations to block numbers @@ -85,7 +85,7 @@ class cover_basic_blockst final /// If this block is a continuation of a previous block through unconditional /// forward gotos, return this blocks number. - static optionalt continuation_of_block( + static optionalt continuation_of_block( const goto_programt::const_targett &instruction, block_mapt &block_map); }; From 3cd2f0b3d5c94c6ea5b51d9886390902def0533e Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 9 Feb 2018 16:29:17 +0000 Subject: [PATCH 2/8] Put interface to cover_blocks in virtual class This will allow to have two implementations for this functor. --- src/goto-instrument/cover_basic_blocks.h | 58 +++++++++++++++++++++--- 1 file changed, 51 insertions(+), 7 deletions(-) diff --git a/src/goto-instrument/cover_basic_blocks.h b/src/goto-instrument/cover_basic_blocks.h index 0d929d26b34..2fe8629ff86 100644 --- a/src/goto-instrument/cover_basic_blocks.h +++ b/src/goto-instrument/cover_basic_blocks.h @@ -18,7 +18,50 @@ Author: Daniel Kroening class message_handlert; -class cover_basic_blockst final +class cover_blocks_baset +{ +public: + /// \param t a goto instruction + /// \return the block number of the block + /// the given goto instruction is part of + virtual std::size_t block_of(goto_programt::const_targett t) const = 0; + + /// \param block_nr a block number + /// \return the instruction selected for + /// instrumentation representative of the given block + virtual optionalt + instruction_of(std::size_t block_nr) const = 0; + + /// \param block_nr a block number + /// \return the source location selected for + /// instrumentation representative of the given block + virtual const source_locationt & + source_location_of(std::size_t block_nr) const = 0; + + /// Select an instruction to be instrumented for each basic block such that + /// the java bytecode indices for each basic block is unique + /// \param goto_program The goto program + /// \param message_handler The message handler + virtual void select_unique_java_bytecode_indices( + const goto_programt &goto_program, + message_handlert &message_handler) + { + } + + /// Outputs the list of blocks + virtual void output(std::ostream &out) const = 0; + + /// Output warnings about ignored blocks + /// \param goto_program The goto program + /// \param message_handler The message handler + virtual void report_block_anomalies( + const goto_programt &goto_program, + message_handlert &message_handler) + { + } +}; + +class cover_basic_blockst final : public cover_blocks_baset { public: explicit cover_basic_blockst(const goto_programt &_goto_program); @@ -26,18 +69,19 @@ class cover_basic_blockst final /// \param t a goto instruction /// \return the block number of the block /// the given goto instruction is part of - std::size_t block_of(goto_programt::const_targett t) const; + std::size_t block_of(goto_programt::const_targett t) const override; /// \param block_nr a block number /// \return the instruction selected for /// instrumentation representative of the given block optionalt - instruction_of(std::size_t block_nr) const; + instruction_of(std::size_t block_nr) const override; /// \param block_nr a block number /// \return the source location selected for /// instrumentation representative of the given block - const source_locationt &source_location_of(std::size_t block_nr) const; + const source_locationt & + source_location_of(std::size_t block_nr) const override; /// Select an instruction to be instrumented for each basic block such that /// the java bytecode indices for each basic block is unique @@ -45,17 +89,17 @@ class cover_basic_blockst final /// \param message_handler The message handler void select_unique_java_bytecode_indices( const goto_programt &goto_program, - message_handlert &message_handler); + message_handlert &message_handler) override; /// Output warnings about ignored blocks /// \param goto_program The goto program /// \param message_handler The message handler void report_block_anomalies( const goto_programt &goto_program, - message_handlert &message_handler); + message_handlert &message_handler) override; /// Outputs the list of blocks - void output(std::ostream &out) const; + void output(std::ostream &out) const override; private: typedef std::map block_mapt; From acf9fe49ca764fe6a173632e09575150a895d690 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 9 Feb 2018 16:31:17 +0000 Subject: [PATCH 3/8] Refer to interface rather than cover_basic_blockst --- src/goto-instrument/cover_instrument.h | 26 +++++++++---------- .../cover_instrument_branch.cpp | 2 +- .../cover_instrument_condition.cpp | 3 ++- .../cover_instrument_decision.cpp | 2 +- .../cover_instrument_location.cpp | 4 +-- src/goto-instrument/cover_instrument_mcdc.cpp | 2 +- .../cover_instrument_other.cpp | 6 ++--- 7 files changed, 23 insertions(+), 22 deletions(-) diff --git a/src/goto-instrument/cover_instrument.h b/src/goto-instrument/cover_instrument.h index baeed5330c7..465165ae29b 100644 --- a/src/goto-instrument/cover_instrument.h +++ b/src/goto-instrument/cover_instrument.h @@ -18,7 +18,7 @@ Author: Peter Schrammel #include enum class coverage_criteriont; -class cover_basic_blockst; +class cover_blocks_baset; class goal_filterst; /// Base class for goto program coverage instrumenters @@ -40,7 +40,7 @@ class cover_instrumenter_baset /// \param basic_blocks: detected basic blocks virtual void operator()( goto_programt &goto_program, - const cover_basic_blockst &basic_blocks) const + const cover_blocks_baset &basic_blocks) const { Forall_goto_program_instructions(i_it, goto_program) { @@ -59,7 +59,7 @@ class cover_instrumenter_baset virtual void instrument( goto_programt &, goto_programt::targett &, - const cover_basic_blockst &) const = 0; + const cover_blocks_baset &) const = 0; void initialize_source_location( goto_programt::targett t, @@ -94,13 +94,13 @@ class cover_instrumenterst /// \param basic_blocks: detected basic blocks of the goto program void operator()( goto_programt &goto_program, - const cover_basic_blockst &basic_blocks) const + const cover_blocks_baset &basic_blocks) const { for(const auto &instrumenter : instrumenters) (*instrumenter)(goto_program, basic_blocks); } -protected: +private: std::vector> instrumenters; }; @@ -119,7 +119,7 @@ class cover_location_instrumentert : public cover_instrumenter_baset void instrument( goto_programt &, goto_programt::targett &, - const cover_basic_blockst &) const override; + const cover_blocks_baset &) const override; }; /// Branch coverage instrumenter @@ -137,7 +137,7 @@ class cover_branch_instrumentert : public cover_instrumenter_baset void instrument( goto_programt &, goto_programt::targett &, - const cover_basic_blockst &) const override; + const cover_blocks_baset &) const override; }; /// Condition coverage instrumenter @@ -155,7 +155,7 @@ class cover_condition_instrumentert : public cover_instrumenter_baset void instrument( goto_programt &, goto_programt::targett &, - const cover_basic_blockst &) const override; + const cover_blocks_baset &) const override; }; /// Decision coverage instrumenter @@ -173,7 +173,7 @@ class cover_decision_instrumentert : public cover_instrumenter_baset void instrument( goto_programt &, goto_programt::targett &, - const cover_basic_blockst &) const override; + const cover_blocks_baset &) const override; }; /// MC/DC coverage instrumenter @@ -191,7 +191,7 @@ class cover_mcdc_instrumentert : public cover_instrumenter_baset void instrument( goto_programt &, goto_programt::targett &, - const cover_basic_blockst &) const override; + const cover_blocks_baset &) const override; }; /// Path coverage instrumenter @@ -209,7 +209,7 @@ class cover_path_instrumentert : public cover_instrumenter_baset void instrument( goto_programt &, goto_programt::targett &, - const cover_basic_blockst &) const override; + const cover_blocks_baset &) const override; }; /// Assertion coverage instrumenter @@ -227,7 +227,7 @@ class cover_assertion_instrumentert : public cover_instrumenter_baset void instrument( goto_programt &, goto_programt::targett &, - const cover_basic_blockst &) const override; + const cover_blocks_baset &) const override; }; /// __CPROVER_cover coverage instrumenter @@ -245,7 +245,7 @@ class cover_cover_instrumentert : public cover_instrumenter_baset void instrument( goto_programt &, goto_programt::targett &, - const cover_basic_blockst &) const override; + const cover_blocks_baset &) const override; }; void cover_instrument_end_of_function( diff --git a/src/goto-instrument/cover_instrument_branch.cpp b/src/goto-instrument/cover_instrument_branch.cpp index 0060ff72629..c63c0fbb36c 100644 --- a/src/goto-instrument/cover_instrument_branch.cpp +++ b/src/goto-instrument/cover_instrument_branch.cpp @@ -15,7 +15,7 @@ Author: Daniel Kroening void cover_branch_instrumentert::instrument( goto_programt &goto_program, goto_programt::targett &i_it, - const cover_basic_blockst &basic_blocks) const + const cover_blocks_baset &basic_blocks) const { if(is_non_cover_assertion(i_it)) i_it->make_skip(); diff --git a/src/goto-instrument/cover_instrument_condition.cpp b/src/goto-instrument/cover_instrument_condition.cpp index 1bc3b2769b1..47cf555ca22 100644 --- a/src/goto-instrument/cover_instrument_condition.cpp +++ b/src/goto-instrument/cover_instrument_condition.cpp @@ -14,11 +14,12 @@ Author: Daniel Kroening #include #include "cover_util.h" +#include "cover_basic_blocks.h" void cover_condition_instrumentert::instrument( goto_programt &goto_program, goto_programt::targett &i_it, - const cover_basic_blockst &basic_blocks) const + const cover_blocks_baset &basic_blocks) const { if(is_non_cover_assertion(i_it)) i_it->make_skip(); diff --git a/src/goto-instrument/cover_instrument_decision.cpp b/src/goto-instrument/cover_instrument_decision.cpp index 122e05046e3..c6cda3c397a 100644 --- a/src/goto-instrument/cover_instrument_decision.cpp +++ b/src/goto-instrument/cover_instrument_decision.cpp @@ -18,7 +18,7 @@ Author: Daniel Kroening void cover_decision_instrumentert::instrument( goto_programt &goto_program, goto_programt::targett &i_it, - const cover_basic_blockst &basic_blocks) const + const cover_blocks_baset &basic_blocks) const { if(is_non_cover_assertion(i_it)) i_it->make_skip(); diff --git a/src/goto-instrument/cover_instrument_location.cpp b/src/goto-instrument/cover_instrument_location.cpp index c0655255bac..638f74c4e9e 100644 --- a/src/goto-instrument/cover_instrument_location.cpp +++ b/src/goto-instrument/cover_instrument_location.cpp @@ -17,12 +17,12 @@ Author: Daniel Kroening void cover_location_instrumentert::instrument( goto_programt &goto_program, goto_programt::targett &i_it, - const cover_basic_blockst &basic_blocks) const + const cover_blocks_baset &basic_blocks) const { if(is_non_cover_assertion(i_it)) i_it->make_skip(); - const unsigned block_nr = basic_blocks.block_of(i_it); + const std::size_t block_nr = basic_blocks.block_of(i_it); const auto representative_instruction = basic_blocks.instruction_of(block_nr); // we only instrument the selected instruction if(representative_instruction && *representative_instruction == i_it) diff --git a/src/goto-instrument/cover_instrument_mcdc.cpp b/src/goto-instrument/cover_instrument_mcdc.cpp index e06508d84d8..4873975e423 100644 --- a/src/goto-instrument/cover_instrument_mcdc.cpp +++ b/src/goto-instrument/cover_instrument_mcdc.cpp @@ -639,7 +639,7 @@ void minimize_mcdc_controlling( void cover_mcdc_instrumentert::instrument( goto_programt &goto_program, goto_programt::targett &i_it, - const cover_basic_blockst &basic_blocks) const + const cover_blocks_baset &basic_blocks) const { if(is_non_cover_assertion(i_it)) i_it->make_skip(); diff --git a/src/goto-instrument/cover_instrument_other.cpp b/src/goto-instrument/cover_instrument_other.cpp index bc97a809da9..740eecd1a67 100644 --- a/src/goto-instrument/cover_instrument_other.cpp +++ b/src/goto-instrument/cover_instrument_other.cpp @@ -18,7 +18,7 @@ Author: Daniel Kroening void cover_path_instrumentert::instrument( goto_programt &goto_program, goto_programt::targett &i_it, - const cover_basic_blockst &basic_blocks) const + const cover_blocks_baset &basic_blocks) const { if(is_non_cover_assertion(i_it)) i_it->make_skip(); @@ -29,7 +29,7 @@ void cover_path_instrumentert::instrument( void cover_assertion_instrumentert::instrument( goto_programt &goto_program, goto_programt::targett &i_it, - const cover_basic_blockst &basic_blocks) const + const cover_blocks_baset &basic_blocks) const { // turn into 'assert(false)' to avoid simplification if(is_non_cover_assertion(i_it)) @@ -43,7 +43,7 @@ void cover_assertion_instrumentert::instrument( void cover_cover_instrumentert::instrument( goto_programt &goto_program, goto_programt::targett &i_it, - const cover_basic_blockst &basic_blocks) const + const cover_blocks_baset &basic_blocks) const { // turn __CPROVER_cover(x) into 'assert(!x)' if(i_it->is_function_call()) From 681123873a2d126d938f44316b7f5561f85c1135 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 9 Feb 2018 16:31:49 +0000 Subject: [PATCH 4/8] cover_block implementation using bytecode location This is a specific implementation of cover block for Java. It uses the bytecode index to determine blocks and replace the use of select_unique_java_bytecode_indices. --- src/goto-instrument/cover.cpp | 26 +++-- src/goto-instrument/cover.h | 1 + src/goto-instrument/cover_basic_blocks.cpp | 113 ++++++++------------- src/goto-instrument/cover_basic_blocks.h | 49 +++++---- 4 files changed, 95 insertions(+), 94 deletions(-) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 750cdd5e010..a5ac36f4b0d 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -24,18 +24,23 @@ Date: May 2016 /// Applies instrumenters to given goto program /// \param goto_program: the goto program /// \param instrumenters: the instrumenters +/// \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( goto_programt &goto_program, const cover_instrumenterst &instrumenters, + const irep_idt &mode, message_handlert &message_handler) { - cover_basic_blockst basic_blocks(goto_program); - basic_blocks.select_unique_java_bytecode_indices( - goto_program, message_handler); - basic_blocks.report_block_anomalies(goto_program, message_handler); - - instrumenters(goto_program, basic_blocks); + const std::unique_ptr basic_blocks = + mode == ID_java ? std::unique_ptr( + new cover_basic_blocks_javat(goto_program)) + : std::unique_ptr( + new cover_basic_blockst(goto_program)); + + basic_blocks->report_block_anomalies(goto_program, message_handler); + instrumenters(goto_program, *basic_blocks); } /// Instruments goto program for a given coverage criterion @@ -43,6 +48,9 @@ void instrument_cover_goals( /// \param goto_program: the goto program /// \param criterion: the coverage criterion /// \param message_handler: a message handler +/// \deprecated use instrument_cover_goals(goto_programt &goto_program, +/// const cover_instrumenterst &instrumenters, +/// message_handlert &message_handler, const irep_idt mode) instead void instrument_cover_goals( const symbol_tablet &symbol_table, goto_programt &goto_program, @@ -55,7 +63,8 @@ void instrument_cover_goals( cover_instrumenterst instrumenters; instrumenters.add_from_criterion(criterion, symbol_table, goal_filters); - instrument_cover_goals(goto_program, instrumenters, message_handler); + instrument_cover_goals( + goto_program, instrumenters, ID_unknown, message_handler); } /// Create and add an instrumenter based on the given criterion @@ -257,7 +266,7 @@ static void instrument_cover_goals( if(config.function_filters(function_id, function)) { instrument_cover_goals( - function.body, config.cover_instrumenters, message_handler); + function.body, config.cover_instrumenters, config.mode, message_handler); changed = true; } @@ -320,6 +329,7 @@ bool instrument_cover_goals( Forall_goto_functions(f_it, goto_functions) { + config->mode = symbol_table.lookup(f_it->first)->mode; instrument_cover_goals( *config, f_it->first, f_it->second, message_handler); } diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index 75352ac9039..7e1967c5477 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -38,6 +38,7 @@ struct cover_configt { bool keep_assertions; bool traces_must_terminate; + irep_idt mode; function_filterst function_filters; goal_filterst goal_filters; cover_instrumenterst cover_instrumenters; diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp index bffdabbe230..160fcd93750 100644 --- a/src/goto-instrument/cover_basic_blocks.cpp +++ b/src/goto-instrument/cover_basic_blocks.cpp @@ -108,74 +108,6 @@ cover_basic_blockst::source_location_of(const std::size_t block_nr) const return block_infos.at(block_nr).source_location; } -void cover_basic_blockst::select_unique_java_bytecode_indices( - const goto_programt &goto_program, - message_handlert &message_handler) -{ - messaget msg(message_handler); - std::set blocks_seen; - std::set bytecode_indices_seen; - - forall_goto_program_instructions(it, goto_program) - { - const std::size_t block_nr = block_of(it); - if(blocks_seen.find(block_nr) != blocks_seen.end()) - continue; - - INVARIANT(block_nr < block_infos.size(), "block number out of range"); - block_infot &block_info = block_infos.at(block_nr); - if(!block_info.representative_inst) - { - if(!it->source_location.get_java_bytecode_index().empty()) - { - // search for a representative - if( - bytecode_indices_seen - .insert(it->source_location.get_java_bytecode_index()) - .second) - { - block_info.representative_inst = it; - block_info.source_location = it->source_location; - update_covered_lines(block_info); - blocks_seen.insert(block_nr); - msg.debug() << it->function << " block " << (block_nr + 1) - << ": location " << it->location_number - << ", bytecode-index " - << it->source_location.get_java_bytecode_index() - << " selected for instrumentation." << messaget::eom; - } - } - } - else if(it == *block_info.representative_inst) - { - // check the existing representative - if(!it->source_location.get_java_bytecode_index().empty()) - { - if( - bytecode_indices_seen - .insert(it->source_location.get_java_bytecode_index()) - .second) - { - blocks_seen.insert(block_nr); - } - else - { - // clash, reset to search for a new one - block_info.representative_inst = {}; - block_info.source_location = source_locationt::nil(); - msg.debug() << it->function << " block " << (block_nr + 1) - << ", location " << it->location_number - << ": bytecode-index " - << it->source_location.get_java_bytecode_index() - << " already instrumented." - << " Searching for alternative instruction" - << " to instrument." << messaget::eom; - } - } - } - } -} - void cover_basic_blockst::report_block_anomalies( const goto_programt &goto_program, message_handlert &message_handler) @@ -228,3 +160,48 @@ void cover_basic_blockst::update_covered_lines(block_infot &block_info) std::string covered_lines = format_number_range(line_list); block_info.source_location.set_basic_block_covered_lines(covered_lines); } + +cover_basic_blocks_javat::cover_basic_blocks_javat( + const goto_programt &_goto_program) +{ + forall_goto_program_instructions(it, _goto_program) + { + const auto &location = it->source_location; + const auto &bytecode_index = location.get_java_bytecode_index(); + if(index_to_block.emplace(bytecode_index, block_infos.size()).second) + { + block_infos.push_back(it); + block_locations.push_back(location); + block_locations.back().set_basic_block_covered_lines(location.get_line()); + } + } +} + +std::size_t +cover_basic_blocks_javat::block_of(goto_programt::const_targett t) const +{ + const auto &bytecode_index = t->source_location.get_java_bytecode_index(); + const auto it = index_to_block.find(bytecode_index); + INVARIANT(it != index_to_block.end(), "instruction must be part of a block"); + return it->second; +} + +optionalt +cover_basic_blocks_javat::instruction_of(const std::size_t block_nr) const +{ + PRECONDITION(block_nr < block_infos.size()); + return block_infos[block_nr]; +} + +const source_locationt & +cover_basic_blocks_javat::source_location_of(const std::size_t block_nr) const +{ + PRECONDITION(block_nr < block_locations.size()); + return block_locations[block_nr]; +} + +void cover_basic_blocks_javat::output(std::ostream &out) const +{ + for(std::size_t i = 0; i < block_locations.size(); ++i) + out << block_locations[i] << " -> " << i << '\n'; +} diff --git a/src/goto-instrument/cover_basic_blocks.h b/src/goto-instrument/cover_basic_blocks.h index 2fe8629ff86..25d37d7df80 100644 --- a/src/goto-instrument/cover_basic_blocks.h +++ b/src/goto-instrument/cover_basic_blocks.h @@ -38,16 +38,6 @@ class cover_blocks_baset virtual const source_locationt & source_location_of(std::size_t block_nr) const = 0; - /// Select an instruction to be instrumented for each basic block such that - /// the java bytecode indices for each basic block is unique - /// \param goto_program The goto program - /// \param message_handler The message handler - virtual void select_unique_java_bytecode_indices( - const goto_programt &goto_program, - message_handlert &message_handler) - { - } - /// Outputs the list of blocks virtual void output(std::ostream &out) const = 0; @@ -83,14 +73,6 @@ class cover_basic_blockst final : public cover_blocks_baset const source_locationt & source_location_of(std::size_t block_nr) const override; - /// Select an instruction to be instrumented for each basic block such that - /// the java bytecode indices for each basic block is unique - /// \param goto_program The goto program - /// \param message_handler The message handler - void select_unique_java_bytecode_indices( - const goto_programt &goto_program, - message_handlert &message_handler) override; - /// Output warnings about ignored blocks /// \param goto_program The goto program /// \param message_handler The message handler @@ -134,4 +116,35 @@ class cover_basic_blockst final : public cover_blocks_baset block_mapt &block_map); }; +class cover_basic_blocks_javat final : public cover_blocks_baset +{ +private: + // map block number to first instruction of the block + std::vector block_infos; + // map block number to its location + std::vector block_locations; + // map java indexes to block indexes + std::unordered_map index_to_block; + +public: + explicit cover_basic_blocks_javat(const goto_programt &_goto_program); + + /// \param t a goto instruction + /// \return block number the given goto instruction is part of + std::size_t block_of(goto_programt::const_targett t) const override; + + /// \param block_number a block number + /// \return first instruction of the given block + optionalt + instruction_of(std::size_t block_number) const override; + + /// \param block_number a block number + /// \return source location corresponding to the given block + const source_locationt & + source_location_of(std::size_t block_number) const override; + + /// Outputs the list of blocks + void output(std::ostream &out) const override; +}; + #endif // CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H From c1045aa66ee48e39932c987ab766678912fb2e2f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 14 Feb 2018 07:20:11 +0000 Subject: [PATCH 5/8] Use [] instead of `at` on vector The index is checked against the size before end so there is no need to use at there. --- src/goto-instrument/cover_basic_blocks.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp index 160fcd93750..f8d85f16061 100644 --- a/src/goto-instrument/cover_basic_blocks.cpp +++ b/src/goto-instrument/cover_basic_blocks.cpp @@ -98,14 +98,14 @@ optionalt cover_basic_blockst::instruction_of(const std::size_t block_nr) const { INVARIANT(block_nr < block_infos.size(), "block number out of range"); - return block_infos.at(block_nr).representative_inst; + return block_infos[block_nr].representative_inst; } const source_locationt & cover_basic_blockst::source_location_of(const std::size_t block_nr) const { INVARIANT(block_nr < block_infos.size(), "block number out of range"); - return block_infos.at(block_nr).source_location; + return block_infos[block_nr].source_location; } void cover_basic_blockst::report_block_anomalies( From 105c7e35c212deb439870d4b513f27e9fae20a40 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 14 Feb 2018 11:13:37 +0000 Subject: [PATCH 6/8] Adapt coverage test for new instrumentation JBMC use to group together several lines within the same block. This is no longer the case for the Java specific block instrumentation. Each line is part of a different goal. --- regression/cbmc-java/covered1/test.desc | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/regression/cbmc-java/covered1/test.desc b/regression/cbmc-java/covered1/test.desc index 6f78ed37e63..8982c0321db 100644 --- a/regression/cbmc-java/covered1/test.desc +++ b/regression/cbmc-java/covered1/test.desc @@ -4,7 +4,16 @@ covered1.class ^EXIT=0$ ^SIGNAL=0$ .*\"coveredLines\": \"22\",$ -.*\"coveredLines\": \"4,6,7,23-25,31-33,36\",$ +.*\"coveredLines\": \"4\",$ +.*\"coveredLines\": \"6\",$ +.*\"coveredLines\": \"7\",$ +.*\"coveredLines\": \"23\",$ +.*\"coveredLines\": \"24\",$ +.*\"coveredLines\": \"25\",$ +.*\"coveredLines\": \"31\",$ +.*\"coveredLines\": \"32\",$ +.*\"coveredLines\": \"33\",$ +.*\"coveredLines\": \"36\",$ .*\"coveredLines\": \"26\",$ .*\"coveredLines\": \"28\",$ .*\"coveredLines\": \"28\",$ From 5f540496a1c7f8c1d7fbd76f235fa4731e746c6b Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 15 Feb 2018 07:40:25 +0000 Subject: [PATCH 7/8] Add unit tests for java block instrumentation This checks that coverage instrumentation assertions are added at the first instruction with given bytecode index. And that there is no such assertion in the middle of instructions with same bytecode index. --- src/goto-instrument/Makefile | 7 ++- unit/CMakeLists.txt | 11 +++- unit/Makefile | 1 + .../virtual_functions.cpp | 54 +++++++++++++++++-- 4 files changed, 67 insertions(+), 6 deletions(-) diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 720a3981d3c..9fe42bddd18 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -94,12 +94,12 @@ INCLUDES= -I .. LIBS = -CLEANFILES = goto-instrument$(EXEEXT) +CLEANFILES = goto-instrument$(EXEEXT) goto-instrument$(LIBEXT) include ../config.inc include ../common -all: goto-instrument$(EXEEXT) +all: goto-instrument$(EXEEXT) goto-instrument$(LIBEXT) ifneq ($(LIB_GLPK),) LIBS += $(LIB_GLPK) @@ -111,6 +111,9 @@ endif goto-instrument$(EXEEXT): $(OBJ) $(LINKBIN) +goto-instrument$(LIBEXT): $(OBJ) + $(LINKLIB) + .PHONY: goto-instrument-mac-signed goto-instrument-mac-signed: goto-instrument$(EXEEXT) diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt index 166c1f8c894..21316d73a38 100644 --- a/unit/CMakeLists.txt +++ b/unit/CMakeLists.txt @@ -36,7 +36,16 @@ target_include_directories(unit ${CBMC_SOURCE_DIR} ${CMAKE_CURRENT_SOURCE_DIR} ) -target_link_libraries(unit testing-utils ansi-c solvers java_bytecode) +target_link_libraries( + unit + testing-utils + ansi-c + solvers + java_bytecode + goto-programs + goto-instrument-lib +) + add_test( NAME unit COMMAND $ diff --git a/unit/Makefile b/unit/Makefile index 20185bd20ed..f1e08911e9a 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -68,6 +68,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \ ../src/util/util$(LIBEXT) \ ../src/big-int/big-int$(LIBEXT) \ ../src/goto-programs/goto-programs$(LIBEXT) \ + ../src/goto-instrument/goto-instrument$(LIBEXT) \ ../src/pointer-analysis/pointer-analysis$(LIBEXT) \ ../src/langapi/langapi$(LIBEXT) \ ../src/assembler/assembler$(LIBEXT) \ diff --git a/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp b/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp index 128c19b2e5b..f093ec81d57 100644 --- a/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp +++ b/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp @@ -8,13 +8,13 @@ #include #include -#include #include #include #include - -#include +#include +#include +#include void check_function_call( const equal_exprt &eq_expr, @@ -115,6 +115,54 @@ SCENARIO( } REQUIRE(found_function); + + WHEN("basic blocks are instrumented") + { + optionst options; + options.set_option("cover", "location"); + REQUIRE_FALSE( + instrument_cover_goals( + options, new_table, new_goto_functions, null_output)); + + auto function = new_goto_functions.function_map.find(function_name); + REQUIRE(function != new_goto_functions.function_map.end()); + + const goto_programt &goto_program = function->second.body; + // Skip the first instruction which is a declaration with no location + auto it = std::next(goto_program.instructions.begin()); + REQUIRE(it != goto_program.instructions.end()); + + THEN( + "Each instruction with a new bytecode index begins with ASSERT" + " and coverage assertions are at the beginning of the block") + { + irep_idt current_index; + + while(it->type != goto_program_instruction_typet::END_FUNCTION) + { + const source_locationt &loc = it->source_location; + REQUIRE(loc != source_locationt::nil()); + REQUIRE_FALSE(loc.get_java_bytecode_index().empty()); + const auto new_index = loc.get_java_bytecode_index(); + + if(new_index != current_index) + { + current_index = new_index; + // instruction with a new bytecode index begins with ASSERT + REQUIRE(it->type == goto_program_instruction_typet::ASSERT); + // the assertion corresponds to a line coverage goal + REQUIRE_FALSE(loc.get_basic_block_covered_lines().empty()); + } + else + { + // there is no line coverage goal in the middle of a block + REQUIRE(loc.get_basic_block_covered_lines().empty()); + } + + ++it; + } + } + } } } } From 63beb71c8af6ef188859a0ba2c0a7fba15bda0bf Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 20 Feb 2018 15:20:24 +0000 Subject: [PATCH 8/8] Update coverage goals in goto-diff test This test mentions explicitely goal numbers, which are changed by the java specific instrumentation. This also fix potential problems with left braces that were not escaped in the regular expression. --- regression/goto-diff/java-properties/test.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/goto-diff/java-properties/test.desc b/regression/goto-diff/java-properties/test.desc index a615e2bf421..895f7360e7f 100644 --- a/regression/goto-diff/java-properties/test.desc +++ b/regression/goto-diff/java-properties/test.desc @@ -5,6 +5,6 @@ old.jar --json-ui --show-properties --cover location activate-multi-line-match EXIT=0 SIGNAL=0 - "deletedFunctions": \[\n {\n "name": "java::Test\.obsolete:\(\)V",\n "properties": \[\n {\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test\.obsolete:\(\)V\.coverage\.1",\n "sourceLocation": {\n "bytecodeIndex": "0",\n "file": "Test\.java",\n "function": "java::Test\.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": {\n "file": "Test\.java",\n "function": "java::Test\.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "modifiedFunctions": \[\n {\n "name": "java::Test\.:\(\)V",\n "properties": \[\n {\n "class": "coverage",\n "coveredLines": "6",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test\.:\(\)V\.coverage\.1",\n "sourceLocation": {\n "bytecodeIndex": "1",\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "6"\n }\n },\n {\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 2",\n "expression": "false",\n "name": "java::Test\.:\(\)V\.coverage\.2",\n "sourceLocation": {\n "bytecodeIndex": "3",\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "4"\n }\n },\n {\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 3",\n "expression": "false",\n "name": "java::Test\.:\(\)V\.coverage\.3",\n "sourceLocation": {\n "bytecodeIndex": "5",\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "4"\n }\n },\n {\n "class": "coverage",\n "coveredLines": "4,7",\n "description": "block 4",\n "expression": "false",\n "name": "java::Test\.:\(\)V\.coverage\.4",\n "sourceLocation": {\n "bytecodeIndex": "6",\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "4"\n }\n }\n ],\n "sourceLocation": {\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "6"\n }\n },\n {\n "name": "java::Test\.:\(\)V",\n "properties": \[\n {\n "class": "coverage",\n "coveredLines": "3",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test\.:\(\)V\.coverage\.1",\n "sourceLocation": {\n "bytecodeIndex": "1",\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "3"\n }\n }\n ],\n "sourceLocation": {\n "file": "Test\.java",\n "function": "java::Test\.:\(\)V",\n "line": "3"\n }\n }\n ],\n "newFunctions": \[\n {\n "name": "java::Test\.newfun:\(\)V",\n "properties": \[\n {\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test\.newfun:\(\)V\.coverage\.1",\n "sourceLocation": {\n "bytecodeIndex": "0",\n "file": "Test\.java",\n "function": "java::Test\.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": {\n "file": "Test\.java",\n "function": "java::Test\.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n + "deletedFunctions": \[\n \{\n "name": "java::Test.obsolete:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test.obsolete:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "0",\n "file": "Test.java",\n "function": "java::Test.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.obsolete:\(\)V",\n "line": "18"\n }\n }\n ],\n "modifiedFunctions": \[\n \{\n "name": "java::Test.:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "6",\n "description": "block 2",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "6"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 3",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.2",\n "sourceLocation": \{\n "bytecodeIndex": "3",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 4",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.3",\n "sourceLocation": \{\n "bytecodeIndex": "5",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "4",\n "description": "block 5",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.4",\n "sourceLocation": \{\n "bytecodeIndex": "6",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "4"\n }\n },\n \{\n "class": "coverage",\n "coveredLines": "7",\n "description": "block 6",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.5",\n "sourceLocation": \{\n "bytecodeIndex": "7",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "7"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "6"\n }\n },\n \{\n "name": "java::Test.:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "3",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test.:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "1",\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "3"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.:\(\)V",\n "line": "3"\n }\n }\n ],\n "newFunctions": \[\n \{\n "name": "java::Test.newfun:\(\)V",\n "properties": \[\n \{\n "class": "coverage",\n "coveredLines": "18",\n "description": "block 1",\n "expression": "false",\n "name": "java::Test.newfun:\(\)V.coverage.1",\n "sourceLocation": \{\n "bytecodeIndex": "0",\n "file": "Test.java",\n "function": "java::Test.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n "sourceLocation": \{\n "file": "Test.java",\n "function": "java::Test.newfun:\(\)V",\n "line": "18"\n }\n }\n ],\n -- ^warning: ignoring