irep2_utils.h

Go to the documentation of this file.

#ifndef UTIL_IREP2_UTILS_H_
#define UTIL_IREP2_UTILS_H_
 
#include <util/lang/c_types.h>
 
#include <irep2/irep2_expr.h>
#include <irep2/simplification_check.h>
#include <util/irep/migrate.h>
#include <util/message/message.h>
 
std::string indent_str_irep2(unsigned int indent);
 
// Parameter names are not part of a function's type (C++ [dcl.fct]p5, C11
// 6.7.6.3p15), but irep2 type equality compares argument_names too. An
// out-of-line virtual definition gives its parameters fresh symbol ids, so the
// vtable slot and the function symbol end up with code types that differ in
// nothing else -- enough for the virtual call to lose its target (#6749).
inline bool same_function_pointer_ignoring_argument_names(
  const type2tc &a,
  const type2tc &b)
{
  if (!is_pointer_type(a) || !is_pointer_type(b))
    return false;
 
  const type2tc &sub_a = to_pointer_type(a).subtype;
  const type2tc &sub_b = to_pointer_type(b).subtype;
  if (!is_code_type(sub_a) || !is_code_type(sub_b))
    return false;
 
  const code_type2t &ca = to_code_type(sub_a);
  const code_type2t &cb = to_code_type(sub_b);
  return ca.arguments == cb.arguments && ca.ret_type == cb.ret_type &&
         ca.ellipsis == cb.ellipsis;
}

inline bool is_bv_type(const type2tc &t)
{
  return t->type_id == type2t::unsignedbv_id ||
         t->type_id == type2t::signedbv_id;
}
 
inline bool is_bv_type(const expr2tc &e)
{
  return is_bv_type(e->type);
}

inline bool is_fractional_type(const type2tc &t)
{
  return t->type_id == type2t::fixedbv_id || t->type_id == type2t::floatbv_id;
}

inline bool is_comparison_expr(const expr2tc &e)
{
  return is_equality2t(e) || is_notequal2t(e) || is_lessthan2t(e) ||
         is_greaterthan2t(e) || is_lessthanequal2t(e) ||
         is_greaterthanequal2t(e);
}

inline bool is_number_type(const type2tc &t)
{
  return t->type_id == type2t::unsignedbv_id ||
         t->type_id == type2t::signedbv_id ||
         t->type_id == type2t::fixedbv_id || t->type_id == type2t::floatbv_id ||
         t->type_id == type2t::bool_id;
}
 
inline bool is_number_type(const expr2tc &e)
{
  return is_number_type(e->type);
}
 
inline bool is_scalar_type(const type2tc &t)
{
  return is_number_type(t) || is_pointer_type(t) || is_empty_type(t) ||
         is_code_type(t);
}
 
inline bool is_scalar_type(const expr2tc &e)
{
  return is_scalar_type(e->type);
}
 
inline bool is_multi_dimensional_array(const type2tc &t)
{
  if (is_array_type(t))
    return is_array_type(to_array_type(t).subtype);
 
  return false;
}
 
inline bool is_multi_dimensional_array(const expr2tc &e)
{
  return is_multi_dimensional_array(e->type);
}
 
// array_type2t and vector_type2t carry the same set of element-shape
// fields (subtype, array_size, size_is_infinite). Callers that have a
// type which they know is one of those two but don't care which use
// these helpers to skip the per-kind switch.
// Whether a type is indexed like an array: its elements sit at consecutive
// element-sized offsets, which is all the code below an index2t needs to know.
inline bool is_array_or_vector_type(const type2tc &t)
{
  return is_array_type(t) || is_vector_type(t);
}
 
inline bool is_array_or_vector_type(const expr2tc &e)
{
  return is_array_or_vector_type(e->type);
}
 
inline const type2tc &array_or_vector_subtype(const type2tc &t)
{
  if (is_array_type(t))
    return to_array_type(t).subtype;
  if (is_vector_type(t))
    return to_vector_type(t).subtype;
  irep2_bad_family_cast(t->type_id, "array_or_vector_subtype");
}
 
inline const expr2tc &array_or_vector_size(const type2tc &t)
{
  if (is_array_type(t))
    return to_array_type(t).array_size;
  if (is_vector_type(t))
    return to_vector_type(t).array_size;
  irep2_bad_family_cast(t->type_id, "array_or_vector_size");
}
 
inline bool array_or_vector_size_is_infinite(const type2tc &t)
{
  if (is_array_type(t))
    return to_array_type(t).size_is_infinite;
  if (is_vector_type(t))
    return to_vector_type(t).size_is_infinite;
  irep2_bad_family_cast(t->type_id, "array_or_vector_size_is_infinite");
}
 
