java_bytecode_language.cpp

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

Module:

Author: Daniel Kroening, kroening@kroening.com

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

#include <string>

#include <util/symbol_table.h>
#include <util/suffix.h>
#include <util/config.h>
#include <util/cmdline.h>
#include <util/string2int.h>
#include <json/json_parser.h>

#include <goto-programs/class_hierarchy.h>

#include "java_bytecode_language.h"
#include "java_bytecode_convert_class.h"
#include "java_bytecode_convert_method.h"
#include "java_bytecode_internal_additions.h"
#include "java_bytecode_typecheck.h"
#include "java_entry_point.h"
#include "java_bytecode_parser.h"
#include "java_class_loader.h"

#include "expr2java.h"

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

Function: java_bytecode_languaget::get_language_options

  Inputs: Command-line options

 Outputs: None

 Purpose: Consume options that are java bytecode specific.

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

void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
{
  disable_runtime_checks=cmd.isset("disable-runtime-check");
  assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null");
  string_refinement_enabled=cmd.isset("refine-strings");
  if(cmd.isset("java-max-input-array-length"))
    max_nondet_array_length=
      std::stoi(cmd.get_value("java-max-input-array-length"));
  if(cmd.isset("java-max-vla-length"))
    max_user_array_length=std::stoi(cmd.get_value("java-max-vla-length"));
  if(cmd.isset("lazy-methods-context-sensitive"))
    lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_SENSITIVE;
  else if(cmd.isset("lazy-methods"))
    lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_INSENSITIVE;
  else
    lazy_methods_mode=LAZY_METHODS_MODE_EAGER;

  if(cmd.isset("java-cp-include-files"))
  {
    java_cp_include_files=cmd.get_value("java-cp-include-files");
    // load file list from JSON file
    if(java_cp_include_files[0]=='@')
    {
      jsont json_cp_config;
      if(parse_json(
           java_cp_include_files.substr(1),
           get_message_handler(),
           json_cp_config))
        throw "cannot read JSON input configuration for JAR loading";

      if(!json_cp_config.is_object())
        throw "the JSON file has a wrong format";
      jsont include_files=json_cp_config["jar"];
      if(!include_files.is_array())
         throw "the JSON file has a wrong format";

      // add jars from JSON config file to classpath
      for(const jsont &file_entry : include_files.array)
      {
        assert(file_entry.is_string() && has_suffix(file_entry.value, ".jar"));
        config.java.classpath.push_back(file_entry.value);
      }
    }
  }
  else
    java_cp_include_files=".*";
}

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

Function: java_bytecode_languaget::extensions

  Inputs:

 Outputs:

 Purpose:

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

std::set<std::string> java_bytecode_languaget::extensions() const
{
  return { "class", "jar" };
}

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

Function: java_bytecode_languaget::modules_provided

  Inputs:

 Outputs:

 Purpose:

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

void java_bytecode_languaget::modules_provided(std::set<std::string> &modules)
{
  // modules.insert(translation_unit(parse_path));
}

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

Function: java_bytecode_languaget::preprocess

  Inputs:

 Outputs:

 Purpose: ANSI-C preprocessing

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

bool java_bytecode_languaget::preprocess(
  std::istream &instream,
  const std::string &path,
  std::ostream &outstream)
{
  // there is no preprocessing!
  return true;
}

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

Function: java_bytecode_languaget::parse

  Inputs:

 Outputs:

 Purpose:

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

bool java_bytecode_languaget::parse(
  std::istream &instream,
  const std::string &path)
{
  java_class_loader.set_message_handler(get_message_handler());
  java_class_loader.set_java_cp_include_files(java_cp_include_files);

  // look at extension
  if(has_suffix(path, ".class"))
  {
    // override main_class
    main_class=java_class_loadert::file_to_class_name(path);
  }
  else if(has_suffix(path, ".jar"))
  {
    if(config.java.main_class.empty())
    {
      // Does it have a main class set in the manifest?
      jar_filet::manifestt manifest=
        java_class_loader.jar_pool(path).get_manifest();
      std::string manifest_main_class=manifest["Main-Class"];

      if(manifest_main_class!="")
        main_class=manifest_main_class;
    }
    else
      main_class=config.java.main_class;

    // Do we have one now?
    if(main_class.empty())
    {
      status() << "JAR file without entry point: loading it all" << eom;
      java_class_loader.load_entire_jar(path);
      for(const auto &kv : java_class_loader.jar_map.at(path).entries)
        main_jar_classes.push_back(kv.first);
    }
    else
      java_class_loader.add_jar_file(path);
  }
  else
    assert(false);

  if(!main_class.empty())
  {
    status() << "Java main class: " << main_class << eom;
    java_class_loader(main_class);
  }

  return false;
}

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

