load_java_class.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Unit test utilities
 
Author: Diffblue Ltd.
 
\*******************************************************************/
 
#include "load_java_class.h"
 
#include <iostream>
#include <testing-utils/free_form_cmdline.h>
#include <testing-utils/message.h>
#include <testing-utils/use_catch.h>
 
#include <util/config.h>
#include <util/options.h>
#include <util/suffix.h>
 
#include <java_bytecode/lazy_goto_model.h>
 
#include <java_bytecode/java_bytecode_language.h>
#include <util/file_util.h>
 
symbol_tablet load_java_class_lazy(
  const std::string &java_class_name,
  const std::string &class_path,
  const std::string &main)
{
  std::unique_ptr<languaget> lang = new_java_bytecode_language();
 
  return load_java_class(java_class_name, class_path, main, std::move(lang));
}
 
symbol_tablet load_java_class(
  const std::string &java_class_name,
  const std::string &class_path,
  const std::string &main)
{
  return load_goto_model_from_java_class(java_class_name, class_path, main)
    .get_symbol_table();
}
 
symbol_tablet load_java_class(
  const std::string &java_class_name,
  const std::string &class_path,
  const std::string &main,
  std::unique_ptr<languaget> &&java_lang,
  const cmdlinet &command_line)
{
  return load_goto_model_from_java_class(
           java_class_name,
           class_path,
           main,
           std::move(java_lang),
           command_line)
    .get_symbol_table();
}
 
goto_modelt load_goto_model_from_java_class(
  const std::string &java_class_name,
  const std::string &class_path,
  const std::string &main,
  std::unique_ptr<languaget> &&java_lang,
  const cmdlinet &command_line)
{
  // We expect the name of the class without the .class suffix to allow us to
  // check it
  PRECONDITION(!has_suffix(java_class_name, ".class"));
  std::string filename=java_class_name + ".class";
 
  // Construct a lazy_goto_modelt
  lazy_goto_modelt lazy_goto_model(
    [](goto_model_functiont &, const abstract_goto_modelt &) {},
    [](goto_modelt &) { return false; },
    [](const irep_idt &) { return false; },
    [](const irep_idt &, symbol_table_baset &, goto_functiont &, bool) {
      return false;
    },
    null_message_handler);
 
  // Configure the path loading
  config.java.classpath.clear();
  config.java.classpath.push_back(class_path);
  config.main = main;
  config.java.main_class = java_class_name;
 
  // Add the language to the model
  language_filet &lf=lazy_goto_model.add_language_file(filename);
  lf.language=std::move(java_lang);
  languaget &language=*lf.language;
 
  std::istringstream java_code_stream("ignored");
 
  optionst options;
  parse_java_language_options(command_line, options);
 
  // Configure the language, load the class files
  language.set_message_handler(null_message_handler);
  language.set_language_options(options);
  language.parse(java_code_stream, filename);
  language.typecheck(lazy_goto_model.symbol_table, "");
  language.generate_support_functions(lazy_goto_model.symbol_table);
  language.final(lazy_goto_model.symbol_table);
 
  lazy_goto_model.load_all_functions();
 
  std::unique_ptr<goto_modelt> maybe_goto_model=
    lazy_goto_modelt::process_whole_model_and_freeze(
      std::move(lazy_goto_model));
  INVARIANT(maybe_goto_model, "Freezing lazy_goto_model failed");
 
  // Verify that the class was loaded
  const std::string class_symbol_name="java::"+java_class_name;
  REQUIRE(maybe_goto_model->symbol_table.has_symbol(class_symbol_name));
  const symbolt &class_symbol=
    *maybe_goto_model->symbol_table.lookup(class_symbol_name);
  REQUIRE(class_symbol.is_type);
  const typet &class_type=class_symbol.type;
  REQUIRE(class_type.id()==ID_struct);
 
  // Log the working directory to help people identify the common error
  // of wrong working directory (should be the `unit` directory when running
  // the unit tests).
  std::string path = get_current_working_directory();
  INFO("Working directory: " << path);
 
  // if this fails it indicates the class was not loaded
  // Check your working directory and the class path is correctly configured
  // as this often indicates that one of these is wrong.
  REQUIRE_FALSE(to_java_class_type(class_type).get_is_stub());
  return std::move(*maybe_goto_model);
}
 
symbol_tablet load_java_class(
  const std::string &java_class_name,
  const std::string &class_path,
  const std::string &main,
  std::unique_ptr<languaget> &&java_lang)
{
  free_form_cmdlinet command_line;
  command_line.add_flag("no-lazy-methods");
  return load_java_class(
    java_class_name, class_path, main, std::move(java_lang), command_line);
}
 
goto_modelt load_goto_model_from_java_class(
  const std::string &java_class_name,
  const std::string &class_path,
  const std::vector<std::string> &command_line_flags,
  const std::unordered_map<std::string, std::string> &command_line_options,
  const std::string &main)
{
  free_form_cmdlinet command_line;
  for(const auto &flag : command_line_flags)
    command_line.add_flag(flag);
  for(const auto &option : command_line_options)
    command_line.add_option(option.first, option.second);
 
  std::unique_ptr<languaget> lang = new_java_bytecode_language();
 
  return load_goto_model_from_java_class(
    java_class_name, class_path, main, std::move(lang), command_line);
}
 
goto_modelt load_goto_model_from_java_class(
  const std::string &java_class_name,
  const std::string &class_path,
  const std::string &main)
{
  return load_goto_model_from_java_class(
    java_class_name, class_path, {"no-lazy-methods"}, {}, main);
}