Remove functions that are destined to be modelled in Java

Remove:
  - StringBuilder.append(Object)
  - StringBuilder.append(Float)
  - StringBuilder.append(Int)
  - StringBuilder.append(Long)

This functions should have java models for them provided instead of
having special treatments for them in the solver.
To be easier to maintain, the solver should only make atomic
operations available, such as concatenation of two strings and
conversion from primitive types to string.

Author: romainbrenguier

src/java_bytecode/java_string_library_preprocess.cpp

@@ -770,65 +770,6 @@ codet java_string_library_preprocesst::
   return code;
 }
 
-/// \param type: type of the function called
-/// \param loc: location in the program
-/// \param symbol_table: symbol table
-/// \return code for the StringBuilder.append(Object) function: > string1 =
-///   arguments[1].toString() > string_expr1 = string_to_string_expr(string1) >
-///   string_expr2 = concat(this, string_expr1) > this =
-///   string_expr_to_string(string_expr2) > return this
-codet java_string_library_preprocesst::make_string_builder_append_object_code(
-  const code_typet &type,
-  const source_locationt &loc,
-  symbol_tablet &symbol_table)
-{
-  code_typet::parameterst params=type.parameters();
-  assert(params.size()==1);
-  exprt this_obj=symbol_exprt(params[0].get_identifier(), params[0].type());
-
-  // Code to be returned
-  code_blockt code;
-
-  // String expression that will hold the result
-  string_exprt string_expr1=fresh_string_expr(loc, symbol_table, code);
-
-  exprt::operandst arguments=process_parameters(
-    type.parameters(), loc, symbol_table, code);
-  assert(arguments.size()==2);
-
-  // > string1 = arguments[1].toString()
-  exprt string1=fresh_string(this_obj.type(), loc, symbol_table);
-  code_function_callt fun_call;
-  fun_call.lhs()=string1;
-  // TODO: we should look in the symbol table for such a symbol
-  fun_call.function()=symbol_exprt(
-    "java::java.lang.Object.toString:()Ljava/lang/String;");
-  fun_call.arguments().push_back(arguments[1]);
-  code_typet fun_type;
-  fun_type.return_type()=string1.type();
-  fun_call.function().type()=fun_type;
-  code.add(fun_call);
-
-  // > string_expr1 = string_to_string_expr(string1)
-  code.add(code_assign_java_string_to_string_expr(
-    string_expr1, string1, symbol_table));
-
-  // > string_expr2 = concat(this, string1)
-  exprt::operandst concat_arguments(arguments);
-  concat_arguments[1]=string_expr1;
-  string_exprt string_expr2=string_expr_of_function_application(
-    ID_cprover_string_concat_func, concat_arguments, loc, symbol_table, code);
-
-  // > this = string_expr
-  code.add(code_assign_string_expr_to_java_string(
-    this_obj, string_expr2, symbol_table));
-
-  // > return this
-  code.add(code_returnt(this_obj));
-
-  return code;
-}
-
 /// Used to provide code for the Java String.equals(Object) function.
 /// \param type: type of the function call
 /// \param loc: location in the program_invocation_name
@@ -856,71 +797,6 @@ codet java_string_library_preprocesst::make_equals_function_code(
   return code;
 }
 
