simple_method_stubbing.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Simple Java method stubbing
 
Author: Diffblue Ltd.
 
\*******************************************************************/
 
 
#include "simple_method_stubbing.h"
 
#include <java_bytecode/java_object_factory.h>
#include <java_bytecode/java_object_factory_parameters.h>
#include <java_bytecode/java_pointer_casts.h>
#include <java_bytecode/java_types.h>
 
#include "java_utils.h"
#include <util/invariant_utils.h>
#include <util/namespace.h>
#include <util/std_code.h>
#include <util/symbol_table_base.h>
 
class java_simple_method_stubst
{
public:
  java_simple_method_stubst(
    symbol_table_baset &_symbol_table,
    bool _assume_non_null,
    const java_object_factory_parameterst &_object_factory_parameters,
    message_handlert &_message_handler)
    : symbol_table(_symbol_table),
      assume_non_null(_assume_non_null),
      object_factory_parameters(_object_factory_parameters),
      message_handler(_message_handler)
  {
  }
 
  void create_method_stub_at(
    const typet &expected_type,
    const exprt &ptr,
    const source_locationt &loc,
    const irep_idt &function_id,
    code_blockt &parent_block,
    unsigned insert_before_index,
    bool is_constructor,
    bool update_in_place);
 
  void create_method_stub(symbolt &symbol);
 
  void check_method_stub(const irep_idt &);
 
protected:
  symbol_table_baset &symbol_table;
  bool assume_non_null;
  const java_object_factory_parameterst &object_factory_parameters;
  message_handlert &message_handler;
};
 
void java_simple_method_stubst::create_method_stub_at(
  const typet &expected_type,
  const exprt &ptr,
  const source_locationt &loc,
  const irep_idt &function_id,
  code_blockt &parent_block,
  const unsigned insert_before_index,
  const bool is_constructor,
  const bool update_in_place)
{
  // At this point we know 'ptr' points to an opaque-typed object.
  // We should nondet-initialize it and insert the instructions *after*
  // the offending call at (*parent_block)[insert_before_index].
 
  INVARIANT_WITH_IREP(
    expected_type.id() == ID_pointer,
    "Nondet initializer result type: expected a pointer",
    expected_type);
 
  if(to_pointer_type(expected_type).base_type().id() != ID_struct_tag)
    return;
 
  namespacet ns(symbol_table);
  const exprt cast_ptr =
    make_clean_pointer_cast(ptr, to_pointer_type(expected_type), ns);
 
  exprt to_init = cast_ptr;
  // If it's a constructor the thing we're constructing has already
  // been allocated by this point.
  if(is_constructor)
    to_init = dereference_exprt(to_init);
 
  java_object_factory_parameterst parameters = object_factory_parameters;
  if(assume_non_null)
    parameters.min_null_tree_depth = 1;
 
  // Generate new instructions.
  code_blockt new_instructions;
  parameters.function_id = function_id;
  gen_nondet_init(
    to_init,
    new_instructions,
    symbol_table,
    loc,
    is_constructor,
    lifetimet::DYNAMIC,
    parameters,
    update_in_place ? update_in_placet::MUST_UPDATE_IN_PLACE
                    : update_in_placet::NO_UPDATE_IN_PLACE,
    message_handler);
 
  // Insert new_instructions into parent block.
  if(!new_instructions.statements().empty())
  {
    auto insert_position = parent_block.statements().begin();
    std::advance(insert_position, insert_before_index);
    parent_block.statements().insert(
      insert_position,
      new_instructions.statements().begin(),
      new_instructions.statements().end());
  }
}
 
