From a8dce46ccc4b6a39fbac5070e199e8558e0dfccf Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 8 Mar 2021 10:56:17 +0000 Subject: [PATCH] move pointer_typet to pointer_expr.h The rationale is that types of a particular group (say bitvectors or pointers) are often used together with the expressions that are specific for them. The goal is that std_types.h will only contain the basic types, such as bool_typet. --- .../abstract_pointer_object.cpp | 2 + src/cpp/cpp_is_pod.cpp | 2 + src/cpp/cpp_type2name.cpp | 2 +- src/cpp/expr2cpp.cpp | 8 +- src/goto-programs/xml_expr.cpp | 2 +- src/solvers/flattening/boolbv_width.cpp | 1 + src/util/base_type.cpp | 1 + src/util/c_types.h | 1 + src/util/format_type.cpp | 1 + src/util/pointer_expr.h | 125 ++++++++++++++++++ src/util/refined_string_type.h | 2 +- src/util/std_types.h | 125 ------------------ src/util/validate_types.cpp | 2 +- 13 files changed, 141 insertions(+), 133 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_pointer_object.cpp b/src/analyses/variable-sensitivity/abstract_pointer_object.cpp index cd9fd2431429..e83a33977e72 100644 --- a/src/analyses/variable-sensitivity/abstract_pointer_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_pointer_object.cpp @@ -9,6 +9,8 @@ #include #include +#include + abstract_pointer_objectt::abstract_pointer_objectt(const typet &t) : abstract_objectt(t) { diff --git a/src/cpp/cpp_is_pod.cpp b/src/cpp/cpp_is_pod.cpp index 7b53a520b7bc..1c0ad8bdba0b 100644 --- a/src/cpp/cpp_is_pod.cpp +++ b/src/cpp/cpp_is_pod.cpp @@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_typecheck.h" +#include + bool cpp_typecheckt::cpp_is_pod(const typet &type) const { if(type.id()==ID_struct) diff --git a/src/cpp/cpp_type2name.cpp b/src/cpp/cpp_type2name.cpp index 31e3c5d2f787..50d65d8e7e66 100644 --- a/src/cpp/cpp_type2name.cpp +++ b/src/cpp/cpp_type2name.cpp @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include +#include #include static std::string do_prefix(const std::string &s) diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp index 00596de1b8a1..008f24f06787 100644 --- a/src/cpp/expr2cpp.cpp +++ b/src/cpp/expr2cpp.cpp @@ -8,12 +8,12 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "expr2cpp.h" -#include -#include -#include -#include #include +#include #include +#include +#include +#include #include #include diff --git a/src/goto-programs/xml_expr.cpp b/src/goto-programs/xml_expr.cpp index b3dacf2e9aaf..7b6a810d35b1 100644 --- a/src/goto-programs/xml_expr.cpp +++ b/src/goto-programs/xml_expr.cpp @@ -20,7 +20,7 @@ Author: Daniel Kroening #include #include #include -#include +#include #include xmlt xml(const typet &type, const namespacet &ns) diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp index be1848d65ee6..5f9777371d9a 100644 --- a/src/solvers/flattening/boolbv_width.cpp +++ b/src/solvers/flattening/boolbv_width.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include boolbv_widtht::boolbv_widtht(const namespacet &_ns):ns(_ns) diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp index f352a834dbdf..5e1c80b0b966 100644 --- a/src/util/base_type.cpp +++ b/src/util/base_type.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "namespace.h" +#include "pointer_expr.h" #include "std_types.h" #include "symbol.h" #include "union_find.h" diff --git a/src/util/c_types.h b/src/util/c_types.h index 998066f60fe9..d3ad77bd7763 100644 --- a/src/util/c_types.h +++ b/src/util/c_types.h @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_C_TYPES_H #define CPROVER_UTIL_C_TYPES_H +#include "pointer_expr.h" #include "std_types.h" bitvector_typet index_type(); diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp index b0b38d94a58c..69a094859574 100644 --- a/src/util/format_type.cpp +++ b/src/util/format_type.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "format_type.h" #include "format_expr.h" +#include "pointer_expr.h" #include "std_types.h" #include diff --git a/src/util/pointer_expr.h b/src/util/pointer_expr.h index a5ef99dee729..57c20749fb09 100644 --- a/src/util/pointer_expr.h +++ b/src/util/pointer_expr.h @@ -16,6 +16,131 @@ Author: Daniel Kroening, kroening@kroening.com class namespacet; +/// The pointer type +/// These are both 'bitvector_typet' (they have a width) +/// and 'type_with_subtypet' (they have a subtype) +class pointer_typet : public bitvector_typet +{ +public: + pointer_typet(typet _subtype, std::size_t width) + : bitvector_typet(ID_pointer, width) + { + subtype().swap(_subtype); + } + + signedbv_typet difference_type() const + { + return signedbv_typet(get_width()); + } + + static void check( + const typet &type, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK(vm, !type.get(ID_width).empty(), "pointer must have width"); + } +}; + +/// Check whether a reference to a typet is a \ref pointer_typet. +/// \param type: Source type. +/// \return True if \p 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 +/// pointer_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref pointer_typet. +inline const pointer_typet &to_pointer_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + pointer_typet::check(type); + return static_cast(type); +} + +/// \copydoc to_pointer_type(const typet &) +inline pointer_typet &to_pointer_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + pointer_typet::check(type); + return static_cast(type); +} + +/// This method tests, +/// if the given typet is a pointer of type void. +inline bool is_void_pointer(const typet &type) +{ + return type.id() == ID_pointer && type.subtype().id() == ID_empty; +} + +/// The reference type +/// +/// Intends to model C++ reference. Comparing to \ref pointer_typet should +/// never be null. +class reference_typet : public pointer_typet +{ +public: + reference_typet(typet _subtype, std::size_t _width) + : pointer_typet(std::move(_subtype), _width) + { + set(ID_C_reference, true); + } + + static void check( + const typet &type, + const validation_modet vm = validation_modet::INVARIANT) + { + PRECONDITION(type.id() == ID_pointer); + const reference_typet &reference_type = + static_cast(type); + DATA_CHECK( + vm, !reference_type.get(ID_width).empty(), "reference must have width"); + DATA_CHECK( + vm, reference_type.get_width() > 0, "reference must have non-zero width"); + } +}; + +/// Check whether a reference to a typet is a \ref reference_typet. +/// \param type: Source type. +/// \return True if \p 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); +} + +/// \brief Cast a typet to a \ref reference_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// reference_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref reference_typet. +inline const reference_typet &to_reference_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + +/// \copydoc to_reference_type(const typet &) +inline reference_typet &to_reference_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + return static_cast(type); +} + +bool is_reference(const typet &type); + +bool is_rvalue_reference(const typet &type); + /// \brief Split an expression into a base object and a (byte) offset class object_descriptor_exprt : public binary_exprt { diff --git a/src/util/refined_string_type.h b/src/util/refined_string_type.h index 706967ff2db7..2fce2cc56a9b 100644 --- a/src/util/refined_string_type.h +++ b/src/util/refined_string_type.h @@ -20,7 +20,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #define CPROVER_UTIL_REFINED_STRING_TYPE_H #include "cprover_prefix.h" -#include "std_types.h" +#include "pointer_expr.h" // Internal type used for string refinement class refined_string_typet: public struct_typet diff --git a/src/util/std_types.h b/src/util/std_types.h index 8641c0aee721..19245f2be9ef 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -1488,131 +1488,6 @@ inline c_bit_field_typet &to_c_bit_field_type(typet &type) return static_cast(type); } -/// The pointer type -/// These are both 'bitvector_typet' (they have a width) -/// and 'type_with_subtypet' (they have a subtype) -class pointer_typet:public bitvector_typet -{ -public: - pointer_typet(typet _subtype, std::size_t width) - : bitvector_typet(ID_pointer, width) - { - subtype().swap(_subtype); - } - - signedbv_typet difference_type() const - { - return signedbv_typet(get_width()); - } - - static void check( - const typet &type, - const validation_modet vm = validation_modet::INVARIANT) - { - DATA_CHECK(vm, !type.get(ID_width).empty(), "pointer must have width"); - } -}; - -/// Check whether a reference to a typet is a \ref pointer_typet. -/// \param type: Source type. -/// \return True if \p 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 -/// pointer_typet. Will fail with a precondition violation if type -/// doesn't match. -/// -/// \param type: Source type. -/// \return Object of type \ref pointer_typet. -inline const pointer_typet &to_pointer_type(const typet &type) -{ - PRECONDITION(can_cast_type(type)); - pointer_typet::check(type); - return static_cast(type); -} - -/// \copydoc to_pointer_type(const typet &) -inline pointer_typet &to_pointer_type(typet &type) -{ - PRECONDITION(can_cast_type(type)); - pointer_typet::check(type); - return static_cast(type); -} - -/// This method tests, -/// if the given typet is a pointer of type void. -inline bool is_void_pointer(const typet &type) -{ - return type.id() == ID_pointer && type.subtype().id() == ID_empty; -} - -/// The reference type -/// -/// Intends to model C++ reference. Comparing to \ref pointer_typet should -/// never be null. -class reference_typet:public pointer_typet -{ -public: - reference_typet(typet _subtype, std::size_t _width) - : pointer_typet(std::move(_subtype), _width) - { - set(ID_C_reference, true); - } - - static void check( - const typet &type, - const validation_modet vm = validation_modet::INVARIANT) - { - PRECONDITION(type.id() == ID_pointer); - const reference_typet &reference_type = - static_cast(type); - DATA_CHECK( - vm, !reference_type.get(ID_width).empty(), "reference must have width"); - DATA_CHECK( - vm, reference_type.get_width() > 0, "reference must have non-zero width"); - } -}; - -/// Check whether a reference to a typet is a \ref reference_typet. -/// \param type: Source type. -/// \return True if \p 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); -} - -/// \brief Cast a typet to a \ref reference_typet -/// -/// This is an unchecked conversion. \a type must be known to be \ref -/// reference_typet. Will fail with a precondition violation if type -/// doesn't match. -/// -/// \param type: Source type. -/// \return Object of type \ref reference_typet. -inline const reference_typet &to_reference_type(const typet &type) -{ - PRECONDITION(can_cast_type(type)); - return static_cast(type); -} - -/// \copydoc to_reference_type(const typet &) -inline reference_typet &to_reference_type(typet &type) -{ - PRECONDITION(can_cast_type(type)); - return static_cast(type); -} - -bool is_reference(const typet &type); - -bool is_rvalue_reference(const typet &type); - /// The C/C++ Booleans class c_bool_typet:public bitvector_typet { diff --git a/src/util/validate_types.cpp b/src/util/validate_types.cpp index 6f833852c3fd..a68b05b39757 100644 --- a/src/util/validate_types.cpp +++ b/src/util/validate_types.cpp @@ -13,7 +13,7 @@ Author: Daniel Poetzl #endif #include "namespace.h" -#include "std_types.h" +#include "pointer_expr.h" #include "type.h" #include "validate.h" #include "validate_helpers.h"