diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp index 87a40c0708f..9288281d4f7 100644 --- a/src/goto-instrument/cover_basic_blocks.cpp +++ b/src/goto-instrument/cover_basic_blocks.cpp @@ -15,6 +15,20 @@ Author: Peter Schrammel #include #include +optionalt cover_basic_blockst::continuation_of_block( + const goto_programt::const_targett &instruction, + cover_basic_blockst::block_mapt &block_map) +{ + if(instruction->incoming_edges.size() != 1) + return {}; + + const goto_programt::targett in_t = *instruction->incoming_edges.cbegin(); + if(in_t->is_goto() && !in_t->is_backwards_goto() && in_t->guard.is_true()) + return block_map[in_t]; + + return {}; +} + cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program) { bool next_is_target = true; @@ -25,25 +39,13 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program) // Is it a potential beginning of a block? if(next_is_target || it->is_target()) { - // We keep the block number if this potential block - // is a continuation of a previous block through - // unconditional forward gotos; otherwise we increase the - // block number. - bool increase_block_nr = true; - if(it->incoming_edges.size() == 1) + if(auto block_number = continuation_of_block(it, block_map)) { - goto_programt::targett in_t = *it->incoming_edges.begin(); - if( - in_t->is_goto() && !in_t->is_backwards_goto() && - in_t->guard.is_true()) - { - current_block = block_map[in_t]; - increase_block_nr = false; - } + current_block = *block_number; } - if(increase_block_nr) + else { - block_infos.push_back(block_infot()); + block_infos.emplace_back(); block_infos.back().representative_inst = it; block_infos.back().source_location = source_locationt::nil(); current_block = block_infos.size() - 1; @@ -87,12 +89,12 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program) unsigned cover_basic_blockst::block_of(goto_programt::const_targett t) const { - block_mapt::const_iterator it = block_map.find(t); + const auto it = block_map.find(t); INVARIANT(it != block_map.end(), "instruction must be part of a block"); return it->second; } -goto_programt::const_targett +optionalt cover_basic_blockst::instruction_of(unsigned block_nr) const { INVARIANT(block_nr < block_infos.size(), "block number out of range"); @@ -116,13 +118,13 @@ void cover_basic_blockst::select_unique_java_bytecode_indices( forall_goto_program_instructions(it, goto_program) { - unsigned block_nr = block_of(it); + const unsigned 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 == goto_program.instructions.end()) + if(!block_info.representative_inst) { if(!it->source_location.get_java_bytecode_index().empty()) { @@ -144,7 +146,7 @@ void cover_basic_blockst::select_unique_java_bytecode_indices( } } } - else if(it == block_info.representative_inst) + else if(it == *block_info.representative_inst) { // check the existing representative if(!it->source_location.get_java_bytecode_index().empty()) @@ -159,7 +161,7 @@ void cover_basic_blockst::select_unique_java_bytecode_indices( else { // clash, reset to search for a new one - block_info.representative_inst = goto_program.instructions.end(); + block_info.representative_inst = {}; block_info.source_location = source_locationt::nil(); msg.debug() << it->function << " block " << (block_nr + 1) << ", location " << it->location_number @@ -182,7 +184,7 @@ void cover_basic_blockst::report_block_anomalies( std::set blocks_seen; forall_goto_program_instructions(it, goto_program) { - unsigned block_nr = block_of(it); + const unsigned block_nr = block_of(it); const block_infot &block_info = block_infos.at(block_nr); if( @@ -223,7 +225,6 @@ void cover_basic_blockst::update_covered_lines(block_infot &block_info) INVARIANT(!cover_set.empty(), "covered lines set must not be empty"); std::vector line_list(cover_set.begin(), cover_set.end()); - format_number_ranget format_lines; - std::string covered_lines = format_lines(line_list); + std::string covered_lines = format_number_range(line_list); block_info.source_location.set_basic_block_covered_lines(covered_lines); } diff --git a/src/goto-instrument/cover_basic_blocks.h b/src/goto-instrument/cover_basic_blocks.h index daab1ab0447..b8ad052443c 100644 --- a/src/goto-instrument/cover_basic_blocks.h +++ b/src/goto-instrument/cover_basic_blocks.h @@ -18,7 +18,7 @@ Author: Daniel Kroening class message_handlert; -class cover_basic_blockst +class cover_basic_blockst final { public: explicit cover_basic_blockst(const goto_programt &_goto_program); @@ -31,7 +31,8 @@ class cover_basic_blockst /// \param block_nr a block number /// \return the instruction selected for /// instrumentation representative of the given block - goto_programt::const_targett instruction_of(unsigned block_nr) const; + optionalt + instruction_of(unsigned block_nr) const; /// \param block_nr a block number /// \return the source location selected for @@ -56,32 +57,37 @@ class cover_basic_blockst /// Outputs the list of blocks void output(std::ostream &out) const; -protected: - // map program locations to block numbers +private: typedef std::map block_mapt; - block_mapt block_map; struct block_infot { /// the program location to instrument for this block - goto_programt::const_targett representative_inst; + optionalt representative_inst; /// the source location representative for this block - // (we need a separate copy of source locations because we attach - // the line number ranges to them) + /// (we need a separate copy of source locations because we attach + /// the line number ranges to them) source_locationt source_location; - // map block numbers to source code locations /// the set of lines belonging to this block std::unordered_set lines; }; - typedef std::vector block_infost; - block_infost block_infos; + /// map program locations to block numbers + block_mapt block_map; + /// map block numbers to block information + std::vector block_infos; /// create list of covered lines as CSV string and set as property of source /// location of basic block, compress to ranges if applicable - void update_covered_lines(block_infot &block_info); + static void update_covered_lines(block_infot &block_info); + + /// If this block is a continuation of a previous block through unconditional + /// forward gotos, return this blocks number. + static optionalt continuation_of_block( + const goto_programt::const_targett &instruction, + block_mapt &block_map); }; #endif // CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H diff --git a/src/goto-instrument/cover_instrument_location.cpp b/src/goto-instrument/cover_instrument_location.cpp index 214b00248c2..c0655255bac 100644 --- a/src/goto-instrument/cover_instrument_location.cpp +++ b/src/goto-instrument/cover_instrument_location.cpp @@ -22,20 +22,19 @@ void cover_location_instrumentert::instrument( if(is_non_cover_assertion(i_it)) i_it->make_skip(); - unsigned block_nr = basic_blocks.block_of(i_it); - goto_programt::const_targett in_t = basic_blocks.instruction_of(block_nr); + const unsigned 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(in_t == i_it) + if(representative_instruction && *representative_instruction == i_it) { - std::string b = std::to_string(block_nr + 1); // start with 1 - std::string id = id2string(i_it->function) + "#" + b; - source_locationt source_location = - basic_blocks.source_location_of(block_nr); + const std::string b = std::to_string(block_nr + 1); // start with 1 + const std::string id = id2string(i_it->function) + "#" + b; + const auto source_location = basic_blocks.source_location_of(block_nr); // filter goals if(goal_filters(source_location)) { - std::string comment = "block " + b; + const std::string comment = "block " + b; const irep_idt function = i_it->function; goto_program.insert_before_swap(i_it); i_it->make_assertion(false_exprt()); diff --git a/src/util/format_number_range.cpp b/src/util/format_number_range.cpp index c3cc9d24b9c..2a88d94f2ff 100644 --- a/src/util/format_number_range.cpp +++ b/src/util/format_number_range.cpp @@ -16,9 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "format_number_range.h" /// create shorter representation for output -/// \par parameters: vector of numbers +/// \param parameters: vector of numbers /// \return string of compressed number range representation -std::string format_number_ranget::operator()(std::vector &numbers) +std::string format_number_range(std::vector &numbers) { std::string number_range; std::sort(numbers.begin(), numbers.end()); diff --git a/src/util/format_number_range.h b/src/util/format_number_range.h index 493b82abc99..98c54d9a533 100644 --- a/src/util/format_number_range.h +++ b/src/util/format_number_range.h @@ -15,10 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -class format_number_ranget -{ -public: - std::string operator()(std::vector &); -}; +std::string format_number_range(std::vector &); #endif // CPROVER_UTIL_FORMAT_NUMBER_RANGE_H