Merge pull request #5895 from diffblue/move_pointer_typet

kroening · web-flow · commit 94c64daa2d17 · 2021-03-08T16:17:48.000Z
Move pointer_typet into pointer_expr.h
diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt
@@ -92,10 +92,10 @@ warning: Included by graph for 'invariant.h' not generated, too many nodes (187)
 warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'message.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'namespace.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (106), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_expr.h' not generated, too many nodes (244), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_types.h' not generated, too many nodes (121), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_expr.h' not generated, too many nodes (243), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_types.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
diff --git a/src/analyses/variable-sensitivity/abstract_pointer_object.cpp b/src/analyses/variable-sensitivity/abstract_pointer_object.cpp
@@ -9,6 +9,8 @@
 #include <analyses/variable-sensitivity/abstract_environment.h>
 #include <analyses/variable-sensitivity/abstract_pointer_object.h>
 
+#include <util/pointer_expr.h>
+
 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
@@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_typecheck.h"
 
+#include <util/pointer_expr.h>
+
 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
@@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <string>
 
 #include <util/cprover_prefix.h>
-#include <util/std_types.h>
+#include <util/pointer_expr.h>
 #include <util/type.h>
 
 static std::string do_prefix(const std::string &s)
diff --git 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 <util/std_types.h>
-#include <util/std_expr.h>
-#include <util/symbol.h>
-#include <util/lispirep.h>
 #include <util/lispexpr.h>
+#include <util/lispirep.h>
 #include <util/namespace.h>
+#include <util/pointer_expr.h>
+#include <util/std_expr.h>
+#include <util/symbol.h>
 
 #include <ansi-c/c_misc.h>
 #include <ansi-c/c_qualifiers.h>
diff --git a/src/goto-programs/xml_expr.cpp b/src/goto-programs/xml_expr.cpp
@@ -20,7 +20,7 @@ Author: Daniel Kroening
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/namespace.h>
-#include <util/std_expr.h>
+#include <util/pointer_expr.h>
 #include <util/xml.h>
 
 xmlt xml(const typet &type, const namespacet &ns)
diff --git 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 <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/namespace.h>
+#include <util/pointer_expr.h>
 #include <util/std_types.h>
 
 boolbv_widtht::boolbv_widtht(const namespacet &_ns):ns(_ns)
diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <set>
 
 #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
@@ -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
@@ -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 <ostream>
diff --git 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<pointer_typet>(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<pointer_typet>(type));
+  pointer_typet::check(type);
+  return static_cast<const pointer_typet &>(type);
+}
+
+/// \copydoc to_pointer_type(const typet &)
+inline pointer_typet &to_pointer_type(typet &type)
+{
+  PRECONDITION(can_cast_type<pointer_typet>(type));
+  pointer_typet::check(type);
+  return static_cast<pointer_typet &>(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<const reference_typet &>(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<reference_typet>(const typet &type)
+{
+  return can_cast_type<pointer_typet>(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<reference_typet>(type));
+  return static_cast<const reference_typet &>(type);
+}
+
+/// \copydoc to_reference_type(const typet &)
+inline reference_typet &to_reference_type(typet &type)
+{
+  PRECONDITION(can_cast_type<reference_typet>(type));
+  return static_cast<reference_typet &>(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
@@ -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
@@ -1488,131 +1488,6 @@ inline c_bit_field_typet &to_c_bit_field_type(typet &type)
   return static_cast<c_bit_field_typet &>(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<pointer_typet>(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<pointer_typet>(type));
-  pointer_typet::check(type);
-  return static_cast<const pointer_typet &>(type);
-}
-
-/// \copydoc to_pointer_type(const typet &)
-inline pointer_typet &to_pointer_type(typet &type)
-{
-  PRECONDITION(can_cast_type<pointer_typet>(type));
-  pointer_typet::check(type);
-  return static_cast<pointer_typet &>(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<const reference_typet &>(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<reference_typet>(const typet &type)
-{
-  return can_cast_type<pointer_typet>(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<reference_typet>(type));
-  return static_cast<const reference_typet &>(type);
-}
-
-/// \copydoc to_reference_type(const typet &)
-inline reference_typet &to_reference_type(typet &type)
-{
-  PRECONDITION(can_cast_type<reference_typet>(type));
-  return static_cast<reference_typet &>(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
@@ -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"

Original file line number	Diff line number	Diff line change
`@@ -9,6 +9,8 @@`
`9`	`9`	`#include <analyses/variable-sensitivity/abstract_environment.h>`
`10`	`10`	`#include <analyses/variable-sensitivity/abstract_pointer_object.h>`
`11`	`11`
	`12`	`+#include <util/pointer_expr.h>`
	`13`	`+`
`12`	`14`	`abstract_pointer_objectt::abstract_pointer_objectt(const typet &t)`
`13`	`15`	`: abstract_objectt(t)`
`14`	`16`	`{`
Original file line number	Diff line number	Diff line change
`@@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu`
`11`	`11`
`12`	`12`	`#include "cpp_typecheck.h"`
`13`	`13`
	`14`	`+#include <util/pointer_expr.h>`
	`15`	`+`
`14`	`16`	`bool cpp_typecheckt::cpp_is_pod(const typet &type) const`
`15`	`17`	`{`
`16`	`18`	`if(type.id()==ID_struct)`