Skip to content

Use array comprehension for large byte_extract lowering #8840

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
tautschnig wants to merge 1 commit into
base: develop
Choose a base branch
from
Open

Use array comprehension for large byte_extract lowering #8840

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 20 additions & 11 deletions src/util/lower_byte_operators.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include "c_types.h"
#include "endianness_map.h"
#include "expr_util.h"
#include "magic.h"
#include "namespace.h"
#include "narrow.h"
#include "pointer_offset_size.h"
Expand Down Expand Up @@ -1112,7 +1113,13 @@ static exprt lower_byte_extract_array_vector(
else
num_elements = numeric_cast<std::size_t>(to_vector_type(src.type()).size());

if(num_elements.has_value())
// For large arrays, element-by-element expansion creates N expressions
// that are each recursively lowered and simplified, resulting in O(N^2)
// behaviour. Use array_comprehension_exprt (below) instead, which
// represents the same semantics with a single symbolic expression.
if(
num_elements.has_value() &&
(src.type().id() != ID_array || *num_elements <= MAX_FLATTENED_ARRAY_SIZE))
{
exprt::operandst operands;
operands.reserve(*num_elements);
Expand Down Expand Up @@ -1797,8 +1804,8 @@ static exprt lower_byte_update_array_vector_non_const(

// compute the number of bytes (from the update value) that are going to be
// consumed for updating the first element
const exprt update_size =
from_integer(value_as_byte_array.operands().size(), subtype_size.type());
const exprt update_size = typecast_exprt::conditional_cast(
to_array_type(value_as_byte_array.type()).size(), subtype_size.type());
exprt initial_bytes = minus_exprt{subtype_size, update_offset};
exprt update_bound;
if(non_const_update_bound.has_value())
Expand All @@ -1808,9 +1815,6 @@ static exprt lower_byte_update_array_vector_non_const(
}
else
{
DATA_INVARIANT(
value_as_byte_array.id() == ID_array,
"value should be an array expression if the update bound is constant");
update_bound = update_size;
}
initial_bytes = if_exprt{
Expand All @@ -1833,12 +1837,16 @@ static exprt lower_byte_update_array_vector_non_const(

if(value_as_byte_array.id() != ID_array)
{
exprt update_bound =
non_const_update_bound.has_value()
? *non_const_update_bound
: to_array_type(value_as_byte_array.type()).size();
return lower_byte_update_array_vector_unbounded(
src,
subtype,
subtype_size,
value_as_byte_array,
*non_const_update_bound,
update_bound,
initial_bytes,
first_index,
first_update_value,
Expand Down Expand Up @@ -2333,11 +2341,12 @@ static exprt lower_byte_update(
{
if(value_as_byte_array.id() != ID_array)
{
DATA_INVARIANT(
non_const_update_bound.has_value(),
"constant update bound should yield an array expression");
exprt update_bound =
non_const_update_bound.has_value()
? *non_const_update_bound
: to_array_type(value_as_byte_array.type()).size();
return lower_byte_update_byte_array_vector_non_const(
src, *subtype, value_as_byte_array, *non_const_update_bound, ns);
src, *subtype, value_as_byte_array, update_bound, ns);
}

return lower_byte_update_byte_array_vector(
Expand Down
46 changes: 46 additions & 0 deletions unit/util/lower_byte_operators.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,54 @@
#include <util/string_constant.h>
#include <util/symbol_table.h>

#include <util/magic.h>

#include <testing-utils/use_catch.h>

TEST_CASE(
"byte update with large array value",
"[core][util][lowering][byte_update]")
{
// this test does require a proper architecture to be set so that byte update
// uses adequate endianness
cmdlinet cmdline;
config.set(cmdline);

const symbol_tablet symbol_table;
const namespacet ns(symbol_table);

// Target: a char array larger than the update value
const std::size_t update_size = MAX_FLATTENED_ARRAY_SIZE + 1;
const std::size_t target_size = 2 * update_size;
const array_typet target_type{
unsignedbv_typet{config.ansi_c.char_width},
from_integer(target_size, size_type())};
const symbol_exprt target{"target", target_type};

// Update value: a char array with more than MAX_FLATTENED_ARRAY_SIZE elements
// so that lower_byte_extract produces an array_comprehension_exprt
const array_typet update_type{
unsignedbv_typet{config.ansi_c.char_width},
from_integer(update_size, size_type())};
const symbol_exprt update_value{"update_value", update_type};

// Constant offset
const byte_update_exprt bu{
ID_byte_update_little_endian,
target,
from_integer(0, c_index_type()),
update_value,
config.ansi_c.char_width};

// This must not crash (previously triggered an invariant violation because
// lower_byte_extract produces an array_comprehension_exprt for large arrays,
// which was not handled by lower_byte_update).
const exprt result = lower_byte_update(bu, ns);
REQUIRE(result.type() == target_type);
REQUIRE(!has_subexpr(result, ID_byte_update_little_endian));
REQUIRE(!has_subexpr(result, ID_byte_update_big_endian));
}

TEST_CASE("byte extract and bits", "[core][util][lowering][byte_extract]")
{
// this test does require a proper architecture to be set so that byte extract
Expand Down
Loading