Function: get_virtual_method_target

  Inputs: `needed_classes`: set of classes that can be instantiated.
            Any potential callee not in this set will be ignored.
          `call_basename`: unqualified function name with type
            signature (e.g. "f:(I)")
          `classname`: class name that may define or override a
            function named `call_basename`.
          `symbol_table`: global symtab

 Outputs: Returns the fully qualified name of `classname`'s definition
          of `call_basename` if found and `classname` is present in
          `needed_classes`, or irep_idt() otherwise.

 Purpose: Find a virtual callee, if one is defined and the callee type
          is known to exist.

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

static irep_idt get_virtual_method_target(
  const std::set<irep_idt> &needed_classes,
  const irep_idt &call_basename,
  const irep_idt &classname,
  const symbol_tablet &symbol_table)
{
  // Program-wide, is this class ever instantiated?
  if(!needed_classes.count(classname))
    return irep_idt();
  auto methodid=id2string(classname)+"."+id2string(call_basename);
  if(symbol_table.has_symbol(methodid))
    return methodid;
  else
    return irep_idt();
}

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

Function: get_virtual_method_target

  Inputs: `c`: function call whose potential target functions should
            be determined.
          `needed_classes`: set of classes that can be instantiated.
            Any potential callee not in this set will be ignored.
          `symbol_table`: global symtab
          `class_hierarchy`: global class hierarchy

 Outputs: Populates `needed_methods` with all possible `c` callees,
          taking `needed_classes` into account (virtual function
          overrides defined on classes that are not 'needed' are
          ignored)

 Purpose: Find possible callees, excluding types that are not known
          to be instantiated.

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

static void get_virtual_method_targets(
  const code_function_callt &c,
  const std::set<irep_idt> &needed_classes,
  std::vector<irep_idt> &needed_methods,
  symbol_tablet &symbol_table,
  const class_hierarchyt &class_hierarchy)
{
  const auto &called_function=c.function();
  assert(called_function.id()==ID_virtual_function);

  const auto &call_class=called_function.get(ID_C_class);
  assert(call_class!=irep_idt());
  const auto &call_basename=called_function.get(ID_component_name);
  assert(call_basename!=irep_idt());

  auto old_size=needed_methods.size();

  auto child_classes=class_hierarchy.get_children_trans(call_class);
  for(const auto &child_class : child_classes)
  {
    auto child_method=
      get_virtual_method_target(
        needed_classes,
        call_basename,
        child_class,
        symbol_table);
    if(child_method!=irep_idt())
      needed_methods.push_back(child_method);
  }

  irep_idt parent_class_id=call_class;
  while(1)
  {
    auto parent_method=
      get_virtual_method_target(
        needed_classes,
        call_basename,
        parent_class_id,
        symbol_table);
    if(parent_method!=irep_idt())
    {
      needed_methods.push_back(parent_method);
      break;
    }
    else
    {
      auto findit=class_hierarchy.class_map.find(parent_class_id);
      if(findit==class_hierarchy.class_map.end())
        break;
      else
      {
        const auto &entry=findit->second;
        if(entry.parents.empty())
          break;
        else
          parent_class_id=entry.parents[0];
      }
    }
  }

  if(needed_methods.size()==old_size)
  {
    // Didn't find any candidate callee. Generate a stub.
    std::string stubname=id2string(call_class)+"."+id2string(call_basename);
    symbolt symbol;
    symbol.name=stubname;
    symbol.base_name=call_basename;
    symbol.type=c.function().type();
    symbol.value.make_nil();
    symbol.mode=ID_java;
    symbol_table.add(symbol);
  }
}

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

Function: gather_virtual_callsites

  Inputs: `e`: expression tree to search

 Outputs: Populates `result` with pointers to each function call
            within e that calls a virtual function.

 Purpose: See output

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

static void gather_virtual_callsites(
  const exprt &e,
  std::vector<const code_function_callt *> &result)
{
  if(e.id()!=ID_code)
    return;
  const codet &c=to_code(e);
  if(c.get_statement()==ID_function_call &&
     to_code_function_call(c).function().id()==ID_virtual_function)
    result.push_back(&to_code_function_call(c));
  else
    forall_operands(it, e)
      gather_virtual_callsites(*it, result);
}

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

