Initialise string solver function parameter names

Get the names of the parameters for string solver functions from bytecode if we have the bytecode for them

Author: NathanJPhillips

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2844,6 +2844,96 @@ codet java_bytecode_convert_methodt::convert_instructions(
   return code;
 }
 
+/// This uses a cut-down version of the logic in
+/// java_bytecode_convert_methodt::convert to initialize symbols for the
+/// parameters and update the parameters in the type of method_symbol with
+/// names read from the local_variable_table read from the bytecode
+/// \remarks This is useful for pre-initialization for methods generated by
+/// the string solver
+/// \param method_symbol: The symbol for the method for which to initialize the
+///   parameters
+/// \param local_variable_table: The local variable table containing the
+///   bytecode for the parameters
+/// \param symbol_table: The symbol table into which to insert symbols for the
+///   parameters
+void java_bytecode_initialize_parameter_names(
+  symbolt &method_symbol,
+  const java_bytecode_parse_treet::methodt::local_variable_tablet
+    &local_variable_table,
+  symbol_table_baset &symbol_table)
+{
+  // Obtain a std::vector of code_typet::parametert objects from the
+  // (function) type of the symbol
+  code_typet &code_type = to_code_type(method_symbol.type);
+  code_typet::parameterst &parameters = code_type.parameters();
+
+  // Find number of parameters
+  unsigned slots_for_parameters = java_method_parameter_slots(code_type);
+
+  // Find parameter names in the local variable table:
+  typedef std::pair<irep_idt, irep_idt> base_name_and_identifiert;
+  std::map<std::size_t, base_name_and_identifiert> param_names;
+  for(const auto &v : local_variable_table)
+  {
+    if(v.index < slots_for_parameters)
+      param_names.emplace(
+        v.index,
+        make_pair(
+          v.name, id2string(method_symbol.name) + "::" + id2string(v.name)));
+  }
+
+  // Assign names to parameters
+  std::size_t param_index = 0;
+  for(auto &param : parameters)
+  {
+    irep_idt base_name, identifier;
+
+    // Construct a sensible base name (base_name) and a fully qualified name
+    // (identifier) for every parameter of the method under translation,
+    // regardless of whether we have an LVT or not; and assign it to the
+    // parameter object (which is stored in the type of the symbol, not in the
+    // symbol table)
+    if(param_index == 0 && param.get_this())
+    {
+      // my.package.ClassName.myMethodName:(II)I::this
+      base_name = "this";
+      identifier = id2string(method_symbol.name) + "::" + id2string(base_name);
+    }
+    else
+    {
+      auto param_name = param_names.find(param_index);
+      if(param_name != param_names.end())
+      {
+        base_name = param_name->second.first;
+        identifier = param_name->second.second;
+      }
+      else
+      {
+        // my.package.ClassName.myMethodName:(II)I::argNT, where N is the local
+        // variable slot where the parameter is stored and T is a character
+        // indicating the type
+        const typet &type = param.type();
+        char suffix = java_char_from_type(type);
+        base_name = "arg" + std::to_string(param_index) + suffix;
+        identifier =
+          id2string(method_symbol.name) + "::" + id2string(base_name);
+      }
+    }
+    param.set_base_name(base_name);
+    param.set_identifier(identifier);
+
+    // Build a new symbol for the parameter and add it to the symbol table
+    parameter_symbolt parameter_symbol;
+    parameter_symbol.base_name = base_name;
+    parameter_symbol.mode = ID_java;
+    parameter_symbol.name = identifier;
+    parameter_symbol.type = param.type();
+    symbol_table.insert(parameter_symbol);
+
+    param_index += java_local_variable_slots(param.type());
+  }
+}
+
 void java_bytecode_convert_method(
   const symbolt &class_symbol,
   const java_bytecode_parse_treet::methodt &method,

src/java_bytecode/java_bytecode_convert_method.h

@@ -21,6 +21,12 @@ Author: Daniel Kroening, [email protected]
 
 class class_hierarchyt;
 
+void java_bytecode_initialize_parameter_names(
+  symbolt &method_symbol,
+  const java_bytecode_parse_treet::methodt::local_variable_tablet
+    &local_variable_table,
+  symbol_table_baset &symbol_table);
+
 void java_bytecode_convert_method(
   const symbolt &class_symbol,
   const java_bytecode_parse_treet::methodt &,

src/java_bytecode/java_bytecode_language.cpp

@@ -256,11 +256,9 @@ bool java_bytecode_languaget::typecheck(
       convert_single_method(method_sig.first, journalling_symbol_table);
     }
     // Now convert all newly added string methods
-    id_sett string_methods;
-    string_preprocess.get_all_function_names(string_methods);
     for(const auto &fn_name : journalling_symbol_table.get_inserted())
     {
-      if(string_methods.count(fn_name) != 0)
+      if(string_preprocess.implements_function(fn_name))
         convert_single_method(fn_name, symbol_table);
     }
   }
@@ -392,17 +390,29 @@ bool java_bytecode_languaget::convert_single_method(
   if(symbol.value.is_not_nil())
     return false;
 
-  exprt generated_code =
-    string_preprocess.code_for_function(symbol, symbol_table);
-  if(generated_code.is_not_nil())
+  // Get bytecode for specified function if we have it
+  method_bytecodet::opt_reft cmb = method_bytecode.get(function_id);
+
+  // Check if have a string solver implementation
+  if(string_preprocess.implements_function(function_id))
   {
+    symbolt &symbol = symbol_table.get_writeable_ref(function_id);
+    // Load parameter names from any extant bytecode before filling in body
+    if(cmb)
+    {
+      java_bytecode_initialize_parameter_names(
+        symbol, cmb->get().method.local_variable_table, symbol_table);
+    }
     // Populate body of the function with code generated by string preprocess
-    symbol_table.get_writeable_ref(function_id).value = generated_code;
+    exprt generated_code =
+      string_preprocess.code_for_function(symbol, symbol_table);
+    INVARIANT(
+      generated_code.is_not_nil(), "Couldn't retrieve code for string method");
+    symbol.value = generated_code;
     return false;
   }
 
   // No string solver implementation, check if have bytecode for it
-  method_bytecodet::opt_reft cmb = method_bytecode.get(function_id);
   if(cmb)
   {
     java_bytecode_convert_method(

src/java_bytecode/java_string_library_preprocess.cpp

@@ -1758,6 +1758,16 @@ codet java_string_library_preprocesst::make_string_length_code(
   return code_returnt(get_length(deref, symbol_table));
 }
 
+bool java_string_library_preprocesst::implements_function(
+  const irep_idt &function_id) const
+{
+  for(const id_mapt *map : id_maps)
+    if(map->count(function_id) != 0)
+      return true;
+
+  return conversion_table.count(function_id) != 0;
+}
+
 template <typename TMap, typename TContainer>
 void add_keys_to_container(const TMap &map, TContainer &container)
 {
@@ -1775,14 +1785,7 @@ void add_keys_to_container(const TMap &map, TContainer &container)
 void java_string_library_preprocesst::get_all_function_names(
   id_sett &methods) const
 {
-  const id_mapt *maps[] = {
-    &cprover_equivalent_to_java_function,
-    &cprover_equivalent_to_java_string_returning_function,
-    &cprover_equivalent_to_java_constructor,
-    &cprover_equivalent_to_java_assign_and_return_function,
-    &cprover_equivalent_to_java_assign_function,
-  };
-  for(const id_mapt *map : maps)
+  for(const id_mapt *map : id_maps)
     add_keys_to_container(*map, methods);
 
   add_keys_to_container(conversion_table, methods);

src/java_bytecode/java_string_library_preprocess.h

@@ -22,6 +22,7 @@ Date:   March 2017
 
 #include <util/ieee_float.h> // should get rid of this
 
+#include <array>
 #include <unordered_set>
 #include <functional>
 #include "character_refine_preprocess.h"
@@ -45,6 +46,7 @@ class java_string_library_preprocesst:public messaget
   void initialize_conversion_table();
   void initialize_refined_string_type();
 
+  bool implements_function(const irep_idt &function_id) const;
   void get_all_function_names(id_sett &methods) const;
 
   exprt
@@ -126,6 +128,17 @@ class java_string_library_preprocesst:public messaget
   // of returning it
   id_mapt cprover_equivalent_to_java_assign_function;
 
+  const std::array<id_mapt *, 5> id_maps = std::array<id_mapt *, 5>
+    {
+      {
+        &cprover_equivalent_to_java_function,
+        &cprover_equivalent_to_java_string_returning_function,
+        &cprover_equivalent_to_java_constructor,
+        &cprover_equivalent_to_java_assign_and_return_function,
+        &cprover_equivalent_to_java_assign_function,
+      }
+    };
+
   // A set tells us what java types should be considered as string objects
   std::unordered_set<irep_idt, irep_id_hash> string_types;