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

Module: Read goto object files.

Author: CM Wintersteiger

Date: June 2006

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

/// \file
/// Read goto object files.

#include "read_bin_goto_object.h"

#include <util/irep_serialization.h>
#include <util/message.h>
#include <util/symbol_table_base.h>

#include "goto_functions.h"
#include "write_goto_binary.h"

static void read_bin_symbol_table_object(
  std::istream &in,
  symbol_table_baset &symbol_table,
  irep_serializationt &irepconverter)
{
  const std::size_t count = irepconverter.read_gb_word(in); // # of symbols

  for(std::size_t i=0; i<count; i++)
  {
    symbolt sym;

    sym.type = static_cast<const typet &>(irepconverter.reference_convert(in));
    sym.value = static_cast<const exprt &>(irepconverter.reference_convert(in));
    sym.location = static_cast<const source_locationt &>(
      irepconverter.reference_convert(in));

    sym.name = irepconverter.read_string_ref(in);
    sym.module = irepconverter.read_string_ref(in);
    sym.base_name = irepconverter.read_string_ref(in);
    sym.mode = irepconverter.read_string_ref(in);
    sym.pretty_name = irepconverter.read_string_ref(in);

    // obsolete: symordering
    irepconverter.read_gb_word(in);

    std::size_t flags=irepconverter.read_gb_word(in);

    sym.is_weak = (flags &(1 << 16))!=0;
    sym.is_type = (flags &(1 << 15))!=0;
    sym.is_property = (flags &(1 << 14))!=0;
    sym.is_macro = (flags &(1 << 13))!=0;
    sym.is_exported = (flags &(1 << 12))!=0;
    sym.is_input = (flags &(1 << 11))!=0;
    sym.is_output = (flags &(1 << 10))!=0;
    sym.is_state_var = (flags &(1 << 9))!=0;
    sym.is_parameter = (flags &(1 << 8))!=0;
    sym.is_auxiliary = (flags &(1 << 7))!=0;
    // sym.binding = (flags &(1 << 6))!=0;
    sym.is_lvalue = (flags &(1 << 5))!=0;
    sym.is_static_lifetime = (flags &(1 << 4))!=0;
    sym.is_thread_local = (flags &(1 << 3))!=0;
    sym.is_file_local = (flags &(1 << 2))!=0;
    sym.is_extern = (flags &(1 << 1))!=0;
    sym.is_volatile = (flags &1)!=0;

    symbol_table.add(sym);
  }
}

/// The serialised form of the goto-model currently includes the parameter
/// identifiers in the symbol table attached to the types of function symbols.
/// However it is not included in the goto functions. Therefore this function is
/// needed to copy the parameter identifiers from the symbol table to the
/// functions.
static void copy_parameter_identifiers(
  const symbol_table_baset &symbol_table,
  goto_functionst &functions)
{
  for(const auto &name_symbol : symbol_table)
  {
    const auto &symbol = name_symbol.second;
    if(symbol.is_type)
      continue;

    const auto code_type = type_try_dynamic_cast<code_typet>(symbol.type);
    if(!code_type)
      continue;

    // Makes sure there is an empty function for every function symbol.
    auto emplaced =
      functions.function_map.emplace(symbol.name, goto_functiont());
    emplaced.first->second.set_parameter_identifiers(*code_type);
  }
}