Function: gather_needed_globals

  Inputs: `e`: expression tree to search
          `symbol_table`: global symtab

 Outputs: Populates `needed` with global variable symbols referenced
          from `e` or its children.

 Purpose: See output

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

static void gather_needed_globals(
  const exprt &e,
  const symbol_tablet &symbol_table,
  symbol_tablet &needed)
{
  if(e.id()==ID_symbol)
  {
    const auto &sym=symbol_table.lookup(to_symbol_expr(e).get_identifier());
    if(sym.is_static_lifetime)
      needed.add(sym);
  }
  else
    forall_operands(opit, e)
      gather_needed_globals(*opit, symbol_table, needed);
}

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

Function: gather_field_types

  Inputs: `class_type`: root of class tree to search
          `ns`: global namespace

 Outputs: Populates `needed_classes` with all Java reference types
            reachable starting at `class_type`. For example if
            `class_type` is `symbol_typet("java::A")` and A has a B
            field, then `B` (but not `A`) will be added to
            `needed_classes`.

 Purpose: See output

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

static void gather_field_types(
  const typet &class_type,
  const namespacet &ns,
  std::set<irep_idt> &needed_classes)
{
  const auto &underlying_type=to_struct_type(ns.follow(class_type));
  for(const auto &field : underlying_type.components())
  {
    if(field.type().id()==ID_struct || field.type().id()==ID_symbol)
      gather_field_types(field.type(), ns, needed_classes);
    else if(field.type().id()==ID_pointer)
    {
      // Skip array primitive pointers, for example:
      if(field.type().subtype().id()!=ID_symbol)
        continue;
      const auto &field_classid=
        to_symbol_type(field.type().subtype()).get_identifier();
      if(needed_classes.insert(field_classid).second)
        gather_field_types(field.type().subtype(), ns, needed_classes);
    }
  }
}

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

Function: initialize_needed_classes

  Inputs: `entry_points`: list of fully-qualified function names that
            we should assume are reachable
          `ns`: global namespace
          `ch`: global class hierarchy

 Outputs: Populates `needed_classes` with all Java reference types
            whose references may be passed, directly or indirectly,
            to any of the functions in `entry_points`.

 Purpose: See output

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

static void initialize_needed_classes(
  const std::vector<irep_idt> &entry_points,
  const namespacet &ns,
  const class_hierarchyt &ch,
  std::set<irep_idt> &needed_classes)
{
  for(const auto &mname : entry_points)
  {
    const auto &symbol=ns.lookup(mname);
    const auto &mtype=to_code_type(symbol.type);
    for(const auto &param : mtype.parameters())
    {
      if(param.type().id()==ID_pointer)
      {
        const auto &param_classid=
          to_symbol_type(param.type().subtype()).get_identifier();
        std::vector<irep_idt> class_and_parents=
          ch.get_parents_trans(param_classid);
        class_and_parents.push_back(param_classid);
        for(const auto &classid : class_and_parents)
          needed_classes.insert(classid);
        gather_field_types(param.type().subtype(), ns, needed_classes);
      }
    }
  }

  // Also add classes whose instances are magically
  // created by the JVM and so won't be spotted by
  // looking for constructors and calls as usual:
  needed_classes.insert("java::java.lang.String");
  needed_classes.insert("java::java.lang.Class");
  needed_classes.insert("java::java.lang.Object");
}

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

Function: java_bytecode_languaget::typecheck

  Inputs:

 Outputs:

 Purpose:

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

bool java_bytecode_languaget::typecheck(
  symbol_tablet &symbol_table,
  const std::string &module)
{
  // first convert all
  for(java_class_loadert::class_mapt::const_iterator
      c_it=java_class_loader.class_map.begin();
      c_it!=java_class_loader.class_map.end();
      c_it++)
  {
    if(c_it->second.parsed_class.name.empty())
      continue;

    debug() << "Converting class " << c_it->first << eom;

    if(java_bytecode_convert_class(
         c_it->second,
         symbol_table,
         get_message_handler(),
         disable_runtime_checks,
         max_user_array_length,
         lazy_methods,
         lazy_methods_mode,
         string_refinement_enabled))
      return true;
  }

  // Now incrementally elaborate methods
  // that are reachable from this entry point.
  if(lazy_methods_mode==LAZY_METHODS_MODE_CONTEXT_INSENSITIVE)
  {
    // ci: context-insensitive.
    if(do_ci_lazy_method_conversion(symbol_table, lazy_methods))
      return true;
  }

  // now typecheck all
  if(java_bytecode_typecheck(
       symbol_table, get_message_handler(), string_refinement_enabled))
    return true;

  return false;
}

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

