bitvector_types.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Pre-defined bitvector types
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_UTIL_BITVECTOR_TYPES_H
#define CPROVER_UTIL_BITVECTOR_TYPES_H
 
#include "std_types.h"
 
inline bool is_signed_or_unsigned_bitvector(const typet &type)
{
  return type.id() == ID_signedbv || type.id() == ID_unsignedbv;
}
 
inline const bitvector_typet &to_bitvector_type(const typet &type)
{
  PRECONDITION(can_cast_type<bitvector_typet>(type));
 
  return static_cast<const bitvector_typet &>(type);
}
 
inline bitvector_typet &to_bitvector_type(typet &type)
{
  PRECONDITION(can_cast_type<bitvector_typet>(type));
 
  return static_cast<bitvector_typet &>(type);
}
 
class bv_typet : public bitvector_typet
{
public:
  explicit bv_typet(std::size_t width) : bitvector_typet(ID_bv)
  {
    set_width(width);
  }
 
  static void check(
    const typet &type,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    DATA_CHECK(
      vm, !type.get(ID_width).empty(), "bitvector type must have width");
  }
 
  // helpers to create common constants
  constant_exprt all_zeros_expr() const;
  constant_exprt all_ones_expr() const;
};
 
template <>
inline bool can_cast_type<bv_typet>(const typet &type)
{
  return type.id() == ID_bv;
}
 
inline const bv_typet &to_bv_type(const typet &type)
{
  PRECONDITION(can_cast_type<bv_typet>(type));
  bv_typet::check(type);
  return static_cast<const bv_typet &>(type);
}
 
inline bv_typet &to_bv_type(typet &type)
{
  PRECONDITION(can_cast_type<bv_typet>(type));
  bv_typet::check(type);
  return static_cast<bv_typet &>(type);
}
 
class integer_bitvector_typet : public bitvector_typet
{
public:
  integer_bitvector_typet(const irep_idt &id, std::size_t width)
    : bitvector_typet(id, width)
  {
  }
 
  mp_integer smallest() const;
  mp_integer largest() const;
 
  // If we ever need any of the following three methods in \ref fixedbv_typet or
  // \ref floatbv_typet, we might want to move them to a new class
  // numeric_bitvector_typet, which would be between integer_bitvector_typet and
  // bitvector_typet in the hierarchy.
 
  constant_exprt smallest_expr() const;
  constant_exprt zero_expr() const;
  constant_exprt largest_expr() const;
};
 
template <>
inline bool can_cast_type<integer_bitvector_typet>(const typet &type)
{
  return type.id() == ID_signedbv || type.id() == ID_unsignedbv;
}
 
inline const integer_bitvector_typet &
to_integer_bitvector_type(const typet &type)
{
  PRECONDITION(can_cast_type<integer_bitvector_typet>(type));
 
  return static_cast<const integer_bitvector_typet &>(type);
}
 
inline integer_bitvector_typet &to_integer_bitvector_type(typet &type)
{
  PRECONDITION(can_cast_type<integer_bitvector_typet>(type));
 
  return static_cast<integer_bitvector_typet &>(type);
}
 
class unsignedbv_typet : public integer_bitvector_typet
{
public:
  explicit unsignedbv_typet(std::size_t width)
    : integer_bitvector_typet(ID_unsignedbv, width)
  {
  }
 
  static void check(
    const typet &type,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    bitvector_typet::check(type, vm);
  }
};
 
template <>
inline bool can_cast_type<unsignedbv_typet>(const typet &type)
{
  return type.id() == ID_unsignedbv;
}
 
inline const unsignedbv_typet &to_unsignedbv_type(const typet &type)
{
  PRECONDITION(can_cast_type<unsignedbv_typet>(type));
  unsignedbv_typet::check(type);
  return static_cast<const unsignedbv_typet &>(type);
}
 
inline unsignedbv_typet &to_unsignedbv_type(typet &type)
{
  PRECONDITION(can_cast_type<unsignedbv_typet>(type));
  unsignedbv_typet::check(type);
  return static_cast<unsignedbv_typet &>(type);
}
 
class signedbv_typet : public integer_bitvector_typet
{
public:
  explicit signedbv_typet(std::size_t width)
    : integer_bitvector_typet(ID_signedbv, width)
  {
  }
 
  static void check(
    const typet &type,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    DATA_CHECK(
      vm, !type.get(ID_width).empty(), "signed bitvector type must have width");
  }
};
 
template <>
inline bool can_cast_type<signedbv_typet>(const typet &type)
{
  return type.id() == ID_signedbv;
}
 
inline const signedbv_typet &to_signedbv_type(const typet &type)
{
  PRECONDITION(can_cast_type<signedbv_typet>(type));
  signedbv_typet::check(type);
  return static_cast<const signedbv_typet &>(type);
}
 
inline signedbv_typet &to_signedbv_type(typet &type)
{
  PRECONDITION(can_cast_type<signedbv_typet>(type));
  signedbv_typet::check(type);
  return static_cast<signedbv_typet &>(type);
}
 
class fixedbv_typet : public bitvector_typet
{
public:
  fixedbv_typet() : bitvector_typet(ID_fixedbv)
  {
  }
 
  std::size_t get_fraction_bits() const
  {
    return get_width() - get_integer_bits();
  }
 
  std::size_t get_integer_bits() const;
 
  void set_integer_bits(std::size_t b)
  {
    set_size_t(ID_integer_bits, b);
  }
 
  static void check(
    const typet &type,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    DATA_CHECK(
      vm, !type.get(ID_width).empty(), "fixed bitvector type must have width");
  }
};
 
template <>
inline bool can_cast_type<fixedbv_typet>(const typet &type)
{
  return type.id() == ID_fixedbv;
}
 
inline const fixedbv_typet &to_fixedbv_type(const typet &type)
{
  PRECONDITION(can_cast_type<fixedbv_typet>(type));
  fixedbv_typet::check(type);
  return static_cast<const fixedbv_typet &>(type);
}
 
inline fixedbv_typet &to_fixedbv_type(typet &type)
{
  PRECONDITION(can_cast_type<fixedbv_typet>(type));
  fixedbv_typet::check(type);
  return static_cast<fixedbv_typet &>(type);
}
 
class floatbv_typet : public bitvector_typet
{
public:
  floatbv_typet() : bitvector_typet(ID_floatbv)
  {
  }
 
  std::size_t get_e() const
  {
    // subtract one for sign bit
    return get_width() - get_f() - 1;
  }
 
  std::size_t get_f() const;
 
  void set_f(std::size_t b)
  {
    set_size_t(ID_f, b);
  }
 
  static void check(
    const typet &type,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    DATA_CHECK(
      vm, !type.get(ID_width).empty(), "float bitvector type must have width");
  }
};
 
template <>
inline bool can_cast_type<floatbv_typet>(const typet &type)
{
  return type.id() == ID_floatbv;
}
 
inline const floatbv_typet &to_floatbv_type(const typet &type)
{
  PRECONDITION(can_cast_type<floatbv_typet>(type));
  floatbv_typet::check(type);
  return static_cast<const floatbv_typet &>(type);
}
 
inline floatbv_typet &to_floatbv_type(typet &type)
{
  PRECONDITION(can_cast_type<floatbv_typet>(type));
  floatbv_typet::check(type);
  return static_cast<floatbv_typet &>(type);
}
 
#endif // CPROVER_UTIL_BITVECTOR_TYPES_H