From 91dc2203e093aa938f564eeb1cc732f41d54aa1d Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 22 Aug 2018 10:09:00 +0100 Subject: [PATCH 1/4] Move functions from type to std_types --- .../java_bytecode/ci_lazy_methods_needed.h | 3 +- src/util/std_types.cpp | 84 ++++++++++++++++- src/util/std_types.h | 7 ++ src/util/type.cpp | 90 ------------------- src/util/type.h | 8 -- 5 files changed, 92 insertions(+), 100 deletions(-) diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.h b/jbmc/src/java_bytecode/ci_lazy_methods_needed.h index da9c3fe83ac..49e18d38bbf 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.h +++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.h @@ -12,10 +12,11 @@ Author: Chris Smowton, chris.smowton@diffblue.com #ifndef CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H #define CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H -#include #include #include +#include #include +#include class select_pointer_typet; class pointer_typet; diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp index 0712ad7cbe1..e8e0f72dfad 100644 --- a/src/util/std_types.cpp +++ b/src/util/std_types.cpp @@ -12,9 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "std_types.h" -#include "string2int.h" #include "arith_tools.h" +#include "namespace.h" #include "std_expr.h" +#include "string2int.h" std::size_t fixedbv_typet::get_integer_bits() const { @@ -195,3 +196,84 @@ constant_exprt unsignedbv_typet::largest_expr() const { return from_integer(largest(), *this); } + +/// Returns true if the type is a rational, real, integer, natural, complex, +/// unsignedbv, signedbv, floatbv or fixedbv. +bool is_number(const typet &type) +{ + const irep_idt &id = type.id(); + return id == ID_rational || id == ID_real || id == ID_integer || + id == ID_natural || id == ID_complex || id == ID_unsignedbv || + id == ID_signedbv || id == ID_floatbv || id == ID_fixedbv; +} + +/// Identify whether a given type is constant itself or contains constant +/// components. +/// Examples include: +/// - const int a; +/// - struct contains_constant_pointer { int x; int * const p; }; +/// - const int b[3]; +/// \param type The type we want to query constness of. +/// \param ns The namespace, needed for resolution of symbols. +/// \return Whether passed in type is const or not. +bool is_constant_or_has_constant_components( + const typet &type, + const namespacet &ns) +{ + // Helper function to avoid the code duplication in the branches + // below. + const auto has_constant_components = [&ns](const typet &subtype) -> bool { + if(subtype.id() == ID_struct || subtype.id() == ID_union) + { + const auto &struct_union_type = to_struct_union_type(subtype); + for(const auto &component : struct_union_type.components()) + { + if(is_constant_or_has_constant_components(component.type(), ns)) + return true; + } + } + return false; + }; + + // There are 4 possibilities the code below is handling. + // The possibilities are enumerated as comments, to show + // what each code is supposed to be handling. For more + // comprehensive test case for this, take a look at + // regression/cbmc/no_nondet_static/main.c + + // const int a; + if(type.get_bool(ID_C_constant)) + return true; + + // This is a termination condition to break the recursion + // for recursive types such as the following: + // struct list { const int datum; struct list * next; }; + // NOTE: the difference between this condition and the previous + // one is that this one always returns. + if(type.id() == ID_pointer) + return type.get_bool(ID_C_constant); + + // When we have a case like the following, we don't immediately + // see the struct t. Instead, we only get to see symbol t1, which + // we have to use the namespace to resolve to its definition: + // struct t { const int a; }; + // struct t t1; + if(type.id() == ID_symbol_type) + { + const auto &resolved_type = ns.follow(type); + return has_constant_components(resolved_type); + } + + // In a case like this, where we see an array (b[3] here), we know that + // the array contains subtypes. We get the first one, and + // then resolve it to its definition through the usage of the namespace. + // struct contains_constant_pointer { int x; int * const p; }; + // struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} }; + if(type.has_subtype()) + { + const auto &subtype = type.subtype(); + return is_constant_or_has_constant_components(subtype, ns); + } + + return false; +} diff --git a/src/util/std_types.h b/src/util/std_types.h index 3cf53f56db1..8795a54c762 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com #include class constant_exprt; +class namespacet; /// The Boolean type class bool_typet:public typet @@ -1708,4 +1709,10 @@ inline mathematical_function_typet & return static_cast(type); } +bool is_number(const typet &type); + +bool is_constant_or_has_constant_components( + const typet &type, + const namespacet &ns); + #endif // CPROVER_UTIL_STD_TYPES_H diff --git a/src/util/type.cpp b/src/util/type.cpp index 735f8ed2129..6919e3978b1 100644 --- a/src/util/type.cpp +++ b/src/util/type.cpp @@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com /// Implementations of some functions of typet #include "type.h" -#include "std_types.h" -#include "namespace.h" /// Copy the provided type to the subtypes of this type. /// \param type The type to add to subtypes @@ -30,91 +28,3 @@ void typet::move_to_subtypes(typet &type) sub.push_back(static_cast(get_nil_irep())); sub.back().swap(type); } - -/// Returns true if the type is a rational, real, integer, natural, complex, -/// unsignedbv, signedbv, floatbv or fixedbv. -bool is_number(const typet &type) -{ - const irep_idt &id=type.id(); - return id==ID_rational || - id==ID_real || - id==ID_integer || - id==ID_natural || - id==ID_complex || - id==ID_unsignedbv || - id==ID_signedbv || - id==ID_floatbv || - id==ID_fixedbv; -} - -/// Identify whether a given type is constant itself or contains constant -/// components. -/// Examples include: -/// - const int a; -/// - struct contains_constant_pointer { int x; int * const p; }; -/// - const int b[3]; -/// \param type The type we want to query constness of. -/// \param ns The namespace, needed for resolution of symbols. -/// \return Whether passed in type is const or not. -bool is_constant_or_has_constant_components( - const typet &type, const namespacet &ns) -{ - // Helper function to avoid the code duplication in the branches - // below. - const auto has_constant_components = - [&ns](const typet &subtype) -> bool - { - if(subtype.id() == ID_struct || subtype.id() == ID_union) - { - const auto &struct_union_type = to_struct_union_type(subtype); - for(const auto &component : struct_union_type.components()) - { - if(is_constant_or_has_constant_components(component.type(), ns)) - return true; - } - } - return false; - }; - - // There are 4 possibilities the code below is handling. - // The possibilities are enumerated as comments, to show - // what each code is supposed to be handling. For more - // comprehensive test case for this, take a look at - // regression/cbmc/no_nondet_static/main.c - - // const int a; - if(type.get_bool(ID_C_constant)) - return true; - - // This is a termination condition to break the recursion - // for recursive types such as the following: - // struct list { const int datum; struct list * next; }; - // NOTE: the difference between this condition and the previous - // one is that this one always returns. - if(type.id()==ID_pointer) - return type.get_bool(ID_C_constant); - - // When we have a case like the following, we don't immediately - // see the struct t. Instead, we only get to see symbol t1, which - // we have to use the namespace to resolve to its definition: - // struct t { const int a; }; - // struct t t1; - if(type.id() == ID_symbol_type) - { - const auto &resolved_type = ns.follow(type); - return has_constant_components(resolved_type); - } - - // In a case like this, where we see an array (b[3] here), we know that - // the array contains subtypes. We get the first one, and - // then resolve it to its definition through the usage of the namespace. - // struct contains_constant_pointer { int x; int * const p; }; - // struct contains_constant_pointer b[3] = { {23, &y}, {23, &y}, {23, &y} }; - if(type.has_subtype()) - { - const auto &subtype = type.subtype(); - return is_constant_or_has_constant_components(subtype, ns); - } - - return false; -} diff --git a/src/util/type.h b/src/util/type.h index d2ea25f2d95..81e6abe535d 100644 --- a/src/util/type.h +++ b/src/util/type.h @@ -18,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com #define SUBTYPE_IN_GETSUB #define SUBTYPES_IN_GETSUB -class namespacet; - /// The type of an expression, extends irept. Types may have subtypes. This is /// modeled with two subs named “subtype” (a single type) and “subtypes” /// (a vector of types). The class typet only adds specialized methods @@ -177,10 +175,4 @@ class type_with_subtypest:public typet for(typet::subtypest::iterator it=(type).subtypes().begin(); \ it!=(type).subtypes().end(); ++it) -bool is_number(const typet &type); - -bool is_constant_or_has_constant_components( - const typet &type, - const namespacet &ns); - #endif // CPROVER_UTIL_TYPE_H From a449f734a3c2790fa22c64d371312cd8b97ea0a1 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 22 Aug 2018 11:19:26 +0100 Subject: [PATCH 2/4] Add missing can_casts and casts --- src/util/std_types.h | 438 ++++++++++++++++++++++++++++++++----------- 1 file changed, 328 insertions(+), 110 deletions(-) diff --git a/src/util/std_types.h b/src/util/std_types.h index 8795a54c762..e129bd1148a 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -112,6 +112,15 @@ class symbol_typet:public typet } }; +/// Check whether a reference to a typet is a \ref symbol_typet. +/// \param type Source type. +/// \return True if \param type is a \ref symbol_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_symbol_type; +} + /// \brief Cast a typet to a \ref symbol_typet. /// /// This is an unchecked conversion. \a type must be known to be @@ -122,26 +131,17 @@ class symbol_typet:public typet /// \return Object of type \ref symbol_typet. inline const symbol_typet &to_symbol_type(const typet &type) { - PRECONDITION(type.id() == ID_symbol_type); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_symbol_type(const typet &) inline symbol_typet &to_symbol_type(typet &type) { - PRECONDITION(type.id() == ID_symbol_type); + PRECONDITION(can_cast_type(type)); return static_cast(type); } -/// Check whether a reference to a typet is a \ref symbol_typet. -/// \param type Source type. -/// \return True if \param type is a \ref symbol_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return type.id() == ID_symbol_type; -} - /// Base type for structs and unions /// /// For example C structs, C unions, C++ classes, Java classes. @@ -253,6 +253,15 @@ class struct_union_typet:public typet void set_tag(const irep_idt &tag) { set(ID_tag, tag); } }; +/// Check whether a reference to a typet is a \ref struct_union_typet. +/// \param type Source type. +/// \return True if \param type is a \ref struct_union_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_struct || type.id() == ID_union; +} + /// \brief Cast a typet to a \ref struct_union_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -263,14 +272,14 @@ class struct_union_typet:public typet /// \return Object of type \ref struct_union_typet inline const struct_union_typet &to_struct_union_type(const typet &type) { - PRECONDITION(type.id()==ID_struct || type.id()==ID_union); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_struct_union_type(const typet &) inline struct_union_typet &to_struct_union_type(typet &type) { - PRECONDITION(type.id()==ID_struct || type.id()==ID_union); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -285,6 +294,15 @@ class struct_typet:public struct_union_typet bool is_prefix_of(const struct_typet &other) const; }; +/// Check whether a reference to a typet is a \ref struct_typet. +/// \param type Source type. +/// \return True if \param type is a \ref struct_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_struct; +} + /// \brief Cast a typet to a \ref struct_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -295,26 +313,17 @@ class struct_typet:public struct_union_typet /// \return Object of type \ref struct_typet. inline const struct_typet &to_struct_type(const typet &type) { - PRECONDITION(type.id()==ID_struct); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_struct_type(const typet &) inline struct_typet &to_struct_type(typet &type) { - PRECONDITION(type.id()==ID_struct); + PRECONDITION(can_cast_type(type)); return static_cast(type); } -/// Check whether a reference to a typet is a \ref struct_typet. -/// \param type Source type. -/// \return True if \param type is a \ref struct_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return type.id() == ID_struct; -} - /// Class type /// /// For example, C++ and Java classes. @@ -402,6 +411,15 @@ class class_typet:public struct_typet } }; +/// Check whether a reference to a typet is a \ref class_typet. +/// \param type Source type. +/// \return True if \param type is a \ref class_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return can_cast_type(type) && type.get_bool(ID_C_class); +} + /// \brief Cast a typet to a \ref class_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -412,26 +430,17 @@ class class_typet:public struct_typet /// \return Object of type \ref class_typet. inline const class_typet &to_class_type(const typet &type) { - PRECONDITION(type.id()==ID_struct); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_class_type(const typet &) inline class_typet &to_class_type(typet &type) { - PRECONDITION(type.id()==ID_struct); + PRECONDITION(can_cast_type(type)); return static_cast(type); } -/// Check whether a reference to a typet is a \ref class_typet. -/// \param type Source type. -/// \return True if \param type is a \ref class_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return can_cast_type(type) && type.get_bool(ID_C_class); -} - /// The union type /// /// For example, C union. @@ -443,6 +452,15 @@ class union_typet:public struct_union_typet } }; +/// Check whether a reference to a typet is a \ref union_typet. +/// \param type Source type. +/// \return True if \param type is a \ref union_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_union; +} + /// \brief Cast a typet to a \ref union_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -453,14 +471,14 @@ class union_typet:public struct_union_typet /// \return Object of type \ref union_typet inline const union_typet &to_union_type(const typet &type) { - PRECONDITION(type.id()==ID_union); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_union_type(const typet &) inline union_typet &to_union_type(typet &type) { - PRECONDITION(type.id()==ID_union); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -486,6 +504,16 @@ class tag_typet:public typet } }; +/// Check whether a reference to a typet is a \ref tag_typet. +/// \param type Source type. +/// \return True if \param type is a \ref tag_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_c_enum_tag || type.id() == ID_struct_tag || + type.id() == ID_union_tag; +} + /// \brief Cast a typet to a \ref tag_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -496,18 +524,14 @@ class tag_typet:public typet /// \return Object of type \ref tag_typet. inline const tag_typet &to_tag_type(const typet &type) { - PRECONDITION(type.id()==ID_c_enum_tag || - type.id()==ID_struct_tag || - type.id()==ID_union_tag); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_tag_type(const typet &) inline tag_typet &to_tag_type(typet &type) { - PRECONDITION(type.id()==ID_c_enum_tag || - type.id()==ID_struct_tag || - type.id()==ID_union_tag); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -521,6 +545,15 @@ class struct_tag_typet:public tag_typet } }; +/// Check whether a reference to a typet is a \ref struct_tag_typet. +/// \param type Source type. +/// \return True if \param type is a \ref struct_tag_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_struct_tag; +} + /// \brief Cast a typet to a \ref struct_tag_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -531,14 +564,14 @@ class struct_tag_typet:public tag_typet /// \return Object of type \ref struct_tag_typet inline const struct_tag_typet &to_struct_tag_type(const typet &type) { - PRECONDITION(type.id()==ID_struct_tag); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_struct_tag_type(const typet &) inline struct_tag_typet &to_struct_tag_type(typet &type) { - PRECONDITION(type.id()==ID_struct_tag); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -552,6 +585,15 @@ class union_tag_typet:public tag_typet } }; +/// Check whether a reference to a typet is a \ref union_tag_typet. +/// \param type Source type. +/// \return True if \param type is a \ref union_tag_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_union_tag; +} + /// \brief Cast a typet to a \ref union_tag_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -562,14 +604,14 @@ class union_tag_typet:public tag_typet /// \return Object of type \ref union_tag_typet. inline const union_tag_typet &to_union_tag_type(const typet &type) { - PRECONDITION(type.id()==ID_union_tag); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_union_tag_type(const typet &) inline union_tag_typet &to_union_tag_type(typet &type) { - PRECONDITION(type.id()==ID_union_tag); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -593,6 +635,15 @@ class enumeration_typet:public typet } }; +/// Check whether a reference to a typet is a \ref enumeration_typet. +/// \param type Source type. +/// \return True if \param type is a \ref enumeration_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_enumeration; +} + /// \brief Cast a typet to a \ref enumeration_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -603,14 +654,14 @@ class enumeration_typet:public typet /// \return Object of type \ref enumeration_typet. inline const enumeration_typet &to_enumeration_type(const typet &type) { - PRECONDITION(type.id()==ID_enumeration); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_enumeration_type(const typet &) inline enumeration_typet &to_enumeration_type(typet &type) { - PRECONDITION(type.id()==ID_enumeration); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -648,6 +699,15 @@ class c_enum_typet:public type_with_subtypet } }; +/// Check whether a reference to a typet is a \ref c_enum_typet. +/// \param type Source type. +/// \return True if \param type is a \ref c_enum_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_c_enum; +} + /// \brief Cast a typet to a \ref c_enum_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -658,14 +718,14 @@ class c_enum_typet:public type_with_subtypet /// \return Object of type \ref c_enum_typet. inline const c_enum_typet &to_c_enum_type(const typet &type) { - PRECONDITION(type.id()==ID_c_enum); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_c_enum_type(const typet &) inline c_enum_typet &to_c_enum_type(typet &type) { - PRECONDITION(type.id()==ID_c_enum); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -679,6 +739,15 @@ class c_enum_tag_typet:public tag_typet } }; +/// Check whether a reference to a typet is a \ref c_enum_tag_typet. +/// \param type Source type. +/// \return True if \param type is a \ref c_enum_tag_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_c_enum_tag; +} + /// \brief Cast a typet to a \ref c_enum_tag_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -689,14 +758,14 @@ class c_enum_tag_typet:public tag_typet /// \return Object of type \ref c_enum_tag_typet. inline const c_enum_tag_typet &to_c_enum_tag_type(const typet &type) { - PRECONDITION(type.id()==ID_c_enum_tag); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_c_enum_tag_type(const typet &) inline c_enum_tag_typet &to_c_enum_tag_type(typet &type) { - PRECONDITION(type.id()==ID_c_enum_tag); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -1024,6 +1093,15 @@ class incomplete_array_typet:public type_with_subtypet } }; +/// Check whether a reference to a typet is a \ref incomplete_array_typet. +/// \param type Source type. +/// \return True if \param type is a \ref incomplete_array_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_array; +} + /// \brief Cast a typet to an \ref incomplete_array_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1034,14 +1112,14 @@ class incomplete_array_typet:public type_with_subtypet /// \return Object of type \ref incomplete_array_typet. inline const incomplete_array_typet &to_incomplete_array_type(const typet &type) { - PRECONDITION(type.id()==ID_array); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_incomplete_array_type(const typet &) inline incomplete_array_typet &to_incomplete_array_type(typet &type) { - PRECONDITION(type.id()==ID_array); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -1088,6 +1166,20 @@ class bitvector_typet:public type_with_subtypet } }; +/// Check whether a reference to a typet is a \ref bitvector_typet. +/// \param type Source type. +/// \return True if \param type is a \ref bitvector_typet. +template <> +inline bool can_cast_type(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; +} + /// \brief Cast a typet to a \ref bitvector_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1098,16 +1190,7 @@ class bitvector_typet:public type_with_subtypet /// \return Object of type \ref bitvector_typet. inline const bitvector_typet &to_bitvector_type(const typet &type) { - PRECONDITION(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); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -1115,16 +1198,7 @@ inline const bitvector_typet &to_bitvector_type(const typet &type) /// \copydoc to_bitvector_type(const typet &type) inline bitvector_typet &to_bitvector_type(typet &type) { - PRECONDITION(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); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -1139,6 +1213,15 @@ class bv_typet:public bitvector_typet } }; +/// Check whether a reference to a typet is a \ref bv_typet. +/// \param type Source type. +/// \return True if \param type is a \ref bv_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_bv; +} + /// \brief Cast a typet to a \ref bv_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1149,14 +1232,14 @@ class bv_typet:public bitvector_typet /// \return Object of type \ref bv_typet. inline const bv_typet &to_bv_type(const typet &type) { - PRECONDITION(type.id()==ID_bv); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_bv_type(const typet &) inline bv_typet &to_bv_type(typet &type) { - PRECONDITION(type.id()==ID_bv); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -1176,6 +1259,15 @@ class unsignedbv_typet:public bitvector_typet constant_exprt largest_expr() const; }; +/// Check whether a reference to a typet is a \ref unsignedbv_typet. +/// \param type Source type. +/// \return True if \param type is a \ref unsignedbv_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_unsignedbv; +} + /// \brief Cast a typet to an \ref unsignedbv_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1186,14 +1278,14 @@ class unsignedbv_typet:public bitvector_typet /// \return Object of type \ref unsignedbv_typet. inline const unsignedbv_typet &to_unsignedbv_type(const typet &type) { - PRECONDITION(type.id()==ID_unsignedbv); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_unsignedbv_type(const typet &) inline unsignedbv_typet &to_unsignedbv_type(typet &type) { - PRECONDITION(type.id()==ID_unsignedbv); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -1213,6 +1305,15 @@ class signedbv_typet:public bitvector_typet constant_exprt largest_expr() const; }; +/// Check whether a reference to a typet is a \ref signedbv_typet. +/// \param type Source type. +/// \return True if \param type is a \ref signedbv_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_signedbv; +} + /// \brief Cast a typet to a \ref signedbv_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1223,14 +1324,14 @@ class signedbv_typet:public bitvector_typet /// \return Object of type \ref signedbv_typet. inline const signedbv_typet &to_signedbv_type(const typet &type) { - PRECONDITION(type.id()==ID_signedbv); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_signedbv_type(const typet &) inline signedbv_typet &to_signedbv_type(typet &type) { - PRECONDITION(type.id()==ID_signedbv); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -1258,6 +1359,15 @@ class fixedbv_typet:public bitvector_typet } }; +/// Check whether a reference to a typet is a \ref fixedbv_typet. +/// \param type Source type. +/// \return True if \param type is a \ref fixedbv_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_fixedbv; +} + /// \brief Cast a typet to a \ref fixedbv_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1268,10 +1378,17 @@ class fixedbv_typet:public bitvector_typet /// \return Object of type \ref fixedbv_typet. inline const fixedbv_typet &to_fixedbv_type(const typet &type) { - PRECONDITION(type.id()==ID_fixedbv); + PRECONDITION(can_cast_type(type)); return static_cast(type); } +/// \copydoc to_fixedbv_type(const typet &) +inline fixedbv_typet &to_fixedbv_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + /// Fixed-width bit-vector with IEEE floating-point interpretation class floatbv_typet:public bitvector_typet { @@ -1294,6 +1411,15 @@ class floatbv_typet:public bitvector_typet } }; +/// Check whether a reference to a typet is a \ref floatbv_typet. +/// \param type Source type. +/// \return True if \param type is a \ref floatbv_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_floatbv; +} + /// \brief Cast a typet to a \ref floatbv_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1304,10 +1430,17 @@ class floatbv_typet:public bitvector_typet /// \return Object of type \ref floatbv_typet. inline const floatbv_typet &to_floatbv_type(const typet &type) { - PRECONDITION(type.id()==ID_floatbv); + PRECONDITION(can_cast_type(type)); return static_cast(type); } +/// \copydoc to_floatbv_type(const typet &) +inline floatbv_typet &to_floatbv_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + /// Type for C bit fields class c_bit_field_typet:public bitvector_typet { @@ -1320,6 +1453,15 @@ class c_bit_field_typet:public bitvector_typet // These have a sub-type }; +/// Check whether a reference to a typet is a \ref c_bit_field_typet. +/// \param type Source type. +/// \return True if \param type is a \ref c_bit_field_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_c_bit_field; +} + /// \brief Cast a typet to a \ref c_bit_field_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1330,14 +1472,14 @@ class c_bit_field_typet:public bitvector_typet /// \return Object of type \ref c_bit_field_typet. inline const c_bit_field_typet &to_c_bit_field_type(const typet &type) { - PRECONDITION(type.id()==ID_c_bit_field); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_c_bit_field_type(const typet &type) inline c_bit_field_typet &to_c_bit_field_type(typet &type) { - PRECONDITION(type.id()==ID_c_bit_field); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -1356,6 +1498,15 @@ class pointer_typet:public bitvector_typet } }; +/// Check whether a reference to a typet is a \ref pointer_typet. +/// \param type Source type. +/// \return True if \param type is a \ref pointer_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_pointer; +} + /// \brief Cast a typet to a \ref pointer_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1366,7 +1517,7 @@ class pointer_typet:public bitvector_typet /// \return Object of type \ref pointer_typet. inline const pointer_typet &to_pointer_type(const typet &type) { - PRECONDITION(type.id()==ID_pointer); + PRECONDITION(can_cast_type(type)); const pointer_typet &ret = static_cast(type); validate_type(ret); return ret; @@ -1375,21 +1526,12 @@ inline const pointer_typet &to_pointer_type(const typet &type) /// \copydoc to_pointer_type(const typet &) inline pointer_typet &to_pointer_type(typet &type) { - PRECONDITION(type.id()==ID_pointer); + PRECONDITION(can_cast_type(type)); pointer_typet &ret = static_cast(type); validate_type(ret); return ret; } -/// Check whether a reference to a typet is a \ref pointer_typet. -/// \param type Source type. -/// \return True if \param type is a \ref pointer_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return type.id() == ID_pointer; -} - inline void validate_type(const pointer_typet &type) { DATA_INVARIANT(!type.get(ID_width).empty(), "pointer must have width"); @@ -1410,6 +1552,16 @@ class reference_typet:public pointer_typet } }; +/// Check whether a reference to a typet is a \ref reference_typet. +/// \param type Source type. +/// \return True if \param type is a \ref reference_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return can_cast_type(type) && type.get_bool(ID_C_reference) && + !type.get(ID_width).empty(); +} + /// \brief Cast a typet to a \ref reference_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1420,16 +1572,14 @@ class reference_typet:public pointer_typet /// \return Object of type \ref reference_typet. inline const reference_typet &to_reference_type(const typet &type) { - PRECONDITION(type.id()==ID_pointer && type.get_bool(ID_C_reference)); - PRECONDITION(!type.get(ID_width).empty()); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_reference_type(const typet &) inline reference_typet &to_reference_type(typet &type) { - PRECONDITION(type.id()==ID_pointer && type.get_bool(ID_C_reference)); - PRECONDITION(!type.get(ID_width).empty()); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -1451,6 +1601,15 @@ class c_bool_typet:public bitvector_typet } }; +/// Check whether a reference to a typet is a \ref c_bool_typet. +/// \param type Source type. +/// \return True if \param type is a \ref c_bool_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_c_bool; +} + /// \brief Cast a typet to a \ref c_bool_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1461,14 +1620,14 @@ class c_bool_typet:public bitvector_typet /// \return Object of type \ref c_bool_typet. inline const c_bool_typet &to_c_bool_type(const typet &type) { - PRECONDITION(type.id()==ID_c_bool); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_c_bool_type(const typet &) inline c_bool_typet &to_c_bool_type(typet &type) { - PRECONDITION(type.id()==ID_c_bool); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -1483,6 +1642,15 @@ class string_typet:public typet } }; +/// Check whether a reference to a typet is a \ref string_typet. +/// \param type Source type. +/// \return True if \param type is a \ref string_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_string; +} + /// \brief Cast a typet to a \ref string_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1493,10 +1661,17 @@ class string_typet:public typet /// \return Object of type \ref string_typet. inline const string_typet &to_string_type(const typet &type) { - PRECONDITION(type.id()==ID_string); + PRECONDITION(can_cast_type(type)); return static_cast(type); } +/// \copydoc to_string_type(const typet &) +inline string_typet &to_string_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + /// A type for subranges of integers class range_typet:public typet { @@ -1514,6 +1689,15 @@ class range_typet:public typet void set_to(const mp_integer &to); }; +/// Check whether a reference to a typet is a \ref range_typet. +/// \param type Source type. +/// \return True if \param type is a \ref range_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_range; +} + /// \brief Cast a typet to a \ref range_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1524,10 +1708,17 @@ class range_typet:public typet /// \return Object of type \ref range_typet. inline const range_typet &to_range_type(const typet &type) { - PRECONDITION(type.id()==ID_range); + PRECONDITION(can_cast_type(type)); return static_cast(type); } +/// \copydoc to_range_type(const typet &) +inline range_typet &to_range_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + /// The vector type /// /// Used to represent the short vectors used by CPU instruction sets such as @@ -1557,6 +1748,15 @@ class vector_typet:public type_with_subtypet } }; +/// Check whether a reference to a typet is a \ref vector_typet. +/// \param type Source type. +/// \return True if \param type is a \ref vector_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_vector; +} + /// \brief Cast a typet to a \ref vector_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1567,14 +1767,14 @@ class vector_typet:public type_with_subtypet /// \return Object of type \ref vector_typet. inline const vector_typet &to_vector_type(const typet &type) { - PRECONDITION(type.id()==ID_vector); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_vector_type(const typet &) inline vector_typet &to_vector_type(typet &type) { - PRECONDITION(type.id()==ID_vector); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -1592,6 +1792,15 @@ class complex_typet:public type_with_subtypet } }; +/// Check whether a reference to a typet is a \ref complex_typet. +/// \param type Source type. +/// \return True if \param type is a \ref complex_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_complex; +} + /// \brief Cast a typet to a \ref complex_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1602,14 +1811,14 @@ class complex_typet:public type_with_subtypet /// \return Object of type \ref complex_typet. inline const complex_typet &to_complex_type(const typet &type) { - PRECONDITION(type.id()==ID_complex); + PRECONDITION(can_cast_type(type)); return static_cast(type); } /// \copydoc to_complex_type(const typet &) inline complex_typet &to_complex_type(typet &type) { - PRECONDITION(type.id()==ID_complex); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -1686,6 +1895,15 @@ class mathematical_function_typet:public typet } }; +/// Check whether a reference to a typet is a \ref mathematical_function_typet. +/// \param type Source type. +/// \return True if \param type is a \ref mathematical_function_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_mathematical_function; +} + /// \brief Cast a typet to a \ref mathematical_function_typet /// /// This is an unchecked conversion. \a type must be known to be \ref @@ -1697,7 +1915,7 @@ class mathematical_function_typet:public typet inline const mathematical_function_typet & to_mathematical_function_type(const typet &type) { - PRECONDITION(type.id()==ID_mathematical_function); + PRECONDITION(can_cast_type(type)); return static_cast(type); } @@ -1705,7 +1923,7 @@ inline const mathematical_function_typet & inline mathematical_function_typet & to_mathematical_function_type(typet &type) { - PRECONDITION(type.id()==ID_mathematical_function); + PRECONDITION(can_cast_type(type)); return static_cast(type); } From 2c05b3a32263a0af121b94704a06649f6343e7fc Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 22 Aug 2018 11:31:44 +0100 Subject: [PATCH 3/4] Use type_try_dynamic_cast instead of direct id check and cast --- src/util/type_eq.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/util/type_eq.cpp b/src/util/type_eq.cpp index aefd710be0a..57e838116f0 100644 --- a/src/util/type_eq.cpp +++ b/src/util/type_eq.cpp @@ -32,18 +32,18 @@ bool type_eq(const typet &type1, const typet &type2, const namespacet &ns) if(type1==type2) return true; - if(type1.id() == ID_symbol_type) + if(const auto symbol_type1 = type_try_dynamic_cast(type1)) { - const symbolt &symbol = ns.lookup(to_symbol_type(type1)); + const symbolt &symbol = ns.lookup(*symbol_type1); if(!symbol.is_type) throw "symbol "+id2string(symbol.name)+" is not a type"; return type_eq(symbol.type, type2, ns); } - if(type2.id() == ID_symbol_type) + if(const auto symbol_type2 = type_try_dynamic_cast(type2)) { - const symbolt &symbol = ns.lookup(to_symbol_type(type2)); + const symbolt &symbol = ns.lookup(*symbol_type2); if(!symbol.is_type) throw "symbol "+id2string(symbol.name)+" is not a type"; From 1a28613b3bdaa25060c5f125a55504d6ea670a62 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 22 Aug 2018 11:45:49 +0100 Subject: [PATCH 4/4] Move mathematical types from std_types --- src/util/Makefile | 1 + src/util/mathematical_types.cpp | 23 +++++ src/util/mathematical_types.h | 162 ++++++++++++++++++++++++++++++++ src/util/simplify_expr_int.cpp | 1 + src/util/std_expr.h | 4 +- src/util/std_types.cpp | 10 -- src/util/std_types.h | 143 ---------------------------- src/util/type.h | 2 +- 8 files changed, 190 insertions(+), 156 deletions(-) create mode 100644 src/util/mathematical_types.cpp create mode 100644 src/util/mathematical_types.h diff --git a/src/util/Makefile b/src/util/Makefile index d19524cd81c..7be29d060ed 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -41,6 +41,7 @@ SRC = arith_tools.cpp \ json_stream.cpp \ lispexpr.cpp \ lispirep.cpp \ + mathematical_types.cpp \ memory_info.cpp \ merge_irep.cpp \ message.cpp \ diff --git a/src/util/mathematical_types.cpp b/src/util/mathematical_types.cpp new file mode 100644 index 00000000000..874f3e915d0 --- /dev/null +++ b/src/util/mathematical_types.cpp @@ -0,0 +1,23 @@ +/*******************************************************************\ + +Module: Mathematical types + +Author: Daniel Kroening, kroening@kroening.com + Maria Svorenova, maria.svorenova@diffblue.com + +\*******************************************************************/ + +/// \file +/// Mathematical types + +#include "mathematical_types.h" + +/// Returns true if the type is a rational, real, integer, natural, complex, +/// unsignedbv, signedbv, floatbv or fixedbv. +bool is_number(const typet &type) +{ + const irep_idt &id = type.id(); + return id == ID_rational || id == ID_real || id == ID_integer || + id == ID_natural || id == ID_complex || id == ID_unsignedbv || + id == ID_signedbv || id == ID_floatbv || id == ID_fixedbv; +} diff --git a/src/util/mathematical_types.h b/src/util/mathematical_types.h new file mode 100644 index 00000000000..e9645f8766a --- /dev/null +++ b/src/util/mathematical_types.h @@ -0,0 +1,162 @@ +/*******************************************************************\ + +Module: Mathematical types + +Author: Daniel Kroening, kroening@kroening.com + Maria Svorenova, maria.svorenova@diffblue.com + +\*******************************************************************/ + +/// \file +/// Mathematical types + +#ifndef CPROVER_UTIL_MATHEMATICAL_TYPES_H +#define CPROVER_UTIL_MATHEMATICAL_TYPES_H + +#include "expr_cast.h" +#include "invariant.h" +#include "type.h" + +/// Unbounded, signed integers (mathematical integers, not bitvectors) +class integer_typet : public typet +{ +public: + integer_typet() : typet(ID_integer) + { + } +}; + +/// Natural numbers including zero (mathematical integers, not bitvectors) +class natural_typet : public typet +{ +public: + natural_typet() : typet(ID_natural) + { + } +}; + +/// Unbounded, signed rational numbers +class rational_typet : public typet +{ +public: + rational_typet() : typet(ID_rational) + { + } +}; + +/// Unbounded, signed real numbers +class real_typet : public typet +{ +public: + real_typet() : typet(ID_real) + { + } +}; + +/// A type for mathematical functions (do not confuse with functions/methods +/// in code) +class mathematical_function_typet : public typet +{ +public: + // the domain of the function is composed of zero, one, or + // many variables + class variablet : public irept + { + public: + // the identifier is optional + irep_idt get_identifier() const + { + return get(ID_identifier); + } + + void set_identifier(const irep_idt &identifier) + { + return set(ID_identifier, identifier); + } + + typet &type() + { + return static_cast(add(ID_type)); + } + + const typet &type() const + { + return static_cast(find(ID_type)); + } + }; + + using domaint = std::vector; + + mathematical_function_typet(const domaint &_domain, const typet &_codomain) + : typet(ID_mathematical_function) + { + subtypes().resize(2); + domain() = _domain; + codomain() = _codomain; + } + + domaint &domain() + { + return (domaint &)subtypes()[0].subtypes(); + } + + const domaint &domain() const + { + return (const domaint &)subtypes()[0].subtypes(); + } + + variablet &add_variable() + { + auto &d = domain(); + d.push_back(variablet()); + return d.back(); + } + + /// Return the codomain, i.e., the set of values that the function maps to + /// (the "target"). + typet &codomain() + { + return subtypes()[1]; + } + + /// \copydoc codomain() + const typet &codomain() const + { + return subtypes()[1]; + } +}; + +/// Check whether a reference to a typet is a \ref mathematical_function_typet. +/// \param type Source type. +/// \return True if \param type is a \ref mathematical_function_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_mathematical_function; +} + +/// \brief Cast a typet to a \ref mathematical_function_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// mathematical_function_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type Source type. +/// \return Object of type \ref mathematical_function_typet. +inline const mathematical_function_typet & +to_mathematical_function_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + +/// \copydoc to_mathematical_function_type(const typet &) +inline mathematical_function_typet &to_mathematical_function_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + +bool is_number(const typet &type); + +#endif // CPROVER_UTIL_MATHEMATICAL_TYPES_H diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 6856c6a38fc..e16657b6143 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "fixedbv.h" #include "ieee_float.h" #include "invariant.h" +#include "mathematical_types.h" #include "namespace.h" #include "pointer_offset_size.h" #include "rational.h" diff --git a/src/util/std_expr.h b/src/util/std_expr.h index c9b22a083e7..f7f812f3076 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -13,10 +13,10 @@ Author: Daniel Kroening, kroening@kroening.com /// \file util/std_expr.h /// API to expression classes +#include "expr_cast.h" #include "invariant.h" +#include "mathematical_types.h" #include "std_types.h" -#include "expr_cast.h" - /// Transition system, consisting of state invariant, initial state predicate, /// and transition predicate. diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp index e8e0f72dfad..efa5420b171 100644 --- a/src/util/std_types.cpp +++ b/src/util/std_types.cpp @@ -197,16 +197,6 @@ constant_exprt unsignedbv_typet::largest_expr() const return from_integer(largest(), *this); } -/// Returns true if the type is a rational, real, integer, natural, complex, -/// unsignedbv, signedbv, floatbv or fixedbv. -bool is_number(const typet &type) -{ - const irep_idt &id = type.id(); - return id == ID_rational || id == ID_real || id == ID_integer || - id == ID_natural || id == ID_complex || id == ID_unsignedbv || - id == ID_signedbv || id == ID_floatbv || id == ID_fixedbv; -} - /// Identify whether a given type is constant itself or contains constant /// components. /// Examples include: diff --git a/src/util/std_types.h b/src/util/std_types.h index e129bd1148a..65df782c18f 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -56,42 +56,6 @@ class void_typet:public empty_typet { }; -/// Unbounded, signed integers (mathematical integers, not bitvectors) -class integer_typet:public typet -{ -public: - integer_typet():typet(ID_integer) - { - } -}; - -/// Natural numbers including zero (mathematical integers, not bitvectors) -class natural_typet:public typet -{ -public: - natural_typet():typet(ID_natural) - { - } -}; - -/// Unbounded, signed rational numbers -class rational_typet:public typet -{ -public: - rational_typet():typet(ID_rational) - { - } -}; - -/// Unbounded, signed real numbers -class real_typet:public typet -{ -public: - real_typet():typet(ID_real) - { - } -}; - /// A reference into the symbol table class symbol_typet:public typet { @@ -1822,113 +1786,6 @@ inline complex_typet &to_complex_type(typet &type) return static_cast(type); } -/// A type for mathematical functions (do not confuse with functions/methods -/// in code) -class mathematical_function_typet:public typet -{ -public: - // the domain of the function is composed of zero, one, or - // many variables - class variablet:public irept - { - public: - // the identifier is optional - irep_idt get_identifier() const - { - return get(ID_identifier); - } - - void set_identifier(const irep_idt &identifier) - { - return set(ID_identifier, identifier); - } - - typet &type() - { - return static_cast(add(ID_type)); - } - - const typet &type() const - { - return static_cast(find(ID_type)); - } - }; - - using domaint=std::vector; - - mathematical_function_typet(const domaint &_domain, const typet &_codomain) - : typet(ID_mathematical_function) - { - subtypes().resize(2); - domain() = _domain; - codomain() = _codomain; - } - - domaint &domain() - { - return (domaint &)subtypes()[0].subtypes(); - } - - const domaint &domain() const - { - return (const domaint &)subtypes()[0].subtypes(); - } - - variablet &add_variable() - { - auto &d=domain(); - d.push_back(variablet()); - return d.back(); - } - - /// Return the codomain, i.e., the set of values that the function maps to - /// (the "target"). - typet &codomain() - { - return subtypes()[1]; - } - - /// \copydoc codomain() - const typet &codomain() const - { - return subtypes()[1]; - } -}; - -/// Check whether a reference to a typet is a \ref mathematical_function_typet. -/// \param type Source type. -/// \return True if \param type is a \ref mathematical_function_typet. -template <> -inline bool can_cast_type(const typet &type) -{ - return type.id() == ID_mathematical_function; -} - -/// \brief Cast a typet to a \ref mathematical_function_typet -/// -/// This is an unchecked conversion. \a type must be known to be \ref -/// mathematical_function_typet. Will fail with a precondition violation if type -/// doesn't match. -/// -/// \param type Source type. -/// \return Object of type \ref mathematical_function_typet. -inline const mathematical_function_typet & - to_mathematical_function_type(const typet &type) -{ - PRECONDITION(can_cast_type(type)); - return static_cast(type); -} - -/// \copydoc to_mathematical_function_type(const typet &) -inline mathematical_function_typet & - to_mathematical_function_type(typet &type) -{ - PRECONDITION(can_cast_type(type)); - return static_cast(type); -} - -bool is_number(const typet &type); - bool is_constant_or_has_constant_components( const typet &type, const namespacet &ns); diff --git a/src/util/type.h b/src/util/type.h index 81e6abe535d..37d5a0b9b42 100644 --- a/src/util/type.h +++ b/src/util/type.h @@ -22,7 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com /// modeled with two subs named “subtype” (a single type) and “subtypes” /// (a vector of types). The class typet only adds specialized methods /// for accessing the subtype information to the interface of irept. -/// For pre-defined types see `std_types.h`. +/// For pre-defined types see `std_types.h` and `mathematical_types.h`. class typet:public irept { public: