Remove code that is now unreachable

To use the builtin format function, the java entry point is now
CProverString.format, so we can remove the legacy code which was
handling String.format directly.

Author: romainbrenguier

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -1101,278 +1101,6 @@ code_blockt java_string_library_preprocesst::make_assign_function_from_call(
     function_id, type, loc, symbol_table, false);
 }
 
-/// Adds to the code an assignment of the form
-/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-/// type_name tmp_type_name
-/// tmp_type_name = ((Classname*)arg_i)->value
-/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-/// and returns `tmp_typename`.
-/// In case the class corresponding to `type_name` is not available in
-/// `symbol_table`, the variable is declared but not assigned.
-/// Used to access the values of the arguments of `String.format`.
-/// \param object: an expression representing a reference to an object
-/// \param type_name: name of the corresponding primitive type, this can be
-///   one of the following: ID_boolean, ID_char, ID_byte, ID_short, ID_int,
-///   ID_long, ID_float, ID_double, ID_void
-/// \param loc: a location in the source
-/// \param function_id: the name of the function
-/// \param symbol_table: the symbol table
-/// \param code: code block to which we are adding some assignments
-/// \return An expression containing a symbol `tmp_type_name` where `type_name`
-///   is the given argument (ie. boolean, char etc.). Which represents the
-///   primitive value contained in the given object.
-optionalt<symbol_exprt>
-java_string_library_preprocesst::get_primitive_value_of_object(
-    const exprt &object, irep_idt type_name, const source_locationt &loc,
-    const irep_idt &function_id, symbol_table_baset &symbol_table,
-    code_blockt &code) {
-  optionalt<struct_tag_typet> object_type;
-
-  typet value_type;
-  if (type_name == ID_boolean) {
-    value_type = java_boolean_type();
-    object_type = struct_tag_typet("java::java.lang.Boolean");
-  } else if (type_name == ID_char) {
-    value_type = java_char_type();
-    object_type = struct_tag_typet("java::java.lang.Character");
-  } else if (type_name == ID_byte) {
-    value_type = java_byte_type();
-    object_type = struct_tag_typet("java::java.lang.Byte");
-  } else if (type_name == ID_short) {
-    value_type = java_short_type();
-    object_type = struct_tag_typet("java::java.lang.Short");
-  } else if (type_name == ID_int) {
-    value_type = java_int_type();
-    object_type = struct_tag_typet("java::java.lang.Integer");
-  } else if (type_name == ID_long) {
-    value_type = java_long_type();
-    object_type = struct_tag_typet("java::java.lang.Long");
-  } else if (type_name == ID_float) {
-    value_type = java_float_type();
-    object_type = struct_tag_typet("java::java.lang.Float");
-  } else if (type_name == ID_double) {
-    value_type = java_double_type();
-    object_type = struct_tag_typet("java::java.lang.Double");
-  } else if (type_name == ID_void)
-    return {};
-  else
-    UNREACHABLE;
-
-  DATA_INVARIANT(object_type.has_value(), "must have symbol for primitive");
-
-  // declare tmp_type_name to hold the value
-  const std::string aux_name = "tmp_" + id2string(type_name);
-  const symbolt &symbol =
-      fresh_java_symbol(value_type, aux_name, loc, function_id, symbol_table);
-  const auto value = symbol.symbol_expr();
-
-  // Check that the type of the object is in the symbol table,
-  // otherwise there is no safe way of finding its value.
-  if (const auto maybe_symbol =
-          symbol_table.lookup(object_type->get_identifier())) {
-    const struct_typet &struct_type = to_struct_type(maybe_symbol->type);
-    // Check that the type has a value field
-    const struct_union_typet::componentt &value_comp =
-        struct_type.get_component("value");
-    if (!value_comp.is_nil()) {
-      const pointer_typet struct_pointer_type = pointer_type(struct_type);
-      dereference_exprt deref{typecast_exprt(object, struct_pointer_type),
-                              struct_pointer_type.subtype()};
-      const member_exprt deref_value{std::move(deref), value_comp.get_name(),
-                                     value_comp.type()};
-      code.add(code_assignt(value, deref_value), loc);
-      return value;
-    }
-  }
-
-  warning() << object_type->get_identifier()
-            << " not available to format function" << eom;
-  code.add(code_declt(value), loc);
-  return value;
-}
-
-/// Helper for format function. Returns the expression:
-/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-/// *((void**)(argv->data)+index )
-/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-/// which corresponds to the object at position `index` in  `argv`.
-/// \param argv: reference to an array of references
-/// \param index: index of the desired object
-/// \return An expression representing the object at position `index` of `argv`.
-dereference_exprt
-java_string_library_preprocesst::get_object_at_index(const exprt &argv,
-                                                     std::size_t index) {
-  const dereference_exprt deref_objs{argv, argv.type().subtype()};
-  const pointer_typet empty_pointer = pointer_type(java_void_type());
-  const pointer_typet pointer_of_pointer = pointer_type(empty_pointer);
-  const member_exprt data_member{deref_objs, "data", pointer_of_pointer};
-  const plus_exprt data_pointer_plus_index{
-      data_member, from_integer(index, java_int_type()), data_member.type()};
-  return dereference_exprt{data_pointer_plus_index,
-                           data_pointer_plus_index.type().subtype()};
-}
-
-/// Helper for format function. Adds code:
-/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-/// string_expr arg_i_string_expr;
-/// int tmp_int;
-/// float tmp_float;
-/// char tmp_char;
-/// boolean tmp_boolean;
-/// Object* arg_i=get_object_at_index(argv, index)
-/// if(arg_i.@class_identifier=="java::java.lang.String")
-/// {
-///   arg_i_string_expr = (string_expr)((String*)arg_i_as_string)
-/// }
-/// tmp_int=((Integer)arg_i)->value
-/// tmp_float=((Float)arg_i)->value
-/// tmp_char=((Char)arg_i)->value
-/// tmp_boolean=((Boolean)arg_i)->value
-/// arg_i_struct = { string_expr=arg_i_string_expr;
-///   integer=tmp_int; float=tmp_float; char=tmp_char; boolean=tmp_boolean}
-/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-/// and returns `arg_i_struct`.
-///
-/// TODO: date_time and hash code are not implemented
-/// \param argv: reference to an array of references
-/// \param index: index of the desired argument
-/// \param structured_type: type for arguments of the internal format function
-/// \param loc: a location in the source
-/// \param function_id: function the generated expression will be used in
-/// \param symbol_table: the symbol table
-/// \param code: code block to which we are adding some assignments
-/// \return An expression of type `structured_type` representing the possible
-///         values of the argument at position `index` of `argv`.
-struct_exprt java_string_library_preprocesst::make_argument_for_format(
-    const exprt &argv, std::size_t index, const struct_typet &structured_type,
-    const source_locationt &loc, const irep_idt &function_id,
-    symbol_table_baset &symbol_table, code_blockt &code) {
-  // Declarations of the fields of arg_i_struct
-  // arg_i_struct is { arg_i_string_expr, tmp_int, tmp_char, ... }
-  struct_exprt arg_i_struct({}, structured_type);
-  std::list<exprt> field_exprs;
-  for (const auto &comp : structured_type.components()) {
-    const irep_idt &name = comp.get_name();
-    const typet &type = comp.type();
-    exprt field_expr;
-    if (name != "string_expr") {
-      std::string tmp_name = "tmp_" + id2string(name);
-      const symbolt &field_symbol =
-          fresh_java_symbol(type, tmp_name, loc, function_id, symbol_table);
-      auto field_symbol_expr = field_symbol.symbol_expr();
-      field_expr = field_symbol_expr;
-      code.add(code_declt(field_symbol_expr), loc);
-    } else
-      field_expr =
-          make_nondet_string_expr(loc, function_id, symbol_table, code);
-
-    field_exprs.push_back(field_expr);
-    arg_i_struct.copy_to_operands(field_expr);
-  }
-
-  // arg_i = argv[index]
-  const exprt obj = get_object_at_index(argv, index);
-  const symbolt &object_symbol = fresh_java_symbol(
-      obj.type(), "tmp_format_obj", loc, function_id, symbol_table);
-  const symbol_exprt arg_i = object_symbol.symbol_expr();
-
-  allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
-
-  code_blockt tmp;
-  allocate_objects.allocate_dynamic_object(tmp, arg_i, arg_i.type().subtype());
-  allocate_objects.declare_created_symbols(code);
-  code.append(tmp);
-
-  code.add(code_assignt(arg_i, obj), loc);
-  code.add(code_assumet(not_exprt(equal_exprt(
-               arg_i, null_pointer_exprt(to_pointer_type(arg_i.type()))))),
-           loc);
-
-  code_blockt code_not_null;
-
-  // Assigning all the fields of arg_i_struct
-  for (const auto &comp : structured_type.components()) {
-    const irep_idt &name = comp.get_name();
-    exprt field_expr = field_exprs.front();
-    field_exprs.pop_front();
-
-    if (name == "string_expr") {
-      const pointer_typet string_pointer =
-          java_reference_type(struct_tag_typet("java::java.lang.String"));
-      const typecast_exprt arg_i_as_string{arg_i, string_pointer};
-      code_assign_java_string_to_string_expr(to_string_expr(field_expr),
-                                             arg_i_as_string, loc, symbol_table,
-                                             code_not_null);
-    } else if (name == ID_int || name == ID_float || name == ID_char ||
-               name == ID_boolean) {
-      const auto value = get_primitive_value_of_object(
-          arg_i, name, loc, function_id, symbol_table, code_not_null);
-      if (value.has_value())
-        code_not_null.add(code_assignt(field_expr, *value), loc);
-      else
-        code_not_null.add(code_assignt(field_expr, nil_exprt()), loc);
-    } else {
-      // TODO: date_time and hash_code not implemented
-    }
-  }
-
-  code.add(code_not_null, loc);
-  return arg_i_struct;
-}
-
-/// Used to provide code for the Java String.format function.
-///
-/// TODO: date_time and hash code are not implemented, and we set a limit of
-/// 10 arguments
-/// \param type: type of the function call
-/// \param loc: location in the program_invocation_name
-/// \param function_id: function the generated code will be used in
-/// \param symbol_table: symbol table
-/// \return Code implementing the Java String.format function. Since the exact
-///   class of the arguments is not known, we give as argument to the internal
-//    format function a structure containing the different possible types.
-code_blockt java_string_library_preprocesst::make_string_format_code(
-    const java_method_typet &type, const source_locationt &loc,
-    const irep_idt &function_id, symbol_table_baset &symbol_table) {
-  PRECONDITION(type.parameters().size() == 2);
-  code_blockt code;
-  exprt::operandst args = process_parameters(type.parameters(), loc,
-                                             function_id, symbol_table, code);
-  INVARIANT(args.size() == 2, "String.format should have two arguments");
-
-  // The argument can be:
-  // a string, an integer, a floating point, a character, a boolean,
-  // an object of which we take the hash code, or a date/time
-  struct_typet structured_type({{"string_expr", refined_string_type},
-                                {ID_int, java_int_type()},
-                                {ID_float, java_float_type()},
-                                {ID_char, java_char_type()},
-                                {ID_boolean, java_boolean_type()},
-                                // TODO: hash_code not implemented for now
-                                {"hashcode", java_int_type()},
-                                // TODO: date_time type not implemented for now
-                                {"date_time", java_int_type()}});
-  structured_type.set_tag(CPROVER_PREFIX "string_formatter_variant");
-
-  // We will process arguments so that each is converted to a `struct_exprt`
-  // containing each possible type used in format specifiers.
-  std::vector<exprt> processed_args;
-  processed_args.push_back(args[0]);
-  for (std::size_t i = 0; i < MAX_FORMAT_ARGS; ++i)
-    processed_args.push_back(make_argument_for_format(
-        args[1], i, structured_type, loc, function_id, symbol_table, code));
-
-  const refined_string_exprt string_expr = string_expr_of_function(
-      ID_cprover_string_format_func, processed_args, loc, symbol_table, code);
-  const exprt java_string = allocate_fresh_string(
-      type.return_type(), loc, function_id, symbol_table, code);
-  code.add(code_assign_string_expr_to_java_string(java_string, string_expr,
-                                                  symbol_table, true),
-           loc);
-  code.add(code_returnt(java_string), loc);
-  return code;
-}
-
 /// Used to provide our own implementation of the java.lang.Object.getClass()
 /// function.
 /// \param type: type of the function called

