push up all_zeros_expr and all_ones_expr helpers to bitvector_typet

src/ansi-c/c_typecheck_base.h

@@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <map>
 
 class ansi_c_declarationt;
+class bitvector_typet;
 class c_bit_field_typet;
 class shift_exprt;
 

src/ansi-c/literals/convert_integer_literal.cpp

@@ -11,13 +11,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "convert_integer_literal.h"
 
-#include <cctype>
-
 #include <util/arith_tools.h>
+#include <util/c_types.h> // IWYU pragma: keep
 #include <util/config.h>
 #include <util/std_expr.h>
 #include <util/string2int.h>
 
+#include <cctype>
+
 exprt convert_integer_literal(const std::string &src)
 {
   bool is_unsigned=false, is_imaginary=false;

src/goto-programs/xml_goto_trace.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening
 #include "xml_goto_trace.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_types.h>
 #include <util/namespace.h>
 #include <util/string_constant.h>
 #include <util/symbol.h>

src/statement-list/converters/statement_list_types.cpp

@@ -13,6 +13,7 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com
 
 #include <util/bitvector_types.h>
 #include <util/ieee_float.h>
+#include <util/std_types.h>
 
 signedbv_typet get_int_type()
 {

src/util/bitvector_expr.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file util/bitvector_expr.h
 /// API to expression classes for bitvectors
 
+#include "bitvector_types.h"
 #include "std_expr.h"
 
 /// \brief The byte swap expression

src/util/bitvector_types.cpp

@@ -16,13 +16,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "std_expr.h"
 #include "string2int.h"
 
-constant_exprt bv_typet::all_zeros_expr() const
+constant_exprt bitvector_typet::all_zeros_expr() const
 {
   return constant_exprt{
     make_bvrep(get_width(), [](std::size_t) { return false; }), *this};
 }
 
-constant_exprt bv_typet::all_ones_expr() const
+constant_exprt bitvector_typet::all_ones_expr() const
 {
   return constant_exprt{
     make_bvrep(get_width(), [](std::size_t) { return true; }), *this};

src/util/bitvector_types.h

@@ -12,7 +12,74 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_BITVECTOR_TYPES_H
 #define CPROVER_UTIL_BITVECTOR_TYPES_H
 
-#include "std_types.h"
+#include "expr_cast.h" // IWYU pragma: keep
+#include "mp_arith.h"
+#include "type.h"
+
+class constant_exprt;
+
+/// Base class of fixed-width bit-vector types
+///
+/// Superclass of anything represented by bits, for example integers (in 32
+/// or 64-bit representation), floating point numbers etc. In contrast, \ref
+/// integer_typet is a direct integer representation.
+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");
+  }
+
+  // helpers to create common constants
+  constant_exprt all_zeros_expr() const;
+  constant_exprt all_ones_expr() const;
+};
+
+/// Check whether a reference to a typet is a \ref bitvector_typet.
+/// \param type: Source type.
+/// \return True if \p type is a \ref bitvector_typet.
+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;
+}
 
 /// This method tests,
 /// if the given typet is a signed or unsigned bitvector.
@@ -60,10 +127,6 @@ class bv_typet : public bitvector_typet
     DATA_CHECK(
       vm, !type.get(ID_width).empty(), "bitvector type must have width");
   }
-
-  // helpers to create common constants
-  constant_exprt all_zeros_expr() const;
-  constant_exprt all_ones_expr() const;
 };
 
 /// Check whether a reference to a typet is a \ref bv_typet.

src/util/simplify_expr_int.cpp

@@ -771,9 +771,8 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr)
   // 'all zeros' in bitand yields zero
   if(new_expr.id() == ID_bitand)
   {
-    const constant_exprt zero = new_expr.type().id() == ID_bv
-                                  ? to_bv_type(new_expr.type()).all_zeros_expr()
-                                  : from_integer(0, new_expr.type());
+    const constant_exprt zero =
+      to_bitvector_type(new_expr.type()).all_zeros_expr();
     for(const auto &op : new_expr.operands())
     {
       if(op == zero)

src/util/std_types.h

@@ -900,65 +900,6 @@ inline array_typet &to_array_type(typet &type)
   return static_cast<array_typet &>(type);
 }
 
-/// Base class of fixed-width bit-vector types
-///
-/// Superclass of anything represented by bits, for example integers (in 32
-/// or 64-bit representation), floating point numbers etc. In contrast, \ref
-/// integer_typet is a direct integer representation.
-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");
-  }
-};
-
-/// Check whether a reference to a typet is a \ref bitvector_typet.
-/// \param type: Source type.
-/// \return True if \p type is a \ref bitvector_typet.
-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;
-}
-
 /// String type
 ///
 /// Represents string constants, such as `@class_identifier`.

unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp

@@ -7,6 +7,7 @@
 \*******************************************************************/
 
 #include <util/arith_tools.h>
+#include <util/bitvector_types.h>
 #include <util/namespace.h>
 #include <util/symbol_table.h>