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\",$ 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 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/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 9288281d4f7..f8d85f16061 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,85 +95,17 @@ 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; + return block_infos[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; -} - -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 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) - { - 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; - } - } - } - } + return block_infos[block_nr].source_location; } void cover_basic_blockst::report_block_anomalies( @@ -181,10 +113,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( @@ -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 b8ad052443c..25d37d7df80 100644 --- a/src/goto-instrument/cover_basic_blocks.h +++ b/src/goto-instrument/cover_basic_blocks.h @@ -18,47 +18,73 @@ Author: Daniel Kroening class message_handlert; -class cover_basic_blockst final +class cover_blocks_baset { public: - explicit cover_basic_blockst(const goto_programt &_goto_program); - /// \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; + 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 - optionalt - instruction_of(unsigned block_nr) const; + 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 - const source_locationt &source_location_of(unsigned block_nr) const; + virtual const source_locationt & + source_location_of(std::size_t block_nr) const = 0; + + /// Outputs the list of blocks + virtual void output(std::ostream &out) const = 0; - /// Select an instruction to be instrumented for each basic block such that - /// the java bytecode indices for each basic block is unique + /// Output warnings about ignored blocks /// \param goto_program The goto program /// \param message_handler The message handler - void select_unique_java_bytecode_indices( + virtual void report_block_anomalies( const goto_programt &goto_program, - message_handlert &message_handler); + message_handlert &message_handler) + { + } +}; + +class cover_basic_blockst final : public cover_blocks_baset +{ +public: + explicit cover_basic_blockst(const goto_programt &_goto_program); + + /// \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 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 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 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; + typedef std::map block_mapt; struct block_infot { @@ -71,7 +97,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,9 +111,40 @@ 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); }; +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 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()) 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; + } + } + } } } }