From a9e2e519372dc07fb005394374bde09b619cb734 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 7 Feb 2018 17:40:27 +0100 Subject: [PATCH 1/5] Add ID_C_java_removed_virtual_call to irep defs --- src/util/irep_ids.def | 1 + 1 file changed, 1 insertion(+) 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 From 83481aa9b714fe1918fc5b64f8e3af1d12afd6ad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 7 Feb 2018 17:42:47 +0100 Subject: [PATCH 2/5] Add possibility to mark instructions to `source_locationt`` --- src/util/source_location.h | 13 +++++++++++++ 1 file changed, 13 insertions(+) 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); From e596be14a35c348268558baaaeeb4992bd9b6d5c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 7 Feb 2018 17:43:14 +0100 Subject: [PATCH 3/5] Mark instructions in `remove_virtual_functions` --- src/goto-programs/remove_virtual_functions.cpp | 2 ++ 1 file changed, 2 insertions(+) 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); From 012985f110be9dda9a9ad5c76c217cca080dfd18 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 7 Feb 2018 17:41:20 +0100 Subject: [PATCH 4/5] Skip instructions from virtual call removal from instrumentation This adds a goal_filter to the instrumentation that skips over instructions marked as originating from a removed virtual call. --- src/goto-instrument/cover_filter.cpp | 3 +++ 1 file changed, 3 insertions(+) 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; } From d0aea6e25f1c2074ec6a9434ab97ba8160613626 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Thu, 8 Feb 2018 13:16:58 +0100 Subject: [PATCH 5/5] Add unit test for non-instrumentation of Java virtual calls --- src/goto-instrument/Makefile | 7 ++- unit/CMakeLists.txt | 10 +++- unit/Makefile | 1 + .../virtual_functions.cpp | 51 ++++++++++++++++++- 4 files changed, 64 insertions(+), 5 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..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; + } + } + } + } } } }