irep2_expr.h

Go to the documentation of this file.

#ifndef IREP2_EXPR_H_
#define IREP2_EXPR_H_
 
#include <util/config/config.h>
#include <util/lang/c_types.h>
#include <util/arith/fixedbv.h>
#include <util/arith/ieee_float.h>
#include <util/irep/location.h>
#include <irep2/irep2_type.h>
 
// So - make some type definitions for the different types we're going to be
// working with. This is to avoid the repeated use of template names in later
// definitions. If you'd like to add another type - don't. Vast tracts of code
// only expect the types below, it's be extremely difficult to hack new ones in.
 
// Start of definitions for expressions. Forward decls
//
// Forward-declare a concrete <kind>2t class for every entry in the
// expr_kinds.inc manifest. The same manifest drives the expr_ids
// enum (in irep2.h) and the is_/to_/try_to_ predicate generators
// further down this file.
#define IREP2_EXPR(kind, pretty) class kind##2t;
#include <irep2/expr_kinds.inc>
#undef IREP2_EXPR
 
enum class constant_string_kindt
{
  DEFAULT, /* "" */
  WIDE,    /* L"" */
  UNICODE, /* u8"", u"" and U"" */
};

enum class symbol_renaming_level
{
  level0,
  level1,
  level2,
  level1_global,
  level2_global,
};

void assert_arith_2ops_consistency(
  const type2tc &t,
  expr2t::expr_ids id,
  const expr2tc &v1,
  const expr2tc &v2);

enum class sideeffect_allockind
{
  malloc,
  realloc,
  alloca,
  cpp_new,
  cpp_new_arr,
  nondet,
  va_arg,
  printf2,
  function_call,
  preincrement,
  postincrement,
  predecrement,
  postdecrement,
  old_snapshot,               // For __ESBMC_old() in function contracts
  assigns_target,             // For __ESBMC_assigns() in function contracts
  statement_expression,       // GNU C ({ ... }) extension
  temporary_object,           // C++ temporary created inline (constructor)
  gcc_conditional_expression, // GNU C `a ?: b` (omitted middle operand)
  cpp_delete,                 // C++ `delete p` in expression position
  cpp_delete_array            // C++ `delete[] p` in expression position
};

enum class printf_kindt
{
  PRINTF,
  FPRINTF,
  DPRINTF,
  SPRINTF,
  VFPRINTF,
  SNPRINTF,
  VPRINTF,
  VSPRINTF,
  VSNPRINTF,
  ASPRINTF,
  VASPRINTF,
};

printf_kindt printf_kind_from_name(const irep_idt &name);
 
#define irep_typedefs(basename)                                                \
  template <typename... Args>                                                  \
  inline expr2tc basename##2tc(Args && ...args)                                \
  {                                                                            \
    return make_irep<basename##2t>(std::forward<Args>(args)...);               \
  }
 
irep_typedefs(constant_int);
irep_typedefs(constant_fixedbv);
irep_typedefs(constant_floatbv);
irep_typedefs(constant_struct);
irep_typedefs(constant_union);
irep_typedefs(constant_array);
irep_typedefs(constant_vector);
irep_typedefs(constant_bool);
irep_typedefs(constant_array_of);
irep_typedefs(constant_string);
irep_typedefs(symbol);
irep_typedefs(nearbyint);
irep_typedefs(typecast);
irep_typedefs(bitcast);
irep_typedefs(if);
irep_typedefs(equality);
irep_typedefs(notequal);
irep_typedefs(lessthan);
irep_typedefs(greaterthan);
irep_typedefs(lessthanequal);
irep_typedefs(greaterthanequal);
irep_typedefs(cmp_three_way);
irep_typedefs(not);
irep_typedefs(and);
irep_typedefs(or);
irep_typedefs(xor);
irep_typedefs(implies);
irep_typedefs(bitand);
irep_typedefs(bitor);
irep_typedefs(bitxor);
irep_typedefs(lshr);
irep_typedefs(bitnot);
irep_typedefs(neg);
irep_typedefs(abs);
irep_typedefs(add);
irep_typedefs(sub);
irep_typedefs(mul);
irep_typedefs(div);
irep_typedefs(ieee_add);
irep_typedefs(ieee_sub);
irep_typedefs(ieee_mul);
irep_typedefs(ieee_div);
irep_typedefs(ieee_rem);
irep_typedefs(ieee_fma);
irep_typedefs(ieee_sqrt);
irep_typedefs(modulus);
irep_typedefs(shl);
irep_typedefs(ashr);
irep_typedefs(same_object);
irep_typedefs(pointer_offset);
irep_typedefs(pointer_object);
irep_typedefs(pointer_capability);
irep_typedefs(address_of);
irep_typedefs(byte_extract);
irep_typedefs(byte_update);
irep_typedefs(with);
irep_typedefs(member);
irep_typedefs(member_ref);
irep_typedefs(ptr_mem);
irep_typedefs(index);
irep_typedefs(isnan);
irep_typedefs(overflow);
irep_typedefs(overflow_cast);
irep_typedefs(overflow_neg);
irep_typedefs(unknown);
irep_typedefs(invalid);
irep_typedefs(null_object);
irep_typedefs(dynamic_object);
irep_typedefs(dereference);
irep_typedefs(valid_object);
irep_typedefs(races_check);
irep_typedefs(deallocated_obj);
irep_typedefs(dynamic_size);
irep_typedefs(sideeffect);
irep_typedefs(code_block);
irep_typedefs(code_assign);
irep_typedefs(code_decl);
irep_typedefs(code_dead);
irep_typedefs(code_printf);
irep_typedefs(code_expression);
irep_typedefs(code_return);
irep_typedefs(code_skip);
irep_typedefs(code_free);
irep_typedefs(code_goto);
irep_typedefs(object_descriptor);
irep_typedefs(code_function_call);
irep_typedefs(code_ifthenelse);
irep_typedefs(code_while);
irep_typedefs(code_dowhile);
irep_typedefs(code_for);
irep_typedefs(code_switch);
irep_typedefs(code_break);
irep_typedefs(code_continue);
irep_typedefs(code_label);
irep_typedefs(code_switch_case);
irep_typedefs(code_assert);
irep_typedefs(code_assume);
irep_typedefs(sideeffect_assign);
irep_typedefs(code_comma);
irep_typedefs(invalid_pointer);
irep_typedefs(code_asm);
irep_typedefs(code_cpp_del_array);
irep_typedefs(code_cpp_delete);
irep_typedefs(code_cpp_catch);
irep_typedefs(code_cpp_throw);
irep_typedefs(isinf);
irep_typedefs(isnormal);
irep_typedefs(isfinite);
irep_typedefs(signbit);
irep_typedefs(popcount);
irep_typedefs(bswap);
irep_typedefs(concat);
irep_typedefs(extract);
irep_typedefs(capability_base);
irep_typedefs(capability_top);
irep_typedefs(forall);
irep_typedefs(exists);
irep_typedefs(isinstance);
irep_typedefs(hasattr);
irep_typedefs(isnone);
irep_typedefs(new_object);
irep_typedefs(sizeof);
irep_typedefs(uninterpreted_func);
 
class exists2t : public expr2t
{
public:
  expr2tc side_1, side_2;
  exists2t(const type2tc &type, const expr2tc &sym, const expr2tc &predicate)
    : expr2t(type, exists_id), side_1(sym), side_2(predicate)
  {
  }
  exists2t(const exists2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &exists2t::side_1, &exists2t::side_2);
  static std::string field_names[esbmct::num_type_fields];
};
 
class forall2t : public expr2t
{
public:
  expr2tc side_1, side_2;
  forall2t(const type2tc &type, const expr2tc &sym, const expr2tc &predicate)
    : expr2t(type, forall_id), side_1(sym), side_2(predicate)
  {
  }
  forall2t(const forall2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &forall2t::side_1, &forall2t::side_2);
  static std::string field_names[esbmct::num_type_fields];
};

class constant_int2t : public expr2t
{
public:
  BigInt value;
  irep_idt cformat;

  constant_int2t(
    const type2tc &type,
    const BigInt &input,
    const irep_idt &fmt = irep_idt())
    : expr2t(type, constant_int_id), value(input), cformat(fmt)
  {
  }
  constant_int2t(const constant_int2t &ref) = default;

  unsigned long as_ulong() const;
  long as_long() const;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &constant_int2t::value);
  static constexpr std::size_t excluded_field_bytes = sizeof(irep_idt);
  static std::string field_names[esbmct::num_type_fields];
};

class constant_fixedbv2t : public expr2t
{
public:
  fixedbvt value;

