symbol_table_base.h

Go to the documentation of this file.

 
 
#ifndef CPROVER_UTIL_SYMBOL_TABLE_BASE_H
#define CPROVER_UTIL_SYMBOL_TABLE_BASE_H
 
#include "symbol.h" // IWYU pragma: keep
 
#include <list>
#include <map>
#include <unordered_map>
 
typedef std::multimap<irep_idt, irep_idt> symbol_base_mapt;
typedef std::multimap<irep_idt, irep_idt> symbol_module_mapt;
 
class symbol_tablet;
 
class symbol_table_baset
{
public:
  typedef std::unordered_map<irep_idt, symbolt> symbolst;
 
public:
  const symbolst &symbols;
  const symbol_base_mapt &symbol_base_map;
  const symbol_module_mapt &symbol_module_map;
 
public:
  symbol_table_baset(
    const symbolst &symbols,
    const symbol_base_mapt &symbol_base_map,
    const symbol_module_mapt &symbol_module_map)
    : symbols(symbols),
      symbol_base_map(symbol_base_map),
      symbol_module_map(symbol_module_map)
  {
  }
 
  symbol_table_baset(const symbol_table_baset &other) = delete;
  symbol_table_baset &operator=(const symbol_table_baset &other) = delete;
 
  virtual ~symbol_table_baset();
 
  std::size_t
  next_unused_suffix(const std::string &prefix, std::size_t start_number) const
  {
    while(this->symbols.find(prefix + std::to_string(start_number)) !=
          symbols.end())
      ++start_number;
 
    return start_number;
  }
 
  virtual std::size_t next_unused_suffix(const std::string &prefix) const
  {
    return next_unused_suffix(prefix, 0);
  }
 
  operator const symbol_tablet &() const
  {
    return get_symbol_table();
  }
  virtual const symbol_tablet &get_symbol_table() const = 0;
 
  bool has_symbol(const irep_idt &name) const
  {
    return symbols.find(name) != symbols.end();
  }
 
  const symbolt *lookup(const irep_idt &name) const
  {
    symbolst::const_iterator it = symbols.find(name);
    return it != symbols.end() ? &it->second : nullptr;
  }
 
  const symbolt &lookup_ref(const irep_idt &name) const
  {
    const symbolt *const symbol = lookup(name);
    INVARIANT(
      symbol, "`" + id2string(name) + "' must exist in the symbol table.");
    return *symbol;
  }
 
  std::list<symbolst::const_iterator>
  match_name_or_base_name(const irep_idt &id) const
  {
    std::list<symbolst::const_iterator> results;
 
    auto name_it = symbols.find(id);
    if(name_it != symbols.end())
      results.push_back(name_it);
 
    auto base_name_it_pair = symbol_base_map.equal_range(id);
    for(auto base_name_it = base_name_it_pair.first;
        base_name_it != base_name_it_pair.second;
        ++base_name_it)
    {
      name_it = symbols.find(base_name_it->second);
      CHECK_RETURN(name_it != symbols.end());
      // don't add entries where name and base name match as this amounts to the
      // case already covered above
      if(base_name_it->first != base_name_it->second)
        results.push_back(name_it);
    }
 
    return results;
  }
 
  virtual symbolt *get_writeable(const irep_idt &name) = 0;
 
  symbolt &get_writeable_ref(const irep_idt &name)
  {
    symbolt *symbol = get_writeable(name);
    if(symbol == nullptr)
      throw std::out_of_range("name not found in symbol_table");
    return *symbol;
  }
 
  bool add(const symbolt &symbol);
  virtual std::pair<symbolt &, bool> insert(symbolt symbol) = 0;
  virtual bool move(symbolt &symbol, symbolt *&new_symbol) = 0;
 
  bool remove(const irep_idt &name);
  virtual void erase(const symbolst::const_iterator &entry) = 0;
  virtual void clear() = 0;
 
  void show(std::ostream &out) const;
 
  std::vector<irep_idt> sorted_symbol_names() const;
 
  class iteratort
  {
  private:
    symbolst::iterator it;
    std::function<void(const irep_idt &id)> on_get_writeable;
 
  public:
    explicit iteratort(symbolst::iterator it) : it(std::move(it))
    {
    }
 
    iteratort(
        const iteratort &it,
        std::function<void(const irep_idt &id)> on_get_writeable)
      : it(it.it), on_get_writeable(std::move(on_get_writeable))
    {
    }
 
    operator symbolst::const_iterator() const
    {
      return symbolst::const_iterator{it};
    }
 
    // The following typedefs are NOLINT as they are needed by the STL
    typedef symbolst::iterator::difference_type difference_type;     // NOLINT
    typedef symbolst::const_iterator::value_type value_type;         // NOLINT
    typedef symbolst::const_iterator::pointer pointer;               // NOLINT
    typedef symbolst::const_iterator::reference reference;           // NOLINT
    typedef symbolst::iterator::iterator_category iterator_category; // NOLINT
 
    bool operator!=(const iteratort &other) const
    {
      return it != other.it;
    }
 
    bool operator==(const iteratort &other) const
    {
      return it == other.it;
    }
 
    iteratort &operator++()
    {
      ++it;
      return *this;
    }
 
    iteratort operator++(int)
    {
      iteratort copy(*this);
      this->operator++();
      return copy;
    }
 
    reference operator*() const
    {
      return *it;
    }
 
    pointer operator->() const
    {
      return &**this;
    }
 
    symbolt &get_writeable_symbol()
    {
      if(on_get_writeable)
        on_get_writeable((*this)->first);
      return it->second;
    }
  };
 
  virtual iteratort begin() = 0;
  virtual iteratort end() = 0;
 
  using const_iteratort = symbolst::const_iterator;
 
  virtual const_iteratort begin() const;
  virtual const_iteratort end() const;
 
  virtual void
  validate(const validation_modet vm = validation_modet::INVARIANT) const = 0;
};
 
std::ostream &
operator<<(std::ostream &out, const symbol_table_baset &symbol_table);
 
#endif // CPROVER_UTIL_SYMBOL_TABLE_BASE_H