std_types.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Pre-defined types
 
Author: Daniel Kroening, kroening@kroening.com
        Maria Svorenova, maria.svorenova@diffblue.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_UTIL_STD_TYPES_H
#define CPROVER_UTIL_STD_TYPES_H
 
#include "expr.h"
#include "expr_cast.h" // IWYU pragma: keep
#include "invariant.h"
#include "mp_arith.h"
#include "validate.h"
 
#include <unordered_map>
 
class constant_exprt;
class namespacet;
 
inline bool is_constant(const typet &type)
{
  return type.get_bool(ID_C_constant);
}
 
class bool_typet:public typet
{
public:
  bool_typet():typet(ID_bool)
  {
  }
};
 
template <>
inline bool can_cast_type<bool_typet>(const typet &base)
{
  return base.id() == ID_bool;
}
 
class empty_typet:public typet
{
public:
  empty_typet():typet(ID_empty)
  {
  }
};
 
class struct_union_typet:public typet
{
public:
  explicit struct_union_typet(const irep_idt &_id):typet(_id)
  {
  }
 
  class componentt:public exprt
  {
  public:
    componentt() = default;
 
    componentt(const irep_idt &_name, typet _type)
    {
      set_name(_name);
      type().swap(_type);
    }
 
    const irep_idt &get_name() const
    {
      return get(ID_name);
    }
 
    void set_name(const irep_idt &name)
    {
      return set(ID_name, name);
    }
 
    const irep_idt &get_base_name() const
    {
      return get(ID_C_base_name);
    }
 
    void set_base_name(const irep_idt &base_name)
    {
      return set(ID_C_base_name, base_name);
    }
 
    const irep_idt &get_access() const
    {
      return get(ID_access);
    }
 
    void set_access(const irep_idt &access)
    {
      return set(ID_access, access);
    }
 
    const irep_idt &get_pretty_name() const
    {
      return get(ID_C_pretty_name);
    }
 
    void set_pretty_name(const irep_idt &name)
    {
      return set(ID_C_pretty_name, name);
    }
 
    bool get_anonymous() const
    {
      return get_bool(ID_anonymous);
    }
 
    void set_anonymous(bool anonymous)
    {
      return set(ID_anonymous, anonymous);
    }
 
    bool get_is_padding() const
    {
      return get_bool(ID_C_is_padding);
    }
 
    void set_is_padding(bool is_padding)
    {
      return set(ID_C_is_padding, is_padding);
    }
  };
 
  typedef std::vector<componentt> componentst;
 
  struct_union_typet(const irep_idt &_id, componentst _components) : typet(_id)
  {
    components() = std::move(_components);
  }
 
  const componentst &components() const
  {
    return (const componentst &)(find(ID_components).get_sub());
  }
 
  componentst &components()
  {
    return (componentst &)(add(ID_components).get_sub());
  }
 
  bool has_component(const irep_idt &component_name) const
  {
    return get_component(component_name).is_not_nil();
  }
 
  const componentt &get_component(
    const irep_idt &component_name) const;
 
  std::size_t component_number(const irep_idt &component_name) const;
  const typet &component_type(const irep_idt &component_name) const;
 
  irep_idt get_tag() const { return get(ID_tag); }
  void set_tag(const irep_idt &tag) { set(ID_tag, tag); }
 
  bool is_class() const
  {
    return id() == ID_struct && get_bool(ID_C_class);
  }
 
  irep_idt default_access() const
  {
    return is_class() ? ID_private : ID_public;
  }
 
  bool is_incomplete() const
  {
    return get_bool(ID_incomplete);
  }
 
  void make_incomplete()
  {
    set(ID_incomplete, true);
  }
};
 
template <>
inline bool can_cast_type<struct_union_typet>(const typet &type)
{
  return type.id() == ID_struct || type.id() == ID_union;
}
 
inline const struct_union_typet &to_struct_union_type(const typet &type)
{
  PRECONDITION(can_cast_type<struct_union_typet>(type));
  return static_cast<const struct_union_typet &>(type);
}
 
inline struct_union_typet &to_struct_union_type(typet &type)
{
  PRECONDITION(can_cast_type<struct_union_typet>(type));
  return static_cast<struct_union_typet &>(type);
}
 