  constant_fixedbv2t(const fixedbvt &value)
    : expr2t(value.spec.get_type(), constant_fixedbv_id), value(value)
  {
  }
  constant_fixedbv2t(const constant_fixedbv2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &constant_fixedbv2t::value);
  static std::string field_names[esbmct::num_type_fields];
};

class constant_floatbv2t : public expr2t
{
public:
  ieee_floatt value;
  irep_idt cformat;

  constant_floatbv2t(const ieee_floatt &value, const irep_idt &fmt = irep_idt())
    : expr2t(value.spec.get_type(), constant_floatbv_id),
      value(value),
      cformat(fmt)
  {
  }
  constant_floatbv2t(const constant_floatbv2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &constant_floatbv2t::value);
  static constexpr std::size_t excluded_field_bytes = sizeof(irep_idt);
  static std::string field_names[esbmct::num_type_fields];
};

class constant_bool2t : public expr2t
{
public:
  bool value;

  constant_bool2t(bool value)
    : expr2t(get_bool_type(), constant_bool_id), value(value)
  {
  }
  constant_bool2t(const constant_bool2t &ref) = default;

  bool is_true() const;
  bool is_false() const;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &constant_bool2t::value);
  static std::string field_names[esbmct::num_type_fields];
};

class constant_string2t : public expr2t
{
public:
  using kindt = constant_string_kindt;
 
  irep_idt value;
  constant_string_kindt kind;

  constant_string2t(
    const type2tc &type,
    const irep_idt &stringref,
    constant_string_kindt kind)
    : expr2t(type, constant_string_id), value(stringref), kind(kind)
  {
  }
  constant_string2t(const constant_string2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &constant_string2t::value,
    &constant_string2t::kind);

  expr2tc to_array() const;

  size_t array_size() const;

  expr2tc at(size_t i) const;
 
  static std::string field_names[esbmct::num_type_fields];
};

class constant_struct2t : public expr2t
{
public:
  std::vector<expr2tc> datatype_members;

  constant_struct2t(const type2tc &type, const std::vector<expr2tc> &members)
    : expr2t(type, constant_struct_id), datatype_members(members)
  {
    // complex_type2t is a primitive subtype but lowers to a 2-element
    // struct view at the SMT boundary (see struct_union_members), and
    // the clang frontend builds complex literals as struct-id exprt
    // with a complex type — accept that shape here.
    //
    // A symbol_id type is permitted ONLY as a transient pre-resolution state,
    // the same V.1k "two-phase source invariant" the member2t/index2t asserts
    // carry: the Python frontend stores class instances with a by-name
    // symbol_type and resolves it lazily, so migrating a constant aggregate
    // before the IREP2-native adjuster has followed the type would otherwise
    // abort here. The adjuster re-establishes the strong invariant before
    // symex; no frontend builds a constant_struct2t pre-adjust today, so this
    // disjunct is staged enabling infra exercised by the --python-irep2-adjust
    // path.
    assert(
      type->type_id == type2t::struct_id ||
      type->type_id == type2t::complex_id ||
      type->type_id == type2t::symbol_id);
  }
  constant_struct2t(const constant_struct2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &constant_struct2t::datatype_members);
  static std::string field_names[esbmct::num_type_fields];
};

class constant_union2t : public expr2t
{
public:
  std::vector<expr2tc> datatype_members;
  irep_idt init_field;

  constant_union2t(
    const type2tc &type,
    irep_idt if_,
    const std::vector<expr2tc> &members)
    : expr2t(type, constant_union_id),
      datatype_members(members),
      init_field(std::move(if_))
  {
    // A symbol_id type is permitted on the same terms constant_struct2t
    // permits it above: a transient pre-resolution state. migrate_expr builds
    // a union literal from `constant_union2tc(migrate_type(expr.type()), ...)`
    // (migrate.cpp:923), and a frontend whose union tag is still by-name at
    // that point yields symbol_type2t rather than union_type2t -- which aborted
    // here for 12 of regression/esbmc's tests under --clang-c-irep2-adjust,
    // while the identical shape passed for structs. The asymmetry was an
    // oversight, not a rule: NDEBUG builds already construct these nodes.
    assert(is_union_type(type) || type->type_id == type2t::symbol_id);
    // smt_conv.cpp's counterexample reconstruction intentionally builds unions
    //  with multiple members (see TODO in get_by_ast), so we can't check if the
    // union has at most 1 member initializer, with
    // assert(this->datatype_members.size() <= 1);
  }
  constant_union2t(const constant_union2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &constant_union2t::init_field,
    &constant_union2t::datatype_members);
  static std::string field_names[esbmct::num_type_fields];
};

class constant_array2t : public expr2t
{
public:
  std::vector<expr2tc> datatype_members;

  constant_array2t(const type2tc &type, const std::vector<expr2tc> &members)
    : expr2t(type, constant_array_id), datatype_members(members)
  {
    assert(type->type_id == type2t::array_id);
  }
  constant_array2t(const constant_array2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &constant_array2t::datatype_members);
  static std::string field_names[esbmct::num_type_fields];
};

class constant_vector2t : public expr2t
{
public:
  std::vector<expr2tc> datatype_members;

  constant_vector2t(const type2tc &type, const std::vector<expr2tc> &members)
    : expr2t(type, constant_vector_id), datatype_members(members)
  {
  }
  constant_vector2t(const constant_vector2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &constant_vector2t::datatype_members);
  static std::string field_names[esbmct::num_type_fields];
};

class constant_array_of2t : public expr2t
{
public:
  expr2tc initializer;

  constant_array_of2t(const type2tc &type, const expr2tc &init)
    : expr2t(type, constant_array_of_id), initializer(init)
  {
  }
  constant_array_of2t(const constant_array_of2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &constant_array_of2t::initializer);
  static std::string field_names[esbmct::num_type_fields];
};

class symbol2t : public expr2t
{
public:
  using renaming_level = symbol_renaming_level;
 
  irep_idt thename;
  symbol_renaming_level rlevel;
  unsigned int level1_num;
  unsigned int level2_num;
  unsigned int thread_num;
  unsigned int node_num;

  symbol2t(
    const type2tc &type,
    const irep_idt &init,
    renaming_level lev = renaming_level::level0,
    unsigned int l1 = 0,
    unsigned int l2 = 0,
    unsigned int trd = 0,
    unsigned int node = 0)
    : expr2t(type, symbol_id),
      thename(init),
      rlevel(lev),
      level1_num(l1),
      level2_num(l2),
      thread_num(trd),
      node_num(node)
  {
    /* At some point in the past, symbols named "NULL" and "0" were equivalent.
     * The symbol called "0" should no longer be created for uniformity reasons.
     * Confirm that here, since support for it has been removed from
     * smt_solver_baset. No other reason to disallow "0" as a symbol. */
    assert(init != "0");
  }
 
  symbol2t(const symbol2t &ref) = default;
 
  std::string get_symbol_name() const;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &symbol2t::thename,
    &symbol2t::rlevel,
    &symbol2t::level1_num,
    &symbol2t::level2_num,
    &symbol2t::thread_num,
    &symbol2t::node_num);
  static std::string field_names[esbmct::num_type_fields];
};

class nearbyint2t : public expr2t
{
public:
  expr2tc from;
  expr2tc rounding_mode;

  nearbyint2t(
    const type2tc &type,
    const expr2tc &from_,
    const expr2tc &rounding_mode_)
    : expr2t(type, nearbyint_id), from(from_), rounding_mode(rounding_mode_)
  {
  }

  nearbyint2t(const type2tc &type, const expr2tc &from_)
    : expr2t(type, nearbyint_id),
      from(from_),
      rounding_mode(symbol2tc(get_int32_type(), "c:@__ESBMC_rounding_mode"))
  {
  }
 
  nearbyint2t(const nearbyint2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &nearbyint2t::from,
    &nearbyint2t::rounding_mode);
  static std::string field_names[esbmct::num_type_fields];
};

class typecast2t : public expr2t
{
public:
  expr2tc from;
  expr2tc rounding_mode;

  irep_idt derived_to_base;

  bool base_to_derived;

  /** Primary constructor.
   *  @param type Type to typecast to
   *  @param from Expression to cast from.
   *  @param rounding_mode Rounding mode, important only for floatbvs
   */
  typecast2t(
    const type2tc &type,
    const expr2tc &from_,
    const expr2tc &rounding_mode_,
    const irep_idt &derived_to_base_ = irep_idt(),
    bool base_to_derived_ = false)
    : expr2t(type, typecast_id),
      from(from_),
      rounding_mode(rounding_mode_),
      derived_to_base(derived_to_base_),
      base_to_derived(base_to_derived_)
  {
  }


