diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 04f62124ba0..d54d18d761a 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -351,19 +351,6 @@ class recursion_set_entryt } }; -/// Get max value for an integer type -/// \param type: -/// Type to find maximum value for -/// \return Maximum integer value -static mp_integer max_value(const typet &type) -{ - if(type.id() == ID_signedbv) - return to_signedbv_type(type).largest(); - else if(type.id() == ID_unsignedbv) - return to_unsignedbv_type(type).largest(); - UNREACHABLE; -} - /// Initialise length and data fields for a nondeterministic String structure. /// /// If the structure is not a nondeterministic structure, the call results in @@ -458,7 +445,9 @@ void initialize_nondet_string_fields( code.add(code_assumet(binary_relation_exprt(length_expr, ID_ge, min_length))); // assume (length_expr <= max_input_length) - if(max_nondet_string_length <= max_value(length_expr.type())) + if( + max_nondet_string_length <= + to_integer_bitvector_type(length_expr.type()).largest()) { exprt max_length = from_integer(max_nondet_string_length, length_expr.type()); diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 231d21a4fd9..0513b34c8a5 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -377,18 +377,8 @@ bool generate_ansi_c_start_function( } // assume envp_size is INTMAX-1 - mp_integer max; - - if(envp_size_symbol.type.id()==ID_signedbv) - { - max=to_signedbv_type(envp_size_symbol.type).largest(); - } - else if(envp_size_symbol.type.id()==ID_unsignedbv) - { - max=to_unsignedbv_type(envp_size_symbol.type).largest(); - } - else - UNREACHABLE; + const mp_integer max = + to_integer_bitvector_type(envp_size_symbol.type).largest(); exprt max_minus_one=from_integer(max-1, envp_size_symbol.type); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 7e81fe61fac..b60b1593355 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "arith_tools.h" -#include "bv_arithmetic.h" #include "byte_operators.h" #include "config.h" #include "expr_util.h" @@ -1879,8 +1878,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr) if(expr.op0().type().id()==ID_unsignedbv || expr.op0().type().id()==ID_signedbv) { - bv_spect spec(expr.op0().type()); - mp_integer max(spec.max_value()); + mp_integer max(to_integer_bitvector_type(expr.op0().type()).largest()); if(expr.id()==ID_notequal) { diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp index 2b391db5b04..ccdf13c4147 100644 --- a/src/util/std_types.cpp +++ b/src/util/std_types.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "std_types.h" #include "arith_tools.h" +#include "bv_arithmetic.h" #include "namespace.h" #include "std_expr.h" #include "string2int.h" @@ -161,52 +162,27 @@ mp_integer range_typet::get_to() const return string2integer(get_string(ID_to)); } -mp_integer signedbv_typet::smallest() const +mp_integer integer_bitvector_typet::smallest() const { - return -power(2, get_width()-1); + return bv_spect(*this).min_value(); } -mp_integer signedbv_typet::largest() const +mp_integer integer_bitvector_typet::largest() const { - return power(2, get_width()-1)-1; + return bv_spect(*this).max_value(); } -constant_exprt signedbv_typet::zero_expr() const +constant_exprt integer_bitvector_typet::zero_expr() const { return from_integer(0, *this); } -constant_exprt signedbv_typet::smallest_expr() const +constant_exprt integer_bitvector_typet::smallest_expr() const { return from_integer(smallest(), *this); } -constant_exprt signedbv_typet::largest_expr() const -{ - return from_integer(largest(), *this); -} - -mp_integer unsignedbv_typet::smallest() const -{ - return 0; -} - -mp_integer unsignedbv_typet::largest() const -{ - return power(2, get_width())-1; -} - -constant_exprt unsignedbv_typet::zero_expr() const -{ - return from_integer(0, *this); -} - -constant_exprt unsignedbv_typet::smallest_expr() const -{ - return from_integer(smallest(), *this); -} - -constant_exprt unsignedbv_typet::largest_expr() const +constant_exprt integer_bitvector_typet::largest_expr() const { return from_integer(largest(), *this); } diff --git a/src/util/std_types.h b/src/util/std_types.h index 454925b2275..9e650b288da 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -1167,20 +1167,74 @@ inline bv_typet &to_bv_type(typet &type) return static_cast(type); } -/// Fixed-width bit-vector with unsigned binary interpretation -class unsignedbv_typet:public bitvector_typet +/// Fixed-width bit-vector representing a signed or unsigned integer +class integer_bitvector_typet : public bitvector_typet { public: - explicit unsignedbv_typet(std::size_t width): - bitvector_typet(ID_unsignedbv, width) + integer_bitvector_typet(const irep_idt &id, std::size_t width) + : bitvector_typet(id, width) { } + /// Return the smallest value that can be represented using this type. mp_integer smallest() const; + /// Return the largest value that can be represented using this type. mp_integer largest() const; + + // If we ever need any of the following three methods in \ref fixedbv_typet or + // \ref floatbv_typet, we might want to move them to a new class + // numeric_bitvector_typet, which would be between integer_bitvector_typet and + // bitvector_typet in the hierarchy. + + /// Return an expression representing the smallest value of this type. constant_exprt smallest_expr() const; + /// Return an expression representing the zero value of this type. constant_exprt zero_expr() const; + /// Return an expression representing the largest value of this type. constant_exprt largest_expr() const; +}; + +/// Check whether a reference to a typet is an \ref integer_bitvector_typet. +/// \param type: Source type. +/// \return True if \p type is an \ref integer_bitvector_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_signedbv || type.id() == ID_unsignedbv; +} + +/// \brief Cast a typet to an \ref integer_bitvector_typet +/// +/// This is an unchecked conversion. \a type must be known to be \ref +/// integer_bitvector_typet. Will fail with a precondition violation if type +/// doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref integer_bitvector_typet. +inline const integer_bitvector_typet & +to_integer_bitvector_type(const typet &type) +{ + PRECONDITION(can_cast_type(type)); + + return static_cast(type); +} + +/// \copydoc to_integer_bitvector_type(const typet &type) +inline integer_bitvector_typet &to_integer_bitvector_type(typet &type) +{ + PRECONDITION(can_cast_type(type)); + + return static_cast(type); +} + +/// Fixed-width bit-vector with unsigned binary interpretation +class unsignedbv_typet : public integer_bitvector_typet +{ +public: + explicit unsignedbv_typet(std::size_t width) + : integer_bitvector_typet(ID_unsignedbv, width) + { + } static void check( const typet &type, @@ -1223,20 +1277,14 @@ inline unsignedbv_typet &to_unsignedbv_type(typet &type) } /// Fixed-width bit-vector with two's complement interpretation -class signedbv_typet:public bitvector_typet +class signedbv_typet : public integer_bitvector_typet { public: - explicit signedbv_typet(std::size_t width): - bitvector_typet(ID_signedbv, width) + explicit signedbv_typet(std::size_t width) + : integer_bitvector_typet(ID_signedbv, width) { } - mp_integer smallest() const; - mp_integer largest() const; - constant_exprt smallest_expr() const; - constant_exprt zero_expr() const; - constant_exprt largest_expr() const; - static void check( const typet &type, const validation_modet vm = validation_modet::INVARIANT)