Lowering of byte_extract over string constants
These need to be handled like arrays of characters.
This commit is contained in:
parent
c580d94eeb
commit
9a67ec4d55
|
@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
||||||
#include <util/pointer_offset_size.h>
|
#include <util/pointer_offset_size.h>
|
||||||
#include <util/replace_symbol.h>
|
#include <util/replace_symbol.h>
|
||||||
#include <util/simplify_expr.h>
|
#include <util/simplify_expr.h>
|
||||||
|
#include <util/string_constant.h>
|
||||||
|
|
||||||
#include "flatten_byte_extract_exceptions.h"
|
#include "flatten_byte_extract_exceptions.h"
|
||||||
|
|
||||||
|
@ -275,6 +276,26 @@ static exprt unpack_rec(
|
||||||
ns,
|
ns,
|
||||||
unpack_byte_array);
|
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)
|
else if(src.type().id()!=ID_empty)
|
||||||
{
|
{
|
||||||
// a basic type; we turn that into extractbits while considering
|
// a basic type; we turn that into extractbits while considering
|
||||||
|
|
|
@ -21,6 +21,7 @@
|
||||||
#include <util/simplify_expr.h>
|
#include <util/simplify_expr.h>
|
||||||
#include <util/simplify_expr_class.h>
|
#include <util/simplify_expr_class.h>
|
||||||
#include <util/std_types.h>
|
#include <util/std_types.h>
|
||||||
|
#include <util/string_constant.h>
|
||||||
#include <util/symbol_table.h>
|
#include <util/symbol_table.h>
|
||||||
|
|
||||||
SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
|
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")
|
GIVEN("A collection of types")
|
||||||
{
|
{
|
||||||
unsignedbv_typet u8(8);
|
unsignedbv_typet u8(8);
|
||||||
|
|
Loading…
Reference in New Issue