Merge pull request #2265 from smowton/smowton/fix/dont-advertise-ignored-methods

Java frontend: don't advertise ignored methods

Author: smowton

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2824,32 +2824,13 @@ void java_bytecode_convert_method(
   java_string_library_preprocesst &string_preprocess,
   const class_hierarchyt &class_hierarchy)
 {
-  static const std::unordered_set<std::string> methods_to_ignore
-  {
-    "nondetBoolean",
-    "nondetByte",
-    "nondetChar",
-    "nondetShort",
-    "nondetInt",
-    "nondetLong",
-    "nondetFloat",
-    "nondetDouble",
-    "nondetWithNull",
-    "nondetWithoutNull",
-    "notModelled",
-    "atomicBegin",
-    "atomicEnd",
-    "startThread",
-    "endThread",
-    "getCurrentThreadID"
-  };
-
   if(std::regex_match(
        id2string(class_symbol.name),
        std::regex(".*org\\.cprover\\.CProver.*")) &&
-     methods_to_ignore.find(id2string(method.name))!=methods_to_ignore.end())
+     cprover_methods_to_ignore.count(id2string(method.name)))
   {
-    // Ignore these methods, rely on default stubbing behaviour.
+    // Ignore these methods; fall back to the driver program's
+    // stubbing behaviour.
     return;
   }
 

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -843,11 +843,36 @@ const select_pointer_typet &
 void java_bytecode_languaget::methods_provided(
   std::unordered_set<irep_idt> &methods) const
 {
+  static std::string cprover_class_prefix = "java::org.cprover.CProver.";
+
   // Add all string solver methods to map
   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);

jbmc/src/java_bytecode/java_utils.cpp

@@ -426,3 +426,25 @@ bool is_non_null_library_global(const irep_idt &symbolid)
     "java::java.lang.System.in"};
   return non_null_globals.count(symbolid);
 }
+
+/// Methods belonging to the class org.cprover.CProver that should be ignored
+/// (not converted), leaving the driver program to stub them if it wishes.
+const std::unordered_set<std::string> cprover_methods_to_ignore
+{
+  "nondetBoolean",
+  "nondetByte",
+  "nondetChar",
+  "nondetShort",
+  "nondetInt",
+  "nondetLong",
+  "nondetFloat",
+  "nondetDouble",
+  "nondetWithNull",
+  "nondetWithoutNull",
+  "notModelled",
+  "atomicBegin",
+  "atomicEnd",
+  "startThread",
+  "endThread",
+  "getCurrentThreadID"
+};

jbmc/src/java_bytecode/java_utils.h

@@ -9,6 +9,8 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
 #define CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
 
+#include <unordered_set>
+
 #include <util/message.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
@@ -108,4 +110,6 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component(
 
 bool is_non_null_library_global(const irep_idt &);
 
+extern const std::unordered_set<std::string> cprover_methods_to_ignore;
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H