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_filter.cpp b/src/goto-instrument/cover_filter.cpp index 3ca83843170..9bd2634fb16 100644 --- a/src/goto-instrument/cover_filter.cpp +++ b/src/goto-instrument/cover_filter.cpp @@ -101,5 +101,8 @@ operator()(const source_locationt &source_location) const if(source_location.is_built_in()) return false; + if(source_location.get_java_removed_virtual_call()) + return false; + return true; } diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 00a9c459b0d..7e674f35298 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -276,6 +276,8 @@ void remove_virtual_functionst::remove_virtual_function( const irep_idt property_class=it->source_location.get_property_class(); const irep_idt comment=it->source_location.get_comment(); it->source_location=target->source_location; + // mark instruction as originating from a removed virtual function call + it->source_location.set_java_removed_virtual_call(); it->function=target->function; if(!property_class.empty()) it->source_location.set_property_class(property_class); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 2cd85d63963..eb204346d22 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -840,6 +840,7 @@ IREP_ID_TWO(type_variables, #type_variables) IREP_ID_ONE(havoc_object) IREP_ID_TWO(overflow_shl, overflow-shl) IREP_ID_TWO(C_no_initialization_required, #no_initialization_required) +IREP_ID_TWO(C_java_removed_virtual_call, #java_removed_virtual_call) #undef IREP_ID_ONE #undef IREP_ID_TWO diff --git a/src/util/source_location.h b/src/util/source_location.h index d09f8f2e36f..a4d90772f3a 100644 --- a/src/util/source_location.h +++ b/src/util/source_location.h @@ -151,6 +151,19 @@ class source_locationt:public irept return set(ID_basic_block_covered_lines, covered_lines); } + /// Add comment to source location as originating from removed virtual call + void set_java_removed_virtual_call() + { + set(ID_C_java_removed_virtual_call, true); + } + + /// Get information about whether call originated from a removed virtual + /// function call + bool get_java_removed_virtual_call() const + { + return get_bool(ID_C_java_removed_virtual_call); + } + void set_hide() { set(ID_hide, true); diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt index 166c1f8c894..7d42ac4fa98 100644 --- a/unit/CMakeLists.txt +++ b/unit/CMakeLists.txt @@ -36,7 +36,15 @@ 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 91dc62345cf..5f3a10fb63a 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -66,6 +66,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..002f0f11aa7 100644 --- a/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp +++ b/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp @@ -13,7 +13,8 @@ #include #include #include - +#include +#include #include void check_function_call( @@ -113,8 +114,54 @@ SCENARIO( } } } - REQUIRE(found_function); + + WHEN("basic blocks are instrumented") + { + optionst options; + options.set_option("cover", "location"); + THEN("instrumentation assertions are inserted") + { + REQUIRE_FALSE( + instrument_cover_goals( + options, new_table, new_goto_functions, null_output)); + } + THEN( + "instructions are marked as originating from virtual function call " + "removal") + { + 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; + auto it = std::find_if( + goto_program.instructions.begin(), + goto_program.instructions.end(), + [](const goto_programt::instructiont &instruction) { + return instruction.type == goto_program_instruction_typet::GOTO && + instruction.guard.id() == ID_equal; + }); + REQUIRE(it != goto_program.instructions.end()); + THEN( + "all instructions that share the same bytecode index " + "are marked as originating from a removed virtual function " + "call and there is no GOTO ASSERT") + { + const source_locationt &loc = it->source_location; + REQUIRE(loc != source_locationt::nil()); + REQUIRE(!loc.get_java_bytecode_index().empty()); + + while(it->source_location != source_locationt::nil() && + it->source_location.get_java_bytecode_index() == + loc.get_java_bytecode_index()) + { + REQUIRE(it->source_location.get_java_removed_virtual_call()); + REQUIRE(it->type != goto_program_instruction_typet::ASSERT); + ++it; + } + } + } + } } } }