irep.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_UTIL_IREP_H
#define CPROVER_UTIL_IREP_H
 
#include <string>
#include <vector>
 
#include "invariant.h"
#include "irep_ids.h"
 
#define SHARING
#ifndef HASH_CODE
#  define HASH_CODE 1
#endif
// use forward_list by default, unless _GLIBCXX_DEBUG is set as the debug
// overhead is noticeably higher with the regression test suite taking four
// times as long.
#if !defined(NAMED_SUB_IS_FORWARD_LIST) && !defined(_GLIBCXX_DEBUG)
#  define NAMED_SUB_IS_FORWARD_LIST 1
#endif
 
#if NAMED_SUB_IS_FORWARD_LIST
#  include "forward_list_as_map.h"
#else
#include <map>
#endif
 
#ifdef USE_DSTRING
typedef dstringt irep_idt;
// NOLINTNEXTLINE(readability/identifiers)
typedef dstring_hash irep_id_hash;
#else
#include "string_hash.h"
typedef std::string irep_idt;
// NOLINTNEXTLINE(readability/identifiers)
typedef string_hash irep_id_hash;
#endif
 
inline const std::string &id2string(const irep_idt &d)
{
  #ifdef USE_DSTRING
  return as_string(d);
  #else
  return d;
  #endif
}
 
#ifdef IREP_DEBUG
#include <iostream>
#endif
 
class irept;
const irept &get_nil_irep();
 
template <bool enabled>
struct ref_count_ift
{
};
 
template <>
struct ref_count_ift<true>
{
  unsigned ref_count = 1;
};
 
template <typename treet, typename named_subtreest, bool sharing = true>
class tree_nodet : public ref_count_ift<sharing>
{
public:
  // These are not stable.
  typedef std::vector<treet> subt;
 
  // named_subt has to provide stable references; we can
  // use std::forward_list or std::vector< unique_ptr<T> > to save
  // memory and increase efficiency.
  using named_subt = named_subtreest;
 
  friend treet;
 
  irep_idt data;
 
  named_subt named_sub;
  subt sub;
 
#if HASH_CODE
  mutable std::size_t hash_code = 0;
#endif
 
  void clear()
  {
    data.clear();
    sub.clear();
    named_sub.clear();
#if HASH_CODE
    hash_code = 0;
#endif
  }
 
  void swap(tree_nodet &d)
  {
    d.data.swap(data);
    d.sub.swap(sub);
    d.named_sub.swap(named_sub);
#if HASH_CODE
    std::swap(d.hash_code, hash_code);
#endif
  }
 
  tree_nodet() = default;
 
  explicit tree_nodet(irep_idt _data) : data(std::move(_data))
  {
  }
 
  tree_nodet(irep_idt _data, named_subt _named_sub, subt _sub)
    : data(std::move(_data)),
      named_sub(std::move(_named_sub)),
      sub(std::move(_sub))
  {
  }
};
 
template <typename derivedt, typename named_subtreest>
class sharing_treet
{
public:
  using dt = tree_nodet<derivedt, named_subtreest, true>;
  using subt = typename dt::subt;
  using named_subt = typename dt::named_subt;
 
  using tree_implementationt = sharing_treet;
 
  explicit sharing_treet(irep_idt _id) : data(new dt(std::move(_id)))
  {
  }
 
  sharing_treet(irep_idt _id, named_subt _named_sub, subt _sub)
    : data(new dt(std::move(_id), std::move(_named_sub), std::move(_sub)))
  {
  }
 
  // constructor for blank irep
  sharing_treet() : data(&empty_d)
  {
  }
 
  // copy constructor
  sharing_treet(const sharing_treet &irep) : data(irep.data)
  {
    if(data!=&empty_d)
    {
      PRECONDITION(data->ref_count != 0);
      data->ref_count++;
#ifdef IREP_DEBUG
      std::cout << "COPY " << data << " " << data->ref_count << '\n';
#endif
    }
  }
 
  // Copy from rvalue reference.
  // Note that this does avoid a branch compared to the
  // standard copy constructor above.
  sharing_treet(sharing_treet &&irep) : data(irep.data)
  {
#ifdef IREP_DEBUG
    std::cout << "COPY MOVE\n";
#endif
    irep.data=&empty_d;
  }
 
  sharing_treet &operator=(const sharing_treet &irep)
  {
#ifdef IREP_DEBUG
    std::cout << "ASSIGN\n";
#endif
 
    // Ordering is very important here!
    // Consider self-assignment, which may destroy 'irep'
    dt *irep_data=irep.data;
    if(irep_data!=&empty_d)
      irep_data->ref_count++;
 
    remove_ref(data); // this may kill 'irep'
    data=irep_data;
 
    return *this;
  }
 