static void read_bin_functions_object(
  std::istream &in,
  goto_functionst &functions,
  irep_serializationt &irepconverter)
{
  const std::size_t count = irepconverter.read_gb_word(in); // # of functions

  for(std::size_t fct_index = 0; fct_index < count; ++fct_index)
  {
    irep_idt fname=irepconverter.read_gb_string(in);
    goto_functionst::goto_functiont &f = functions.function_map[fname];

    typedef std::map<
      goto_programt::targett,
      std::list<unsigned>,
      goto_programt::target_less_than>
      target_mapt;
    target_mapt target_map;
    typedef std::map<unsigned, goto_programt::targett> rev_target_mapt;
    rev_target_mapt rev_target_map;

    bool hidden=false;

    std::size_t ins_count = irepconverter.read_gb_word(in); // # of instructions
    for(std::size_t ins_index = 0; ins_index < ins_count; ++ins_index)
    {
      goto_programt::targett itarget = f.body.add_instruction();

      // take copies as references into irepconverter are not stable
      codet code =
        static_cast<const codet &>(irepconverter.reference_convert(in));
      source_locationt source_location = static_cast<const source_locationt &>(
        irepconverter.reference_convert(in));
      goto_program_instruction_typet instruction_type =
        (goto_program_instruction_typet)irepconverter.read_gb_word(in);
      exprt guard =
        static_cast<const exprt &>(irepconverter.reference_convert(in));

      goto_programt::instructiont instruction{
        code, source_location, instruction_type, guard, {}};

      instruction.target_number = irepconverter.read_gb_word(in);
      if(instruction.is_target() &&
         rev_target_map.insert(
           rev_target_map.end(),
           std::make_pair(instruction.target_number, itarget))->second!=itarget)
        UNREACHABLE;

      std::size_t t_count = irepconverter.read_gb_word(in); // # of targets
      for(std::size_t i=0; i<t_count; i++)
        // just save the target numbers
        target_map[itarget].push_back(irepconverter.read_gb_word(in));

      std::size_t l_count = irepconverter.read_gb_word(in); // # of labels

      for(std::size_t i=0; i<l_count; i++)
      {
        irep_idt label=irepconverter.read_string_ref(in);
        instruction.labels.push_back(label);
        if(label == CPROVER_PREFIX "HIDE")
          hidden=true;
        // The above info is also held in the goto_functiont object, and could
        // be stored in the binary.
      }

      itarget->swap(instruction);
    }

    // Resolve targets
    for(target_mapt::iterator tit = target_map.begin();
        tit!=target_map.end();
        tit++)
    {
      goto_programt::targett ins = tit->first;

      for(std::list<unsigned>::iterator nit = tit->second.begin();
          nit!=tit->second.end();
          nit++)
      {
        unsigned n=*nit;
        rev_target_mapt::const_iterator entry=rev_target_map.find(n);
        INVARIANT(
          entry != rev_target_map.end(),
          "something from the target map should also be in the reverse target "
          "map");
        ins->targets.push_back(entry->second);
      }
    }

    f.body.update();

    if(hidden)
      f.make_hidden();
  }

  functions.compute_location_numbers();
}

/// read goto binary format
/// \par parameters: input stream, symbol_table, functions
static void read_bin_goto_object(
  std::istream &in,
  symbol_table_baset &symbol_table,
  goto_functionst &functions,
  irep_serializationt &irepconverter)
{
  read_bin_symbol_table_object(in, symbol_table, irepconverter);
  copy_parameter_identifiers(symbol_table, functions);
  read_bin_functions_object(in, functions, irepconverter);
}

/// reads a goto binary file back into a symbol and a function table
/// \par parameters: input stream, symbol table, functions
/// \return true on error, false otherwise
bool read_bin_goto_object(
  std::istream &in,
  const std::string &filename,
  symbol_table_baset &symbol_table,
  goto_functionst &functions,
  message_handlert &message_handler)
{
  messaget message(message_handler);

  char hdr[4];
  hdr[0] = static_cast<char>(in.get());
  hdr[1] = static_cast<char>(in.get());
  hdr[2] = static_cast<char>(in.get());

  if(hdr[0] == 'G' && hdr[1] == 'B' && hdr[2] == 'F')
  {
    // OK!
  }
  else
  {
    hdr[3] = static_cast<char>(in.get());
    if(hdr[0] == 0x7f && hdr[1] == 'G' && hdr[2] == 'B' && hdr[3] == 'F')
    {
      // OK!
    }
    else if(hdr[0] == 0x7f && hdr[1] == 'E' && hdr[2] == 'L' && hdr[3] == 'F')
    {
      if(!filename.empty())
        message.error() << "Sorry, but I can't read ELF binary '" << filename
                        << "'" << messaget::eom;
      else
        message.error() << "Sorry, but I can't read ELF binaries"
                        << messaget::eom;

      return true;
    }
    else
    {
      message.error() << "'" << filename << "' is not a goto-binary"
                      << messaget::eom;
      return true;
    }
  }

  irep_serializationt::ireps_containert ic;
  irep_serializationt irepconverter(ic);

  const std::size_t version = irepconverter.read_gb_word(in);

  if(version < GOTO_BINARY_VERSION)
  {
    message.error() << "The input was compiled with an old version of "
                       "goto-cc; please recompile"
                    << messaget::eom;
    return true;
  }
  else if(version == GOTO_BINARY_VERSION)
  {
    read_bin_goto_object(in, symbol_table, functions, irepconverter);
    return false;
  }
  else
  {
    message.error() << "The input was compiled with an unsupported version of "
                       "goto-cc; please recompile"
                    << messaget::eom;
    return true;
  }
}