class struct_tag_typet;
 
class struct_typet:public struct_union_typet
{
public:
  struct_typet():struct_union_typet(ID_struct)
  {
  }
 
  explicit struct_typet(componentst _components)
    : struct_union_typet(ID_struct, std::move(_components))
  {
  }
 
  bool is_prefix_of(const struct_typet &other) const;
 
  bool is_class() const
  {
    return get_bool(ID_C_class);
  }
 
  class baset : public exprt
  {
  public:
    struct_tag_typet &type();
    const struct_tag_typet &type() const;
    explicit baset(struct_tag_typet base);
  };
 
  typedef std::vector<baset> basest;
 
  const basest &bases() const
  {
    return (const basest &)find(ID_bases).get_sub();
  }
 
  basest &bases()
  {
    return (basest &)add(ID_bases).get_sub();
  }
 
  void add_base(const struct_tag_typet &base);
 
  std::optional<baset> get_base(const irep_idt &id) const;
 
  bool has_base(const irep_idt &id) const
  {
    return get_base(id).has_value();
  }
};
 
template <>
inline bool can_cast_type<struct_typet>(const typet &type)
{
  return type.id() == ID_struct;
}
 
inline const struct_typet &to_struct_type(const typet &type)
{
  PRECONDITION(can_cast_type<struct_typet>(type));
  return static_cast<const struct_typet &>(type);
}
 
inline struct_typet &to_struct_type(typet &type)
{
  PRECONDITION(can_cast_type<struct_typet>(type));
  return static_cast<struct_typet &>(type);
}
 
class class_typet:public struct_typet
{
public:
  class_typet():struct_typet()
  {
    set(ID_C_class, true);
  }
 
  typedef componentt methodt;
  typedef componentst methodst;
 
  const methodst &methods() const
  {
    return (const methodst &)(find(ID_methods).get_sub());
  }
 
  methodst &methods()
  {
    return (methodst &)(add(ID_methods).get_sub());
  }
 
  using static_membert = componentt;
  using static_memberst = componentst;
 
  const static_memberst &static_members() const
  {
    return (const static_memberst &)(find(ID_static_members).get_sub());
  }
 
  static_memberst &static_members()
  {
    return (static_memberst &)(add(ID_static_members).get_sub());
  }
 
  bool is_abstract() const
  {
    return get_bool(ID_abstract);
  }
};
 
template <>
inline bool can_cast_type<class_typet>(const typet &type)
{
  return can_cast_type<struct_typet>(type) && type.get_bool(ID_C_class);
}
 
inline const class_typet &to_class_type(const typet &type)
{
  PRECONDITION(can_cast_type<class_typet>(type));
  return static_cast<const class_typet &>(type);
}
 
inline class_typet &to_class_type(typet &type)
{
  PRECONDITION(can_cast_type<class_typet>(type));
  return static_cast<class_typet &>(type);
}
 
class tag_typet:public typet
{
public:
  explicit tag_typet(
    const irep_idt &_id,
    const irep_idt &identifier):typet(_id)
  {
    set_identifier(identifier);
  }
 
  void set_identifier(const irep_idt &identifier)
  {
    set(ID_identifier, identifier);
  }
 
  const irep_idt &get_identifier() const
  {
    return get(ID_identifier);
  }
};
 
template <>
inline bool can_cast_type<tag_typet>(const typet &type)
{
  return type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
         type.id() == ID_union_tag;
}
 
inline const tag_typet &to_tag_type(const typet &type)
{
  PRECONDITION(can_cast_type<tag_typet>(type));
  return static_cast<const tag_typet &>(type);
}
 
inline tag_typet &to_tag_type(typet &type)
{
  PRECONDITION(can_cast_type<tag_typet>(type));
  return static_cast<tag_typet &>(type);
}
 
class struct_or_union_tag_typet : public tag_typet
{
protected:
  struct_or_union_tag_typet(const irep_idt &id, const irep_idt &identifier)
    : tag_typet(id, identifier)
  {
    PRECONDITION(id == ID_struct_tag || id == ID_union_tag);
  }
};
 
template <>
inline bool can_cast_type<struct_or_union_tag_typet>(const typet &type)
{
  return type.id() == ID_struct_tag || type.id() == ID_union_tag;
}
 
