Merge pull request #4258 from smowton/smowton/fix/java-fake-stubs-parameter-identifiers

Java frontend: treat CProver stubbed methods more like normal stubs

Author: smowton

jbmc/regression/jbmc/fake_stubs/Test.class

@@ -0,0 +1,9 @@
+public class Test {
+
+  public static void main() {
+
+    org.cprover.CProver.startThread(1);
+
+  }
+
+}

jbmc/regression/jbmc/fake_stubs/Test.java

@@ -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)

jbmc/regression/jbmc/fake_stubs/test.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)

jbmc/regression/jbmc/fake_stubs/uses_cprover_start_thread.desc

@@ -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 << "'"

jbmc/src/java_bytecode/java_bytecode_convert_class.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,

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -933,30 +933,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);