diff --git a/regression/cbmc-java/lazyloading_no_candidates/Test$factory_intf.class b/regression/cbmc-java/lazyloading_no_candidates/Test$factory_intf.class new file mode 100644 index 00000000000..cd677924e04 Binary files /dev/null and b/regression/cbmc-java/lazyloading_no_candidates/Test$factory_intf.class differ diff --git a/regression/cbmc-java/lazyloading_no_candidates/Test$intf.class b/regression/cbmc-java/lazyloading_no_candidates/Test$intf.class new file mode 100644 index 00000000000..769b5398c84 Binary files /dev/null and b/regression/cbmc-java/lazyloading_no_candidates/Test$intf.class differ diff --git a/regression/cbmc-java/lazyloading_no_candidates/Test.class b/regression/cbmc-java/lazyloading_no_candidates/Test.class new file mode 100644 index 00000000000..65600fab4b9 Binary files /dev/null and b/regression/cbmc-java/lazyloading_no_candidates/Test.class differ diff --git a/regression/cbmc-java/lazyloading_no_candidates/Test.java b/regression/cbmc-java/lazyloading_no_candidates/Test.java new file mode 100644 index 00000000000..856ccbad136 --- /dev/null +++ b/regression/cbmc-java/lazyloading_no_candidates/Test.java @@ -0,0 +1,12 @@ +public class Test { + + interface factory_intf { + public intf getintf(); + } + + interface intf { + public void f(); + } + + public static void main(factory_intf i) { i.getintf().f(); } +} diff --git a/regression/cbmc-java/lazyloading_no_candidates/test.desc b/regression/cbmc-java/lazyloading_no_candidates/test.desc new file mode 100644 index 00000000000..a7920b53795 --- /dev/null +++ b/regression/cbmc-java/lazyloading_no_candidates/test.desc @@ -0,0 +1,10 @@ +CORE symex-driven-lazy-loading-expected-failure +Test.class +--lazy-methods --show-goto-functions --verbosity 10 --function Test.main +^EXIT=0$ +^SIGNAL=0$ +^CI lazy methods: elaborate java::Test\$intf\.f:\(\)V$ +Test\$intf\.f:\(\)V\(\);$ +-- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp index 6d34d869e8e..ccb892a296c 100644 --- a/src/java_bytecode/ci_lazy_methods.cpp +++ b/src/java_bytecode/ci_lazy_methods.cpp @@ -72,8 +72,7 @@ bool ci_lazy_methodst::operator()( method_bytecodet &method_bytecode, const method_convertert &method_converter) { - std::vector method_worklist1; - std::vector method_worklist2; + std::unordered_set methods_to_convert_later; main_function_resultt main_function = get_main_symbol(symbol_table, main_class, get_message_handler()); @@ -95,51 +94,46 @@ bool ci_lazy_methodst::operator()( const irep_idt methodid = "java::" + id2string(class_name) + "." + id2string(method.name) + ":" + id2string(method.descriptor); - method_worklist2.push_back(methodid); + methods_to_convert_later.insert(methodid); } } } else - method_worklist2.push_back(main_function.main_function.name); + methods_to_convert_later.insert(main_function.main_function.name); // Add any extra entry points specified; we should elaborate these in the // same way as the main function. std::vector extra_entry_points=lazy_methods_extra_entry_points; resolve_method_names(extra_entry_points, symbol_table); - method_worklist2.insert( - method_worklist2.begin(), - extra_entry_points.begin(), - extra_entry_points.end()); + methods_to_convert_later.insert( + extra_entry_points.begin(), extra_entry_points.end()); - std::set instantiated_classes; + std::unordered_set instantiated_classes; { - std::vector initial_callable_methods; + std::unordered_set initial_callable_methods; ci_lazy_methods_neededt initial_lazy_methods( - initial_callable_methods, - instantiated_classes, - symbol_table); + initial_callable_methods, instantiated_classes, symbol_table); initialize_instantiated_classes( - method_worklist2, - namespacet(symbol_table), - initial_lazy_methods); - method_worklist2.insert( - method_worklist2.end(), - initial_callable_methods.begin(), - initial_callable_methods.end()); + methods_to_convert_later, namespacet(symbol_table), initial_lazy_methods); + methods_to_convert_later.insert( + initial_callable_methods.begin(), initial_callable_methods.end()); } - std::set methods_already_populated; - std::vector virtual_callsites; + std::unordered_set methods_already_populated; + std::unordered_set virtual_function_calls; - bool any_new_methods=false; - do + bool any_new_classes = true; + while(any_new_classes) + {bool any_new_methods = true; + while(any_new_methods) { any_new_methods=false; - while(!method_worklist2.empty()) + while(!methods_to_convert_later.empty()) { - std::swap(method_worklist1, method_worklist2); - for(const auto &mname : method_worklist1) + std::unordered_set methods_to_convert; + std::swap(methods_to_convert, methods_to_convert_later); + for(const auto &mname : methods_to_convert) { if(!methods_already_populated.insert(mname).second) continue; @@ -147,42 +141,74 @@ bool ci_lazy_methodst::operator()( if( method_converter( mname, - // Note this wraps *references* to method_worklist2 & + // Note this wraps *references* to methods_to_convert_later & // instantiated_classes ci_lazy_methods_neededt( - method_worklist2, instantiated_classes, symbol_table))) + methods_to_convert_later, instantiated_classes, symbol_table))) { // Couldn't convert this function continue; } gather_virtual_callsites( - symbol_table.lookup_ref(mname).value, - virtual_callsites); + symbol_table.lookup_ref(mname).value, virtual_function_calls); any_new_methods=true; } - method_worklist1.clear(); } - // Given the object types we now know may be created, populate more - // possible virtual function call targets: + // Given the object types we now know may be created, populate more + // possible virtual function call targets: - debug() << "CI lazy methods: add virtual method targets (" - << virtual_callsites.size() - << " callsites)" - << eom; + debug() << "CI lazy methods: add virtual method targets (" + << virtual_function_calls.size() << " callsites)" << eom; - std::unordered_set unique_functions; - for(const code_function_callt *virtual_callsite : virtual_callsites) - unique_functions.insert(virtual_callsite->function()); + for(const exprt &function : virtual_function_calls) + { + get_virtual_method_targets( + function, + instantiated_classes, + methods_to_convert_later, + symbol_table); + } + } + + any_new_classes = false; - for(const exprt &function : unique_functions) + // Look for virtual callsites with no candidate targets. If we have + // invokevirtual A.f and we don't believe either A or any of its children + // may exist, we assume specifically A is somehow instantiated. Note this + // may result in an abstract class being classified as instantiated, which + // stands in for some unknown concrete subclass: in this case the called + // method will be a stub. + for(const exprt &virtual_function_call : virtual_function_calls) { - // This will also create a stub if a virtual callsite has no targets. + std::unordered_set candidate_target_methods; get_virtual_method_targets( - function, instantiated_classes, method_worklist2, symbol_table); + virtual_function_call, + instantiated_classes, + candidate_target_methods, + symbol_table); + + if(!candidate_target_methods.empty()) + continue; + + // Add the call class to instantiated_classes and assert that it + // didn't already exist + const irep_idt &call_class = virtual_function_call.get(ID_C_class); + auto ret_class = instantiated_classes.insert(call_class); + CHECK_RETURN(ret_class.second); + any_new_classes = true; + + // Check that `get_virtual_method_target` returns a method now + const irep_idt &call_basename = + virtual_function_call.get(ID_component_name); + const irep_idt method_name = get_virtual_method_target( + instantiated_classes, call_basename, call_class, symbol_table); + CHECK_RETURN(!method_name.empty()); + + // Add what it returns to methods_to_convert_later + methods_to_convert_later.insert(method_name); } } - while(any_new_methods); // Remove symbols for methods that were declared but never used: symbol_tablet keep_symbols; @@ -279,7 +305,7 @@ void ci_lazy_methodst::resolve_method_names( /// whose references may be passed, directly or indirectly, to any of the /// functions in `entry_points`. void ci_lazy_methodst::initialize_instantiated_classes( - const std::vector &entry_points, + const std::unordered_set &entry_points, const namespacet &ns, ci_lazy_methods_neededt &needed_lazy_methods) { @@ -386,7 +412,7 @@ void ci_lazy_methodst::initialize_instantiated_classes_from_pointer( /// e that calls a virtual function. void ci_lazy_methodst::gather_virtual_callsites( const exprt &e, - std::vector &result) + std::unordered_set &result) { if(e.id()!=ID_code) return; @@ -394,7 +420,7 @@ void ci_lazy_methodst::gather_virtual_callsites( if(c.get_statement()==ID_function_call && to_code_function_call(c).function().id()==ID_virtual_function) { - result.push_back(&to_code_function_call(c)); + result.insert(to_code_function_call(c).function()); } else { @@ -409,14 +435,14 @@ void ci_lazy_methodst::gather_virtual_callsites( /// should be determined. /// \param instantiated_classes: set of classes that can be instantiated. Any /// potential callee not in this set will be ignored. -/// \param symbol_table: global symbol table /// \param [out] callable_methods: Populated with all possible `c` callees, /// taking `instantiated_classes` into account (virtual function overrides /// defined on classes that are not 'needed' are ignored) +/// \param symbol_table: global symbol table void ci_lazy_methodst::get_virtual_method_targets( const exprt &called_function, - const std::set &instantiated_classes, - std::vector &callable_methods, + const std::unordered_set &instantiated_classes, + std::unordered_set &callable_methods, symbol_tablet &symbol_table) { PRECONDITION(called_function.id()==ID_virtual_function); @@ -429,26 +455,16 @@ void ci_lazy_methodst::get_virtual_method_targets( !call_basename.empty(), "Virtual function must have a reasonable name after removing class"); - const irep_idt &self_method= - get_virtual_method_target( - instantiated_classes, call_basename, call_class, symbol_table); - - if(!self_method.empty()) - { - callable_methods.push_back(self_method); - } + class_hierarchyt::idst self_and_child_classes = + class_hierarchy.get_children_trans(call_class); + self_and_child_classes.push_back(call_class); - const auto child_classes=class_hierarchy.get_children_trans(call_class); - for(const auto &child_class : child_classes) + for(const irep_idt &class_name : self_and_child_classes) { - const auto child_method= - get_virtual_method_target( - instantiated_classes, - call_basename, - child_class, - symbol_table); - if(!child_method.empty()) - callable_methods.push_back(child_method); + const irep_idt method_name = get_virtual_method_target( + instantiated_classes, call_basename, class_name, symbol_table); + if(!method_name.empty()) + callable_methods.insert(method_name); } } @@ -554,7 +570,7 @@ void ci_lazy_methodst::gather_field_types( /// `call_basename` if found and `classname` is present in /// `instantiated_classes`, or irep_idt() otherwise. irep_idt ci_lazy_methodst::get_virtual_method_target( - const std::set &instantiated_classes, + const std::unordered_set &instantiated_classes, const irep_idt &call_basename, const irep_idt &classname, const symbol_tablet &symbol_table) diff --git a/src/java_bytecode/ci_lazy_methods.h b/src/java_bytecode/ci_lazy_methods.h index f78414c44be..11095fa3d8a 100644 --- a/src/java_bytecode/ci_lazy_methods.h +++ b/src/java_bytecode/ci_lazy_methods.h @@ -115,7 +115,7 @@ class ci_lazy_methodst:public messaget const symbol_tablet &symbol_table); void initialize_instantiated_classes( - const std::vector &entry_points, + const std::unordered_set &entry_points, const namespacet &ns, ci_lazy_methods_neededt &needed_lazy_methods); @@ -131,12 +131,12 @@ class ci_lazy_methodst:public messaget void gather_virtual_callsites( const exprt &e, - std::vector &result); + std::unordered_set &result); void get_virtual_method_targets( const exprt &called_function, - const std::set &instantiated_classes, - std::vector &callable_methods, + const std::unordered_set &instantiated_classes, + std::unordered_set &callable_methods, symbol_tablet &symbol_table); void gather_needed_globals( @@ -150,7 +150,7 @@ class ci_lazy_methodst:public messaget ci_lazy_methods_neededt &needed_lazy_methods); irep_idt get_virtual_method_target( - const std::set &instantiated_classes, + const std::unordered_set &instantiated_classes, const irep_idt &call_basename, const irep_idt &classname, const symbol_tablet &symbol_table); diff --git a/src/java_bytecode/ci_lazy_methods_needed.cpp b/src/java_bytecode/ci_lazy_methods_needed.cpp index eda4ae3f835..e3b10b0ebbf 100644 --- a/src/java_bytecode/ci_lazy_methods_needed.cpp +++ b/src/java_bytecode/ci_lazy_methods_needed.cpp @@ -20,7 +20,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com void ci_lazy_methods_neededt::add_needed_method( const irep_idt &method_symbol_name) { - callable_methods.push_back(method_symbol_name); + callable_methods.insert(method_symbol_name); } /// Notes class `class_symbol_name` will be instantiated, or a static field diff --git a/src/java_bytecode/ci_lazy_methods_needed.h b/src/java_bytecode/ci_lazy_methods_needed.h index dcc6a222000..ecb95c0d129 100644 --- a/src/java_bytecode/ci_lazy_methods_needed.h +++ b/src/java_bytecode/ci_lazy_methods_needed.h @@ -14,18 +14,19 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include +#include #include class ci_lazy_methods_neededt { public: ci_lazy_methods_neededt( - std::vector &_callable_methods, - std::set &_instantiated_classes, - symbol_tablet &_symbol_table): - callable_methods(_callable_methods), - instantiated_classes(_instantiated_classes), - symbol_table(_symbol_table) + std::unordered_set &_callable_methods, + std::unordered_set &_instantiated_classes, + symbol_tablet &_symbol_table) + : callable_methods(_callable_methods), + instantiated_classes(_instantiated_classes), + symbol_table(_symbol_table) {} void add_needed_method(const irep_idt &); @@ -38,11 +39,11 @@ class ci_lazy_methods_neededt // contain all methods that have previously been elaborated. // It should be changed to a set if we develop the need to use // it that way. - std::vector &callable_methods; + std::unordered_set &callable_methods; // instantiated_classes on the other hand is a true set of every class // found so far, so we can use a membership test to avoid // repeatedly exploring a class hierarchy. - std::set &instantiated_classes; + std::unordered_set &instantiated_classes; symbol_tablet &symbol_table; };