inline const struct_or_union_tag_typet &
to_struct_or_union_tag_type(const typet &type)
{
  PRECONDITION(can_cast_type<struct_or_union_tag_typet>(type));
  return static_cast<const struct_or_union_tag_typet &>(type);
}
 
inline struct_or_union_tag_typet &to_struct_or_union_tag_type(typet &type)
{
  PRECONDITION(can_cast_type<struct_or_union_tag_typet>(type));
  return static_cast<struct_or_union_tag_typet &>(type);
}
 
class struct_tag_typet : public struct_or_union_tag_typet
{
public:
  explicit struct_tag_typet(const irep_idt &identifier)
    : struct_or_union_tag_typet(ID_struct_tag, identifier)
  {
  }
};
 
template <>
inline bool can_cast_type<struct_tag_typet>(const typet &type)
{
  return type.id() == ID_struct_tag;
}
 
inline const struct_tag_typet &to_struct_tag_type(const typet &type)
{
  PRECONDITION(can_cast_type<struct_tag_typet>(type));
  return static_cast<const struct_tag_typet &>(type);
}
 
inline struct_tag_typet &to_struct_tag_type(typet &type)
{
  PRECONDITION(can_cast_type<struct_tag_typet>(type));
  return static_cast<struct_tag_typet &>(type);
}
 
class enumeration_typet:public typet
{
public:
  enumeration_typet():typet(ID_enumeration)
  {
  }
 
  const irept::subt &elements() const
  {
    return find(ID_elements).get_sub();
  }
 
  irept::subt &elements()
  {
    return add(ID_elements).get_sub();
  }
};
 
template <>
inline bool can_cast_type<enumeration_typet>(const typet &type)
{
  return type.id() == ID_enumeration;
}
 
inline const enumeration_typet &to_enumeration_type(const typet &type)
{
  PRECONDITION(can_cast_type<enumeration_typet>(type));
  return static_cast<const enumeration_typet &>(type);
}
 
inline enumeration_typet &to_enumeration_type(typet &type)
{
  PRECONDITION(can_cast_type<enumeration_typet>(type));
  return static_cast<enumeration_typet &>(type);
}
 
class code_typet:public typet
{
public:
  class parametert;
  typedef std::vector<parametert> parameterst;
 
  code_typet(parameterst _parameters, typet _return_type) : typet(ID_code)
  {
    parameters().swap(_parameters);
    return_type().swap(_return_type);
  }
 
  // used to be argumentt -- now uses standard terminology
 
  class parametert:public exprt
  {
  public:
    explicit parametert(const typet &type):exprt(ID_parameter, type)
    {
    }
 
    const exprt &default_value() const
    {
      return find_expr(ID_C_default_value);
    }
 
    bool has_default_value() const
    {
      return default_value().is_not_nil();
    }
 
    exprt &default_value()
    {
      return add_expr(ID_C_default_value);
    }
 
    // The following for methods will go away;
    // these should not be part of the signature of a function,
    // but rather part of the body.
    void set_identifier(const irep_idt &identifier)
    {
      set(ID_C_identifier, identifier);
    }
 
    void set_base_name(const irep_idt &name)
    {
      set(ID_C_base_name, name);
    }
 
    const irep_idt &get_identifier() const
    {
      return get(ID_C_identifier);
    }
 
    const irep_idt &get_base_name() const
    {
      return get(ID_C_base_name);
    }
 
    bool get_this() const
    {
      return get_bool(ID_C_this);
    }
 
    void set_this()
    {
      set(ID_C_this, true);
    }
  };
 
  bool has_ellipsis() const
  {
    return find(ID_parameters).get_bool(ID_ellipsis);
  }
 
  bool has_this() const
  {
    return get_this() != nullptr;
  }
 
  const parametert *get_this() const
  {
    const parameterst &p=parameters();
    if(!p.empty() && p.front().get_this())
      return &p.front();
    else
      return nullptr;
  }
 
  bool is_KnR() const
  {
    return get_bool(ID_C_KnR);
  }
 
  void make_ellipsis()
  {
    add(ID_parameters).set(ID_ellipsis, true);
  }
 
  void remove_ellipsis()
  {
    add(ID_parameters).remove(ID_ellipsis);
  }
 
