From c14677b03af8c31dd623a691b87a4a07e7f4d25a Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Thu, 31 May 2018 17:40:53 +0100
Subject: [PATCH] Java frontend: don't advertise ignored methods

Some org.cprover.CProver methods are always ignored by java-bytecode-convert-method (they are
left with no body), but they are currently advertised to language_filest as available, making
it harder for a driver program to discern when it should introduce a stub. This change stops
advertising them, so they look more like other stub methods.
---
 .../java_bytecode_convert_method.cpp          | 25 +++----------------
 .../java_bytecode/java_bytecode_language.cpp  | 25 +++++++++++++++++++
 jbmc/src/java_bytecode/java_utils.cpp         | 22 ++++++++++++++++
 jbmc/src/java_bytecode/java_utils.h           |  4 +++
 4 files changed, 54 insertions(+), 22 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index d76a499eeb6..6669e0e05a2 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/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;
   }
 
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp
index a3130545edb..8269069b972 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.cpp
+++ b/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);
diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp
index 3a84813ba14..f822e5e3f03 100644
--- a/jbmc/src/java_bytecode/java_utils.cpp
+++ b/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"
+};
diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h
index d2ceb0442dd..1cc5c7727d4 100644
--- a/jbmc/src/java_bytecode/java_utils.h
+++ b/jbmc/src/java_bytecode/java_utils.h
@@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #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