Java frontend: set parameter identifiers for forcibly-stubbed methods

org.cprover.CProver methods are sometimes deliberately ignored in order to invite the
front-end program to produce stub bodies. This means the symbols are discovered through
normal class loading, not through usage (how stub methods usually get their parameter
identifiers), but they are not subject to the usual java_bytecode_convert_method routine
(which sets the parameter identifiers for normal methods). This commit handles this in-
between special case and adds a test checking these methods are usable without crashing,
typically in goto-symex which requires these identifiers to be set.

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 to CProver.startThread, which are special-cased by the Java front-end (which omits the method's body
+in hope of the front-end handling it like a stub), but which don't get their 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

@@ -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
@@ -3084,6 +3094,17 @@ void java_bytecode_convert_method(
   {
     // Ignore these methods; fall back to the driver program's
     // stubbing behaviour.
+
+    // Assign parameter names -- this would normally be done either by the
+    // normal method conversion routine or upon discovering the stub method,
+    // but this fake stubbing awkwardly falls between the two ways.
+    const irep_idt method_id = get_method_identifier(class_symbol.name, method);
+    symbolt &method_symbol = symbol_table.get_writeable_ref(method_id);
+    assign_parameter_names(
+      to_java_method_type(method_symbol.type),
+      method_symbol.name,
+      symbol_table);
+
     return;
   }