diff --git a/src/util/bitvector_types.cpp b/src/util/bitvector_types.cpp index 24e098fc217..ea6fd054ef1 100644 --- a/src/util/bitvector_types.cpp +++ b/src/util/bitvector_types.cpp @@ -16,6 +16,18 @@ Author: Daniel Kroening, kroening@kroening.com #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); diff --git a/src/util/bitvector_types.h b/src/util/bitvector_types.h index 777123354ba..2f8a2c3b9ad 100644 --- a/src/util/bitvector_types.h +++ b/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. diff --git a/src/util/lower_byte_operators.cpp b/src/util/lower_byte_operators.cpp index 889f851fc2c..701214d1936 100644 --- a/src/util/lower_byte_operators.cpp +++ b/src/util/lower_byte_operators.cpp @@ -579,7 +579,7 @@ static exprt unpack_array_vector( numeric_cast_v(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(*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}};