   *  the __ESBMC_rounding_mode symbol
   *  @param type Type to typecast to
   *  @param from Expression to cast from.
   */
  typecast2t(
    const type2tc &type,
    const expr2tc &from_,
    const irep_idt &derived_to_base_ = irep_idt(),
    bool base_to_derived_ = false)
    : expr2t(type, typecast_id),
      from(from_),
      rounding_mode(symbol2tc(get_int32_type(), "c:@__ESBMC_rounding_mode")),
      derived_to_base(derived_to_base_),
      base_to_derived(base_to_derived_)
  {
  }
 
  typecast2t(const typecast2t &ref) = default;
  expr2tc do_simplify() const override;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &typecast2t::from,
    &typecast2t::rounding_mode,
    &typecast2t::derived_to_base,
    &typecast2t::base_to_derived);
  static std::string field_names[esbmct::num_type_fields];
};

class bitcast2t : public expr2t
{
public:
  expr2tc from;

  bitcast2t(const type2tc &type, const expr2tc &from_)
    : expr2t(type, bitcast_id), from(from_)
  {
    try
    {
      assert(type->get_width() == from_->type->get_width());
    }
    catch (const type2t::symbolic_type_excp &)
    {
      /* ignore */
    }
  }
 
  bitcast2t(const bitcast2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &bitcast2t::from);
  static std::string field_names[esbmct::num_type_fields];
};

class if2t : public expr2t
{
public:
  expr2tc cond;
  expr2tc true_value;
  expr2tc false_value;
  locationt
    location; // not reflected: carries the ? position for witness branching
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);


   *  @param type Type this expression evaluates to.
   *  @param cond Condition to evaulate which side of ternary operator is used.
   *  @param trueval Value to use if cond evaluates to true.
   *  @param falseval Value to use if cond evaluates to false.
   *  @param loc Source location of the ? token (optional).
   */
  if2t(
    const type2tc &type,
    const expr2tc &cond_,
    const expr2tc &trueval,
    const expr2tc &falseval,
    const locationt &loc = locationt())
    : expr2t(type, if_id),
      cond(cond_),
      true_value(trueval),
      false_value(falseval),
      location(loc)
  {
    assert(type->type_id == trueval->type->type_id);
    assert(type->type_id == falseval->type->type_id);
  }
  if2t(const if2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &if2t::cond,
    &if2t::true_value,
    &if2t::false_value);
  static std::string field_names[esbmct::num_type_fields];
};

