diff --git a/jbmc/regression/jbmc/fake_stubs/Test.class b/jbmc/regression/jbmc/fake_stubs/Test.class new file mode 100644 index 00000000000..53232913a65 Binary files /dev/null and b/jbmc/regression/jbmc/fake_stubs/Test.class differ diff --git a/jbmc/regression/jbmc/fake_stubs/Test.java b/jbmc/regression/jbmc/fake_stubs/Test.java new file mode 100644 index 00000000000..fe33e22d1cc --- /dev/null +++ b/jbmc/regression/jbmc/fake_stubs/Test.java @@ -0,0 +1,9 @@ +public class Test { + + public static void main() { + + org.cprover.CProver.startThread(1); + + } + +} diff --git a/jbmc/regression/jbmc/fake_stubs/test.desc b/jbmc/regression/jbmc/fake_stubs/test.desc new file mode 100644 index 00000000000..3067de23d3c --- /dev/null +++ b/jbmc/regression/jbmc/fake_stubs/test.desc @@ -0,0 +1,11 @@ +CORE +Test.class +--function Test.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This calls CProver.startThread, which is special-cased by the Java front-end (which omits the method's body +in hope of the front-end handling it like a stub), and doesn't get its parameter names assigned by the usual +mechanism (setting the names when the stub is discovered for the first time) diff --git a/jbmc/regression/jbmc/fake_stubs/uses_cprover_start_thread.desc b/jbmc/regression/jbmc/fake_stubs/uses_cprover_start_thread.desc new file mode 100644 index 00000000000..1eb8433d048 --- /dev/null +++ b/jbmc/regression/jbmc/fake_stubs/uses_cprover_start_thread.desc @@ -0,0 +1,9 @@ +CORE +Test.class +--function Test.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions +org\.cprover\.CProver\.startThread:\(I\)V +^EXIT=0$ +^SIGNAL=0$ +-- +-- +Companion to the main test.desc that checks the function under test uses org.cprover.CProver.startThread(int) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 1c1751e9a01..3241a20fbb7 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -138,12 +138,13 @@ class java_bytecode_convert_classt:public messaget return method.has_annotation(ID_overlay_method); } - /// Check if a method is an ignored method by searching for - /// `ID_ignored_method` in its list of annotations. + /// Check if a method is an ignored method, by one of two mechanisms: /// - /// An ignored method is a method with the annotation - /// \@IgnoredMethodImplementation. They will be ignored by JBMC. They are - /// intended for use in + /// 1. If the class under consideration is org.cprover.CProver, and the method + /// is listed as ignored. + /// + /// 2. If it has the annotation\@IgnoredMethodImplementation. + /// This kind of ignord method is intended for use in /// [overlay classes](\ref java_class_loader.cpp::is_overlay_class), in /// particular for methods which must exist in the overlay class so that /// it will compile, e.g. default constructors, but which we do not want @@ -154,11 +155,17 @@ class java_bytecode_convert_classt:public messaget /// [overlay method](\ref java_bytecode_convert_classt::is_overlay_method) /// or an ignored method. /// + /// \param class_name: class the method is declared on /// \param method: a `methodt` object from a java bytecode parse tree /// \return true if the method is an ignored method, else false - static bool is_ignored_method(const methodt &method) + static bool is_ignored_method( + const irep_idt &class_name, const methodt &method) { - return method.has_annotation(ID_ignored_method); + static irep_idt org_cprover_CProver_name = "org.cprover.CProver"; + return + (class_name == org_cprover_CProver_name && + cprover_methods_to_ignore.count(id2string(method.name)) != 0) || + method.has_annotation(ID_ignored_method); } bool check_field_exists( @@ -504,7 +511,7 @@ void java_bytecode_convert_classt::convert( const irep_idt method_identifier = qualified_classname + "." + id2string(method.name) + ":" + method.descriptor; - if(is_ignored_method(method)) + if(is_ignored_method(c.name, method)) { debug() << "Ignoring method: '" << method_identifier << "'" @@ -552,7 +559,7 @@ void java_bytecode_convert_classt::convert( const irep_idt method_identifier= qualified_classname + "." + id2string(method.name) + ":" + method.descriptor; - if(is_ignored_method(method)) + if(is_ignored_method(c.name, method)) { debug() << "Ignoring method: '" << method_identifier << "'" diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index dd1f4d131f2..bcbc97e4ae7 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -398,6 +398,15 @@ void java_bytecode_convert_method_lazy( symbol_table.add(method_symbol); } +static irep_idt get_method_identifier( + const irep_idt &class_identifier, + const java_bytecode_parse_treet::methodt &method) +{ + return + id2string(class_identifier) + "." + id2string(method.name) + ":" + + method.descriptor; +} + void java_bytecode_convert_methodt::convert( const symbolt &class_symbol, const methodt &m) @@ -406,8 +415,9 @@ void java_bytecode_convert_methodt::convert( // (e.g. "my.package.ClassName.myMethodName:(II)I") and query the symbol table // to retrieve the symbol (constructed by java_bytecode_convert_method_lazy) // associated to the method - const irep_idt method_identifier= - id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.descriptor; + const irep_idt method_identifier = + get_method_identifier(class_symbol.name, m); + method_id=method_identifier; // Obtain a std::vector of java_method_typet::parametert objects from the @@ -3077,16 +3087,6 @@ void java_bytecode_convert_method( bool threading_support) { - if(std::regex_match( - id2string(class_symbol.name), - std::regex(".*org\\.cprover\\.CProver.*")) && - cprover_methods_to_ignore.count(id2string(method.name))) - { - // Ignore these methods; fall back to the driver program's - // stubbing behaviour. - return; - } - java_bytecode_convert_methodt java_bytecode_convert_method( symbol_table, message_handler, diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 5bb0f861d5d..d47a59a51bd 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -924,30 +924,7 @@ void java_bytecode_languaget::methods_provided( string_preprocess.get_all_function_names(methods); // Add all concrete methods to map for(const auto &kv : method_bytecode) - { - const std::string &method_id = id2string(kv.first); - - // Avoid advertising org.cprover.CProver methods that the Java frontend will - // never provide bodies for (java_bytecode_convert_method always leaves them - // bodyless with intent for the driver program to stub them): - if(has_prefix(method_id, cprover_class_prefix)) - { - std::size_t method_name_end_offset = - method_id.find(':', cprover_class_prefix.length()); - INVARIANT( - method_name_end_offset != std::string::npos, - "org.cprover.CProver method should have a postfix type descriptor"); - - const std::string method_name = - method_id.substr( - cprover_class_prefix.length(), - method_name_end_offset - cprover_class_prefix.length()); - - if(cprover_methods_to_ignore.count(method_name)) - continue; - } methods.insert(kv.first); - } // Add all synthetic methods to map for(const auto &kv : synthetic_methods) methods.insert(kv.first);