From 841313daee0221ad3f51f5396da33979c09f032d Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Mon, 2 Jul 2018 16:28:14 +0100 Subject: [PATCH 1/2] Add ability to mark methods as ignored (not loaded) --- .../java_bytecode_convert_class.cpp | 21 ++++++++++++------- .../java_bytecode/java_bytecode_parse_tree.h | 5 +++++ src/util/irep_ids.def | 1 + 3 files changed, 19 insertions(+), 8 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 9f3ff3d7744..869038381d3 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -118,7 +118,15 @@ class java_bytecode_convert_classt:public messaget // see definition below for more info static void add_array_types(symbol_tablet &symbol_table); - static bool is_overlay_method(const methodt &method); + static bool is_overlay_method(const methodt &method) + { + return method.has_annotation(ID_overlay_method); + } + + static bool is_ignored_method(const methodt &method) + { + return method.has_annotation(ID_ignored_method); + } bool check_field_exists( const fieldt &field, @@ -455,6 +463,8 @@ void java_bytecode_convert_classt::convert( { for(const methodt &method : overlay_class.get().methods) { + if(is_ignored_method(method)) + continue; const irep_idt method_identifier = qualified_classname + "." + id2string(method.name) + ":" + method.descriptor; @@ -496,6 +506,8 @@ void java_bytecode_convert_classt::convert( } for(const methodt &method : c.methods) { + if(is_ignored_method(method)) + continue; const irep_idt method_identifier= qualified_classname + "." + id2string(method.name) + ":" + method.descriptor; @@ -877,13 +889,6 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) } } -bool java_bytecode_convert_classt::is_overlay_method(const methodt &method) -{ - return java_bytecode_parse_treet::find_annotation( - method.annotations, ID_overlay_method) - .has_value(); -} - bool java_bytecode_convert_class( const java_class_loadert::parse_tree_with_overlayst &parse_trees, symbol_tablet &symbol_table, diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index c5762137152..d3709b11826 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -84,6 +84,11 @@ class java_bytecode_parse_treet is_private(false), is_static(false), is_final(false) { } + + bool has_annotation(const irep_idt &annotation_id) const + { + return find_annotation(annotations, annotation_id).has_value(); + } }; class methodt:public membert diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 05e84f1d9f2..fa888b75474 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -664,6 +664,7 @@ IREP_ID_TWO(overflow_shl, overflow-shl) IREP_ID_TWO(C_no_initialization_required, #no_initialization_required) IREP_ID_TWO(overlay_class, java::com.diffblue.OverlayClassImplementation) IREP_ID_TWO(overlay_method, java::com.diffblue.OverlayMethodImplementation) +IREP_ID_TWO(ignored_method, java::com.diffblue.IgnoredMethodImplementation) IREP_ID_ONE(is_annotation) IREP_ID_TWO(C_annotations, #annotations) IREP_ID_ONE(final) From 4a12a29d94cc20f91e87b6ad04574aabe20b8baa Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Tue, 3 Jul 2018 13:15:35 +0100 Subject: [PATCH 2/2] Prevent crash when only instance of class is marked as an overlay --- jbmc/src/java_bytecode/java_class_loader.cpp | 70 ++++++++++---------- 1 file changed, 34 insertions(+), 36 deletions(-) diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index cfe64958a2d..048d41cc5fb 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -168,50 +168,48 @@ java_class_loadert::get_parse_tree( } } - if(!parse_trees.empty()) + auto parse_tree_it = parse_trees.begin(); + // If the first class implementation is an overlay emit a warning and + // skip over it until we find a non-overlay class + while(parse_tree_it != parse_trees.end()) { - auto parse_tree_it = parse_trees.begin(); - // If the first class implementation is an overlay emit a warning and - // skip over it until we find a non-overlay class - while(parse_tree_it != parse_trees.end()) - { - // Skip parse trees that failed to load - though these shouldn't exist yet - if(parse_tree_it->loading_successful) - { - if(!is_overlay_class(parse_tree_it->parsed_class)) - { - // Keep the non-overlay class - ++parse_tree_it; - break; - } - warning() - << "Skipping class " << class_name - << " marked with OverlayClassImplementation but found before" - " original definition" - << eom; - } - auto unloaded_or_overlay_out_of_order_it = parse_tree_it; - ++parse_tree_it; - parse_trees.erase(unloaded_or_overlay_out_of_order_it); - } - // Collect overlay classes - while(parse_tree_it != parse_trees.end()) + // Skip parse trees that failed to load - though these shouldn't exist yet + if(parse_tree_it->loading_successful) { - // Remove non-initial classes that aren't overlays if(!is_overlay_class(parse_tree_it->parsed_class)) { - warning() - << "Skipping duplicate definition of class " << class_name - << " not marked with OverlayClassImplementation" << eom; - auto duplicate_non_overlay_it = parse_tree_it; + // Keep the non-overlay class ++parse_tree_it; - parse_trees.erase(duplicate_non_overlay_it); + break; } - else - ++parse_tree_it; + warning() + << "Skipping class " << class_name + << " marked with OverlayClassImplementation but found before" + " original definition" + << eom; } - return parse_trees; + auto unloaded_or_overlay_out_of_order_it = parse_tree_it; + ++parse_tree_it; + parse_trees.erase(unloaded_or_overlay_out_of_order_it); } + // Collect overlay classes + while(parse_tree_it != parse_trees.end()) + { + // Remove non-initial classes that aren't overlays + if(!is_overlay_class(parse_tree_it->parsed_class)) + { + warning() + << "Skipping duplicate definition of class " << class_name + << " not marked with OverlayClassImplementation" << eom; + auto duplicate_non_overlay_it = parse_tree_it; + ++parse_tree_it; + parse_trees.erase(duplicate_non_overlay_it); + } + else + ++parse_tree_it; + } + if(!parse_trees.empty()) + return parse_trees; // Not found or failed to load warning() << "failed to load class `" << class_name << '\'' << eom;