Minor improvements in bytecode typecheck

Remove commented code.
Remove comment that is no longer relevant as the type is now char array
of fixed size for string litterals data field.
Remove unused includes.
More informative names for symbols introduced.
Improving (pretty_/base_)name of string litterals.

Avoid direct access to struct with hardcoded field numbers.

Author: romainbrenguier

src/java_bytecode/java_bytecode_typecheck_expr.cpp

@@ -13,8 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <iomanip>
 
-#include <util/std_expr.h>
-#include <util/prefix.h>
 #include <util/arith_tools.h>
 #include <util/unicode.h>
 
@@ -110,10 +108,11 @@ void java_bytecode_typecheckt::typecheck_expr_java_string_literal(exprt &expr)
   const irep_idt value=expr.get(ID_value);
   const symbol_typet string_type("java::java.lang.String");
 
-  std::string escaped_symbol_name=JAVA_STRING_LITERAL_PREFIX ".";
-  escaped_symbol_name+=escape_non_alnum(id2string(value));
+  const std::string escaped_symbol_name = escape_non_alnum(id2string(value));
+  const std::string escaped_symbol_name_with_prefix =
+    JAVA_STRING_LITERAL_PREFIX "." + escaped_symbol_name;
 
-  auto findit=symbol_table.symbols.find(escaped_symbol_name);
+  auto findit = symbol_table.symbols.find(escaped_symbol_name_with_prefix);
   if(findit!=symbol_table.symbols.end())
   {
     expr=address_of_exprt(findit->second.symbol_expr());
@@ -122,9 +121,9 @@ void java_bytecode_typecheckt::typecheck_expr_java_string_literal(exprt &expr)
 
   // Create a new symbol:
   symbolt new_symbol;
-  new_symbol.name=escaped_symbol_name;
+  new_symbol.name = escaped_symbol_name_with_prefix;
   new_symbol.type=string_type;
-  new_symbol.base_name="Literal";
+  new_symbol.base_name = escaped_symbol_name;
   new_symbol.pretty_name=value;
   new_symbol.mode=ID_java;
   new_symbol.is_type=false;
@@ -144,15 +143,19 @@ void java_bytecode_typecheckt::typecheck_expr_java_string_literal(exprt &expr)
   if(string_refinement_enabled)
   {
     struct_exprt literal_init(new_symbol.type);
-    literal_init.move_to_operands(jlo_init);
-    literal_init.copy_to_operands(
-      from_integer(id2string(value).size(), jls_struct.components()[1].type()));
+    literal_init.operands().resize(jls_struct.components().size());
+    const std::size_t jlo_nb = jls_struct.component_number("@java.lang.Object");
+    literal_init.operands()[jlo_nb] = jlo_init;
+
+    const std::size_t length_nb = jls_struct.component_number("length");
+    const typet &length_type = jls_struct.components()[length_nb].type();
+    const exprt length = from_integer(id2string(value).size(), length_type);
+    literal_init.operands()[length_nb] = length;
 
     // Initialize the string with a constant utf-16 array:
     symbolt array_symbol;
-    array_symbol.name=escaped_symbol_name+"_constarray";
-    array_symbol.base_name="Literal_constarray";
-    // TODO: this should be obtained from java_string_library_preprocess
+    array_symbol.name = escaped_symbol_name_with_prefix + "_constarray";
+    array_symbol.base_name = escaped_symbol_name + "_constarray";
     array_symbol.pretty_name=value;
     array_symbol.mode=ID_java;
     array_symbol.is_type=false;
@@ -168,23 +171,28 @@ void java_bytecode_typecheckt::typecheck_expr_java_string_literal(exprt &expr)
       throw "failed to add constarray symbol to symbol table";
 
     const symbol_exprt array_expr = array_symbol.symbol_expr();
-    const address_of_exprt first_index(
+    const address_of_exprt array_pointer(
       index_exprt(array_expr, from_integer(0, java_int_type())));
-    literal_init.copy_to_operands(first_index);
+
+    const std::size_t data_nb = jls_struct.component_number("data");
+    literal_init.operands()[data_nb] = array_pointer;
 
     // Associate array with pointer
     symbolt return_symbol;
-    return_symbol.name = "return_value_" + escaped_symbol_name;
-    return_symbol.base_name = escaped_symbol_name;
-    return_symbol.pretty_name = "return_value";
+    return_symbol.name = escaped_symbol_name_with_prefix + "_return_value";
+    return_symbol.base_name = escaped_symbol_name + "_return_value";
+    return_symbol.pretty_name =
+      escaped_symbol_name.length() > 10
+        ? escaped_symbol_name.substr(0, 10) + "..._return_value"
+        : escaped_symbol_name + "_return_value";
     return_symbol.mode = ID_java;
     return_symbol.is_type = false;
     return_symbol.is_lvalue = true;
     return_symbol.is_static_lifetime = true;
     return_symbol.is_state_var = true;
     return_symbol.value = make_function_application(
       ID_cprover_associate_array_to_pointer_func,
-      {array_symbol.value, first_index},
+      {array_symbol.value, array_pointer},
       java_int_type(),
       symbol_table);
     return_symbol.type = return_symbol.value.type();