  const typet &return_type() const
  {
    return find_type(ID_return_type);
  }
 
  typet &return_type()
  {
    return add_type(ID_return_type);
  }
 
  const parameterst &parameters() const
  {
    return (const parameterst &)find(ID_parameters).get_sub();
  }
 
  parameterst &parameters()
  {
    return (parameterst &)add(ID_parameters).get_sub();
  }
 
  bool get_inlined() const
  {
    return get_bool(ID_C_inlined);
  }
 
  void set_inlined(bool value)
  {
    set(ID_C_inlined, value);
  }
 
  const irep_idt &get_access() const
  {
    return get(ID_access);
  }
 
  void set_access(const irep_idt &access)
  {
    return set(ID_access, access);
  }
 
  bool get_is_constructor() const
  {
    return get_bool(ID_constructor);
  }
 
  void set_is_constructor()
  {
    set(ID_constructor, true);
  }
 
  std::vector<irep_idt> parameter_identifiers() const
  {
    std::vector<irep_idt> result;
    const parameterst &p=parameters();
    result.reserve(p.size());
    for(parameterst::const_iterator it=p.begin();
        it!=p.end(); it++)
      result.push_back(it->get_identifier());
    return result;
  }
 
  typedef std::unordered_map<irep_idt, std::size_t> parameter_indicest;
 
  parameter_indicest parameter_indices() const
  {
    parameter_indicest parameter_indices;
    const parameterst &params = parameters();
    parameter_indices.reserve(params.size());
    std::size_t index = 0;
    for(const auto &p : params)
    {
      const irep_idt &id = p.get_identifier();
      if(!id.empty())
        parameter_indices.insert({ id, index });
      ++index;
    }
    return parameter_indices;
  }
};
 
template <>
inline bool can_cast_type<code_typet>(const typet &type)
{
  return type.id() == ID_code;
}
 
inline const code_typet &to_code_type(const typet &type)
{
  PRECONDITION(can_cast_type<code_typet>(type));
  code_typet::check(type);
  return static_cast<const code_typet &>(type);
}
 
inline code_typet &to_code_type(typet &type)
{
  PRECONDITION(can_cast_type<code_typet>(type));
  code_typet::check(type);
  return static_cast<code_typet &>(type);
}
 
class array_typet:public type_with_subtypet
{
public:
  array_typet(typet _subtype, exprt _size)
    : type_with_subtypet(ID_array, std::move(_subtype))
  {
    add(ID_size, std::move(_size));
  }
 
  typet index_type() const;
 
  typet &index_type_nonconst()
  {
    return static_cast<typet &>(add(ID_C_index_type));
  }
 
  const typet &element_type() const
  {
    return subtype();
  }
 
  typet &element_type()
  {
    return subtype();
  }
 
  // We will eventually enforce that the type of the size
  // is the same as the index type.
  const exprt &size() const
  {
    return static_cast<const exprt &>(find(ID_size));
  }
 
  // We will eventually enforce that the type of the size
  // is the same as the index type.
  exprt &size()
  {
    return static_cast<exprt &>(add(ID_size));
  }
 
  bool is_complete() const
  {
    return size().is_not_nil();
  }
 
  bool is_incomplete() const
  {
    return size().is_nil();
  }
 
  static void check(
    const typet &type,
    const validation_modet vm = validation_modet::INVARIANT);
 
protected:
  // Use element_type() instead
  using type_with_subtypet::subtype;
};
 
template <>
inline bool can_cast_type<array_typet>(const typet &type)
{
  return type.id() == ID_array;
}
 
inline const array_typet &to_array_type(const typet &type)
{
  PRECONDITION(can_cast_type<array_typet>(type));
  array_typet::check(type);
  return static_cast<const array_typet &>(type);
}
 
inline array_typet &to_array_type(typet &type)
{
  PRECONDITION(can_cast_type<array_typet>(type));
  array_typet::check(type);
  return static_cast<array_typet &>(type);
}
 
class bitvector_typet : public typet
{
public:
  explicit bitvector_typet(const irep_idt &_id) : typet(_id)
  {
  }
 
  bitvector_typet(const irep_idt &_id, std::size_t width) : typet(_id)
  {
    set_width(width);
  }
 