  // Note that the move assignment operator does avoid
  // three branches compared to standard operator above.
  sharing_treet &operator=(sharing_treet &&irep)
  {
#ifdef IREP_DEBUG
    std::cout << "ASSIGN MOVE\n";
#endif
    // we simply swap two pointers
    std::swap(data, irep.data);
    return *this;
  }
 
  ~sharing_treet()
  {
    remove_ref(data);
  }
 
protected:
  dt *data;
  static dt empty_d;
 
  static void remove_ref(dt *old_data);
  static void nonrecursive_destructor(dt *old_data);
  void detach();
 
public:
  const dt &read() const
  {
    return *data;
  }
 
  dt &write()
  {
    detach();
#if HASH_CODE
    data->hash_code = 0;
#endif
    return *data;
  }
};
 
// Static field initialization
template <typename derivedt, typename named_subtreest>
typename sharing_treet<derivedt, named_subtreest>::dt
  sharing_treet<derivedt, named_subtreest>::empty_d;
 
template <typename derivedt, typename named_subtreest>
class non_sharing_treet
{
public:
  using dt = tree_nodet<derivedt, named_subtreest, false>;
  using subt = typename dt::subt;
  using named_subt = typename dt::named_subt;
 
  using tree_implementationt = non_sharing_treet;
 
  explicit non_sharing_treet(irep_idt _id) : data(std::move(_id))
  {
  }
 
  non_sharing_treet(irep_idt _id, named_subt _named_sub, subt _sub)
    : data(std::move(_id), std::move(_named_sub), std::move(_sub))
  {
  }
 
  non_sharing_treet() = default;
 
  const dt &read() const
  {
    return data;
  }
 
  dt &write()
  {
#if HASH_CODE
    data.hash_code = 0;
#endif
    return data;
  }
 
protected:
  dt data;
};
 
class irept
#ifdef SHARING
  : public sharing_treet<
      irept,
#else
  : public non_sharing_treet<
      irept,
#endif
#if NAMED_SUB_IS_FORWARD_LIST
      forward_list_as_mapt<irep_idt, irept>>
#else
      std::map<irep_idt, irept>>
#endif
{
public:
  using baset = tree_implementationt;
 
  bool is_nil() const
  {
    return id() == ID_nil;
  }
  bool is_not_nil() const
  {
    return id() != ID_nil;
  }
 
  explicit irept(const irep_idt &_id) : baset(_id)
  {
  }
 
  irept(const irep_idt &_id, const named_subt &_named_sub, const subt &_sub)
    : baset(_id, _named_sub, _sub)
  {
  }
 
  irept() = default;
 
  const irep_idt &id() const
  { return read().data; }
 
  const std::string &id_string() const
  { return id2string(read().data); }
 
  void id(const irep_idt &_data)
  { write().data=_data; }
 
  const irept &find(const irep_idt &name) const;
  irept &add(const irep_idt &name);
  irept &add(const irep_idt &name, irept irep);
 
  const std::string &get_string(const irep_idt &name) const
  {
    return id2string(get(name));
  }
 
  const irep_idt &get(const irep_idt &name) const;
  bool get_bool(const irep_idt &name) const;
  signed int get_int(const irep_idt &name) const;
  std::size_t get_size_t(const irep_idt &name) const;
  long long get_long_long(const irep_idt &name) const;
 
  void set(const irep_idt &name, const irep_idt &value)
  {
    add(name, irept(value));
  }
  void set(const irep_idt &name, irept irep)
  {
    add(name, std::move(irep));
  }
  void set(const irep_idt &name, const long long value);
  void set_size_t(const irep_idt &name, const std::size_t value);
 
  void remove(const irep_idt &name);
  void move_to_sub(irept &irep);
  void move_to_named_sub(const irep_idt &name, irept &irep);
 
  bool operator==(const irept &other) const;
 
  bool operator!=(const irept &other) const
  {
    return !(*this==other);
  }
 
  void swap(irept &irep)
  {
    std::swap(irep.data, data);
  }
 
  bool operator<(const irept &other) const;
  bool ordering(const irept &other) const;
 
  int compare(const irept &i) const;
 
  void clear() { *this=irept(); }
 
  void make_nil() { *this=get_nil_irep(); }
 
  subt &get_sub() { return write().sub; } // DANGEROUS
  const subt &get_sub() const { return read().sub; }
  named_subt &get_named_sub() { return write().named_sub; } // DANGEROUS
  const named_subt &get_named_sub() const { return read().named_sub; }
 
  std::size_t hash() const;
  std::size_t full_hash() const;
 
  bool full_eq(const irept &other) const;
 
  std::string pretty(unsigned indent=0, unsigned max_indent=0) const;
 
  static bool is_comment(const irep_idt &name)
  { return !name.empty() && name[0]=='#'; }
 
  static std::size_t number_of_non_comments(const named_subt &);
};
 
