extend java_bytecode for test-gen-support

Author: Matthias Güdemann

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -54,6 +54,56 @@ class patternt
   const char *p;
 };
 
+/*******************************************************************\
+
+Function: assign_parameter_names
+
+  Inputs: `ftype`: Function type whose parameters should be named
+          `name_prefix`: Prefix for parameter names, typically the
+            parent function's name.
+          `symbol_table`: Global symbol table
+
+ Outputs: Assigns parameter names (side-effects on `ftype`) to
+          function stub parameters, which are initially nameless
+          as method conversion hasn't happened.
+          Also creates symbols in `symbol_table`.
+
+ Purpose: See above
+
+\*******************************************************************/
+
+void assign_parameter_names(
+  code_typet &ftype,
+  const irep_idt &name_prefix,
+  symbol_tablet &symbol_table)
+{
+  code_typet::parameterst &parameters=ftype.parameters();
+
+  // Mostly borrowed from java_bytecode_convert.cpp; maybe factor this out.
+  // assign names to parameters
+  for(std::size_t i=0; i<parameters.size(); ++i)
+  {
+    irep_idt base_name, identifier;
+
+    if(i==0 && parameters[i].get_this())
+      base_name="this";
+    else
+      base_name="stub_ignored_arg"+std::to_string(i);
+
+    identifier=id2string(name_prefix)+"::"+id2string(base_name);
+    parameters[i].set_base_name(base_name);
+    parameters[i].set_identifier(identifier);
+
+    // add to symbol table
+    parameter_symbolt parameter_symbol;
+    parameter_symbol.base_name=base_name;
+    parameter_symbol.mode=ID_java;
+    parameter_symbol.name=identifier;
+    parameter_symbol.type=parameters[i].type();
+    symbol_table.add(parameter_symbol);
+  }
+}
+
 static bool operator==(const irep_idt &what, const patternt &pattern)
 {
   return pattern==what;
@@ -1216,9 +1266,18 @@ codet java_bytecode_convert_methodt::convert_instructions(
         symbolt symbol;
         symbol.name=id;
         symbol.base_name=arg0.get(ID_C_base_name);
+        symbol.pretty_name=
+          id2string(arg0.get(ID_C_class)).substr(6)+"."+
+          id2string(symbol.base_name)+"()";
         symbol.type=arg0.type();
         symbol.value.make_nil();
         symbol.mode=ID_java;
+
+        assign_parameter_names(
+          to_code_type(symbol.type),
+          symbol.name,
+          symbol_table);
+
         symbol_table.add(symbol);
       }
 

src/java_bytecode/java_bytecode_language.cpp

@@ -751,7 +751,6 @@ bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
   */
   java_internal_additions(symbol_table);
 
-
   main_function_resultt res=
     get_main_symbol(symbol_table, main_class, get_message_handler());
   if(res.stop_convert)

src/java_bytecode/java_bytecode_language.h

@@ -48,7 +48,7 @@ class java_bytecode_languaget:public languaget
     symbol_tablet &context,
     const std::string &module) override;
 
-  bool final(
+  virtual bool final(
     symbol_tablet &context) override;
 
   void show_parse(std::ostream &out) override;

src/java_bytecode/java_entry_point.cpp

@@ -289,7 +289,8 @@ void java_record_outputs(
     codet output(ID_output);
     output.operands().resize(2);
 
-    const symbolt &return_symbol=symbol_table.lookup("return'");
+    const symbolt &return_symbol=
+      symbol_table.lookup(JAVA_ENTRY_POINT_RETURN_SYMBOL);
 
     output.op0()=
       address_of_exprt(
@@ -583,7 +584,7 @@ bool java_entry_point(
     auxiliary_symbolt return_symbol;
     return_symbol.mode=ID_C;
     return_symbol.is_static_lifetime=false;
-    return_symbol.name="return'";
+    return_symbol.name=JAVA_ENTRY_POINT_RETURN_SYMBOL;
     return_symbol.base_name="return";
     return_symbol.type=to_code_type(symbol.type).return_type();
 

src/java_bytecode/java_entry_point.h

@@ -33,4 +33,4 @@ main_function_resultt get_main_symbol(
   message_handlert &,
   bool allow_no_body=false);
 
-#endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H
+#endif