symbol.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
#include "symbol.h"
 
#include <ostream>
 
#include "source_location.h"
#include "std_expr.h"
#include "suffix.h"
 
void symbolt::show(std::ostream &out) const
{
  out << "  " << name << '\n';
  out << "    type:  " << type.pretty(4) << '\n'
      << "    value: " << value.pretty(4) << '\n';
 
  out << "  flags:";
  if(is_lvalue)
    out << " lvalue";
  if(is_static_lifetime)
    out << " static_lifetime";
  if(is_thread_local)
    out << " thread_local";
  if(is_file_local)
    out << " file_local";
  if(is_type)
    out << " type";
  if(is_extern)
    out << " extern";
  if(is_input)
    out << " input";
  if(is_output)
    out << " output";
  if(is_macro)
    out << " macro";
  if(is_parameter)
    out << " parameter";
  if(is_auxiliary)
    out << " auxiliary";
  if(is_weak)
    out << " weak";
  if(is_property)
    out << " property";
  if(is_state_var)
    out << " state_var";
  if(is_exported)
    out << " exported";
  if(is_volatile)
    out << " volatile";
  if(!mode.empty())
    out << " mode=" << mode;
  if(!base_name.empty())
    out << " base_name=" << base_name;
  if(!module.empty())
    out << " module=" << module;
  if(!pretty_name.empty())
    out << " pretty_name=" << pretty_name;
  out << '\n';
  out << "  location: " << location << '\n';
 
  out << '\n';
}
 
std::ostream &operator<<(std::ostream &out,
                         const symbolt &symbol)
{
  symbol.show(out);
  return out;
}
 
void symbolt::swap(symbolt &b)
{
  #define SYM_SWAP1(x) x.swap(b.x)
 
  SYM_SWAP1(type);
  SYM_SWAP1(value);
  SYM_SWAP1(name);
  SYM_SWAP1(pretty_name);
  SYM_SWAP1(module);
  SYM_SWAP1(base_name);
  SYM_SWAP1(mode);
  SYM_SWAP1(location);
 
  #define SYM_SWAP2(x) std::swap(x, b.x)
 
  SYM_SWAP2(is_type);
  SYM_SWAP2(is_macro);
  SYM_SWAP2(is_exported);
  SYM_SWAP2(is_input);
  SYM_SWAP2(is_output);
  SYM_SWAP2(is_state_var);
  SYM_SWAP2(is_property);
  SYM_SWAP2(is_parameter);
  SYM_SWAP2(is_auxiliary);
  SYM_SWAP2(is_weak);
  SYM_SWAP2(is_lvalue);
  SYM_SWAP2(is_static_lifetime);
  SYM_SWAP2(is_thread_local);
  SYM_SWAP2(is_file_local);
  SYM_SWAP2(is_extern);
  SYM_SWAP2(is_volatile);
}
 
symbol_exprt symbolt::symbol_expr() const
{
  return symbol_exprt(name, type).with_source_location(location);
}
 
bool symbolt::is_well_formed() const
{
  // Well-formedness criterion number 1 is for a symbol
  // to have a non-empty mode (see #1880)
  if(mode.empty())
  {
    return false;
  }
 
  // Well-formedness criterion number 2 is for a symbol
  // to have it's base name as a suffix to it's more
  // general name.
 
  // Exception: Java symbols' base names do not have type signatures
  // (for example, they can have name "someclass.method:(II)V" and base name
  // "method")
  if(
    !has_suffix(id2string(name), id2string(base_name)) && mode != ID_java &&
    mode != ID_cpp)
  {
    bool criterion_must_hold = true;
 
    // There are some special cases where this criterion doesn't hold, check
    // to see if we have one of those cases
 
    if(is_type)
    {
      // Typedefs
      if(
        type.find(ID_C_typedef).is_not_nil() &&
        type.find(ID_C_typedef).id() == base_name)
      {
        criterion_must_hold = false;
      }
 
      // Tag types
      if(type.find(ID_tag).is_not_nil() && type.find(ID_tag).id() == base_name)
      {
        criterion_must_hold = false;
      }
    }
 
    // Linker renaming may have added $linkN suffixes to the name, and other
    // suffixes such as #return_value may have then be subsequently added.
    // Strip out the first $linkN substring and then see if the criterion holds
    const auto &unstripped_name = id2string(name);
    const size_t dollar_link_start_pos = unstripped_name.find("$link");
 
    if(dollar_link_start_pos != std::string::npos)
    {
      size_t dollar_link_end_pos = dollar_link_start_pos + 5;
      while(isdigit(unstripped_name[dollar_link_end_pos]))
      {
        ++dollar_link_end_pos;
      }
 
      const auto stripped_name =
        unstripped_name.substr(0, dollar_link_start_pos) +
        unstripped_name.substr(dollar_link_end_pos, std::string::npos);
 
      if(has_suffix(stripped_name, id2string(base_name)))
        criterion_must_hold = false;
    }
 
    if(criterion_must_hold)
    {
      // For all other cases this criterion should hold
      return false;
    }
  }
 
  return true;
}
 
bool symbolt::operator==(const symbolt &other) const
{
  // clang-format off
  return
    type == other.type &&
    value == other.value &&
    location == other.location &&
    name == other.name &&
    module == other.module &&
    base_name == other.base_name &&
    mode == other.mode &&
    pretty_name == other.pretty_name &&
    is_type == other.is_type &&
    is_macro == other.is_macro &&
    is_exported == other.is_exported &&
    is_input == other.is_input &&
    is_output == other.is_output &&
    is_state_var == other.is_state_var &&
    is_property == other.is_property &&
    is_parameter == other.is_parameter &&
    is_auxiliary == other.is_auxiliary &&
    is_weak == other.is_weak &&
    is_lvalue == other.is_lvalue &&
    is_static_lifetime == other.is_static_lifetime &&
    is_thread_local == other.is_thread_local &&
    is_file_local == other.is_file_local &&
    is_extern == other.is_extern &&
    is_volatile == other.is_volatile;
  // clang-format on
}
 
bool symbolt::operator!=(const symbolt &other) const
{
  return !(*this == other);
}