diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp index 8bcc2554d2f..58756b8c45f 100644 --- a/src/solvers/lowering/byte_operators.cpp +++ b/src/solvers/lowering/byte_operators.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include "flatten_byte_extract_exceptions.h" @@ -275,6 +276,26 @@ static exprt unpack_rec( ns, unpack_byte_array); } + else if(src.id() == ID_string_constant) + { + return unpack_rec( + to_string_constant(src).to_array_expr(), + little_endian, + offset_bytes, + max_bytes, + ns, + unpack_byte_array); + } + else if(src.id() == ID_constant && src.type().id() == ID_string) + { + return unpack_rec( + string_constantt(to_constant_expr(src).get_value()).to_array_expr(), + little_endian, + offset_bytes, + max_bytes, + ns, + unpack_byte_array); + } else if(src.type().id()!=ID_empty) { // a basic type; we turn that into extractbits while considering diff --git a/unit/solvers/lowering/byte_operators.cpp b/unit/solvers/lowering/byte_operators.cpp index 81fe96e3bfc..19d2e824ca7 100644 --- a/unit/solvers/lowering/byte_operators.cpp +++ b/unit/solvers/lowering/byte_operators.cpp @@ -21,6 +21,7 @@ #include #include #include +#include #include SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]") @@ -90,6 +91,35 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]") } } + GIVEN("A a byte_extract from a string constant") + { + string_constantt s("ABCD"); + const byte_extract_exprt be1( + ID_byte_extract_little_endian, + s, + from_integer(1, index_type()), + unsignedbv_typet(16)); + + THEN("byte_extract lowering yields the expected value") + { + const exprt lower_be1 = lower_byte_extract(be1, ns); + + REQUIRE(!has_subexpr(lower_be1, ID_byte_extract_little_endian)); + REQUIRE(lower_be1.type() == be1.type()); + REQUIRE( + lower_be1 == from_integer((int{'C'} << 8) + 'B', unsignedbv_typet(16))); + + byte_extract_exprt be2 = be1; + be2.id(ID_byte_extract_big_endian); + const exprt lower_be2 = lower_byte_extract(be2, ns); + + REQUIRE(!has_subexpr(lower_be2, ID_byte_extract_big_endian)); + REQUIRE(lower_be2.type() == be2.type()); + REQUIRE( + lower_be2 == from_integer((int{'B'} << 8) + 'C', unsignedbv_typet(16))); + } + } + GIVEN("A collection of types") { unsignedbv_typet u8(8);