inline bool is_byte_type(const type2tc &t)
{
  return is_bv_type(t) && t->get_width() == 8;
}
 
inline bool is_byte_type(const expr2tc &e)
{
  return is_byte_type(e->type);
}
 
inline bool is_constant_number(const expr2tc &t)
{
  return t->expr_id == expr2t::constant_int_id ||
         t->expr_id == expr2t::constant_fixedbv_id ||
         t->expr_id == expr2t::constant_floatbv_id ||
         t->expr_id == expr2t::constant_bool_id;
}
 
inline bool is_constant_expr(const expr2tc &t)
{
  return is_constant_number(t) || t->expr_id == expr2t::constant_string_id ||
         t->expr_id == expr2t::constant_struct_id ||
         t->expr_id == expr2t::constant_union_id ||
         t->expr_id == expr2t::constant_array_id ||
         t->expr_id == expr2t::constant_array_of_id ||
         t->expr_id == expr2t::constant_vector_id;
}
 
inline bool is_constant(const expr2tc &t)
{
  if (is_pointer_type(t) && is_symbol2t(t))
  {
    symbol2t s = to_symbol2t(t);
    if (s.thename == "NULL")
      return true;
  }
  return is_constant_expr(t);
}
 
inline bool is_structure_type(const type2tc &t)
{
  return t->type_id == type2t::struct_id || t->type_id == type2t::union_id;
}
 
inline bool is_structure_type(const expr2tc &e)
{
  return is_structure_type(e->type);
}
 
inline bool is_arith_expr(const expr2tc &expr)
{
  return expr->expr_id == expr2t::neg_id || expr->expr_id == expr2t::abs_id ||
         expr->expr_id == expr2t::add_id || expr->expr_id == expr2t::sub_id ||
         expr->expr_id == expr2t::mul_id || expr->expr_id == expr2t::div_id ||
         expr->expr_id == expr2t::modulus_id;
}
 
inline bool is_comp_expr(const expr2tc &expr)
{
  return expr->expr_id == expr2t::lessthan_id ||
         expr->expr_id == expr2t::lessthanequal_id ||
         expr->expr_id == expr2t::greaterthan_id ||
         expr->expr_id == expr2t::greaterthanequal_id ||
         expr->expr_id == expr2t::equality_id ||
         expr->expr_id == expr2t::notequal_id;
}

inline bool is_true(const expr2tc &expr)
{
  if (is_constant_bool2t(expr) && to_constant_bool2t(expr).value)
    return true;
 
  if (is_constant_int2t(expr) && !to_constant_int2t(expr).value.is_zero())
    return true;
 
  if (
    is_constant_floatbv2t(expr) && !to_constant_floatbv2t(expr).value.is_zero())
    return true;
 
  if (
    is_constant_fixedbv2t(expr) && !to_constant_fixedbv2t(expr).value.is_zero())
    return true;
 
  return false;
}

inline bool is_false(const expr2tc &expr)
{
  if (is_constant_bool2t(expr) && !to_constant_bool2t(expr).value)
    return true;
 
  if (is_constant_int2t(expr) && to_constant_int2t(expr).value.is_zero())
    return true;
 
  if (
    is_constant_floatbv2t(expr) && to_constant_floatbv2t(expr).value.is_zero())
    return true;
 
  if (
    is_constant_fixedbv2t(expr) && to_constant_fixedbv2t(expr).value.is_zero())
    return true;
 
  return false;
}
 
// Returning by const reference is sound here: `c` has static storage
// duration and outlives every possible caller. Callers that bind to an
// `expr2tc` value get the usual refcount-bump copy; callers that pass
// the result through to a function taking `const expr2tc &` save one
// pair of atomic refcount ops per call.
inline const expr2tc &gen_true_expr()
{
  static const expr2tc c = constant_bool2tc(true);
  return c;
}
 
inline const expr2tc &gen_false_expr()
{
  static const expr2tc c = constant_bool2tc(false);
  return c;
}
 
inline expr2tc gen_long(const type2tc &type, BigInt val)
{
  return constant_int2tc(type, std::move(val));
}
 
inline expr2tc gen_ulong(BigInt v)
{
  return constant_int2tc(get_uint_type(config.ansi_c.word_size), std::move(v));
}
 
inline expr2tc gen_ulong(unsigned long val)
{
  return gen_ulong(BigInt(val));
}
 
inline const type2tc &get_base_array_subtype(const type2tc &type)
{
  const auto &subtype = to_array_type(type).subtype;
  if (is_array_type(subtype))
    return get_base_array_subtype(subtype);
 
  return subtype;
}
 
