java_class_loader.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
#include "java_class_loader.h"
 
#include <stack>
 
#include <util/message.h>
#include <util/suffix.h>
 
#include "java_class_loader_limit.h"
 
java_class_loadert::parse_tree_with_overlayst &java_class_loadert::
operator()(const irep_idt &class_name, message_handlert &message_handler)
{
  messaget log(message_handler);
 
  log.debug() << "Classpath:";
  for(const auto &entry : classpath_entries)
  {
    log.debug() << "\n  " << entry.path;
  }
  log.debug() << messaget::eom;
 
  std::stack<irep_idt> queue;
  // Always require java.lang.Object, as it is the base of
  // internal classes such as array types.
  queue.push("java.lang.Object");
  // java.lang.String
  queue.push("java.lang.String");
  // add java.lang.Class
  queue.push("java.lang.Class");
  // Require java.lang.Throwable as the catch-type used for
  // universal exception handlers:
  queue.push("java.lang.Throwable");
  queue.push(class_name);
 
  // Require user provided classes to be loaded even without explicit reference
  for(const auto &id : java_load_classes)
    queue.push(id);
 
  java_class_loader_limitt class_loader_limit(
    message_handler, java_cp_include_files);
 
  while(!queue.empty())
  {
    irep_idt c=queue.top();
    queue.pop();
 
    if(class_map.count(c) != 0)
      continue;
 
    log.debug() << "Reading class " << c << messaget::eom;
 
    parse_tree_with_overlayst &parse_trees =
      get_parse_tree(class_loader_limit, c, message_handler);
 
    // Add any dependencies to queue
    for(const java_bytecode_parse_treet &parse_tree : parse_trees)
      for(const irep_idt &class_ref : parse_tree.class_refs)
        queue.push(class_ref);
 
    // Add any extra dependencies provided by our caller:
    if(get_extra_class_refs)
    {
      for(const irep_idt &id : get_extra_class_refs(c))
        queue.push(id);
    }
  }
 
  return class_map.at(class_name);
}
 
static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
{
  return java_bytecode_parse_treet::find_annotation(
           c.annotations, ID_overlay_class)
    .has_value();
}
 
bool java_class_loadert::can_load_class(
  const irep_idt &class_name,
  message_handlert &message_handler)
{
  for(const auto &cp_entry : classpath_entries)
  {
    auto parse_tree = load_class(class_name, cp_entry, message_handler);
    if(parse_tree.has_value())
      return true;
  }
  return false;
}
 
java_class_loadert::parse_tree_with_overlayst &
java_class_loadert::get_parse_tree(
  java_class_loader_limitt &class_loader_limit,
  const irep_idt &class_name,
  message_handlert &message_handler)
{
  parse_tree_with_overlayst &parse_trees = class_map[class_name];
  PRECONDITION(parse_trees.empty());
 
  messaget log(message_handler);
 
  // do we refuse to load?
  if(!class_loader_limit.load_class_file(class_name_to_jar_file(class_name)))
  {
    log.debug() << "not loading " << class_name << " because of limit"
                << messaget::eom;
    parse_trees.emplace_back(class_name);
    return parse_trees;
  }
 
  // Rummage through the class path
  for(const auto &cp_entry : classpath_entries)
  {
    auto parse_tree = load_class(class_name, cp_entry, message_handler);
    if(parse_tree.has_value())
      parse_trees.emplace_back(std::move(*parse_tree));
  }
 
  auto parse_tree_it = parse_trees.begin();
  // If the first class implementation is an overlay emit a warning and
  // skip over it until we find a non-overlay class
  while(parse_tree_it != parse_trees.end())
  {
    // Skip parse trees that failed to load - though these shouldn't exist yet
    if(parse_tree_it->loading_successful)
    {
      if(!is_overlay_class(parse_tree_it->parsed_class))
      {
        // Keep the non-overlay class
        ++parse_tree_it;
        break;
      }
      log.debug() << "Skipping class " << class_name
                  << " marked with OverlayClassImplementation but found before"
                     " original definition"
                  << messaget::eom;
    }
    auto unloaded_or_overlay_out_of_order_it = parse_tree_it;
    ++parse_tree_it;
    parse_trees.erase(unloaded_or_overlay_out_of_order_it);
  }
  // Collect overlay classes
  while(parse_tree_it != parse_trees.end())
  {
    // Remove non-initial classes that aren't overlays
    if(!is_overlay_class(parse_tree_it->parsed_class))
    {
      log.debug() << "Skipping duplicate definition of class " << class_name
                  << " not marked with OverlayClassImplementation"
                  << messaget::eom;
      auto duplicate_non_overlay_it = parse_tree_it;
      ++parse_tree_it;
      parse_trees.erase(duplicate_non_overlay_it);
    }
    else
      ++parse_tree_it;
  }
  if(!parse_trees.empty())
    return parse_trees;
 
  // Not found or failed to load
  log.debug() << "failed to load class " << class_name << messaget::eom;
  parse_trees.emplace_back(class_name);
  return parse_trees;
}
 
std::vector<irep_idt> java_class_loadert::load_entire_jar(
  const std::string &jar_path,
  message_handlert &message_handler)
{
  auto classes = read_jar_file(jar_path, message_handler);
  if(!classes.has_value())
    return {};
 
  classpath_entries.push_front(
    classpath_entryt(classpath_entryt::JAR, jar_path));
 
  for(const auto &c : *classes)
    operator()(c, message_handler);
 
  classpath_entries.pop_front();
 
  return *classes;
}
 
std::optional<std::vector<irep_idt>> java_class_loadert::read_jar_file(
  const std::string &jar_path,
  message_handlert &message_handler)
{
  messaget log(message_handler);
 
  std::vector<std::string> filenames;
  try
  {
    filenames = jar_pool(jar_path).filenames();
  }
  catch(const std::runtime_error &)
  {
    log.error() << "failed to open JAR file '" << jar_path << "'"
                << messaget::eom;
    return {};
  }
  log.debug() << "Adding JAR file '" << jar_path << "'" << messaget::eom;
 
  // Create a new entry in the map and initialize using the list of file names
  // that are in jar_filet
  std::vector<irep_idt> classes;
  for(auto &file_name : filenames)
  {
    if(has_suffix(file_name, ".class"))
    {
      log.debug() << "Found class file " << file_name << " in JAR '" << jar_path
                  << "'" << messaget::eom;
      irep_idt class_name=file_to_class_name(file_name);
      classes.push_back(class_name);
    }
  }
  return classes;
}