// NOLINTNEXTLINE(readability/identifiers)
struct irep_hash
{
  std::size_t operator()(const irept &irep) const
  {
    return irep.hash();
  }
};
 
// NOLINTNEXTLINE(readability/identifiers)
struct irep_full_hash
{
  std::size_t operator()(const irept &irep) const
  {
    return irep.full_hash();
  }
};
 
// NOLINTNEXTLINE(readability/identifiers)
struct irep_full_eq
{
  bool operator()(const irept &i1, const irept &i2) const
  {
    return i1.full_eq(i2);
  }
};
 
struct irep_pretty_diagnosticst
{
  const irept &irep;
  explicit irep_pretty_diagnosticst(const irept &irep);
};
 
template <>
struct diagnostics_helpert<irep_pretty_diagnosticst>
{
  static std::string diagnostics_as_string(const irep_pretty_diagnosticst &irep)
  {
    return irep.irep.pretty();
  }
};
 
template <typename derivedt, typename named_subtreest>
void sharing_treet<derivedt, named_subtreest>::detach()
{
#ifdef IREP_DEBUG
  std::cout << "DETACH1: " << data << '\n';
#endif
 
  if(data == &empty_d)
  {
    data = new dt;
 
#ifdef IREP_DEBUG
    std::cout << "ALLOCATED " << data << '\n';
#endif
  }
  else if(data->ref_count > 1)
  {
    dt *old_data(data);
    data = new dt(*old_data);
 
#ifdef IREP_DEBUG
    std::cout << "ALLOCATED " << data << '\n';
#endif
 
    data->ref_count = 1;
    remove_ref(old_data);
  }
 
  POSTCONDITION(data->ref_count == 1);
 
#ifdef IREP_DEBUG
  std::cout << "DETACH2: " << data << '\n';
#endif
}
 
template <typename derivedt, typename named_subtreest>
void sharing_treet<derivedt, named_subtreest>::remove_ref(dt *old_data)
{
  if(old_data == &empty_d)
    return;
 
#if 0
    nonrecursive_destructor(old_data);
#else
 
  PRECONDITION(old_data->ref_count != 0);
 
#ifdef IREP_DEBUG
  std::cout << "R: " << old_data << " " << old_data->ref_count << '\n';
#endif
 
  old_data->ref_count--;
  if(old_data->ref_count == 0)
  {
#ifdef IREP_DEBUG
    std::cout << "D: " << pretty() << '\n';
    std::cout << "DELETING " << old_data->data << " " << old_data << '\n';
    old_data->clear();
    std::cout << "DEALLOCATING " << old_data << "\n";
#endif
 
    // may cause recursive call
    delete old_data;
 
#ifdef IREP_DEBUG
    std::cout << "DONE\n";
#endif
  }
#endif
}
 
template <typename derivedt, typename named_subtreest>
void sharing_treet<derivedt, named_subtreest>::nonrecursive_destructor(
  dt *old_data)
{
  std::vector<dt *> stack(1, old_data);
 
  while(!stack.empty())
  {
    dt *d = stack.back();
    stack.erase(--stack.end());
    if(d == &empty_d)
      continue;
 
    INVARIANT(d->ref_count != 0, "All contents of the stack must be in use");
    d->ref_count--;
 
    if(d->ref_count == 0)
    {
      stack.reserve(
        stack.size() + std::distance(d->named_sub.begin(), d->named_sub.end()) +
        d->sub.size());
 
      for(typename named_subt::iterator it = d->named_sub.begin();
          it != d->named_sub.end();
          it++)
      {
        stack.push_back(it->second.data);
        it->second.data = &empty_d;
      }
 
      for(typename subt::iterator it = d->sub.begin(); it != d->sub.end(); it++)
      {
        stack.push_back(it->data);
        it->data = &empty_d;
      }
 
      // now delete, won't do recursion
      delete d;
    }
  }
}
 
#endif // CPROVER_UTIL_IREP_H