void java_simple_method_stubst::create_method_stub(symbolt &symbol)
{
  code_blockt new_instructions;
  java_method_typet &required_type = to_java_method_type(symbol.type);
 
  // synthetic source location that contains the opaque function name only
  source_locationt synthesized_source_location;
  synthesized_source_location.set_function(symbol.name);
 
  // make sure all parameters are named
  for(auto &parameter : required_type.parameters())
  {
    if(parameter.get_identifier().empty())
    {
      symbolt &parameter_symbol = fresh_java_symbol(
        parameter.type(),
        "#anon",
        synthesized_source_location,
        symbol.name,
        symbol_table);
      parameter_symbol.is_parameter = true;
      parameter.set_base_name(parameter_symbol.base_name);
      parameter.set_identifier(parameter_symbol.name);
    }
  }
 
  // Initialize the return value or `this` parameter under construction.
  // Note symbol.type is required_type, but with write access
  // Probably required_type should not be const
  const bool is_constructor = required_type.get_is_constructor();
  if(is_constructor)
  {
    const auto &this_argument = required_type.parameters()[0];
    const typet &this_type = this_argument.type();
    symbolt &init_symbol = fresh_java_symbol(
      this_type,
      "to_construct",
      synthesized_source_location,
      symbol.name,
      symbol_table);
    const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr();
    code_frontend_assignt get_argument(
      init_symbol_expression,
      symbol_exprt(this_argument.get_identifier(), this_type));
    get_argument.add_source_location() = synthesized_source_location;
    new_instructions.add(get_argument);
    create_method_stub_at(
      this_type,
      init_symbol_expression,
      synthesized_source_location,
      symbol.name,
      new_instructions,
      1,
      true,
      false);
  }
  else
  {
    const typet &required_return_type = required_type.return_type();
    if(required_return_type != java_void_type())
    {
      symbolt &to_return_symbol = fresh_java_symbol(
        required_return_type,
        "to_return",
        synthesized_source_location,
        symbol.name,
        symbol_table);
      const exprt &to_return = to_return_symbol.symbol_expr();
      if(to_return_symbol.type.id() != ID_pointer)
      {
        java_object_factory_parameterst parameters = object_factory_parameters;
        if(assume_non_null)
          parameters.min_null_tree_depth = 1;
 
        gen_nondet_init(
          to_return,
          new_instructions,
          symbol_table,
          source_locationt(),
          false,
          lifetimet::AUTOMATIC_LOCAL, // Irrelevant as type is primitive
          parameters,
          update_in_placet::NO_UPDATE_IN_PLACE,
          message_handler);
      }
      else
        create_method_stub_at(
          required_return_type,
          to_return,
          synthesized_source_location,
          symbol.name,
          new_instructions,
          0,
          false,
          false);
      new_instructions.add(code_frontend_returnt(to_return));
    }
  }
 
  symbol.value = new_instructions;
}
 
void java_simple_method_stubst::check_method_stub(const irep_idt &symname)
{
  const symbolt &sym = symbol_table.lookup_ref(symname);
  if(!sym.is_type && sym.value.id() == ID_nil &&
    sym.type.id() == ID_code &&
    // do not stub internal locking calls as 'create_method_stub' does not
    // automatically create the appropriate symbols for the formal parameters.
    // This means that symex will (rightfully) crash  when it encounters the
    // function call as it will not be able to find symbols for the fromal
    // parameters.
    sym.name !=
      "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" &&
    sym.name !=
      "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V")
  {
    create_method_stub(symbol_table.get_writeable_ref(symname));
  }
}
 
void java_generate_simple_method_stub(
  const irep_idt &function_name,
  symbol_table_baset &symbol_table,
  bool assume_non_null,
  const java_object_factory_parameterst &object_factory_parameters,
  message_handlert &message_handler)
{
  java_simple_method_stubst stub_generator(
    symbol_table, assume_non_null, object_factory_parameters, message_handler);
 
  stub_generator.check_method_stub(function_name);
}
 
void java_generate_simple_method_stubs(
  symbol_table_baset &symbol_table,
  bool assume_non_null,
  const java_object_factory_parameterst &object_factory_parameters,
  message_handlert &message_handler)
{
  // The intent here is to apply stub_generator.check_method_stub() to
  // all the identifiers in the symbol table. However this method may alter the
  // symbol table and iterating over a container which is being modified has
  // undefined behaviour. Therefore in order for this to work reliably, we must
  // take a copy of the identifiers in the symbol table and iterate over that,
  // instead of iterating over the symbol table itself.
  std::vector<irep_idt> identifiers;
  identifiers.reserve(symbol_table.symbols.size());
  for(const auto &symbol : symbol_table)
    identifiers.push_back(symbol.first);
 
  java_simple_method_stubst stub_generator(
    symbol_table, assume_non_null, object_factory_parameters, message_handler);
 
  for(const auto &identifier : identifiers)
  {
    stub_generator.check_method_stub(identifier);
  }
}