Function: java_bytecode_languaget::do_ci_lazy_method_conversion

  Inputs: `symbol_table`: global symbol table
          `lazy_methods`: map from method names to relevant symbol
                          and parsed-method objects.

 Outputs: Elaborates lazily-converted methods that may be reachable
          starting from the main entry point (usually provided with
          the --function command-line option) (side-effect on the
          symbol_table). Returns false on success.

 Purpose: Uses a simple context-insensitive ('ci') analysis to
          determine which methods may be reachable from the main
          entry point. In brief, static methods are reachable if we
          find a callsite in another reachable site, while virtual
          methods are reachable if we find a virtual callsite
          targeting a compatible type *and* a constructor callsite
          indicating an object of that type may be instantiated (or
          evidence that an object of that type exists before the
          main function is entered, such as being passed as a
          parameter).

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

bool java_bytecode_languaget::do_ci_lazy_method_conversion(
  symbol_tablet &symbol_table,
  lazy_methodst &lazy_methods)
{
  class_hierarchyt ch;
  ch(symbol_table);

  std::vector<irep_idt> method_worklist1;
  std::vector<irep_idt> method_worklist2;

  auto main_function=
    get_main_symbol(symbol_table, main_class, get_message_handler(), true);
  if(main_function.stop_convert)
  {
    // Failed, mark all functions in the given main class(es) reachable.
    std::vector<irep_idt> reachable_classes;
    if(!main_class.empty())
      reachable_classes.push_back(main_class);
    else
      reachable_classes=main_jar_classes;
    for(const auto &classname : reachable_classes)
    {
      const auto &methods=
        java_class_loader.class_map.at(classname).parsed_class.methods;
      for(const auto &method : methods)
      {
        const irep_idt methodid="java::"+id2string(classname)+"."+
          id2string(method.name)+":"+
          id2string(method.signature);
        method_worklist2.push_back(methodid);
      }
    }
  }
  else
    method_worklist2.push_back(main_function.main_function.name);

  std::set<irep_idt> needed_classes;
  initialize_needed_classes(
    method_worklist2,
    namespacet(symbol_table),
    ch,
    needed_classes);

  std::set<irep_idt> methods_already_populated;
  std::vector<const code_function_callt *> virtual_callsites;

  bool any_new_methods;
  do
  {
    any_new_methods=false;
    while(method_worklist2.size()!=0)
    {
      std::swap(method_worklist1, method_worklist2);
      for(const auto &mname : method_worklist1)
      {
        if(!methods_already_populated.insert(mname).second)
          continue;
        auto findit=lazy_methods.find(mname);
        if(findit==lazy_methods.end())
        {
          debug() << "Skip " << mname << eom;
          continue;
        }
        debug() << "CI lazy methods: elaborate " << mname << eom;
        const auto &parsed_method=findit->second;
        java_bytecode_convert_method(
          *parsed_method.first,
          *parsed_method.second,
          symbol_table,
          get_message_handler(),
          disable_runtime_checks,
          max_user_array_length,
          safe_pointer<std::vector<irep_idt> >::create_non_null(
            &method_worklist2),
          safe_pointer<std::set<irep_idt> >::create_non_null(
            &needed_classes));
        gather_virtual_callsites(
          symbol_table.lookup(mname).value,
          virtual_callsites);
        any_new_methods=true;
      }
      method_worklist1.clear();
    }

    // Given the object types we now know may be created, populate more
    // possible virtual function call targets:

    debug() << "CI lazy methods: add virtual method targets ("
            << virtual_callsites.size()
            << " callsites)"
            << eom;

    for(const auto &callsite : virtual_callsites)
    {
      // This will also create a stub if a virtual callsite has no targets.
      get_virtual_method_targets(
        *callsite,
        needed_classes,
        method_worklist2,
        symbol_table,
        ch);
    }
  }
  while(any_new_methods);

  // Remove symbols for methods that were declared but never used:
  symbol_tablet keep_symbols;

  for(const auto &sym : symbol_table.symbols)
  {
    if(sym.second.is_static_lifetime)
      continue;
    if(lazy_methods.count(sym.first) &&
       !methods_already_populated.count(sym.first))
    {
      continue;
    }
    if(sym.second.type.id()==ID_code)
      gather_needed_globals(sym.second.value, symbol_table, keep_symbols);
    keep_symbols.add(sym.second);
  }

  debug() << "CI lazy methods: removed "
          << symbol_table.symbols.size() - keep_symbols.symbols.size()
          << " unreachable methods and globals"
          << eom;

  symbol_table.swap(keep_symbols);

  return false;
}

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

