Merge pull request #4352 from antlechner/antonia/bv-min-max-refactor

Refactor code related to bitvector type min/max values

Author: tautschnig

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());

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);
 

src/util/simplify_expr_int.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 
 #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)
     {

src/util/std_types.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #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);
 }

src/util/std_types.h

@@ -1167,20 +1167,74 @@ inline bv_typet &to_bv_type(typet &type)
   return static_cast<bv_typet &>(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<integer_bitvector_typet>(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<integer_bitvector_typet>(type));
+
+  return static_cast<const integer_bitvector_typet &>(type);
+}
+
+/// \copydoc to_integer_bitvector_type(const typet &type)
+inline integer_bitvector_typet &to_integer_bitvector_type(typet &type)
+{
+  PRECONDITION(can_cast_type<integer_bitvector_typet>(type));
+
+  return static_cast<integer_bitvector_typet &>(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)