From 5598a324cec368c386a6dc3274127928080f9439 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 19 Apr 2026 10:53:20 -0700 Subject: [PATCH 1/2] move bitvector_typet into bitvector_type.h This moves the class bitvector_typet from std_types.h into bitvector_types.h, which is more intuitive. --- src/ansi-c/c_typecheck_base.h | 1 + .../literals/convert_integer_literal.cpp | 5 +- src/goto-programs/xml_goto_trace.cpp | 1 + .../converters/statement_list_types.cpp | 1 + src/util/bitvector_expr.h | 1 + src/util/bitvector_types.h | 65 ++++++++++++++++++- src/util/std_types.h | 59 ----------------- .../extremes-go-top.cpp | 1 + 8 files changed, 72 insertions(+), 62 deletions(-) diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 37316eafa98..a22c7b7f5f7 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include class ansi_c_declarationt; +class bitvector_typet; class c_bit_field_typet; class shift_exprt; diff --git a/src/ansi-c/literals/convert_integer_literal.cpp b/src/ansi-c/literals/convert_integer_literal.cpp index f11ca833b0c..99a93978ec3 100644 --- a/src/ansi-c/literals/convert_integer_literal.cpp +++ b/src/ansi-c/literals/convert_integer_literal.cpp @@ -11,13 +11,14 @@ Author: Daniel Kroening, kroening@kroening.com #include "convert_integer_literal.h" -#include - #include +#include // IWYU pragma: keep #include #include #include +#include + exprt convert_integer_literal(const std::string &src) { bool is_unsigned=false, is_imaginary=false; diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index 446cf102059..84ab0be426c 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening #include "xml_goto_trace.h" #include +#include #include #include #include diff --git a/src/statement-list/converters/statement_list_types.cpp b/src/statement-list/converters/statement_list_types.cpp index f2ee5e84d18..ffbcd13180f 100644 --- a/src/statement-list/converters/statement_list_types.cpp +++ b/src/statement-list/converters/statement_list_types.cpp @@ -13,6 +13,7 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #include #include +#include signedbv_typet get_int_type() { diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h index 1275925eb62..64f7d55330c 100644 --- a/src/util/bitvector_expr.h +++ b/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 diff --git a/src/util/bitvector_types.h b/src/util/bitvector_types.h index ba7a7cb7e67..d4ae4d78cca 100644 --- a/src/util/bitvector_types.h +++ b/src/util/bitvector_types.h @@ -12,7 +12,70 @@ 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"); + } +}; + +/// 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(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. diff --git a/src/util/std_types.h b/src/util/std_types.h index b875c5b0023..25f04e66328 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -900,65 +900,6 @@ inline array_typet &to_array_type(typet &type) return static_cast(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(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`. diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp index 1bb6303e750..32d87327c6d 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp @@ -7,6 +7,7 @@ \*******************************************************************/ #include +#include #include #include From 1166ac006dc34951644156af1cd70900d772c528 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 19 Apr 2026 10:57:42 -0700 Subject: [PATCH 2/2] push up all_zeros_expr and all_ones_expr helpers to bitvector_typet This pushes up the two helper methods all_zeros_expr and all_ones_expr from bv_typet to bitvector_typet, as it is often desirable to create all-zeros and all-ones constants for the other bitvector types as well. --- src/util/bitvector_types.cpp | 4 ++-- src/util/bitvector_types.h | 8 ++++---- src/util/simplify_expr_int.cpp | 5 ++--- 3 files changed, 8 insertions(+), 9 deletions(-) diff --git a/src/util/bitvector_types.cpp b/src/util/bitvector_types.cpp index ea6fd054ef1..efc0d352289 100644 --- a/src/util/bitvector_types.cpp +++ b/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}; diff --git a/src/util/bitvector_types.h b/src/util/bitvector_types.h index d4ae4d78cca..f3db88296f1 100644 --- a/src/util/bitvector_types.h +++ b/src/util/bitvector_types.h @@ -61,6 +61,10 @@ class bitvector_typet : public 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 bitvector_typet. @@ -123,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. diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 48ce5962bc2..0c393ad4f7b 100644 --- a/src/util/simplify_expr_int.cpp +++ b/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)