Skip to content

Commit afda322

Browse files
committed
Implement extract_bits conversion
This only works so long as the bits to extract are constant values. This is the same limitation as is present in the old back end. The reason for this is limitation is due to the way the `extract` operation is defined in the smtlib version of bitvector theory. It may be possible to work around this limitation but the work around is unlikely to be trivial.
1 parent 29799b4 commit afda322

File tree

2 files changed

+26
-0
lines changed

2 files changed

+26
-0
lines changed

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -733,6 +733,11 @@ static smt_termt convert_expr_to_smt(const extractbit_exprt &extract_bit)
733733

734734
static smt_termt convert_expr_to_smt(const extractbits_exprt &extract_bits)
735735
{
736+
const smt_termt from = convert_expr_to_smt(extract_bits.src());
737+
const auto upper_value = numeric_cast<std::size_t>(extract_bits.upper());
738+
const auto lower_value = numeric_cast<std::size_t>(extract_bits.lower());
739+
if(upper_value && lower_value)
740+
return smt_bit_vector_theoryt::extract(*upper_value, *lower_value)(from);
736741
UNIMPLEMENTED_FEATURE(
737742
"Generation of SMT formula for extract bits expression: " +
738743
extract_bits.pretty());

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -819,6 +819,27 @@ SCENARIO(
819819
}
820820
}
821821

822+
TEST_CASE(
823+
"expr to smt conversion for extract bits expressions",
824+
"[core][smt2_incremental]")
825+
{
826+
const typet operand_type = unsignedbv_typet{8};
827+
const exprt input = extractbits_exprt{
828+
symbol_exprt{"foo", operand_type},
829+
from_integer(4, operand_type),
830+
from_integer(2, operand_type),
831+
unsignedbv_typet{3}};
832+
const smt_termt expected_result = smt_bit_vector_theoryt::extract(4, 2)(
833+
smt_identifier_termt{"foo", smt_bit_vector_sortt{8}});
834+
CHECK(convert_expr_to_smt(input) == expected_result);
835+
const cbmc_invariants_should_throwt invariants_throw;
836+
CHECK_THROWS(convert_expr_to_smt(extractbits_exprt{
837+
symbol_exprt{"foo", operand_type},
838+
symbol_exprt{"bar", operand_type},
839+
symbol_exprt{"bar", operand_type},
840+
unsignedbv_typet{3}}));
841+
}
842+
822843
TEST_CASE("expr to smt conversion for type casts", "[core][smt2_incremental]")
823844
{
824845
const symbol_exprt bool_expr{"foo", bool_typet{}};

0 commit comments

Comments
 (0)