  bitvector_typet(const irep_idt &_id, mp_integer _width) : typet(_id)
  {
    width(_width);
  }
 
  std::size_t get_width() const
  {
    return get_size_t(ID_width);
  }
 
  std::size_t width() const;
 
  void set_width(std::size_t width)
  {
    set_size_t(ID_width, width);
  }
 
  void width(const mp_integer &);
 
  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");
  }
};
 
template <>
inline bool can_cast_type<bitvector_typet>(const typet &type)
{
  return type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
         type.id() == ID_fixedbv || type.id() == ID_floatbv ||
         type.id() == ID_verilog_signedbv ||
         type.id() == ID_verilog_unsignedbv || type.id() == ID_bv ||
         type.id() == ID_pointer || type.id() == ID_c_bit_field ||
         type.id() == ID_c_bool;
}
 
class string_typet:public typet
{
public:
  string_typet():typet(ID_string)
  {
  }
};
 
template <>
inline bool can_cast_type<string_typet>(const typet &type)
{
  return type.id() == ID_string;
}
 
inline const string_typet &to_string_type(const typet &type)
{
  PRECONDITION(can_cast_type<string_typet>(type));
  return static_cast<const string_typet &>(type);
}
 
inline string_typet &to_string_type(typet &type)
{
  PRECONDITION(can_cast_type<string_typet>(type));
  return static_cast<string_typet &>(type);
}
 
class range_typet:public typet
{
public:
  range_typet(const mp_integer &_from, const mp_integer &_to) : typet(ID_range)
  {
    set_from(_from);
    set_to(_to);
  }
 
  mp_integer get_from() const;
  mp_integer get_to() const;
 
  void set_from(const mp_integer &_from);
  void set_to(const mp_integer &to);
};
 
template <>
inline bool can_cast_type<range_typet>(const typet &type)
{
  return type.id() == ID_range;
}
 
inline const range_typet &to_range_type(const typet &type)
{
  PRECONDITION(can_cast_type<range_typet>(type));
  return static_cast<const range_typet &>(type);
}
 
inline range_typet &to_range_type(typet &type)
{
  PRECONDITION(can_cast_type<range_typet>(type));
  return static_cast<range_typet &>(type);
}
 
class vector_typet:public type_with_subtypet
{
public:
  vector_typet(typet index_type, typet element_type, constant_exprt size);
 
  typet index_type() const;
 
  typet &index_type_nonconst()
  {
    return static_cast<typet &>(add(ID_C_index_type));
  }
 
  const typet &element_type() const
  {
    return subtype();
  }
 
  typet &element_type()
  {
    return subtype();
  }
 
  const constant_exprt &size() const;
  constant_exprt &size();
 
protected:
  // Use element_type() instead
  using type_with_subtypet::subtype;
};
 
template <>
inline bool can_cast_type<vector_typet>(const typet &type)
{
  return type.id() == ID_vector;
}
 
inline const vector_typet &to_vector_type(const typet &type)
{
  PRECONDITION(can_cast_type<vector_typet>(type));
  type_with_subtypet::check(type);
  return static_cast<const vector_typet &>(type);
}
 
inline vector_typet &to_vector_type(typet &type)
{
  PRECONDITION(can_cast_type<vector_typet>(type));
  type_with_subtypet::check(type);
  return static_cast<vector_typet &>(type);
}
 
class complex_typet:public type_with_subtypet
{
public:
  explicit complex_typet(typet _subtype)
    : type_with_subtypet(ID_complex, std::move(_subtype))
  {
  }
};
 
template <>
inline bool can_cast_type<complex_typet>(const typet &type)
{
  return type.id() == ID_complex;
}
 
inline const complex_typet &to_complex_type(const typet &type)
{
  PRECONDITION(can_cast_type<complex_typet>(type));
  type_with_subtypet::check(type);
  return static_cast<const complex_typet &>(type);
}
 
inline complex_typet &to_complex_type(typet &type)
{
  PRECONDITION(can_cast_type<complex_typet>(type));
  type_with_subtypet::check(type);
  return static_cast<complex_typet &>(type);
}
 
bool is_constant_or_has_constant_components(
  const typet &type,
  const namespacet &ns);
 
#endif // CPROVER_UTIL_STD_TYPES_H