renamed.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symbolic Execution
 
Author: Romain Brenguier, romain.brenguier@diffblue.com
 
\*******************************************************************/
 
#ifndef CPROVER_GOTO_SYMEX_RENAMED_H
#define CPROVER_GOTO_SYMEX_RENAMED_H
 
#include <util/expr_iterator.h>
#include <util/simplify_expr.h>
#include <util/std_expr.h>
 
class ssa_exprt;
 
enum levelt
{
  L0 = 0,
  L1 = 1,
  L1_WITH_CONSTANT_PROPAGATION = 2,
  L2 = 3
};
 
template <typename underlyingt, levelt level>
class renamedt : private underlyingt
{
public:
  static_assert(
    std::is_base_of<exprt, underlyingt>::value ||
      std::is_base_of<typet, underlyingt>::value,
    "underlyingt should inherit from exprt or typet");
 
  const underlyingt &get() const
  {
    return static_cast<const underlyingt &>(*this);
  }
 
  void simplify(const namespacet &ns)
  {
    (void)::simplify(value(), ns);
  }
 
  using mutator_functiont =
    std::function<optionalt<renamedt>(const renamedt &)>;
 
private:
  underlyingt &value()
  {
    return static_cast<underlyingt &>(*this);
  };
 
  friend renamedt<ssa_exprt, L0>
  symex_level0(ssa_exprt, const namespacet &, std::size_t);
  friend struct symex_level1t;
  friend struct symex_level2t;
  friend class goto_symex_statet;
 
  template <levelt make_renamed_level>
  friend renamedt<exprt, make_renamed_level>
  make_renamed(constant_exprt constant);
 
  template <levelt selectively_mutate_level>
  friend void selectively_mutate(
    renamedt<exprt, selectively_mutate_level> &renamed,
    typename renamedt<exprt, selectively_mutate_level>::mutator_functiont
      get_mutated_expr);
 
  explicit renamedt(underlyingt value) : underlyingt(std::move(value))
  {
  }
};
 
template <levelt level>
renamedt<exprt, level> make_renamed(constant_exprt constant)
{
  return renamedt<exprt, level>(std::move(constant));
}
 
template <levelt level>
void selectively_mutate(
  renamedt<exprt, level> &renamed,
  typename renamedt<exprt, level>::mutator_functiont get_mutated_expr)
{
  for(auto it = renamed.depth_begin(), itend = renamed.depth_end(); it != itend;
      ++it)
  {
    optionalt<renamedt<exprt, level>> replacement =
      get_mutated_expr(static_cast<const renamedt<exprt, level> &>(*it));
 
    if(replacement)
      it.mutate() = std::move(replacement->value());
  }
}
 
#endif // CPROVER_GOTO_SYMEX_RENAMED_H