-/// Used to provide code for the Java StringBuilder.append(F) function.
-/// \param type: type of the function call
-/// \param loc: location in the program_invocation_name
-/// \param symbol_table: symbol table
-/// \return Code corresponding to: > string1 = arguments[1].toString() >
-///   string_expr1 = string_to_string_expr(string1) > string_expr2 =
-///   concat(this, string_expr1) > this = string_expr_to_string(string_expr2) >
-///   return this
-codet java_string_library_preprocesst::make_string_builder_append_float_code(
-  const code_typet &type,
-  const source_locationt &loc,
-  symbol_tablet &symbol_table)
-{
-  code_typet::parameterst params=type.parameters();
-  assert(params.size()==1);
-  exprt this_obj=symbol_exprt(params[0].get_identifier(), params[0].type());
-
-  // Getting types
-  typet length_type=string_length_type();
-
-  // Code to be returned
-  code_blockt code;
-
-  // String expression that will hold the result
-  refined_string_typet ref_type(length_type, java_char_type());
-  string_exprt string_expr1=fresh_string_expr(loc, symbol_table, code);
-
-  exprt::operandst arguments=process_parameters(
-    type.parameters(), loc, symbol_table, code);
-  assert(arguments.size()==2);
-
-  // > string1 = arguments[1].toString()
-  exprt string1=fresh_string(this_obj.type(), loc, symbol_table);
-  code_function_callt fun_call;
-  fun_call.lhs()=string1;
-  // TODO: we should look in the symbol table for such a symbol
-  fun_call.function()=symbol_exprt(
-    "java::java.lang.Float.toString:()Ljava/lang/String;");
-  fun_call.arguments().push_back(arguments[1]);
-  code_typet fun_type;
-  fun_type.return_type()=string1.type();
-  fun_call.function().type()=fun_type;
-  code.add(fun_call);
-
-  // > string_expr1 = string_to_string_expr(string1)
-  code.add(code_assign_java_string_to_string_expr(
-    string_expr1, string1, symbol_table));
-
-  // > string_expr2 = concat(this, string1)
-  exprt::operandst concat_arguments(arguments);
-  concat_arguments[1]=string_expr1;
-
-  string_exprt string_expr2=string_expr_of_function_application(
-    ID_cprover_string_concat_func, concat_arguments, loc, symbol_table, code);
-
-  // > this = string_expr
-  code.add(code_assign_string_expr_to_java_string(
-    this_obj, string_expr2, symbol_table));
-
-  // > return this
-  code.add(code_returnt(this_obj));
-
-  return code;
-}
-
 /// construct a Java string literal from a constant string value
 /// \param s: a string
 /// \return an expression representing a Java string literal with the given
@@ -1739,29 +1615,14 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_assign_and_return_function
     ["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"]=
       ID_cprover_string_concat_double_func;
-  conversion_table
-    ["java::java.lang.StringBuilder.append:(F)Ljava/lang/StringBuilder;"]=
-      std::bind(
-        &java_string_library_preprocesst::make_string_builder_append_float_code,
-        this,
-        std::placeholders::_1,
-        std::placeholders::_2,
-        std::placeholders::_3);
-  cprover_equivalent_to_java_assign_and_return_function
-    ["java::java.lang.StringBuilder.append:(I)Ljava/lang/StringBuilder;"]=
-      ID_cprover_string_concat_int_func;
-  cprover_equivalent_to_java_assign_and_return_function
-    ["java::java.lang.StringBuilder.append:(J)Ljava/lang/StringBuilder;"]=
-      ID_cprover_string_concat_long_func;
-
-  conversion_table["java::java.lang.StringBuilder.append:"
-                   "(Ljava/lang/Object;)Ljava/lang/StringBuilder;"]=
-    std::bind(
-      &java_string_library_preprocesst::make_string_builder_append_object_code,
-      this,
-      std::placeholders::_1,
-      std::placeholders::_2,
-      std::placeholders::_3);
+  // Not supported: "java.lang.StringBuilder.append:"
+  //   "(F)Ljava/lang/StringBuilder;"
+  // Not supported: "java.lang.StringBuilder.append:(I)"
+  //   "Ljava/lang/StringBuilder;"
+  // Not supported: "java.lang.StringBuilder.append:(J)"
+  //   "Ljava/lang/StringBuilder;"
+  // Not supported: "java.lang.StringBuilder.append:"
+  //   "(Ljava/lang/Object;)Ljava/lang/StringBuilder;"
   cprover_equivalent_to_java_assign_and_return_function
     ["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
       "Ljava/lang/StringBuilder;"]=

src/java_bytecode/java_string_library_preprocess.h

@@ -113,22 +113,11 @@ class java_string_library_preprocesst:public messaget
   // A set tells us what java types should be considered as string objects
   std::unordered_set<irep_idt, irep_id_hash> string_types;
 
-  // Conversion functions
-  codet make_string_builder_append_object_code(
-    const code_typet &type,
-    const source_locationt &loc,
-    symbol_tablet &symbol_table);
-
   codet make_equals_function_code(
     const code_typet &type,
     const source_locationt &loc,
     symbol_tablet &symbol_table);
 
-  codet make_string_builder_append_float_code(
-    const code_typet &type,
-    const source_locationt &loc,
-    symbol_tablet &symbol_table);
-
   codet make_float_to_string_code(
     const code_typet &type,
     const source_locationt &loc,