jbmc/src/java_bytecode/java_string_library_preprocess.h

@@ -151,11 +151,6 @@ class java_string_library_preprocesst:public messaget
     const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
-  code_blockt make_string_format_code(const java_method_typet &type,
-                                      const source_locationt &loc,
-                                      const irep_idt &function_id,
-                                      symbol_table_baset &symbol_table);
-
   code_blockt make_copy_string_code(
     const java_method_typet &type,
     const source_locationt &loc,
@@ -312,20 +307,6 @@ class java_string_library_preprocesst:public messaget
     const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
-
-  struct_exprt make_argument_for_format(const exprt &argv, std::size_t index,
-                                        const struct_typet &structured_type,
-                                        const source_locationt &loc,
-                                        const irep_idt &function_id,
-                                        symbol_table_baset &symbol_table,
-                                        code_blockt &code);
-
-  optionalt<symbol_exprt> get_primitive_value_of_object(
-      const exprt &object, irep_idt type_name, const source_locationt &loc,
-      const irep_idt &function_id, symbol_table_baset &symbol_table,
-      code_blockt &code);
-
-  dereference_exprt get_object_at_index(const exprt &argv, std::size_t index);
 };
 
 exprt make_nondet_infinite_char_array(

src/solvers/strings/string_constraint_generator_format.cpp

@@ -239,17 +239,6 @@ static std::vector<format_elementt> parse_format_string(std::string s)
   return al;
 }
 
