From 3eb2a3d5a993e0c715c92fb8eac3466b37cb8b65 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 4 Feb 2024 09:05:15 -0800 Subject: [PATCH] introduce update_bits_exprt This introduces update_bits_exprt, which allows replacing parts of a bit-vector identified by a (potentially variable) index by a given bit-vector. This supersedes with_exprt in the case of single-bit operands. --- src/solvers/Makefile | 1 + src/solvers/flattening/boolbv.h | 4 + src/solvers/flattening/boolbv_update_bits.cpp | 16 ++++ src/solvers/smt2/smt2_conv.cpp | 9 ++ src/solvers/smt2/smt2_conv.h | 2 + src/util/bitvector_expr.cpp | 30 +++++++ src/util/bitvector_expr.h | 86 +++++++++++++++++++ src/util/irep_ids.def | 1 + 8 files changed, 149 insertions(+) create mode 100644 src/solvers/flattening/boolbv_update_bits.cpp diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 64f606312af4..ccf66d4cfa60 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -128,6 +128,7 @@ SRC = $(BOOLEFORCE_SRC) \ flattening/boolbv_unary_minus.cpp \ flattening/boolbv_union.cpp \ flattening/boolbv_update.cpp \ + flattening/boolbv_update_bits.cpp \ flattening/boolbv_width.cpp \ flattening/boolbv_with.cpp \ flattening/bv_dimacs.cpp \ diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 2daa9d26cc1d..5992bdc4b0df 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -39,6 +39,7 @@ class overflow_result_exprt; class replication_exprt; class unary_overflow_exprt; class union_typet; +class update_bits_exprt; class boolbvt:public arrayst { @@ -176,6 +177,7 @@ class boolbvt:public arrayst virtual bvt convert_member(const member_exprt &expr); virtual bvt convert_with(const with_exprt &expr); virtual bvt convert_update(const update_exprt &); + virtual bvt convert_update_bits(const update_bits_exprt &); virtual bvt convert_case(const exprt &expr); virtual bvt convert_cond(const cond_exprt &); virtual bvt convert_shift(const binary_exprt &expr); @@ -196,6 +198,8 @@ class boolbvt:public arrayst virtual bvt convert_saturating_add_sub(const binary_exprt &expr); virtual bvt convert_overflow_result(const overflow_result_exprt &expr); + bvt convert_update_bits(bvt src, const exprt &index, const bvt &new_value); + void convert_with( const typet &type, const exprt &where, diff --git a/src/solvers/flattening/boolbv_update_bits.cpp b/src/solvers/flattening/boolbv_update_bits.cpp new file mode 100644 index 000000000000..1d7212b5d31f --- /dev/null +++ b/src/solvers/flattening/boolbv_update_bits.cpp @@ -0,0 +1,16 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include + +#include "boolbv.h" + +bvt boolbvt::convert_update_bits(const update_bits_exprt &expr) +{ + return convert_bv(expr.lower()); +} diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 5b7ab53c4ea5..9ccf7dda4668 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1683,6 +1683,10 @@ void smt2_convt::convert_expr(const exprt &expr) { convert_update(to_update_expr(expr)); } + else if(expr.id() == ID_update_bits) + { + convert_update_bits(to_update_bits_expr(expr)); + } else if(expr.id() == ID_object_address) { out << "(object-address "; @@ -4338,6 +4342,11 @@ void smt2_convt::convert_update(const update_exprt &expr) SMT2_TODO("smt2_convt::convert_update to be implemented"); } +void smt2_convt::convert_update_bits(const update_bits_exprt &expr) +{ + return convert_expr(expr.lower()); +} + void smt2_convt::convert_index(const index_exprt &expr) { const typet &array_op_type = expr.array().type(); diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index 9f83687f8be9..16c784626410 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_SMT2_SMT2_CONV_H #define CPROVER_SOLVERS_SMT2_SMT2_CONV_H +#include #include #include #include @@ -149,6 +150,7 @@ class smt2_convt : public stack_decision_proceduret void convert_with(const with_exprt &expr); void convert_update(const update_exprt &); + void convert_update_bits(const update_bits_exprt &); void convert_expr(const exprt &); void convert_type(const typet &); diff --git a/src/util/bitvector_expr.cpp b/src/util/bitvector_expr.cpp index adeaec40305f..eb8fa4807a58 100644 --- a/src/util/bitvector_expr.cpp +++ b/src/util/bitvector_expr.cpp @@ -42,6 +42,36 @@ extractbits_exprt::extractbits_exprt( from_integer(_lower, integer_typet())); } +exprt update_bits_exprt::lower() const +{ + const auto width = to_bitvector_type(type()).get_width(); + const auto new_value_width = + to_bitvector_type(new_value().type()).get_width(); + auto src_bv_type = bv_typet(width); + + // build a mask 1...1 0...0 + auto mask_bv = make_bvrep(width, [new_value_width](std::size_t index) { + return index >= new_value_width; + }); + auto mask_expr = constant_exprt(mask_bv, src_bv_type); + + // shift the mask by the index + auto mask_shifted = shl_exprt(mask_expr, index()); + + auto src_masked = + bitand_exprt(typecast_exprt(src(), src_bv_type), mask_shifted); + + // zero-extend or shrink the replacement bits to match src + auto new_value_casted = typecast_exprt(new_value(), src_bv_type); + + // shift the replacement bits + auto new_value_shifted = shl_exprt(new_value_casted, index()); + + // or the masked src and the shifted replacement bits + return typecast_exprt( + bitor_exprt(src_masked, new_value_shifted), src().type()); +} + exprt popcount_exprt::lower() const { // Hacker's Delight, variant pop0: diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h index 516634c52de5..3d40b3567982 100644 --- a/src/util/bitvector_expr.h +++ b/src/util/bitvector_expr.h @@ -531,6 +531,92 @@ inline extractbits_exprt &to_extractbits_expr(exprt &expr) return ret; } +/// \brief Replaces a sub-range of a bit-vector operand +class update_bits_exprt : public expr_protectedt +{ +public: + /// Replace the bits [\p _index .. \p _index + size] from \p _src + /// where size is the width of \p _new_value to produce a result of + /// the same type as \p _src. The index counts from the + /// least-significant bit. + update_bits_exprt(exprt _src, exprt _index, exprt _new_value) + : expr_protectedt( + ID_update_bits, + _src.type(), + {_src, std::move(_index), std::move(_new_value)}) + { + } + + update_bits_exprt(exprt _src, const std::size_t _index, exprt _new_value); + + exprt &src() + { + return op0(); + } + + exprt &index() + { + return op1(); + } + + exprt &new_value() + { + return op2(); + } + + const exprt &src() const + { + return op0(); + } + + const exprt &index() const + { + return op1(); + } + + const exprt &new_value() const + { + return op2(); + } + + static void check( + const exprt &expr, + const validation_modet vm = validation_modet::INVARIANT) + { + validate_operands(expr, 3, "update_bits must have three operands"); + } + + /// A lowering to masking, shifting, or. + exprt lower() const; +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_update_bits; +} + +/// \brief Cast an exprt to an \ref update_bits_exprt +/// +/// \a expr must be known to be \ref update_bits_exprt. +/// +/// \param expr: Source expression +/// \return Object of type \ref update_bits_exprt +inline const update_bits_exprt &to_update_bits_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_update_bits); + update_bits_exprt::check(expr); + return static_cast(expr); +} + +/// \copydoc to_update_bits_expr(const exprt &) +inline update_bits_exprt &to_update_bits_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_update_bits); + update_bits_exprt::check(expr); + return static_cast(expr); +} + /// \brief Bit-vector replication class replication_exprt : public binary_exprt { diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index ecc73c69b42e..c06f62930555 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -185,6 +185,7 @@ IREP_ID_ONE(exists) IREP_ID_ONE(repeat) IREP_ID_ONE(extractbit) IREP_ID_ONE(extractbits) +IREP_ID_ONE(update_bits) IREP_ID_TWO(C_reference, #reference) IREP_ID_TWO(C_rvalue_reference, #rvalue_reference) IREP_ID_ONE(true)