From 4c724de4872d90b2e949633959038babedbfcd91 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Fri, 22 Feb 2019 15:51:48 +0000
Subject: [PATCH] Java frontend: ignore CProver methods earlier

We already tried to ignore org.cprover.CProver methods such as nondetInt, relying upon
the front-end to supply stub bodies if desired based on their type. However, by creating
symbols for them as for normal (non-stub) methods, but then refusing to provide a body or
advertise them as normal methods, we failed to set up their type properly (specifically
the parameter names), as they were neither set like a stub (upon symbol creation, upon
discovery by a caller) or like a normal method (during java_bytecode_convert_method). By
refusing to create the symbol at all, this treats the special CProver methods more like
normal stubs: their symbols are now created on demand.

It is also no longer necessary for java_bytecode_languaget::methods_provided to special
case them, as they are not added to method_bytecodet either, again matching "real" stub
methods more closely.
---
 jbmc/regression/jbmc/fake_stubs/Test.class    | Bin 0 -> 292 bytes
 jbmc/regression/jbmc/fake_stubs/Test.java     |   9 +++++++
 jbmc/regression/jbmc/fake_stubs/test.desc     |  11 ++++++++
 .../fake_stubs/uses_cprover_start_thread.desc |   9 +++++++
 .../java_bytecode_convert_class.cpp           |  25 +++++++++++-------
 .../java_bytecode_convert_method.cpp          |  24 ++++++++---------
 .../java_bytecode/java_bytecode_language.cpp  |  23 ----------------
 7 files changed, 57 insertions(+), 44 deletions(-)
 create mode 100644 jbmc/regression/jbmc/fake_stubs/Test.class
 create mode 100644 jbmc/regression/jbmc/fake_stubs/Test.java
 create mode 100644 jbmc/regression/jbmc/fake_stubs/test.desc
 create mode 100644 jbmc/regression/jbmc/fake_stubs/uses_cprover_start_thread.desc

diff --git a/jbmc/regression/jbmc/fake_stubs/Test.class b/jbmc/regression/jbmc/fake_stubs/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..53232913a6521276700cb30f21db1041c33fe935
GIT binary patch
literal 292
zcmYLD!A=4(6r8s#RLUv{UOjLF5AMaI@j_xkV${S9_wLeQ3GAA(@L!%Z9QXh~$}lA{
zw#l36%)Ci|e)k6ecev7sk!YObLZPeB6SVGK>FNhTV>F%#;z>2Pg6@+m?elh>Tc4SH
zMI~MvR|@o7we^L4bU|xpc2nOj&CVofqNQ+|ppOB=!4UL<m99*=NMG`$Ehr5tzetM@
zU+t_<C$A?IbT+l|b@uM9nR9zI9nUaCgP#p2f`ocb#n&}ah|QZX$R~;5j5FAQw|W1f
X!;{8n{Eg^8s@X`9?TP_S9-(stqW3Uq

literal 0
HcmV?d00001

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