-/// Helper for add_axioms_for_format_specifier
-/// \param expr: a structured expression
-/// \param component_name: name of the desired component
-/// \return Expression in the component of `expr` named `component_name`.
-static exprt get_component_in_struct(const struct_exprt &expr,
-                                     irep_idt component_name) {
-  const struct_typet &type = to_struct_type(expr.type());
-  std::size_t number = type.component_number(component_name);
-  return expr.operands()[number];
-}
-
 /// Parse `s` and add axioms ensuring the output corresponds to the output of
 /// String.format. Assumes the argument is a structured expression which
 /// contains the fields: string expr, int, float, char, boolean, hashcode,
@@ -447,6 +436,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
     if(fe.is_format_specifier())
     {
       const format_specifiert &fs = fe.get_format_specifier();
+      std::function<exprt(const irep_idt &)> get_arg =
+          [](const irep_idt &) -> exprt { UNREACHABLE; };
+
       if(
         fs.conversion != format_specifiert::PERCENT_SIGN &&
         fs.conversion != format_specifiert::LINE_SEPARATOR)
@@ -470,36 +462,26 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
           arg = to_struct_expr(args[fs.index - 1]);
         }
 
-        std::function<exprt(const irep_idt &)> get_arg;
-        if(is_refined_string_type(arg.type()))
-        {
-          const array_string_exprt string_arg =
-            get_string_expr(array_pool, arg);
-          get_arg = [string_arg](const irep_idt &id) {
-            return format_arg_from_string(string_arg, id);
-          };
-        }
-        else
-        {
-          INVARIANT(
-            arg.id() == ID_struct,
-            "format argument should be a string or a struct");
-          get_arg = [&](const irep_idt &id) {
-            return get_component_in_struct(to_struct_expr(arg), id);
-          };
-        }
-        auto result = add_axioms_for_format_specifier(
-          fresh_symbol,
-          fs,
-          get_arg,
-          index_type,
-          char_type,
-          array_pool,
-          message,
-          ns);
-        merge(constraints, std::move(result.second));
-        intermediary_strings.push_back(result.first);
+        INVARIANT(
+          is_refined_string_type(arg.type()),
+          "arguments of format should be strings");
+        const array_string_exprt string_arg = get_string_expr(array_pool, arg);
+        get_arg = [string_arg](const irep_idt &id) {
+          return format_arg_from_string(string_arg, id);
+        };
       }
+
+      auto result = add_axioms_for_format_specifier(
+        fresh_symbol,
+        fs,
+        get_arg,
+        index_type,
+        char_type,
+        array_pool,
+        message,
+        ns);
+      merge(constraints, std::move(result.second));
+      intermediary_strings.push_back(result.first);
     }
     else
     {