java_bytecode_convert_method_class.h

/*******************************************************************\

Module: JAVA Bytecode Language Conversion

Author: Daniel Kroening, kroening@kroening.com

\*******************************************************************/

/// \file
/// JAVA Bytecode Language Conversion

#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_CLASS_H
#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_CLASS_H

#include <util/expanding_vector.h>
#include <util/message.h>
#include <util/std_types.h>
#include <util/std_expr.h>
#include <analyses/cfg_dominators.h>
#include "java_bytecode_parse_tree.h"
#include "java_bytecode_convert_class.h"
#include <java_bytecode/ci_lazy_methods_needed.h>

#include <vector>
#include <list>

class symbol_tablet;
class symbolt;

class java_bytecode_convert_methodt:public messaget
{
public:
  java_bytecode_convert_methodt(
    symbol_table_baset &symbol_table,
    message_handlert &_message_handler,
    size_t _max_array_length,
    optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
    java_string_library_preprocesst &_string_preprocess,
    const class_hierarchyt &class_hierarchy)
    : messaget(_message_handler),
      symbol_table(symbol_table),
      max_array_length(_max_array_length),
      needed_lazy_methods(std::move(needed_lazy_methods)),
      string_preprocess(_string_preprocess),
      slots_for_parameters(0),
      method_has_this(false),
      class_hierarchy(class_hierarchy)
  {
  }

  typedef java_bytecode_parse_treet::methodt methodt;
  typedef java_bytecode_parse_treet::instructiont instructiont;
  typedef methodt::instructionst instructionst;
  typedef methodt::local_variable_tablet local_variable_tablet;
  typedef methodt::local_variablet local_variablet;

  void operator()(const symbolt &class_symbol, const methodt &method)
  {
    convert(class_symbol, method);
  }

protected:
  symbol_table_baset &symbol_table;
  const size_t max_array_length;
  optionalt<ci_lazy_methods_neededt> needed_lazy_methods;

  /// Fully qualified name of the method under translation.
  /// Initialized by `convert`.
  /// Example: "my.package.ClassName.myMethodName:(II)I"
  irep_idt method_id;

  /// A copy of `method_id` :/
  irep_idt current_method;

  /// Return type of the method under conversion.
  /// Initialized by `convert`.
  typet method_return_type;

  java_string_library_preprocesst &string_preprocess;

  /// Number of local variable slots used by the JVM to pass parameters upon
  /// invocation of the method under translation.
  /// Initialized in `convert`.
  unsigned slots_for_parameters;

public:
  struct holet
  {
    unsigned start_pc;
    unsigned length;
  };

  struct local_variable_with_holest
  {
    local_variablet var;
    bool is_parameter;
    std::vector<holet> holes;
  };

  typedef std::vector<local_variable_with_holest>
    local_variable_table_with_holest;

  class variablet
  {
  public:
    symbol_exprt symbol_expr;
    size_t start_pc;
    size_t length;
    bool is_parameter;
    std::vector<holet> holes;
    variablet() : symbol_expr(), start_pc(0), length(0), is_parameter(false) {}
  };

protected:
  typedef std::vector<variablet> variablest;
  expanding_vectort<variablest> variables;
  std::set<symbol_exprt> used_local_names;
  bool method_has_this;
  std::map<irep_idt, bool> class_has_clinit_method;
  std::map<irep_idt, bool> any_superclass_has_clinit_method;
  class_hierarchyt class_hierarchy;

  enum instruction_sizet
  {
    INST_INDEX=2,
    INST_INDEX_CONST=3
  };

  // return corresponding reference of variable
  const variablet &find_variable_for_slot(
    size_t address,
    variablest &var_list);

  // JVM local variables
  enum variable_cast_argumentt
  {
    CAST_AS_NEEDED,
    NO_CAST
  };

  const exprt variable(
    const exprt &arg,
    char type_char,
    size_t address,
    variable_cast_argumentt do_cast);

  // temporary variables
  std::list<symbol_exprt> tmp_vars;

  symbol_exprt tmp_variable(const std::string &prefix, const typet &type);

  // JVM program locations
  irep_idt label(const irep_idt &address);

  // JVM Stack
  typedef std::vector<exprt> stackt;
  stackt stack;

  exprt::operandst pop(std::size_t n);

  void pop_residue(std::size_t n);
  void push(const exprt::operandst &o);

  /// Returns true iff the slot index of the local variable of a method (coming
  /// from the LVT) is a parameter of that method. Assumes that
  /// `slots_for_parameters` is initialized upon call.
  bool is_parameter(const local_variablet &v)
  {
    return v.index<slots_for_parameters;
  }

  struct converted_instructiont
  {
    converted_instructiont(
      const instructionst::const_iterator &it,
      const codet &_code):source(it), code(_code), done(false)
      {}

    instructionst::const_iterator source;
    std::list<unsigned> successors;
    std::set<unsigned> predecessors;
    codet code;
    stackt stack;
    bool done;
  };

public:
  typedef std::map<unsigned, converted_instructiont> address_mapt;
  typedef std::pair<const methodt &, const address_mapt &> method_with_amapt;
  typedef cfg_dominators_templatet<method_with_amapt, unsigned, false>
    java_cfg_dominatorst;

protected:
  void find_initializers(
    local_variable_table_with_holest &vars,
    const address_mapt &amap,
    const java_cfg_dominatorst &doms);

  void find_initializers_for_slot(
    local_variable_table_with_holest::iterator firstvar,
    local_variable_table_with_holest::iterator varlimit,
    const address_mapt &amap,
    const java_cfg_dominatorst &doms);

  void setup_local_variables(const methodt &m, const address_mapt &amap);

  struct block_tree_nodet
  {
    bool leaf;
    std::vector<unsigned> branch_addresses;
    std::vector<block_tree_nodet> branch;
    block_tree_nodet():leaf(false) {}
    explicit block_tree_nodet(bool l):leaf(l) {}
    static block_tree_nodet get_leaf() { return block_tree_nodet(true); }
  };

  static void replace_goto_target(
    codet &repl,
    const irep_idt &old_label,
    const irep_idt &new_label);

  code_blockt &get_block_for_pcrange(
    block_tree_nodet &tree,
    code_blockt &this_block,
    unsigned address_start,
    unsigned address_limit,
    unsigned next_block_start_address);

  code_blockt &get_or_create_block_for_pcrange(
    block_tree_nodet &tree,
    code_blockt &this_block,
    unsigned address_start,
    unsigned address_limit,
    unsigned next_block_start_address,
    const address_mapt &amap,
    bool allow_merge=true);

  optionalt<symbolt> get_lambda_method_symbol(
    const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
    const size_t &index);

  // conversion
  void convert(const symbolt &class_symbol, const methodt &);

  codet convert_instructions(
    const methodt &,
    const code_typet &,
    const irep_idt &,
    const java_class_typet::java_lambda_method_handlest &);

  const bytecode_infot &get_bytecode_info(const irep_idt &statement);

  codet get_clinit_call(const irep_idt &classname);

  bool is_method_inherited(
    const irep_idt &classname,
    const irep_idt &methodid) const;

  irep_idt get_static_field(
    const irep_idt &class_identifier, const irep_idt &component_name) const;

  enum class bytecode_write_typet { VARIABLE, ARRAY_REF, STATIC_FIELD, FIELD};
  void save_stack_entries(
    const std::string &,
    const typet &,
    code_blockt &,
    const bytecode_write_typet,
    const irep_idt &);
  void create_stack_tmp_var(
    const std::string &,
    const typet &,
    code_blockt &,
    exprt &);
};

#endif