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

Module: Unit test utilities

Author: Diffblue Ltd.

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

#include "load_java_class.h"

#include <util/config.h>
#include <util/options.h>
#include <util/suffix.h>

#include <java_bytecode/java_bytecode_language.h>
#include <java_bytecode/lazy_goto_model.h>
#include <testing-utils/free_form_cmdline.h>
#include <testing-utils/message.h>
#include <testing-utils/use_catch.h>

#include <filesystem>
#include <iostream>

/// Go through the process of loading, type-checking and finalising loading a
/// specific class file to build the symbol table. The functions are converted
/// using ci_lazy_methods (equivalent to passing --lazy-methods to JBMC)
/// \param java_class_name: The name of the class file to load. It should not
///   include the .class extension.
/// \param class_path: The path to load the class from. Should be relative to
///   the unit directory.
/// \param main: The name of the main function or "" to use the default
///   behaviour to find a main function.
/// \return The symbol table that is generated by parsing this file.
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));
}

/// Returns the symbol table from
/// \ref load_goto_model_from_java_class(const std::string &java_class_name, const std::string &class_path, const std::string &main) // NOLINT
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();
}

/// Returns the symbol table from \ref load_goto_model_from_java_class
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();
}

/// Go through the process of loading, type-checking and finalising a
/// specific class file to build a goto model from it.
/// \param java_class_name: The name of the class file to load. It should not
///   include the .class extension.
/// \param class_path: The path to load the class from. Should be relative to
///   the unit directory.
/// \param main: The name of the main function or "" to use the default
///   behaviour to find a main function.
/// \param java_lang: The language implementation to use for the loading,
///   which will be destroyed by this function.
/// \param command_line: The command line used to configure the provided
///   language
/// \return The goto model containing both the functions and the symbol table
///   from loading this class.
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);
  java_bytecode_languaget &language =
    dynamic_cast<java_bytecode_languaget &>(*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_language_options(options, null_message_handler);
  language.parse(java_code_stream, filename, null_message_handler);
  language.typecheck(lazy_goto_model.symbol_table, "", null_message_handler);
  language.generate_support_functions(
    lazy_goto_model.symbol_table, null_message_handler);
  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 = std::filesystem::current_path().string();
  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);
}

/// Returns the symbol table from \ref load_goto_model_from_java_class
/// with the command line set to be disabling lazy loading and string
/// refinement
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);
}

/// See \ref load_goto_model_from_java_class
/// With the command line configured to disable lazy loading and string
/// refinement and the language set to be the default java_bytecode language
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);
}