inline bool simplify(expr2tc &expr)
{
  expr2tc tmp = expr->simplify();
  if (!is_nil_expr(tmp))
  {
    // No verify_rewrite() here: simplify() now checks each rewrite where it is
    // made, so a whole-expression claim would restate what is already proved,
    // in the widest and most decline-prone query of the run (esbmc/esbmc#7260).
    expr = tmp;
    return true;
  }
 
  return false;
}

void make_not(expr2tc &expr);

expr2tc conjunction(std::vector<expr2tc> cs);

expr2tc disjunction(std::vector<expr2tc> cs);

expr2tc gen_nondet(const type2tc &type);

expr2tc gen_zero(const type2tc &type, bool array_as_array_of = false);

expr2tc gen_one(const type2tc &type);

template <typename Func>
inline expr2tc
distribute_vector_operation(Func func, const expr2tc &op1, const expr2tc &op2)
{
  assert(is_constant_vector2t(op1) || is_constant_vector2t(op2));
  /*
   * If both op1 and op2 are vectors the resulting value
   * would be the operation over each member
   *
   * Example:
   *
   * op1 = {1,2,3,4}
   * op2 = {1,1,1,1}
   * func = add
   *
   * This would result in:
   *
   * { add(op1[0], op2[0]), add(op1[1], op2[1]), ...}
   * {2,3,4,5}
   */
  if (is_constant_vector2t(op1) && is_constant_vector2t(op2))
  {
    std::vector<expr2tc> members = to_constant_vector2t(op1).datatype_members;
    const constant_vector2t *vec2 = &to_constant_vector2t(op2);
    for (size_t i = 0; i < members.size(); i++)
    {
      auto &A = members[i];
      auto &B = vec2->datatype_members[i];
      auto new_op = func(A->type, A, B);
      members[i] = new_op;
    }
    return constant_vector2tc(op1->type, std::move(members));
  }
  /*
   * If only one of the operators is a constant vector, then the result
   * would extract each value of the vector and apply the value to
   * the other operator, or to its matching lane when that is a vector
   *
   * Example:
   *
   * op1 = {1,2,3,4}
   * op2 = 1
   * func = add
   *
   * This would result in:
   *
   * { add(op1[0], 1), add(op1[1], 1), ...}
   * {2,3,4,5}
   */
  else
  {
    bool is_op1_vec = is_constant_vector2t(op1);
    expr2tc c = !is_op1_vec ? op1 : op2;
    expr2tc v = is_op1_vec ? op1 : op2;
    std::vector<expr2tc> members = to_constant_vector2t(v).datatype_members;
    for (size_t i = 0; i < members.size(); i++)
    {
      auto &op = members[i];
      // A non-constant vector operand contributes its own lane, not itself.
      expr2tc lane = c;
      if (is_vector_type(c))
        lane = index2tc(
          to_vector_type(c->type).subtype,
          c,
          constant_int2tc(get_uint32_type(), BigInt(i)));
      auto e1 = is_op1_vec ? op : lane;
      auto e2 = is_op1_vec ? lane : op;
      auto new_op = func(op->type, e1, e2);
      // do_simplify() returns nil when no per-op peephole fires. Don't
      // store nil into the member slot — keep new_op so the lane
      // expression survives unsimplified for the SMT layer.
      auto folded = new_op->do_simplify();
      if (!is_nil_expr(folded))
        simplification_check::verify_rewrite(new_op, folded);
      op = is_nil_expr(folded) ? new_op : folded;
    }
    return constant_vector2tc(v->type, std::move(members));
  }
}

expr2tc distribute_vector_operation(
  expr2t::expr_ids id,
  const expr2tc &op1,
  const expr2tc &op2 = expr2tc(),
  const expr2tc &rm = expr2tc());
 
// Build a comparison-category struct value with the discriminant set to v.
// Used for the C++20 spaceship operator: strong_ordering / weak_ordering /
// partial_ordering all layout the discriminant as the first field, so
// writing operand[0] is enough; remaining fields (if any) are zero-filled
// for layout safety against custom comparison-category types.
//
// Returns nil if @p t is not a struct or has no fields.
expr2tc make_cmp_value(const type2tc &t, int v);

void get_symbols(
  const expr2tc &expr,
  std::unordered_set<expr2tc, irep2_hash> &symbols);

std::vector<expr2tc>
pad_struct_operands(const struct_type2t &st, std::vector<expr2tc> ops);

irep_idt quantifier_bound_name(const expr2tc &binder);

irep_idt quantifier_direct_bound_name(const expr2tc &binder);
 
#endif /* UTIL_IREP2_UTILS_H_ */