expr.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
#ifndef CPROVER_UTIL_EXPR_H
#define CPROVER_UTIL_EXPR_H
 
#include "as_const.h"
#include "type.h"
#include "validate_expressions.h"
#include "validate_types.h"
#include "validation_mode.h"
 
#include <functional>
 
#define forall_operands(it, expr)                                              \
  for(exprt::operandst::const_iterator                                         \
        it = as_const(expr).operands().begin(),                                \
        it##_end = as_const(expr).operands().end();                            \
      it != it##_end;                                                          \
      ++it)
 
#define Forall_operands(it, expr) \
  if((expr).has_operands()) /* NOLINT(readability/braces) */ \
    for(exprt::operandst::iterator it=(expr).operands().begin(); \
        it!=(expr).operands().end(); ++it)
 
#define forall_expr(it, expr) \
  for(exprt::operandst::const_iterator it=(expr).begin(); \
      it!=(expr).end(); ++it)
 
#define Forall_expr(it, expr) \
  for(exprt::operandst::iterator it=(expr).begin(); \
      it!=(expr).end(); ++it)
 
class depth_iteratort;
class const_depth_iteratort;
class const_unique_depth_iteratort;
 
class exprt:public irept
{
public:
  typedef std::vector<exprt> operandst;
 
  // constructors
  exprt() { }
  explicit exprt(const irep_idt &_id):irept(_id) { }
 
  exprt(irep_idt _id, typet _type)
    : irept(std::move(_id), {{ID_type, std::move(_type)}}, {})
  {
  }
 
  exprt(irep_idt _id, typet _type, operandst &&_operands)
    : irept(
        std::move(_id),
        {{ID_type, std::move(_type)}},
        std::move((irept::subt &&) _operands))
  {
  }
 
  exprt(const irep_idt &id, typet type, source_locationt loc)
    : exprt(id, std::move(type))
  {
    add_source_location() = std::move(loc);
  }
 
  typet &type() { return static_cast<typet &>(add(ID_type)); }
  const typet &type() const
  {
    return static_cast<const typet &>(find(ID_type));
  }
 
  bool has_operands() const
  { return !operands().empty(); }
 
  operandst &operands()
  { return (operandst &)get_sub(); }
 
  const operandst &operands() const
  { return (const operandst &)get_sub(); }
 
  exprt &with_source_location(source_locationt location) &
  {
    if(location.is_not_nil())
      add_source_location() = std::move(location);
    return *this;
  }
 
  exprt &&with_source_location(source_locationt location) &&
  {
    if(location.is_not_nil())
      add_source_location() = std::move(location);
    return std::move(*this);
  }
 
  exprt &with_source_location(const exprt &other) &
  {
    if(other.source_location().is_not_nil())
      add_source_location() = other.source_location();
    return *this;
  }
 
  exprt &&with_source_location(const exprt &other) &&
  {
    if(other.source_location().is_not_nil())
      add_source_location() = other.source_location();
    return std::move(*this);
  }
 
protected:
  exprt &op0()
  { return operands().front(); }
 
  exprt &op1()
  { return operands()[1]; }
 
  exprt &op2()
  { return operands()[2]; }
 
  exprt &op3()
  { return operands()[3]; }
 
  const exprt &op0() const
  { return operands().front(); }
 
  const exprt &op1() const
  { return operands()[1]; }
 
  const exprt &op2() const
  { return operands()[2]; }
 
  const exprt &op3() const
  { return operands()[3]; }
 
public:
  void reserve_operands(operandst::size_type n)
  { operands().reserve(n) ; }
 
  void copy_to_operands(const exprt &expr)
  {
    operands().push_back(expr);
  }
 
  void add_to_operands(const exprt &expr)
  {
    copy_to_operands(expr);
  }
 
  void add_to_operands(exprt &&expr)
  {
    operands().push_back(std::move(expr));
  }
 
  void add_to_operands(exprt &&e1, exprt &&e2)
  {
    operandst &op = operands();
    #ifndef USE_LIST
    op.reserve(op.size() + 2);
    #endif
    op.push_back(std::move(e1));
    op.push_back(std::move(e2));
  }
 
  void add_to_operands(exprt &&e1, exprt &&e2, exprt &&e3)
  {
    operandst &op = operands();
    #ifndef USE_LIST
    op.reserve(op.size() + 3);
    #endif
    op.push_back(std::move(e1));
    op.push_back(std::move(e2));
    op.push_back(std::move(e3));
  }
 
  bool is_constant() const
  {
    return id() == ID_constant;
  }
 
  bool is_true() const;
  bool is_false() const;
  bool is_zero() const;
  bool is_one() const;
 
  bool is_boolean() const
  {
    return type().id() == ID_bool;
  }
 
  const source_locationt &find_source_location() const;
 
  const source_locationt &source_location() const
  {
    return static_cast<const source_locationt &>(find(ID_C_source_location));
  }
 
  source_locationt &add_source_location()
  {
    return static_cast<source_locationt &>(add(ID_C_source_location));
  }
 
  void drop_source_location()
  {
    remove(ID_C_source_location);
  }
 
  static void check(const exprt &, const validation_modet)
  {
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    check_expr(expr, vm);
  }
 
  static void validate_full(
    const exprt &expr,
    const namespacet &ns,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    // first check operands (if any)
    for(const exprt &op : expr.operands())
    {
      validate_full_expr(op, ns, vm);
    }
 
    // type may be nil
    const typet &t = expr.type();
 
    validate_full_type(t, ns, vm);
 
    validate_expr(expr, ns, vm);
  }
 
protected:
  exprt &add_expr(const irep_idt &name)
  {
    return static_cast<exprt &>(add(name));
  }
 
  const exprt &find_expr(const irep_idt &name) const
  {
    return static_cast<const exprt &>(find(name));
  }
 
public:
  void visit(class expr_visitort &visitor);
  void visit(class const_expr_visitort &visitor) const;
  void visit_pre(std::function<void(exprt &)>);
  void visit_pre(std::function<void(const exprt &)>) const;
 
  void visit_post(std::function<void(exprt &)>);
  void visit_post(std::function<void(const exprt &)>) const;
 
  depth_iteratort depth_begin();
  depth_iteratort depth_end();
  const_depth_iteratort depth_begin() const;
  const_depth_iteratort depth_end() const;
  const_depth_iteratort depth_cbegin() const;
  const_depth_iteratort depth_cend() const;
  depth_iteratort depth_begin(std::function<exprt &()> mutate_root) const;
  const_unique_depth_iteratort unique_depth_begin() const;
  const_unique_depth_iteratort unique_depth_end() const;
  const_unique_depth_iteratort unique_depth_cbegin() const;
  const_unique_depth_iteratort unique_depth_cend() const;
};
 
class expr_protectedt : public exprt
{
protected:
  // constructors
  expr_protectedt(irep_idt _id, typet _type)
    : exprt(std::move(_id), std::move(_type))
  {
  }
 
  expr_protectedt(irep_idt _id, typet _type, operandst _operands)
    : exprt(std::move(_id), std::move(_type), std::move(_operands))
  {
  }
 
  // protect these low-level methods
  using exprt::add;
  using exprt::op0;
  using exprt::op1;
  using exprt::op2;
  using exprt::op3;
  using exprt::remove;
};
 
class expr_visitort
{
public:
  virtual ~expr_visitort() { }
  virtual void operator()(exprt &) { }
};
 
class const_expr_visitort
{
public:
  virtual ~const_expr_visitort() { }
  virtual void operator()(const exprt &) { }
};
 
#endif // CPROVER_UTIL_EXPR_H