expr_iterator.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: exprt iterator module
 
Author: Diffblue Ltd.
 
\*******************************************************************/
 
#ifndef CPROVER_UTIL_EXPR_ITERATOR_H
#define CPROVER_UTIL_EXPR_ITERATOR_H
 
#include <deque>
#include <iterator>
#include <functional>
#include <set>
#include <algorithm>
#include "expr.h"
#include "invariant.h"
 
// Forward declarations - table of contents
 
 
class depth_iteratort;
class const_depth_iteratort;
class const_unique_depth_iteratort;
class const_post_depth_iteratort;
 
struct depth_iterator_expr_statet final
{
  typedef exprt::operandst::const_iterator operands_iteratort;
  explicit depth_iterator_expr_statet(const exprt &expr) : expr(expr), op_idx(0)
  {
  }
  std::reference_wrapper<const exprt> expr;
  std::size_t op_idx;
};
 
inline bool operator==(
  const depth_iterator_expr_statet &left,
  const depth_iterator_expr_statet &right)
{
  return left.op_idx == right.op_idx && left.expr.get() == right.expr.get();
}
 
template<typename depth_iterator_t>
class depth_iterator_baset
{
public:
  typedef void difference_type;   // NOLINT Required by STL
  typedef exprt value_type;       // NOLINT
  typedef const exprt *pointer;   // NOLINT
  typedef const exprt &reference; // NOLINT
  typedef std::forward_iterator_tag iterator_category; // NOLINT
 
  template <typename other_depth_iterator_t>
  friend class depth_iterator_baset;
 
  template <typename other_depth_iterator_t>
  bool operator==(
    const depth_iterator_baset<other_depth_iterator_t> &other) const
  {
    return m_stack==other.m_stack;
  }
 
  template <typename other_depth_iterator_t>
  bool operator!=(
    const depth_iterator_baset<other_depth_iterator_t> &other) const
  {
    return !(*this == other);
  }
 
  depth_iterator_t &operator++()
  {
    PRECONDITION(!m_stack.empty());
    while(true)
    {
      if(m_stack.back().op_idx == m_stack.back().expr.get().operands().size())
      {
        m_stack.pop_back();
        if(m_stack.empty())
          break;
      }
      // Check eg. if we haven't seen this node before
      else if(this->downcast().push_expr(
                m_stack.back().expr.get().operands()[m_stack.back().op_idx]))
      {
        break;
      }
      ++m_stack.back().op_idx;
    }
    return this->downcast();
  }
 
  depth_iterator_t &next_sibling_or_parent()
  {
    PRECONDITION(!m_stack.empty());
    m_stack.pop_back();
    if(!m_stack.empty())
    {
      ++m_stack.back().op_idx;
      return ++(*this);
    }
    return this->downcast();
  }
 
  depth_iterator_t operator++(int)
  {
    depth_iterator_t tmp(this->downcast());
    this->operator++();
    return tmp;
  }
 
  const exprt &operator*() const
  {
    PRECONDITION(!m_stack.empty());
    return m_stack.back().expr.get();
  }
 
  const exprt *operator->() const
  { return &**this; }
 
protected:
  depth_iterator_baset()=default;
 
  explicit depth_iterator_baset(const exprt &root)
  { this->push_expr(root); }
 
  ~depth_iterator_baset()=default;
 
  depth_iterator_baset(const depth_iterator_baset &)=default;
  depth_iterator_baset(depth_iterator_baset &&other)
  { m_stack=std::move(other.m_stack); }
  depth_iterator_baset &operator=(const depth_iterator_baset&)=default;
  depth_iterator_baset &operator=(depth_iterator_baset &&other)
  {
    m_stack = std::move(other.m_stack);
    return *this;
  }
 
  const exprt &get_root()
  {
    return m_stack.front().expr.get();
  }
 
  exprt &mutate()
  {
    PRECONDITION(!m_stack.empty());
    // Cast the root expr to non-const
    exprt *expr = &const_cast<exprt &>(get_root());
    for(auto &state : m_stack)
    {
      // This deliberately breaks sharing as expr is now non-const
      (void)expr->write();
      state.expr = *expr;
      // Get the expr for the next level down to use in the next iteration
      if(!(state == m_stack.back()))
        expr = &expr->operands()[state.op_idx];
    }
    return *expr;
  }
 
  bool push_expr(const exprt &expr)
  {
    m_stack.emplace_back(expr);
    return true;
  }
 
private:
  std::deque<depth_iterator_expr_statet> m_stack;
 
  depth_iterator_t &downcast()
  { return static_cast<depth_iterator_t &>(*this); }
};
 
class const_depth_iteratort final:
  public depth_iterator_baset<const_depth_iteratort>
{
public:
  explicit const_depth_iteratort(const exprt &expr):
    depth_iterator_baset(expr) { }
  const_depth_iteratort()=default;
};
 