#define ESBMC_DEFINE_RELATION2T(name)                                          \
  class name##2t : public expr2t                                               \
  {                                                                            \
  public:                                                                      \
    expr2tc side_1, side_2;                                                    \
    name##2t(const expr2tc &v1, const expr2tc &v2)                             \
      : expr2t(get_bool_type(), name##_id), side_1(v1), side_2(v2)             \
    {                                                                          \
    }                                                                          \
    name##2t(const name##2t & ref) = default;                                  \
    expr2tc do_simplify() const override;                                      \
    static constexpr auto fields =                                             \
      std::make_tuple(&expr2t::type, &name##2t ::side_1, &name##2t ::side_2);  \
    static std::string field_names[esbmct::num_type_fields];                   \
  }
 
ESBMC_DEFINE_RELATION2T(equality);
ESBMC_DEFINE_RELATION2T(notequal);
ESBMC_DEFINE_RELATION2T(lessthan);
ESBMC_DEFINE_RELATION2T(greaterthan);
ESBMC_DEFINE_RELATION2T(lessthanequal);
ESBMC_DEFINE_RELATION2T(greaterthanequal);
#undef ESBMC_DEFINE_RELATION2T
 
/* The macros below fold sets of `*2t` classes that share a constructor
 * shape and behaviour. Each generated class still inherits directly
 * from expr2t and owns its own fields; the macro just spares the
 * repetition of writing six near-identical class bodies. */


/** Arithmetic two-operand node (`add`/`sub`/`mul`/`div`/`modulus`). */
#define ESBMC_DEFINE_ARITH_2OP(name)                                           \
  class name##2t : public expr2t                                               \
  {                                                                            \
  public:                                                                      \
    expr2tc side_1, side_2;                                                    \
    name##2t(const type2tc &type, const expr2tc &v1, const expr2tc &v2)        \
      : expr2t(type, name##_id), side_1(v1), side_2(v2)                        \
    {                                                                          \
      assert_arith_2ops_consistency(type, name##_id, v1, v2);                  \
    }                                                                          \
    name##2t(const name##2t & ref) = default;                                  \
    expr2tc do_simplify() const override;                                      \
    static constexpr auto fields =                                             \
      std::make_tuple(&expr2t::type, &name##2t ::side_1, &name##2t ::side_2);  \
    static std::string field_names[esbmct::num_type_fields];                   \
  }
 
ESBMC_DEFINE_ARITH_2OP(add);
ESBMC_DEFINE_ARITH_2OP(sub);
ESBMC_DEFINE_ARITH_2OP(mul);
ESBMC_DEFINE_ARITH_2OP(div);
ESBMC_DEFINE_ARITH_2OP(modulus);
#undef ESBMC_DEFINE_ARITH_2OP


 *  `shl`/`ashr`/`lshr`). */
#define ESBMC_DEFINE_BIT_2OP(name)                                             \
  class name##2t : public expr2t                                               \
  {                                                                            \
  public:                                                                      \
    expr2tc side_1, side_2;                                                    \
    name##2t(const type2tc &type, const expr2tc &v1, const expr2tc &v2)        \
      : expr2t(type, name##_id), side_1(v1), side_2(v2)                        \
    {                                                                          \
    }                                                                          \
    name##2t(const name##2t & ref) = default;                                  \
    expr2tc do_simplify() const override;                                      \
    static constexpr auto fields =                                             \
      std::make_tuple(&expr2t::type, &name##2t ::side_1, &name##2t ::side_2);  \
    static std::string field_names[esbmct::num_type_fields];                   \
  }
 
ESBMC_DEFINE_BIT_2OP(bitand);
ESBMC_DEFINE_BIT_2OP(bitor);
ESBMC_DEFINE_BIT_2OP(bitxor);
ESBMC_DEFINE_BIT_2OP(lshr);
ESBMC_DEFINE_BIT_2OP(shl);
ESBMC_DEFINE_BIT_2OP(ashr);
#undef ESBMC_DEFINE_BIT_2OP

#define ESBMC_DEFINE_ARITH_1OP(name)                                           \
  class name##2t : public expr2t                                               \
  {                                                                            \
  public:                                                                      \
    expr2tc value;                                                             \
    name##2t(const type2tc &type, const expr2tc &v)                            \
      : expr2t(type, name##_id), value(v)                                      \
    {                                                                          \
    }                                                                          \
    name##2t(const name##2t & ref) = default;                                  \
    expr2tc do_simplify() const override;                                      \
    static constexpr auto fields =                                             \
      std::make_tuple(&expr2t::type, &name##2t ::value);                       \
    static std::string field_names[esbmct::num_type_fields];                   \
  }
 
ESBMC_DEFINE_ARITH_1OP(neg);
ESBMC_DEFINE_ARITH_1OP(abs);
ESBMC_DEFINE_ARITH_1OP(bitnot);
ESBMC_DEFINE_ARITH_1OP(bswap);
#undef ESBMC_DEFINE_ARITH_1OP


#define ESBMC_DEFINE_POINTER_1OP(name)                                         \
  class name##2t : public expr2t                                               \
  {                                                                            \
  public:                                                                      \
    expr2tc ptr_obj;                                                           \
    name##2t(const type2tc &type, const expr2tc &v)                            \
      : expr2t(type, name##_id), ptr_obj(v)                                    \
    {                                                                          \
    }                                                                          \
    name##2t(const name##2t & ref) = default;                                  \
    expr2tc do_simplify() const override;                                      \
    static constexpr auto fields =                                             \
      std::make_tuple(&expr2t::type, &name##2t ::ptr_obj);                     \
    static std::string field_names[esbmct::num_type_fields];                   \
  }
 
ESBMC_DEFINE_POINTER_1OP(pointer_object);
ESBMC_DEFINE_POINTER_1OP(pointer_capability);
#undef ESBMC_DEFINE_POINTER_1OP

#define ESBMC_DEFINE_LOGIC_2OP(name)                                           \
  class name##2t : public expr2t                                               \
  {                                                                            \
  public:                                                                      \
    expr2tc side_1, side_2;                                                    \
    name##2t(const expr2tc &s1, const expr2tc &s2)                             \
      : expr2t(get_bool_type(), name##_id), side_1(s1), side_2(s2)             \
    {                                                                          \
    }                                                                          \
    name##2t(const name##2t & ref) = default;                                  \
    expr2tc do_simplify() const override;                                      \
    static constexpr auto fields =                                             \
      std::make_tuple(&expr2t::type, &name##2t ::side_1, &name##2t ::side_2);  \
    static std::string field_names[esbmct::num_type_fields];                   \
  }
 
ESBMC_DEFINE_LOGIC_2OP(and);
ESBMC_DEFINE_LOGIC_2OP(or);
ESBMC_DEFINE_LOGIC_2OP(xor);
ESBMC_DEFINE_LOGIC_2OP(implies);
ESBMC_DEFINE_LOGIC_2OP(isinstance);
ESBMC_DEFINE_LOGIC_2OP(hasattr);
ESBMC_DEFINE_LOGIC_2OP(isnone);
#undef ESBMC_DEFINE_LOGIC_2OP

#define ESBMC_DEFINE_FP_PREDICATE_1OP(name)                                    \
  class name##2t : public expr2t                                               \
  {                                                                            \
  public:                                                                      \
    expr2tc value;                                                             \
    name##2t(const expr2tc &operand)                                           \
      : expr2t(get_bool_type(), name##_id), value(operand)                     \
    {                                                                          \
    }                                                                          \
    name##2t(const name##2t & ref) = default;                                  \
    expr2tc do_simplify() const override;                                      \
    static constexpr auto fields = std::make_tuple(&name##2t ::value);         \
    static std::string field_names[esbmct::num_type_fields];                   \
  }
 
ESBMC_DEFINE_FP_PREDICATE_1OP(isnan);
ESBMC_DEFINE_FP_PREDICATE_1OP(isinf);
ESBMC_DEFINE_FP_PREDICATE_1OP(isnormal);
ESBMC_DEFINE_FP_PREDICATE_1OP(isfinite);
#undef ESBMC_DEFINE_FP_PREDICATE_1OP

#define ESBMC_DEFINE_OBJECT_PREDICATE_1OP(name)                                \
  class name##2t : public expr2t                                               \
  {                                                                            \
  public:                                                                      \
    expr2tc value;                                                             \
    name##2t(const expr2tc &operand)                                           \
      : expr2t(get_bool_type(), name##_id), value(operand)                     \
    {                                                                          \
    }                                                                          \
    name##2t(const name##2t & ref) = default;                                  \
    expr2tc do_simplify() const override;                                      \
    static constexpr auto fields = std::make_tuple(&name##2t ::value);         \
    static std::string field_names[esbmct::num_type_fields];                   \
  }
 
ESBMC_DEFINE_OBJECT_PREDICATE_1OP(valid_object);
ESBMC_DEFINE_OBJECT_PREDICATE_1OP(races_check);
ESBMC_DEFINE_OBJECT_PREDICATE_1OP(deallocated_obj);
#undef ESBMC_DEFINE_OBJECT_PREDICATE_1OP

#define ESBMC_DEFINE_OBJECT_SIZE_1OP(name)                                     \
  class name##2t : public expr2t                                               \
  {                                                                            \
  public:                                                                      \
    expr2tc value;                                                             \
    name##2t(const expr2tc &operand)                                           \
      : expr2t(size_type2(), name##_id), value(operand)                        \
    {                                                                          \
    }                                                                          \
    name##2t(const name##2t & ref) = default;                                  \
    expr2tc do_simplify() const override;                                      \
    static constexpr auto fields = std::make_tuple(&name##2t ::value);         \
    static std::string field_names[esbmct::num_type_fields];                   \
  }
 
ESBMC_DEFINE_OBJECT_SIZE_1OP(dynamic_size);
ESBMC_DEFINE_OBJECT_SIZE_1OP(capability_base);
ESBMC_DEFINE_OBJECT_SIZE_1OP(capability_top);
#undef ESBMC_DEFINE_OBJECT_SIZE_1OP

#define ESBMC_DEFINE_OVERFLOW_INT32_1OP(name)                                  \
  class name##2t : public expr2t                                               \
  {                                                                            \
  public:                                                                      \
    expr2tc operand;                                                           \
    name##2t(const expr2tc &op)                                                \
      : expr2t(get_int32_type(), name##_id), operand(op)                       \
    {                                                                          \
    }                                                                          \
    name##2t(const name##2t & ref) = default;                                  \
    expr2tc do_simplify() const override;                                      \
    static constexpr auto fields =                                             \
      std::make_tuple(&expr2t::type, &name##2t ::operand);                     \
    static std::string field_names[esbmct::num_type_fields];                   \
  }
 
ESBMC_DEFINE_OVERFLOW_INT32_1OP(signbit);
ESBMC_DEFINE_OVERFLOW_INT32_1OP(popcount);
#undef ESBMC_DEFINE_OVERFLOW_INT32_1OP

#define ESBMC_DEFINE_TYPE_ONLY(name)                                           \
  class name##2t : public expr2t                                               \
  {                                                                            \
  public:                                                                      \
    name##2t(const type2tc &type) : expr2t(type, name##_id)                    \
    {                                                                          \
    }                                                                          \
    name##2t(const name##2t & ref) = default;                                  \
    expr2tc do_simplify() const override;                                      \
    static constexpr auto fields = std::make_tuple(&expr2t::type);             \
    static std::string field_names[esbmct::num_type_fields];                   \
  }
 
ESBMC_DEFINE_TYPE_ONLY(unknown);
ESBMC_DEFINE_TYPE_ONLY(invalid);
ESBMC_DEFINE_TYPE_ONLY(null_object);
#undef ESBMC_DEFINE_TYPE_ONLY

#define ESBMC_DEFINE_CODE_EXPRESSION_1OP(name)                                 \
  class name##2t : public expr2t                                               \
  {                                                                            \
  public:                                                                      \
    expr2tc operand;                                                           \
    locationt location; /* not reflected: source loc travels with the stmt */  \
    static constexpr std::size_t excluded_field_bytes = sizeof(locationt);     \
    name##2t(const expr2tc &op, const locationt &loc = locationt())            \
      : expr2t(get_empty_type(), name##_id), operand(op), location(loc)        \
    {                                                                          \
    }                                                                          \
    name##2t(const name##2t & ref) = default;                                  \
    expr2tc do_simplify() const override;                                      \
    static constexpr auto fields = std::make_tuple(&name##2t ::operand);       \
    static std::string field_names[esbmct::num_type_fields];                   \
  }
 
ESBMC_DEFINE_CODE_EXPRESSION_1OP(code_expression);
ESBMC_DEFINE_CODE_EXPRESSION_1OP(code_return);
ESBMC_DEFINE_CODE_EXPRESSION_1OP(code_free);
ESBMC_DEFINE_CODE_EXPRESSION_1OP(code_cpp_del_array);
ESBMC_DEFINE_CODE_EXPRESSION_1OP(code_cpp_delete);
#undef ESBMC_DEFINE_CODE_EXPRESSION_1OP

#define ESBMC_DEFINE_CODE_DECL(name)                                           \
  class name##2t : public expr2t                                               \
  {                                                                            \
  public:                                                                      \
    irep_idt value;                                                            \
    locationt location; /* not reflected: source loc travels with the stmt */  \
    static constexpr std::size_t excluded_field_bytes = sizeof(locationt);     \
    name##2t(                                                                  \
      const type2tc &type,                                                     \
      const irep_idt &n,                                                       \
      const locationt &loc = locationt())                                      \
      : expr2t(type, name##_id), value(n), location(loc)                       \
    {                                                                          \
    }                                                                          \
    name##2t(const name##2t & ref) = default;                                  \
    expr2tc do_simplify() const override;                                      \
    static constexpr auto fields =                                             \
      std::make_tuple(&expr2t::type, &name##2t ::value);                       \
    static std::string field_names[esbmct::num_type_fields];                   \
  }
 
ESBMC_DEFINE_CODE_DECL(code_dead);
#undef ESBMC_DEFINE_CODE_DECL

class code_decl2t : public expr2t
{
public:
  irep_idt value;     // symbol name
  expr2tc init;       // optional initializer; nil when absent
  locationt location; // not reflected: source loc travels with the stmt
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
  code_decl2t(
    const type2tc &type,
    const irep_idt &n,
    const expr2tc &i = expr2tc(),
    const locationt &loc = locationt())
    : expr2t(type, code_decl_id), value(n), init(i), location(loc)
  {
  }
  code_decl2t(const code_decl2t &ref) = default;
  expr2tc do_simplify() const override;
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &code_decl2t::value, &code_decl2t::init);
  static std::string field_names[esbmct::num_type_fields];
};

class cmp_three_way2t : public expr2t
{
public:
  expr2tc side_1;
  expr2tc side_2;
 
  cmp_three_way2t(const type2tc &t, const expr2tc &v1, const expr2tc &v2)
    : expr2t(t, cmp_three_way_id), side_1(v1), side_2(v2)
  {
  }
  cmp_three_way2t(const cmp_three_way2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &cmp_three_way2t::side_1,
    &cmp_three_way2t::side_2);
  static std::string field_names[esbmct::num_type_fields];
};

class not2t : public expr2t
{
public:
  expr2tc value;

  not2t(const expr2tc &val) : expr2t(get_bool_type(), not_id), value(val)
  {
  }
  not2t(const not2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields = std::make_tuple(&not2t::value);
  static std::string field_names[esbmct::num_type_fields];
};

#define ESBMC_DEFINE_IEEE_ARITH_2OP(name)                                      \
  class name##2t : public expr2t                                               \
  {                                                                            \
  public:                                                                      \
    expr2tc rounding_mode, side_1, side_2;                                     \
    name##2t(                                                                  \
      const type2tc &type,                                                     \
      const expr2tc &v1,                                                       \
      const expr2tc &v2,                                                       \
      const expr2tc &rm)                                                       \
      : expr2t(type, name##_id), rounding_mode(rm), side_1(v1), side_2(v2)     \
    {                                                                          \
    }                                                                          \
    name##2t(const name##2t & ref) = default;                                  \
    expr2tc do_simplify() const override;                                      \
    static constexpr auto fields = std::make_tuple(                            \
      &expr2t::type,                                                           \
      &name##2t ::rounding_mode,                                               \
      &name##2t ::side_1,                                                      \
      &name##2t ::side_2);                                                     \
    static std::string field_names[esbmct::num_type_fields];                   \
  }
 
ESBMC_DEFINE_IEEE_ARITH_2OP(ieee_add);
ESBMC_DEFINE_IEEE_ARITH_2OP(ieee_sub);
ESBMC_DEFINE_IEEE_ARITH_2OP(ieee_mul);
ESBMC_DEFINE_IEEE_ARITH_2OP(ieee_div);
ESBMC_DEFINE_IEEE_ARITH_2OP(ieee_rem);
#undef ESBMC_DEFINE_IEEE_ARITH_2OP

class ieee_fma2t : public expr2t
{
public:
  expr2tc rounding_mode;
  expr2tc value_1;
  expr2tc value_2;
  expr2tc value_3;

  ieee_fma2t(
    const type2tc &type,
    const expr2tc &v1,
    const expr2tc &v2,
    const expr2tc &v3,
    const expr2tc &rm)
    : expr2t(type, ieee_fma_id),
      rounding_mode(rm),
      value_1(v1),
      value_2(v2),
      value_3(v3)
  {
  }
  ieee_fma2t(const ieee_fma2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &ieee_fma2t::value_1,
    &ieee_fma2t::value_2,
    &ieee_fma2t::value_3,
    &ieee_fma2t::rounding_mode);
  static std::string field_names[esbmct::num_type_fields];
};

class ieee_sqrt2t : public expr2t
{
public:
  expr2tc rounding_mode;
  expr2tc value;

  ieee_sqrt2t(const type2tc &type, const expr2tc &v1, const expr2tc &rm)
    : expr2t(type, ieee_sqrt_id), rounding_mode(rm), value(v1)
  {
  }
  ieee_sqrt2t(const ieee_sqrt2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &ieee_sqrt2t::value,
    &ieee_sqrt2t::rounding_mode);
  static std::string field_names[esbmct::num_type_fields];
};

class same_object2t : public expr2t
{
public:
  expr2tc side_1;
  expr2tc side_2;

  same_object2t(const expr2tc &v1, const expr2tc &v2)
    : expr2t(get_bool_type(), same_object_id), side_1(v1), side_2(v2)
  {
  }
  same_object2t(const same_object2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &same_object2t::side_1,
    &same_object2t::side_2);
  static std::string field_names[esbmct::num_type_fields];
};

class pointer_offset2t : public expr2t
{
public:
  expr2tc ptr_obj;

  pointer_offset2t(const type2tc &type, const expr2tc &ptrobj)
    : expr2t(type, pointer_offset_id), ptr_obj(ptrobj)
  {
    assert(type->type_id == type2t::signedbv_id);
    assert(type->get_width() == config.ansi_c.address_width);
  }
  pointer_offset2t(const pointer_offset2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &pointer_offset2t::ptr_obj);
  static std::string field_names[esbmct::num_type_fields];
};

class address_of2t : public expr2t
{
public:
  expr2tc ptr_obj;

  bool implicit;
 
  address_of2t(
    const type2tc &subtype,
    const expr2tc &ptrobj,
    bool is_implicit = false,
    pointer_ref_kindt rk = pointer_ref_kindt::NONE)
    : expr2t(pointer_type2tc(subtype, false, rk), address_of_id),
      ptr_obj(ptrobj),
      implicit(is_implicit)
  {
    assert(ptrobj->expr_id != expr2t::constant_int_id);
    assert(ptrobj->expr_id != expr2t::address_of_id);
  }
  address_of2t(const address_of2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &address_of2t::ptr_obj,
    &address_of2t::implicit);
  static std::string field_names[esbmct::num_type_fields];
};

class byte_extract2t : public expr2t
{
public:
  expr2tc source_value;
  expr2tc source_offset;
  bool big_endian;

  byte_extract2t(
    const type2tc &type,
    const expr2tc &source,
    const expr2tc &offset,
    bool is_big_endian)
    : expr2t(type, byte_extract_id),
      source_value(source),
      source_offset(offset),
      big_endian(is_big_endian)
  {
  }
  byte_extract2t(const byte_extract2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &byte_extract2t::source_value,
    &byte_extract2t::source_offset,
    &byte_extract2t::big_endian);
  static std::string field_names[esbmct::num_type_fields];
};

class byte_update2t : public expr2t
{
public:
  expr2tc source_value;
  expr2tc source_offset;
  expr2tc update_value;
  bool big_endian;

  byte_update2t(
    const type2tc &type,
    const expr2tc &source,
    const expr2tc &offset,
    const expr2tc &updateval,
    bool is_big_endian)
    : expr2t(type, byte_update_id),
      source_value(source),
      source_offset(offset),
      update_value(updateval),
      big_endian(is_big_endian)
  {
  }
  byte_update2t(const byte_update2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &byte_update2t::source_value,
    &byte_update2t::source_offset,
    &byte_update2t::update_value,
    &byte_update2t::big_endian);
  static std::string field_names[esbmct::num_type_fields];
};

class with2t : public expr2t
{
  void assert_consistency() const;
 
public:
  expr2tc source_value;
  expr2tc update_field;
  expr2tc update_value;

  with2t(
    const type2tc &type,
    const expr2tc &source,
    const expr2tc &field,
    const expr2tc &value)
    : expr2t(type, with_id),
      source_value(source),
      update_field(field),
      update_value(value)
  {
#ifndef NDEBUG
    assert_consistency();
#endif
  }
  with2t(const with2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &with2t::source_value,
    &with2t::update_field,
    &with2t::update_value);
  static std::string field_names[esbmct::num_type_fields];
};

class member2t : public expr2t
{
public:
  expr2tc source_value;
  irep_idt member;

  member2t(const type2tc &type, const expr2tc &source, const irep_idt &memb)
    : expr2t(type, member_id), source_value(source), member(memb)
  {
#ifndef NDEBUG /* only check consistency in non-Release builds */
    /* The source is normally a resolved struct/union/complex. A `symbol_id`
       source is permitted ONLY as a transient pre-resolution state: the
       IREP2-migration V.1k "two-phase source invariant" lets a frontend build a
       member2t before type resolution (the Python converter, ahead of the
       IREP2-native adjuster) hand a by-name `symbol_type2t` here; the adjuster
       MUST follow it to a struct before symex. The strong invariant is
       re-enforced post-adjust by that pass, not dropped. No existing frontend
       builds member2t pre-adjust (all go through migrate at goto-convert, which
       is post-adjust), so this disjunct is staged enabling infra, exercised
       once the V.1k converter/adjuster pilot lands. */
    /* A `pointer_id` source is the same transient state index2t already
       permits, and for the same reason: a legacy `member` over a pointer base
       is what the C adjuster's adjust_member rewrites to
       `member(dereference(base))`, so migrating a symbol value before that arm
       has run hands one here. index2t's sibling comment names this pairing; the
       relaxation had been applied there and not here. An `array_id` source is
       the same thing for adjust_member other branch, which rewrites an array
       base to `member(index(base, 0))`. */
    assert(
      source->type->type_id == type2t::struct_id ||
      source->type->type_id == type2t::union_id ||
      source->type->type_id == type2t::complex_id ||
      source->type->type_id == type2t::symbol_id ||
      source->type->type_id == type2t::pointer_id ||
      source->type->type_id == type2t::array_id);
    /* member must exist exactly once in the parent struct/union — only
       checkable once the source type is resolved (skipped for the transient
       cases above; the lookup throws on an unresolved source -- without that
       guard `python2goto` cannot build the Python OM library, §162.2).
 
       A code-typed member is the exception, and it is checked the other way
       round: it names a method, methods are no part of a struct_type2t, so it
       must NOT resolve to a component. What verifies such a member exists at
       all is upstream, where a namespace is in hand --
       clang_cpp_adjust_irep2::adjust_cpp_member looks it up by name and asserts
       the symbol is code (docs/roadmap/frontends-to-irep2.md §76). */
    if (
      source->type->type_id != type2t::symbol_id &&
      source->type->type_id != type2t::pointer_id &&
      source->type->type_id != type2t::array_id)
      assert(
        struct_union_get_component_number(source->type, memb).has_value() ==
        (type->type_id != type2t::code_id));
#endif
  }
  member2t(const member2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &member2t::source_value, &member2t::member);
  static std::string field_names[esbmct::num_type_fields];
};

class member_ref2t : public expr2t
{
public:
  irep_idt member;

  member_ref2t(const type2tc &type, const irep_idt &memb)
    : expr2t(type, member_ref_id), member(memb)
  {
  }
  member_ref2t(const member_ref2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &member_ref2t::member);
  static std::string field_names[esbmct::num_type_fields];
};

class ptr_mem2t : public expr2t
{
public:
  expr2tc source_value;
  expr2tc member_pointer;

  ptr_mem2t(const type2tc &type, const expr2tc &source, const expr2tc &pointer)
    : expr2t(type, ptr_mem_id), source_value(source), member_pointer(pointer)
  {
  }
  ptr_mem2t(const ptr_mem2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &ptr_mem2t::source_value,
    &ptr_mem2t::member_pointer);
  static std::string field_names[esbmct::num_type_fields];
};

class index2t : public expr2t
{
public:
  expr2tc source_value;
  expr2tc index;

  index2t(const type2tc &type, const expr2tc &source, const expr2tc &idx)
    : expr2t(type, index_id), source_value(source), index(idx)
  {
    /* A `symbol_id` or `pointer_id` source is permitted only as a transient
       pre-resolution state (V.1k two-phase source invariant, see member2t
       above); the IREP2-native adjuster resolves a symbol source to an
       array/vector and rewrites a pointer source `p[i]` to `*(p+i)` before
       symex. A pointer source arises when a legacy `index` over a decayed
       array (a Python string, char*) is migrated via get_value2(). */
    assert(
      is_array_type(source) || is_vector_type(source) ||
      source->type->type_id == type2t::symbol_id ||
      source->type->type_id == type2t::pointer_id);
  }
  index2t(const index2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &index2t::source_value, &index2t::index);
  static std::string field_names[esbmct::num_type_fields];
};

class overflow2t : public expr2t
{
public:
  expr2tc operand;

  overflow2t(const expr2tc &operand_)
    : expr2t(get_bool_type(), overflow_id), operand(operand_)
  {
  }
  overflow2t(const overflow2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &overflow2t::operand);
  static std::string field_names[esbmct::num_type_fields];
};

class overflow_cast2t : public expr2t
{
public:
  expr2tc operand;
  unsigned int bits;

  overflow_cast2t(const expr2tc &operand_, unsigned int bits_)
    : expr2t(get_bool_type(), overflow_cast_id), operand(operand_), bits(bits_)
  {
  }
  overflow_cast2t(const overflow_cast2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &overflow_cast2t::operand,
    &overflow_cast2t::bits);
  static std::string field_names[esbmct::num_type_fields];
};

class overflow_neg2t : public expr2t
{
public:
  expr2tc operand;

  overflow_neg2t(const expr2tc &operand_)
    : expr2t(get_bool_type(), overflow_neg_id), operand(operand_)
  {
  }
  overflow_neg2t(const overflow_neg2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &overflow_neg2t::operand);
  static std::string field_names[esbmct::num_type_fields];
};

class dynamic_object2t : public expr2t
{
public:
  expr2tc instance;
  bool invalid;
  bool unknown;
 
  dynamic_object2t(
    const type2tc &type,
    const expr2tc &inst,
    bool inv,
    bool uknown)
    : expr2t(type, dynamic_object_id),
      instance(inst),
      invalid(inv),
      unknown(uknown)
  {
  }
  dynamic_object2t(const dynamic_object2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &dynamic_object2t::instance,
    &dynamic_object2t::invalid,
    &dynamic_object2t::unknown);
  static std::string field_names[esbmct::num_type_fields];
};

class dereference2t : public expr2t
{
public:
  expr2tc value;

  dereference2t(const type2tc &type, const expr2tc &operand)
    : expr2t(type, dereference_id), value(operand)
  {
  }
  dereference2t(const dereference2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &dereference2t::value);
  static std::string field_names[esbmct::num_type_fields];
};

class sideeffect2t : public expr2t
{
public:
  using allockind = sideeffect_allockind;
 
  expr2tc operand;
  expr2tc size;
  std::vector<expr2tc> arguments;
  type2tc alloctype;
  sideeffect_allockind kind;

  bool constructor;
 
  locationt location; // not reflected: source loc travels with the stmt
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);

  sideeffect2t(
    const type2tc &t,
    const expr2tc &oper,
    const expr2tc &sz,
    const std::vector<expr2tc> &a,
    const type2tc &alloct,
    sideeffect_allockind k,
    const locationt &loc = locationt(),
    bool ctor = false)
    : expr2t(t, sideeffect_id),
      operand(oper),
      size(sz),
      arguments(a),
      alloctype(alloct),
      kind(k),
      constructor(ctor),
      location(loc)
  {
    if (k == sideeffect_allockind::alloca)
      assert(oper->type == sz->type);
  }
  sideeffect2t(const sideeffect2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &sideeffect2t::operand,
    &sideeffect2t::size,
    &sideeffect2t::arguments,
    &sideeffect2t::alloctype,
    &sideeffect2t::kind);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_block2t : public expr2t
{
public:
  std::vector<expr2tc> operands;
  locationt location; // not reflected: source loc travels with the stmt
  // not reflected: the closing-brace location travels with the block too, so a
  // code_block2t consumed natively by goto_convert (W1, esbmc/esbmc#4715) keeps
  // the end location convert_block needs for destructor placement.
  locationt end_location;
  static constexpr std::size_t excluded_field_bytes = 2 * sizeof(locationt);
 
  code_block2t(
    const std::vector<expr2tc> &ops,
    const locationt &loc = locationt(),
    const locationt &end_loc = locationt())
    : expr2t(get_empty_type(), code_block_id),
      operands(ops),
      location(loc),
      end_location(end_loc)
  {
  }
  code_block2t(const code_block2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &code_block2t::operands);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_assign2t : public expr2t
{
public:
  expr2tc target;
  expr2tc source;
  locationt location; // not reflected: source loc travels with the stmt
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
 
  code_assign2t(
    const expr2tc &tgt,
    const expr2tc &src,
    const locationt &loc = locationt())
    : expr2t(get_empty_type(), code_assign_id),
      target(tgt),
      source(src),
      location(loc)
  {
  }
  code_assign2t(const code_assign2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &code_assign2t::target,
    &code_assign2t::source);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_printf2t : public expr2t
{
public:
  std::vector<expr2tc> operands;
  printf_kindt kind;
  locationt location; // not reflected: source loc travels with the stmt
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
 
  code_printf2t(
    const std::vector<expr2tc> &opers,
    printf_kindt k,
    const locationt &loc = locationt())
    : expr2t(get_empty_type(), code_printf_id),
      operands(opers),
      kind(k),
      location(loc)
  {
  }
  code_printf2t(const code_printf2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &code_printf2t::operands,
    &code_printf2t::kind);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_skip2t : public expr2t
{
public:
  locationt location; // not reflected: source loc travels with the stmt
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
  code_skip2t(const type2tc &type, const locationt &loc = locationt())
    : expr2t(type, code_skip_id), location(loc)
  {
  }
  code_skip2t(const code_skip2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(&expr2t::type);
  static std::string field_names[esbmct::num_type_fields];
};

class new_object2t : public expr2t
{
public:
  new_object2t(const type2tc &type) : expr2t(type, new_object_id)
  {
  }
  new_object2t(const new_object2t &ref) = default;
 
  expr2tc do_simplify() const override;
  static constexpr auto fields = std::make_tuple(&expr2t::type);
  static std::string field_names[esbmct::num_type_fields];
};

class uninterpreted_func2t : public expr2t
{
public:
  irep_idt function_name;
  std::vector<expr2tc> arguments;
 
  uninterpreted_func2t(
    const type2tc &type,
    const irep_idt &name,
    const std::vector<expr2tc> &args)
    : expr2t(type, uninterpreted_func_id), function_name(name), arguments(args)
  {
  }
  uninterpreted_func2t(const uninterpreted_func2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &uninterpreted_func2t::function_name,
    &uninterpreted_func2t::arguments);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_goto2t : public expr2t
{
public:
  irep_idt target;
  locationt location; // not reflected: source loc travels with the stmt
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
 
  code_goto2t(const irep_idt &targ, const locationt &loc = locationt())
    : expr2t(get_empty_type(), code_goto_id), target(targ), location(loc)
  {
  }
  code_goto2t(const code_goto2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &code_goto2t::target);
  static std::string field_names[esbmct::num_type_fields];
};
 
class object_descriptor2t : public expr2t
{
public:
  expr2tc object;
  expr2tc offset;
  unsigned int alignment;
 
  object_descriptor2t(
    const type2tc &t,
    const expr2tc &root,
    const expr2tc &offs,
    unsigned int align)
    : expr2t(t, object_descriptor_id),
      object(root),
      offset(offs),
      alignment(align)
  {
  }
  object_descriptor2t(const object_descriptor2t &ref) = default;
 
  const expr2tc &get_root_object() const;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &object_descriptor2t::object,
    &object_descriptor2t::offset,
    &object_descriptor2t::alignment);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_function_call2t : public expr2t
{
public:
  expr2tc ret;
  expr2tc function;
  std::vector<expr2tc> operands;
  locationt location; // not reflected: source loc travels with the stmt
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
 
  code_function_call2t(
    const expr2tc &r,
    const expr2tc &func,
    const std::vector<expr2tc> &args,
    const locationt &loc = locationt())
    : expr2t(get_empty_type(), code_function_call_id),
      ret(r),
      function(func),
      operands(args),
      location(loc)
  {
  }
  code_function_call2t(const code_function_call2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &code_function_call2t::ret,
    &code_function_call2t::function,
    &code_function_call2t::operands);
  static std::string field_names[esbmct::num_type_fields];
};
 
// V.4 (esbmc/esbmc#4715): structured control-flow code kinds. IREP2 had only
// the flat goto-level code kinds; these mirror the legacy structured codet
// statements (ifthenelse/while/for/switch/break/continue/label) so the
// frontend can build IREP2 bodies and goto_convert can consume them, removing
// the per-instruction back-migration at the body seam (wall W1). Shipped
// dead-but-tested first: nothing builds them until the goto_convert wiring
// phase, so they are behaviour-inert and only the round-trip unit tests
// exercise them (the V-track pattern).
//
// V.4.1: each kind carries a `locationt location` so a future IREP2-native
// goto_convert can stamp each instruction's source location -- the legacy
// codet carries it on the node, but expr2t/migrate do not, so an IREP2 body
// would otherwise lose all counterexample line numbers. The field is
// deliberately NOT part of the `fields` tuple, so it does not enter the IREP2
// hash/equality (matching how a goto instructiont stores its locationt
// separately); it is preserved through clone() by the defaulted copy ctor and
// threaded by hand in migrate (forward copies code.location(), back restores
// it).
class code_ifthenelse2t : public expr2t
{
public:
  expr2tc cond;
  expr2tc then_case;
  expr2tc else_case;  // nil when there is no else branch
  locationt location; // not reflected (see note above)
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
 
  code_ifthenelse2t(
    const expr2tc &c,
    const expr2tc &t,
    const expr2tc &e,
    const locationt &loc = locationt())
    : expr2t(get_empty_type(), code_ifthenelse_id),
      cond(c),
      then_case(t),
      else_case(e),
      location(loc)
  {
  }
  code_ifthenelse2t(const code_ifthenelse2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &code_ifthenelse2t::cond,
    &code_ifthenelse2t::then_case,
    &code_ifthenelse2t::else_case);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_while2t : public expr2t
{
public:
  expr2tc cond;
  expr2tc body;
  locationt location; // not reflected (see note above)
  // `#pragma unroll N` count: travels with the loop statement so the
  // --irep2-bodies round-trip preserves the per-loop unwind bound that
  // goto_convert later stamps onto the loop's GOTO instruction. Not
  // reflected, so it stays out of value identity (like `location`).
  unsigned pragma_unroll_count;
  static constexpr std::size_t excluded_field_bytes =
    sizeof(locationt) + sizeof(unsigned);
 
  code_while2t(
    const expr2tc &c,
    const expr2tc &b,
    const locationt &loc = locationt(),
    unsigned pragma = 0)
    : expr2t(get_empty_type(), code_while_id),
      cond(c),
      body(b),
      location(loc),
      pragma_unroll_count(pragma)
  {
  }
  code_while2t(const code_while2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &code_while2t::cond, &code_while2t::body);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_dowhile2t : public expr2t
{
public:
  expr2tc cond;
  expr2tc body;
  locationt location; // not reflected (see note above)
  // `#pragma unroll N` count (see code_while2t).
  unsigned pragma_unroll_count;
  static constexpr std::size_t excluded_field_bytes =
    sizeof(locationt) + sizeof(unsigned);
 
  code_dowhile2t(
    const expr2tc &c,
    const expr2tc &b,
    const locationt &loc = locationt(),
    unsigned pragma = 0)
    : expr2t(get_empty_type(), code_dowhile_id),
      cond(c),
      body(b),
      location(loc),
      pragma_unroll_count(pragma)
  {
  }
  code_dowhile2t(const code_dowhile2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &code_dowhile2t::cond,
    &code_dowhile2t::body);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_for2t : public expr2t
{
public:
  expr2tc init; // nil when absent
  expr2tc cond; // nil when absent
  expr2tc iter; // nil when absent
  expr2tc body;
  locationt location; // not reflected (see note above)
  // `#pragma unroll N` count (see code_while2t).
  unsigned pragma_unroll_count;
  static constexpr std::size_t excluded_field_bytes =
    sizeof(locationt) + sizeof(unsigned);
 
  code_for2t(
    const expr2tc &i,
    const expr2tc &c,
    const expr2tc &it,
    const expr2tc &b,
    const locationt &loc = locationt(),
    unsigned pragma = 0)
    : expr2t(get_empty_type(), code_for_id),
      init(i),
      cond(c),
      iter(it),
      body(b),
      location(loc),
      pragma_unroll_count(pragma)
  {
  }
  code_for2t(const code_for2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &code_for2t::init,
    &code_for2t::cond,
    &code_for2t::iter,
    &code_for2t::body);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_switch2t : public expr2t
{
public:
  expr2tc value;
  expr2tc body;
  locationt location; // not reflected (see note above)
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
 
  code_switch2t(
    const expr2tc &v,
    const expr2tc &b,
    const locationt &loc = locationt())
    : expr2t(get_empty_type(), code_switch_id), value(v), body(b), location(loc)
  {
  }
  code_switch2t(const code_switch2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &code_switch2t::value, &code_switch2t::body);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_break2t : public expr2t
{
public:
  locationt location; // not reflected (see note above)
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
 
  code_break2t(const locationt &loc = locationt())
    : expr2t(get_empty_type(), code_break_id), location(loc)
  {
  }
  code_break2t(const code_break2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(&expr2t::type);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_continue2t : public expr2t
{
public:
  locationt location; // not reflected (see note above)
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
 
  code_continue2t(const locationt &loc = locationt())
    : expr2t(get_empty_type(), code_continue_id), location(loc)
  {
  }
  code_continue2t(const code_continue2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(&expr2t::type);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_label2t : public expr2t
{
public:
  irep_idt label;
  expr2tc code;
  locationt location; // not reflected (see note above)
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
 
  code_label2t(
    const irep_idt &l,
    const expr2tc &c,
    const locationt &loc = locationt())
    : expr2t(get_empty_type(), code_label_id), label(l), code(c), location(loc)
  {
  }
  code_label2t(const code_label2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &code_label2t::label, &code_label2t::code);
  static std::string field_names[esbmct::num_type_fields];
};

class code_switch_case2t : public expr2t
{
public:
  bool is_default;
  expr2tc case_op;    // nil when is_default
  expr2tc case_op_hi; // GNU `case lo ... hi:` upper bound; nil otherwise
  expr2tc code;
  locationt location; // not reflected (see note above)
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
 
  code_switch_case2t(
    bool _is_default,
    const expr2tc &_case_op,
    const expr2tc &_code,
    const locationt &loc = locationt(),
    const expr2tc &_case_op_hi = expr2tc())
    : expr2t(get_empty_type(), code_switch_case_id),
      is_default(_is_default),
      case_op(_case_op),
      case_op_hi(_case_op_hi),
      code(_code),
      location(loc)
  {
  }
  code_switch_case2t(const code_switch_case2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &code_switch_case2t::is_default,
    &code_switch_case2t::case_op,
    &code_switch_case2t::case_op_hi,
    &code_switch_case2t::code);
  static std::string field_names[esbmct::num_type_fields];
};

class code_assert2t : public expr2t
{
public:
  expr2tc guard;
  locationt location; // not reflected (see note above)
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
 
  code_assert2t(const expr2tc &g, const locationt &loc = locationt())
    : expr2t(get_empty_type(), code_assert_id), guard(g), location(loc)
  {
  }
  code_assert2t(const code_assert2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &code_assert2t::guard);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_assume2t : public expr2t
{
public:
  expr2tc guard;
  locationt location; // not reflected (see note above)
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
 
  code_assume2t(const expr2tc &g, const locationt &loc = locationt())
    : expr2t(get_empty_type(), code_assume_id), guard(g), location(loc)
  {
  }
  code_assume2t(const code_assume2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &code_assume2t::guard);
  static std::string field_names[esbmct::num_type_fields];
};

class sideeffect_assign2t : public expr2t
{
public:
  irep_idt op; // "assign", "assign+", "assign-", "assign*", etc.

  bool member_init;
 
  expr2tc lhs;
  expr2tc rhs;
  locationt location; // not reflected: source loc travels with the stmt
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
 
  sideeffect_assign2t(
    const type2tc &t,
    const irep_idt &o,
    const expr2tc &l,
    const expr2tc &r,
    const locationt &loc = locationt(),
    bool member_init_ = false)
    : expr2t(t, sideeffect_assign_id),
      op(o),
      member_init(member_init_),
      lhs(l),
      rhs(r),
      location(loc)
  {
  }
  sideeffect_assign2t(const sideeffect_assign2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &sideeffect_assign2t::op,
    &sideeffect_assign2t::lhs,
    &sideeffect_assign2t::rhs);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_comma2t : public expr2t
{
public:
  expr2tc side_1;
  expr2tc side_2;
 
  code_comma2t(const type2tc &t, const expr2tc &s1, const expr2tc &s2)
    : expr2t(t, code_comma_id), side_1(s1), side_2(s2)
  {
  }
  code_comma2t(const code_comma2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &code_comma2t::side_1,
    &code_comma2t::side_2);
  static std::string field_names[esbmct::num_type_fields];
};
 
class invalid_pointer2t : public expr2t
{
public:
  expr2tc ptr_obj;
 
  invalid_pointer2t(const expr2tc &obj)
    : expr2t(get_bool_type(), invalid_pointer_id), ptr_obj(obj)
  {
  }
  invalid_pointer2t(const invalid_pointer2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(&invalid_pointer2t::ptr_obj);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_asm2t : public expr2t
{
public:
  irep_idt value;
  locationt location; // not reflected: source loc travels with the stmt
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
 
  code_asm2t(
    const type2tc &type,
    const irep_idt &stringref,
    const locationt &loc = locationt())
    : expr2t(type, code_asm_id), value(stringref), location(loc)
  {
  }
  code_asm2t(const code_asm2t &ref) = default;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &code_asm2t::value);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_cpp_catch2t : public expr2t
{
public:
  std::vector<irep_idt> exception_list;
  // Source-level try/catch operands: operands[0] is the try block, operands
  // [1..N] the catch-handler blocks (parallel to exception_list). Empty for
  // the post-goto-convert CATCH-push/pop marker instructions, which carry only
  // the catchable-type list. Retained so a try/catch body survives the
  // --irep2-bodies round-trip (esbmc/esbmc#4715); convert_catch reads it back.
  std::vector<expr2tc> operands;
  locationt location; // not reflected: source loc travels with the stmt
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
 
  code_cpp_catch2t(
    const std::vector<irep_idt> &el,
    const locationt &loc = locationt())
    : expr2t(get_empty_type(), code_cpp_catch_id),
      exception_list(el),
      location(loc)
  {
  }
  code_cpp_catch2t(
    const std::vector<irep_idt> &el,
    const std::vector<expr2tc> &ops,
    const locationt &loc = locationt())
    : expr2t(get_empty_type(), code_cpp_catch_id),
      exception_list(el),
      operands(ops),
      location(loc)
  {
  }
  code_cpp_catch2t(const code_cpp_catch2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &code_cpp_catch2t::exception_list,
    &code_cpp_catch2t::operands);
  static std::string field_names[esbmct::num_type_fields];
};
 
class code_cpp_throw2t : public expr2t
{
public:
  expr2tc operand;
  std::vector<irep_idt> exception_list;
  locationt location; // not reflected: source loc travels with the stmt
  static constexpr std::size_t excluded_field_bytes = sizeof(locationt);
 
  code_cpp_throw2t(
    const expr2tc &o,
    const std::vector<irep_idt> &l,
    const locationt &loc = locationt())
    : expr2t(get_empty_type(), code_cpp_throw_id),
      operand(o),
      exception_list(l),
      location(loc)
  {
  }
  code_cpp_throw2t(const code_cpp_throw2t &ref) = default;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &code_cpp_throw2t::operand,
    &code_cpp_throw2t::exception_list);
  static std::string field_names[esbmct::num_type_fields];
};

class concat2t : public expr2t
{
public:
  expr2tc side_1;
  expr2tc side_2;
 
  concat2t(const type2tc &type, const expr2tc &forward, const expr2tc &aft)
    : expr2t(type, concat_id), side_1(forward), side_2(aft)
  {
    assert(is_unsignedbv_type(forward));
    assert(is_unsignedbv_type(aft));
  }
  concat2t(const concat2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &concat2t::side_1, &concat2t::side_2);
  static std::string field_names[esbmct::num_type_fields];
};
 
class extract2t : public expr2t
{
public:
  expr2tc from;
  unsigned int upper;
  unsigned int lower;
 
  extract2t(
    const type2tc &type,
    const expr2tc &from_,
    unsigned int upper_,
    unsigned int lower_)
    : expr2t(type, extract_id), from(from_), upper(upper_), lower(lower_)
  {
  }
  extract2t(const extract2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields = std::make_tuple(
    &expr2t::type,
    &extract2t::from,
    &extract2t::upper,
    &extract2t::lower);
  static std::string field_names[esbmct::num_type_fields];
};

class sizeof2t : public expr2t
{
public:
  expr2tc value;
  type2tc sizeof_type;
 
  sizeof2t(const type2tc &type, const expr2tc &val, const type2tc &sizeof_t)
    : expr2t(type, sizeof_id), value(val), sizeof_type(sizeof_t)
  {
  }
  sizeof2t(const sizeof2t &ref) = default;
 
  expr2tc do_simplify() const override;
 
  static constexpr auto fields =
    std::make_tuple(&expr2t::type, &sizeof2t::value, &sizeof2t::sizeof_type);
  static std::string field_names[esbmct::num_type_fields];
};
 
// Same deal as for "type_macros": is_<name>2t predicates plus to_<name>2t
// downcasts routed through irep2_checked_expr_cast so a bad to_*2t throws
// irep2_cast_error in every build mode.
#define expr_macros(name)                                                      \
  inline bool is_##name##2t(const expr2tc &t)                                  \
  {                                                                            \
    return t->expr_id == expr2t::name##_id;                                    \
  }                                                                            \
  inline const name##2t & to_##name##2t(const expr2tc &t)                      \
  {                                                                            \
    return irep2_checked_expr_cast<const name##2t>(                            \
      *t, expr2t::name##_id, #name);                                           \
  }                                                                            \
  inline name##2t & to_##name##2t(expr2tc & t)                                 \
  {                                                                            \
    return irep2_checked_expr_cast<name##2t>(                                  \
      *t.get(), expr2t::name##_id, #name);                                     \
  }                                                                            \
  inline const name##2t * try_to_##name##2t(const expr2tc &t)                  \
  {                                                                            \
    return is_##name##2t(t) ? &to_##name##2t(t) : nullptr;                     \
  }
 
// Instantiate the is_/to_/try_to_ predicate triple for every kind in
// expr_kinds.inc. Same manifest as the enum and forward declarations
// above, so adding a kind is a single line there.
#define IREP2_EXPR(kind, pretty) expr_macros(kind)
#include <irep2/expr_kinds.inc>
#undef IREP2_EXPR
 
#undef expr_macros
 
#endif /* IREP2_EXPR_H_ */