Merge pull request #8350 from diffblue/bv_typet-helpers

add two helpers for bv_typet

Author: tautschnig

src/util/bitvector_types.cpp

@@ -16,6 +16,18 @@ Author: Daniel Kroening, [email protected]
 #include "std_expr.h"
 #include "string2int.h"
 
+constant_exprt bv_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
+{
+  return constant_exprt{
+    make_bvrep(get_width(), [](std::size_t) { return true; }), *this};
+}
+
 std::size_t fixedbv_typet::get_integer_bits() const
 {
   const irep_idt integer_bits = get(ID_integer_bits);

src/util/bitvector_types.h

@@ -60,6 +60,10 @@ 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/lower_byte_operators.cpp

@@ -579,7 +579,7 @@ static exprt unpack_array_vector(
         numeric_cast_v<std::size_t>(std::min(
           *offset_bytes - (*offset_bytes % el_bytes),
           *num_elements * el_bytes)),
-        from_integer(0, bv_typet{bits_per_byte}));
+        bv_typet{bits_per_byte}.all_zeros_expr());
     }
   }
 
@@ -791,7 +791,7 @@ static array_exprt unpack_struct(
       byte_operands.resize(
         byte_operands.size() +
           numeric_cast_v<std::size_t>(*component_bits / bits_per_byte),
-        from_integer(0, bv_typet{bits_per_byte}));
+        bv_typet{bits_per_byte}.all_zeros_expr());
     }
     else
     {
@@ -2417,7 +2417,7 @@ static exprt lower_byte_update(
     if(bit_width > type_bits)
     {
       val_before = concatenation_exprt{
-        from_integer(0, bv_typet{bit_width - type_bits}),
+        bv_typet{bit_width - type_bits}.all_zeros_expr(),
         val_before,
         bv_typet{bit_width}};
 
@@ -2492,7 +2492,7 @@ static exprt lower_byte_update(
     if(bit_width > update_size_bits)
     {
       zero_extended = concatenation_exprt{
-        from_integer(0, bv_typet{bit_width - update_size_bits}),
+        bv_typet{bit_width - update_size_bits}.all_zeros_expr(),
         value,
         bv_typet{bit_width}};