class depth_iteratort final:
  public depth_iterator_baset<depth_iteratort>
{
private:
  std::function<exprt &()> mutate_root;
 
public:
  depth_iteratort()=default;
 
  explicit depth_iteratort(exprt &expr) : depth_iterator_baset(expr)
  {
  }
 
  explicit depth_iteratort(
    const exprt &expr,
    std::function<exprt &()> mutate_root)
    : depth_iterator_baset(expr), mutate_root(std::move(mutate_root))
  {
    // If you don't provide a mutate_root function then you must pass a
    // non-const exprt (use the other constructor).
    PRECONDITION(this->mutate_root);
  }
 
  exprt &mutate()
  {
    if(mutate_root)
    {
      exprt &new_root = mutate_root();
      INVARIANT(
        &new_root.read() == &get_root().read(),
        "mutate_root must return the same root node that depth_iteratort was "
        "constructed with");
      mutate_root = nullptr;
    }
    return depth_iterator_baset::mutate();
  }
};
 
class const_unique_depth_iteratort final:
  public depth_iterator_baset<const_unique_depth_iteratort>
{
  friend depth_iterator_baset;
public:
  explicit const_unique_depth_iteratort(const exprt &expr):
    depth_iterator_baset(expr),
    m_traversed({ expr }) { }
  const_unique_depth_iteratort()=default;
private:
  bool push_expr(const exprt &expr) // "override" - hide base class method
  {
    const bool inserted=this->m_traversed.insert(expr).second;
    if(inserted)
      depth_iterator_baset::push_expr(expr);
    return inserted;
  }
  std::set<exprt> m_traversed;
};
 
class const_depth_iterator_range_adaptert
{
public:
  explicit const_depth_iterator_range_adaptert(const exprt &_root) : root{_root}
  {
  }
 
  const_depth_iteratort begin() const
  {
    return root.depth_cbegin();
  }
 
  const_depth_iteratort end() const
  {
    return root.depth_cend();
  }
 
protected:
  const exprt &root;
};
 
static inline const_depth_iterator_range_adaptert
pre_traversal(const exprt &root)
{
  return const_depth_iterator_range_adaptert{root};
}
 
class const_post_depth_iteratort final
{
public:
  typedef void difference_type;                        // NOLINT Required by STL
  typedef exprt value_type;                            // NOLINT
  typedef const exprt *pointer;                        // NOLINT
  typedef const exprt &reference;                      // NOLINT
  typedef std::forward_iterator_tag iterator_category; // NOLINT
 
  explicit const_post_depth_iteratort(const exprt &expr)
  {
    descend_to_leftmost_leaf(expr);
  }
 
  const_post_depth_iteratort() = default;
 
  bool operator==(const const_post_depth_iteratort &other) const
  {
    return m_stack == other.m_stack;
  }
 
  bool operator!=(const const_post_depth_iteratort &other) const
  {
    return !(*this == other);
  }
 
  const_post_depth_iteratort &operator++()
  {
    PRECONDITION(!m_stack.empty());
 
    // Pop the current node (we've just visited it)
    m_stack.pop_back();
 
    if(m_stack.empty())
      return *this;
 
    // Move to next sibling
    ++m_stack.back().op_idx;
 
    // If there's a next sibling, descend to its leftmost leaf
    if(m_stack.back().op_idx < m_stack.back().expr.get().operands().size())
    {
      descend_to_leftmost_leaf(
        m_stack.back().expr.get().operands()[m_stack.back().op_idx]);
    }
    // Otherwise, the parent is the next node to visit (already on stack)
 
    return *this;
  }
 
  const_post_depth_iteratort operator++(int)
  {
    const_post_depth_iteratort tmp(*this);
    ++(*this);
    return tmp;
  }
 
  const exprt &operator*() const
  {
    PRECONDITION(!m_stack.empty());
    return m_stack.back().expr.get();
  }
 
  const exprt *operator->() const
  {
    return &**this;
  }
 
private:
  void descend_to_leftmost_leaf(const exprt &expr)
  {
    const exprt *current = &expr;
    while(true)
    {
      m_stack.emplace_back(*current);
      if(current->operands().empty())
        break;
      current = &current->operands().front();
    }
  }
 
  std::deque<depth_iterator_expr_statet> m_stack;
};
 
class const_post_depth_iterator_range_adaptert
{
public:
  explicit const_post_depth_iterator_range_adaptert(const exprt &_root)
    : root{_root}
  {
  }
 
  const_post_depth_iteratort begin() const
  {
    return const_post_depth_iteratort{root};
  }
 
  const_post_depth_iteratort end() const
  {
    return const_post_depth_iteratort{};
  }
 
protected:
  const exprt &root;
};
 
static inline const_post_depth_iterator_range_adaptert
post_traversal(const exprt &root)
{
  return const_post_depth_iterator_range_adaptert{root};
}
 
#endif