Function: java_bytecode_languaget::lazy_methods_provided

  Inputs: None

 Outputs: Populates `methods` with the complete list of lazy methods
          that are available to convert (those which are valid
          parameters for `convert_lazy_method`)

 Purpose: Provide feedback to `language_filest` so that when asked
          for a lazy method, it can delegate to this instance of
          java_bytecode_languaget.

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

void java_bytecode_languaget::lazy_methods_provided(
  std::set<irep_idt> &methods) const
{
  for(const auto &kv : lazy_methods)
    methods.insert(kv.first);
}

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

Function: java_bytecode_languaget::convert_lazy_method

  Inputs: `id`: method ID to convert
          `symtab`: global symbol table

 Outputs: Amends the symbol table entry for function `id`, which
          should be a lazy method provided by this instance of
          `java_bytecode_languaget`. It should initially have a nil
          value. After this method completes, it will have a value
          representing the method body, identical to that produced
          using eager method conversion.

 Purpose: Promote a lazy-converted method (one whose type is known
          but whose body hasn't been converted) into a fully-
          elaborated one.

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

void java_bytecode_languaget::convert_lazy_method(
  const irep_idt &id,
  symbol_tablet &symtab)
{
  const auto &lazy_method_entry=lazy_methods.at(id);
  java_bytecode_convert_method(
    *lazy_method_entry.first,
    *lazy_method_entry.second,
    symtab,
    get_message_handler(),
    disable_runtime_checks,
    max_user_array_length);
}

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

Function: java_bytecode_languaget::final

  Inputs:

 Outputs:

 Purpose:

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

bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
{
  /*
  if(c_final(symbol_table, message_handler)) return true;
  */
  java_internal_additions(symbol_table);

  main_function_resultt res=
    get_main_symbol(symbol_table, main_class, get_message_handler());
  if(res.stop_convert)
    return res.error_found;

  symbolt entry=res.main_function;

  return(
    java_entry_point(
      symbol_table,
      main_class,
      get_message_handler(),
      assume_inputs_non_null,
      max_nondet_array_length));
}

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

Function: java_bytecode_languaget::show_parse

  Inputs:

 Outputs:

 Purpose:

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

void java_bytecode_languaget::show_parse(std::ostream &out)
{
  java_class_loader(main_class).output(out);
}

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

Function: new_java_bytecode_language

  Inputs:

 Outputs:

 Purpose:

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

languaget *new_java_bytecode_language()
{
  return new java_bytecode_languaget;
}

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

Function: java_bytecode_languaget::from_expr

  Inputs:

 Outputs:

 Purpose:

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

bool java_bytecode_languaget::from_expr(
  const exprt &expr,
  std::string &code,
  const namespacet &ns)
{
  code=expr2java(expr, ns);
  return false;
}

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

Function: java_bytecode_languaget::from_type

  Inputs:

 Outputs:

 Purpose:

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

bool java_bytecode_languaget::from_type(
  const typet &type,
  std::string &code,
  const namespacet &ns)
{
  code=type2java(type, ns);
  return false;
}

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

Function: java_bytecode_languaget::to_expr

  Inputs:

 Outputs:

 Purpose:

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

bool java_bytecode_languaget::to_expr(
  const std::string &code,
  const std::string &module,
  exprt &expr,
  const namespacet &ns)
{
  #if 0
  expr.make_nil();

  // no preprocessing yet...

  std::istringstream i_preprocessed(code);

  // parsing

  java_bytecode_parser.clear();
  java_bytecode_parser.filename="";
  java_bytecode_parser.in=&i_preprocessed;
  java_bytecode_parser.set_message_handler(message_handler);
  java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
  java_bytecode_parser.mode=java_bytecode_parsert::GCC;
  java_bytecode_scanner_init();

  bool result=java_bytecode_parser.parse();

  if(java_bytecode_parser.parse_tree.items.empty())
    result=true;
  else
  {
    expr=java_bytecode_parser.parse_tree.items.front().value();

    result=java_bytecode_convert(expr, "", message_handler);

    // typecheck it
    if(!result)
      result=java_bytecode_typecheck(expr, message_handler, ns);
  }

  // save some memory
  java_bytecode_parser.clear();

  return result;
  #endif

  return true; // fail for now
}

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

Function: java_bytecode_languaget::~java_bytecode_languaget

  Inputs:

 Outputs:

 Purpose:

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

java_bytecode_languaget::~java_bytecode_languaget()
{
}